fix tests

HOL-Theorem-Prover · Nov 15, 2024 · a3c0174 · a3c0174
1 parent 7db7df9
commit a3c0174
Show file tree

Hide file tree

Showing 5 changed files with 67 additions and 86 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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))
 
 
 (* -------------------------------------------------------------------------