Merge remote-tracking branch 'origin/sail2' into c_fixes

7 files changed, 48 insertions, 43 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/prompt.lem
deleted file mode 100644
index edbd3752..00000000
--- a/lib/hol/prompt.lem
+++ /dev/null
@@ -1,18 +0,0 @@
-open import Prompt_monad
-open import State_monad
-open import State
-
-let inline undefined_bool = undefined_boolS
-let inline bool_of_bitU_oracle = bool_of_bitU_oracleS
-let inline bool_of_bitU_fail = bool_of_bitU_fail
-let inline bools_of_bits_oracle = bools_of_bits_oracleS
-let inline of_bits_oracle = of_bits_oracleS
-let inline of_bits_fail = of_bits_failS
-let inline mword_oracle = mword_oracleS
-let inline reg_deref = read_regS
-
-let inline foreachM = foreachS
-let inline whileM = whileS
-let inline untilM = untilS
-let inline and_boolM = and_boolS
-let inline or_boolM = or_boolS
diff --git a/lib/hol/sail2_prompt.lem b/lib/hol/sail2_prompt.lem
new file mode 100644
index 00000000..674d4e34
--- /dev/null
+++ b/lib/hol/sail2_prompt.lem
@@ -0,0 +1,19 @@
+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
+let inline bool_of_bitU_fail = bool_of_bitU_fail
+let inline bools_of_bits_nondet = bools_of_bits_nondetS
+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
+let inline untilM = untilS
+let inline and_boolM = and_boolS
+let inline or_boolM = or_boolS
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"
 
 
 (****************************************************)