From 17b79b72c379912b5e44bbc80e46519da4d062d4 Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Sun, 14 Sep 2025 02:13:01 -0500 Subject: [PATCH 01/13] make HOL_ERR wrap a datatype rather than a record --- src/prekernel/Feedback.sig | 26 +++++--- src/prekernel/Feedback.sml | 124 +++++++++++++++++++++++-------------- tools-poly/prelude.ML | 3 +- 3 files changed, 96 insertions(+), 57 deletions(-) diff --git a/src/prekernel/Feedback.sig b/src/prekernel/Feedback.sig index b64d1cf059..7bac38f634 100644 --- a/src/prekernel/Feedback.sig +++ b/src/prekernel/Feedback.sig @@ -1,17 +1,25 @@ signature Feedback = sig - type error_record = {origin_structure : string, - origin_function : string, - source_location : locn.locn, - message : string} + datatype hol_error = HOL_ERROR of + {origin_structure : string, + origin_function : string, + source_location : locn.locn, + message : string} + + val structure_of : hol_error -> string + val function_of : hol_error -> string + val location_of : hol_error -> locn.locn + val message_of : hol_error -> string + val set_message : string -> hol_error -> hol_error + val set_origin_function : string -> hol_error -> hol_error + val pp_hol_error : hol_error -> HOLPP.pretty + + exception HOL_ERR of hol_error - exception HOL_ERR of error_record val mk_HOL_ERR : string -> string -> string -> exn 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 @@ -24,14 +32,14 @@ sig (* heeds emit_ERR, uses ERR_outstream *) val output_ERR : string -> unit - val format_ERR : error_record -> string + val format_ERR : hol_error -> string val format_MESG : string -> string val format_WARNING : string -> string -> string -> string val quiet_warnings : ('a -> 'b) -> ('a -> 'b) val quiet_messages : ('a -> 'b) -> ('a -> 'b) - val ERR_to_string : (error_record -> string) ref + val ERR_to_string : (hol_error -> string) ref val MESG_to_string : (string -> string) ref val WARNING_to_string : (string -> string -> string -> string) ref val exn_to_string : exn -> string diff --git a/src/prekernel/Feedback.sml b/src/prekernel/Feedback.sml index bd2c4cbf34..9cc7181cd0 100644 --- a/src/prekernel/Feedback.sml +++ b/src/prekernel/Feedback.sml @@ -11,44 +11,83 @@ structure Feedback :> Feedback = struct -type error_record = {origin_structure : string, - origin_function : string, - source_location : locn.locn, - message : string} +local open HOLPP in end + +datatype hol_error = + HOL_ERROR of + {origin_structure : string, + origin_function : string, + source_location : locn.locn, + message : string} + +(*--------------------------------------------------------------------------- + Projections + ---------------------------------------------------------------------------*) + +fun structure_of (HOL_ERROR {origin_structure,...}) = origin_structure +fun function_of (HOL_ERROR {origin_function,...}) = origin_function +fun location_of (HOL_ERROR {source_location,...}) = source_location +fun message_of (HOL_ERROR {message,...}) = message + +exception HOL_ERR of hol_error + +fun format_err_recd {message, origin_function, origin_structure, source_location} = + String.concat + ["at ", origin_structure, ".", origin_function, ":\n", + case source_location of + locn.Loc_Unknown => "" + | _ => locn.toString source_location ^ ":\n", + message] -exception HOL_ERR of error_record +fun format_hol_error(HOL_ERROR recd) = format_err_recd recd + +fun pp_hol_error (HOL_ERROR recd) = + let open HOLPP + val {origin_structure, origin_function, source_location, message} = recd + in block CONSISTENT 0 + [add_string (origin_structure^"."^origin_function),add_string ":",NL,NL, + add_string message, NL,NL, add_string (locn.toString source_location)] + end (*--------------------------------------------------------------------------- Curried version of HOL_ERR; can be more comfortable to use. ---------------------------------------------------------------------------*) fun mk_HOL_ERR s1 s2 s3 = - HOL_ERR {origin_structure = s1, - origin_function = s2, - source_location = locn.Loc_Unknown, - message = s3} + HOL_ERR + (HOL_ERROR + {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, - 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, - source_location = source_location, - origin_function = origin_function, - message = msg} + HOL_ERR + (HOL_ERROR + {origin_structure = s1, + origin_function = s2, + source_location = locn, + message = s3}) + +fun set_origin_function fnm (HOL_ERROR recd) = + let val {origin_structure, source_location, message, ...} = recd + in HOL_ERROR + {origin_structure = origin_structure, + source_location = source_location, + origin_function = fnm, + message = message} + end + +fun set_message msg (HOL_ERROR recd) = + let val{origin_structure, source_location, origin_function, ...} = recd + in HOL_ERROR + {origin_structure = origin_structure, + source_location = source_location, + origin_function = origin_function, + message = msg} + end val ERR = mk_HOL_ERR "Feedback" (* local to this file *) @@ -89,16 +128,8 @@ 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} = - String.concat - ["at ", origin_structure, ".", origin_function, ":\n", - case source_location of - locn.Loc_Unknown => "" - | _ => locn.toString source_location ^ ":\n", - message] - -fun format_ERR err_rec = - String.concat ["\nException raised ", format_err_rec err_rec, "\n"] +fun format_ERR (HOL_ERROR recd) = + String.concat ["\nException raised ", format_err_recd recd, "\n"] fun format_MESG s = String.concat ["<>\n"] @@ -117,7 +148,7 @@ fun output_ERR s = if !emit_ERR then !ERR_outstream s else () that the exception is an Interrupt, we raise it. ---------------------------------------------------------------------------*) -fun exn_to_string (HOL_ERR sss) = !ERR_to_string sss +fun exn_to_string (HOL_ERR herr) = !ERR_to_string herr | exn_to_string Portable.Interrupt = raise Portable.Interrupt | exn_to_string e = General.exnMessage e @@ -138,12 +169,13 @@ 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 (HOL_ERROR recd)) = + mk_HOL_ERR s f (format_err_recd recd) | 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 - | wrap_exn_loc s f l (HOL_ERR err_rec) = - mk_HOL_ERRloc s f l (format_err_rec err_rec) + | wrap_exn_loc s f l (HOL_ERR (HOL_ERROR recd)) = + mk_HOL_ERRloc s f l (format_err_recd recd) | wrap_exn_loc s f l exn = mk_HOL_ERRloc s f l (General.exnMessage exn) fun HOL_MESG s = @@ -172,8 +204,6 @@ fun HOL_WARNINGloc s1 s2 locn s3 = * Traces, numeric flags; the higher setting, the more verbose the output. * *---------------------------------------------------------------------------*) -local open HOLPP in end - datatype tracefns = TRFP of {get: unit -> int, set: int -> unit} fun trfp_set (TRFP {set, ...}) = set fun trfp_get (TRFP {get, ...}) = get () @@ -223,7 +253,7 @@ fun register_trace0 fnm (nm, r, max) = then raise ERR fnm "Can't have trace values less than zero." else let - val trfns as TRFP rcd = ref2trfp r + val trfns as TRFP recd = ref2trfp r in case Binarymap.peek (!trace_map, nm) of NONE => () @@ -232,7 +262,7 @@ fun register_trace0 fnm (nm, r, max) = trace_map := Binarymap.insert (!trace_map, nm, TR {value = trfns, default = !r, aliases = [], maximum = max}); - rcd + recd end val register_trace = ignore o register_trace0 "register_trace" @@ -254,9 +284,9 @@ fun register_alias_trace {original, alias} = val aliases' = if List.exists (fn s => s = alias) aliases then aliases else alias::aliases - val rcd = {aliases = aliases', maximum = maximum, default = default, + val recd = {aliases = aliases', maximum = maximum, default = default, value = value} - val record_alias = Binarymap.insert(!trace_map, original, TR rcd) + val record_alias = Binarymap.insert(!trace_map, original, TR recd) val mk_alias = Binarymap.insert(record_alias, alias, ALIAS original) in case Binarymap.peek (record_alias, alias) of diff --git a/tools-poly/prelude.ML b/tools-poly/prelude.ML index 7733424bb3..6a21ea6823 100644 --- a/tools-poly/prelude.ML +++ b/tools-poly/prelude.ML @@ -119,7 +119,8 @@ in PolyML.addPrettyPrinter (pp2polypp proofManagerLib.pp_proof); PolyML.addPrettyPrinter (pp2polypp proofManagerLib.pp_proofs); PolyML.addPrettyPrinter (pp2polypp type_grammar.prettyprint_grammar); - PolyML.addPrettyPrinter (pp2polypp Feedback.pp_trace_elt) + PolyML.addPrettyPrinter (pp2polypp Feedback.pp_trace_elt); + PolyML.addPrettyPrinter (pp2polypp Feedback.pp_hol_error) end val _ = PolyML.use (OS.Path.concat(HOLDIR, "tools-poly/holinteractive.ML")); From 3cc01f08cb13eb31219fdc32987f1614d1541515 Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Sun, 14 Sep 2025 02:15:52 -0500 Subject: [PATCH 02/13] remove record-oriented HOL_ERR handling --- examples/arm/v7/arm_parserLib.sml | 260 +++++++++--------- examples/arm/v7/arm_random_testingLib.sml | 2 +- .../l3-machine-code/arm/step/arm_stepLib.sml | 29 +- examples/l3-machine-code/common/Import.sml | 17 +- examples/l3-machine-code/common/stateLib.sml | 42 ++- examples/l3-machine-code/common/utilsLib.sml | 8 +- .../l3-machine-code/m0/step/m0_stepLib.sml | 58 ++-- .../mips/prog/mips_progLib.sml | 4 +- .../mips/step/mips_stepLib.sml | 8 +- .../riscv/step/riscv_stepLib.sml | 6 +- .../l3-machine-code/x64/step/x64_stepLib.sml | 6 +- src/1/Conv.sml | 95 ++++--- src/1/Mutual.sml | 12 +- src/1/Tactical.sml | 42 +-- src/HolSat/satTools.sml | 14 +- src/HolSmt/HolSmtLib.sml | 4 +- src/HolSmt/selftest.sml | 13 +- src/IndDef/selftest.sml | 12 +- src/TeX/holindex.sml | 2 +- src/basicProof/BasicProvers.sml | 7 +- src/boss/selftest.sml | 9 +- src/boss/theory_tests/bylocnScript.sml | 6 +- src/coretypes/PairedLambda.sml | 2 +- src/finite_maps/alist_treeLib.sml | 2 +- src/floating-point/binary_ieeeLib.sml | 10 +- src/integer/CooperMath.sml | 5 +- src/integer/IntDP_Munge.sml | 8 +- src/integer/selftest.sml | 8 +- src/list/src/listSyntax.sml | 3 +- src/metis/metisTools.sml | 6 +- src/n-bit/bitstringLib.sml | 12 +- src/n-bit/selftest.sml | 4 +- src/n-bit/wordsLib.sml | 12 +- .../cv_compute/automation/cv_transLib.sml | 2 +- src/parse/ParseDatatype.sml | 6 +- src/parse/testutils.sml | 2 +- src/postkernel/HolKernel.sml | 4 +- src/res_quan/src/Cond_rewrite.sml | 31 ++- src/res_quan/src/res_quanLib.sml | 8 +- src/simp/src/Traverse.sml | 11 +- src/tactictoe/src/tttEval.sml | 21 +- src/tfl/src/Defn.sml | 17 +- src/tfl/src/selftest.sml | 6 +- src/unwind/unwindLib.sml | 7 +- 44 files changed, 474 insertions(+), 369 deletions(-) diff --git a/examples/arm/v7/arm_parserLib.sml b/examples/arm/v7/arm_parserLib.sml index 686815dea8..1b34876481 100644 --- a/examples/arm/v7/arm_parserLib.sml +++ b/examples/arm/v7/arm_parserLib.sml @@ -1246,28 +1246,28 @@ fun int_one_comp tm = fun mode1_immediate1 thumb m i = if thumb then (dp_opcode m,int_to_thumb2_mode1_immediate i) - handle HOL_ERR {message,origin_function,...} => + handle HOL_ERR herr => (dp_opcode (swap_opcode m),int_to_thumb2_mode1_immediate (int_one_comp i)) - handle HOL_ERR _ => raise ERR origin_function message + handle HOL_ERR _ => raise ERR (function_of herr) (message_of herr) else (dp_opcode m,int_to_mode1_immediate i) - handle HOL_ERR {message,origin_function,...} => + handle HOL_ERR herr => (dp_opcode (swap_opcode m),int_to_mode1_immediate (int_one_comp i)) - handle HOL_ERR _ => raise ERR origin_function message; + handle HOL_ERR _ => raise ERR (function_of herr) (message_of herr); fun mode1_immediate2 thumb m i = if thumb then (dp_opcode m,int_to_thumb2_mode1_immediate i) - handle HOL_ERR {message,origin_function,...} => + handle HOL_ERR herr => (dp_opcode (swap_opcode m), int_to_thumb2_mode1_immediate (intSyntax.mk_negated i)) - handle HOL_ERR _ => raise ERR origin_function message + handle HOL_ERR _ => raise ERR (function_of herr) (message_of herr) else (dp_opcode m,int_to_mode1_immediate i) - handle HOL_ERR {message,origin_function,...} => + handle HOL_ERR herr => (dp_opcode (swap_opcode m), int_to_mode1_immediate (intSyntax.mk_negated i)) - handle HOL_ERR _ => raise ERR origin_function message; + handle HOL_ERR _ => raise ERR (function_of herr) (message_of herr) fun mode1_register rm = mk_Mode1_register (mk_word5 0,mk_word2 0,rm); @@ -1329,8 +1329,8 @@ val arm_parse_mode1_shift : term -> term M = assertT (not shift32 orelse mem s [LSR_shift,ASR_shift]) ("arm_parse_mode1_shift", "cannot shift by 32") (return (mk_Mode1_register (imm5,stype,rm))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode1_shift", message)) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode1_shift", message_of herr)) (fn _ => arm_parse_register >>= (fn rs => return (mk_Mode1_register_shifted_register (rs,stype,rm)))) @@ -1373,14 +1373,14 @@ fun add_sub_literal m (rd,i) = assertT_thumb "add_sub_literal" q narrow_okay wide_okay (return (pick_enc true narrow_okay, mk_Add_Sub (mk_bool add,mk_word4 15,rd,imm12))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_add_sub", message)) + end handle HOL_ERR herr => + other_errorT ("arm_parse_add_sub", message_of herr)) else let val (opc,imm12) = mode1_immediate2 false m i in return (Encoding_ARM_tm, mk_Add_Sub (mk_bool (opc ~~ mk_word4 4),mk_word4 15,rd,imm12)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_add_sub", message)); + end handle HOL_ERR herr => + other_errorT ("arm_parse_add_sub", message_of herr)); fun narrow_okay_imm m i (rd,rn) = let val v = sint_of_term i handle HOL_ERR _ => 1024 in @@ -1445,8 +1445,8 @@ fun data_processing_immediate m (rd,rn,i) = (return (enc, mk_Data_Processing (opc,sflag,rn,rd,mk_Mode1_immediate imm12))) - end handle HOL_ERR {message,...} => - other_errorT ("data_processing_immediate", message))) + end handle HOL_ERR herr => + other_errorT ("data_processing_immediate", message_of herr))) else assertT (m <> ORN) ("data_processing_immediate", "not a valid ARM instruction") @@ -1477,8 +1477,8 @@ fun data_processing_register m (rd,rn,rm,mode1) = assertT_thumb "data_processing_register" q narrow_okay wide_okay (return (pick_enc true narrow_okay, mk_Data_Processing (dp_opcode m,sflag,rn,rd,mode1))) - end handle HOL_ERR {message,...} => - other_errorT ("data_processing_register", message))))) + end handle HOL_ERR herr => + other_errorT ("data_processing_register", message_of herr))))) else assertT (m <> ORN) ("data_processing_immediate", "not a valid ARM instruction") @@ -1562,8 +1562,8 @@ fun move_test_immediate m (rdn,i) = assertT_thumb "move_test_immediate" q narrow_okay true (return (enc, mk_Data_Processing (opc,sflag,rn,rd,mk_Mode1_immediate imm12))) - end handle HOL_ERR {message,...} => - other_errorT ("data_processing_immediate", message))) + end handle HOL_ERR herr => + other_errorT ("data_processing_immediate", message_of herr))) else let val (opc,imm12) = mode1_immediate2 false m i val r0 = mk_word4 0 @@ -1596,8 +1596,8 @@ fun move_test_reg m (rdn,rm,mode1) = assertT_thumb "data_processing_register" q narrow_okay wide_okay (return (pick_enc true narrow_okay, mk_Data_Processing (dp_opcode m,sflag,rn,rd,mode1))) - end handle HOL_ERR {message,...} => - other_errorT ("data_processing_register", message))))) + end handle HOL_ERR herr => + other_errorT ("data_processing_register", message_of herr))))) else let val r0 = mk_word4 0 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r0) else (r0,rdn) @@ -1640,7 +1640,7 @@ in (return (pick_enc thumb narrow_okay, mk_Data_Processing (dp_opcode MOV,sflag,rn,rd, mk_Mode1_register (imm5,shift_type m,rm))))) -end handle HOL_ERR {message,...} => other_errorT ("shift_immediate", message); +end handle HOL_ERR herr => other_errorT ("shift_immediate", message_of herr); fun shift_register m thumb q InITBlock sflag (rd,rn,rm) = let val narrow_okay = q <> Wide andalso rd ~~ rn andalso @@ -1652,7 +1652,7 @@ in (return (pick_enc thumb narrow_okay, mk_Data_Processing (dp_opcode MOV,sflag,rn',rd, mk_Mode1_register_shifted_register (rm,shift_type m,rn)))) -end handle HOL_ERR {message,...} => other_errorT ("shift_register", message); +end handle HOL_ERR herr => other_errorT ("shift_register", message_of herr); val arm_parse_mov_shift : instruction_mnemonic -> (term * term) M = fn m => @@ -1700,8 +1700,8 @@ val arm_parse_mov_halfword : term -> (term * term) M = arm_parse_constant >>= (fn i => let val imm16 = uint_to_word ``:16`` i in return (enc,mk_Move_Halfword (high,rd,imm16)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mov_halfword", message))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_mov_halfword", message_of herr))))); val arm_parse_addw_subw : term -> (term * term) M = fn add => @@ -1720,8 +1720,8 @@ val arm_parse_addw_subw : term -> (term * term) M = val imm12 = uint_to_word ``:12`` i in return (Encoding_Thumb2_tm, mk_Add_Sub (add,rn,rd,imm12)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_addw_subw", message))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_addw_subw", message_of herr))))); val arm_parse_adr : (term * term) M = arm_parse_register >>= (fn rd => @@ -1751,8 +1751,8 @@ val arm_parse_adr : (term * term) M = else other_errorT ("arm_parse_adr", "bad register, unaligned or offset beyond permitted range") - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_adr", message)) + end handle HOL_ERR herr => + other_errorT ("arm_parse_adr", message_of herr)) else let open intSyntax val offset = eval (mk_minus(i, ``8i``)) @@ -1761,8 +1761,8 @@ val arm_parse_adr : (term * term) M = return (Encoding_ARM_tm, mk_Add_Sub (mk_bool (not (is_negated offset)),mk_word4 15,rd, int_to_mode1_immediate absoffset)) - end handle HOL_ERR {message, ...} => - other_errorT ("arm_parse_adr", message)))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_adr", message_of herr)))); (* ------------------------------------------------------------------------- *) @@ -1793,8 +1793,8 @@ val arm_parse_branch_target : (term * term) M = (assertT_thumb "arm_parse_branch_target" q narrow_okay wide_okay (return (pick_enc true narrow_okay, mk_Branch_Target (offset_to_imm24 (offset div 2))))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_branch_target", message)) + end handle HOL_ERR herr => + other_errorT ("arm_parse_branch_target", message_of herr)) else let val offset = sint_of_term i - 8 in assertT (offset mod 4 = 0) @@ -1803,8 +1803,8 @@ val arm_parse_branch_target : (term * term) M = ("arm_parse_branch_target", "offset beyond permitted range") (return (Encoding_ARM_tm, mk_Branch_Target (offset_to_imm24 (offset div 4))))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_branch_target", message)))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_branch_target", message_of herr)))); val arm_parse_branch_link : (term * term) M = arm_parse_branch_offset >>= (fn i => @@ -1831,8 +1831,8 @@ val arm_parse_branch_link : (term * term) M = (return (Encoding_Thumb2_tm, mk_Branch_Link_Exchange_Immediate (H,F,offset_to_imm24 (offset div 4))))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_branch_link", message)))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_branch_link", message_of herr)))) else if is_var i then return (Encoding_ARM_tm, @@ -1847,8 +1847,8 @@ val arm_parse_branch_link : (term * term) M = (return (Encoding_ARM_tm, mk_Branch_Link_Exchange_Immediate (F,T,offset_to_imm24 (offset div 4))))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_branch_link", message))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_branch_link", message_of herr))); val arm_parse_branch_link_exchange : (term * term) M = need_v5 "arm_parse_branch_link_exchange" @@ -1889,8 +1889,8 @@ val arm_parse_branch_link_exchange : (term * term) M = (return (Encoding_Thumb2_tm, mk_Branch_Link_Exchange_Immediate (F,T,offset_to_imm24 (offset div 4))))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_branch_link_exchange", message)))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_branch_link_exchange", message_of herr)))) else read_cond >>= (fn cond => assertT (is_AL cond) @@ -1913,9 +1913,9 @@ val arm_parse_branch_link_exchange : (term * term) M = (return (Encoding_ARM_tm, mk_Branch_Link_Exchange_Immediate (H,F,offset_to_imm24 (offset div 4))))) - end handle HOL_ERR {message,...} => + end handle HOL_ERR herr => other_errorT - ("arm_parse_branch_link_exchange", message)))))))); + ("arm_parse_branch_link_exchange", message_of herr)))))))); val arm_parse_bx : (term * term) M = thumb_or_arm_okay (fn enc => @@ -1958,8 +1958,8 @@ val arm_parse_cbz_cbnz : term -> (term * term) M = mk_Compare_Branch (nonzero, mk_word6 (Int.abs (offset div 2)), mk_word3 (uint_of_word rn))))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_cbz_cbnz", message))))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_cbz_cbnz", message_of herr))))))); val arm_parse_clz : (term * term) M = need_v5 "arm_parse_clz" @@ -2099,8 +2099,8 @@ val arm_parse_tbh : (term * term) M = (return (Encoding_Thumb2_tm,mk_Table_Branch_Byte (rn,T,rm)))) else syntax_errorT ("#1","#" ^ term_to_string i) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_tbh", message))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_tbh", message_of herr))))); val arm_parse_mul : (term * term) M = arm_parse_register >>= (fn rd => @@ -2321,8 +2321,8 @@ val arm_parse_pkh : term -> (term * term) M = uint_to_word ``:5`` i in return (enc,mk_Pack_Halfword (rn,rd,imm5,tbform,rm)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_pkh", message))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_pkh", message_of herr))) (fn _ => if is_T tbform then return (enc,mk_Pack_Halfword (rm,rd,mk_word5 0,F,rn)) @@ -2351,8 +2351,8 @@ val arm_parse_mode2_shift : bool -> qualifier -> term -> term M = assertT (0 <= v andalso v <= max) ("arm_parse_mode2_shift", "shift out of range") (return (mk_Mode2_register (imm5, stype, rm))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode2_shift", message))))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode2_shift", message_of herr))))) (fn _ => return (mk_Mode2_register (mk_word5 0, shift_to_word2 LSL_shift, rm))); @@ -2423,8 +2423,8 @@ val arm_parse_mode2_offset : (if ld then mk_Load else mk_Store) (mk_bool indx,u,byte,w,unpriv,rn,rt, mk_Mode2_immediate imm12))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode2_offset", message))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode2_offset", message_of herr))) (fn _ => arm_parse_plus_minus >>= (fn pos => arm_parse_register >>= (fn rm => @@ -2504,8 +2504,8 @@ val arm_parse_mode2 : bool -> term -> (term * term) M = (pick_enc thumb narrow_okay, mk_Load (T,mk_bool (0 <= v andalso not (i ~~ ``-0i``)), byte,F,F,mk_word4 15,rt,mode2))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode2", message)) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode2", message_of herr)) end)))) >>= (fn result => read_OutsideOrLastInITBlock >>= (fn OutsideOrLastInITBlock => assertT (not (is_PC rt) orelse OutsideOrLastInITBlock) @@ -2536,8 +2536,8 @@ val arm_parse_mode2_unpriv : bool -> term -> (term * term) M = mk_Load (T,T,byte,F,T,rn,rt,mode2) else mk_Store (T,T,byte,F,T,rn,rt,mode2))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode2_unpriv", message)))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode2_unpriv", message_of herr)))) (fn _ => arm_parse_rsquare >>- tryT arm_parse_comma @@ -2565,8 +2565,8 @@ val arm_parse_mode3_shift : bool -> qualifier -> term -> term M = arm_parse_constant >>= (fn i => let val imm2 = uint_to_word ``:2`` i in return (mk_Mode3_register (imm2, rm)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode3_shift", message)))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode3_shift", message_of herr)))) (fn _ => return (mode3_register rm)); val arm_parse_mode3_offset : @@ -2618,8 +2618,8 @@ val arm_parse_mode3_offset : | NONE => mk_Store_Halfword (mk_bool indx,u,w,unpriv,rn,rt, mk_Mode3_immediate imm12))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode3_offset", message))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode3_offset", message_of herr))) (fn _ => arm_parse_plus_minus >>= (fn pos => arm_parse_register >>= (fn rm => @@ -2714,8 +2714,8 @@ val arm_parse_mode3 : (term * term) option -> (term * term) M = mk_Load_Halfword (T, mk_bool (0 <= v andalso not (i ~~ ``-0i``)),F, signed,half,F,mk_word4 15,rt,mode3))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode3", message) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode3", message_of herr) end)))))); val arm_parse_mode3_unpriv : (term * term) option -> (term * term) M = @@ -2743,8 +2743,8 @@ val arm_parse_mode3_unpriv : (term * term) option -> (term * term) M = mk_Load_Halfword (T,T,F,signed,half,T,rn,rt,mode3) | NONE => mk_Store_Halfword (T,T,F,T,rn,rt,mode3))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode3_unpriv", message)))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode3_unpriv", message_of herr)))) (fn _ => arm_parse_rsquare >>- tryT arm_parse_comma @@ -2765,8 +2765,8 @@ val arm_parse_mode3_unpriv : (term * term) option -> (term * term) M = (return (mk_bool (0 <= v andalso not (i ~~ ``-0i``)), mk_Mode3_immediate (mk_word12 (Int.abs v)))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode3_unpriv", message))))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode3_unpriv", message_of herr))))) (fn _ => return (T,mk_Mode3_immediate (mk_word12 0))) >>= (fn (add,tm) => let val thumb = enc ~~ Encoding_Thumb2_tm @@ -2803,8 +2803,8 @@ val arm_parse_mode3_dual_offset : bool -> (term * term) M = "offset beyond permitted range (-255 to +255)") (return (mk_bool (0 <= offset andalso not (i ~~ ``-0i``)), mk_Mode3_immediate (mk_word12 (Int.abs offset)))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode3_dual_offset", message)) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode3_dual_offset", message_of herr)) (fn _ => assertT (not thumb) ("arm_parse_mode3_dual_offset", "expecting a constant") @@ -2880,8 +2880,8 @@ val arm_parse_mode3_dual : bool -> (term * term) M = mk_Load_Dual (T,mk_bool (0 <= v andalso not (i ~~ ``-0i``)), F,mk_word4 15,rt,rt2,mode3))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode3_dual", message))))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode3_dual", message_of herr))))) end)))); (* ------------------------------------------------------------------------- *) @@ -2906,8 +2906,8 @@ val arm_parse_ldrex : (term * term) M = ("arm_parse_ldrex", "offset unaligned or out of range") (return (enc, mk_Load_Exclusive (rn,rt,mk_word8 (Int.abs (v div 4))))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_ldrex", message))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_ldrex", message_of herr))) (fn _ => arm_parse_rsquare >>- return (enc, mk_Load_Exclusive (rn,rt,mk_word8 0))))))); @@ -2935,8 +2935,8 @@ val arm_parse_strex : (term * term) M = (return (enc, mk_Store_Exclusive (rn,rd,rt,mk_word8 (Int.abs (v div 4))))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_strex", message))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_strex", message_of herr))) (fn _ => arm_parse_rsquare >>- return (enc, mk_Store_Exclusive (rn,rd,rt,mk_word8 0)))))))); @@ -3266,8 +3266,8 @@ val arm_parse_pld_pli : bool option -> (term * term) M = (mk_bool (0 <= v andalso not (i ~~ ``-0i``)), rn,mode2))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_pld_pli", message)) + end handle HOL_ERR herr => + other_errorT ("arm_parse_pld_pli", message_of herr)) (fn _ => let val thumb = enc ~~ Encoding_Thumb2_tm in arm_parse_plus_minus >>= (fn pos => @@ -3327,8 +3327,8 @@ val arm_parse_pld_pli : bool option -> (term * term) M = (up,mk_bool wide,mk_word4 15,mode2) | NONE => mk_Preload_Instruction (up,mk_word4 15,mode2))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mode3", message)))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_mode3", message_of herr)))))); (* ------------------------------------------------------------------------- *) @@ -3367,13 +3367,13 @@ val arm_parse_ssat_usat : bool -> (term * term) M = (return (enc, mk_Saturate (mk_bool unsigned, mk_word5 sat_imm,rd,imm5,sh,rn))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_ssat_usat",message))))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_ssat_usat",message_of herr))))) (fn _ => return (enc, mk_Saturate (mk_bool unsigned,mk_word5 sat_imm,rd,mk_word5 0,F,rn))))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_ssat_usat", message))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_ssat_usat", message_of herr))))); val arm_parse_ssat16_usat16 : bool -> (term * term) M = fn unsigned => @@ -3392,8 +3392,8 @@ val arm_parse_ssat16_usat16 : bool -> (term * term) M = return (enc,mk_Saturate_16 (mk_bool unsigned,mk_word4 sat_imm,rd,rn)))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_ssat16_usat16", message))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_ssat16_usat16", message_of herr))))); val arm_parse_ror248 : term M = arm_parse_string "ror" >>- @@ -3405,8 +3405,8 @@ val arm_parse_ror248 : term M = | 24 => return (mk_word2 3) | _ => other_errorT ("arm_parse_ror248", "shift must be 0, 8, 16 or 24")) - handle HOL_ERR {message,...} => - other_errorT ("arm_parse_ror248", message)); + handle HOL_ERR herr => + other_errorT ("arm_parse_ror248", message_of herr)); val arm_parse_sxtb_etc : instruction_mnemonic -> (term * term) M = fn m => @@ -3548,8 +3548,8 @@ val arm_parse_sbfx_etc : instruction_mnemonic -> (term * term) M = | BFI => mk_Bit_Field_Clear_Insert (mk_word5 (l + v),rd,lsb,rn) | _ => raise ERR "arm_parse_sbfx_etc" "invalid mnemonic")) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_sbfx_etc", message))))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_sbfx_etc", message_of herr))))))); local fun barrier_option s = @@ -3654,8 +3654,8 @@ val arm_parse_msr : (term * term) M = (arm_parse_constant >>= (fn i => let val imm12 = int_to_mode1_immediate i in return (enc, mk_Immediate_to_Status (spsr,mask,imm12)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_msr", message))))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_msr", message_of herr))))))); val arm_parse_cps : (term * term) M = need_v6 "arm_parse_cps" @@ -3664,8 +3664,8 @@ val arm_parse_cps : (term * term) M = arm_parse_constant >>= (fn i => let val imm5 = optionSyntax.mk_some (uint_to_word ``:5`` i) in return (enc,mk_Change_Processor_State (mk_word2 0,F,F,F,imm5)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_cps", message)))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_cps", message_of herr)))); fun cps_iflags s = let fun recurse [] x = x @@ -3696,8 +3696,8 @@ val arm_parse_cpsie_cpsid : term -> (term * term) M = arm_parse_constant >>= (fn i => let val imm5 = optionSyntax.mk_some (uint_to_word ``:5`` i) in return (false,imm5) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_cpsie_cpsid", message))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_cpsie_cpsid", message_of herr))) (fn _ => return (true,optionSyntax.mk_none ``:word5``)) >>= (fn (narrow_okay,mode) => read_thumb >>= (fn thumb => @@ -3734,8 +3734,8 @@ val arm_parse_srs : term -> term -> (term * term) M = arm_parse_constant >>= (fn i => let val imm5 = uint_to_word ``:5`` i in return (enc, mk_Store_Return_State (p,inc,w,imm5)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_srs", message)))))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_srs", message_of herr)))))))); val arm_parse_rfe : term -> term -> (term * term) M = fn p => fn inc => @@ -3761,13 +3761,13 @@ val arm_parse_svc : (term * term) M = ("arm_parse_svc", "narrow only with contant 0-255") (return (Encoding_Thumb_tm, mk_Supervisor_Call (uint_to_word ``:24`` i))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_svc", message)) + end handle HOL_ERR herr => + other_errorT ("arm_parse_svc", message_of herr)) else let val imm24 = uint_to_word ``:24`` i in return (Encoding_ARM_tm, mk_Supervisor_Call imm24) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_svc", message))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_svc", message_of herr))); val arm_parse_smc : (term * term) M = thumb2_or_arm_okay "arm_parse_smc" @@ -3778,8 +3778,8 @@ val arm_parse_smc : (term * term) M = assertT OutsideOrLastInITBlock ("arm_parse_smc", "must be outside or last in IT block") (return (enc, mk_Secure_Monitor_Call imm4)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_smc", message)))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_smc", message_of herr)))); val arm_parse_bkpt : (term * term) M = need_v5 "arm_parse_bkpt" @@ -3792,13 +3792,13 @@ val arm_parse_bkpt : (term * term) M = ("arm_parse_bkpt", "narrow only with contant 0-255") (return (Encoding_Thumb_tm, mk_Breakpoint (uint_to_word ``:16`` i))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_bkpt", message)) + end handle HOL_ERR herr => + other_errorT ("arm_parse_bkpt", message_of herr)) else let val imm16 = uint_to_word ``:16`` i in return (Encoding_ARM_tm, mk_Breakpoint imm16) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_bkpt", message)))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_bkpt", message_of herr)))); val arm_parse_nop : (term * term) M = read_thumb >>= (fn thumb => @@ -3877,8 +3877,8 @@ val arm_parse_handler_branch_link : term -> (term * term) M = (arm_parse_constant >>= (fn i => let val h = uint_to_word ``:8`` i in return (Encoding_ThumbEE_tm, mk_Handler_Branch_Link (link,h)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_handler_branch_link", message))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_handler_branch_link", message_of herr))))); val arm_parse_handler_branch_parameter : (term * term) M = read_thumbee >>= (fn thumbee => @@ -3893,8 +3893,8 @@ val arm_parse_handler_branch_parameter : (term * term) M = val h = uint_to_word ``:5`` j in return (Encoding_ThumbEE_tm, mk_Handler_Branch_Parameter (imm3,h)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_handler_branch_parameter", message)))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_handler_branch_parameter", message_of herr)))))); val arm_parse_handler_branch_link_parameter : (term * term) M = read_thumbee >>= (fn thumbee => @@ -3911,9 +3911,9 @@ val arm_parse_handler_branch_link_parameter : (term * term) M = return (Encoding_ThumbEE_tm, mk_Handler_Branch_Link_Parameter (imm5,h)) - end handle HOL_ERR {message,...} => + end handle HOL_ERR herr => other_errorT - ("arm_parse_handler_branch_link_parameter", message)))))); + ("arm_parse_handler_branch_link_parameter", message_of herr)))))); (* ------------------------------------------------------------------------- *) @@ -3942,16 +3942,16 @@ val arm_parse_ldc_stc : instruction_mnemonic -> (term * term) M = (return (F,mk_bool (0 <= v andalso not (i ~~ ``-0i``)),T, mk_word8 (Int.abs (v div 4)))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_ldc_stc", message)) + end handle HOL_ERR herr => + other_errorT ("arm_parse_ldc_stc", message_of herr)) (fn _ => arm_parse_lbrace >>- arm_parse_number >>= (fn i => arm_parse_rbrace >>- let val imm8 = int_to_word ``:8`` i in return (F,T,F,imm8) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_ldc_stc", message)))) + end handle HOL_ERR herr => + other_errorT ("arm_parse_ldc_stc", message_of herr)))) (fn _ => return (T,T,F,mk_word8 0))) (fn _ => arm_parse_comma >>- @@ -3965,8 +3965,8 @@ val arm_parse_ldc_stc : instruction_mnemonic -> (term * term) M = "offset not aligned or beyond permitted range (+/-1020)") (return (T,mk_bool (0 <= v andalso not (i ~~ ``-0i``)),w, mk_word8 (Int.abs (v div 4)))) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_ldc_stc", message)))) >>= + end handle HOL_ERR herr => + other_errorT ("arm_parse_ldc_stc", message_of herr)))) >>= (fn (p,u,w,imm8) => return (enc, case m @@ -3996,14 +3996,14 @@ val arm_parse_cdp : (term * term) M = (fn i => let val imm3 = int_to_word ``:3`` i in return imm3 - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_cdp", message)) + end handle HOL_ERR herr => + other_errorT ("arm_parse_cdp", message_of herr)) (fn _ => return (mk_word3 0)) >>= (fn opc2 => let val imm4 = int_to_word ``:4`` opc1 in return (enc, mk_Coprocessor_Data_Processing (imm4,crn,crd,coproc,opc2,crm)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_cdp", message)))))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_cdp", message_of herr)))))))); val arm_parse_mrc_mcr : instruction_mnemonic -> (term * term) M = fn m => @@ -4022,15 +4022,15 @@ val arm_parse_mrc_mcr : instruction_mnemonic -> (term * term) M = (fn i => let val imm3 = int_to_word ``:3`` i in return imm3 - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mrc_mcr", message)) + end handle HOL_ERR herr => + other_errorT ("arm_parse_mrc_mcr", message_of herr)) (fn _ => return (mk_word3 0)) >>= (fn opc2 => let val imm3 = int_to_word ``:3`` opc1 val b = mk_bool (m = MRC orelse m = MRC2) in return (enc, mk_Coprocessor_Transfer (imm3,b,crn,rt,coproc,opc2,crm)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mrc_mcr", message)))))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_mrc_mcr", message_of herr)))))))); val arm_parse_mrrc_mcrr : instruction_mnemonic -> (term * term) M = fn m => @@ -4049,8 +4049,8 @@ val arm_parse_mrrc_mcrr : instruction_mnemonic -> (term * term) M = val b = mk_bool (m = MRRC orelse m = MRRC2) in return (enc, mk_Coprocessor_Transfer_Two (b,rt2,rt,coproc,imm4,crm)) - end handle HOL_ERR {message,...} => - other_errorT ("arm_parse_mrrc_mcrr", message))))))); + end handle HOL_ERR herr => + other_errorT ("arm_parse_mrrc_mcrr", message_of herr))))))); (* ------------------------------------------------------------------------- *) diff --git a/examples/arm/v7/arm_random_testingLib.sml b/examples/arm/v7/arm_random_testingLib.sml index 57ee80eab5..40a9ed3304 100644 --- a/examples/arm/v7/arm_random_testingLib.sml +++ b/examples/arm/v7/arm_random_testingLib.sml @@ -816,7 +816,7 @@ local in (e,a ^ w,b) end handle HOL_ERR e => - (HOL_WARNING (#origin_structure e) (#origin_function e) + (HOL_WARNING (structure_of e) (function_of e) (String.concat [Hol_pp.term_to_string enc, ": ", Hol_pp.term_to_string tm, "\n"]); diff --git a/examples/l3-machine-code/arm/step/arm_stepLib.sml b/examples/l3-machine-code/arm/step/arm_stepLib.sml index 408e0f22a0..a602573d27 100644 --- a/examples/l3-machine-code/arm/step/arm_stepLib.sml +++ b/examples/l3-machine-code/arm/step/arm_stepLib.sml @@ -2581,11 +2581,12 @@ in "decode ARM (cond not in {14, 15})" x rwts_other) fun find_rw_other tm = Lib.singleton_of_list (utilsLib.find_rw net tm) - handle HOL_ERR {message = "not found", ...} => raise Conv.UNCHANGED - | HOL_ERR {message = m, - origin_function = "singleton_of_list", ...} => - raise ERR "arm_decode" - "more than one matching decode pattern" + handle (e as HOL_ERR herr) => + if message_of herr = "not found" then + raise Conv.UNCHANGED else + if function_of herr = "singleton_of_list" then + raise ERR "arm_decode" "more than one matching decode pattern" + else raise e val FALL_CONV = REWRITE_CONV (DecodeVFP :: datatype_thms [v2w_ground4] @ undef @ @@ -4177,11 +4178,13 @@ in | l => (Parse.print_term tm ; print "\n" ; raise ERR "eval" "more than one valid step theorem")) - handle HOL_ERR {message = "not found", - origin_function = "find_rw", ...} => - raise (Parse.print_term tm - ; print "\n" - ; ERR "eval" "instruction instance not supported") + handle (e as HOL_ERR herr) => + if message_of herr = "not found" andalso + function_of herr = "find_rw" then + raise (Parse.print_term tm + ; print "\n" + ; ERR "eval" "instruction instance not supported") + else raise e end end @@ -4241,8 +4244,10 @@ in val thm = Drule.LIST_CONJ [thm1, thm2, thm3, thm4, thm5, thm6] in MP_Next thm - handle HOL_ERR {message = "different constructors", ...} => - MP_Next0 thm + handle (e as HOL_ERR herr) => + if message_of herr = "different constructors" then + MP_Next0 thm + else raise e end end end diff --git a/examples/l3-machine-code/common/Import.sml b/examples/l3-machine-code/common/Import.sml index fb58811e61..083ba7cc41 100644 --- a/examples/l3-machine-code/common/Import.sml +++ b/examples/l3-machine-code/common/Import.sml @@ -236,8 +236,10 @@ fun Call (f, ty, tm) = let val typ = Type.--> (Term.type_of tm, Ty ty) val vc = mk_local_const (f, typ) - handle HOL_ERR {origin_function = "mk_thy_const", ...} => - Term.mk_var (f, typ) (* for recursion *) + handle (e as HOL_ERR herr) => + if function_of herr = "mk_thy_const" then + Term.mk_var (f, typ) (* for recursion *) + else raise e in Term.mk_comb (vc, tm) end @@ -249,8 +251,10 @@ fun Const (c, ty) = val typ = Ty ty in mk_local_const (c, typ) - handle HOL_ERR {origin_function = "mk_thy_const", ...} => - Term.mk_var (c, typ) (* for recursion *) + handle (e as HOL_ERR herr) => + if function_of herr = "mk_thy_const" then + Term.mk_var (c, typ) (* for recursion *) + else raise e end (* Variables *) @@ -308,7 +312,10 @@ fun CS (x, cs) = fun Let (v,e,b) = boolSyntax.mk_let (Close (v, b), e) - handle HOL_ERR {origin_function = "mk_pabs", ...} => CS (e, [(v, b)]) + handle HOL_ERR herr => + if function_of herr = "mk_pabs" then + CS (e, [(v, b)]) + else raise HOL_ERR herr (* Set of list *) diff --git a/examples/l3-machine-code/common/stateLib.sml b/examples/l3-machine-code/common/stateLib.sml index 953b95cd3c..eff088415b 100644 --- a/examples/l3-machine-code/common/stateLib.sml +++ b/examples/l3-machine-code/common/stateLib.sml @@ -231,8 +231,10 @@ in val tm = thm |> Thm.concl |> boolSyntax.strip_forall |> snd |> boolSyntax.rhs |> pred_setSyntax.strip_set |> List.hd val tm_thm = (REWRITE_CONV thms THENC Conv.CHANGED_CONV EVAL) tm - handle HOL_ERR {origin_function = "CHANGED_CONV", ...} => - combinTheory.I_THM + handle (e as HOL_ERR herr) => + if function_of herr = "CHANGED_CONV" then + combinTheory.I_THM + else raise e in STAR_SELECT_STATE |> Drule.ISPECL ([tm, proj_tm] @ l) @@ -503,7 +505,7 @@ fun define_map_component (s, f, def) = in (mdef, thm) end - handle HOL_ERR {message, ...} => raise ERR "define_map_component" message + handle HOL_ERR herr => raise ERR "define_map_component" (message_of herr) (* ------------------------------------------------------------------------ mk_code_pool: make term ``CODE_POOL f {(v, opc)}`` @@ -518,7 +520,7 @@ in in boolSyntax.list_mk_icomb (code_pool_tm, [f, x]) end - handle HOL_ERR {message, ...} => raise ERR "mk_code_pool" message + handle HOL_ERR herr => raise ERR "mk_code_pool" (message_of herr) end (* ------------------------------------------------------------------------ @@ -837,7 +839,10 @@ in end | NONE => default (f_upd, l, p, q)) | (s, l) => default (s, l, p, q) : (term list * term list)) - handle HOL_ERR {origin_function = "dest_thy_const", ...} => (p, q) + handle (e as HOL_ERR herr) => + if function_of herr = "dest_thy_const" then + (p, q) + else raise e in loop end @@ -1448,7 +1453,8 @@ fun chunks_intro_pre_process m_def = in PURE_REWRITE_RULE rwts thm end - handle HOL_ERR {origin_function = "EQT_ELIM", ...} => thm + handle (e as HOL_ERR herr) => + if function_of herr = "EQT_ELIM" then thm else raise e end end @@ -1467,8 +1473,11 @@ fun chunks_intro be m_def = then thm else helperLib.PRE_POST_RULE cnv (Thm.INST (List.concat s) thm) end - handle HOL_ERR {origin_function = "group_into_n", - message = "too few", ...} => thm + handle (e as HOL_ERR herr) => + if function_of herr = "group_into_n" andalso + message_of herr = "too few" + then thm + else raise e end (* ------------------------------------------------------------------------ @@ -1568,8 +1577,11 @@ in THENC helperLib.POST_CONV (star rwt2)) thm')) end end - handle HOL_ERR {origin_function = "group_into_n", - message = "too few", ...} => thm + handle (e as HOL_ERR herr) => + if function_of herr = "group_into_n" andalso + message_of herr = "too few" + then thm + else raise e end end @@ -1627,7 +1639,7 @@ in List.length l = reg_width orelse raise (err "assertion failed") ; l end - handle HOL_ERR {message = s, ...} => raise (err s) + handle HOL_ERR herr => raise (err (message_of herr)) fun match_register (tm1, v1, _) (tm2, v2, v3) = let val _ = v3 ~~ v2 orelse raise ERR "match_register" "changed" @@ -1668,10 +1680,10 @@ in let val (h, t) = Lib.pluck no_free l - handle - HOL_ERR - {message = "predicate not satisfied", - ...} => (hd l, tl l) + handle (e as HOL_ERR herr) => + if message_of herr = "predicate not satisfied" + then (hd l, tl l) + else raise e fun mtch x = let val s = match_register h x diff --git a/examples/l3-machine-code/common/utilsLib.sml b/examples/l3-machine-code/common/utilsLib.sml index 902cab56ef..f3ed611722 100644 --- a/examples/l3-machine-code/common/utilsLib.sml +++ b/examples/l3-machine-code/common/utilsLib.sml @@ -1211,9 +1211,11 @@ local val l = buildAst thy (dom t) in List.map (fn x => Term.mk_comb (t, x) - handle HOL_ERR {origin_function = "mk_comb", ...} => - (Parse.print_term t; print "\n"; - Parse.print_term x; raise ERR "buildAst" "")) l + handle (e as HOL_ERR herr) => + if function_of herr = "mk_comb" then + (Parse.print_term t; print "\n"; + Parse.print_term x; raise ERR "buildAst" "") + else raise e) l end) n in t0 @ t1 @ List.concat n diff --git a/examples/l3-machine-code/m0/step/m0_stepLib.sml b/examples/l3-machine-code/m0/step/m0_stepLib.sml index f27c1c6770..dc91e5dbe7 100644 --- a/examples/l3-machine-code/m0/step/m0_stepLib.sml +++ b/examples/l3-machine-code/m0/step/m0_stepLib.sml @@ -909,8 +909,10 @@ in val split_thumb2_pat = mk_thumb2_pair o dest_bool_list fun hex_to_bits s = hex_to_bits_16 s - handle HOL_ERR {message = "bad Bool list", ...} => - hex_to_bits_16x2 s + handle HOL_ERR herr => + if message_of herr = "bad Bool list" then + hex_to_bits_16x2 s + else raise HOL_ERR herr fun mk_opcode v = case Lib.total pairSyntax.dest_pair v of SOME (l, r) => @@ -1059,12 +1061,14 @@ in fn v => let val l = dest_bool_list v - handle e as HOL_ERR {message = "bad Bool list", ...} => - let - val (l1, l2) = Lib.with_exn pairSyntax.dest_pair v e - in - dest_bool_list l1 @ dest_bool_list l2 - end + handle (e as HOL_ERR herr) => + if message_of herr = "bad Bool list" then + let + val (l1, l2) = Lib.with_exn pairSyntax.dest_pair v e + in + dest_bool_list l1 @ dest_bool_list l2 + end + else raise e in if List.length l <= 16 then check (v, "is a Thumb-2 prefix") @@ -1189,10 +1193,12 @@ in val (thm, s) = (DecodeThumb, state_with_pcinc ``2w:word32`` :: fst (Term.match_term v1 pat)) - handle HOL_ERR {message = "different constructors", - origin_function = "raw_match_term", ...} => - (DecodeThumb2, - state_with_pcinc ``4w:word32`` :: fst (Term.match_term v2 pat)) + handle (e as HOL_ERR herr) => + if message_of herr = "different constructors" andalso + function_of herr = "raw_match_term" then + (DecodeThumb2, + state_with_pcinc ``4w:word32`` :: fst (Term.match_term v2 pat)) + else raise e in rule (Thm.INST s thm) end @@ -1443,8 +1449,10 @@ local val DecodeThumb2_tm = mk_arm_const "DecodeThumb2" fun mk_decode_thumb t = Term.list_mk_comb (DecodeThumb_tm, [t, pcinc2]) - handle HOL_ERR {message = "incompatible types", ...} => - Term.list_mk_comb (DecodeThumb2_tm, [t, pcinc4]) + handle (e as HOL_ERR herr) => + if message_of herr = "incompatible types" then + Term.list_mk_comb (DecodeThumb2_tm, [t, pcinc4]) + else raise e val rewrites = [v2w_13_15_rwts, bitstringLib.v2n_CONV ``v2n [F;F;F;F;F]``, @@ -1909,11 +1917,13 @@ in | l => (Parse.print_term tm ; print "\n" ; raise ERR "eval" "more than one valid step theorem")) - handle HOL_ERR {message = "not found", - origin_function = "find_rw", ...} => - raise (Parse.print_term tm - ; print "\n" - ; ERR "eval" "instruction instance not supported") + handle (e as HOL_ERR herr) => + if message_of herr = "not found" andalso + function_of herr = "find_rw" then + raise (Parse.print_term tm + ; print "\n" + ; ERR "eval" "instruction instance not supported") + else raise e end end @@ -1959,10 +1969,12 @@ in (utilsLib.ALL_HYP_CONV_RULE (REWRITE_CONV ineq_hyps) thm2, REWRITE_RULE ineq_hyps thm4) val r = get_state thm4 - handle HOL_ERR {origin_function = "dest_pair", ...} => - (Parse.print_thm thm4 - ; print "\n" - ; raise ERR "eval_thumb" "failed to fully evaluate") + handle (e as HOL_ERR herr) => + if function_of herr = "dest_pair" then + (Parse.print_thm thm4 + ; print "\n" + ; raise ERR "eval_thumb" "failed to fully evaluate") + else raise e val thm5 = STATE_CONV (mk_proj_exception r) val thm = Drule.LIST_CONJ [thm1, thm2, thm3, thm4, thm5] in diff --git a/examples/l3-machine-code/mips/prog/mips_progLib.sml b/examples/l3-machine-code/mips/prog/mips_progLib.sml index df0c8bbb65..99a0981384 100644 --- a/examples/l3-machine-code/mips/prog/mips_progLib.sml +++ b/examples/l3-machine-code/mips/prog/mips_progLib.sml @@ -134,8 +134,10 @@ val mips_frame = local fun dest_const tm = Term.dest_const tm - handle e as HOL_ERR {message = "not a const", ...} => + handle e as HOL_ERR herr => + if message_of herr = "not a const" then (Parse.print_term tm; print "\n"; raise e) + else raise e val l = [ "cond", "mips_exception", "mips_exceptionSignalled", diff --git a/examples/l3-machine-code/mips/step/mips_stepLib.sml b/examples/l3-machine-code/mips/step/mips_stepLib.sml index 07e2136800..e9d9505c45 100644 --- a/examples/l3-machine-code/mips/step/mips_stepLib.sml +++ b/examples/l3-machine-code/mips/step/mips_stepLib.sml @@ -1092,9 +1092,11 @@ in | [x] => x | l => (List.app (fn x => (Parse.print_thm x; print "\n")) l ; err "more than one valid step theorem")) - handle HOL_ERR {message = "not found", - origin_function = "find_rw", ...} => - err "instruction instance not supported" + handle (e as HOL_ERR herr) => + if message_of herr = "not found" andalso + function_of herr = "find_rw" + then err "instruction instance not supported" + else raise e end end end diff --git a/examples/l3-machine-code/riscv/step/riscv_stepLib.sml b/examples/l3-machine-code/riscv/step/riscv_stepLib.sml index fa765d2564..794cda036e 100644 --- a/examples/l3-machine-code/riscv/step/riscv_stepLib.sml +++ b/examples/l3-machine-code/riscv/step/riscv_stepLib.sml @@ -277,8 +277,10 @@ in [] => err tm "no valid step theorem" | [x] => x | l => List.last (mlibUseful.sort_map neg_count Int.compare l)) - handle HOL_ERR {message = "not found", origin_function = "find_rw", ...} => - err tm "instruction instance not supported" + handle (e as HOL_ERR herr) => + if message_of herr = "not found" andalso function_of herr = "find_rw" then + err tm "instruction instance not supported" + else raise e end (* ------------------------------------------------------------------------- diff --git a/examples/l3-machine-code/x64/step/x64_stepLib.sml b/examples/l3-machine-code/x64/step/x64_stepLib.sml index 6626d1f108..296d3607e6 100644 --- a/examples/l3-machine-code/x64/step/x64_stepLib.sml +++ b/examples/l3-machine-code/x64/step/x64_stepLib.sml @@ -1145,8 +1145,10 @@ in val thm = Drule.LIST_CONJ [thm1, thm2, thm4, thm5, thm6] in MP_Next thm - handle HOL_ERR {message = "different constructors", ...} => - MP_Next0 thm + handle (e as HOL_ERR herr) => + if message_of herr = "different constructors" then + MP_Next0 thm + else raise e end fun x64_step_hex s = let diff --git a/src/1/Conv.sml b/src/1/Conv.sml index 75d0cf3cd8..bd4dccd70e 100644 --- a/src/1/Conv.sml +++ b/src/1/Conv.sml @@ -27,6 +27,7 @@ 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) @@ -47,7 +48,6 @@ fun w nm c t = c t handle UNCHANGED => raise UNCHANGED * (PART_MATCH (fst o dest_eq));; * *----------------------------------------------------------------------*) - fun REWR_CONV0 (part_matcher, fn_name) th = let val instth = part_matcher lhs th @@ -81,24 +81,26 @@ 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 set_origin fnm (HOL_ERROR recd) = + let val {origin_structure, origin_function, source_location, message} = recd + in 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) + end fun RAND_CONV conv tm = let - val {Rator, Rand} = - dest_comb tm handle HOL_ERR _ => raise ERR "RAND_CONV" "not a comb" + val (Rator, Rand) = + Term.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 in AP_TERM Rator newrand - handle HOL_ERR {message, ...} => - raise ERR "RAND_CONV" ("Application of AP_TERM failed: " ^ message) + handle HOL_ERR e => + raise ERR "RAND_CONV" ("Application of AP_TERM failed: " ^ message_of e) end (*----------------------------------------------------------------------* @@ -113,15 +115,16 @@ fun RAND_CONV conv tm = fun RATOR_CONV conv tm = let - val {Rator, Rand} = - dest_comb tm handle HOL_ERR _ => raise ERR "RATOR_CONV" "not a comb" + val (Rator, Rand) = + Term.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 in AP_THM newrator Rand - handle HOL_ERR {message, ...} => - raise ERR "RATOR_CONV" ("Application of AP_THM failed: " ^ message) + handle HOL_ERR e => + raise ERR "RATOR_CONV" ("Application of AP_THM failed: " ^ message_of e) end (* remember this as "left-hand conv", where RAND_CONV is "right-hand conv". *) @@ -927,11 +930,13 @@ in IMP_ANTISYM_RULE imp1 (DISCH otm thm2) end end - handle e as HOL_ERR {origin_structure = "Conv", - origin_function = "EXISTS_AND_CONV", ...} => raise e - | HOL_ERR _ => raise ERR "EXISTS_AND_CONV" "" + handle e as HOL_ERR herr => + if structure_of herr = "Conv" andalso + function_of herr = "EXISTS_AND_CONV" then raise e + else raise ERR "EXISTS_AND_CONV" "" end + (*----------------------------------------------------------------------* * AND_EXISTS_CONV : move existential quantifier out of conjunction. * * * @@ -959,9 +964,10 @@ in (mk_exists {Bvar = x, Body = mk_conj {conj1 = P, conj2 = Q}})) end - handle e as HOL_ERR {origin_structure = "Conv", - origin_function = "AND_EXISTS_CONV", ...} => raise e - | HOL_ERR _ => raise ERR "AND_EXISTS_CONV" "" + handle e as HOL_ERR herr => + if structure_of herr = "Conv" andalso + function_of herr = "AND_EXISTS_CONV" then raise e + else raise ERR "AND_EXISTS_CONV" "" end (*----------------------------------------------------------------------* @@ -1099,9 +1105,10 @@ in IMP_ANTISYM_RULE imp1 (DISCH otm imp2) end end - handle e as HOL_ERR {origin_structure = "Conv", - origin_function = "FORALL_OR_CONV", ...} => raise e - | HOL_ERR _ => raise ERR "FORALL_OR_CONV" "" + handle e as HOL_ERR herr => + if structure_of herr = "Conv" andalso + function_of herr = "FORALL_OR_CONV" then raise e + else raise ERR "FORALL_OR_CONV" "" end (*----------------------------------------------------------------------* @@ -1130,9 +1137,10 @@ in else SYM (FORALL_OR_CONV (mk_forall {Bvar = x, Body = mk_disj {disj1 = P, disj2 = Q}})) end - handle e as HOL_ERR {origin_structure = "Conv", - origin_function = "OR_FORALL_CONV", ...} => raise e - | HOL_ERR _ => raise ERR "OR_FORALL_CONV" "" + handle e as HOL_ERR herr => + if structure_of herr = "Conv" andalso + function_of herr = "OR_FORALL_CONV" then raise e + else raise ERR "OR_FORALL_CONV" "" end (*----------------------------------------------------------------------* @@ -1257,9 +1265,10 @@ in IMP_ANTISYM_RULE imp1 imp2 end end - handle e as HOL_ERR {origin_structure = "Conv", - origin_function = "FORALL_IMP_CONV", ...} => raise e - | HOL_ERR _ => raise ERR "FORALL_IMP_CONV" "" + handle e as HOL_ERR herr => + if structure_of herr = "Conv" andalso + function_of herr = "FORALL_IMP_CONV" then raise e + else raise ERR "FORALL_IMP_CONV" "" end (*----------------------------------------------------------------------* @@ -1385,9 +1394,10 @@ in IMP_ANTISYM_RULE imp1 imp2 end end - handle e as HOL_ERR {origin_structure = "Conv", - origin_function = "EXISTS_IMP_CONV", ...} => raise e - | HOL_ERR _ => raise ERR "EXISTS_IMP_CONV" "" + handle e as HOL_ERR herr => + if structure_of herr = "Conv" andalso + function_of herr = "EXISTS_IMP_CONV" then raise e + else raise ERR "EXISTS_IMP_CONV" "" end (*----------------------------------------------------------------------* @@ -1499,11 +1509,10 @@ in IMP_ANTISYM_RULE imp1 imp2 end end - 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 *) + handle e as HOL_ERR herr => + if structure_of herr = "Conv" andalso + function_of herr = "X_SKOLEM_CONV" then raise e + else raise ERR "X_SKOLEM_CONV" "" end (*----------------------------------------------------------------------* @@ -1529,7 +1538,6 @@ in X_SKOLEM_CONV (variant (free_vars tm) fv) tm end handle HOL_ERR _ => raise ERR "SKOLEM_CONV" "" - (* val SKOLEM_CONV = w "SKOLEM_CONV" SKOLEM_CONV *) end (*----------------------------------------------------------------------* @@ -1622,7 +1630,7 @@ in end else err (#Name (dest_var x) ^ " has the wrong type") end - handle e => raise (wrap_exn "Conv" "X_FUN_EQ_CONV" e) + handle e => raise wrap_exn "Conv" "X_FUN_EQ_CONV" e end (*----------------------------------------------------------------------* @@ -1700,6 +1708,7 @@ end * * * Fails if the term is not a conjunction. * *----------------------------------------------------------------------*) + local val conv = REWR_CONV (GSYM CONJ_ASSOC) in @@ -1710,7 +1719,7 @@ fun SPLICE_CONJ_CONV t = if is_conj t then recurse t else - raise mk_HOL_ERR "Conv" "SPLICE_CONJ_CONV" "Not a conjunction" + raise ERR "SPLICE_CONJ_CONV" "Not a conjunction" end end (* local *) @@ -2237,7 +2246,7 @@ in else if aconv rhs T then SPEC lhs bT else raise ERR "bool_EQ_CONV" "inapplicable" end - handle e => raise (wrap_exn "Conv" "bool_EQ_CONV" e) + handle e => raise wrap_exn "Conv" "bool_EQ_CONV" e end (*----------------------------------------------------------------------* @@ -2442,7 +2451,7 @@ fun AC_CONV (associative, commutative) = EQT_INTRO (EQ_MP (SYM init) (asce (dest_eq gl))) end end - handle e => raise (wrap_exn "Conv" "AC_CONV" e) + handle e => raise wrap_exn "Conv" "AC_CONV" e (*--------------------------------------------------------------------------* * Conversions for messing with bound variables. * diff --git a/src/1/Mutual.sml b/src/1/Mutual.sml index 4660365ec5..7e7a9f31db 100644 --- a/src/1/Mutual.sml +++ b/src/1/Mutual.sml @@ -291,6 +291,8 @@ and GALPHA tm = (* --------------------------------------------------------------------- *) local val bool = genvar (Type.bool) +val ILL_FORMED = ERR "MUTUAL_INDUCT_THEN" "ill-formed induction theorem" + fun MUTUAL_INDUCT_THEN1 th = let val th' = REPAIR th (* @@ -377,10 +379,12 @@ fun MUTUAL_INDUCT_THEN1 th = handle HOL_ERR _ => raise ERR "MUTUAL_INDUCT_THEN" "tactic application error" end - handle (e as HOL_ERR - {origin_structure = "Mutual", - origin_function = "MUTUAL_INDUCT_THEN",...}) => raise e - | _ => raise ERR "MUTUAL_INDUCT_THEN" "ill-formed induction theorem" + handle (e as HOL_ERR herr) => + if structure_of herr = "Mutual" andalso + function_of herr = "MUTUAL_INDUCT_THEN" then + raise e + else raise ILL_FORMED + | otherwise => raise ILL_FORMED in diff --git a/src/1/Tactical.sml b/src/1/Tactical.sml index 62be0965e6..938eaf8954 100644 --- a/src/1/Tactical.sml +++ b/src/1/Tactical.sml @@ -52,16 +52,22 @@ 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, ...}) => - (mesg ("Proof of \n\n" ^ Parse.term_to_string t ^ "\n\nfailed.\n") - ; (case (m, f, unsolved ()) of - ("unsolved goals", "TAC_PROOF", (_, u)::_) => - if Term.term_eq u t - then () - else mesg ("First unsolved sub-goal is\n\n" ^ - Parse.term_to_string u ^ "\n\n") - | _ => ()) - ; raise e) + handle e as HOL_ERR herr => + let val m = message_of herr + val f = function_of herr + in + mesg ("Proof of \n\n" ^ Parse.term_to_string t ^ "\n\nfailed.\n") + ; + (case (m, f, unsolved ()) + of ("unsolved goals", "TAC_PROOF", (_, u)::_) => + if Term.term_eq u t then + () + else mesg ("First unsolved sub-goal is\n\n" ^ + Parse.term_to_string u ^ "\n\n") + | otherwise => ()) + ; + raise e + end val internal_prover = ref (provide_feedback default_prover: Term.term * tactic -> Thm.thm) in @@ -222,13 +228,16 @@ fun op THEN1 (tac1: tactic, tac2: tactic) : tactic = end val op >- = op THEN1 + fun op>>-(tac1, n) tac2 g = op>- (tac1, tac2) g - handle e as HOL_ERR (er as {message,...}) => - if is_substring "THEN1" message then raise e + handle e as HOL_ERR er => + if is_substring "THEN1" (message_of er) then raise e else - raise HOL_ERR (set_message - (message ^ " (THEN1 on line "^Int.toString n^")") er) + raise HOL_ERR + (set_message + (message_of er ^ " (THEN1 on line "^Int.toString n^")") er) + fun (f ?? x) = f x @@ -556,6 +565,7 @@ fun CONJ_VALIDATE tac (g as (asl,_)) = end end (* local *) + (* could avoid duplication of code in the above by the following fun GEN_VALIDATE flag tac = ALL_TAC THEN_LT GEN_VALIDATE_LT flag (TACS_TO_LT [tac]) ; @@ -873,8 +883,8 @@ local in (gl, (if is_neg w then NEG_DISCH ant else DISCH ant) o prf) end - handle HOL_ERR {message,origin_function, ...} => - raise ERR "DISCH_THEN" (origin_function ^ ":" ^ message) + handle HOL_ERR e => + raise ERR "DISCH_THEN" (function_of e ^ ":" ^ message_of e) 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..3d61f14cba 100644 --- a/src/HolSat/satTools.sml +++ b/src/HolSat/satTools.sml @@ -1,4 +1,3 @@ - structure satTools = struct local @@ -6,7 +5,6 @@ local open Lib boolLib Globals Parse Term Type Thm Drule Psyntax Conv Feedback open SatSolvers satCommonTools satTheory - in infix |->; @@ -125,12 +123,12 @@ 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 - then UNDISCH (EQF_ELIM (REWRITE_CONV [] t)) - handle HOL_ERR _ => raise satCheckError - else raise satCheckError - | _ => raise satCheckError; + | HOL_ERR herr => + if function_of herr = "EQT_ELIM" andalso is_neg t then + (UNDISCH (EQF_ELIM (REWRITE_CONV [] t)) + handle HOL_ERR _ => raise satCheckError) + else raise satCheckError + | otherwise => raise satCheckError; end end diff --git a/src/HolSmt/HolSmtLib.sml b/src/HolSmt/HolSmtLib.sml index a4bae505ce..ca7aacb3ad 100644 --- a/src/HolSmt/HolSmtLib.sml +++ b/src/HolSmt/HolSmtLib.sml @@ -63,8 +63,8 @@ structure HolSmtLib :> HolSmtLib = struct ) fun provoke_err prove_fn = ignore (prove_fn boolSyntax.T) (* should fail *) - handle Feedback.HOL_ERR {message, ...} => - Feedback.HOL_MESG ("HolSmtLib: " ^ message) + handle Feedback.HOL_ERR herr => + Feedback.HOL_MESG ("HolSmtLib: " ^ Feedback.message_of herr) in Feedback.set_trace "HolSmtLib" 0; if CVC.is_configured () then diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml index 5ea5452f20..49af909f52 100644 --- a/src/HolSmt/selftest.sml +++ b/src/HolSmt/selftest.sml @@ -49,12 +49,15 @@ 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, source_location, message} => - die ("Test of solver '" ^ name ^ "' failed on term '" ^ + handle Feedback.HOL_ERR (HOL_ERROR recd) => + let val {origin_structure, origin_function, source_location, message} = recd + in + die ("Test of solver '" ^ name ^ "' failed on term '" ^ term_with_types t ^ "': exception HOL_ERR (in " ^ origin_structure ^ "." ^ origin_function ^ " " ^ locn.toString source_location ^ ", message: " ^ message ^ ")") + end in if null (Thm.hyp thm) andalso Thm.concl thm ~~ t then () else @@ -76,7 +79,9 @@ 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, source_location, message} => + end handle Feedback.HOL_ERR (HOL_ERROR recd) => + let val {origin_structure, origin_function, source_location, message} = recd + in if origin_structure = "HolSmtLib" andalso origin_function = "GENERIC_SMT_TAC" andalso (message = "solver reports negated term to be 'satisfiable'" orelse @@ -91,7 +96,7 @@ fun expect_sat name smt_tac t = origin_structure ^ "." ^ origin_function ^ " " ^ locn.toString source_location ^ ", message: " ^ message ^ ")") - + end fun mk_test_fun is_configured expect_fun name smt_tac = if is_configured then (fn g => (expect_fun name smt_tac g; print ".")) diff --git a/src/IndDef/selftest.sml b/src/IndDef/selftest.sml index ee9b6d315a..9110b6cfa0 100644 --- a/src/IndDef/selftest.sml +++ b/src/IndDef/selftest.sml @@ -95,22 +95,22 @@ val _ = shouldfail {testfn = quietly (xHol_reln "tr"), val _ = tprint "Vacuous clause failure" val _ = if (Hol_reln `(!x. rel x Z) /\ (!x y. rel x y)` ; false) - handle HOL_ERR {message,...} => + handle HOL_ERR herr => String.isSuffix "Vacuous clause trivialises whole definition" - message + (message_of herr) then OK() else die "FAILED" val _ = shouldfail { testfn = quietly (xHol_reln "tr"), printresult = (fn (th,_,_) => thm_to_string th), printarg = K "Double implication should fail", - checkexn = (fn(HOL_ERR{message,...}) => + checkexn = (fn(HOL_ERR herr) => String.isSubstring "double implication" - message + (message_of herr) | _ => false) } - ‘fib Z ONE /\ fib ONE ONE /\ !m r s. fib m r ==> fib (SUC m) s ==> fib (SUC (SUC m)) (r + s)’ - + ‘fib Z ONE /\ fib ONE ONE /\ !m r s. fib m r ==> fib (SUC m) s ==> fib (SUC (SUC m)) (r + s)’ + (* isolate_to_front test cases *) val failcount = ref 0 val _ = diemode := Remember failcount diff --git a/src/TeX/holindex.sml b/src/TeX/holindex.sml index 7c4a7c6f7a..d86379446a 100644 --- a/src/TeX/holindex.sml +++ b/src/TeX/holindex.sml @@ -197,7 +197,7 @@ let val (ty, tm) = destruct_theory_thm (valOf content); val _ = DB.fetch ty tm handle HOL_ERR e => - (report_error (#message e);Feedback.fail()); + (report_error (message_of e);Feedback.fail()); in () end else (); diff --git a/src/basicProof/BasicProvers.sml b/src/basicProof/BasicProvers.sml index 4af88a517d..ce99f70b9c 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 herr => + if function_of herr = "Q_TAC" then raise e else case qlinenum q of SOME l => raise ERR "suffices_by" @@ -630,12 +630,9 @@ fun (q suffices_by tac) g = | NONE => raise ERR "suffices_by" "suffices_by's tactic failed to prove goal" - - fun subgoal q = Q.SUBGOAL_THEN q STRIP_ASSUME_TAC val sg = subgoal - infix on fun ((ttac:thm->tactic) on (q:term frag list, tac:tactic)) : tactic = (fn (g as (asl:term list, w:term)) => let diff --git a/src/boss/selftest.sml b/src/boss/selftest.sml index b45ec7eee1..1cd7169754 100644 --- a/src/boss/selftest.sml +++ b/src/boss/selftest.sml @@ -43,10 +43,11 @@ 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, ...} => - 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\"" + handle HOL_ERR herr => + if function_of herr <> "new_type_definition" orelse + structure_of herr <> "Theory.Definition" orelse + message_of herr <> + "at Thm.prim_type_definition:\nexpected a theorem of the form \"?x. P x\"" then die "FAILED" else OK() diff --git a/src/boss/theory_tests/bylocnScript.sml b/src/boss/theory_tests/bylocnScript.sml index 824826957e..b8ee670078 100644 --- a/src/boss/theory_tests/bylocnScript.sml +++ b/src/boss/theory_tests/bylocnScript.sml @@ -10,13 +10,13 @@ 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 herr => if suffp then - if message = "suffices_by's tactic failed to prove goal on line "^ + if message_of herr = "suffices_by's tactic failed to prove goal on line "^ Int.toString l then save_thm("test" ^ Int.toString (!c), TRUTH) else raise e - else if message = "by's tactic failed to prove subgoal on line "^ + else if message_of herr = "by's tactic failed to prove subgoal on line "^ Int.toString l then save_thm("test" ^ Int.toString (!c), TRUTH) else raise e) diff --git a/src/coretypes/PairedLambda.sml b/src/coretypes/PairedLambda.sml index 9c3b8bd426..73f861d26c 100644 --- a/src/coretypes/PairedLambda.sml +++ b/src/coretypes/PairedLambda.sml @@ -100,7 +100,7 @@ fun PAIRED_ETA_CONV tm = in EXT (GEN xv (SUBS [SYM peq] bth)) end - handle HOL_ERR {message, ...} => raise ERR "PAIRED_ETA_CONV" message + handle HOL_ERR herr => raise ERR "PAIRED_ETA_CONV" (message_of herr) end; (*--------------------------------------------------------------------*) diff --git a/src/finite_maps/alist_treeLib.sml b/src/finite_maps/alist_treeLib.sml index 24e5737780..db999161bc 100644 --- a/src/finite_maps/alist_treeLib.sml +++ b/src/finite_maps/alist_treeLib.sml @@ -70,7 +70,7 @@ fun assume_prems thm = if not (is_imp (concl thm)) then thm fun do_inst_mp insts mp_thm arg_thm = let val (prem, _) = dest_imp (concl mp_thm) fun rerr e s = let - val m = s ^ ": " ^ #message e + val m = s ^ ": " ^ message_of e in print ("error in do_inst_mp: " ^ m ^ "\n"); print_thm mp_thm; print "\n"; print_thm arg_thm; print "\n"; raise (err "do_inst_mp" m) end diff --git a/src/floating-point/binary_ieeeLib.sml b/src/floating-point/binary_ieeeLib.sml index 5dc9c795cb..f01ac5018a 100644 --- a/src/floating-point/binary_ieeeLib.sml +++ b/src/floating-point/binary_ieeeLib.sml @@ -392,10 +392,12 @@ local val c = boolSyntax.mk_conj (f0, e1) in mlibUseful.INL (ties_to_even (boolSyntax.mk_imp (c, rx))) - handle HOL_ERR {origin_function = "EQT_ELIM", ...} => - mlibUseful.INR - (conj_assoc_rule - (ties_to_even (boolSyntax.mk_conj (c, boolSyntax.mk_neg rx)))) + handle (e as HOL_ERR herr) => + if function_of herr = "EQT_ELIM" then + mlibUseful.INR + (conj_assoc_rule + (ties_to_even (boolSyntax.mk_conj (c, boolSyntax.mk_neg rx)))) + else raise e end val lt_thm = Drule.MATCH_MP (REAL_ARITH ``(a <= b <=> F) ==> b < a: real``) diff --git a/src/integer/CooperMath.sml b/src/integer/CooperMath.sml index 2c2f9bd658..61c4cf0304 100644 --- a/src/integer/CooperMath.sml +++ b/src/integer/CooperMath.sml @@ -534,7 +534,10 @@ local 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 + end handle (e as HOL_ERR herr) => + (if structure_of herr = "Lib" then + ALL_CONV tm + else raise e) 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..ca84f7070e 100644 --- a/src/integer/IntDP_Munge.sml +++ b/src/integer/IntDP_Munge.sml @@ -235,9 +235,11 @@ in LAND_CONV eliminate_nat_quants THENC RATOR_CONV (RATOR_CONV (RAND_CONV eliminate_nat_quants)) else ALL_CONV -end tm handle HOL_ERR {origin_function = "REWR_CONV", ...} => - raise ERR "IntDP_Munge" "Uneliminable natural number term remains" - +end tm +handle (e as HOL_ERR herr) => + if function_of herr = "REWR_CONV" then + raise ERR "IntDP_Munge" "Uneliminable natural number term remains" + else raise e fun tacTHEN t1 t2 tm = let val (g1, v1) = t1 tm diff --git a/src/integer/selftest.sml b/src/integer/selftest.sml index 5761fb1f8d..03eeca5d65 100644 --- a/src/integer/selftest.sml +++ b/src/integer/selftest.sml @@ -8,8 +8,8 @@ fun okparse_exnstruct s = s = "Parse" orelse s = "Preterm" val _ = shouldfail { - checkexn = fn HOL_ERR {origin_structure, ...} => - okparse_exnstruct origin_structure + checkexn = fn HOL_ERR herr => + okparse_exnstruct (structure_of herr) | _ => false, printarg = (fn s => "Parse should fail: “" ^ s ^ "”"), printresult = term_to_string, @@ -18,8 +18,8 @@ val _ = val _ = shouldfail { - checkexn = fn HOL_ERR {origin_structure, ...} => - okparse_exnstruct origin_structure + checkexn = fn HOL_ERR herr => + okparse_exnstruct (structure_of herr) | _ => false, printarg = (fn s => "Parse should be ambiguous: “" ^ s ^ "”"), printresult = term_to_string, diff --git a/src/list/src/listSyntax.sml b/src/list/src/listSyntax.sml index daeed68184..73215f1cb7 100644 --- a/src/list/src/listSyntax.sml +++ b/src/list/src/listSyntax.sml @@ -177,7 +177,8 @@ fun dest_mem t = let val (x,setl) = pred_setSyntax.dest_in t in (x, dest_list_to_set setl) -end handle HOL_ERR {message,...} => raise ERR "dest_mem" message +end +handle HOL_ERR herr => raise ERR "dest_mem" (message_of herr) (*--------------------------------------------------------------------------- diff --git a/src/metis/metisTools.sml b/src/metis/metisTools.sml index 2b15c1a9d7..7c1bafe85a 100644 --- a/src/metis/metisTools.sml +++ b/src/metis/metisTools.sml @@ -209,8 +209,10 @@ fun const_scheme c = fun trap f g x = f x - handle e as HOL_ERR {message, ...} => - (if not (contains "proof translation error" message) then raise e else + handle e as HOL_ERR herr => + (if not (contains "proof translation error" (message_of herr)) then + raise e + else (chatting 1 andalso chat "metis: proof translation error: trying again with types.\n"; g x)); diff --git a/src/n-bit/bitstringLib.sml b/src/n-bit/bitstringLib.sml index e4f90d6ed4..6256132eaf 100644 --- a/src/n-bit/bitstringLib.sml +++ b/src/n-bit/bitstringLib.sml @@ -148,7 +148,7 @@ in in Drule.MATCH_MP (Thm.INST_TYPE [Type.alpha |-> ty] v2w_n2w_thm) thm end - handle HOL_ERR {message = m, ...} => raise ERR "v2w_n2w_CONV" m + handle HOL_ERR herr => raise ERR "v2w_n2w_CONV" (message_of herr) end val v2w_n2w_ss = @@ -168,7 +168,7 @@ fun n2w_v2w_CONV tm = in Thm.SYM (v2w_n2w_CONV (bitstringSyntax.mk_v2w (l, ty))) end - handle HOL_ERR {message = m, ...} => raise ERR "n2w_v2w_CONV" m + handle HOL_ERR herr => raise ERR "n2w_v2w_CONV" (message_of herr) (* ------------------------------------------------------------------------- *) @@ -202,7 +202,7 @@ fun v2w_eq_CONV tm = THENC FIX_CONV) THENC listLib.LIST_EQ_SIMP_CONV) tm end - handle HOL_ERR {message = m, ...} => raise ERR "v2w_eq_n2w_CONV" m + handle HOL_ERR herr => raise ERR "v2w_eq_n2w_CONV" (message_of herr) (* ------------------------------------------------------------------------- *) @@ -236,7 +236,7 @@ in then (Conv.RHS_CONV v2w_n2w_CONV THENC wordsLib.word_EQ_CONV) tm else wordsLib.word_EQ_CONV tm end - handle HOL_ERR {message = m, ...} => raise ERR "word_eq_CONV" m + handle HOL_ERR herr => raise ERR "word_eq_CONV" (message_of herr) end (* ------------------------------------------------------------------------- *) @@ -292,7 +292,7 @@ in THENC Conv.RAND_CONV (Conv.RAND_CONV shiftr_CONV) THENC Conv.RAND_CONV FIX_CONV) tm end - handle HOL_ERR {message = m, ...} => raise ERR "extract_v2w_CONV" m + handle HOL_ERR herr => raise ERR "extract_v2w_CONV" (message_of herr) end (* ------------------------------------------------------------------------- *) @@ -335,7 +335,7 @@ in in (c THENC Conv.REWR_CONV thm THENC cnv) tm end - handle HOL_ERR {message = m, ...} => raise ERR "word_bit_CONV" m + handle HOL_ERR herr => raise ERR "word_bit_CONV" (message_of herr) end (* ------------------------------------------------------------------------- *) diff --git a/src/n-bit/selftest.sml b/src/n-bit/selftest.sml index 6d65779562..7370f8affd 100644 --- a/src/n-bit/selftest.sml +++ b/src/n-bit/selftest.sml @@ -92,8 +92,8 @@ fun test_counter (c:conv) tm = let NONE else SOME "bad counterexample" - | HOL_ERR {origin_function,...} => - SOME ("unexpected exception from " ^ origin_function) + | HOL_ERR herr => + SOME ("unexpected exception from " ^ function_of herr) in tprint ("Counterexample: " ^ trunc 49 tm); case res of diff --git a/src/n-bit/wordsLib.sml b/src/n-bit/wordsLib.sml index d0d667d27f..14a5f34a02 100644 --- a/src/n-bit/wordsLib.sml +++ b/src/n-bit/wordsLib.sml @@ -1533,10 +1533,10 @@ fun WORD_SUB_CONV tm = 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" + handle (e as HOL_ERR herr) => + if function_of herr = "CHANGED_CONV" then raise Conv.UNCHANGED - else raise HOL_ERR err + else raise e val WORD_SUB_ss = simpLib.name_ss "WORD_SUB" @@ -1829,8 +1829,10 @@ fun WORD_BIT_INDEX_CONV toindex = in Drule.ISPEC w (Drule.MATCH_MP thm lt) end - handle HOL_ERR {origin_function = "EQT_ELIM", ...} => - raise ERR "WORD_BIT_INDEX_CONV" "index too large" + handle e as HOL_ERR herr => + if function_of herr = "EQT_ELIM" then + raise ERR "WORD_BIT_INDEX_CONV" "index too large" + else raise e end (* ------------------------------------------------------------------------- *) diff --git a/src/num/theories/cv_compute/automation/cv_transLib.sml b/src/num/theories/cv_compute/automation/cv_transLib.sml index dbba1a7def..ecc32d7911 100644 --- a/src/num/theories/cv_compute/automation/cv_transLib.sml +++ b/src/num/theories/cv_compute/automation/cv_transLib.sml @@ -914,7 +914,7 @@ fun get_code_eq_info const_tm = let val tm = cv_def |> SPEC_ALL |> concl |> dest_eq |> snd val res = get_cv_consts tm handle HOL_ERR e => let - val _ = print ("\nERROR: " ^ #message e ^ "\n") + val _ = print ("\nERROR: " ^ message_of e ^ "\n") val _ = print "This appears in definition:\n\n" val _ = print_thm cv_def val _ = print "\n\n" diff --git a/src/parse/ParseDatatype.sml b/src/parse/ParseDatatype.sml index 01cfd4963e..a156083c9c 100644 --- a/src/parse/ParseDatatype.sml +++ b/src/parse/ParseDatatype.sml @@ -271,8 +271,10 @@ fun parse_harg G qb = end else (parse_atom G qb - handle HOL_ERR {origin_structure = "Parse", message, ...} => - raise ERR "parse_harg" message) + handle e as HOL_ERR herr => + if structure_of herr = "Parse" then + raise ERR "parse_harg" (message_of herr) + else raise e) | (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..919d498b33 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(HOL_ERROR{origin_structure,origin_function,message,...}) => P (origin_structure, origin_function, message) | _ => false diff --git a/src/postkernel/HolKernel.sml b/src/postkernel/HolKernel.sml index 5f03a79036..a789d9ff34 100644 --- a/src/postkernel/HolKernel.sml +++ b/src/postkernel/HolKernel.sml @@ -183,7 +183,7 @@ fun list_mk_lbinop _ [] = raise ERR "list_mk_lbinop" "empty list" fun mk_binder c f (p as (Bvar, _)) = mk_comb (inst [alpha |-> type_of Bvar] c, mk_abs p) - handle HOL_ERR {message, ...} => raise ERR f message + handle HOL_ERR e => raise ERR f (message_of e) fun list_mk_fun (dtys, rty) = List.foldr op--> rty dtys @@ -227,7 +227,7 @@ in in Term.list_mk_comb (Term.inst (Type.match_type tyl tyr) tm, xs) end - handle HOL_ERR {message, ...} => raise ERR "list_mk_icomb" message + handle HOL_ERR e => raise ERR "list_mk_icomb" (message_of e) fun syntax_fns {n: int, make: term -> 'a -> term, dest: term -> exn -> term -> 'b} diff --git a/src/res_quan/src/Cond_rewrite.sml b/src/res_quan/src/Cond_rewrite.sml index 5bcd77d8dc..355e8d1d1e 100644 --- a/src/res_quan/src/Cond_rewrite.sml +++ b/src/res_quan/src/Cond_rewrite.sml @@ -167,8 +167,8 @@ fun MATCH_SUBS th fvs asm mlist = (* --------------------------------------------------------------------- *) fun COND_REWR_TAC f th = - (fn (asm,gl) => - (let val (vars,body) = strip_forall (concl th) + fn (asm,gl) => + let val (vars,body) = strip_forall (concl th) val (antes,eqn) = strip_imp body val {lhs=tml, rhs=tmr} = dest_eq eqn val freevars = subtract vars (frees tml) @@ -183,9 +183,10 @@ fun COND_REWR_TAC f th = ((SUBGOAL_THEN (hd sgl) STRIP_ASSUME_TAC THENL[ REPEAT CONJ_TAC, SUBST_TAC thms]) (asm,gl)) end - handle HOL_ERR {message = message,...} => - (raise COND_REWR_ERR {function="COND_REWR_TAC", - message=message}))); + handle HOL_ERR herr => + raise COND_REWR_ERR + {function="COND_REWR_TAC", + message=message_of herr} (* ---------------------------------------------------------------------*) (* search_top_down carries out a top-down left-to-right search for *) @@ -250,12 +251,13 @@ val COND_REWRITE1_TAC:thm_tactic = fn th => (* instance(s) are used in a REWRITE_CONV to produce the final theorem. *) (* --------------------------------------------------------------------- *) -fun COND_REWR_CONV f th = (fn tm => +fun COND_REWR_CONV f th = + fn tm => let val (vars,b) = strip_forall (concl th) - val tm1 = lhs(snd(strip_imp b)) - val ilist = f tm1 tm + val tm1 = lhs(snd(strip_imp b)) + val ilist = f tm1 tm in - if (null ilist) + if null ilist then raise COND_REWR_ERR{function="COND_REWR_CONV", message="no match"} else let val thm1 = SPEC_ALL th val rlist = map (fn l => UNDISCH_ALL(INST_TY_TERM l thm1)) ilist @@ -263,19 +265,20 @@ fun COND_REWR_CONV f th = (fn tm => REWRITE_CONV rlist tm end end - handle HOL_ERR {message = message,...} => - (raise COND_REWR_ERR {function="COND_REWR_CONV", - message=message})):conv; + handle HOL_ERR herr => + raise COND_REWR_ERR {function="COND_REWR_CONV", + message=message_of herr} (* ---------------------------------------------------------------------*) (* COND_REWRITE1_CONV : thm list -> thm -> conv *) (* COND_REWRITE1_CONV thms thm tm *) (* ---------------------------------------------------------------------*) -fun COND_REWRITE1_CONV thms th = (fn tm => + +fun COND_REWRITE1_CONV thms th = fn tm => let val thm1 = COND_REWR_CONV search_top_down (COND_REWR_CANON th) tm in itlist PROVE_HYP thms thm1 - end):conv; + end end (* structure Cond_rewrite *) diff --git a/src/res_quan/src/res_quanLib.sml b/src/res_quan/src/res_quanLib.sml index 5eab677137..0b961a561e 100644 --- a/src/res_quan/src/res_quanLib.sml +++ b/src/res_quan/src/res_quanLib.sml @@ -362,8 +362,8 @@ fun RESQ_IMP_RES_THEN ttac resth = let val th = check_res resth in IMP_RES_THEN ttac th end - handle HOL_ERR{message = s,...} => - raise ERR "RESQ_IMP_RES_THEN" s + handle HOL_ERR herr => + raise ERR "RESQ_IMP_RES_THEN" (message_of herr) (* --------------------------------------------------------------------- *) (* RESQ_RES_THEN : Resolve all restricted universally quantified *) @@ -573,8 +573,8 @@ fun RESQ_DEF_EXISTS_RULE tm = else defthm end end - handle HOL_ERR {message = s,...} => - raise ERR "RESQ_DEF_EXISTS_RULE" s; + handle HOL_ERR herr => + raise ERR "RESQ_DEF_EXISTS_RULE" (message_of herr); (* --------------------------------------------------------------------- *) (* new_gen_resq_definition flag (name, (--`!x1::P1. ... !xn::Pn. *) diff --git a/src/simp/src/Traverse.sml b/src/simp/src/Traverse.sml index e1f5e5c285..f5a997e64d 100644 --- a/src/simp/src/Traverse.sml +++ b/src/simp/src/Traverse.sml @@ -183,11 +183,14 @@ 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", - message = "Congruence gives no change", ...} => raise e + handle e as HOL_ERR herr => + if structure_of herr = "Opening" andalso + function_of herr = "CONGPROC" andalso + message_of herr = "Congruence gives no change" + then raise e + else FIRSTCQC_CONV cs t | Interrupt => raise Interrupt - | _ => FIRSTCQC_CONV cs t + | otherwise => FIRSTCQC_CONV cs t end (* And another thing. The current simplifer doesn't allow users to diff --git a/src/tactictoe/src/tttEval.sml b/src/tactictoe/src/tttEval.sml index fc797a37bf..7e67c0c4d3 100644 --- a/src/tactictoe/src/tttEval.sml +++ b/src/tactictoe/src/tttEval.sml @@ -14,15 +14,22 @@ open HolKernel Abbrev boolLib aiLib tttSetup tttSearch tttRecord tacticToe tttToken tttTrain val ERR = mk_HOL_ERR "tttEval" + fun catch_err 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); - raise ERR "tttEval" "error caught (see log)") + f x handle HOL_ERR (HOL_ERROR recd) => + let val {origin_structure,origin_function,source_location,message} = recd + in print_endline (String.concat + [msg, ":", origin_structure, ":", origin_function, ":", + locn.toShortString source_location, ":", message]); + raise ERR "tttEval" "error caught (see log)" + end 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)) + f x handle HOL_ERR (HOL_ERROR recd) => + let val {origin_structure,origin_function,source_location,message} = recd + in print_endline (String.concat + [msg, ":", origin_structure, ":", origin_function, ":", + locn.toShortString source_location, ":", message]) + end (* ------------------------------------------------------------------------- diff --git a/src/tfl/src/Defn.sml b/src/tfl/src/Defn.sml index 4d0e77df82..904634322a 100644 --- a/src/tfl/src/Defn.sml +++ b/src/tfl/src/Defn.sml @@ -1131,8 +1131,12 @@ fun pairf (stem, eqs0) = (tuple_args [(f, (stem', argtys))] eqs0, stem'name, untuple_args) end end - handle e as HOL_ERR {message = "incompatible types", ...} => - case move_arg eqs0 of SOME tm => pairf (stem, tm) | NONE => raise e + handle e as HOL_ERR herr => + if message_of herr = "incompatible types" then + (case move_arg eqs0 + of SOME tm => pairf (stem, tm) + | NONE => raise e) + else raise e (*---------------------------------------------------------------------------*) (* Abbreviation or prim. rec. definitions. *) @@ -1233,9 +1237,12 @@ fun stdrec_defn (facts,(stem,stem'),wfrec_res,untuple) = in TotalDefn. ---------------------------------------------------------------------------*) -fun holexnMessage (HOL_ERR {origin_structure,origin_function,source_location,message}) = - origin_structure ^ "." ^ origin_function ^ - ":" ^ locn.toShortString source_location ^ ": " ^ message +fun holexnMessage (HOL_ERR (HOL_ERROR recd)) = + let val {origin_structure,origin_function,source_location,message} = recd + in String.concat + [origin_structure, ".", origin_function, ":", + locn.toShortString source_location, ": ", message] + end | holexnMessage e = General.exnMessage e fun is_simple_arg t = diff --git a/src/tfl/src/selftest.sml b/src/tfl/src/selftest.sml index 2093aa6d62..578ef4b107 100644 --- a/src/tfl/src/selftest.sml +++ b/src/tfl/src/selftest.sml @@ -52,10 +52,10 @@ fun define q = in Defn.mk_defn (hd names) tm end -fun exnlookfor sl (Exn (HOL_ERR {message,...})) = - if List.all (fn s => String.isSubstring s message) sl then OK() +fun exnlookfor sl (Exn (HOL_ERR herr)) = + if List.all (fn s => String.isSubstring s (message_of herr)) sl then OK() else - die ("\nBad exception message:\n "^message) + die ("\nBad exception message:\n "^message_of herr) | exnlookfor _ (Exn e) = die ("\nException not a HOL_ERR;\n "^General.exnMessage e) | exnlookfor _ _ = die ("\nExecution unexpectedly successful") diff --git a/src/unwind/unwindLib.sml b/src/unwind/unwindLib.sml index 44343af5ca..0586322264 100644 --- a/src/unwind/unwindLib.sml +++ b/src/unwind/unwindLib.sml @@ -116,9 +116,10 @@ fun CONJ_FORALL_ONCE_CONV t = in IMP_ANTISYM_RULE th1 th2 end end - handle (e as HOL_ERR{origin_function = "CONJ_FORALL_ONCE_CONV",...}) - => raise e - | HOL_ERR _ => raise UNWIND_ERR "CONJ_FORALL_ONCE_CONV" "" + handle (e as HOL_ERR herr) => + if function_of herr = "CONJ_FORALL_ONCE_CONV" then + raise e + else raise UNWIND_ERR "CONJ_FORALL_ONCE_CONV" "" end; (*---------------------------------------------------------------------------*) From 6c68a5cb16f6fb8cd4f617944f136e1e975f155b Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Mon, 15 Sep 2025 16:10:35 -0500 Subject: [PATCH 03/13] prelim solution to getting HOL_ERR to prettyprint properly --- src/prekernel/Feedback.sig | 4 ++-- src/prekernel/Feedback.sml | 47 ++++++++++++++++++++++---------------- tools-poly/prelude.ML | 5 ++-- 3 files changed, 32 insertions(+), 24 deletions(-) diff --git a/src/prekernel/Feedback.sig b/src/prekernel/Feedback.sig index 7bac38f634..2c1609f694 100644 --- a/src/prekernel/Feedback.sig +++ b/src/prekernel/Feedback.sig @@ -6,6 +6,8 @@ sig source_location : locn.locn, message : string} + exception HOL_ERR of hol_error + val structure_of : hol_error -> string val function_of : hol_error -> string val location_of : hol_error -> locn.locn @@ -14,8 +16,6 @@ sig val set_origin_function : string -> hol_error -> hol_error val pp_hol_error : hol_error -> HOLPP.pretty - exception HOL_ERR of hol_error - val mk_HOL_ERR : string -> string -> string -> exn val mk_HOL_ERRloc : string -> string -> locn.locn -> string -> exn val wrap_exn : string -> string -> exn -> exn diff --git a/src/prekernel/Feedback.sml b/src/prekernel/Feedback.sml index 9cc7181cd0..4eefefb78b 100644 --- a/src/prekernel/Feedback.sml +++ b/src/prekernel/Feedback.sml @@ -20,6 +20,8 @@ datatype hol_error = source_location : locn.locn, message : string} +exception HOL_ERR of hol_error; + (*--------------------------------------------------------------------------- Projections ---------------------------------------------------------------------------*) @@ -29,26 +31,6 @@ fun function_of (HOL_ERROR {origin_function,...}) = origin_function fun location_of (HOL_ERROR {source_location,...}) = source_location fun message_of (HOL_ERROR {message,...}) = message -exception HOL_ERR of hol_error - -fun format_err_recd {message, origin_function, origin_structure, source_location} = - String.concat - ["at ", origin_structure, ".", origin_function, ":\n", - case source_location of - locn.Loc_Unknown => "" - | _ => locn.toString source_location ^ ":\n", - message] - -fun format_hol_error(HOL_ERROR recd) = format_err_recd recd - -fun pp_hol_error (HOL_ERROR recd) = - let open HOLPP - val {origin_structure, origin_function, source_location, message} = recd - in block CONSISTENT 0 - [add_string (origin_structure^"."^origin_function),add_string ":",NL,NL, - add_string message, NL,NL, add_string (locn.toString source_location)] - end - (*--------------------------------------------------------------------------- Curried version of HOL_ERR; can be more comfortable to use. ---------------------------------------------------------------------------*) @@ -89,6 +71,31 @@ fun set_message msg (HOL_ERROR recd) = message = msg} end +fun pp_hol_error (HOL_ERROR recd) = + let open HOLPP + val {origin_structure, origin_function, source_location, message} = recd + in block CONSISTENT 0 + [add_string (origin_structure^"."^origin_function),add_string ":", + NL,NL, add_string message, NL,NL, + add_string (locn.toString source_location)] + end + +val _ = + let fun pp i _ e = pp_hol_error e + in PolyML.addPrettyPrinter pp + end + +fun format_err_recd + {message, origin_function, origin_structure, source_location} = + String.concat + ["at ", origin_structure, ".", origin_function, ":\n", + case source_location of + locn.Loc_Unknown => "" + | _ => locn.toString source_location ^ ":\n", + message] + +fun format_hol_error(HOL_ERROR recd) = format_err_recd recd + val ERR = mk_HOL_ERR "Feedback" (* local to this file *) (*--------------------------------------------------------------------------- diff --git a/tools-poly/prelude.ML b/tools-poly/prelude.ML index 6a21ea6823..483ef76725 100644 --- a/tools-poly/prelude.ML +++ b/tools-poly/prelude.ML @@ -119,8 +119,9 @@ in PolyML.addPrettyPrinter (pp2polypp proofManagerLib.pp_proof); PolyML.addPrettyPrinter (pp2polypp proofManagerLib.pp_proofs); PolyML.addPrettyPrinter (pp2polypp type_grammar.prettyprint_grammar); - PolyML.addPrettyPrinter (pp2polypp Feedback.pp_trace_elt); - PolyML.addPrettyPrinter (pp2polypp Feedback.pp_hol_error) + PolyML.addPrettyPrinter (pp2polypp Feedback.pp_trace_elt) +(* ; + PolyML.addPrettyPrinter (pp2polypp Feedback.pp_hol_error) *) end val _ = PolyML.use (OS.Path.concat(HOLDIR, "tools-poly/holinteractive.ML")); From a33cf0ebbac0b5828fd7256b881966ddb6c10ae4 Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Fri, 19 Sep 2025 01:10:10 -0500 Subject: [PATCH 04/13] tidy up printing of hol_error elements --- src/num/termination/TotalDefn.sml | 30 +++++----- src/prekernel/Feedback.sig | 8 ++- src/prekernel/Feedback.sml | 92 ++++++++++++++++--------------- 3 files changed, 70 insertions(+), 60 deletions(-) diff --git a/src/num/termination/TotalDefn.sml b/src/num/termination/TotalDefn.sml index f3c20d1d61..1256203fed 100644 --- a/src/num/termination/TotalDefn.sml +++ b/src/num/termination/TotalDefn.sml @@ -31,13 +31,13 @@ val WARN = HOL_WARNING "TotalDefn"; fun render_exn srcfn e = if !Globals.interactive then - (Feedback.output_ERR (Feedback.exn_to_string e); - raise ERR srcfn "Exception raised") + raise e else - raise e + (Feedback.output_ERR (Feedback.exn_to_string e); + raise BATCH_ERR srcfn) (*---------------------------------------------------------------------------*) -(* Set up trace stuff *) +(* Set up traces *) (*---------------------------------------------------------------------------*) local @@ -689,7 +689,7 @@ local open Defn else () in if not (!Globals.interactive) then - raise ERR "defnDefine" (msg1 defName loc ^ goalstring) + raise ERR "defnDefine" (msg1 defName loc ^ "\n" ^ goalstring ^ "\n") else raise ERR "defnDefine" (msg1 defName loc ^ msg2 defName goalstring) end @@ -709,23 +709,23 @@ local open Defn val V = params_of defn val _ = if not (null V) then fvs_on_rhs V else () (* can fail *) val (defn',opt) = - if should_try_to_prove_termination defn V then - let val tprover = proveTotal (mk_term_tac()) - fun try_proof Rcand = tprover (set_reln defn Rcand) - in - (if reln_is_not_set defn then (* look for suitable term. reln *) + if not (should_try_to_prove_termination defn V) then + (defn,NONE) + else + let val tprover = proveTotal (mk_term_tac()) + fun try_proof Rcand = tprover (set_reln defn Rcand) + in + (if reln_is_not_set defn then (* look for suitable term. reln *) let val candidates = guessR defn val (cand,result) = trylist try_proof candidates val () = report_successful_candidate cand candidates in result end - else (* one is already installed, try to prove TCs *) + else (* one is already installed, try to prove TCs *) tprover defn - ) handle HOL_ERR _ => + ) handle HOL_ERR _ => (report_failure_of_candidates(); termination_proof_failed loc defn) - end - else - (defn,NONE) + end in save_defn_at loc defn' ; (LIST_CONJ (map GEN_ALL (eqns_of defn')), ind_of defn', opt) diff --git a/src/prekernel/Feedback.sig b/src/prekernel/Feedback.sig index 2c1609f694..811da7515b 100644 --- a/src/prekernel/Feedback.sig +++ b/src/prekernel/Feedback.sig @@ -6,15 +6,19 @@ sig source_location : locn.locn, message : string} - exception HOL_ERR of hol_error - val structure_of : hol_error -> string val function_of : hol_error -> string val location_of : hol_error -> locn.locn val message_of : hol_error -> string + val dest_hol_error : hol_error -> string * string * locn.locn * string + val mk_hol_error : string -> string -> locn.locn -> string -> hol_error val set_message : string -> hol_error -> hol_error val set_origin_function : string -> hol_error -> hol_error val pp_hol_error : hol_error -> HOLPP.pretty + val trivial_hol_error : hol_error + + exception HOL_ERR of hol_error + exception BATCH_ERR of string val mk_HOL_ERR : string -> string -> string -> exn val mk_HOL_ERRloc : string -> string -> locn.locn -> string -> exn diff --git a/src/prekernel/Feedback.sml b/src/prekernel/Feedback.sml index 4eefefb78b..1b3b684b52 100644 --- a/src/prekernel/Feedback.sml +++ b/src/prekernel/Feedback.sml @@ -20,38 +20,67 @@ datatype hol_error = source_location : locn.locn, message : string} -exception HOL_ERR of hol_error; - -(*--------------------------------------------------------------------------- - Projections - ---------------------------------------------------------------------------*) +fun mk_hol_error s1 s2 loc mesg = + HOL_ERROR + {origin_structure = s1, + origin_function = s2, + source_location = loc, + message = mesg} + +val trivial_hol_error = mk_hol_error "" "" locn.Loc_None "" + +fun dest_hol_error (HOL_ERROR recd) = + let val {origin_structure, origin_function, source_location, message} = recd + in (origin_structure, origin_function, source_location, message) + end fun structure_of (HOL_ERROR {origin_structure,...}) = origin_structure fun function_of (HOL_ERROR {origin_function,...}) = origin_function fun location_of (HOL_ERROR {source_location,...}) = source_location fun message_of (HOL_ERROR {message,...}) = message +fun pp_hol_error (err as HOL_ERROR recd) = + let open HOLPP + val {origin_structure, origin_function, source_location, message} = recd + in if err = trivial_hol_error then + add_string "" + else + block INCONSISTENT 0 (List.concat [ + [add_string "at ", + add_string (origin_structure^"."^origin_function),add_string ":", + add_break(1,0)], + (case source_location + of locn.Loc_Unknown => [] + | _ => [add_string (locn.toString source_location ^":"),add_break(1,0)]), + [add_string message] + ]) + end + +fun format_err_recd recd = + HOLPP.pp_to_string (!Globals.linewidth) pp_hol_error (HOL_ERROR recd) + +val _ = + let fun pp i _ e = pp_hol_error e + in PolyML.addPrettyPrinter pp + end + +(*---------------------------------------------------------------------------*) +(* Exception used in HOL code. *) +(*---------------------------------------------------------------------------*) + +exception HOL_ERR of hol_error; + +exception BATCH_ERR of string; + (*--------------------------------------------------------------------------- Curried version of HOL_ERR; can be more comfortable to use. ---------------------------------------------------------------------------*) -fun mk_HOL_ERR s1 s2 s3 = - HOL_ERR - (HOL_ERROR - {origin_structure = s1, - origin_function = s2, - source_location = locn.Loc_Unknown, - message = s3}) +fun mk_HOL_ERRloc s1 s2 locn s3 = HOL_ERR (mk_hol_error s1 s2 locn s3) -(* Errors with a known location. *) +fun mk_HOL_ERR s1 s2 s3 = HOL_ERR (mk_hol_error s1 s2 locn.Loc_Unknown s3) -fun mk_HOL_ERRloc s1 s2 locn s3 = - HOL_ERR - (HOL_ERROR - {origin_structure = s1, - origin_function = s2, - source_location = locn, - message = s3}) +(* Errors with a known location. *) fun set_origin_function fnm (HOL_ERROR recd) = let val {origin_structure, source_location, message, ...} = recd @@ -71,29 +100,6 @@ fun set_message msg (HOL_ERROR recd) = message = msg} end -fun pp_hol_error (HOL_ERROR recd) = - let open HOLPP - val {origin_structure, origin_function, source_location, message} = recd - in block CONSISTENT 0 - [add_string (origin_structure^"."^origin_function),add_string ":", - NL,NL, add_string message, NL,NL, - add_string (locn.toString source_location)] - end - -val _ = - let fun pp i _ e = pp_hol_error e - in PolyML.addPrettyPrinter pp - end - -fun format_err_recd - {message, origin_function, origin_structure, source_location} = - String.concat - ["at ", origin_structure, ".", origin_function, ":\n", - case source_location of - locn.Loc_Unknown => "" - | _ => locn.toString source_location ^ ":\n", - message] - fun format_hol_error(HOL_ERROR recd) = format_err_recd recd val ERR = mk_HOL_ERR "Feedback" (* local to this file *) From 77421eae09b97bf16e8900d1e14e831cfa6dd3c5 Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Tue, 23 Sep 2025 18:33:09 -0500 Subject: [PATCH 05/13] patching up selftests --- src/boss/selftest.sml | 4 +-- src/boss/theory_tests/github196Script.sml | 3 +- src/n-bit/selftest.sml | 5 ++-- src/num/termination/selftest.sml | 35 +++++++++++++---------- 4 files changed, 25 insertions(+), 22 deletions(-) diff --git a/src/boss/selftest.sml b/src/boss/selftest.sml index 1cd7169754..0eb8d889f7 100644 --- a/src/boss/selftest.sml +++ b/src/boss/selftest.sml @@ -14,8 +14,6 @@ val goal_toString = pairp (listp term_to_string, term_to_string) val goals_toString = listp goal_toString - - fun test_CONV (c,nm) (t, expected) = let val _ = tprint (nm^" on `"^term_to_string t^"`") val th = Conv.QCONV c t @@ -47,7 +45,7 @@ val _ = if function_of herr <> "new_type_definition" orelse structure_of herr <> "Theory.Definition" orelse message_of herr <> - "at Thm.prim_type_definition:\nexpected a theorem of the form \"?x. P x\"" + "at Thm.prim_type_definition: expected a theorem of the form \"?x. P x\"" then die "FAILED" else OK() diff --git a/src/boss/theory_tests/github196Script.sml b/src/boss/theory_tests/github196Script.sml index 95715a4f7f..ffeed87f00 100644 --- a/src/boss/theory_tests/github196Script.sml +++ b/src/boss/theory_tests/github196Script.sml @@ -4,5 +4,4 @@ val _ = ( Define ` (dummy2 c NONE = c) /\ (dummy2 d (SOME _) = c)` ; print "Malformed definition goes through - FAILURE\n"; OS.Process.exit OS.Process.failure) -handle HOL_ERR _ => print "Test-case OK\n" - +handle BATCH_ERR _ => print "Test-case OK\n" diff --git a/src/n-bit/selftest.sml b/src/n-bit/selftest.sml index 7370f8affd..92109d2352 100644 --- a/src/n-bit/selftest.sml +++ b/src/n-bit/selftest.sml @@ -150,8 +150,9 @@ val _ = let trace ("Definition.auto Defn.tgoal", 0) $ trace ("Theory.allow_rebinds", 1) $ quietly $ - TotalDefn.qDefine "wfact" - ‘wfact w = if w = 0w then 1 else w2n w * wfact (w - 1w)’ + Lib.with_flag(Globals.interactive, true) + (TotalDefn.qDefine "wfact" + ‘wfact w = if w = 0w then 1 else w2n w * wfact (w - 1w)’) in require_msg (check_result (K true)) thm_to_string fact_defn NONE; TotalDefn.temp_exclude_termsimp "words.WORD_PRED_THM"; diff --git a/src/num/termination/selftest.sml b/src/num/termination/selftest.sml index 84720122c5..e1d6635fbd 100644 --- a/src/num/termination/selftest.sml +++ b/src/num/termination/selftest.sml @@ -73,23 +73,28 @@ fun tdefoutput_pp(th,thopt) = "(" ^ thm_to_string th ^ ", " ^ (case thopt of NONE => "NONE" | SOME th' => "SOME " ^ thm_to_string th') ^ ")" + fun quietDefn f x = Lib.with_flag (Globals.interactive, false) f x -val _ = shouldfail { checkexn = is_struct_HOL_ERR "TotalDefn", - printarg = K "tDefine: no schematic defs when \ - \termination tac is supplied", - printresult = tdefoutput_pp, - testfn = (fn q => quietDefn (TotalDefn.tDefine "foo" q) - (WF_REL_TAC ‘$<’))} - ‘foo x = if x = 0 then y else foo(x - 1)*2’; - -val _ = shouldfail { checkexn = is_struct_HOL_ERR "TotalDefn", - printarg = K "qDefine: no schematic defs when \ - \termination tac is supplied", - printresult = thm_to_string, - testfn = (fn q => quietDefn (TotalDefn.qDefine "foo" q) - (SOME (WF_REL_TAC ‘$<’)))} - ‘foo x = if x = 0 then y else foo(x - 1)*2’; + +fun repl_mode f x = + Lib.with_flag (Globals.interactive, true) f x + +val _ = + shouldfail + { checkexn = is_struct_HOL_ERR "TotalDefn", + printarg = K "tDefine: no schematic defs when termination tac is supplied", + printresult = tdefoutput_pp, + testfn = (fn q => repl_mode (TotalDefn.tDefine "foo" q) (WF_REL_TAC ‘$<’))} + ‘foo x = if x = 0 then y else foo(x - 1)*2’; + +val _ = + shouldfail + { checkexn = is_struct_HOL_ERR "TotalDefn", + printarg = K "qDefine: no schematic defs when termination tac is supplied", + printresult = thm_to_string, + testfn = (fn q => repl_mode(TotalDefn.qDefine "foo" q) (SOME (WF_REL_TAC ‘$<’)))} + ‘foo x = if x = 0 then y else foo(x - 1)*2’; fun lhs_has_two_args th = th |> concl |> strip_forall |> #2 |> lhs |> strip_comb |> #2 |> length From be5e78aba81c1032cb8b876acdff8456a75cf371 Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Tue, 23 Sep 2025 18:52:33 -0500 Subject: [PATCH 06/13] move useful function to Feedback --- src/num/termination/TotalDefn.sml | 7 ------- src/prekernel/Feedback.sig | 1 + src/prekernel/Feedback.sml | 17 +++++++++++++++-- 3 files changed, 16 insertions(+), 9 deletions(-) diff --git a/src/num/termination/TotalDefn.sml b/src/num/termination/TotalDefn.sml index 1256203fed..915fc30ea5 100644 --- a/src/num/termination/TotalDefn.sml +++ b/src/num/termination/TotalDefn.sml @@ -29,13 +29,6 @@ val ERR = mk_HOL_ERR "TotalDefn"; val ERRloc = mk_HOL_ERRloc "TotalDefn"; val WARN = HOL_WARNING "TotalDefn"; -fun render_exn srcfn e = - if !Globals.interactive then - raise e - else - (Feedback.output_ERR (Feedback.exn_to_string e); - raise BATCH_ERR srcfn) - (*---------------------------------------------------------------------------*) (* Set up traces *) (*---------------------------------------------------------------------------*) diff --git a/src/prekernel/Feedback.sig b/src/prekernel/Feedback.sig index 811da7515b..2bbbfba44a 100644 --- a/src/prekernel/Feedback.sig +++ b/src/prekernel/Feedback.sig @@ -20,6 +20,7 @@ sig exception HOL_ERR of hol_error exception BATCH_ERR of string + val render_exn : string -> exn -> 'a val mk_HOL_ERR : string -> string -> string -> exn val mk_HOL_ERRloc : string -> string -> locn.locn -> string -> exn val wrap_exn : string -> string -> exn -> exn diff --git a/src/prekernel/Feedback.sml b/src/prekernel/Feedback.sml index 1b3b684b52..491396f09d 100644 --- a/src/prekernel/Feedback.sml +++ b/src/prekernel/Feedback.sml @@ -43,7 +43,7 @@ fun pp_hol_error (err as HOL_ERROR recd) = let open HOLPP val {origin_structure, origin_function, source_location, message} = recd in if err = trivial_hol_error then - add_string "" + add_string "" else block INCONSISTENT 0 (List.concat [ [add_string "at ", @@ -65,7 +65,7 @@ val _ = end (*---------------------------------------------------------------------------*) -(* Exception used in HOL code. *) +(* Exceptions used in HOL code. *) (*---------------------------------------------------------------------------*) exception HOL_ERR of hol_error; @@ -165,6 +165,19 @@ fun exn_to_string (HOL_ERR herr) = !ERR_to_string herr | exn_to_string Portable.Interrupt = raise Portable.Interrupt | exn_to_string e = General.exnMessage e +(*---------------------------------------------------------------------------*) +(* Either raise the exception, presumably a HOL_ERR, in the REPL (it gets *) +(* printed by the installed prettyprinter) or print the error and raise *) +(* BATCH_ERR with a message. *) +(*---------------------------------------------------------------------------*) + +fun render_exn srcfn e = + if !Globals.interactive then + raise e + else + (output_ERR (exn_to_string e); + raise BATCH_ERR srcfn) + fun Raise e = (output_ERR (exn_to_string e); raise e) local From 297298151ac4def49edea5e8ab95ff278e5a2fc9 Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Thu, 25 Sep 2025 03:07:47 -0500 Subject: [PATCH 07/13] add repl/batch mode awareness to errors emerging from Modern Syntax constructs --- src/1/boolLib.sml | 33 ++++++++++++++++++++++----------- src/IndDef/CoIndDefLib.sml | 5 ++++- src/IndDef/IndDefLib.sml | 6 ++++-- src/datatype/Datatype.sml | 13 ++++++++++--- 4 files changed, 40 insertions(+), 17 deletions(-) diff --git a/src/1/boolLib.sml b/src/1/boolLib.sml index 956ca8be79..37d44bda50 100644 --- a/src/1/boolLib.sml +++ b/src/1/boolLib.sml @@ -6,7 +6,7 @@ structure boolLib = struct -open boolTheory boolSyntax Hol_pp ParseExtras +open boolTheory boolSyntax Hol_pp ParseExtras Feedback Drule Tactical Tactic Thm_cont Conv Rewrite Prim_rec Abbrev DB BoundedRewrites TexTokenMap term_tactic @@ -14,6 +14,8 @@ local open TypeBase Ho_Rewrite Psyntax Rsyntax in end val parse_from_grammars = Parse.parse_from_grammars; +val ERR = mk_HOL_ERR "boolLib" + (*--------------------------------------------------------------------------- Stock the rewriter in Ho_Rewrite with some rules not yet proved in boolTheory. @@ -104,8 +106,6 @@ val UNIQUE_SKOLEM_THM = prove ASM_REWRITE_TAC[], DISCH_THEN(MP_TAC o C AP_THM ``x:'a``) THEN REWRITE_TAC[BETA_THM]]]) - - end (* local open *) val def_suffix = ref "_def" @@ -130,13 +130,13 @@ in fun save_thm_attrs loc (attrblock, th) = let val {thmname=n,attrs,unknown,reserved} = attrblock val _ = null unknown orelse - raise mk_HOL_ERR "boolLib" "save_thm_attrs" + raise ERR "save_thm_attrs" ("Unknown attributes: " ^ String.concatWith ", " (map #1 unknown)) val (localp,privp,rebindok,reserved_leftover) = extract_localpriv (false,false,false,[]) reserved val _ = null reserved_leftover orelse - raise mk_HOL_ERR "boolLib" "save_thm_attrs" + raise ERR "save_thm_attrs" ("Unhandled attributes: " ^ String.concatWith ", " (map #1 reserved_leftover)) val save = @@ -151,17 +151,28 @@ fun save_thm_attrs loc (attrblock, th) = let in storemod save(n,th) before app do_attr attrs end -fun store_thm_at loc (n0,t,tac) = let - val attrblock = ThmAttribute.extract_attributes n0 - val th = Tactical.prove(t,tac) - handle e => (print ("Failed to prove theorem " ^ #thmname attrblock ^ ".\n"); - Raise e) + +local + fun tac_failure s1 s2 = + String.concat ["Failed to prove theorem ", s1, ".\n", s2] in - save_thm_attrs loc (attrblock,th) +fun store_thm_at loc (n0,t,tac) = + let val attrblock = ThmAttribute.extract_attributes n0 + val th = Tactical.prove(t,tac) handle HOL_ERR herr => + let val err_mesg = tac_failure (#thmname attrblock) (message_of herr) + val err = HOL_ERR (set_message err_mesg herr) + in raise wrap_exn "boolLib" "store_thm_at" err end + in + save_thm_attrs loc (attrblock,th) + end + handle e => render_exn "store_thm_at" e end + val store_thm = store_thm_at DB.Unknown + fun save_thm_at loc (n0,th) = save_thm_attrs loc (ThmAttribute.extract_attributes n0,th) + val save_thm = save_thm_at DB.Unknown fun new_recursive_definition rcd = diff --git a/src/IndDef/CoIndDefLib.sml b/src/IndDef/CoIndDefLib.sml index 2ec40af471..5ada0fa44a 100644 --- a/src/IndDef/CoIndDefLib.sml +++ b/src/IndDef/CoIndDefLib.sml @@ -194,13 +194,16 @@ val parse = fun xHol_coreln name q = Hol_mono_coreln name (!IndDefLib.the_monoset) (parse q) + handle e as HOL_ERR _ => + render_exn "xHol_coreln" (wrap_exn "CoIndDefLib" "xHol_coreln" e) fun Hol_coreln q = let val def as (def_t, _) = parse q val name = IndDefLib.name_from_def def_t in Hol_mono_coreln name (!IndDefLib.the_monoset) def -end handle e => Raise (wrap_exn "CoIndDefLib" "Hol_coreln" e); +end handle e => + render_exn "Hol_coreln" (wrap_exn "CoIndDefLib" "Hol_coreln" e) end (* CoIndDefLib *) diff --git a/src/IndDef/IndDefLib.sml b/src/IndDef/IndDefLib.sml index e5eb063694..d4087397cc 100644 --- a/src/IndDef/IndDefLib.sml +++ b/src/IndDef/IndDefLib.sml @@ -495,7 +495,8 @@ val parse = fun xHol_reln name q = Hol_mono_reln name (!the_monoset) (parse q) - handle e => Raise (wrap_exn "IndDefLib" "Hol_reln" e) + handle e => + render_exn "xHol_reln" (wrap_exn "IndDefLib" "Hol_reln" e) fun name_from_def t = let open boolSyntax @@ -510,6 +511,7 @@ fun Hol_reln q = let val name = name_from_def def_t in Hol_mono_reln name (!the_monoset) def -end handle e => Raise (wrap_exn "IndDefLib" "Hol_reln" e); +end handle e => + render_exn "Hol_reln" (wrap_exn "IndDefLib" "Hol_reln" e) end diff --git a/src/datatype/Datatype.sml b/src/datatype/Datatype.sml index ab7c9ae7fe..7fade76368 100644 --- a/src/datatype/Datatype.sml +++ b/src/datatype/Datatype.sml @@ -771,10 +771,17 @@ fun astHol_datatype astl = in persistent_tyinfo tyinfos; HOL_MESG message - end handle e as HOL_ERR _ => Raise (wrap_exn "Datatype" "Hol_datatype" e); + end + +fun Hol_datatype q = + astHol_datatype (ParseDatatype.parse (type_grammar()) q) + handle e as HOL_ERR _ => + render_exn "Hol_datatype" (wrap_exn "Datatype" "Hol_datatype" e) -fun Hol_datatype q = astHol_datatype (ParseDatatype.parse (type_grammar()) q) -fun Datatype q = astHol_datatype (ParseDatatype.hparse (type_grammar()) q) +fun Datatype q = + astHol_datatype (ParseDatatype.hparse (type_grammar()) q) + handle e as HOL_ERR _ => + render_exn "Datatype" (wrap_exn "Datatype" "Datatype" e) val _ = Parse.temp_set_grammars ambient_grammars From f93fcf1b928ce6d81988e058e53d85173d2de411 Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Thu, 25 Sep 2025 03:31:25 -0500 Subject: [PATCH 08/13] repl/batch mode awareness for Theorem construct --- src/1/boolLib.sml | 5 +++-- src/prekernel/Feedback.sig | 6 +++--- src/prekernel/Feedback.sml | 6 +++--- 3 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/1/boolLib.sml b/src/1/boolLib.sml index 37d44bda50..c3a1f8d049 100644 --- a/src/1/boolLib.sml +++ b/src/1/boolLib.sml @@ -6,7 +6,7 @@ structure boolLib = struct -open boolTheory boolSyntax Hol_pp ParseExtras Feedback +open boolTheory boolSyntax Hol_pp ParseExtras Drule Tactical Tactic Thm_cont Conv Rewrite Prim_rec Abbrev DB BoundedRewrites TexTokenMap term_tactic @@ -14,7 +14,7 @@ local open TypeBase Ho_Rewrite Psyntax Rsyntax in end val parse_from_grammars = Parse.parse_from_grammars; -val ERR = mk_HOL_ERR "boolLib" +val ERR = Feedback.mk_HOL_ERR "boolLib" (*--------------------------------------------------------------------------- Stock the rewriter in Ho_Rewrite with some rules not yet @@ -153,6 +153,7 @@ in end local + open Feedback fun tac_failure s1 s2 = String.concat ["Failed to prove theorem ", s1, ".\n", s2] in diff --git a/src/prekernel/Feedback.sig b/src/prekernel/Feedback.sig index 2bbbfba44a..a1b8725139 100644 --- a/src/prekernel/Feedback.sig +++ b/src/prekernel/Feedback.sig @@ -6,16 +6,16 @@ sig source_location : locn.locn, message : string} + val mk_hol_error : string -> string -> locn.locn -> string -> hol_error + val dest_hol_error : hol_error -> string * string * locn.locn * string + val empty_hol_error : hol_error val structure_of : hol_error -> string val function_of : hol_error -> string val location_of : hol_error -> locn.locn val message_of : hol_error -> string - val dest_hol_error : hol_error -> string * string * locn.locn * string - val mk_hol_error : string -> string -> locn.locn -> string -> hol_error val set_message : string -> hol_error -> hol_error val set_origin_function : string -> hol_error -> hol_error val pp_hol_error : hol_error -> HOLPP.pretty - val trivial_hol_error : hol_error exception HOL_ERR of hol_error exception BATCH_ERR of string diff --git a/src/prekernel/Feedback.sml b/src/prekernel/Feedback.sml index 491396f09d..bd3fc9a27d 100644 --- a/src/prekernel/Feedback.sml +++ b/src/prekernel/Feedback.sml @@ -27,7 +27,7 @@ fun mk_hol_error s1 s2 loc mesg = source_location = loc, message = mesg} -val trivial_hol_error = mk_hol_error "" "" locn.Loc_None "" +val empty_hol_error = mk_hol_error "" "" locn.Loc_None "" fun dest_hol_error (HOL_ERROR recd) = let val {origin_structure, origin_function, source_location, message} = recd @@ -42,8 +42,8 @@ fun message_of (HOL_ERROR {message,...}) = message fun pp_hol_error (err as HOL_ERROR recd) = let open HOLPP val {origin_structure, origin_function, source_location, message} = recd - in if err = trivial_hol_error then - add_string "" + in if err = empty_hol_error then + add_string "" else block INCONSISTENT 0 (List.concat [ [add_string "at ", From d0c904c8a5ed99a38eac50fe9e8da1ee0ac8189d Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Fri, 26 Sep 2025 03:07:03 -0500 Subject: [PATCH 09/13] more pursuit of nice error messages coming from Modern Syntax --- src/1/boolLib.sml | 16 +++++++++------ src/IndDef/IndDefLib.sml | 2 +- src/boss/theory_tests/bylocnScript.sml | 27 +++++++++++++------------- src/num/termination/selftest.sml | 7 ++----- src/parse/testutils.sig | 2 ++ src/parse/testutils.sml | 6 ++++++ 6 files changed, 35 insertions(+), 25 deletions(-) diff --git a/src/1/boolLib.sml b/src/1/boolLib.sml index c3a1f8d049..88581e6176 100644 --- a/src/1/boolLib.sml +++ b/src/1/boolLib.sml @@ -155,18 +155,22 @@ end local open Feedback fun tac_failure s1 s2 = - String.concat ["Failed to prove theorem ", s1, ".\n", s2] + String.concat ["Failed to prove theorem ", Lib.quote s1, ":\n", s2] in fun store_thm_at loc (n0,t,tac) = let val attrblock = ThmAttribute.extract_attributes n0 - val th = Tactical.prove(t,tac) handle HOL_ERR herr => - let val err_mesg = tac_failure (#thmname attrblock) (message_of herr) - val err = HOL_ERR (set_message err_mesg herr) - in raise wrap_exn "boolLib" "store_thm_at" err end + val name = #thmname attrblock + val th = Tactical.prove(t,tac) + handle HOL_ERR herr => + let val err_mesg = tac_failure name (message_of herr) + val err = HOL_ERR (set_message err_mesg herr) + in render_exn "store_thm_at" + (wrap_exn "boolLib" "store_thm_at" err) end in save_thm_attrs loc (attrblock,th) + handle e => render_exn "store_thm_at" + (wrap_exn "boolLib" "store_thm_at" e) end - handle e => render_exn "store_thm_at" e end val store_thm = store_thm_at DB.Unknown diff --git a/src/IndDef/IndDefLib.sml b/src/IndDef/IndDefLib.sml index d4087397cc..bd483bff37 100644 --- a/src/IndDef/IndDefLib.sml +++ b/src/IndDef/IndDefLib.sml @@ -496,7 +496,7 @@ val parse = fun xHol_reln name q = Hol_mono_reln name (!the_monoset) (parse q) handle e => - render_exn "xHol_reln" (wrap_exn "IndDefLib" "Hol_reln" e) + render_exn "xHol_reln" (wrap_exn "IndDefLib" "xHol_reln" e) fun name_from_def t = let open boolSyntax diff --git a/src/boss/theory_tests/bylocnScript.sml b/src/boss/theory_tests/bylocnScript.sml index b8ee670078..ad0307e9a0 100644 --- a/src/boss/theory_tests/bylocnScript.sml +++ b/src/boss/theory_tests/bylocnScript.sml @@ -1,10 +1,9 @@ Theory bylocn - - +Libs testutils val c = ref 0 -fun test l suffp q = +fun test l suffp q = (* NB: tactic error wrapped by store_thm error handling *) (c := !c + 1; store_thm("test" ^ Int.toString (!c), ``something impossible : bool``, @@ -12,22 +11,24 @@ fun test l suffp q = else q by ALL_TAC)) handle e as HOL_ERR herr => if suffp then - if message_of herr = "suffices_by's tactic failed to prove goal on line "^ - Int.toString l + if String.isSuffix + ("suffices_by's tactic failed to prove goal on line "^ Int.toString l) + (message_of herr) then save_thm("test" ^ Int.toString (!c), TRUTH) else raise e - else if message_of herr = "by's tactic failed to prove subgoal on line "^ - Int.toString l + else if String.isSuffix + ("by's tactic failed to prove subgoal on line "^ Int.toString l) + (message_of herr) then save_thm("test" ^ Int.toString (!c), TRUTH) else raise e) -val _ = test 24 false `foo:bool`; -val _ = test 25 true `foo:bool`; +val _ = in_repl_mode (test 25 false) `foo:bool`; +val _ = in_repl_mode (test 26 true) `foo:bool`; -val _ = test 27 false `^(concl TRUTH)`; -val _ = test 28 true `^(concl TRUTH)`; +val _ = in_repl_mode (test 28 false) `^(concl TRUTH)`; +val _ = in_repl_mode (test 29 true) `^(concl TRUTH)`; val t = concl TRUTH -val _ = test 32 false `^t`; -val _ = test 33 true `^t`; +val _ = in_repl_mode (test 33 false) `^t`; +val _ = in_repl_mode (test 34 true) `^t`; diff --git a/src/num/termination/selftest.sml b/src/num/termination/selftest.sml index e1d6635fbd..103138b4f8 100644 --- a/src/num/termination/selftest.sml +++ b/src/num/termination/selftest.sml @@ -77,15 +77,12 @@ fun tdefoutput_pp(th,thopt) = fun quietDefn f x = Lib.with_flag (Globals.interactive, false) f x -fun repl_mode f x = - Lib.with_flag (Globals.interactive, true) f x - val _ = shouldfail { checkexn = is_struct_HOL_ERR "TotalDefn", printarg = K "tDefine: no schematic defs when termination tac is supplied", printresult = tdefoutput_pp, - testfn = (fn q => repl_mode (TotalDefn.tDefine "foo" q) (WF_REL_TAC ‘$<’))} + testfn = (fn q => in_repl_mode (TotalDefn.tDefine "foo" q) (WF_REL_TAC ‘$<’))} ‘foo x = if x = 0 then y else foo(x - 1)*2’; val _ = @@ -93,7 +90,7 @@ val _ = { checkexn = is_struct_HOL_ERR "TotalDefn", printarg = K "qDefine: no schematic defs when termination tac is supplied", printresult = thm_to_string, - testfn = (fn q => repl_mode(TotalDefn.qDefine "foo" q) (SOME (WF_REL_TAC ‘$<’)))} + testfn = (fn q => in_repl_mode(TotalDefn.qDefine "foo" q) (SOME (WF_REL_TAC ‘$<’)))} ‘foo x = if x = 0 then y else foo(x - 1)*2’; fun lhs_has_two_args th = diff --git a/src/parse/testutils.sig b/src/parse/testutils.sig index a01161c27f..7f86727eec 100644 --- a/src/parse/testutils.sig +++ b/src/parse/testutils.sig @@ -27,6 +27,8 @@ val shouldfail : {testfn: 'a -> 'b, printresult: 'b -> string, printarg : 'a -> string, checkexn: exn -> bool} -> 'a -> unit +val in_repl_mode : ('a -> 'b) -> 'a -> 'b +val in_batch_mode : ('a -> 'b) -> 'a -> 'b val is_struct_HOL_ERR : string -> exn -> bool val check_HOL_ERRexn : (string * string * string -> bool) -> exn -> bool val check_HOL_ERR : (string * string * string -> bool) -> 'a testresult -> diff --git a/src/parse/testutils.sml b/src/parse/testutils.sml index 919d498b33..6399b9e1b3 100644 --- a/src/parse/testutils.sml +++ b/src/parse/testutils.sml @@ -229,6 +229,12 @@ fun convtest (nm,conv,tm,expected) = timed conv (exncheck c) tm end handle InternalDie p => pretty_die p +fun in_batch_mode f x = + Lib.with_flag (Globals.interactive, false) f x + +fun in_repl_mode f x = + Lib.with_flag (Globals.interactive, true) f x + fun check_HOL_ERRexn P e = case e of HOL_ERR(HOL_ERROR{origin_structure,origin_function,message,...}) => From 9430442da72851d39ff5e5852ff81e936e32804a Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Fri, 26 Sep 2025 03:15:27 -0500 Subject: [PATCH 10/13] overlooked --- src/IndDef/selftest.sml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/IndDef/selftest.sml b/src/IndDef/selftest.sml index 9110b6cfa0..c386db2218 100644 --- a/src/IndDef/selftest.sml +++ b/src/IndDef/selftest.sml @@ -85,8 +85,7 @@ val _ = tprint "Can still look at rule_induction data" val _ = if can ThmSetData.current_data{settype = "rule_induction"} then OK() else die "" - -val _ = shouldfail {testfn = quietly (xHol_reln "tr"), +val _ = shouldfail {testfn = quietly (in_repl_mode (xHol_reln "tr")), printresult = (fn (th,_,_) => thm_to_string th), printarg = K "With Unicode should fail", checkexn = is_struct_HOL_ERR "IndDefLib"} @@ -94,7 +93,7 @@ val _ = shouldfail {testfn = quietly (xHol_reln "tr"), (!x y. ▷ (SUC x) (SUC y) ==> ▷ x y)’ val _ = tprint "Vacuous clause failure" -val _ = if (Hol_reln `(!x. rel x Z) /\ (!x y. rel x y)` ; false) +val _ = if (in_repl_mode Hol_reln `(!x. rel x Z) /\ (!x y. rel x y)` ; false) handle HOL_ERR herr => String.isSuffix "Vacuous clause trivialises whole definition" @@ -102,7 +101,7 @@ val _ = if (Hol_reln `(!x. rel x Z) /\ (!x y. rel x y)` ; false) then OK() else die "FAILED" -val _ = shouldfail { testfn = quietly (xHol_reln "tr"), +val _ = shouldfail { testfn = quietly (in_repl_mode (xHol_reln "tr")), printresult = (fn (th,_,_) => thm_to_string th), printarg = K "Double implication should fail", checkexn = (fn(HOL_ERR herr) => From bd78bf5ad08a1c7d9b048cd2d0a55f3eac996efe Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Wed, 1 Oct 2025 01:01:47 -0500 Subject: [PATCH 11/13] modify hol_error representation to use a stack of origins --- src/1/Conv.sml | 87 ++++++++--------- src/1/Mutual.sml | 4 +- src/1/Tactical.sml | 15 +-- src/1/boolSyntax.sig | 2 - src/1/boolSyntax.sml | 8 +- src/HolSat/satTools.sml | 2 +- src/basicProof/BasicProvers.sml | 4 +- src/integer/CooperMath.sml | 2 +- src/integer/IntDP_Munge.sml | 2 +- src/n-bit/wordsLib.sml | 4 +- src/parse/Parse.sml | 4 +- src/parse/ParseDatatype.sml | 2 +- src/parse/testutils.sml | 11 +-- src/postkernel/HolKernel.sml | 1 + src/postkernel/Theory.sml | 7 +- src/prekernel/Feedback.sig | 29 +++--- src/prekernel/Feedback.sml | 160 +++++++++++++++++--------------- src/prekernel/Globals.sml | 12 --- src/simp/src/Cache.sml | 4 +- src/simp/src/Traverse.sml | 4 +- src/tfl/src/Defn.sml | 11 +-- src/unwind/unwindLib.sml | 2 +- 22 files changed, 189 insertions(+), 188 deletions(-) diff --git a/src/1/Conv.sml b/src/1/Conv.sml index 5601cc36f1..db82676ce0 100644 --- a/src/1/Conv.sml +++ b/src/1/Conv.sml @@ -13,10 +13,9 @@ (* TRANSLATOR : Konrad Slind, University of Calgary *) (* DATE : September 11, 1991 *) (* Many micro-optimizations added, February 24, 1992, KLS *) - (* ===================================================================== *) -structure Conv :> Conv = +structure Conv (* :> Conv *) = struct open HolKernel Parse boolTheory Drule boolSyntax Abbrev @@ -28,10 +27,12 @@ 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) | e => raise Fail (nm ^ ": " ^ General.exnMessage e) +*) (*----------------------------------------------------------------------* * Conversion for rewrite rules of the form |- !x1 ... xn. t == u * @@ -51,13 +52,13 @@ fun w nm c t = c t handle UNCHANGED => raise UNCHANGED fun REWR_CONV0 (part_matcher, fn_name) th = let val instth = part_matcher lhs th - handle e => - raise (wrap_exn "Conv" - (fn_name ^ ": bad theorem argument: " ^ - trace ("PP.avoid_unicode", 1) - term_to_string (concl th)) e) - in - fn tm => + handle e => raise + wrap_exn "Conv" + (String.concat + [fn_name, ": bad theorem argument: ", + trace ("PP.avoid_unicode", 1) + term_to_string (concl th)]) e + in fn tm => let val eqn = instth tm val l = lhs (concl eqn) @@ -69,7 +70,7 @@ fun REWR_CONV0 (part_matcher, fn_name) th = val REWR_CONV = REWR_CONV0 (PART_MATCH, "REWR_CONV") val HO_REWR_CONV = REWR_CONV0 (HO_PART_MATCH, "HO_REWR_CONV") -val REWR_CONV_A = REWR_CONV0 (PART_MATCH_A, "REWR_CONV_A") +val REWR_CONV_A = REWR_CONV0 (PART_MATCH_A, "REWR_CONV_A") (*----------------------------------------------------------------------* * RAND_CONV conv "t1 t2" applies conv to t2 * @@ -81,27 +82,28 @@ val REWR_CONV_A = REWR_CONV0 (PART_MATCH_A, "REWR_CONV_A") * now passes on information about nested failure * *----------------------------------------------------------------------*) -fun set_origin fnm (HOL_ERROR recd) = - let val {origin_structure, origin_function, source_location, message} = recd - in 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) - end +fun set_origin fnm holerr = + if Lib.mem (top_function_of holerr) + ["RAND_CONV", "RATOR_CONV", "ABS_CONV"] + andalso top_structure_of holerr = "Conv" + then set_top_function fnm holerr + else wrap_hol_error "Conv" fnm (top_location_of holerr) holerr 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 + conv Rand + handle HOL_ERR e => raise HOL_ERR (set_origin "RAND_CONV" e) in AP_TERM Rator newrand handle HOL_ERR e => - raise ERR "RAND_CONV" ("Application of AP_TERM failed: " ^ message_of e) + raise ERR "RAND_CONV" + ("Application of AP_TERM failed: " ^ message_of e) end + (*----------------------------------------------------------------------* * RATOR_CONV conv "t1 t2" applies conv to t1 * * * @@ -118,7 +120,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 HOL_ERR e => raise HOL_ERR (set_origin "RATOR_CONV" e) in AP_THM newrator Rand handle HOL_ERR e => @@ -141,8 +143,8 @@ fun LAND_CONV c = RATOR_CONV (RAND_CONV c) fun ABS_CONV conv tm = let - val (Bvar,Body) = - dest_abs tm handle HOL_ERR _ => raise ERR "ABS_CONV" "Term not an abstraction" + val (Bvar,Body) = dest_abs tm + handle HOL_ERR _ => raise ERR "ABS_CONV" "Term not an abstraction" val newbody = conv Body in ABS Bvar newbody @@ -159,7 +161,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 HOL_ERR e => raise HOL_ERR (set_origin "ABS_CONV" e) end (*----------------------------------------------------------------------* @@ -923,8 +925,8 @@ in end end handle e as HOL_ERR herr => - if structure_of herr = "Conv" andalso - function_of herr = "EXISTS_AND_CONV" then raise e + if top_structure_of herr = "Conv" andalso + top_function_of herr = "EXISTS_AND_CONV" then raise e else raise ERR "EXISTS_AND_CONV" "" end @@ -944,21 +946,20 @@ in let val (conj1, conj2) = dest_conj tm handle HOL_ERR _ => raise AE_ERR val (x, P) = dest_exists conj1 - handle HOL_ERR _ => raise AE_ERR + handle HOL_ERR _ => raise AE_ERR val (y, Q) = dest_exists conj2 - handle HOL_ERR_ => raise AE_ERR + handle HOL_ERR_ => raise AE_ERR in if not (aconv x y) then raise AE_ERR else if free_in x P orelse free_in x Q then raise ERR "AND_EXISTS_CONV" ("`" ^ (#1 (dest_var x)) ^ "` free in conjunct(s)") else SYM (EXISTS_AND_CONV - (mk_exists (x, - mk_conj (P, Q)))) + (mk_exists (x, mk_conj (P, Q)))) end handle e as HOL_ERR herr => - if structure_of herr = "Conv" andalso - function_of herr = "AND_EXISTS_CONV" then raise e + if top_structure_of herr = "Conv" andalso + top_function_of herr = "AND_EXISTS_CONV" then raise e else raise ERR "AND_EXISTS_CONV" "" end @@ -1098,8 +1099,8 @@ in end end handle e as HOL_ERR herr => - if structure_of herr = "Conv" andalso - function_of herr = "FORALL_OR_CONV" then raise e + if top_structure_of herr = "Conv" andalso + top_function_of herr = "FORALL_OR_CONV" then raise e else raise ERR "FORALL_OR_CONV" "" end @@ -1130,8 +1131,8 @@ in (mk_forall (x,mk_disj (P, Q)))) end handle e as HOL_ERR herr => - if structure_of herr = "Conv" andalso - function_of herr = "OR_FORALL_CONV" then raise e + if top_structure_of herr = "Conv" andalso + top_function_of herr = "OR_FORALL_CONV" then raise e else raise ERR "OR_FORALL_CONV" "" end @@ -1258,8 +1259,8 @@ in end end handle e as HOL_ERR herr => - if structure_of herr = "Conv" andalso - function_of herr = "FORALL_IMP_CONV" then raise e + if top_structure_of herr = "Conv" andalso + top_function_of herr = "FORALL_IMP_CONV" then raise e else raise ERR "FORALL_IMP_CONV" "" end @@ -1387,8 +1388,8 @@ in end end handle e as HOL_ERR herr => - if structure_of herr = "Conv" andalso - function_of herr = "EXISTS_IMP_CONV" then raise e + if top_structure_of herr = "Conv" andalso + top_function_of herr = "EXISTS_IMP_CONV" then raise e else raise ERR "EXISTS_IMP_CONV" "" end @@ -1502,8 +1503,8 @@ in end end handle e as HOL_ERR herr => - if structure_of herr = "Conv" andalso - function_of herr = "X_SKOLEM_CONV" then raise e + if top_structure_of herr = "Conv" andalso + top_function_of herr = "X_SKOLEM_CONV" then raise e else raise ERR "X_SKOLEM_CONV" "" end @@ -2324,7 +2325,7 @@ in if aconv cond T then SPEC rarm (SPEC larm (INST_TYPE' CT)) else if aconv cond F then SPEC rarm (SPEC larm (INST_TYPE' CF)) else if aconv larm rarm then SPEC larm (SPEC cond (INST_TYPE' COND_ID)) - else raise ERR "" "" + else raise HOL_ERR empty_hol_error end handle HOL_ERR _ => raise ERR "COND_CONV" "" end diff --git a/src/1/Mutual.sml b/src/1/Mutual.sml index 7e7a9f31db..340066904d 100644 --- a/src/1/Mutual.sml +++ b/src/1/Mutual.sml @@ -380,8 +380,8 @@ fun MUTUAL_INDUCT_THEN1 th = => raise ERR "MUTUAL_INDUCT_THEN" "tactic application error" end handle (e as HOL_ERR herr) => - if structure_of herr = "Mutual" andalso - function_of herr = "MUTUAL_INDUCT_THEN" then + if top_structure_of herr = "Mutual" andalso + top_function_of herr = "MUTUAL_INDUCT_THEN" then raise e else raise ILL_FORMED | otherwise => raise ILL_FORMED diff --git a/src/1/Tactical.sml b/src/1/Tactical.sml index 938eaf8954..d3641933aa 100644 --- a/src/1/Tactical.sml +++ b/src/1/Tactical.sml @@ -54,7 +54,7 @@ local f (t, tac) handle e as HOL_ERR herr => let val m = message_of herr - val f = function_of herr + val f = top_function_of herr in mesg ("Proof of \n\n" ^ Parse.term_to_string t ^ "\n\nfailed.\n") ; @@ -231,12 +231,13 @@ val op >- = op THEN1 fun op>>-(tac1, n) tac2 g = op>- (tac1, tac2) g - handle e as HOL_ERR er => - if is_substring "THEN1" (message_of er) then raise e + handle e as HOL_ERR holerr => + if is_substring "THEN1" (message_of holerr) then raise e else - raise HOL_ERR - (set_message - (message_of er ^ " (THEN1 on line "^Int.toString n^")") er) + raise HOL_ERR (set_message + (String.concat + [message_of holerr, + " (THEN1 on line ", Int.toString n, ")"]) holerr) fun (f ?? x) = f x @@ -884,7 +885,7 @@ local (gl, (if is_neg w then NEG_DISCH ant else DISCH ant) o prf) end handle HOL_ERR e => - raise ERR "DISCH_THEN" (function_of e ^ ":" ^ message_of e) + raise ERR "DISCH_THEN" (top_function_of e ^ ":" ^ message_of e) 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/1/boolSyntax.sig b/src/1/boolSyntax.sig index fa3657d92f..f648ac2024 100644 --- a/src/1/boolSyntax.sig +++ b/src/1/boolSyntax.sig @@ -217,6 +217,4 @@ sig val sep_type_unify : hol_type -> hol_type -> (hol_type, hol_type) Lib.subst * (hol_type, hol_type) Lib.subst - - end diff --git a/src/1/boolSyntax.sml b/src/1/boolSyntax.sml index 6e8abb5950..e1caf0bd74 100644 --- a/src/1/boolSyntax.sml +++ b/src/1/boolSyntax.sml @@ -14,8 +14,9 @@ struct open Feedback Lib HolKernel boolTheory; +type goal = term list * term + val ERR = mk_HOL_ERR "boolSyntax" -type goal = term list * term (*--------------------------------------------------------------------------- Basic constants @@ -321,6 +322,7 @@ fun remove_junk cstr cnm junkas attrs0 = end val _ = List.app ThmAttribute.reserve_word ["notuserdef"] + fun new_thm_with_attributes {call_str, call_f} genth (s, arg) = let open ThmAttribute val {thmname=s0,reserved=R,unknown=U,attrs=attrs} = @@ -330,7 +332,7 @@ fun new_thm_with_attributes {call_str, call_f} genth (s, arg) = ["local", "schematic", "nocompute", "unlisted"] R val _ = null R orelse - raise mk_HOL_ERR "boolSyntax" call_str + raise mk_HOL_ERR "boolSyntax" call_f ("Unhandled reserved attribute(s): " ^ String.concatWith ", " (map #1 R)) val attrs = if notuserdefp orelse not (is_attribute "userdef") orelse @@ -645,7 +647,6 @@ in fun gen_tyvarify tm = Term.inst (gen_tyvar_sigma (type_vars_in_term tm)) tm - end (* ---------------------------------------------------------------------- @@ -673,5 +674,4 @@ fun tmx_eq (tm1,x1) (tm2,x2) = x1 = x2 andalso Term.aconv tm1 tm2 fun xtm_eq (x1,tm1) (x2,tm2) = x1 = x2 andalso Term.aconv tm1 tm2 end - end diff --git a/src/HolSat/satTools.sml b/src/HolSat/satTools.sml index 3d61f14cba..229a030b66 100644 --- a/src/HolSat/satTools.sml +++ b/src/HolSat/satTools.sml @@ -124,7 +124,7 @@ fun satCheck model t = end handle Interrupt => raise Interrupt | HOL_ERR herr => - if function_of herr = "EQT_ELIM" andalso is_neg t then + if top_function_of herr = "EQT_ELIM" andalso is_neg t then (UNDISCH (EQF_ELIM (REWRITE_CONV [] t)) handle HOL_ERR _ => raise satCheckError) else raise satCheckError diff --git a/src/basicProof/BasicProvers.sml b/src/basicProof/BasicProvers.sml index ce99f70b9c..ea04a2ceb0 100644 --- a/src/basicProof/BasicProvers.sml +++ b/src/basicProof/BasicProvers.sml @@ -612,7 +612,7 @@ fun by0 k (q, tac) (g as (asl,w)) = let in (SUBGOAL_THEN tm finisher gTHEN1 (tac THEN k)) g handle HOL_ERR _ => - raise ERR "by" ("by's tactic failed to prove subgoal"^mk_errmsg()) + raise ERR "by" ("by's tactic failed to prove subgoal"^mk_errmsg()) end val op by = by0 NO_TAC @@ -621,7 +621,7 @@ 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 herr => - if function_of herr = "Q_TAC" then raise e + if top_function_of herr = "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 61c4cf0304..53fd2a7293 100644 --- a/src/integer/CooperMath.sml +++ b/src/integer/CooperMath.sml @@ -535,7 +535,7 @@ local EQT_ELIM (AC_CONV (INT_MUL_ASSOC, INT_MUL_SYM) (mk_eq(tm, mk_mult(list_mk_mult rest, var)))) end handle (e as HOL_ERR herr) => - (if structure_of herr = "Lib" then + (if top_structure_of herr = "Lib" then ALL_CONV tm else raise e) else if is_comb tm then diff --git a/src/integer/IntDP_Munge.sml b/src/integer/IntDP_Munge.sml index ca84f7070e..384919f7a8 100644 --- a/src/integer/IntDP_Munge.sml +++ b/src/integer/IntDP_Munge.sml @@ -237,7 +237,7 @@ in else ALL_CONV end tm handle (e as HOL_ERR herr) => - if function_of herr = "REWR_CONV" then + if top_function_of herr = "REWR_CONV" then raise ERR "IntDP_Munge" "Uneliminable natural number term remains" else raise e diff --git a/src/n-bit/wordsLib.sml b/src/n-bit/wordsLib.sml index 14a5f34a02..0c6e90ef22 100644 --- a/src/n-bit/wordsLib.sml +++ b/src/n-bit/wordsLib.sml @@ -1534,7 +1534,7 @@ fun WORD_SUB_CONV tm = THENC PURE_REWRITE_CONV [WORD_SUB_INTRO, WORD_NEG_SUB, WORD_SUB_RNEG, WORD_NEG_NEG, WORD_MULT_CLAUSES, NEG1_WORD1]) tm handle (e as HOL_ERR herr) => - if function_of herr = "CHANGED_CONV" + if top_function_of herr = "CHANGED_CONV" then raise Conv.UNCHANGED else raise e @@ -1830,7 +1830,7 @@ fun WORD_BIT_INDEX_CONV toindex = Drule.ISPEC w (Drule.MATCH_MP thm lt) end handle e as HOL_ERR herr => - if function_of herr = "EQT_ELIM" then + if top_function_of herr = "EQT_ELIM" then raise ERR "WORD_BIT_INDEX_CONV" "index too large" else raise e end diff --git a/src/parse/Parse.sml b/src/parse/Parse.sml index 85038b8f2b..bc48bb1403 100644 --- a/src/parse/Parse.sml +++ b/src/parse/Parse.sml @@ -4,6 +4,8 @@ struct open Feedback HolKernel HOLgrammars GrammarSpecials term_grammar type_grammar open term_grammar_dtype +val _ = print "Loading Parse structure.\n" + type pp_element = term_grammar.pp_element type PhraseBlockStyle = term_grammar.PhraseBlockStyle type ParenStyle = term_grammar.ParenStyle @@ -587,7 +589,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 HOL_ERR e => raise HOL_ERR (set_top_function 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 a156083c9c..eee10e379f 100644 --- a/src/parse/ParseDatatype.sml +++ b/src/parse/ParseDatatype.sml @@ -272,7 +272,7 @@ fun parse_harg G qb = else (parse_atom G qb handle e as HOL_ERR herr => - if structure_of herr = "Parse" then + if top_structure_of herr = "Parse" then raise ERR "parse_harg" (message_of herr) else raise e) | (base_tokens.BT_AQ ty, _) => (qbuf.advance qb; dAQ ty) diff --git a/src/parse/testutils.sml b/src/parse/testutils.sml index 6399b9e1b3..5af7627bdf 100644 --- a/src/parse/testutils.sml +++ b/src/parse/testutils.sml @@ -236,20 +236,19 @@ fun in_repl_mode f x = Lib.with_flag (Globals.interactive, true) f x fun check_HOL_ERRexn P e = - case e of - HOL_ERR(HOL_ERROR{origin_structure,origin_function,message,...}) => - P (origin_structure, origin_function, message) - | _ => false + case e of + HOL_ERR holerr => + P (top_structure_of holerr, top_function_of holerr, message_of holerr) + | other_exn => 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 - - fun require_msgk P pr f k x = let open HOLPP diff --git a/src/postkernel/HolKernel.sml b/src/postkernel/HolKernel.sml index a789d9ff34..1948c99b3c 100644 --- a/src/postkernel/HolKernel.sml +++ b/src/postkernel/HolKernel.sml @@ -768,4 +768,5 @@ val sort_vars = Portable.pull_prefix o map (fn n => equal n o #1 o dest_var) end + end diff --git a/src/postkernel/Theory.sml b/src/postkernel/Theory.sml index 4f20f6a998..7507e04ced 100644 --- a/src/postkernel/Theory.sml +++ b/src/postkernel/Theory.sml @@ -1239,14 +1239,15 @@ fun located_new_definition0 fnm {name,def=M,loc} = gen_store_definition (name, post(V,def_th),loc) before call_hooks (TheoryDelta.NewConstant{Name=Name, Thy=Thy}) end - handle e => raise (wrap_exn "Definition" fnm e); + handle e => raise wrap_exn "Definition" fnm e +; + val located_new_definition = located_new_definition0 "located_new_definition" + fun new_definition(n,def_t) = located_new_definition0 "new_definition" {loc=Unknown,def=def_t,name=n} - - end (* Definition struct *) end (* Theory *) diff --git a/src/prekernel/Feedback.sig b/src/prekernel/Feedback.sig index a1b8725139..458be1345f 100644 --- a/src/prekernel/Feedback.sig +++ b/src/prekernel/Feedback.sig @@ -1,28 +1,35 @@ signature Feedback = sig - datatype hol_error = HOL_ERROR of - {origin_structure : string, - origin_function : string, - source_location : locn.locn, - message : string} + + type origin = + {origin_structure:string, + origin_function:string, + source_location : locn.locn} + + datatype hol_error = + HOL_ERROR of + {origins : origin list, + message : string} val mk_hol_error : string -> string -> locn.locn -> string -> hol_error - val dest_hol_error : hol_error -> string * string * locn.locn * string + val wrap_hol_error : string -> string -> locn.locn -> hol_error -> hol_error val empty_hol_error : hol_error - val structure_of : hol_error -> string - val function_of : hol_error -> string - val location_of : hol_error -> locn.locn + val top_structure_of: hol_error -> string + val top_function_of : hol_error -> string + val top_location_of : hol_error -> locn.locn + val origins_of : hol_error -> origin list val message_of : hol_error -> string val set_message : string -> hol_error -> hol_error - val set_origin_function : string -> hol_error -> hol_error + val set_top_function : string -> hol_error -> hol_error val pp_hol_error : hol_error -> HOLPP.pretty exception HOL_ERR of hol_error exception BATCH_ERR of string - val render_exn : string -> exn -> 'a val mk_HOL_ERR : string -> string -> string -> exn val mk_HOL_ERRloc : string -> string -> locn.locn -> string -> exn + + val render_exn : string -> exn -> 'a val wrap_exn : string -> string -> exn -> exn val wrap_exn_loc : string -> string -> locn.locn -> exn -> exn diff --git a/src/prekernel/Feedback.sml b/src/prekernel/Feedback.sml index bd3fc9a27d..7152abae50 100644 --- a/src/prekernel/Feedback.sml +++ b/src/prekernel/Feedback.sml @@ -13,94 +13,109 @@ struct local open HOLPP in end +type origin = + {origin_structure:string, + origin_function:string, + source_location : locn.locn} + +fun mk_origin s1 s2 loc = + {origin_structure = s1, + origin_function = s2, + source_location = loc} + datatype hol_error = HOL_ERROR of - {origin_structure : string, - origin_function : string, - source_location : locn.locn, - message : string} + {origins : origin list, + message : string} fun mk_hol_error s1 s2 loc mesg = HOL_ERROR - {origin_structure = s1, - origin_function = s2, - source_location = loc, - message = mesg} + {origins = [mk_origin s1 s2 loc], + message = mesg} -val empty_hol_error = mk_hol_error "" "" locn.Loc_None "" +fun wrap_hol_error s f l (HOL_ERROR {origins,message}) = + HOL_ERROR + {origins = mk_origin s f l::origins, + message = message} -fun dest_hol_error (HOL_ERROR recd) = - let val {origin_structure, origin_function, source_location, message} = recd - in (origin_structure, origin_function, source_location, message) - end +val empty_hol_error = + HOL_ERROR + {origins = [], message = ""} + +fun empty_origins_error sfn = + HOL_ERROR + {origins = [mk_origin "Feedback" sfn locn.Loc_Unknown], + message = "no origin"} + +(*-------------------------------------------------------------------------*) +(* Exceptions used in HOL code. *) +(*---------------------------------------------------------------------------*) + +exception HOL_ERR of hol_error; + +exception BATCH_ERR of string; -fun structure_of (HOL_ERROR {origin_structure,...}) = origin_structure -fun function_of (HOL_ERROR {origin_function,...}) = origin_function -fun location_of (HOL_ERROR {source_location,...}) = source_location +fun origins_of (HOL_ERROR {origins,...}) = origins fun message_of (HOL_ERROR {message,...}) = message -fun pp_hol_error (err as HOL_ERROR recd) = +fun top_structure_of herr = + case origins_of herr + of [] => raise HOL_ERR (empty_origins_error "top_structure_of") + | h::_ => #origin_structure h + +fun top_function_of herr = + case origins_of herr + of [] => raise HOL_ERR (empty_origins_error "top_function_of") + | h::_ => #origin_function h + +fun top_location_of herr = + case origins_of herr + of [] => raise HOL_ERR (empty_origins_error "top_location_of") + | h::_ => #source_location h + +val pp_hol_error = let open HOLPP - val {origin_structure, origin_function, source_location, message} = recd - in if err = empty_hol_error then + fun pp_origin {origin_structure,origin_function,source_location} = + block INCONSISTENT 2 + ([add_string "at ", + add_string (origin_structure^"."^origin_function),add_string ":"] + @ + (case source_location + of locn.Loc_Unknown => [] + | _ => [add_break(1,0), + add_string (locn.toString source_location ^":")])) + in + fn (err as HOL_ERROR{origins,message}) => + if err = empty_hol_error then add_string "" else - block INCONSISTENT 0 (List.concat [ - [add_string "at ", - add_string (origin_structure^"."^origin_function),add_string ":", - add_break(1,0)], - (case source_location - of locn.Loc_Unknown => [] - | _ => [add_string (locn.toString source_location ^":"),add_break(1,0)]), - [add_string message] - ]) + block INCONSISTENT 2 + (pr_list pp_origin [NL] origins @ [NL, add_string message]) end -fun format_err_recd recd = - HOLPP.pp_to_string (!Globals.linewidth) pp_hol_error (HOL_ERROR recd) +fun format_hol_error holerr = + HOLPP.pp_to_string (!Globals.linewidth) pp_hol_error holerr val _ = let fun pp i _ e = pp_hol_error e in PolyML.addPrettyPrinter pp end -(*---------------------------------------------------------------------------*) -(* Exceptions used in HOL code. *) -(*---------------------------------------------------------------------------*) - -exception HOL_ERR of hol_error; - -exception BATCH_ERR of string; - -(*--------------------------------------------------------------------------- - Curried version of HOL_ERR; can be more comfortable to use. - ---------------------------------------------------------------------------*) - fun mk_HOL_ERRloc s1 s2 locn s3 = HOL_ERR (mk_hol_error s1 s2 locn s3) fun mk_HOL_ERR s1 s2 s3 = HOL_ERR (mk_hol_error s1 s2 locn.Loc_Unknown s3) -(* Errors with a known location. *) - -fun set_origin_function fnm (HOL_ERROR recd) = - let val {origin_structure, source_location, message, ...} = recd - in HOL_ERROR - {origin_structure = origin_structure, - source_location = source_location, - origin_function = fnm, +fun set_top_function fnm (HOL_ERROR {origins,message}) = + case origins + of [] => raise HOL_ERR (empty_origins_error "set_origin_function") + | h::t => HOL_ERROR + {origins = {origin_structure = #origin_structure h, + source_location = #source_location h, + origin_function = fnm} :: t, message = message} - end - -fun set_message msg (HOL_ERROR recd) = - let val{origin_structure, source_location, origin_function, ...} = recd - in HOL_ERROR - {origin_structure = origin_structure, - source_location = source_location, - origin_function = origin_function, - message = msg} - end -fun format_hol_error(HOL_ERROR recd) = format_err_recd recd +fun set_message msg (HOL_ERROR {origins,message}) = + HOL_ERROR {origins = origins, message = msg} val ERR = mk_HOL_ERR "Feedback" (* local to this file *) @@ -141,8 +156,8 @@ fun quiet_messages f = Portable.with_flag (emit_MESG, false) f * Formatting and output for exceptions, messages, and warnings. * *---------------------------------------------------------------------------*) -fun format_ERR (HOL_ERROR recd) = - String.concat ["\nException raised ", format_err_recd recd, "\n"] +fun format_ERR holerr = + String.concat ["\nException raised ", format_hol_error holerr, "\n"] fun format_MESG s = String.concat ["<>\n"] @@ -189,20 +204,17 @@ in end (*--------------------------------------------------------------------------- - Takes an exception, grabs its message as best as possible, then - make a HOL exception out of it. Subtlety: if we see that the - exception is an Interrupt, we raise it. + Support for backtracing exceptions, treating HOL_ERR specially. + Subtlety: if we see that the exception is an Interrupt, we raise it. ---------------------------------------------------------------------------*) -fun wrap_exn s f Portable.Interrupt = raise Portable.Interrupt - | wrap_exn s f (HOL_ERR (HOL_ERROR recd)) = - mk_HOL_ERR s f (format_err_recd recd) - | wrap_exn s f exn = mk_HOL_ERR s f (General.exnMessage exn) +fun wrap_exn_loc s f l e = + case e + of Portable.Interrupt => raise Portable.Interrupt + | HOL_ERR holerr => HOL_ERR (wrap_hol_error s f l holerr) + | exn => mk_HOL_ERRloc s f l (General.exnMessage exn) -fun wrap_exn_loc s f l Portable.Interrupt = raise Portable.Interrupt - | wrap_exn_loc s f l (HOL_ERR (HOL_ERROR recd)) = - mk_HOL_ERRloc s f l (format_err_recd recd) - | wrap_exn_loc s f l exn = mk_HOL_ERRloc s f l (General.exnMessage exn) +fun wrap_exn s f = wrap_exn_loc s f locn.Loc_Unknown fun HOL_MESG s = if !emit_MESG then !MESG_outstream (!MESG_to_string s) else () diff --git a/src/prekernel/Globals.sml b/src/prekernel/Globals.sml index 45a5f0425d..90b18692f4 100644 --- a/src/prekernel/Globals.sml +++ b/src/prekernel/Globals.sml @@ -49,18 +49,6 @@ val show_axioms = ref true val show_scrub = ref true -(*---------------------------------------------------------------------------* - * Assignable function for printing errors. * - *---------------------------------------------------------------------------*) - -fun outHOL_ERR_default {message,origin_function,origin_structure} = - (TextIO.output (TextIO.stdOut, - "\nException raised at " ^ origin_structure ^ "." ^ - origin_function ^ ":\n" ^ message ^ "\n") - ; TextIO.flushOut TextIO.stdOut) - -val output_HOL_ERR = ref outHOL_ERR_default - (*---------------------------------------------------------------------------* * Prettyprinting flags * *---------------------------------------------------------------------------*) diff --git a/src/simp/src/Cache.sml b/src/simp/src/Cache.sml index 8bf7d76840..d8d8eb56d3 100644 --- a/src/simp/src/Cache.sml +++ b/src/simp/src/Cache.sml @@ -1,8 +1,8 @@ structure Cache :> Cache = struct -open HolKernel liteLib Trace Abbrev boolSyntax boolLib - +open HolKernel liteLib Abbrev boolSyntax boolLib +open Trace type key = term type hypinfo = {hyps : term HOLset.set, thms : term HOLset.set} diff --git a/src/simp/src/Traverse.sml b/src/simp/src/Traverse.sml index f5a997e64d..4d37d90363 100644 --- a/src/simp/src/Traverse.sml +++ b/src/simp/src/Traverse.sml @@ -184,8 +184,8 @@ fun FIRSTCQC_CONV [] t = failwith "no conversion worked" in c t handle e as HOL_ERR herr => - if structure_of herr = "Opening" andalso - function_of herr = "CONGPROC" andalso + if top_structure_of herr = "Opening" andalso + top_function_of herr = "CONGPROC" andalso message_of herr = "Congruence gives no change" then raise e else FIRSTCQC_CONV cs t diff --git a/src/tfl/src/Defn.sml b/src/tfl/src/Defn.sml index 904634322a..90cebd65ba 100644 --- a/src/tfl/src/Defn.sml +++ b/src/tfl/src/Defn.sml @@ -1237,14 +1237,6 @@ fun stdrec_defn (facts,(stem,stem'),wfrec_res,untuple) = in TotalDefn. ---------------------------------------------------------------------------*) -fun holexnMessage (HOL_ERR (HOL_ERROR recd)) = - let val {origin_structure,origin_function,source_location,message} = recd - in String.concat - [origin_structure, ".", origin_function, ":", - locn.toShortString source_location, ": ", message] - end - | holexnMessage e = General.exnMessage e - fun is_simple_arg t = is_var t orelse (case Lib.total dest_pair t of @@ -1271,8 +1263,7 @@ fun prim_mk_defn stem eqns = List.all is_simple_arg args then (* not recursive, yet failed *) - raise err ("Simple definition failed with message: "^ - holexnMessage e) + raise wrap_exn "Defn" "prim_mk_defn (simple definition)" e else let val (tup_eqs, stem', untuple) = pairf (stem, eqns) diff --git a/src/unwind/unwindLib.sml b/src/unwind/unwindLib.sml index 0586322264..80784a6782 100644 --- a/src/unwind/unwindLib.sml +++ b/src/unwind/unwindLib.sml @@ -117,7 +117,7 @@ fun CONJ_FORALL_ONCE_CONV t = end end handle (e as HOL_ERR herr) => - if function_of herr = "CONJ_FORALL_ONCE_CONV" then + if top_function_of herr = "CONJ_FORALL_ONCE_CONV" then raise e else raise UNWIND_ERR "CONJ_FORALL_ONCE_CONV" "" end; From 66d7ab37dbdf313d99450a5e438c1fc0527f0054 Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Thu, 25 Sep 2025 03:07:47 -0500 Subject: [PATCH 12/13] [HOL_ERROR] - modify HOL_ERR representation to use a stack of origins - more pursuit of nice error messages coming from Modern Syntax --- examples/arm/v7/arm_parserLib.sml | 8 ++--- examples/arm/v7/arm_random_testingLib.sml | 2 +- .../l3-machine-code/arm/step/arm_stepLib.sml | 4 +-- .../cheri/step/cheri_stepLib.sml | 8 +++-- examples/l3-machine-code/common/Import.sml | 6 ++-- examples/l3-machine-code/common/stateLib.sml | 10 +++--- examples/l3-machine-code/common/utilsLib.sml | 2 +- .../l3-machine-code/m0/step/m0_stepLib.sml | 6 ++-- .../mips/step/mips_stepLib.sml | 2 +- .../riscv/step/riscv_stepLib.sml | 4 ++- src/HolSmt/selftest.sml | 32 ++++++++----------- src/boss/selftest.sml | 6 ++-- src/floating-point/binary_ieeeLib.sml | 2 +- src/integer/selftest.sml | 4 +-- src/n-bit/selftest.sml | 2 +- src/prekernel/Feedback.sml | 21 ++++++------ src/proofman/tests/selftest.sml | 6 +++- src/tactictoe/src/tttEval.sml | 27 +++++++++------- src/tfl/src/selftest.sml | 4 +-- 19 files changed, 82 insertions(+), 74 deletions(-) diff --git a/examples/arm/v7/arm_parserLib.sml b/examples/arm/v7/arm_parserLib.sml index 1b34876481..85d25328e9 100644 --- a/examples/arm/v7/arm_parserLib.sml +++ b/examples/arm/v7/arm_parserLib.sml @@ -1248,12 +1248,12 @@ fun mode1_immediate1 thumb m i = (dp_opcode m,int_to_thumb2_mode1_immediate i) handle HOL_ERR herr => (dp_opcode (swap_opcode m),int_to_thumb2_mode1_immediate (int_one_comp i)) - handle HOL_ERR _ => raise ERR (function_of herr) (message_of herr) + handle HOL_ERR _ => raise ERR (top_function_of herr) (message_of herr) else (dp_opcode m,int_to_mode1_immediate i) handle HOL_ERR herr => (dp_opcode (swap_opcode m),int_to_mode1_immediate (int_one_comp i)) - handle HOL_ERR _ => raise ERR (function_of herr) (message_of herr); + handle HOL_ERR _ => raise ERR (top_function_of herr) (message_of herr); fun mode1_immediate2 thumb m i = if thumb then @@ -1261,13 +1261,13 @@ fun mode1_immediate2 thumb m i = handle HOL_ERR herr => (dp_opcode (swap_opcode m), int_to_thumb2_mode1_immediate (intSyntax.mk_negated i)) - handle HOL_ERR _ => raise ERR (function_of herr) (message_of herr) + handle HOL_ERR _ => raise ERR (top_function_of herr) (message_of herr) else (dp_opcode m,int_to_mode1_immediate i) handle HOL_ERR herr => (dp_opcode (swap_opcode m), int_to_mode1_immediate (intSyntax.mk_negated i)) - handle HOL_ERR _ => raise ERR (function_of herr) (message_of herr) + handle HOL_ERR _ => raise ERR (top_function_of herr) (message_of herr) fun mode1_register rm = mk_Mode1_register (mk_word5 0,mk_word2 0,rm); diff --git a/examples/arm/v7/arm_random_testingLib.sml b/examples/arm/v7/arm_random_testingLib.sml index 40a9ed3304..32cab3cd27 100644 --- a/examples/arm/v7/arm_random_testingLib.sml +++ b/examples/arm/v7/arm_random_testingLib.sml @@ -816,7 +816,7 @@ local in (e,a ^ w,b) end handle HOL_ERR e => - (HOL_WARNING (structure_of e) (function_of e) + (HOL_WARNING (top_structure_of e) (top_function_of e) (String.concat [Hol_pp.term_to_string enc, ": ", Hol_pp.term_to_string tm, "\n"]); diff --git a/examples/l3-machine-code/arm/step/arm_stepLib.sml b/examples/l3-machine-code/arm/step/arm_stepLib.sml index a602573d27..4887cedc4d 100644 --- a/examples/l3-machine-code/arm/step/arm_stepLib.sml +++ b/examples/l3-machine-code/arm/step/arm_stepLib.sml @@ -2584,7 +2584,7 @@ in handle (e as HOL_ERR herr) => if message_of herr = "not found" then raise Conv.UNCHANGED else - if function_of herr = "singleton_of_list" then + if top_function_of herr = "singleton_of_list" then raise ERR "arm_decode" "more than one matching decode pattern" else raise e val FALL_CONV = @@ -4180,7 +4180,7 @@ in ; raise ERR "eval" "more than one valid step theorem")) handle (e as HOL_ERR herr) => if message_of herr = "not found" andalso - function_of herr = "find_rw" then + top_function_of herr = "find_rw" then raise (Parse.print_term tm ; print "\n" ; ERR "eval" "instruction instance not supported") diff --git a/examples/l3-machine-code/cheri/step/cheri_stepLib.sml b/examples/l3-machine-code/cheri/step/cheri_stepLib.sml index 3267e98334..c7b579e9dc 100644 --- a/examples/l3-machine-code/cheri/step/cheri_stepLib.sml +++ b/examples/l3-machine-code/cheri/step/cheri_stepLib.sml @@ -350,9 +350,11 @@ in | [x, _] => x (* ignore exception case *) | l => (List.app (fn x => (Parse.print_thm x; print "\n")) l ; err "more than one valid step theorem")) - handle HOL_ERR {message = "not found", - origin_function = "find_rw", ...} => - err "instruction instance not supported" + handle e as HOL_ERR holerr => + if message_of holerr = "not found" andalso + top_function_of holerr = "find_rw" + then err "instruction instance not supported" + else raise e end end diff --git a/examples/l3-machine-code/common/Import.sml b/examples/l3-machine-code/common/Import.sml index 083ba7cc41..ad4022557d 100644 --- a/examples/l3-machine-code/common/Import.sml +++ b/examples/l3-machine-code/common/Import.sml @@ -237,7 +237,7 @@ fun Call (f, ty, tm) = val typ = Type.--> (Term.type_of tm, Ty ty) val vc = mk_local_const (f, typ) handle (e as HOL_ERR herr) => - if function_of herr = "mk_thy_const" then + if top_function_of herr = "mk_thy_const" then Term.mk_var (f, typ) (* for recursion *) else raise e in @@ -252,7 +252,7 @@ fun Const (c, ty) = in mk_local_const (c, typ) handle (e as HOL_ERR herr) => - if function_of herr = "mk_thy_const" then + if top_function_of herr = "mk_thy_const" then Term.mk_var (c, typ) (* for recursion *) else raise e end @@ -313,7 +313,7 @@ fun CS (x, cs) = fun Let (v,e,b) = boolSyntax.mk_let (Close (v, b), e) handle HOL_ERR herr => - if function_of herr = "mk_pabs" then + if top_function_of herr = "mk_pabs" then CS (e, [(v, b)]) else raise HOL_ERR herr diff --git a/examples/l3-machine-code/common/stateLib.sml b/examples/l3-machine-code/common/stateLib.sml index eff088415b..fae1d9b9d3 100644 --- a/examples/l3-machine-code/common/stateLib.sml +++ b/examples/l3-machine-code/common/stateLib.sml @@ -232,7 +232,7 @@ in |> boolSyntax.rhs |> pred_setSyntax.strip_set |> List.hd val tm_thm = (REWRITE_CONV thms THENC Conv.CHANGED_CONV EVAL) tm handle (e as HOL_ERR herr) => - if function_of herr = "CHANGED_CONV" then + if top_function_of herr = "CHANGED_CONV" then combinTheory.I_THM else raise e in @@ -840,7 +840,7 @@ in | NONE => default (f_upd, l, p, q)) | (s, l) => default (s, l, p, q) : (term list * term list)) handle (e as HOL_ERR herr) => - if function_of herr = "dest_thy_const" then + if top_function_of herr = "dest_thy_const" then (p, q) else raise e in @@ -1454,7 +1454,7 @@ fun chunks_intro_pre_process m_def = PURE_REWRITE_RULE rwts thm end handle (e as HOL_ERR herr) => - if function_of herr = "EQT_ELIM" then thm else raise e + if top_function_of herr = "EQT_ELIM" then thm else raise e end end @@ -1474,7 +1474,7 @@ fun chunks_intro be m_def = else helperLib.PRE_POST_RULE cnv (Thm.INST (List.concat s) thm) end handle (e as HOL_ERR herr) => - if function_of herr = "group_into_n" andalso + if top_function_of herr = "group_into_n" andalso message_of herr = "too few" then thm else raise e @@ -1578,7 +1578,7 @@ in end end handle (e as HOL_ERR herr) => - if function_of herr = "group_into_n" andalso + if top_function_of herr = "group_into_n" andalso message_of herr = "too few" then thm else raise e diff --git a/examples/l3-machine-code/common/utilsLib.sml b/examples/l3-machine-code/common/utilsLib.sml index f3ed611722..5cc294ac50 100644 --- a/examples/l3-machine-code/common/utilsLib.sml +++ b/examples/l3-machine-code/common/utilsLib.sml @@ -1212,7 +1212,7 @@ local in List.map (fn x => Term.mk_comb (t, x) handle (e as HOL_ERR herr) => - if function_of herr = "mk_comb" then + if top_function_of herr = "mk_comb" then (Parse.print_term t; print "\n"; Parse.print_term x; raise ERR "buildAst" "") else raise e) l diff --git a/examples/l3-machine-code/m0/step/m0_stepLib.sml b/examples/l3-machine-code/m0/step/m0_stepLib.sml index dc91e5dbe7..79c2354cfb 100644 --- a/examples/l3-machine-code/m0/step/m0_stepLib.sml +++ b/examples/l3-machine-code/m0/step/m0_stepLib.sml @@ -1195,7 +1195,7 @@ in state_with_pcinc ``2w:word32`` :: fst (Term.match_term v1 pat)) handle (e as HOL_ERR herr) => if message_of herr = "different constructors" andalso - function_of herr = "raw_match_term" then + top_function_of herr = "raw_match_term" then (DecodeThumb2, state_with_pcinc ``4w:word32`` :: fst (Term.match_term v2 pat)) else raise e @@ -1919,7 +1919,7 @@ in ; raise ERR "eval" "more than one valid step theorem")) handle (e as HOL_ERR herr) => if message_of herr = "not found" andalso - function_of herr = "find_rw" then + top_function_of herr = "find_rw" then raise (Parse.print_term tm ; print "\n" ; ERR "eval" "instruction instance not supported") @@ -1970,7 +1970,7 @@ in REWRITE_RULE ineq_hyps thm4) val r = get_state thm4 handle (e as HOL_ERR herr) => - if function_of herr = "dest_pair" then + if top_function_of herr = "dest_pair" then (Parse.print_thm thm4 ; print "\n" ; raise ERR "eval_thumb" "failed to fully evaluate") diff --git a/examples/l3-machine-code/mips/step/mips_stepLib.sml b/examples/l3-machine-code/mips/step/mips_stepLib.sml index e9d9505c45..c34c276bb8 100644 --- a/examples/l3-machine-code/mips/step/mips_stepLib.sml +++ b/examples/l3-machine-code/mips/step/mips_stepLib.sml @@ -1094,7 +1094,7 @@ in ; err "more than one valid step theorem")) handle (e as HOL_ERR herr) => if message_of herr = "not found" andalso - function_of herr = "find_rw" + top_function_of herr = "find_rw" then err "instruction instance not supported" else raise e end diff --git a/examples/l3-machine-code/riscv/step/riscv_stepLib.sml b/examples/l3-machine-code/riscv/step/riscv_stepLib.sml index 794cda036e..60b1691a88 100644 --- a/examples/l3-machine-code/riscv/step/riscv_stepLib.sml +++ b/examples/l3-machine-code/riscv/step/riscv_stepLib.sml @@ -278,7 +278,9 @@ in | [x] => x | l => List.last (mlibUseful.sort_map neg_count Int.compare l)) handle (e as HOL_ERR herr) => - if message_of herr = "not found" andalso function_of herr = "find_rw" then + if message_of herr = "not found" andalso + top_function_of herr = "find_rw" + then err tm "instruction instance not supported" else raise e end diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml index 49af909f52..1834927a56 100644 --- a/src/HolSmt/selftest.sml +++ b/src/HolSmt/selftest.sml @@ -49,15 +49,12 @@ fun expect_thm name smt_tac t = let open boolLib val thm = Tactical.TAC_PROOF (([], t), smt_tac) - handle Feedback.HOL_ERR (HOL_ERROR recd) => - let val {origin_structure, origin_function, source_location, message} = recd - in + handle Feedback.HOL_ERR holerr => die ("Test of solver '" ^ name ^ "' failed on term '" ^ term_with_types t ^ "': exception HOL_ERR (in " ^ - origin_structure ^ "." ^ origin_function ^ - " " ^ locn.toString source_location ^ ", message: " ^ message ^ - ")") - end + top_structure_of holerr ^ "." ^ top_function_of holerr ^ + " " ^ locn.toString (top_location_of holerr) ^ + ", message: " ^ message_of holerr ^ ")") in if null (Thm.hyp thm) andalso Thm.concl thm ~~ t then () else @@ -79,13 +76,11 @@ 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 (HOL_ERROR recd) => - let val {origin_structure, origin_function, source_location, message} = recd - in - if origin_structure = "HolSmtLib" andalso - origin_function = "GENERIC_SMT_TAC" andalso - (message = "solver reports negated term to be 'satisfiable'" orelse - message = "solver reports negated term to be 'satisfiable' (model returned)") + end handle Feedback.HOL_ERR holerr => + if top_structure_of holerr = "HolSmtLib" andalso + top_function_of holerr = "GENERIC_SMT_TAC" andalso + (message_of holerr = "solver reports negated term to be 'satisfiable'" orelse + message_of holerr = "solver reports negated term to be 'satisfiable' (model returned)") then (* re-enable inclusion of theorems, i.e. restore the default setting *) SmtLib.include_theorems := true @@ -93,10 +88,11 @@ 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 ^ - " " ^ locn.toString source_location ^ ", message: " ^ message ^ - ")") - end + top_structure_of holerr ^ "." ^ + top_function_of holerr ^ + " " ^ locn.toString (top_location_of holerr) ^ + ", message: " ^ message_of holerr ^ ")") + fun mk_test_fun is_configured expect_fun name smt_tac = if is_configured then (fn g => (expect_fun name smt_tac g; print ".")) diff --git a/src/boss/selftest.sml b/src/boss/selftest.sml index 666bbe7f99..fa33b2a8d3 100644 --- a/src/boss/selftest.sml +++ b/src/boss/selftest.sml @@ -42,10 +42,10 @@ val _ = tprint "new_type_definition error message" val _ = ignore (new_type_definition("mytydef", tydef_th)) handle HOL_ERR herr => - if function_of herr <> "new_type_definition" orelse - structure_of herr <> "Theory.Definition" orelse + if top_function_of herr <> "new_type_definition" orelse + top_structure_of herr <> "Theory.Definition" orelse message_of herr <> - "at Thm.prim_type_definition: expected a theorem of the form \"?x. P x\"" + "expected a theorem of the form \"?x. P x\"" then die "FAILED" else OK() diff --git a/src/floating-point/binary_ieeeLib.sml b/src/floating-point/binary_ieeeLib.sml index f01ac5018a..c57288f243 100644 --- a/src/floating-point/binary_ieeeLib.sml +++ b/src/floating-point/binary_ieeeLib.sml @@ -393,7 +393,7 @@ local in mlibUseful.INL (ties_to_even (boolSyntax.mk_imp (c, rx))) handle (e as HOL_ERR herr) => - if function_of herr = "EQT_ELIM" then + if top_function_of herr = "EQT_ELIM" then mlibUseful.INR (conj_assoc_rule (ties_to_even (boolSyntax.mk_conj (c, boolSyntax.mk_neg rx)))) diff --git a/src/integer/selftest.sml b/src/integer/selftest.sml index 03eeca5d65..b9ed6d9f22 100644 --- a/src/integer/selftest.sml +++ b/src/integer/selftest.sml @@ -9,7 +9,7 @@ fun okparse_exnstruct s = s = "Parse" orelse s = "Preterm" val _ = shouldfail { checkexn = fn HOL_ERR herr => - okparse_exnstruct (structure_of herr) + okparse_exnstruct (top_structure_of herr) | _ => false, printarg = (fn s => "Parse should fail: “" ^ s ^ "”"), printresult = term_to_string, @@ -19,7 +19,7 @@ val _ = val _ = shouldfail { checkexn = fn HOL_ERR herr => - okparse_exnstruct (structure_of herr) + okparse_exnstruct (top_structure_of herr) | _ => false, printarg = (fn s => "Parse should be ambiguous: “" ^ s ^ "”"), printresult = term_to_string, diff --git a/src/n-bit/selftest.sml b/src/n-bit/selftest.sml index 92109d2352..32eb5b4b8e 100644 --- a/src/n-bit/selftest.sml +++ b/src/n-bit/selftest.sml @@ -93,7 +93,7 @@ fun test_counter (c:conv) tm = let else SOME "bad counterexample" | HOL_ERR herr => - SOME ("unexpected exception from " ^ function_of herr) + SOME ("unexpected exception from " ^ top_function_of herr) in tprint ("Counterexample: " ^ trunc 49 tm); case res of diff --git a/src/prekernel/Feedback.sml b/src/prekernel/Feedback.sml index 7152abae50..e85f88febb 100644 --- a/src/prekernel/Feedback.sml +++ b/src/prekernel/Feedback.sml @@ -28,15 +28,18 @@ datatype hol_error = {origins : origin list, message : string} +fun origins_of (HOL_ERROR {origins,...}) = origins +fun message_of (HOL_ERROR {message,...}) = message + fun mk_hol_error s1 s2 loc mesg = HOL_ERROR {origins = [mk_origin s1 s2 loc], message = mesg} fun wrap_hol_error s f l (HOL_ERROR {origins,message}) = - HOL_ERROR - {origins = mk_origin s f l::origins, - message = message} + HOL_ERROR + {origins = mk_origin s f l::origins, + message = message} val empty_hol_error = HOL_ERROR @@ -55,9 +58,6 @@ exception HOL_ERR of hol_error; exception BATCH_ERR of string; -fun origins_of (HOL_ERROR {origins,...}) = origins -fun message_of (HOL_ERROR {message,...}) = message - fun top_structure_of herr = case origins_of herr of [] => raise HOL_ERR (empty_origins_error "top_structure_of") @@ -205,7 +205,7 @@ end (*--------------------------------------------------------------------------- Support for backtracing exceptions, treating HOL_ERR specially. - Subtlety: if we see that the exception is an Interrupt, we raise it. + If we see that the exception is an Interrupt, we raise it. ---------------------------------------------------------------------------*) fun wrap_exn_loc s f l e = @@ -220,14 +220,13 @@ fun HOL_MESG s = if !emit_MESG then !MESG_outstream (!MESG_to_string s) else () fun HOL_PROGRESS_MESG (start, finish) f x = - if !emit_MESG then - let - in + if !emit_MESG then + let in !MESG_outstream ("<>\n") end - else f x + else f x fun HOL_WARNING s1 s2 s3 = if !WARNINGs_as_ERRs then raise mk_HOL_ERR s1 s2 s3 diff --git a/src/proofman/tests/selftest.sml b/src/proofman/tests/selftest.sml index 8604c41454..2cfc350c7e 100644 --- a/src/proofman/tests/selftest.sml +++ b/src/proofman/tests/selftest.sml @@ -199,7 +199,10 @@ val _ = List.app testf [ val _ = Parse.current_backend := PPBackEnd.raw_terminal -val _ = app (fn (w,s) => Portable.with_flag(testutils.linewidth,w) tpp s) +val _ = + let fun testr (w,s) = + Portable.with_flag(testutils.linewidth,w) tpp s + in app testr [(20, "f\n (longterm =\n longterm)"), (20, "f\n (term001 = term002)"), (30, "let\n\ @@ -218,6 +221,7 @@ val _ = app (fn (w,s) => Portable.with_flag(testutils.linewidth,w) tpp s) \ x /\\ y /\\ z)"), (80, ">") ] + end val _ = List.app tpp ["$var$(*\\))", "$var$((*\\z)"] diff --git a/src/tactictoe/src/tttEval.sml b/src/tactictoe/src/tttEval.sml index 7e67c0c4d3..9e1516ff12 100644 --- a/src/tactictoe/src/tttEval.sml +++ b/src/tactictoe/src/tttEval.sml @@ -16,20 +16,25 @@ open HolKernel Abbrev boolLib aiLib val ERR = mk_HOL_ERR "tttEval" fun catch_err msg f x = - f x handle HOL_ERR (HOL_ERROR recd) => - let val {origin_structure,origin_function,source_location,message} = recd - in print_endline (String.concat - [msg, ":", origin_structure, ":", origin_function, ":", - locn.toShortString source_location, ":", message]); + f x handle HOL_ERR holerr => + let in + print_endline $ String.concat + [msg, ":", + top_structure_of holerr, ":", + top_function_of holerr, ":", + locn.toShortString (top_location_of holerr), ":", + message_of holerr]; raise ERR "tttEval" "error caught (see log)" end + fun catch_err_ignore msg f x = - f x handle HOL_ERR (HOL_ERROR recd) => - let val {origin_structure,origin_function,source_location,message} = recd - in print_endline (String.concat - [msg, ":", origin_structure, ":", origin_function, ":", - locn.toShortString source_location, ":", message]) - end + f x handle HOL_ERR holerr => + print_endline $ String.concat + [msg, ":", + top_structure_of holerr, ":", + top_function_of holerr, ":", + locn.toShortString (top_location_of holerr), ":", + message_of holerr] (* ------------------------------------------------------------------------- diff --git a/src/tfl/src/selftest.sml b/src/tfl/src/selftest.sml index 578ef4b107..1528cc259c 100644 --- a/src/tfl/src/selftest.sml +++ b/src/tfl/src/selftest.sml @@ -1,6 +1,5 @@ open HolKernel Parse open Defn - open testutils fun test msg f x = (tprint msg; require (check_result (K true)) f x) @@ -52,6 +51,7 @@ fun define q = in Defn.mk_defn (hd names) tm end + fun exnlookfor sl (Exn (HOL_ERR herr)) = if List.all (fn s => String.isSubstring s (message_of herr)) sl then OK() else @@ -61,7 +61,7 @@ fun exnlookfor sl (Exn (HOL_ERR herr)) = | exnlookfor _ _ = die ("\nExecution unexpectedly successful") fun badvarcheck r = - exnlookfor ["Simple definition failed", "Free variables in rhs"] r + exnlookfor ["Free variables in rhs"] r fun wfunivq r = exnlookfor ["Universally quantified equation as argument"] r From 4f8aa960a1ecdd23e536bf904330c19f1b15a139 Mon Sep 17 00:00:00 2001 From: Konrad Slind Date: Sun, 5 Oct 2025 22:37:16 -0500 Subject: [PATCH 13/13] tweak test where Globals.linewidth and testutils.linewidth are both at play --- src/proofman/tests/selftest.sml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/src/proofman/tests/selftest.sml b/src/proofman/tests/selftest.sml index 2cfc350c7e..292cc47929 100644 --- a/src/proofman/tests/selftest.sml +++ b/src/proofman/tests/selftest.sml @@ -277,14 +277,28 @@ val _ = let separator = [TOK ";", BreakSpace(1,0)], cons = "INSERT", nilstr = "EMPTY", block_info = (PP.INCONSISTENT, 1)}; - fun test (wdth, s, t) = - with_flag(linewidth,wdth) +(* This looks funky : the invocation of term_to_string is done under a + different linewidth than the invocation of tpp_expected *) +(* fun test (wdth, s, t) = + with_flag(Globals.linewidth,wdth) (trace ("types", 1) tpp_expected) {input = trace ("types", 1) term_to_string t, output = s, testf = fn s => "Width=" ^ Int.toString wdth ^ " type-annotation of “" ^ s ^ "”"} +*) +fun test (wdth, s, t) = + let val tstr = with_flag (Globals.linewidth,wdth) + (trace ("types", 1) term_to_string) t + val _ = print ("\ntstr:\n\n"^tstr^"\n\n") + in with_flag(testutils.linewidth,wdth) + (trace ("types", 1) tpp_expected) + {input = tstr, + output = s, + testf = fn s => "Width=" ^ Int.toString wdth ^ + " type-annotation of “" ^ s ^ "”"} + end in List.app test [ (75,