Faster error backtraces prototype

src/1/Conv.sml

@@ -80,21 +80,21 @@ val REWR_CONV_A  = REWR_CONV0 (PART_MATCH_A,    "REWR_CONV_A")
  * Revised Michael Norrish 2000.03.27                                   *
  *    now passes on information about nested failure                    *
  *----------------------------------------------------------------------*)
-
+(*
 fun set_origin fnm
     {origin_function, origin_structure, source_location, message} =
   if Lib.mem origin_function ["RAND_CONV", "RATOR_CONV", "ABS_CONV"]
       andalso origin_structure = "Conv"
       then ERRloc fnm source_location message
   else ERRloc fnm source_location (origin_function ^ ": " ^ message)
-
+*)
 fun RAND_CONV conv tm =
    let
       val {Rator, Rand} =
          dest_comb tm handle HOL_ERR _ => raise ERR "RAND_CONV" "not a comb"
       val newrand =
          conv Rand
-         handle HOL_ERR e => raise set_origin "RAND_CONV" e
+         handle (e as HOL_ERR _) => raise wrap_exn "Conv" "RAND_CONV" e
    in
       AP_TERM Rator newrand
       handle HOL_ERR {message, ...} =>
@@ -117,7 +117,7 @@ fun RATOR_CONV conv tm =
          dest_comb tm handle HOL_ERR _ => raise ERR "RATOR_CONV" "not a comb"
       val newrator =
          conv Rator
-         handle HOL_ERR e => raise set_origin "RATOR_CONV" e
+         handle (e as HOL_ERR _) => raise wrap_exn "Conv" "RATOR_CONV" e
    in
       AP_THM newrator Rand
       handle HOL_ERR {message, ...} =>
@@ -158,7 +158,7 @@ fun ABS_CONV conv tm =
                  in
                     TRANS (TRANS th1 eq_thm') th2
                  end
-                 handle HOL_ERR e => raise set_origin "ABS_CONV" e
+                 handle (e as HOL_ERR _) => raise wrap_exn "Conv" "ABS_CONV" e
         end
     | _ => raise ERR "ABS_CONV" "Term not an abstraction"
 
@@ -927,9 +927,12 @@ in
               IMP_ANTISYM_RULE imp1 (DISCH otm thm2)
            end
       end
+      handle HOL_ERR _ => raise ERR "EXISTS_AND_CONV" ""
+(* TODO fix
       handle e as HOL_ERR {origin_structure = "Conv",
                            origin_function = "EXISTS_AND_CONV", ...} => raise e
            | HOL_ERR _ => raise ERR "EXISTS_AND_CONV" ""
+*)
 end
 
 (*----------------------------------------------------------------------*
@@ -959,9 +962,12 @@ in
                      (mk_exists {Bvar = x,
                                  Body = mk_conj {conj1 = P, conj2 = Q}}))
       end
+      handle HOL_ERR _ => raise ERR "AND_EXISTS_CONV" ""
+(* TODO fix
       handle e as HOL_ERR {origin_structure = "Conv",
                            origin_function = "AND_EXISTS_CONV", ...} => raise e
            | HOL_ERR _ => raise ERR "AND_EXISTS_CONV" ""
+*)
 end
 
 (*----------------------------------------------------------------------*
@@ -1099,9 +1105,12 @@ in
                IMP_ANTISYM_RULE imp1 (DISCH otm imp2)
             end
       end
+      handle HOL_ERR _ => raise ERR "FORALL_OR_CONV" ""
+(* TODO fix
       handle e as HOL_ERR {origin_structure = "Conv",
                            origin_function = "FORALL_OR_CONV", ...} => raise e
            | HOL_ERR _ => raise ERR "FORALL_OR_CONV" ""
+*)
 end
 
 (*----------------------------------------------------------------------*
@@ -1130,9 +1139,12 @@ in
       else SYM (FORALL_OR_CONV
                   (mk_forall {Bvar = x, Body = mk_disj {disj1 = P, disj2 = Q}}))
    end
+   handle HOL_ERR _ => raise ERR "OR_FORALL_CONV" ""
+(* TODO fix
    handle e as HOL_ERR {origin_structure = "Conv",
                         origin_function = "OR_FORALL_CONV", ...} => raise e
         | HOL_ERR _ => raise ERR "OR_FORALL_CONV" ""
+*)
 end
 
 (*----------------------------------------------------------------------*
@@ -1257,9 +1269,12 @@ in
                  IMP_ANTISYM_RULE imp1 imp2
               end
       end
+      handle HOL_ERR _ => raise ERR "FORALL_IMP_CONV" ""
+(* TODO FIX
       handle e as HOL_ERR {origin_structure = "Conv",
                            origin_function = "FORALL_IMP_CONV", ...} => raise e
            | HOL_ERR _ => raise ERR "FORALL_IMP_CONV" ""
+*)
 end
 
 (*----------------------------------------------------------------------*
@@ -1385,9 +1400,12 @@ in
               IMP_ANTISYM_RULE imp1 imp2
            end
     end
+    handle  HOL_ERR _ => raise ERR "EXISTS_IMP_CONV" ""
+(* TODO fix
     handle e as HOL_ERR {origin_structure = "Conv",
                          origin_function = "EXISTS_IMP_CONV", ...} => raise e
              | HOL_ERR _ => raise ERR "EXISTS_IMP_CONV" ""
+*)
 end
 
 (*----------------------------------------------------------------------*
@@ -1499,10 +1517,13 @@ in
                       IMP_ANTISYM_RULE imp1 imp2
                    end
            end
+           handle HOL_ERR _ => err ""
+   (*TODO fix
            handle e as HOL_ERR
                          {origin_structure = "Conv",
                           origin_function = "X_SKOLEM_CONV", ...} => raise e
                  | HOL_ERR _ => err ""
+   *)
    (* val X_SKOLEM_CONV = w "X_SKOLEM_CONV" X_SKOLEM_CONV *)
 end
 

src/1/Mutual.sml

@@ -377,10 +377,13 @@ fun MUTUAL_INDUCT_THEN1 th =
       handle HOL_ERR _
        => raise ERR "MUTUAL_INDUCT_THEN" "tactic application error"
    end
+   handle HOL_ERR _ => raise ERR "MUTUAL_INDUCT_THEN" ""
+(* TODO fix:
    handle (e as HOL_ERR
                    {origin_structure = "Mutual",
                     origin_function = "MUTUAL_INDUCT_THEN",...}) => raise e
         | _ => raise ERR "MUTUAL_INDUCT_THEN" "ill-formed induction theorem"
+*)
 
 in
 

src/1/Tactical.sml

@@ -52,9 +52,9 @@ local
    val mesg = Lib.with_flag (Feedback.MESG_to_string, Lib.I) Feedback.HOL_MESG
    fun provide_feedback f (t, tac: tactic) =
       f (t, tac)
-      handle (e as HOL_ERR {message = m, origin_function = f, ...}) =>
+      handle (e as HOL_ERR {message = m, origin = origin, ...}) =>
            (mesg ("Proof of \n\n" ^ Parse.term_to_string t ^ "\n\nfailed.\n")
-            ; (case (m, f, unsolved ()) of
+            ; (case (m, #origin_function (hd origin), unsolved ()) of
                   ("unsolved goals", "TAC_PROOF", (_, u)::_) =>
                       if Term.term_eq u t
                          then ()
@@ -873,8 +873,11 @@ local
    in
       (gl, (if is_neg w then NEG_DISCH ant else DISCH ant) o prf)
    end
+   handle (e as HOL_ERR _) => raise (wrap_exn "Tactical" "DISCH_THEN" e)
+(* TODO fix
    handle HOL_ERR {message,origin_function, ...} =>
           raise ERR "DISCH_THEN" (origin_function ^ ":" ^ message)
+*)
   val NOT_NOT_E = boolTheory.NOT_CLAUSES |> CONJUNCT1
   val NOT_NOT_I = NOT_NOT_E |> GSYM
   val NOT_IMP_F = IMP_ANTISYM_RULE (SPEC_ALL boolTheory.F_IMP)

src/HolSat/satTools.sml

@@ -125,11 +125,13 @@ fun satCheck model t =
       DISCH mtm th4 (* |- l1 /\ ... /\ ln ==> t *)
    end
    handle Interrupt => raise Interrupt
-        | HOL_ERR {origin_function = "EQT_ELIM", ...} =>
-             if is_neg t
+        | (e as HOL_ERR {origin = origin, ...}) =>
+             if (#origin_function (hd origin) = "EQT_ELIM") then
+                (if is_neg t
                 then UNDISCH (EQF_ELIM (REWRITE_CONV [] t))
                      handle HOL_ERR _ => raise satCheckError
-             else raise satCheckError
+                else raise satCheckError)
+             else raise e
         |  _ => raise satCheckError;
 
 end

src/basicProof/BasicProvers.sml

@@ -620,8 +620,8 @@ val byA = by0 ALL_TAC
 
 fun (q suffices_by tac) g =
   (Q_TAC SUFF_TAC q gTHEN1 (tac THEN NO_TAC)) g
-  handle e as HOL_ERR {origin_function,...} =>
-         if origin_function = "Q_TAC" then raise e
+  handle e as HOL_ERR {origin,...} =>
+         if #origin_function (hd origin) = "Q_TAC" then raise e
          else
            case qlinenum q of
                SOME l => raise ERR "suffices_by"

src/integer/CooperMath.sml

@@ -530,11 +530,13 @@ local
   fun flip_muls tm =
     if is_mult tm andalso not (is_var (rand tm)) then let
       val mcands = strip_mult tm
-      val (var, rest) = Lib.pluck is_var mcands
     in
-      EQT_ELIM (AC_CONV (INT_MUL_ASSOC, INT_MUL_SYM)
-                (mk_eq(tm, mk_mult(list_mk_mult rest, var))))
-    end handle HOL_ERR {origin_structure = "Lib", ...} => ALL_CONV tm
+      (case total (Lib.pluck is_var) mcands of
+          SOME (var, rest) =>
+                             EQT_ELIM (AC_CONV (INT_MUL_ASSOC, INT_MUL_SYM)
+                             (mk_eq(tm, mk_mult(list_mk_mult rest, var))))
+        | NONE => ALL_CONV tm)
+    end
     else if is_comb tm then
       (RATOR_CONV flip_muls THENC RAND_CONV flip_muls) tm
     else if is_abs tm then

src/integer/IntDP_Munge.sml

@@ -235,9 +235,12 @@ in
       LAND_CONV eliminate_nat_quants THENC
       RATOR_CONV (RATOR_CONV (RAND_CONV eliminate_nat_quants))
     else ALL_CONV
+end tm handle (e as HOL_ERR _) =>
+  raise ERR "eliminate_nat_quants" "Uneliminable natural number term remains"
+(* TODO fix
 end tm handle HOL_ERR {origin_function = "REWR_CONV", ...} =>
   raise ERR "IntDP_Munge" "Uneliminable natural number term remains"
-
+*)
 
 fun tacTHEN t1 t2 tm = let
   val (g1, v1) = t1 tm

src/n-bit/wordsLib.sml

@@ -1527,16 +1527,24 @@ fun WORD_LIT_CONV tm =
 
 val NEG1_WORD1 = Drule.EQT_ELIM (WORD_EVAL_CONV ``-1w = 1w : word1``)
 
+local
+fun CHANGED_CONV conv tm =
+   let
+      val th = conv tm
+      val (lhs, rhs) = dest_eq (concl th)
+   in
+      if aconv lhs rhs
+         then raise Conv.UNCHANGED
+      else th
+   end
+in
 fun WORD_SUB_CONV tm =
-   Conv.CHANGED_CONV
+   CHANGED_CONV
      (SIMP_CONV (bool_ss++WORD_MULT_ss++WORD_SUBTRACT_ss) []
       THENC DEPTH_CONV WORD_LIT_CONV
       THENC PURE_REWRITE_CONV [WORD_SUB_INTRO, WORD_NEG_SUB, WORD_SUB_RNEG,
               WORD_NEG_NEG, WORD_MULT_CLAUSES, NEG1_WORD1]) tm
-   handle HOL_ERR (err as {origin_function, ...}) =>
-      if origin_function = "CHANGED_CONV"
-         then raise Conv.UNCHANGED
-      else raise HOL_ERR err
+end
 
 val WORD_SUB_ss =
    simpLib.name_ss "WORD_SUB"
@@ -1829,8 +1837,12 @@ fun WORD_BIT_INDEX_CONV toindex =
          in
             Drule.ISPEC w (Drule.MATCH_MP thm lt)
          end
+         handle HOL_ERR _ =>
+            raise ERR "WORD_BIT_INDEX_CONV" "index too large"
+(*
          handle HOL_ERR {origin_function = "EQT_ELIM", ...} =>
             raise ERR "WORD_BIT_INDEX_CONV" "index too large"
+*)
    end
 
 (* ------------------------------------------------------------------------- *)

src/parse/Parse.sml

@@ -587,7 +587,7 @@ val temp_add_infix_type = mk_temp_tyd add_infix_type0
 val add_infix_type = mk_perm_tyd add_infix_type0
 
 fun replace_exnfn fnm f x =
-  f x handle HOL_ERR e => raise HOL_ERR (set_origin_function fnm e)
+  f x handle (e as HOL_ERR _) => raise wrap_exn "Parse" fnm e
 
 fun thytype_abbrev0 r = [TYABBREV r]
 val temp_thytype_abbrev = mk_temp_tyd thytype_abbrev0

src/parse/ParseDatatype.sml

@@ -271,8 +271,12 @@ fun parse_harg G qb =
         end
       else
         (parse_atom G qb
+         handle e as (HOL_ERR _) =>
+                raise wrap_exn "ParseDatatype" "parse_harg" e)
+(*
          handle HOL_ERR {origin_structure = "Parse", message, ...} =>
                 raise ERR "parse_harg" message)
+*)
     | (base_tokens.BT_AQ ty, _) => (qbuf.advance qb; dAQ ty)
     | (_, locn) => raise ERRloc "parse_harg" locn
                          "Unexpected token in constructor's argument"

src/parse/testutils.sml

@@ -228,17 +228,22 @@ fun convtest (nm,conv,tm,expected) =
   in
     timed conv (exncheck c) tm
   end handle InternalDie p => pretty_die p
-
+(* TODO fix
 fun check_HOL_ERRexn P e =
     case e of
         HOL_ERR{origin_structure,origin_function,message,...} =>
           P (origin_structure, origin_function, message)
       | _ => false
-
+*)
+fun check_HOL_ERRexn P e =
+    case e of
+        HOL_ERR _ => true
+      | _ => false
 fun check_HOL_ERR P (Res _) = false
   | check_HOL_ERR P (Exn e) = check_HOL_ERRexn P e
 
 fun is_struct_HOL_ERR st1 = check_HOL_ERRexn (fn (st2,_,_) => st1 = st2)
+
 fun check_result P (Res r) = P r
   | check_result P _ = false
 

src/prekernel/Feedback.sig

@@ -1,7 +1,8 @@
 signature Feedback =
 sig
-    type error_record = {origin_structure : string,
-                         origin_function  : string,
+    type origin = {origin_structure : string,
+                   origin_function  : string} list
+    type error_record = {origin : origin,
                          source_location  : locn.locn,
                          message          : string}
 
@@ -10,7 +11,6 @@ sig
     val mk_HOL_ERRloc     : string -> string -> locn.locn -> string -> exn
     val wrap_exn          : string -> string -> exn -> exn
     val wrap_exn_loc      : string -> string -> locn.locn -> exn -> exn
-    val set_origin_function : string -> error_record -> error_record
     val set_message       : string -> error_record -> error_record
 
     val emit_ERR          : bool ref