Update HOL setup

6 files changed, 33 insertions, 28 deletions

diff --git a/lib/hol/Holmakefile b/lib/hol/Holmakefile
index eac4fec8..8e8403f3 100644
--- a/lib/hol/Holmakefile
+++ b/lib/hol/Holmakefile
@@ -1,11 +1,12 @@
-LEM_SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.sml \
-  sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \
-  state_monadScript.sml stateScript.sml promptScript.sml prompt_monadScript.sml
+LEM_SCRIPTS = sail2_instr_kindsScript.sml sail2_valuesScript.sml sail2_operatorsScript.sml \
+  sail2_operators_mwordsScript.sml sail2_operators_bitlistsScript.sml \
+  sail2_state_monadScript.sml sail2_stateScript.sml sail2_promptScript.sml sail2_prompt_monadScript.sml \
+  sail2_stringScript.sml
 
 LEM_CLEANS = $(LEM_SCRIPTS)
 
 SCRIPTS = $(LEM_SCRIPTS) \
-  sail_valuesAuxiliaryScript.sml stateAuxiliaryScript.sml
+  sail2_valuesAuxiliaryScript.sml sail2_stateAuxiliaryScript.sml
 
 THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS))
 
diff --git a/lib/hol/Makefile b/lib/hol/Makefile
index 065f887a..783ef23d 100644
--- a/lib/hol/Makefile
+++ b/lib/hol/Makefile
@@ -1,22 +1,25 @@
 LEMSRC =  \
-  ../../src/lem_interp/sail_instr_kinds.lem \
-  ../../src/gen_lib/sail_values.lem \
-  ../../src/gen_lib/sail_operators.lem \
-  ../../src/gen_lib/sail_operators_mwords.lem \
-  ../../src/gen_lib/sail_operators_bitlists.lem \
-  ../../src/gen_lib/state_monad.lem \
-  ../../src/gen_lib/state.lem \
-  prompt_monad.lem \
-  prompt.lem
+  ../../src/lem_interp/sail2_instr_kinds.lem \
+  ../../src/gen_lib/sail2_values.lem \
+  ../../src/gen_lib/sail2_operators.lem \
+  ../../src/gen_lib/sail2_operators_mwords.lem \
+  ../../src/gen_lib/sail2_operators_bitlists.lem \
+  ../../src/gen_lib/sail2_state_monad.lem \
+  ../../src/gen_lib/sail2_state.lem \
+  ../../src/gen_lib/sail2_string.lem \
+  sail2_prompt_monad.lem \
+  sail2_prompt.lem
 
-SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.sml \
-  sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \
-  state_monadScript.sml stateScript.sml \
-  prompt_monadScript.sml promptScript.sml
+SCRIPTS = sail2_instr_kindsScript.sml sail2_valuesScript.sml sail2_operatorsScript.sml \
+  sail2_operators_mwordsScript.sml sail2_operators_bitlistsScript.sml \
+  sail2_state_monadScript.sml sail2_stateScript.sml \
+  sail2_prompt_monadScript.sml sail2_promptScript.sml \
+  sail2_stringScript.sml
 
 THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS))
 
 all: sail-heap $(THYS)
+all-scripts: $(SCRIPTS)
 
 $(SCRIPTS): $(LEMSRC)
 	lem -hol -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $(LEMSRC)
@@ -28,4 +31,4 @@ $(THYS) sail-heap: $(SCRIPTS)
 clean:
 	Holmake cleanAll
 
-.PHONY: all clean
+.PHONY: all all-scripts clean
diff --git a/lib/hol/prompt.lem b/lib/hol/sail2_prompt.lem
index 3597fa06..674d4e34 100644
--- a/lib/hol/prompt.lem
+++ b/lib/hol/sail2_prompt.lem
@@ -1,6 +1,6 @@
-open import Prompt_monad
-open import State_monad
-open import State
+open import Sail2_prompt_monad
+open import Sail2_state_monad
+open import Sail2_state
 
 let inline undefined_bool = undefined_boolS
 let inline bool_of_bitU_nondet = bool_of_bitU_nondetS
@@ -10,6 +10,7 @@ let inline of_bits_nondet = of_bits_nondetS
 let inline of_bits_fail = of_bits_failS
 let inline mword_nondet = mword_nondetS
 let inline reg_deref = read_regS
+let inline internal_pick = internal_pickS
 
 let inline foreachM = foreachS
 let inline whileM = whileS
diff --git a/lib/hol/prompt_monad.lem b/lib/hol/sail2_prompt_monad.lem
index 8fcd645a..3af931a5 100644
--- a/lib/hol/prompt_monad.lem
+++ b/lib/hol/sail2_prompt_monad.lem
@@ -1,7 +1,7 @@
 open import Pervasives_extra
-open import Sail_instr_kinds
-open import Sail_values
-open import State_monad
+open import Sail2_instr_kinds
+open import Sail2_values
+open import Sail2_state_monad
 
 (* Fake interface of the prompt monad by redirecting to the state monad, since
    the former is not currently supported by HOL4 *)
diff --git a/lib/hol/stateAuxiliaryScript.sml b/lib/hol/sail2_stateAuxiliaryScript.sml
index c8269750..4d70b033 100644
--- a/lib/hol/stateAuxiliaryScript.sml
+++ b/lib/hol/sail2_stateAuxiliaryScript.sml
@@ -1,6 +1,6 @@
 (*Generated by Lem from ../../src/gen_lib/state.lem.*)
 open HolKernel Parse boolLib bossLib;
-open lem_pervasives_extraTheory sail_valuesTheory state_monadTheory stateTheory;
+open lem_pervasives_extraTheory sail2_valuesTheory sail2_state_monadTheory sail2_stateTheory;
 
 val _ = numLib.prefer_num();
 
@@ -8,7 +8,7 @@ val _ = numLib.prefer_num();
 
 open lemLib;
 (* val _ = lemLib.run_interactive := true; *)
-val _ = new_theory "stateAuxiliary"
+val _ = new_theory "sail2_stateAuxiliary"
 
 
 (****************************************************)
diff --git a/lib/hol/sail_valuesAuxiliaryScript.sml b/lib/hol/sail2_valuesAuxiliaryScript.sml
index aa169979..b475c5ea 100644
--- a/lib/hol/sail_valuesAuxiliaryScript.sml
+++ b/lib/hol/sail2_valuesAuxiliaryScript.sml
@@ -1,6 +1,6 @@
 (*Generated by Lem from ../../src/gen_lib/sail_values.lem.*)
 open HolKernel Parse boolLib bossLib;
-open lem_pervasives_extraTheory lem_machine_wordTheory sail_valuesTheory;
+open lem_pervasives_extraTheory lem_machine_wordTheory sail2_valuesTheory;
 open intLib;
 
 val _ = numLib.prefer_num();
@@ -9,7 +9,7 @@ val _ = numLib.prefer_num();
 
 open lemLib;
 (* val _ = lemLib.run_interactive := true; *)
-val _ = new_theory "sail_valuesAuxiliary"
+val _ = new_theory "sail2_valuesAuxiliary"
 
 
 (****************************************************)