From 86b636c26a48c10a3fb34f0cb2523c4331e97bd2 Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Fri, 4 Aug 2023 10:42:15 +1000
Subject: [PATCH] Fix faults in a93d43e; extend tests to riscv_stepLib

---
 .../l3-machine-code/arm/step/arm_stepLib.sml  | 24 +++++++------------
 .../l3-machine-code/m0/step/m0_stepLib.sml    |  1 +
 .../mips/step/mips_stepLib.sml                |  2 +-
 .../l3-machine-code/riscv/step/Holmakefile    |  9 ++++++-
 .../l3-machine-code/x64/step/x64_stepLib.sml  |  2 +-
 5 files changed, 19 insertions(+), 19 deletions(-)

diff --git a/examples/l3-machine-code/arm/step/arm_stepLib.sml b/examples/l3-machine-code/arm/step/arm_stepLib.sml
index a6e6b76e11..3677b1ea7c 100644
--- 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
index e9233d3e00..3a9e70a287 100644
--- 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
index 5cc28bf119..a58e4d3f6b 100644
--- 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
index b92433d66a..8da6ae7045 100644
--- 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
index 18dc31b046..a3ff47a34b 100644
--- 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())