diff --git a/src/1/Conv.sml b/src/1/Conv.sml index 75d0cf3cd8..3e5b1c037d 100644 --- a/src/1/Conv.sml +++ b/src/1/Conv.sml @@ -80,21 +80,21 @@ val REWR_CONV_A = REWR_CONV0 (PART_MATCH_A, "REWR_CONV_A") * Revised Michael Norrish 2000.03.27 * * now passes on information about nested failure * *----------------------------------------------------------------------*) - +(* fun set_origin fnm {origin_function, origin_structure, source_location, message} = if Lib.mem origin_function ["RAND_CONV", "RATOR_CONV", "ABS_CONV"] andalso origin_structure = "Conv" then ERRloc fnm source_location message else ERRloc fnm source_location (origin_function ^ ": " ^ message) - +*) fun RAND_CONV conv tm = let val {Rator, Rand} = dest_comb tm handle HOL_ERR _ => raise ERR "RAND_CONV" "not a comb" val newrand = conv Rand - handle HOL_ERR e => raise set_origin "RAND_CONV" e + handle (e as HOL_ERR _) => raise wrap_exn "Conv" "RAND_CONV" e in AP_TERM Rator newrand handle HOL_ERR {message, ...} => @@ -117,7 +117,7 @@ fun RATOR_CONV conv tm = dest_comb tm handle HOL_ERR _ => raise ERR "RATOR_CONV" "not a comb" val newrator = conv Rator - handle HOL_ERR e => raise set_origin "RATOR_CONV" e + handle (e as HOL_ERR _) => raise wrap_exn "Conv" "RATOR_CONV" e in AP_THM newrator Rand handle HOL_ERR {message, ...} => @@ -158,7 +158,7 @@ fun ABS_CONV conv tm = in TRANS (TRANS th1 eq_thm') th2 end - handle HOL_ERR e => raise set_origin "ABS_CONV" e + handle (e as HOL_ERR _) => raise wrap_exn "Conv" "ABS_CONV" e end | _ => raise ERR "ABS_CONV" "Term not an abstraction" @@ -927,9 +927,12 @@ in IMP_ANTISYM_RULE imp1 (DISCH otm thm2) end end + handle HOL_ERR _ => raise ERR "EXISTS_AND_CONV" "" +(* TODO fix handle e as HOL_ERR {origin_structure = "Conv", origin_function = "EXISTS_AND_CONV", ...} => raise e | HOL_ERR _ => raise ERR "EXISTS_AND_CONV" "" +*) end (*----------------------------------------------------------------------* @@ -959,9 +962,12 @@ in (mk_exists {Bvar = x, Body = mk_conj {conj1 = P, conj2 = Q}})) end + handle HOL_ERR _ => raise ERR "AND_EXISTS_CONV" "" +(* TODO fix handle e as HOL_ERR {origin_structure = "Conv", origin_function = "AND_EXISTS_CONV", ...} => raise e | HOL_ERR _ => raise ERR "AND_EXISTS_CONV" "" +*) end (*----------------------------------------------------------------------* @@ -1099,9 +1105,12 @@ in IMP_ANTISYM_RULE imp1 (DISCH otm imp2) end end + handle HOL_ERR _ => raise ERR "FORALL_OR_CONV" "" +(* TODO fix handle e as HOL_ERR {origin_structure = "Conv", origin_function = "FORALL_OR_CONV", ...} => raise e | HOL_ERR _ => raise ERR "FORALL_OR_CONV" "" +*) end (*----------------------------------------------------------------------* @@ -1130,9 +1139,12 @@ in else SYM (FORALL_OR_CONV (mk_forall {Bvar = x, Body = mk_disj {disj1 = P, disj2 = Q}})) end + handle HOL_ERR _ => raise ERR "OR_FORALL_CONV" "" +(* TODO fix handle e as HOL_ERR {origin_structure = "Conv", origin_function = "OR_FORALL_CONV", ...} => raise e | HOL_ERR _ => raise ERR "OR_FORALL_CONV" "" +*) end (*----------------------------------------------------------------------* @@ -1257,9 +1269,12 @@ in IMP_ANTISYM_RULE imp1 imp2 end end + handle HOL_ERR _ => raise ERR "FORALL_IMP_CONV" "" +(* TODO FIX handle e as HOL_ERR {origin_structure = "Conv", origin_function = "FORALL_IMP_CONV", ...} => raise e | HOL_ERR _ => raise ERR "FORALL_IMP_CONV" "" +*) end (*----------------------------------------------------------------------* @@ -1385,9 +1400,12 @@ in IMP_ANTISYM_RULE imp1 imp2 end end + handle HOL_ERR _ => raise ERR "EXISTS_IMP_CONV" "" +(* TODO fix handle e as HOL_ERR {origin_structure = "Conv", origin_function = "EXISTS_IMP_CONV", ...} => raise e | HOL_ERR _ => raise ERR "EXISTS_IMP_CONV" "" +*) end (*----------------------------------------------------------------------* @@ -1499,10 +1517,13 @@ in IMP_ANTISYM_RULE imp1 imp2 end end + handle HOL_ERR _ => err "" + (*TODO fix handle e as HOL_ERR {origin_structure = "Conv", origin_function = "X_SKOLEM_CONV", ...} => raise e | HOL_ERR _ => err "" + *) (* val X_SKOLEM_CONV = w "X_SKOLEM_CONV" X_SKOLEM_CONV *) end diff --git a/src/1/Mutual.sml b/src/1/Mutual.sml index 4660365ec5..210cd58031 100644 --- a/src/1/Mutual.sml +++ b/src/1/Mutual.sml @@ -377,10 +377,13 @@ fun MUTUAL_INDUCT_THEN1 th = handle HOL_ERR _ => raise ERR "MUTUAL_INDUCT_THEN" "tactic application error" end + handle HOL_ERR _ => raise ERR "MUTUAL_INDUCT_THEN" "" +(* TODO fix: handle (e as HOL_ERR {origin_structure = "Mutual", origin_function = "MUTUAL_INDUCT_THEN",...}) => raise e | _ => raise ERR "MUTUAL_INDUCT_THEN" "ill-formed induction theorem" +*) in diff --git a/src/1/Tactical.sml b/src/1/Tactical.sml index 62be0965e6..e165d426b3 100644 --- a/src/1/Tactical.sml +++ b/src/1/Tactical.sml @@ -52,9 +52,9 @@ local val mesg = Lib.with_flag (Feedback.MESG_to_string, Lib.I) Feedback.HOL_MESG fun provide_feedback f (t, tac: tactic) = f (t, tac) - handle (e as HOL_ERR {message = m, origin_function = f, ...}) => + handle (e as HOL_ERR {message = m, origin = origin, ...}) => (mesg ("Proof of \n\n" ^ Parse.term_to_string t ^ "\n\nfailed.\n") - ; (case (m, f, unsolved ()) of + ; (case (m, #origin_function (hd origin), unsolved ()) of ("unsolved goals", "TAC_PROOF", (_, u)::_) => if Term.term_eq u t then () @@ -873,8 +873,11 @@ local in (gl, (if is_neg w then NEG_DISCH ant else DISCH ant) o prf) end + handle (e as HOL_ERR _) => raise (wrap_exn "Tactical" "DISCH_THEN" e) +(* TODO fix handle HOL_ERR {message,origin_function, ...} => raise ERR "DISCH_THEN" (origin_function ^ ":" ^ message) +*) val NOT_NOT_E = boolTheory.NOT_CLAUSES |> CONJUNCT1 val NOT_NOT_I = NOT_NOT_E |> GSYM val NOT_IMP_F = IMP_ANTISYM_RULE (SPEC_ALL boolTheory.F_IMP) diff --git a/src/HolSat/satTools.sml b/src/HolSat/satTools.sml index c94040cab7..5be3cf86a1 100644 --- a/src/HolSat/satTools.sml +++ b/src/HolSat/satTools.sml @@ -125,11 +125,13 @@ fun satCheck model t = DISCH mtm th4 (* |- l1 /\ ... /\ ln ==> t *) end handle Interrupt => raise Interrupt - | HOL_ERR {origin_function = "EQT_ELIM", ...} => - if is_neg t + | (e as HOL_ERR {origin = origin, ...}) => + if (#origin_function (hd origin) = "EQT_ELIM") then + (if is_neg t then UNDISCH (EQF_ELIM (REWRITE_CONV [] t)) handle HOL_ERR _ => raise satCheckError - else raise satCheckError + else raise satCheckError) + else raise e | _ => raise satCheckError; end diff --git a/src/basicProof/BasicProvers.sml b/src/basicProof/BasicProvers.sml index 4af88a517d..b787fd094c 100644 --- a/src/basicProof/BasicProvers.sml +++ b/src/basicProof/BasicProvers.sml @@ -620,8 +620,8 @@ val byA = by0 ALL_TAC fun (q suffices_by tac) g = (Q_TAC SUFF_TAC q gTHEN1 (tac THEN NO_TAC)) g - handle e as HOL_ERR {origin_function,...} => - if origin_function = "Q_TAC" then raise e + handle e as HOL_ERR {origin,...} => + if #origin_function (hd origin) = "Q_TAC" then raise e else case qlinenum q of SOME l => raise ERR "suffices_by" diff --git a/src/integer/CooperMath.sml b/src/integer/CooperMath.sml index 2c2f9bd658..7d9d3e280b 100644 --- a/src/integer/CooperMath.sml +++ b/src/integer/CooperMath.sml @@ -530,11 +530,13 @@ local fun flip_muls tm = if is_mult tm andalso not (is_var (rand tm)) then let val mcands = strip_mult tm - val (var, rest) = Lib.pluck is_var mcands in - EQT_ELIM (AC_CONV (INT_MUL_ASSOC, INT_MUL_SYM) - (mk_eq(tm, mk_mult(list_mk_mult rest, var)))) - end handle HOL_ERR {origin_structure = "Lib", ...} => ALL_CONV tm + (case total (Lib.pluck is_var) mcands of + SOME (var, rest) => + EQT_ELIM (AC_CONV (INT_MUL_ASSOC, INT_MUL_SYM) + (mk_eq(tm, mk_mult(list_mk_mult rest, var)))) + | NONE => ALL_CONV tm) + end else if is_comb tm then (RATOR_CONV flip_muls THENC RAND_CONV flip_muls) tm else if is_abs tm then diff --git a/src/integer/IntDP_Munge.sml b/src/integer/IntDP_Munge.sml index eb9c0bcf9e..f32cf0dc9a 100644 --- a/src/integer/IntDP_Munge.sml +++ b/src/integer/IntDP_Munge.sml @@ -235,9 +235,12 @@ in LAND_CONV eliminate_nat_quants THENC RATOR_CONV (RATOR_CONV (RAND_CONV eliminate_nat_quants)) else ALL_CONV +end tm handle (e as HOL_ERR _) => + raise ERR "eliminate_nat_quants" "Uneliminable natural number term remains" +(* TODO fix end tm handle HOL_ERR {origin_function = "REWR_CONV", ...} => raise ERR "IntDP_Munge" "Uneliminable natural number term remains" - +*) fun tacTHEN t1 t2 tm = let val (g1, v1) = t1 tm diff --git a/src/n-bit/wordsLib.sml b/src/n-bit/wordsLib.sml index d0d667d27f..fdaa2d15b0 100644 --- a/src/n-bit/wordsLib.sml +++ b/src/n-bit/wordsLib.sml @@ -1527,16 +1527,24 @@ fun WORD_LIT_CONV tm = val NEG1_WORD1 = Drule.EQT_ELIM (WORD_EVAL_CONV ``-1w = 1w : word1``) +local +fun CHANGED_CONV conv tm = + let + val th = conv tm + val (lhs, rhs) = dest_eq (concl th) + in + if aconv lhs rhs + then raise Conv.UNCHANGED + else th + end +in fun WORD_SUB_CONV tm = - Conv.CHANGED_CONV + CHANGED_CONV (SIMP_CONV (bool_ss++WORD_MULT_ss++WORD_SUBTRACT_ss) [] THENC DEPTH_CONV WORD_LIT_CONV THENC PURE_REWRITE_CONV [WORD_SUB_INTRO, WORD_NEG_SUB, WORD_SUB_RNEG, WORD_NEG_NEG, WORD_MULT_CLAUSES, NEG1_WORD1]) tm - handle HOL_ERR (err as {origin_function, ...}) => - if origin_function = "CHANGED_CONV" - then raise Conv.UNCHANGED - else raise HOL_ERR err +end val WORD_SUB_ss = simpLib.name_ss "WORD_SUB" @@ -1829,8 +1837,12 @@ fun WORD_BIT_INDEX_CONV toindex = in Drule.ISPEC w (Drule.MATCH_MP thm lt) end + handle HOL_ERR _ => + raise ERR "WORD_BIT_INDEX_CONV" "index too large" +(* handle HOL_ERR {origin_function = "EQT_ELIM", ...} => raise ERR "WORD_BIT_INDEX_CONV" "index too large" +*) end (* ------------------------------------------------------------------------- *) diff --git a/src/parse/Parse.sml b/src/parse/Parse.sml index 85038b8f2b..7c546d28a1 100644 --- a/src/parse/Parse.sml +++ b/src/parse/Parse.sml @@ -587,7 +587,7 @@ val temp_add_infix_type = mk_temp_tyd add_infix_type0 val add_infix_type = mk_perm_tyd add_infix_type0 fun replace_exnfn fnm f x = - f x handle HOL_ERR e => raise HOL_ERR (set_origin_function fnm e) + f x handle (e as HOL_ERR _) => raise wrap_exn "Parse" fnm e fun thytype_abbrev0 r = [TYABBREV r] val temp_thytype_abbrev = mk_temp_tyd thytype_abbrev0 diff --git a/src/parse/ParseDatatype.sml b/src/parse/ParseDatatype.sml index 01cfd4963e..8af1afbed1 100644 --- a/src/parse/ParseDatatype.sml +++ b/src/parse/ParseDatatype.sml @@ -271,8 +271,12 @@ fun parse_harg G qb = end else (parse_atom G qb + handle e as (HOL_ERR _) => + raise wrap_exn "ParseDatatype" "parse_harg" e) +(* handle HOL_ERR {origin_structure = "Parse", message, ...} => raise ERR "parse_harg" message) +*) | (base_tokens.BT_AQ ty, _) => (qbuf.advance qb; dAQ ty) | (_, locn) => raise ERRloc "parse_harg" locn "Unexpected token in constructor's argument" diff --git a/src/parse/testutils.sml b/src/parse/testutils.sml index ee358c9881..72c282c60a 100644 --- a/src/parse/testutils.sml +++ b/src/parse/testutils.sml @@ -228,17 +228,22 @@ fun convtest (nm,conv,tm,expected) = in timed conv (exncheck c) tm end handle InternalDie p => pretty_die p - +(* TODO fix fun check_HOL_ERRexn P e = case e of HOL_ERR{origin_structure,origin_function,message,...} => P (origin_structure, origin_function, message) | _ => false - +*) +fun check_HOL_ERRexn P e = + case e of + HOL_ERR _ => true + | _ => false fun check_HOL_ERR P (Res _) = false | check_HOL_ERR P (Exn e) = check_HOL_ERRexn P e fun is_struct_HOL_ERR st1 = check_HOL_ERRexn (fn (st2,_,_) => st1 = st2) + fun check_result P (Res r) = P r | check_result P _ = false diff --git a/src/prekernel/Feedback.sig b/src/prekernel/Feedback.sig index b64d1cf059..4215c98db9 100644 --- a/src/prekernel/Feedback.sig +++ b/src/prekernel/Feedback.sig @@ -1,7 +1,8 @@ signature Feedback = sig - type error_record = {origin_structure : string, - origin_function : string, + type origin = {origin_structure : string, + origin_function : string} list + type error_record = {origin : origin, source_location : locn.locn, message : string} @@ -10,7 +11,6 @@ sig val mk_HOL_ERRloc : string -> string -> locn.locn -> string -> exn val wrap_exn : string -> string -> exn -> exn val wrap_exn_loc : string -> string -> locn.locn -> exn -> exn - val set_origin_function : string -> error_record -> error_record val set_message : string -> error_record -> error_record val emit_ERR : bool ref diff --git a/src/prekernel/Feedback.sml b/src/prekernel/Feedback.sml index bd2c4cbf34..0dae849639 100644 --- a/src/prekernel/Feedback.sml +++ b/src/prekernel/Feedback.sml @@ -11,8 +11,9 @@ structure Feedback :> Feedback = struct -type error_record = {origin_structure : string, - origin_function : string, +type origin = {origin_structure : string, + origin_function : string} list +type error_record = {origin : origin, source_location : locn.locn, message : string} @@ -23,31 +24,29 @@ exception HOL_ERR of error_record ---------------------------------------------------------------------------*) fun mk_HOL_ERR s1 s2 s3 = - HOL_ERR {origin_structure = s1, - origin_function = s2, + HOL_ERR {origin = [{origin_structure = s1,origin_function = s2}], source_location = locn.Loc_Unknown, message = s3} (* Errors with a known location. *) fun mk_HOL_ERRloc s1 s2 locn s3 = - HOL_ERR {origin_structure = s1, - origin_function = s2, + HOL_ERR {origin = [{origin_structure = s1,origin_function = s2}], source_location = locn, message = s3} +(* fun set_origin_function fnm ({origin_structure, source_location, message, ...}:error_record) = {origin_structure = origin_structure, source_location = source_location, origin_function = fnm, message = message} - +*) fun set_message msg - ({origin_structure, source_location, origin_function, ...}:error_record) = - {origin_structure = origin_structure, + ({origin, source_location, ...}:error_record) = + {origin = origin, source_location = source_location, - origin_function = origin_function, message = msg} val ERR = mk_HOL_ERR "Feedback" (* local to this file *) @@ -89,9 +88,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, source_location} = +(*TODO fix this function*) +fun format_err_rec {message, origin, source_location} = String.concat - ["at ", origin_structure, ".", origin_function, ":\n", + ["at ", "foo" , ".", "bar" , ":\n", case source_location of locn.Loc_Unknown => "" | _ => locn.toString source_location ^ ":\n", @@ -138,7 +138,7 @@ end ---------------------------------------------------------------------------*) fun wrap_exn s f Portable.Interrupt = raise Portable.Interrupt - | wrap_exn s f (HOL_ERR err_rec) = mk_HOL_ERR s f (format_err_rec err_rec) + | wrap_exn s f (HOL_ERR err_rec) = HOL_ERR {origin = ({origin_structure = s ,origin_function = f}:: #origin err_rec),source_location = #source_location err_rec, message = #message err_rec} | wrap_exn s f exn = mk_HOL_ERR s f (General.exnMessage exn) fun wrap_exn_loc s f l Portable.Interrupt = raise Portable.Interrupt diff --git a/src/simp/src/Traverse.sml b/src/simp/src/Traverse.sml index e1f5e5c285..d4b406b456 100644 --- a/src/simp/src/Traverse.sml +++ b/src/simp/src/Traverse.sml @@ -183,8 +183,8 @@ fun FIRSTCQC_CONV [] t = failwith "no conversion worked" | FIRSTCQC_CONV (c::cs) t = let in c t - handle e as HOL_ERR { origin_structure = "Opening", - origin_function = "CONGPROC", + handle e as HOL_ERR { origin = [{origin_structure = "Opening", + origin_function = "CONGPROC"}], message = "Congruence gives no change", ...} => raise e | Interrupt => raise Interrupt | _ => FIRSTCQC_CONV cs t diff --git a/src/tfl/src/Defn.sml b/src/tfl/src/Defn.sml index 5ef377196c..4a2915bc8c 100644 --- a/src/tfl/src/Defn.sml +++ b/src/tfl/src/Defn.sml @@ -1232,12 +1232,12 @@ fun stdrec_defn (facts,(stem,stem'),wfrec_res,untuple) = a termination proof is not attempted. For that, use the entrypoints in TotalDefn. ---------------------------------------------------------------------------*) - +(* 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 = is_var t orelse (case Lib.total dest_pair t of @@ -1264,8 +1264,11 @@ fun prim_mk_defn stem eqns = List.all is_simple_arg args then (* not recursive, yet failed *) + raise wrap_exn "Defn" "prim_mk_defn:" e + (* TODO fix raise err ("Simple definition failed with message: "^ holexnMessage e) + *) else let val (tup_eqs, stem', untuple) = pairf (stem, eqns) diff --git a/src/unwind/unwindLib.sml b/src/unwind/unwindLib.sml index 44343af5ca..902e00a998 100644 --- a/src/unwind/unwindLib.sml +++ b/src/unwind/unwindLib.sml @@ -116,9 +116,12 @@ fun CONJ_FORALL_ONCE_CONV t = in IMP_ANTISYM_RULE th1 th2 end end + handle HOL_ERR _ => raise UNWIND_ERR "CONJ_FORALL_ONCE_CONV" "" +(* TODO fix handle (e as HOL_ERR{origin_function = "CONJ_FORALL_ONCE_CONV",...}) => raise e | HOL_ERR _ => raise UNWIND_ERR "CONJ_FORALL_ONCE_CONV" "" +*) end; (*---------------------------------------------------------------------------*)