diff --git a/examples/lambda/basics/binderLib.sml b/examples/lambda/basics/binderLib.sml index 4cf8d2f3ba..bcb95d6497 100644 --- a/examples/lambda/basics/binderLib.sml +++ b/examples/lambda/basics/binderLib.sml @@ -290,9 +290,9 @@ fun check_for_errors tm = let "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) - handle Option => ERR "prove_recursive_term_function_exists" - ("No recursion theorem for type "^ - type_to_string dom_ty) + handle Option => + raise ERR "prove_recursive_term_function_exists" + ("No recursion theorem for type " ^ type_to_string dom_ty) val constructors = map #1 (find_constructors recthm) val () = case List.find @@ -507,8 +507,8 @@ fun define_wrapper worker q = let val a = Absyn q val f = head_sym a val fstr = case f of - Absyn.IDENT(_, s) => s - | x => ERR "define_recursive_term_function" "invalid head symbol" + Absyn.IDENT(_, s) => s + | x => raise ERR "define_recursive_term_function" "invalid head symbol" val restore_this = hide fstr fun restore() = Parse.update_overload_maps fstr restore_this val tm = Parse.absyn_to_term (Parse.term_grammar()) a diff --git a/examples/lambda/other-models/ncScript.sml b/examples/lambda/other-models/ncScript.sml index c7e042c1fc..c9c221cfa6 100644 --- a/examples/lambda/other-models/ncScript.sml +++ b/examples/lambda/other-models/ncScript.sml @@ -612,9 +612,7 @@ fun nc_INDUCT_TAC (A,g) = val ith = ISPEC P nc_INDUCTION fun bconv tm = if rator tm !~ P then - raise HOL_ERR{origin_structure = "ncScript.sml", - origin_function = "nc_INDUCT_TAC", - message = "function bconv failed"} + raise mk_HOL_ERR "ncScript.sml" "nc_INDUCT_TAC" "function bconv failed" else BETA_CONV tm val bth = CONV_RULE (ONCE_DEPTH_CONV bconv) ith in diff --git a/src/prekernel/Feedback.sml b/src/prekernel/Feedback.sml index 2c6f0e22e0..3579959d3d 100644 --- a/src/prekernel/Feedback.sml +++ b/src/prekernel/Feedback.sml @@ -90,7 +90,10 @@ fun quiet_messages f = Portable.with_flag (emit_MESG, false) f fun format_err_rec {message, origin_function, origin_structure, source_location} = String.concat ["at ", origin_structure, ".", origin_function, ":\n", - locn.toString source_location, ":\n", message] + case source_location of + Loc_Unknown => "" + | _ => 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/ind_rel.sml b/src/quotient/examples/ind_rel.sml index 6cce2f2b85..70dd0d1033 100644 --- a/src/quotient/examples/ind_rel.sml +++ b/src/quotient/examples/ind_rel.sml @@ -55,14 +55,10 @@ in (fst current_goal, new_claim)], fn [goalthm,claimthm] => MP (DISCH new_claim goalthm) claimthm - | _ => raise HOL_ERR - {origin_structure = "define_inductive_relations", - origin_function = "SUPPOSE_TAC", - message = "invalid application"}) - else raise HOL_ERR - {origin_structure = "define_inductive_relations", - origin_function = "SUPPOSE_TAC", - message = "The claim doesn't have type :bool"} + | _ => raise mk_HOL_ERR "define_inductive_relations" "SUPPOSE_TAC" + "invalid application") + else raise mk_HOL_ERR "define_inductive_relations" "SUPPOSE_TAC" + "The claim doesn't have type :bool" end @@ -122,19 +118,13 @@ fun MP_IMP_TAC imp_thm (thisgoal as (asms,goal)) = fn imp_thm => fn (asms,goal) => ([(asms,fst(dest_imp(concl imp_thm)))], fn [thm] => MP imp_thm thm - | _ => raise HOL_ERR - {origin_structure = "define_inductive_relations", - origin_function = "MP_IMP_TAC", - message = "invalid application"})} + | _ => raise mk_HOL_ERR "define_inductive_relations" "MP_IMP_TAC" + "invalid application")} thisgoal - else raise HOL_ERR - {origin_structure = "define_inductive_relations", - origin_function = "MP_IMP_TAC", - message = "theorem doesn't imply goal"} - else raise HOL_ERR - {origin_structure = "define_inductive_relations", - origin_function = "MP_IMP_TAC", - message = "theorem is not an implication"} + else raise mk_HOL_ERR "define_inductive_relations" "MP_IMP_TAC" + "theorem doesn't imply goal" + else raise mk_HOL_ERR "define_inductive_relations" "MP_IMP_TAC" + "theorem is not an implication" (* This function takes in the rules, checks them, quantifies them, and @@ -231,38 +221,34 @@ fun check_rule rule_num rule = (* check that the relations don't occur in rands *) if (foldr (fn (tm, acc) => relations_in_tm tm orelse acc) false rands) then - raise HOL_ERR - {message = "found relation being defined"^ + raise mk_HOL_ERR "define_inductive_relations" "check_rule" + ("found relation being defined"^ " in arg to "^(fst(dest_var rator))^ " in hypothesis ofrule number "^ - (Lib.int_to_string rule_num), - origin_function = "check_rule", - origin_structure = "define_inductive_relations"} + (Lib.int_to_string rule_num)) else check_hyp hyps - else if relations_in_tm hyp1 then raise HOL_ERR - {message = "found relation being defined"^ + else if relations_in_tm hyp1 then + raise mk_HOL_ERR "define_inductive_relations" "check_rule" + ("found relation being defined"^ " in side condition in rule number "^ - (Lib.int_to_string rule_num), - origin_function = "check_rule", - origin_structure = "define_inductive_relations"} - else check_hyp hyps + (Lib.int_to_string rule_num)) + else check_hyp hyps end | check_hyp [] = true fun check_concl tm = let val (rator, rands) = strip_comb tm in - if not (tmem rator relations) then raise HOL_ERR - {message = "must have relation as operator in "^ - "conclusion of rule "^(Lib.int_to_string rule_num), - origin_function = "check_rule", - origin_structure = "define_inductive_relations"} else - if (foldr (fn (tm, acc) => relations_in_tm tm orelse acc) - false rands) then raise HOL_ERR - {message = "found relation being defined"^ + if not (tmem rator relations) then + raise mk_HOL_ERR "define_inductive_relations" "check_rule" + ("must have relation as operator in "^ + "conclusion of rule "^(Lib.int_to_string rule_num)) + else if + foldr (fn (tm, acc) => relations_in_tm tm orelse acc) false rands + then + raise mk_HOL_ERR "define_inductive_relations" "check_rule" + ("found relation being defined"^ " in arg to "^(fst(dest_var rator))^ " in conclusion of rule number "^ - (Lib.int_to_string rule_num), - origin_function = "check_rule", - origin_structure = "define_inductive_relations"} + (Lib.int_to_string rule_num)) else true end in @@ -478,38 +464,34 @@ fun check_rule rule_num rule = (* check that the relations don't occur in rands *) if (foldr (fn (tm, acc) => relations_in_tm tm orelse acc) false rands) then - raise HOL_ERR - {message = "found relation being defined"^ - " in arg to "^(fst(dest_var rator))^ - " in hypothesis ofrule number "^ - (Lib.int_to_string rule_num), - origin_function = "check_rule", - origin_structure = "define_inductive_relations"} + raise mk_HOL_ERR "define_inductive_relations" "check_rule" + ("found relation being defined"^ + " in arg to "^(fst(dest_var rator))^ + " in hypothesis ofrule number "^ + (Lib.int_to_string rule_num)) else check_hyp hyps - else if relations_in_tm hyp1 then raise HOL_ERR - {message = "found relation being defined"^ + else if relations_in_tm hyp1 then + raise mk_HOL_ERR "define_inductive_relations" "check_rule" + ("found relation being defined"^ " in side condition in rule number "^ - (Lib.int_to_string rule_num), - origin_function = "check_rule", - origin_structure = "define_inductive_relations"} - else check_hyp hyps - end | - check_hyp [] = true + (Lib.int_to_string rule_num)) + else check_hyp hyps + end + | check_hyp [] = true fun check_concl tm = let val (rator, rands) = strip_comb tm in - if not (tmem rator relations) then raise HOL_ERR - {message = "must have relation as operator in "^ - "conclusion of rule "^(Lib.int_to_string rule_num), - origin_function = "check_rule", - origin_structure = "define_inductive_relations"} else - if (foldr (fn (tm, acc) => relations_in_tm tm orelse acc) - false rands) then raise HOL_ERR - {message = "found relation being defined"^ + if not (tmem rator relations) then + raise mk_HOL_ERR "define_inductive_relations" "check_rule" + ("must have relation as operator in "^ + "conclusion of rule "^(Lib.int_to_string rule_num)) + else if + foldr (fn (tm, acc) => relations_in_tm tm orelse acc) false rands + then + raise mk_HOL_ERR "define_inductive_relations" "check_rule" + ("found relation being defined"^ " in arg to "^(fst(dest_var rator))^ " in conclusion of rule number "^ - (Lib.int_to_string rule_num), - origin_function = "check_rule", - origin_structure = "define_inductive_relations"} + (Lib.int_to_string rule_num)) else true end in @@ -992,10 +974,9 @@ fun simp_rule sfn set vs rul th = end end; -fun bad_error ftn_name = raise HOL_ERR - {message = "this case should never happen, real problem here!", - origin_function = ftn_name, - origin_structure = "prove_inversion_theorems"} +fun bad_error ftn_name = + raise mk_HOL_ERR "prove_inversion_theorems" ftn_name + "this case should never happen, real problem here!" fun simp set sfn rul th = let val vs = fst(strip_forall (dest_neg (concl th))) @@ -1727,10 +1708,9 @@ local fun get_correct_tm ((rel, tm)::more_info) rel2 = if rel ~~ rel2 then tm else get_correct_tm more_info rel2 - | get_correct_tm [] rel2 = raise HOL_ERR - {origin_structure = "inductive_relations", - origin_function = "rule_induct", - message = "need term for relation "^(fst (dest_const rel2))} + | get_correct_tm [] rel2 = + raise mk_HOL_ERR "inductive_relations" "rule_induct" + ("need term for relation "^(fst (dest_const rel2))) in fun rule_induct induct_thm (asms, gl) = let val reltns_goals_list = map process_term (strip_conj gl) diff --git a/src/tactictoe/src/tttEval.sml b/src/tactictoe/src/tttEval.sml index f955ebe6b5..fc797a37bf 100644 --- a/src/tactictoe/src/tttEval.sml +++ b/src/tactictoe/src/tttEval.sml @@ -22,7 +22,7 @@ fun catch_err msg f x = fun catch_err_ignore msg f x = f x handle HOL_ERR {origin_structure,origin_function,source_location,message} => (print_endline - (msg ^ ":" ^ origin_structure ^ ":" ^ origin_function ^ ":" ^ locn.toShortString source_location ^ ^ ":" ^ message)) + (msg ^ ":" ^ origin_structure ^ ":" ^ origin_function ^ ":" ^ locn.toShortString source_location ^ ":" ^ message)) (* -------------------------------------------------------------------------