Fix faults in a93d43e; extend tests to riscv_stepLib

HOL-Theorem-Prover · Aug 4, 2023 · 86b636c · 86b636c
1 parent a93d43e
commit 86b636c
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 19 deletions.
diff --git a/examples/l3-machine-code/arm/step/arm_stepLib.sml b/examples/l3-machine-code/arm/step/arm_stepLib.sml
@@ -8,22 +8,14 @@ struct
 open HolKernel boolLib bossLib
 
 open armTheory arm_stepTheory arm_configLib
-open state_transformerSyntax blastLib
+open state_transformerSyntax blastLib Parse
 
-structure Parse =
-struct
-   open Parse
-   val (tyg, (tmg, _)) =
-      apsnd (term_grammar.mfupdate_overload_info
-               (Overload.remove_overloaded_form "add") o
-             ParseExtras.grammar_loose_equality
-            )
-      arm_stepTheory.arm_step_grammars
-   val (Type, Term) = parse_from_grammars (tyg, tmg)
-end
-
-open Parse
-val _ = Parse.hide "add"
+val ambient_grammars = (type_grammar(), term_grammar())
+val _ = temp_set_grammars
+          (arm_stepTheory.arm_step_grammars
+             |> apsnd (#1 o term_grammar.mfupdate_overload_info
+                              (Overload.remove_overloaded_form "add") o
+                       ParseExtras.grammar_loose_equality))
 
 val ERR = Feedback.mk_HOL_ERR "arm_stepLib"
 val WARN = Feedback.HOL_WARNING "arm_stepLib"
@@ -4318,7 +4310,7 @@ in
       end
 end
 
-val () = Parse.reveal "add"
+val _ = temp_set_grammars ambient_grammars
 
 (* ---------------------------- *)
 

diff --git a/examples/l3-machine-code/m0/step/m0_stepLib.sml b/examples/l3-machine-code/m0/step/m0_stepLib.sml
@@ -9,6 +9,7 @@ open HolKernel boolLib bossLib
 
 open m0Theory m0_stepTheory
 open state_transformerSyntax blastLib
+open Parse
 
 val ambient_grammars = (type_grammar(), term_grammar())
 val _ = temp_set_grammars m0_stepTheory.m0_step_grammars

diff --git a/examples/l3-machine-code/mips/step/mips_stepLib.sml b/examples/l3-machine-code/mips/step/mips_stepLib.sml
@@ -5,7 +5,7 @@
 structure mips_stepLib :> mips_stepLib =
 struct
 
-open HolKernel boolLib bossLib
+open HolKernel Parse boolLib bossLib
 open blastLib mipsTheory mips_stepTheory
 
 local open mips in end

diff --git a/examples/l3-machine-code/riscv/step/Holmakefile b/examples/l3-machine-code/riscv/step/Holmakefile
@@ -3,7 +3,7 @@ CLINE_OPTIONS = --qof
 
 ifdef POLY
 HOLHEAP = riscv-heap
-EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
+EXTRA_CLEANS = $(HOLHEAP) riscv-steplib-selftest.log
 
 BARE_THYS = ../model/riscvTheory
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
@@ -15,3 +15,10 @@ $(HOLHEAP): ../../l3-heap $(DEPS)
 	$(protect $(HOLDIR)/bin/buildheap) -b $< -o $(HOLHEAP) $(BARE_THYS)
 
 endif
+
+ifdef HOLSELFTESTLEVEL
+all: riscv-steplib-selftest.log
+
+riscv-steplib-selftest.log: ../../common/testscript.ML riscv_stepLib.uo
+	tmp=`mktemp "$${TMPDIR:-.}/stepLibXXXX"` && TESTLIB=riscv_stepLib $(protect $(HOLDIR)/bin/hol) < $< > $$tmp && $(MV) $$tmp $@
+endif
diff --git a/examples/l3-machine-code/x64/step/x64_stepLib.sml b/examples/l3-machine-code/x64/step/x64_stepLib.sml
@@ -5,7 +5,7 @@
 structure x64_stepLib :> x64_stepLib =
 struct
 
-open HolKernel boolLib bossLib
+open HolKernel Parse boolLib bossLib
 open updateLib utilsLib x64Lib x64Theory x64_stepTheory
 
 val ambient_grammars = (type_grammar(), term_grammar())