HOL_ERR source locations

examples/HolCheck/lzConv.sml

@@ -25,6 +25,7 @@ exception UNCHANGED
 fun QCONV c tm = c tm handle UNCHANGED => REFL tm
 
 val ERR = mk_HOL_ERR "lzConv";
+val ERRloc = mk_HOL_ERRloc "lzConv";
 
 
 (* ---------------------------------------------------------------------*)
@@ -73,13 +74,13 @@ 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 {origin_function, message, origin_structure} =>
+    handle HOL_ERR {origin_function, source_location, message, origin_structure} =>
       if Lib.mem origin_function  ["RAND_CONV", "RATOR_CONV", "ABS_CONV"]
          andalso origin_structure = "lzConv"
       then
-        raise ERR "RAND_CONV" message
+        raise ERRloc "RAND_CONV" source_location message
       else
-        raise ERR "RAND_CONV" (origin_function ^ ": " ^ message)
+        raise ERRloc "RAND_CONV" source_location (origin_function ^ ": " ^ message)
 in
   AP_TERM Rator newrand handle (HOL_ERR {message,...}) =>
     raise ERR "RAND_CONV" ("Application of AP_TERM failed: "^message)
@@ -100,13 +101,13 @@ fun RATOR_CONV conv tm = let
   val {Rator,Rand} =
     dest_comb tm handle (HOL_ERR _) => raise ERR "RATOR_CONV" "not a comb"
   val newrator = conv Rator
-    handle HOL_ERR {origin_function, origin_structure, message} =>
+    handle HOL_ERR {origin_function, origin_structure, source_location, message} =>
       if Lib.mem origin_function  ["RAND_CONV", "RATOR_CONV", "ABS_CONV"]
          andalso origin_structure = "lzConv"
       then
-        raise ERR "RATOR_CONV" message
+        raise ERRloc "RATOR_CONV" source_location message
       else
-        raise ERR "RATOR_CONV" (origin_function ^ ": " ^ message)
+        raise ERRloc "RATOR_CONV" source_location (origin_function ^ ": " ^ message)
 in
   AP_THM newrator Rand handle  (HOL_ERR {message,...}) =>
     raise ERR "RATOR_CONV" ("Application of AP_THM failed: "^message)
@@ -162,14 +163,14 @@ fun ABS_CONV conv tm =
                in
                  TRANS (TRANS th1 eq_thm') th2
                end
-                 handle HOL_ERR {origin_function, origin_structure, message} =>
+                 handle HOL_ERR {origin_function, origin_structure, source_location, message} =>
                         if Lib.mem origin_function  ["RAND_CONV", "RATOR_CONV",
                                                      "ABS_CONV"]
                            andalso origin_structure = "lzConv"
                         then
-                          raise ERR "ABS_CONV" message
+                          raise ERRloc "ABS_CONV" source_location message
                         else
-                          raise ERR "ABS_CONV"
+                          raise ERRloc "ABS_CONV" source_location
                                     (origin_function ^ ": " ^ message)
       end
     | _ => raise ERR "ABS_CONV" "Term not an abstraction"

examples/acl2/ml/polytypicLib.sml

@@ -85,8 +85,8 @@ fun isFatal (polyExn(Fatal,_,_)) = true
 
 fun wrapException name (polyExn(level,trace,msg)) = raise polyExn(level,name::trace,msg)
   | wrapException name Interrupt = raise Interrupt
-  | wrapException name (HOL_ERR {origin_structure,origin_function,message}) =
-                                raise polyExn(Standard,[name,origin_structure ^ "." ^ origin_function],message)
+  | wrapException name (HOL_ERR {origin_structure,origin_function,source_location,message}) =
+    raise polyExn(Standard,[name,origin_structure ^ "." ^ origin_function],locn.toString source_location ^ ":\n" ^ message)
   | wrapException name exn = raise polyExn(Standard,[name],exn_to_string exn);
 
 local
@@ -3740,4 +3740,4 @@ fun add_rule_source_theorem_generator name test rule =
         add_source_theorem_generator name test
         (fn t => rule t handle e => wrapException ("rule:" ^ name ^ " (" ^ type_to_string t ^ ")") e);
 
-end
+end

examples/decidable_separationLogic/src/decidable_separationLogicLib.sml

@@ -54,9 +54,7 @@ val _ = computeLib.add_thms [SF_POINTS_TO_LIST_def, SAFE_FILTER_THM, MAP, APPEND
    sf_points_to_list_cs;
 *)
 
-fun SMALLFOOT_ERR s =
-   raise HOL_ERR {message = s, origin_function = "", origin_structure = "decidable_separationLogicLib"}
-
+val SMALLFOOT_ERR s = raise mk_HOL_ERR "decidable_separationLogicLib" "" s
 
 
 (************************************************************

examples/lambda/basics/binderLib.sml

@@ -19,9 +19,7 @@ val tmToString =
         |> trace ("Unicode", 0)
 
 
-fun ERR f msg = raise (HOL_ERR {origin_function = f,
-                                origin_structure = "binderLib",
-                                message = msg})
+val ERR = mk_HOL_ERR "binderLib"
 
 datatype nominaltype_info =
          NTI of { recursion_thm : thm option,
@@ -281,14 +279,14 @@ end
 fun check_for_errors tm = let
   val conjs = map (#2 o strip_forall) (strip_conj tm)
   val _ = List.all is_eq conjs orelse
-          ERR "prove_recursive_term_function_exists"
+          raise ERR "prove_recursive_term_function_exists"
               "All conjuncts must be equations"
   val f = rator (lhs (hd conjs))
   val _ = List.all (fn t => rator (lhs t) ~~ f) conjs orelse
-          ERR "prove_recursive_term_function_exists"
+          raise ERR "prove_recursive_term_function_exists"
               "Must define same constant in all equations"
   val _ = List.all (fn t => length (#2 (strip_comb (lhs t))) = 1) conjs orelse
-          ERR "prove_recursive_term_function_exists"
+          raise ERR "prove_recursive_term_function_exists"
               "Function being defined must be applied to one argument"
   val dom_ty = #1 (dom_rng (type_of f))
   val recthm = valOf (recthm_for_type dom_ty)
@@ -304,7 +302,7 @@ fun check_for_errors tm = let
                                              (#1 (strip_comb (rand (lhs t))))))
                       constructors) conjs of
         NONE => ()
-      | SOME t => ERR "prove_recursive_term_function_exists"
+      | SOME t => raise ERR "prove_recursive_term_function_exists"
                       ("Unknown constructor "^
                        tmToString (#1 (strip_comb (rand (lhs t)))))
   val () =
@@ -317,7 +315,7 @@ fun check_for_errors tm = let
                     end) conjs of
         NONE => ()
       | SOME (v, c) =>
-        ERR "prove_recursive_term_function_exists"
+        raise ERR "prove_recursive_term_function_exists"
             (#1 (dest_const c)^"^'s argument "^tmToString v^
              " is not a variable")
 in
@@ -427,7 +425,7 @@ fun prove_recursive_term_function_exists0 fin tm = let
       case alist of
         [] => [(c,rhs)]
       | (h as (c',rhs')) :: t => if same_const c c' then
-                                   ERR "prove_recursive_term_function_exists"
+                                   raise ERR "prove_recursive_term_function_exists"
                                        ("Two equations for constructor " ^
                                         #1 (dest_const c))
                                  else h :: insert x t

examples/machine-code/graph/backgroundLib.sml

@@ -127,9 +127,7 @@ fun auto_conv_prove proof_name goal conv =
 
 fun modify_message f e =
   case e of
-    HOL_ERR e => HOL_ERR { message = f (#message e) ,
-                   origin_function = #origin_function e ,
-                   origin_structure = #origin_structure e }
+    HOL_ERR e => HOL_ERR (set_message (f (#message e)) e)
   | _ => e
 
 fun report_error name e = let

help/Docfiles/Feedback.wrap_exn.doc

@@ -9,11 +9,11 @@ Adds supplementary information to an application of {HOL_ERR}.
 exception, error.
 
 \DESCRIBE
-{wrap_exn s1 s2 (HOL_ERR{origin_structure,origin_function,message})}
+{wrap_exn s1 s2 (HOL_ERR{origin_structure,origin_function,source_location,message})}
 where {s1} typically denotes a structure and {s2} typically denotes
 a function, returns
 
-{HOL_ERR{origin_structure=s1,origin_function=s2,message}}
+{HOL_ERR{origin_structure=s1,origin_function=s2,source_location,message}}
 
 where {origin_structure} and {origin_function} have been added to
 the {message} field. This can be used to achieve a kind of backtrace

src/1/Conv.sml

@@ -26,6 +26,7 @@ exception UNCHANGED
 fun QCONV c tm = c tm handle UNCHANGED => REFL tm
 
 val ERR = mk_HOL_ERR "Conv"
+val ERRloc = mk_HOL_ERRloc "Conv"
 fun w nm c t = c t handle UNCHANGED => raise UNCHANGED
                    | e as HOL_ERR _ => Portable.reraise e
                    | Fail s => raise Fail (s ^ " --> " ^ nm)
@@ -80,17 +81,20 @@ val REWR_CONV_A  = REWR_CONV0 (PART_MATCH_A,    "REWR_CONV_A")
  *    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 {origin_function, message, origin_structure} =>
-            if Lib.mem origin_function ["RAND_CONV", "RATOR_CONV", "ABS_CONV"]
-               andalso origin_structure = "Conv"
-               then raise ERR "RAND_CONV" message
-            else raise ERR "RAND_CONV" (origin_function ^ ": " ^ message)
+         handle HOL_ERR e => raise set_origin "RAND_CONV" e
    in
       AP_TERM Rator newrand
       handle HOL_ERR {message, ...} =>
@@ -113,11 +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 {origin_function, origin_structure, message} =>
-            if Lib.mem origin_function  ["RAND_CONV", "RATOR_CONV", "ABS_CONV"]
-               andalso origin_structure = "Conv"
-               then raise ERR "RATOR_CONV" message
-            else raise ERR "RATOR_CONV" (origin_function ^ ": " ^ message)
+         handle HOL_ERR e => raise set_origin "RATOR_CONV" e
    in
       AP_THM newrator Rand
       handle HOL_ERR {message, ...} =>
@@ -158,13 +158,7 @@ fun ABS_CONV conv tm =
                  in
                     TRANS (TRANS th1 eq_thm') th2
                  end
-                 handle HOL_ERR {origin_function, origin_structure, message} =>
-                          if Lib.mem origin_function
-                                     ["RAND_CONV", "RATOR_CONV", "ABS_CONV"]
-                             andalso origin_structure = "Conv"
-                             then raise ERR "ABS_CONV" message
-                          else raise ERR "ABS_CONV"
-                                         (origin_function ^ ": " ^ message)
+                 handle HOL_ERR e => raise set_origin "ABS_CONV" e
         end
     | _ => raise ERR "ABS_CONV" "Term not an abstraction"
 

src/1/Prim_rec.sml

@@ -84,10 +84,8 @@ fun mymatch_and_instantiate axth pattern instance = let
     val forall_env = ListPair.map op|-> (patvars, instvars)
     val pateqn = Term.subst forall_env pateqn0
     val _ = aconv (lhs pateqn) (lhs insteqn) orelse
-      raise HOL_ERR {origin_function =
-                "prove_raw_recursive_functions_exist.mymatch_and_instantiate",
-              origin_structure = "Prim_rec",
-              message = ("Failed to match LHSes in clause "^Int.toString cnum)}
+      raise ERR "prove_raw_recursive_functions_exist.mymatch_and_instantiate"
+        ("Failed to match LHSes in clause "^Int.toString cnum)
     val instrhs = rhs insteqn and patrhs = rhs pateqn
     (* last arguments in the pattern will be instances of a function symbol
        being applied to recursive arguments *)
@@ -108,10 +106,8 @@ fun mymatch_and_instantiate axth pattern instance = let
     case (patconjs, instconjs) of
       ([], []) => List.rev acc
     | (p::ps, i::is) => match_eqns ((match_eqn n p i)::acc) (n + 1) ps is
-    | _ => raise
-        HOL_ERR {origin_function = "prove_raw_recursive_functions_exist",
-                 origin_structure = "recursion",
-                 message = "Number of conjuncts not even the same"}
+    | _ => raise ERR "prove_raw_recursive_functions_exist"
+             "Number of conjuncts not even the same"
   val tmsubst = match_eqns [] 1 (strip_conj new_patbody) (strip_conj instbody)
   val axth1 = Thm.INST_TYPE tyinst axth
   val axth2 = Thm.INST tmsubst axth1

src/1/Tactical.sml

@@ -224,13 +224,11 @@ fun op THEN1 (tac1: tactic, tac2: tactic) : tactic =
 val op >- = op THEN1
 fun op>>-(tac1, n) tac2 g =
   op>- (tac1, tac2) g
-  handle e as HOL_ERR {message,origin_structure,origin_function} =>
+  handle e as HOL_ERR (er as {message,...}) =>
          if is_substring "THEN1" message then raise e
          else
-           raise HOL_ERR {message = message ^
-                                    " (THEN1 on line "^Int.toString n^")",
-                          origin_function = origin_function,
-                          origin_structure = origin_structure}
+           raise HOL_ERR (set_message
+             (message ^ " (THEN1 on line "^Int.toString n^")") er)
 fun (f ?? x) = f x
 
 

src/1/dep_rewrite.sml

@@ -180,16 +180,13 @@ fun print_goal (asl,gl) = (print_term gl; print_newline());
 fun pthm th = (print_all_thm th; th);
 (**)
 
-fun TACTIC_ERR{function,message} =
-    Feedback.HOL_ERR{origin_structure = "Tactic",
-                      origin_function = function,
-                      message = message};
+val ERR = mk_HOL_ERR "Tactic"
 
 fun failwith function =
    ( (**) if debug_fail then
          print_string ("Failure in dep_rewrite: "^function^"\n")
      else (); (**)
-    raise TACTIC_ERR{function = function,message = "Failure in dep_rewrite"});
+    raise ERR function "Failure in dep_rewrite");
 
 
 

src/HolQbf/selftest.sml

@@ -50,19 +50,19 @@ end
 fun prove t =
   if squolem_installed then
     (HolQbfLib.prove t; print ".")
-    handle Feedback.HOL_ERR {origin_structure, origin_function, message} =>
+    handle Feedback.HOL_ERR {origin_structure, origin_function, source_location, message} =>
       die ("Prove failed on term '" ^ Hol_pp.term_to_string t ^
         "': exception HOL_ERR (in " ^ origin_structure ^ "." ^ origin_function ^
-        ", message: " ^ message ^ ")")
+        " " ^ locn.toString source_location ^ ", message: " ^ message ^ ")")
   else ()
 
 fun disprove t =
   if squolem_installed then
     (HolQbfLib.disprove t; print ".")
-    handle Feedback.HOL_ERR {origin_structure, origin_function, message} =>
+    handle Feedback.HOL_ERR {origin_structure, origin_function, source_location, message} =>
       die ("Disprove failed on term '" ^ Hol_pp.term_to_string t ^
         "': exception HOL_ERR (in " ^ origin_structure ^ "." ^ origin_function ^
-        ", message: " ^ message ^ ")")
+        " " ^ locn.toString source_location ^ ", message: " ^ message ^ ")")
   else ()
 
 val thmeq = Lib.pair_eq (Lib.list_eq Term.aconv) Term.aconv
@@ -78,10 +78,10 @@ fun decide t =
             else die ("Decide proved bad theorem on term '" ^
               Hol_pp.term_to_string t ^ "'")
     in print "." end
-    handle Feedback.HOL_ERR {origin_structure, origin_function, message} =>
+    handle Feedback.HOL_ERR {origin_structure, origin_function, source_location, message} =>
       die ("Decide failed on term '" ^ Hol_pp.term_to_string t ^
         "': exception HOL_ERR (in " ^ origin_structure ^ "." ^ origin_function ^
-        ", message: " ^ message ^ ")")
+        " " ^ locn.toString source_location ^ ", message: " ^ message ^ ")")
   else ()
 
 local

src/HolSat/vector_def_CNF/defCNF.sml

@@ -20,8 +20,7 @@ open HolKernel Parse boolLib simpLib numLib normalForms defCNFTheory;
 (* Helper functions.                                                         *)
 (* ------------------------------------------------------------------------- *)
 
-fun ERR f s =
-  HOL_ERR {message = s, origin_function = f, origin_structure = "defCNF"};
+val ERR = mk_HOL_ERR "defCNF"
 
 fun distinct [] = true
   | distinct (x :: rest) = not (mem x rest) andalso distinct rest;

src/HolSmt/selftest.sml

@@ -49,10 +49,11 @@ fun expect_thm name smt_tac t =
   let
     open boolLib
     val thm = Tactical.TAC_PROOF (([], t), smt_tac)
-      handle Feedback.HOL_ERR {origin_structure, origin_function, message} =>
+      handle Feedback.HOL_ERR {origin_structure, origin_function, source_location, message} =>
         die ("Test of solver '" ^ name ^ "' failed on term '" ^
           term_with_types t ^ "': exception HOL_ERR (in " ^
-          origin_structure ^ "." ^ origin_function ^ ", message: " ^ message ^
+          origin_structure ^ "." ^ origin_function ^
+          " " ^ locn.toString source_location ^ ", message: " ^ message ^
           ")")
   in
     if null (Thm.hyp thm) andalso Thm.concl thm ~~ t then ()
@@ -75,7 +76,7 @@ fun expect_sat name smt_tac t =
   in
     die ("Test of solver '" ^ name ^ "' failed on term '" ^
       term_with_types t ^ "': exception expected")
-  end handle Feedback.HOL_ERR {origin_structure, origin_function, message} =>
+  end handle Feedback.HOL_ERR {origin_structure, origin_function, source_location, message} =>
     if origin_structure = "HolSmtLib" andalso
        origin_function = "GENERIC_SMT_TAC" andalso
        (message = "solver reports negated term to be 'satisfiable'" orelse
@@ -87,7 +88,8 @@ fun expect_sat name smt_tac t =
       die ("Test of solver '" ^ name ^ "' failed on term '" ^
         term_with_types t ^
         "': exception HOL_ERR has unexpected argument values (in " ^
-        origin_structure ^ "." ^ origin_function ^ ", message: " ^ message ^
+        origin_structure ^ "." ^ origin_function ^
+        " " ^ locn.toString source_location ^ ", message: " ^ message ^
         ")")
 
 fun mk_test_fun is_configured expect_fun name smt_tac =

src/boss/selftest.sml

@@ -34,7 +34,7 @@ val tydef_th = prove(
 val _ = tprint "new_type_definition error message"
 val _ =
     ignore (new_type_definition("mytydef", tydef_th))
-    handle HOL_ERR {origin_function, message, origin_structure} =>
+    handle HOL_ERR {origin_function, message, origin_structure, ...} =>
            if origin_function <> "new_type_definition" orelse
               origin_structure <> "Theory.Definition" orelse
               message <> "at Thm.prim_type_definition:\nexpected a theorem of the form \"?x. P x\""

src/boss/theory_tests/bylocnScript.sml

@@ -10,7 +10,7 @@ fun test l suffp q =
      ``something impossible : bool``,
      (if suffp then q suffices_by ALL_TAC
       else q by ALL_TAC))
-     handle e as HOL_ERR {message, origin_structure, origin_function} =>
+     handle e as HOL_ERR {message, origin_structure, origin_function, ...} =>
             if suffp then
               if message = "suffices_by's tactic failed to prove goal on line "^
                            Int.toString l