From 7db7df9fe94a7691347840777b38e0534d2ce5e7 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 15 Nov 2024 01:34:06 +0100 Subject: [PATCH] HOL_ERR source locations --- examples/HolCheck/lzConv.sml | 19 +- examples/acl2/ml/polytypicLib.sml | 6 +- .../src/decidable_separationLogicLib.sml | 4 +- examples/lambda/basics/binderLib.sml | 16 +- examples/machine-code/graph/backgroundLib.sml | 4 +- help/Docfiles/Feedback.wrap_exn.doc | 4 +- src/1/Conv.sml | 28 +-- src/1/Prim_rec.sml | 12 +- src/1/Tactical.sml | 8 +- src/1/dep_rewrite.sml | 7 +- src/HolQbf/selftest.sml | 12 +- src/HolSat/vector_def_CNF/defCNF.sml | 3 +- src/HolSmt/selftest.sml | 10 +- src/boss/selftest.sml | 2 +- src/boss/theory_tests/bylocnScript.sml | 2 +- src/compute/src/compute_rules.sml | 9 +- src/datatype/mutrec/MutRecDef.sml | 4 +- src/datatype/mutrec/Recftn.sml | 41 ++-- src/datatype/mutrec/utils/elsaUtils.sml | 4 +- src/datatype/record/RecordType.sml | 6 +- src/experimental-kernel/Type.sml | 6 +- src/hol88/hol88Lib.sml | 4 +- src/integer/OmegaMLShadow.sml | 5 +- src/integer/OmegaMath.sml | 4 +- src/integer/OmegaShell.sml | 4 +- src/integer/OmegaSymbolic.sml | 4 +- src/num/arith/src/Exists_arith.sml | 13 +- src/num/arith/src/Int_extra.sml | 8 +- src/num/arith/src/Prenex.sml | 4 +- src/num/arith/src/Sol_ranges.sml | 4 +- src/num/arith/src/Solve.sml | 10 +- src/num/arith/src/Solve_ineqs.sml | 4 +- src/num/arith/src/Sub_and_cond.sml | 5 +- src/num/arith/src/Sup_Inf.sml | 4 +- src/num/theories/cv_compute/tailrecLib.sml | 5 +- src/parse/GrammarAncestry.sml | 3 +- src/parse/GrammarSpecials.sml | 10 +- src/parse/Parse.sml | 4 +- src/parse/testutils.sml | 2 +- src/parse/type_grammar.sml | 5 +- src/postkernel/Theory.sml | 2 +- src/prekernel/Feedback.sig | 3 + src/prekernel/Feedback.sml | 25 +- src/quotient/examples/lambda/barendregt.sml | 4 +- src/quotient/examples/lambda/betaScript.sml | 10 +- src/quotient/examples/lambda/etaScript.sml | 10 +- .../examples/lambda/reductionScript.sml | 10 +- src/quotient/examples/sigma/barendregt.sml | 4 +- .../examples/sigma/reductionScript.sml | 5 +- .../examples/sigma/semanticsScript.sml | 10 +- src/quotient/examples/tactics.sig | 4 +- src/quotient/examples/tactics.sml | 4 +- src/quotient/src/quotient.sml | 221 ++++++------------ src/real/hrealScript.sml | 3 +- src/res_quan/src/Cond_rewrite.sml | 4 +- src/ring/src/EVAL_quote.sml | 5 +- src/ring/src/EVAL_ringLib.sml | 5 +- src/ring/src/abstraction.sml | 5 +- src/simp/src/Opening.sml | 4 +- src/simp/src/Traverse.sml | 2 +- src/tactictoe/src/tttEval.sml | 8 +- src/tfl/src/Defn.sml | 4 +- src/thm/otknl-thm.ML | 3 +- src/thm/std-thm.ML | 3 +- 64 files changed, 248 insertions(+), 419 deletions(-) diff --git a/examples/HolCheck/lzConv.sml b/examples/HolCheck/lzConv.sml index 812986f660..395834791c 100644 --- a/examples/HolCheck/lzConv.sml +++ b/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" diff --git a/examples/acl2/ml/polytypicLib.sml b/examples/acl2/ml/polytypicLib.sml index 42f800a6a6..cb11bffdb0 100644 --- a/examples/acl2/ml/polytypicLib.sml +++ b/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 \ No newline at end of file +end diff --git a/examples/decidable_separationLogic/src/decidable_separationLogicLib.sml b/examples/decidable_separationLogic/src/decidable_separationLogicLib.sml index 2ba93942b9..2ad170d36c 100644 --- a/examples/decidable_separationLogic/src/decidable_separationLogicLib.sml +++ b/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 (************************************************************ diff --git a/examples/lambda/basics/binderLib.sml b/examples/lambda/basics/binderLib.sml index c4b269eb2c..4cf8d2f3ba 100644 --- a/examples/lambda/basics/binderLib.sml +++ b/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 diff --git a/examples/machine-code/graph/backgroundLib.sml b/examples/machine-code/graph/backgroundLib.sml index f2761042af..2fd174a728 100644 --- a/examples/machine-code/graph/backgroundLib.sml +++ b/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 diff --git a/help/Docfiles/Feedback.wrap_exn.doc b/help/Docfiles/Feedback.wrap_exn.doc index 90cf49e2fb..741355200f 100644 --- a/help/Docfiles/Feedback.wrap_exn.doc +++ b/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 diff --git a/src/1/Conv.sml b/src/1/Conv.sml index 7c8dd219a6..1db51a1c25 100644 --- a/src/1/Conv.sml +++ b/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" diff --git a/src/1/Prim_rec.sml b/src/1/Prim_rec.sml index f2295a8416..57ea459a51 100644 --- a/src/1/Prim_rec.sml +++ b/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 diff --git a/src/1/Tactical.sml b/src/1/Tactical.sml index 804e350237..0731d96799 100644 --- a/src/1/Tactical.sml +++ b/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 diff --git a/src/1/dep_rewrite.sml b/src/1/dep_rewrite.sml index a82d351a14..9df07777ee 100644 --- a/src/1/dep_rewrite.sml +++ b/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"); diff --git a/src/HolQbf/selftest.sml b/src/HolQbf/selftest.sml index f419754ae7..d49431c3f1 100644 --- a/src/HolQbf/selftest.sml +++ b/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 diff --git a/src/HolSat/vector_def_CNF/defCNF.sml b/src/HolSat/vector_def_CNF/defCNF.sml index 7b7c2d5260..87e1593305 100644 --- a/src/HolSat/vector_def_CNF/defCNF.sml +++ b/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; diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml index 70740d5e39..7265727ba6 100644 --- a/src/HolSmt/selftest.sml +++ b/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 = diff --git a/src/boss/selftest.sml b/src/boss/selftest.sml index 986ab37bad..62ebcb333c 100644 --- a/src/boss/selftest.sml +++ b/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\"" diff --git a/src/boss/theory_tests/bylocnScript.sml b/src/boss/theory_tests/bylocnScript.sml index 63dafbebeb..ed848448da 100644 --- a/src/boss/theory_tests/bylocnScript.sml +++ b/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 diff --git a/src/compute/src/compute_rules.sml b/src/compute/src/compute_rules.sml index 74f8d3d56a..ce4151c821 100644 --- a/src/compute/src/compute_rules.sml +++ b/src/compute/src/compute_rules.sml @@ -16,10 +16,7 @@ datatype ('a,'b,'c) stack = | Zabs of { Bvar : 'c, Ctx : ('a,'b,'c) stack } ; -fun RULES_ERR function message = - HOL_ERR{origin_structure = "compute_rules", - origin_function = function, - message = message}; +val ERR = mk_HOL_ERR "compute_rules" (*--------------------------------------------------------------------------- * Serious anomaly of the code (an internal invariant was broken). We don't @@ -103,14 +100,14 @@ fun FUNIFY thm = let val x = rand (lhs (concl thm)) in CONV_RULE (RATOR_CONV (RAND_CONV (REWR_CONV ETA_AX))) (ABS x thm) end - handle HOL_ERR _ => raise RULES_ERR "FUNIFY" "" + handle HOL_ERR _ => raise ERR "FUNIFY" "" fun UNFUNIFY thm = let val (lhs,rhs) = dest_eq (concl thm) val x = variant (free_vars lhs) (bvar rhs) in CONV_RULE (RAND_CONV BETA_CONV) (AP_THM thm x) end - handle HOL_ERR _ => raise RULES_ERR "UNFUNIFY" "" + handle HOL_ERR _ => raise ERR "UNFUNIFY" "" end; diff --git a/src/datatype/mutrec/MutRecDef.sml b/src/datatype/mutrec/MutRecDef.sml index 0d550263ef..ab8fbca2e6 100644 --- a/src/datatype/mutrec/MutRecDef.sml +++ b/src/datatype/mutrec/MutRecDef.sml @@ -30,9 +30,7 @@ type thm = Thm.thm val ambient_grammars = Parse.current_grammars(); val _ = Parse.temp_set_grammars boolTheory.bool_grammars; -fun MUT_REC_ERR {function,message} = HOL_ERR{origin_structure = "MutRecDef", - origin_function = function, - message = message} +fun MUT_REC_ERR {function,message} = mk_HOL_ERR "MutRecDef" function message (* Some general functions and values we need *) diff --git a/src/datatype/mutrec/Recftn.sml b/src/datatype/mutrec/Recftn.sml index 1896f9fd56..9517b194a4 100644 --- a/src/datatype/mutrec/Recftn.sml +++ b/src/datatype/mutrec/Recftn.sml @@ -122,9 +122,8 @@ open Rsyntax (* use records *) #Name (dest_var tm) else if is_const tm then #Name (dest_const tm) - else raise HOL_ERR {origin_structure = "define_mutual_functions", - origin_function = "term_name", - message = "term is not constant or var"} + else raise mk_HOL_ERR "define_mutual_functions" "term_name" + "term is not constant or var" fun type_name ty = #Tyop (dest_type ty) @@ -304,10 +303,8 @@ open Rsyntax (* use records *) defined. Also, we return a list telling, for each type, which (if any) functions is being defined for that type *) fun check_error ftn = - raise HOL_ERR {origin_structure = "define_mutual_functions", - origin_function = "check_def", - message = ("only some cases provided for function " ^ - (term_name ftn))} + raise mk_HOL_ERR "define_mutual_functions" "check_def" + ("only some cases provided for function " ^ term_name ftn) val one_ty = Type`:one` val one_tm = Term`one` @@ -664,11 +661,8 @@ open Rsyntax (* use records *) conjs@(mk_Qtm_body (def_data, exists_data2)) end else - raise HOL_ERR {origin_structure = "define_mutual_functions", - origin_function = "mk_Qtm_body", - message = ("illegal variable " ^ - (term_name constructor) ^ - " in definition")} + raise mk_HOL_ERR "define_mutual_functions" "mk_Qtm_body" + ("illegal variable " ^ term_name constructor ^ " in definition") else let val (conj, exists_data2) = get_conj_for_cons (datum, exists_data) @@ -716,20 +710,15 @@ open Rsyntax (* use records *) ftn_type_data val consts = - case fixities - of SOME fixes => (map2 - (fn name => fn fixity => {const_name = name, - fixity = fixity}) - new_ftn_names - fixes - handle (HOL_ERR _) => raise - HOL_ERR {origin_structure = "top", - origin_function = - "define_mutual_functions", - message = - "term is not constant or var"}) - | NONE => map (fn name => {const_name = name, fixity = Prefix}) - new_ftn_names + case fixities of + SOME fixes => ( + map2 (fn name => fn fixity => {const_name = name, fixity = fixity}) + new_ftn_names fixes + handle HOL_ERR _ => + raise mk_HOL_ERR "top" "define_mutual_functions" + "term is not constant or var") + | NONE => + map (fn name => {const_name = name, fixity = Prefix}) new_ftn_names (* Now we do our definition. *) val final = new_specification diff --git a/src/datatype/mutrec/utils/elsaUtils.sml b/src/datatype/mutrec/utils/elsaUtils.sml index d86992280e..4ba94705a9 100644 --- a/src/datatype/mutrec/utils/elsaUtils.sml +++ b/src/datatype/mutrec/utils/elsaUtils.sml @@ -31,9 +31,7 @@ type thm_tactic = Abbrev.thm_tactic; fun UTILSLIB_ERR{function,message} = - HOL_ERR{origin_structure = "elsaUtils", - origin_function = function, - message = message}; + mk_HOL_ERR "elsaUtils" function message (* Some general-purpose functions *) diff --git a/src/datatype/record/RecordType.sml b/src/datatype/record/RecordType.sml index 08205e1012..bf77e3c047 100644 --- a/src/datatype/record/RecordType.sml +++ b/src/datatype/record/RecordType.sml @@ -209,10 +209,8 @@ fun prove_recordtype_thms (tyinfo, fields) = let val size = length fields val _ = length types = length fields orelse - raise HOL_ERR {origin_function = "prove_recordtype_thms", - origin_structure = "RecordType", - message = - "Number of fields doesn't match number of types"} + raise mk_HOL_ERR "RecordType" "prove_recordtype_thms" + "Number of fields doesn't match number of types" (* we now have the type actually defined in typthm *) fun letgen x y = x @ [variant x (mk_var (app_letter y,y))] diff --git a/src/experimental-kernel/Type.sml b/src/experimental-kernel/Type.sml index 3ad65c2d9a..68f55dec20 100644 --- a/src/experimental-kernel/Type.sml +++ b/src/experimental-kernel/Type.sml @@ -6,10 +6,8 @@ open Feedback Lib KernelTypes infix |-> infixr --> -val WARN = HOL_WARNING "Type"; -fun ERR f msg = HOL_ERR {origin_structure = "Type", - origin_function = f, - message = msg} +val WARN = HOL_WARNING "Type" +val ERR = mk_HOL_ERR "Type" type type_key = {Thy : string, Tyop : string } type type_info = KernelSig.kernelid * int diff --git a/src/hol88/hol88Lib.sml b/src/hol88/hol88Lib.sml index 4ffa6c0565..35eb7d9186 100644 --- a/src/hol88/hol88Lib.sml +++ b/src/hol88/hol88Lib.sml @@ -12,9 +12,7 @@ struct open Lib Abbrev fun HOL88_ERR {function, message} = - Feedback.HOL_ERR {origin_structure = "hol88Lib", - origin_function = function, - message = message} + Feedback.mk_HOL_ERR "hol88Lib" function message infix ## diff --git a/src/integer/OmegaMLShadow.sml b/src/integer/OmegaMLShadow.sml index ab6b59335a..08c35dc2ba 100644 --- a/src/integer/OmegaMLShadow.sml +++ b/src/integer/OmegaMLShadow.sml @@ -223,9 +223,8 @@ fun term_to_factoid vars tm = let case (vlist,slist) of ([],[]) => [Arbint.zero] | ([],[s]) => [int_of_term s] - | ([], _) => raise HOL_ERR { origin_function = "term_to_factoid", - origin_structure = "OmegaMLShadow", - message = "Too many summands in term"} + | ([], _) => + raise mk_HOL_ERR "OmegaMLShadow" "term_to_factoid" "Too many summands in term" | (v::vs, []) => Arbint.zero :: mk_coeffs vs [] | (v::vs, s::ss) => if is_mult s then let diff --git a/src/integer/OmegaMath.sml b/src/integer/OmegaMath.sml index b7bbcff3bd..0e54c4704e 100644 --- a/src/integer/OmegaMath.sml +++ b/src/integer/OmegaMath.sml @@ -11,9 +11,7 @@ val _ = Parse.temp_set_grammars int_arith_grammars val REWRITE_CONV = GEN_REWRITE_CONV TOP_DEPTH_CONV bool_rewrites -fun ERR f msg = HOL_ERR { origin_structure = "OmegaMath", - origin_function = f, - message = msg} +val ERR = mk_HOL_ERR "OmegaMath" val lhand = rand o rator (* ---------------------------------------------------------------------- diff --git a/src/integer/OmegaShell.sml b/src/integer/OmegaShell.sml index 7171412365..cc0218a483 100644 --- a/src/integer/OmegaShell.sml +++ b/src/integer/OmegaShell.sml @@ -20,9 +20,7 @@ val lhand = rand o rator val REWRITE_CONV = GEN_REWRITE_CONV TOP_DEPTH_CONV bool_rewrites -fun ERR f msg = HOL_ERR { origin_structure = "OmegaShell", - origin_function = f, - message = msg} +val ERR = mk_HOL_ERR "OmegaShell" (* ---------------------------------------------------------------------- check_for_early_equalities t diff --git a/src/integer/OmegaSymbolic.sml b/src/integer/OmegaSymbolic.sml index fc48d1cf90..c9a5270d8d 100644 --- a/src/integer/OmegaSymbolic.sml +++ b/src/integer/OmegaSymbolic.sml @@ -23,9 +23,7 @@ val lhand = rand o rator val REWRITE_CONV = GEN_REWRITE_CONV TOP_DEPTH_CONV bool_rewrites -fun ERR f msg = HOL_ERR { origin_structure = "OmegaSymbolic", - origin_function = f, - message = msg} +val ERR = mk_HOL_ERR "OmegaSymbolic" (* ---------------------------------------------------------------------- clause_to_evals v t diff --git a/src/num/arith/src/Exists_arith.sml b/src/num/arith/src/Exists_arith.sml index 8c4f6345d7..46af5d9474 100644 --- a/src/num/arith/src/Exists_arith.sml +++ b/src/num/arith/src/Exists_arith.sml @@ -29,9 +29,7 @@ open Norm_arith; open Norm_ineqs; open Sol_ranges; -fun failwith function = raise HOL_ERR{origin_structure = "Exists_arith", - origin_function = function, - message = ""}; +fun failwith function = raise mk_HOL_ERR "Exists_arith" function "" (*---------------------------------------------------------------------------*) @@ -116,16 +114,13 @@ fun EXISTS_ARITH_CONV tm = let val th = RULE_OF_CONV ARITH_FORM_NORM_CONV (snd (strip_exists (assert (null o free_vars) tm))) handle (HOL_ERR _) => - raise HOL_ERR{origin_structure = "Exists_arith", - origin_function = "EXISTS_ARITH_CONV", - message = "formula not in the allowed subset"} + raise mk_HOL_ERR "Exists_arith" "EXISTS_ARITH_CONV" + "formula not in the allowed subset" in (let val binding = witness (strip_disj (rhs (concl th))) in EQT_INTRO (WITNESS binding tm) end ) handle (HOL_ERR _) => - raise HOL_ERR{origin_structure = "Exists_arith", - origin_function = "EXISTS_ARITH_CONV", - message = "cannot prove formula"} + raise mk_HOL_ERR "Exists_arith" "EXISTS_ARITH_CONV" "cannot prove formula" end ); diff --git a/src/num/arith/src/Int_extra.sml b/src/num/arith/src/Int_extra.sml index f500e775b1..ab1c2b7319 100644 --- a/src/num/arith/src/Int_extra.sml +++ b/src/num/arith/src/Int_extra.sml @@ -34,9 +34,7 @@ fun gcd (i,j) = in (if ((i < zero) orelse (j < zero)) then raise non_neg else if (i < j) then gcd' (j,i) else gcd' (i,j) - ) handle _ => raise HOL_ERR{origin_structure = "Arith", - origin_function = "gcd", - message = ""} + ) handle _ => raise mk_HOL_ERR "Arith" "gcd" "" end; (*---------------------------------------------------------------------------*) @@ -44,8 +42,6 @@ fun gcd (i,j) = (*---------------------------------------------------------------------------*) fun lcm (i,j) = (i * j) div (gcd (i,j)) - handle _ => raise HOL_ERR{origin_structure = "Arith", - origin_function = "lcm", - message = ""}; + handle _ => raise mk_HOL_ERR "Arith" "lcm" "" end diff --git a/src/num/arith/src/Prenex.sml b/src/num/arith/src/Prenex.sml index b8ac27edf9..82ff5843c6 100644 --- a/src/num/arith/src/Prenex.sml +++ b/src/num/arith/src/Prenex.sml @@ -45,9 +45,7 @@ val LEFT_IMP_FORALL_CONV = Conv.LEFT_IMP_FORALL_CONV val LEFT_IMP_EXISTS_CONV = Conv.LEFT_IMP_EXISTS_CONV val RIGHT_IMP_EXISTS_CONV = Conv.RIGHT_IMP_EXISTS_CONV -fun failwith function = raise HOL_ERR{origin_structure = "Prenex", - origin_function = function, - message = ""}; +fun failwith function = raise mk_HOL_ERR "Prenex" function "" (*---------------------------------------------------------------------------*) (* QUANT_EQ_IMP_CONV : conv *) diff --git a/src/num/arith/src/Sol_ranges.sml b/src/num/arith/src/Sol_ranges.sml index 03cbe0fa4d..a5a57eb5be 100644 --- a/src/num/arith/src/Sol_ranges.sml +++ b/src/num/arith/src/Sol_ranges.sml @@ -29,9 +29,7 @@ open Streams; open Lib; infix ##; open Feedback; -fun failwith function = raise HOL_ERR{origin_structure = "Sol_ranges", - origin_function = function, - message = ""}; +fun failwith function = raise mk_HOL_ERR "Sol_ranges" function "" (*---------------------------------------------------------------------------*) diff --git a/src/num/arith/src/Solve.sml b/src/num/arith/src/Solve.sml index d8d7cb50f3..1ae768e12d 100644 --- a/src/num/arith/src/Solve.sml +++ b/src/num/arith/src/Solve.sml @@ -172,15 +172,13 @@ fun FORALL_ARITH_CONV tm = (NEGATE_CONV ((fn tm => ARITH_FORM_NORM_CONV tm handle HOL_ERR _ => - raise HOL_ERR{origin_structure = "Solve", - origin_function = "FORALL_ARITH_CONV", - message = "formula not in the allowed subset"} + raise mk_HOL_ERR "Solve" "FORALL_ARITH_CONV" + "formula not in the allowed subset" ) THENC (fn tm => DISJ_INEQS_FALSE_CONV tm handle HOL_ERR _ => - raise HOL_ERR{origin_structure = "Solve", - origin_function = "FORALL_ARITH_CONV", - message = "cannot prove formula"} + raise mk_HOL_ERR "Solve" "FORALL_ARITH_CONV" + "cannot prove formula" ))) THENC REPEATC FORALL_SIMP_CONV) tm diff --git a/src/num/arith/src/Solve_ineqs.sml b/src/num/arith/src/Solve_ineqs.sml index 7a7fbb0e77..ff82544d3c 100644 --- a/src/num/arith/src/Solve_ineqs.sml +++ b/src/num/arith/src/Solve_ineqs.sml @@ -27,9 +27,7 @@ infix << THENC ##; val num_CONV = Num_conv.num_CONV; val MATCH_MP = Drule.MATCH_MP; -fun failwith function = raise HOL_ERR{origin_structure = "Solve_ineqs", - origin_function = function, - message = ""}; +fun failwith function = raise mk_HOL_ERR "Solve_ineqs" function "" (*===========================================================================*) diff --git a/src/num/arith/src/Sub_and_cond.sml b/src/num/arith/src/Sub_and_cond.sml index 14a5490fbc..5423d4a78b 100644 --- a/src/num/arith/src/Sub_and_cond.sml +++ b/src/num/arith/src/Sub_and_cond.sml @@ -23,10 +23,7 @@ struct val COND_ABS = boolTheory.COND_ABS; val TOP_DEPTH_CONV = Conv.TOP_DEPTH_CONV; -fun failwith function = - raise HOL_ERR{origin_structure = "Sub_and_cond", - origin_function = function, - message = ""}; +fun failwith function = raise mk_HOL_ERR "Sub_and_cond" function "" (*---------------------------------------------------------------------------*) diff --git a/src/num/arith/src/Sup_Inf.sml b/src/num/arith/src/Sup_Inf.sml index a4f3643e62..04edbeec04 100644 --- a/src/num/arith/src/Sup_Inf.sml +++ b/src/num/arith/src/Sup_Inf.sml @@ -27,9 +27,7 @@ open Rationals; open Lib; infix ##; open Feedback; -fun failwith function = raise HOL_ERR{origin_structure = "Sup_Inf", - origin_function = function, - message = ""}; +fun failwith function = raise mk_HOL_ERR "Sup_Inf" function "" (*===========================================================================*) diff --git a/src/num/theories/cv_compute/tailrecLib.sml b/src/num/theories/cv_compute/tailrecLib.sml index ebcbb73f73..154d75247b 100644 --- a/src/num/theories/cv_compute/tailrecLib.sml +++ b/src/num/theories/cv_compute/tailrecLib.sml @@ -3,8 +3,7 @@ struct open HolKernel Parse boolLib simpLib boolSimps -fun mk_HOL_ERR f msg = HOL_ERR {origin_structure = "tailrecLib", - origin_function = f, message = msg} +val ERR = mk_HOL_ERR "tailrecLib" type thmloc = DB_dtype.thm_src_location @@ -59,7 +58,7 @@ fun mk_sum_term fn_t inty tm = else case strip_to_dest fn_t [] t of SOME xs => if null xs then - raise mk_HOL_ERR "mk_sum_term" "malformed term" + raise ERR "mk_sum_term" "malformed term" else sumSyntax.mk_inl (pairSyntax.list_mk_pair xs, type_of t) diff --git a/src/parse/GrammarAncestry.sml b/src/parse/GrammarAncestry.sml index 16e30add83..12c0308c8b 100644 --- a/src/parse/GrammarAncestry.sml +++ b/src/parse/GrammarAncestry.sml @@ -3,8 +3,7 @@ struct open HolKernel HOLsexp -fun ERR f s = HOL_ERR {origin_structure = "GrammarAncestry", - origin_function = f, message = s} +val ERR = mk_HOL_ERR "GrammarAncestry" val tag = "GrammarAncestry" infix >~ >> diff --git a/src/parse/GrammarSpecials.sml b/src/parse/GrammarSpecials.sml index 9986a768c5..90ed27d186 100644 --- a/src/parse/GrammarSpecials.sml +++ b/src/parse/GrammarSpecials.sml @@ -88,17 +88,15 @@ struct val constructorsfn = ref (NONE : ({Thy:string,Tyop:string} -> term list) option) + val ERR = mk_HOL_ERR "GrammarSpecials" + fun compile_pattern_match t = case !compilefn of - NONE => raise HOL_ERR {origin_function = "compile_pattern_match", - origin_structure = "GrammarSpecials", - message = "Function not initialised"} + NONE => raise ERR "compile_pattern_match" "Function not initialised" | SOME f => f t fun type_constructors s = case !constructorsfn of - NONE => raise HOL_ERR {origin_function = "type_constructors", - origin_structure = "GrammarSpecials", - message = "Function not initialised"} + NONE => raise ERR "type_constructors" "Function not initialised" | SOME f => f s fun set_case_specials (cmp,cnst) = (compilefn := SOME cmp; diff --git a/src/parse/Parse.sml b/src/parse/Parse.sml index d21873ae3e..e69e8cad75 100644 --- a/src/parse/Parse.sml +++ b/src/parse/Parse.sml @@ -573,9 +573,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 {message = m, origin_structure = s, ...} => - raise HOL_ERR {message = m, origin_function = fnm, - origin_structure = s} + f x handle HOL_ERR e => raise HOL_ERR (set_origin_function fnm e) fun thytype_abbrev0 r = [TYABBREV r] val temp_thytype_abbrev = mk_temp_tyd thytype_abbrev0 diff --git a/src/parse/testutils.sml b/src/parse/testutils.sml index 262673dce2..ee358c9881 100644 --- a/src/parse/testutils.sml +++ b/src/parse/testutils.sml @@ -231,7 +231,7 @@ fun convtest (nm,conv,tm,expected) = fun check_HOL_ERRexn P e = case e of - HOL_ERR{origin_structure,origin_function,message} => + HOL_ERR{origin_structure,origin_function,message,...} => P (origin_structure, origin_function, message) | _ => false diff --git a/src/parse/type_grammar.sml b/src/parse/type_grammar.sml index dbd9475397..e40a228d85 100644 --- a/src/parse/type_grammar.sml +++ b/src/parse/type_grammar.sml @@ -97,9 +97,8 @@ fun initialise_typrinter f = if not (!initialised_printer) then (type_printer := f; initialised_printer := true) else - raise Feedback.HOL_ERR {origin_structure = "type_grammar", - origin_function = "initialised_printer", - message = "Printer function already initialised"} + raise Feedback.mk_HOL_ERR "type_grammar" "initialised_printer" + "Printer function already initialised" fun pp_type g ty = (!type_printer) g ty diff --git a/src/postkernel/Theory.sml b/src/postkernel/Theory.sml index 86121ff355..030cfc6028 100644 --- a/src/postkernel/Theory.sml +++ b/src/postkernel/Theory.sml @@ -85,7 +85,7 @@ fun call_hooks td = let "Hook "^nm^" failed on event " ^ TheoryDelta.toString td in f td - handle e as HOL_ERR {origin_function,origin_structure,message} => + handle e as HOL_ERR _ => Feedback.HOL_WARNING "Theory" "callhooks" diff --git a/src/prekernel/Feedback.sig b/src/prekernel/Feedback.sig index c46e7d1ac4..fb13160ada 100644 --- a/src/prekernel/Feedback.sig +++ b/src/prekernel/Feedback.sig @@ -2,6 +2,7 @@ signature Feedback = sig type error_record = {origin_structure : string, origin_function : string, + source_location : locn.locn, message : string} exception HOL_ERR of error_record @@ -9,6 +10,8 @@ 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 val emit_MESG : bool ref diff --git a/src/prekernel/Feedback.sml b/src/prekernel/Feedback.sml index e440418d89..2c6f0e22e0 100644 --- a/src/prekernel/Feedback.sml +++ b/src/prekernel/Feedback.sml @@ -13,6 +13,7 @@ struct type error_record = {origin_structure : string, origin_function : string, + source_location : locn.locn, message : string} exception HOL_ERR of error_record @@ -24,6 +25,7 @@ exception HOL_ERR of error_record fun mk_HOL_ERR s1 s2 s3 = HOL_ERR {origin_structure = s1, origin_function = s2, + source_location = locn.Loc_Unknown, message = s3} (* Errors with a known location. *) @@ -31,10 +33,20 @@ fun mk_HOL_ERR s1 s2 s3 = fun mk_HOL_ERRloc s1 s2 locn s3 = HOL_ERR {origin_structure = s1, origin_function = s2, - message = locn.toString locn ^ ":\n" ^ s3} - (* Would like to be much cleverer, adding a field - source_location:locn to error_record, but the pain of fixing all - occurrences of HOL_ERR would be too great. *) + source_location = locn, + message = s3} + +fun set_origin_function fnm {origin_structure, source_location, message, ...} = + {origin_structure = origin_structure, + source_location = source_location, + origin_function = fnm, + message = message} + +fun set_message msg {origin_structure, source_location, origin_function, ...} = + {origin_structure = origin_structure, + source_location = source_location, + origin_function = origin_function, + message = msg} val ERR = mk_HOL_ERR "Feedback" (* local to this file *) @@ -75,9 +87,10 @@ fun quiet_messages f = Portable.with_flag (emit_MESG, false) f * Formatting and output for exceptions, messages, and warnings. * *---------------------------------------------------------------------------*) -fun format_err_rec {message, origin_function, origin_structure} = +fun format_err_rec {message, origin_function, origin_structure, source_location} = String.concat - ["at ", origin_structure, ".", origin_function, ":\n", message] + ["at ", origin_structure, ".", origin_function, ":\n", + locn.toString source_location, ":\n", message] fun format_ERR err_rec = String.concat ["\nException raised ", format_err_rec err_rec, "\n"] diff --git a/src/quotient/examples/lambda/barendregt.sml b/src/quotient/examples/lambda/barendregt.sml index 7c0f7693d4..a36b33fc8f 100644 --- a/src/quotient/examples/lambda/barendregt.sml +++ b/src/quotient/examples/lambda/barendregt.sml @@ -71,9 +71,7 @@ val (asl,gl) = top_goal(); fun TACTIC_ERR{function,message} = - Feedback.HOL_ERR{origin_structure = "Tactic", - origin_function = function, - message = message}; + Feedback.mk_HOL_ERR "Tactic" function message fun failwith function = ( (* if debug_fail then diff --git a/src/quotient/examples/lambda/betaScript.sml b/src/quotient/examples/lambda/betaScript.sml index a021abb096..8d1f3f02d4 100644 --- a/src/quotient/examples/lambda/betaScript.sml +++ b/src/quotient/examples/lambda/betaScript.sml @@ -75,9 +75,8 @@ val TC_INDUCT_TAC = val tc_thm' = BETA_RULE(ISPEC P (ISPEC R tc_thm)) in MATCH_MP_TAC tc_thm' (asl,w) end - handle _ => raise HOL_ERR{origin_structure = "", - origin_function = "TC_INDUCT_TAC", - message = "Unanticipated term structure"} + handle _ => raise mk_HOL_ERR "" "TC_INDUCT_TAC" + "Unanticipated term structure" in tac end; @@ -1563,9 +1562,8 @@ val RC_INDUCT_TAC = val rc_thm' = BETA_RULE(ISPEC P (ISPEC R rc_thm)) in MATCH_MP_TAC rc_thm' (asl,w) end - handle _ => raise HOL_ERR{origin_structure = "", - origin_function = "RC_INDUCT_TAC", - message = "Unanticipated term structure"} + handle _ => raise mk_HOL_ERR "" "RC_INDUCT_TAC" + "Unanticipated term structure" in tac end; diff --git a/src/quotient/examples/lambda/etaScript.sml b/src/quotient/examples/lambda/etaScript.sml index 221dd932b2..a6217ac42c 100644 --- a/src/quotient/examples/lambda/etaScript.sml +++ b/src/quotient/examples/lambda/etaScript.sml @@ -77,9 +77,8 @@ val RC_INDUCT_TAC = val rc_thm' = BETA_RULE(ISPEC P (ISPEC R rc_thm)) in MATCH_MP_TAC rc_thm' (asl,w) end - handle _ => raise HOL_ERR{origin_structure = "", - origin_function = "RC_INDUCT_TAC", - message = "Unanticipated term structure"} + handle _ => raise mk_HOL_ERR "" "RC_INDUCT_TAC" + "Unanticipated term structure" in tac end; @@ -116,9 +115,8 @@ val TC_INDUCT_TAC = val tc_thm' = BETA_RULE(ISPEC P (ISPEC R tc_thm)) in MATCH_MP_TAC tc_thm' (asl,w) end - handle _ => raise HOL_ERR{origin_structure = "", - origin_function = "TC_INDUCT_TAC", - message = "Unanticipated term structure"} + handle _ => raise mk_HOL_ERR "" "TC_INDUCT_TAC" + "Unanticipated term structure" in tac end; diff --git a/src/quotient/examples/lambda/reductionScript.sml b/src/quotient/examples/lambda/reductionScript.sml index bef3ad0606..87e55c47bd 100644 --- a/src/quotient/examples/lambda/reductionScript.sml +++ b/src/quotient/examples/lambda/reductionScript.sml @@ -68,9 +68,8 @@ val TC_INDUCT_TAC = val tc_thm' = BETA_RULE(ISPEC P (ISPEC R tc_thm)) in MATCH_MP_TAC tc_thm' (asl,w) end - handle _ => raise HOL_ERR{origin_structure = "", - origin_function = "TC_INDUCT_TAC", - message = "Unanticipated term structure"} + handle _ => raise mk_HOL_ERR "" "TC_INDUCT_TAC" + "Unanticipated term structure" in tac end; @@ -250,9 +249,8 @@ val RC_INDUCT_TAC = val rc_thm' = BETA_RULE(ISPEC P (ISPEC R rc_thm)) in MATCH_MP_TAC rc_thm' (asl,w) end - handle _ => raise HOL_ERR{origin_structure = "", - origin_function = "RC_INDUCT_TAC", - message = "Unanticipated term structure"} + handle _ => raise mk_HOL_ERR "" "RC_INDUCT_TAC" + "Unanticipated term structure" in tac end; diff --git a/src/quotient/examples/sigma/barendregt.sml b/src/quotient/examples/sigma/barendregt.sml index af26affa02..f9b60b0510 100644 --- a/src/quotient/examples/sigma/barendregt.sml +++ b/src/quotient/examples/sigma/barendregt.sml @@ -72,9 +72,7 @@ val (asl,gl) = top_goal(); fun TACTIC_ERR{function,message} = - Feedback.HOL_ERR{origin_structure = "Tactic", - origin_function = function, - message = message}; + Feedback.mk_HOL_ERR "Tactic" function message fun failwith function = ( (* if debug_fail then diff --git a/src/quotient/examples/sigma/reductionScript.sml b/src/quotient/examples/sigma/reductionScript.sml index 142707faba..3228191038 100644 --- a/src/quotient/examples/sigma/reductionScript.sml +++ b/src/quotient/examples/sigma/reductionScript.sml @@ -302,9 +302,8 @@ val RC_INDUCT_TAC = val rc_thm' = BETA_RULE(ISPEC P (ISPEC R rc_thm)) in MATCH_MP_TAC rc_thm' (asl,w) end - handle _ => raise HOL_ERR{origin_structure = "", - origin_function = "RC_INDUCT_TAC", - message = "Unanticipated term structure"} + handle _ => raise mk_HOL_ERR "" "RC_INDUCT_TAC" + "Unanticipated term structure" in tac end; diff --git a/src/quotient/examples/sigma/semanticsScript.sml b/src/quotient/examples/sigma/semanticsScript.sml index 638a9f1be6..daad3dcb39 100644 --- a/src/quotient/examples/sigma/semanticsScript.sml +++ b/src/quotient/examples/sigma/semanticsScript.sml @@ -82,9 +82,8 @@ val TC_INDUCT_TAC = val tc_thm' = BETA_RULE(ISPEC P (ISPEC R tc_thm)) in MATCH_MP_TAC tc_thm' (asl,w) end - handle _ => raise HOL_ERR{origin_structure = "", - origin_function = "TC_INDUCT_TAC", - message = "Unanticipated term structure"} + handle _ => raise mk_HOL_ERR "" "TC_INDUCT_TAC" + "Unanticipated term structure" in tac end; @@ -1794,9 +1793,8 @@ val RC_INDUCT_TAC = val rc_thm' = BETA_RULE(ISPEC P (ISPEC R rc_thm)) in MATCH_MP_TAC rc_thm' (asl,w) end - handle _ => raise HOL_ERR{origin_structure = "", - origin_function = "RC_INDUCT_TAC", - message = "Unanticipated term structure"} + handle _ => raise mk_HOL_ERR "" "RC_INDUCT_TAC" + "Unanticipated term structure" in tac end; diff --git a/src/quotient/examples/tactics.sig b/src/quotient/examples/tactics.sig index 1d68db6489..7d59b656f0 100644 --- a/src/quotient/examples/tactics.sig +++ b/src/quotient/examples/tactics.sig @@ -56,9 +56,7 @@ val IMP2AND : thm -> thm (* val TACTIC_ERR{function,message} = - Exception.HOL_ERR{origin_structure = "Tactic", - origin_function = function, - message = message}; + Exception.mk_HOL_ERR "Tactic" function message *) val failwith : string -> 'a diff --git a/src/quotient/examples/tactics.sml b/src/quotient/examples/tactics.sml index 5f5a9014da..7418648fd5 100644 --- a/src/quotient/examples/tactics.sml +++ b/src/quotient/examples/tactics.sml @@ -161,9 +161,7 @@ val AND2IMP = REWRITE_RULE[(SYM o SPEC_ALL)AND_IMP_INTRO]; val IMP2AND = REWRITE_RULE[AND_IMP_INTRO]; fun TACTIC_ERR{function,message} = - Feedback.HOL_ERR{origin_structure = "Tactic", - origin_function = function, - message = message}; + Feedback.mk_HOL_ERR "Tactic" function message fun failwith function = raise TACTIC_ERR{function = function,message = ""}; diff --git a/src/quotient/src/quotient.sml b/src/quotient/src/quotient.sml index 33631321f9..0b444885d3 100644 --- a/src/quotient/src/quotient.sml +++ b/src/quotient/src/quotient.sml @@ -635,12 +635,9 @@ fun is_partial_equiv th = is_match_term partial_equiv_tm (concl th); fun check_equiv th = is_equiv th orelse is_partial_equiv th orelse - raise HOL_ERR { - origin_structure = "quotient", - origin_function = "check_equiv", - message = "The following is neither an equivalence nor a partial equivalence theorem:\n" ^ - thm_to_string th ^ "\n" - } + raise mk_HOL_ERR "quotient" "check_equiv" + ("The following is neither an equivalence nor a partial equivalence theorem:\n" ^ + thm_to_string th ^ "\n") fun distinct [] = true | distinct (x::xs) = not (mem x xs) andalso distinct xs @@ -678,12 +675,9 @@ fun check_tyop_equiv th = null (Term.free_vars (concl th)) andalso is_match_term equiv_tm uncond_tm orelse raise Match end - handle e => raise HOL_ERR { - origin_structure = "quotient", - origin_function = "check_tyop_equiv", - message = "The following does not have the form of a type quotient extension theorem:\n" ^ - thm_to_string th ^ "\n" - } + handle e => raise mk_HOL_ERR "quotient" "check_tyop_equiv" + ("The following does not have the form of a type quotient extension theorem:\n" ^ + thm_to_string th ^ "\n") fun dest_QUOTIENT_cond tm = @@ -722,12 +716,9 @@ fun check_tyop_quotient th = null (Term.free_vars (concl th)) andalso is_match_term quotient_tm uncond_tm orelse raise Match end - handle e => raise HOL_ERR { - origin_structure = "quotient", - origin_function = "check_tyop_quotient", - message = "The following does not have the form of a quotient type extension theorem:\n" ^ - thm_to_string th ^ "\n" - } + handle e => raise mk_HOL_ERR "quotient" "check_tyop_quotient" + ("The following does not have the form of a quotient type extension theorem:\n" ^ + thm_to_string th ^ "\n") fun check_tyop_simp th = let val tm = concl th @@ -741,12 +732,9 @@ fun check_tyop_simp th = in true end - handle e => raise HOL_ERR { - origin_structure = "quotient", - origin_function = "check_tyop_simp", - message = "The following does not have the form of a simplification theorem for either\nrelation extension simplification or map function extension simplification:\n" ^ - thm_to_string th ^ "\n" - } + handle e => raise mk_HOL_ERR "quotient" "check_tyop_simp" + ("The following does not have the form of a simplification theorem for either\nrelation extension simplification or map function extension simplification:\n" ^ + thm_to_string th ^ "\n") fun define_quotient_type tyname abs rep equiv = @@ -1076,12 +1064,9 @@ fun find_base tm = (find_base o #conseq o dest_imp o snd o strip_forall) tm fun equiv_type th = (fst o dom_rng o type_of o rand o find_base o concl) th (* (#Ty o dest_var o #Bvar o dest_forall o find_base o concl) th *) - handle e => raise HOL_ERR { - origin_structure = "quotient", - origin_function = "equiv_type", - message ="Invalid structure of equivalence theorem:\n" - ^ thm_to_string th ^ "\n" - } + handle e => raise mk_HOL_ERR "quotient" "equiv_type" + ("Invalid structure of equivalence theorem:\n" + ^ thm_to_string th ^ "\n") fun make_equiv equivs tyop_equivs ty = let val base_tys = map equiv_type equivs @@ -1122,13 +1107,8 @@ fun make_equiv equivs tyop_equivs ty = handle _ => identity_equiv ty in main_make_equiv ty - handle _ =>raise HOL_ERR { - origin_structure = "quotient", - origin_function = "make_equiv", - message = "Could not form the " ^ - "equivalence theorem for " ^ - type_to_string ty - } + handle _ => raise mk_HOL_ERR "quotient" "make_equiv" + ("Could not form the equivalence theorem for " ^ type_to_string ty) end; @@ -1153,14 +1133,11 @@ fun pth s th = if !chatting then (print s; print_thm th; print "\n"; th) else th; (**) -fun quotient_type th = (hd o tl o #Args o dest_type o type_of - o rand o find_base o concl) th - handle e => raise HOL_ERR { - origin_structure = "quotient", - origin_function = "quotient_type", - message ="Invalid structure of quotient theorem:\n" - ^ thm_to_string th ^ "\n" - } +fun quotient_type th = + (hd o tl o #Args o dest_type o type_of + o rand o find_base o concl) th + handle e => raise mk_HOL_ERR "quotient" "quotient_type" + ("Invalid structure of quotient theorem:\n" ^ thm_to_string th ^ "\n") fun make_hyp_quotient hyp_quots quots tyop_quots ty = let val base_tys = map quotient_type quots @@ -1381,16 +1358,14 @@ fun check_quotient_ty tys_quot_ths ty = (* (#Tyop(dest_type rty) = Tyop) *) val ty_qty = tryfind is_ty_qth tys_quot_ths handle HOL_ERR e => - raise HOL_ERR { - origin_structure = "quotient", - origin_function = "check_quotient_ty", - message = "Could not lift the type `" ^ + raise ERR "check_quotient_ty" + ("Could not lift the type `" ^ type_to_string ty ^ "`;\n" ^ "Missing quotient extension theorem for type constructor " ^ "\"" ^ Tyop ^ "\".\n" ^ "Please prove and add to \"tyop_quotients\" inputs for quotient package.\n " (* ^ exn_to_string (HOL_ERR e) *) - } + ) in ty end @@ -1664,15 +1639,11 @@ fun lift_theorem_by_quotients quot_ths equivs tyop_equivs handle HOL_ERR _ => false ) tyop_simps orelse - Raise (HOL_ERR { - origin_structure = "quotient", - origin_function = "check_simp", - message = - "Missing quotient simplification theorem:\n" ^ + Raise (mk_HOL_ERR "quotient" "check_simp" + ("Missing quotient simplification theorem:\n" ^ with_flag (show_types, true) thm_to_string (mk_oracle_thm "quotient" ([],tm)) ^ "\n" ^ - "Please prove and add to \"tyop_simps\" inputs for quotient package.\n " - }) + "Please prove and add to \"tyop_simps\" inputs for quotient package.\n ")) fun check_tyop_simps_present tyop = let val (taus,ksis,Rs,abss,reps,conseq) = strip_QUOTIENT_cond (concl tyop) @@ -1752,11 +1723,7 @@ fun lift_theorem_by_quotients quot_ths equivs tyop_equivs let val (tmtheta,tytheta) = match_term pat ob val pat' = inst tytheta pat in if pat' ~~ ob then (tmtheta,tytheta) - else raise raise HOL_ERR { - origin_structure = "quotient", - origin_function = "match_ty_term", - message = "not a match" - } + else raise ERR "match_ty_term" "not a match" end (* For each constant being lifted, check that its respectfulness theorem @@ -1805,15 +1772,12 @@ fun lift_theorem_by_quotients quot_ths equivs tyop_equivs in GENL margs (SPEC mterm mrefl) end - handle e => raise HOL_ERR - { origin_structure = "quotient", - origin_function = "make_missing_respects", - message = "Missing respectfulness theorem for " ^ + handle e => raise ERR "make_missing_respects" + ("Missing respectfulness theorem for " ^ term_to_string mfunc ^ ".\n" ^ with_flag (show_types, true) thm_to_string (mk_oracle_thm "quotient" ([], fake_respects mfunc)) ^ "\n" ^ - "Please prove and add to \"respects\" inputs for quotient package.\n " - } + "Please prove and add to \"respects\" inputs for quotient package.\n ") in map make_missing_respects missing @ respects end @@ -2303,24 +2267,18 @@ fun lift_theorem_by_quotients quot_ths equivs tyop_equivs else if is_var tm then [] else let val {Name=nm, Ty= ty} = dest_const tm val (atys,rty) = strip_type ty - fun err1 () = HOL_ERR { - origin_structure = "quotient", - origin_function = "findops", - message = "Missing polymorphic respectfulness theorem for `" ^ + fun err1 () = ERR "findops" + ("Missing polymorphic respectfulness theorem for `" ^ term_to_string tm ^ "`.\n" ^ with_flag (show_types, true) thm_to_string (mk_oracle_thm "quotient" ([], fake_poly_respects tm)) ^ "\n" ^ - "Please prove and add to \"poly_respects\" inputs for quotient package.\n " - } - fun err2 () = HOL_ERR { - origin_structure = "quotient", - origin_function = "findops", - message = "Missing polymorphic preservation theorem for `" ^ + "Please prove and add to \"poly_respects\" inputs for quotient package.\n ") + fun err2 () = ERR "findops" + ("Missing polymorphic preservation theorem for `" ^ term_to_string tm ^ "`.\n" ^ with_flag (show_types, true) thm_to_string (mk_oracle_thm "quotient" ([], fake_poly_preserves tm)) ^ "\n" ^ - "Please prove and add to \"poly_preserves\" inputs for quotient package.\n " - } + "Please prove and add to \"poly_preserves\" inputs for quotient package.\n ") in if is_rep_ty ty then if mem (#Name(dest_const tm)) ("respects" :: RELnms @ tyop_RELnms) orelse exists (can (match_ty_term tm)) newdeffuncs @@ -2631,12 +2589,9 @@ corresponding quotient theorem antecedents are resolvable. in tryfind (get_higher_df_op tm) polydfs end - handle e => raise HOL_ERR { - origin_structure = "quotient", - origin_function = "MK_DEF_OP", - message = "Missing polymorphic preservation theorem for " ^ - term_to_string tm ^ ".\n" - } + handle e => raise ERR "MK_DEF_OP" + ("Missing polymorphic preservation theorem for " ^ + term_to_string tm ^ ".\n") (* The tactic LAMBDA_RSP_TAC: @@ -3126,14 +3081,11 @@ R2 (f[x']) (g[y']). th end handle _ => - raise HOL_ERR { - origin_structure = "quotient", - origin_function = "TRANSFORM_CONV", - message = "Could not convert to higher types the term\n" ^ + raise ERR "TRANSFORM_CONV" + ("Could not convert to higher types the term\n" ^ term_to_string tm ^ "\n" ^ "May be missing a respects or a poly_respects theorem" - ^ " for some constant in it." - } + ^ " for some constant in it.") (* ------------------------------------------------------------------------- *) @@ -3440,14 +3392,11 @@ R2 (f[x']) (g[y']). in MP rth th end - handle _ => raise HOL_ERR { - origin_structure = "quotient", - origin_function = "REGULARIZE", - message = "Could not lift the irregular theorem\n" ^ + handle _ => raise ERR "REGULARIZE" + ("Could not lift the irregular theorem\n" ^ thm_to_string th ^ "\n" ^ "May try proving and then lifting\n" ^ - term_to_string tm' - } + term_to_string tm') end @@ -3471,14 +3420,11 @@ R2 (f[x']) (g[y']). in () end else (); if is_rep_ty (type_of tm) then - raise HOL_ERR { - origin_structure = "quotient", - origin_function = "check_high", - message = "Could not lift the term " ^ - term_to_string tm ^ "\n" ^ - "May be missing a constant to be lifted, " ^ - "or a poly_preserves theorem." - } + raise ERR "check_high" + ("Could not lift the term " ^ + term_to_string tm ^ "\n" ^ + "May be missing a constant to be lifted, " ^ + "or a poly_preserves theorem.") else () ) @@ -3583,13 +3529,10 @@ R2 (f[x']) (g[y']). Ho_Rewrite.PURE_REWRITE_RULE LAM_APP_DEFS o QUOT_REWRITE_RULE [GSYM EQUALS_PRS] o CONV_RULE TRANSFORM_CONV) thr - handle e => raise HOL_ERR { - origin_structure = "quotient", - origin_function = "LIFT_RULE", - message = "Could not lift the theorem\n" ^ + handle e => raise ERR "LIFT_RULE" + ("Could not lift the theorem\n" ^ thm_to_string th ^ "\n" ^ - exn_to_string e - } + exn_to_string e) end) in @@ -3639,12 +3582,9 @@ fun check_respects_tm tm = fun check_respects th = null (Term.free_vars (concl th)) andalso check_respects_tm (concl th) - handle e => raise HOL_ERR { - origin_structure = "quotient", - origin_function = "check_respects", - message = "The following theorem is not of the right form for a respectfulness theorem:\n" ^ - thm_to_string th ^ "\n" - }; + handle e => raise ERR "check_respects" + ("The following theorem is not of the right form for a respectfulness theorem:\n" ^ + thm_to_string th ^ "\n") (* --------------------------------------------------------------- *) @@ -3662,12 +3602,9 @@ fun check_poly_respects th = null (Term.free_vars (concl th)) andalso check_respects_tm uncond_tm end - handle e => raise HOL_ERR { - origin_structure = "quotient", - origin_function = "check_poly_respects", - message = "The following theorem is not of the right form for a polymorphic respectfulness\ntheorem:\n" ^ - thm_to_string th ^ "\n" - }; + handle e => raise ERR "check_poly_respects" + ("The following theorem is not of the right form for a polymorphic respectfulness\ntheorem:\n" ^ + thm_to_string th ^ "\n") local fun any_type_var_in tyl ty = exists (C type_var_in ty) tyl @@ -3709,12 +3646,9 @@ fun check_poly_preserves th = in true end - handle e => raise HOL_ERR { - origin_structure = "quotient", - origin_function = "check_poly_preserves", - message = "The following theorem is not of the right form for a polymorphic preservation\ntheorem:\n" ^ - thm_to_string th ^ "\n" - } + handle e => raise ERR "check_poly_preserves" + ("The following theorem is not of the right form for a polymorphic preservation\ntheorem:\n" ^ + thm_to_string th ^ "\n") end; @@ -4013,12 +3947,9 @@ fun is_inhab th = is_ho_match_term inhab_tm (concl th); fun check_inhab th = is_inhab th orelse - raise HOL_ERR { - origin_structure = "quotient", - origin_function = "check_inhab", - message = "The following is not a predicate inhabitation theorem:\n" ^ - thm_to_string th ^ "\n" - } + raise ERR "check_inhab" + ("The following is not a predicate inhabitation theorem:\n" ^ + thm_to_string th ^ "\n") fun dest_con_inhab c = let open Psyntax @@ -4038,12 +3969,9 @@ fun check_con_inhab th = in null (Term.free_vars (concl th)) orelse raise Match end - handle e => raise HOL_ERR { - origin_structure = "quotient", - origin_function = "check_con_inhab", - message = "The following does not have the form of a constant inhabitation theorem:\n" ^ - thm_to_string th ^ "\n" - } + handle e => raise ERR "check_con_inhab" + ("The following does not have the form of a constant inhabitation theorem:\n" ^ + thm_to_string th ^ "\n") fun tryconv f (x:'a) = f x handle HOL_ERR _ => x @@ -4127,12 +4055,9 @@ fun prove_subset_respects Rdefs = val PRs = map dest_Rdef Rdefs val (Ps,Rcons) = unzip PRs fun find_R [] tm = - raise HOL_ERR { - origin_structure = "quotient", - origin_function = "prove_subset_respects", - message = "Term does not match expected predicates: " ^ - term_to_string tm - } + raise ERR "prove_subset_respects" + ("Term does not match expected predicates: " ^ + term_to_string tm) | find_R ((P,R)::rest) tm = let val (x,body) = dest_abs P val (tmS,tyS) = match_term body tm diff --git a/src/real/hrealScript.sml b/src/real/hrealScript.sml index 917375b1b8..1b94fdad56 100644 --- a/src/real/hrealScript.sml +++ b/src/real/hrealScript.sml @@ -1015,8 +1015,7 @@ fun rmel i list = [] => [] | h::t => if aconv h i then t else h :: rmel i t -fun ERR s = HOL_ERR{origin_structure = "realaxScript", - origin_function = "CANCEL_CONV", message = s}; +fun ERR s = mk_HOL_ERR "realaxScript" "CANCEL_CONV"s fun CANCEL_CONV(assoc,sym,lcancelthms) tm = let val lcthms = map (intro o SPEC_ALL) lcancelthms diff --git a/src/res_quan/src/Cond_rewrite.sml b/src/res_quan/src/Cond_rewrite.sml index 1db9459bb8..3c1047e486 100644 --- a/src/res_quan/src/Cond_rewrite.sml +++ b/src/res_quan/src/Cond_rewrite.sml @@ -13,9 +13,7 @@ open HolKernel boolLib Rsyntax; infix ## THEN THENL ORELSEC; fun COND_REWR_ERR {function,message} = - HOL_ERR{origin_structure = "Cond_rewrite", - origin_function = function, - message = message}; + mk_HOL_ERR "Cond_rewrite" function message val frees = rev o Term.free_vars; diff --git a/src/ring/src/EVAL_quote.sml b/src/ring/src/EVAL_quote.sml index 3684350ef0..d01f86fc69 100644 --- a/src/ring/src/EVAL_quote.sml +++ b/src/ring/src/EVAL_quote.sml @@ -9,10 +9,7 @@ struct val (Type,Term) = parse_from_grammars EVAL_quoteTheory.EVAL_quote_grammars end -fun QUOTE_ERR function message = - HOL_ERR{origin_structure = "quote", - origin_function = function, - message = message}; +val QUOTE_ERR = mk_HOL_ERR "quote" fun mk_comb2 (a,b,c) = mk_comb(mk_comb(a,b),c); fun mk_comb3 (a,b,c,d) = mk_comb(mk_comb2(a,b,c),d); diff --git a/src/ring/src/EVAL_ringLib.sml b/src/ring/src/EVAL_ringLib.sml index b4f2306489..374792539d 100644 --- a/src/ring/src/EVAL_ringLib.sml +++ b/src/ring/src/EVAL_ringLib.sml @@ -4,10 +4,7 @@ struct open HolKernel Parse boolLib ternaryComparisonsTheory EVAL_quoteTheory EVAL_quote computeLib; -fun RING_ERR function message = - HOL_ERR{origin_structure = "ringLib", - origin_function = function, - message = message}; +val RING_ERR = mk_HOL_ERR "ringLib" (* reify ring expressions: building a signature, which is the correspondence diff --git a/src/ring/src/abstraction.sml b/src/ring/src/abstraction.sml index 43c82d3477..0253c30ca1 100644 --- a/src/ring/src/abstraction.sml +++ b/src/ring/src/abstraction.sml @@ -4,10 +4,7 @@ struct open HolKernel Parse boolLib; infix o |->; -fun ABS_ERR function message = - HOL_ERR{origin_structure = "abs_tools", - origin_function = function, - message = message}; +val ABS_ERR = mk_HOL_ERR "abs_tools" val curr_assums = ref ([]:term list); val fv_ass = ref ([]:term list); diff --git a/src/simp/src/Opening.sml b/src/simp/src/Opening.sml index fb1b561d26..a48b267a69 100644 --- a/src/simp/src/Opening.sml +++ b/src/simp/src/Opening.sml @@ -252,9 +252,7 @@ in fn {relation,solver,depther,freevars} => if allunch then (* note critical link between this exception and traversal code in Traverse.FIRSTCQC_CONV *) - raise HOL_ERR { origin_structure = "Opening", - origin_function = "CONGPROC", - message = "Congruence gives no change" } + raise mk_HOL_ERR "Opening" "CONGPROC" "Congruence gives no change" else (trace(3,PRODUCE(tm,"congruence rule",final_thm)); final_thm) end end; diff --git a/src/simp/src/Traverse.sml b/src/simp/src/Traverse.sml index 2294bab4d6..e1f5e5c285 100644 --- a/src/simp/src/Traverse.sml +++ b/src/simp/src/Traverse.sml @@ -185,7 +185,7 @@ fun FIRSTCQC_CONV [] t = failwith "no conversion worked" c t handle e as HOL_ERR { origin_structure = "Opening", origin_function = "CONGPROC", - message = "Congruence gives no change"} => raise e + message = "Congruence gives no change", ...} => raise e | Interrupt => raise Interrupt | _ => FIRSTCQC_CONV cs t end diff --git a/src/tactictoe/src/tttEval.sml b/src/tactictoe/src/tttEval.sml index 217069be61..f955ebe6b5 100644 --- a/src/tactictoe/src/tttEval.sml +++ b/src/tactictoe/src/tttEval.sml @@ -15,14 +15,14 @@ open HolKernel Abbrev boolLib aiLib val ERR = mk_HOL_ERR "tttEval" fun catch_err msg f x = - f x handle HOL_ERR {origin_structure,origin_function,message} => + f x handle HOL_ERR {origin_structure,origin_function,source_location,message} => (print_endline - (msg ^ ":" ^ origin_structure ^ ":" ^ origin_function ^ ":" ^ message); + (msg ^ ":" ^ origin_structure ^ ":" ^ origin_function ^ ":" ^ locn.toShortString source_location ^ ":" ^ message); raise ERR "tttEval" "error caught (see log)") fun catch_err_ignore msg f x = - f x handle HOL_ERR {origin_structure,origin_function,message} => + f x handle HOL_ERR {origin_structure,origin_function,source_location,message} => (print_endline - (msg ^ ":" ^ origin_structure ^ ":" ^ origin_function ^ ":" ^ message)) + (msg ^ ":" ^ origin_structure ^ ":" ^ origin_function ^ ":" ^ locn.toShortString source_location ^ ^ ":" ^ message)) (* ------------------------------------------------------------------------- diff --git a/src/tfl/src/Defn.sml b/src/tfl/src/Defn.sml index df76599974..122a1a96b6 100644 --- a/src/tfl/src/Defn.sml +++ b/src/tfl/src/Defn.sml @@ -1264,8 +1264,8 @@ fun stdrec_defn (facts,(stem,stem'),wfrec_res,untuple) = in TotalDefn. ---------------------------------------------------------------------------*) -fun holexnMessage (HOL_ERR {origin_structure,origin_function,message}) = - origin_structure ^ "." ^ origin_function ^ ": " ^ message +fun holexnMessage (HOL_ERR {origin_structure,origin_function,source_location,message}) = + origin_structure ^ "." ^ origin_function ^ ":" ^ locn.toShortString source_location ^ ": " ^ message | holexnMessage e = General.exnMessage e fun is_simple_arg t = diff --git a/src/thm/otknl-thm.ML b/src/thm/otknl-thm.ML index a68f2fe642..8e23380c4b 100644 --- a/src/thm/otknl-thm.ML +++ b/src/thm/otknl-thm.ML @@ -1165,8 +1165,7 @@ fun mk_defn_thm (witness_tag, c, p) = Primitive Definition Principles ---------------------------------------------------------------------- *) -fun ERR f msg = HOL_ERR {origin_structure = "Thm", - origin_function = f, message = msg} +val ERR = mk_HOL_ERR "Thm" val TYDEF_ERR = ERR "prim_type_definition" val DEF_ERR = ERR "new_definition" val SPEC_ERR = ERR "new_specification" diff --git a/src/thm/std-thm.ML b/src/thm/std-thm.ML index b52d38ee4c..4b70017ac0 100644 --- a/src/thm/std-thm.ML +++ b/src/thm/std-thm.ML @@ -1106,8 +1106,7 @@ fun mk_defn_thm (witness_tag, c) = Primitive Definition Principles ---------------------------------------------------------------------- *) -fun ERR f msg = HOL_ERR {origin_structure = "Thm", - origin_function = f, message = msg} +val ERR = mk_HOL_ERR "Thm" val TYDEF_ERR = ERR "prim_type_definition" val DEF_ERR = ERR "new_definition" val SPEC_ERR = ERR "new_specification"