Hol err datatype

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 (top_structure_of e) (top_function_of e)
              (String.concat
                 [Hol_pp.term_to_string enc, ": ",
                  Hol_pp.term_to_string tm, "\n"]);

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 top_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
+                  top_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

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
 

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 top_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 top_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 top_function_of herr = "mk_pabs" then
+        CS (e, [(v, b)])
+     else raise HOL_ERR herr
 
 (* Set of list *)
 

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 top_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 top_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 top_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 top_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 top_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

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 top_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

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
+                    top_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
+                  top_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 top_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

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",

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
+                   top_function_of herr = "find_rw"
+                  then err "instruction instance not supported"
+                else raise e
             end
       end
 end

examples/l3-machine-code/riscv/step/riscv_stepLib.sml

@@ -277,8 +277,12 @@ 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
+         top_function_of herr = "find_rw"
+      then
+         err tm "instruction instance not supported"
+      else raise e
 end
 
 (* -------------------------------------------------------------------------

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