Fix (last few(?)) compile-time errors caused by located_thms

HOL-Theorem-Prover · Nov 27, 2024 · 01016dc · 01016dc
1 parent 9e17096
commit 01016dc
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 12 deletions.
diff --git a/examples/machine-code/lisp/lisp_evalScript.sml b/examples/machine-code/lisp/lisp_evalScript.sml
@@ -5,27 +5,36 @@ open lisp_opsTheory;
 
 val _ = let
   val thms = DB.match [] ``SPEC ARM_MODEL``
-  val thms = filter (can (find_term (can (match_term ``aLISP``))) o concl) (map (fst o snd) thms)
-  val renamer = Q.INST [`x1`|->`exp`,`x2`|->`x`,`x3`|->`y`,`x4`|->`z`,`x5`|->`stack`,`x6`|->`alist`] o INST [``limit:num``|->``l:num``]
+  val thms = filter (can (find_term (can (match_term ``aLISP``))) o concl)
+                    (map (#1 o #2) thms)
+  val renamer = Q.INST [‘x1’|->‘exp’,‘x2’|->‘x’,‘x3’|->‘y’,‘x4’|->‘z’,
+                        ‘x5’|->‘stack’,‘x6’|->‘alist’] o
+                INST [“limit:num”|->“l:num”]
   val thms = map renamer thms
   val _ = add_code_abbrev [arm_alloc_code,arm_equal_code]
   val _ = add_compiled thms
   in () end;
 
 val _ = let
   val thms = DB.match [] ``SPEC PPC_MODEL``
-  val thms = filter (can (find_term (can (match_term ``pLISP``))) o concl) (map (fst o snd) thms)
-  val renamer = Q.INST [`x1`|->`exp`,`x2`|->`x`,`x3`|->`y`,`x4`|->`z`,`x5`|->`stack`,`x6`|->`alist`] o INST [``limit:num``|->``l:num``]
+  val thms = filter (can (find_term (can (match_term ``pLISP``))) o concl)
+                    (map (#1 o #2) thms)
+  val renamer = Q.INST [‘x1’|->‘exp’,‘x2’|->‘x’,‘x3’|->‘y’,‘x4’|->‘z’,
+                        ‘x5’|->‘stack’,‘x6’|->‘alist’] o
+                INST [“limit:num”|->“l:num”]
   val thms = map renamer thms
   val _ = add_code_abbrev [ppc_alloc_code,ppc_equal_code]
   val _ = add_compiled thms
   in () end;
 
 val _ = let
   val thms = DB.match [] ``SPEC X86_MODEL``
-  val thms = filter (can (find_term (can (match_term ``xLISP``))) o concl) (map (fst o snd) thms)
-  val renamer = Q.INST [`x1`|->`exp`,`x2`|->`x`,`x3`|->`y`,`x4`|->`z`,`x5`|->`stack`,`x6`|->`alist`] o
-                INST [``limit:num``|->``l:num``,mk_var("eip",``:word32``) |-> mk_var("p",``:word32``)]
+  val thms = filter (can (find_term (can (match_term ``xLISP``))) o concl)
+                    (map (#1 o #2) thms)
+  val renamer = Q.INST [‘x1’|->‘exp’,‘x2’|->‘x’,‘x3’|->‘y’,‘x4’|->‘z’,
+                        ‘x5’|->‘stack’,‘x6’|->‘alist’] o
+                INST [“limit:num”|->“l:num”,
+                      mk_var("eip",“:word32”) |-> mk_var("p",“:word32”)]
   val thms = map renamer thms
   val _ = add_code_abbrev [x86_alloc_code,x86_equal_code]
   val _ = add_compiled thms

diff --git a/examples/theorem-prover/lisp-runtime/implementation/lisp_bigopsScript.sml b/examples/theorem-prover/lisp-runtime/implementation/lisp_bigopsScript.sml
@@ -11,7 +11,8 @@ open compilerLib decompilerLib codegenLib;
 
 val _ = let
   val thms = DB.match [] ``SPEC X64_MODEL``
-  val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl) (map (fst o snd) thms)
+  val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl)
+                    (map (#1 o #2) thms)
   val _ = map (fn th => add_compiled [th] handle e => ()) thms
   in () end;
 

diff --git a/examples/theorem-prover/lisp-runtime/implementation/lisp_compiler_opScript.sml b/examples/theorem-prover/lisp-runtime/implementation/lisp_compiler_opScript.sml
@@ -15,7 +15,8 @@ open set_sepTheory bitTheory fcpTheory stringTheory optionTheory relationTheory;
 
 val _ = let
   val thms = DB.match [] ``SPEC X64_MODEL``
-  val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl) (map (fst o snd) thms)
+  val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl)
+                    (map (#1 o #2) thms)
   val thms = map (Q.INST [`ddd`|->`SOME F`,`cu`|->`NONE`]) thms
   val _ = map (fn th => add_compiled [th] handle e => ()) thms
   in () end;
@@ -4183,7 +4184,8 @@ val X64_LISP_COMPILE = save_thm("X64_LISP_COMPILE",let
 
 val _ = let (* reload all primitive ops with SOME T for ddd *)
   val thms = DB.match [] ``SPEC X64_MODEL``
-  val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl) (map (fst o snd) thms)
+  val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl)
+                    (map (#1 o #2) thms)
   val thms = map (Q.INST [`ddd`|->`SOME T`,`cu`|->`NONE`]) thms
   val _ = map (fn th => add_compiled [th] handle e => ()) thms
   in () end;
@@ -4609,7 +4611,8 @@ val X64_LISP_COMPILE_FOR_EVAL = save_thm("X64_LISP_COMPILE_FOR_EVAL",let
 
 val _ = let
   val thms = DB.match [] ``SPEC X64_MODEL``
-  val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl) (map (fst o snd) thms)
+  val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl)
+                    (map (#1 o #2) thms)
   val _ = map (fn th => add_compiled [th] handle e => ()) thms
   in () end;
 

diff --git a/examples/theorem-prover/lisp-runtime/implementation/lisp_correctnessScript.sml b/examples/theorem-prover/lisp-runtime/implementation/lisp_correctnessScript.sml
@@ -18,7 +18,8 @@ val RW1 = ONCE_REWRITE_RULE;
 
 val _ = let
   val thms = DB.match [] ``SPEC X64_MODEL``
-  val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl) (map (fst o snd) thms)
+  val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl)
+                    (map (#1 o #2) thms)
   val thms = map (INST [``ddd:bool option``|->``SOME T``]) thms
   val _ = map (fn th => add_compiled [th] handle e => ()) thms
   in () end;