HOL script generation for library and CHERI

(still needs some Lem work on types before it will be useful)

4 files changed, 102 insertions, 0 deletions

diff --git a/lib/hol/Holmakefile b/lib/hol/Holmakefile
new file mode 100644
index 00000000..442b1816
--- /dev/null
+++ b/lib/hol/Holmakefile
@@ -0,0 +1,27 @@
+SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.sml \
+  sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \
+  state_monadScript.sml stateScript.sml
+
+EXTRA_CLEANS = $(SCRIPTS)
+
+THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS))
+
+LEMDIR=../../../lem/hol-lib
+
+INCLUDES = $(LEMDIR)
+
+all: $(THYS)
+.PHONY: all
+
+ifdef POLY
+HOLHEAP = sail-heap
+EXTRA_CLEANS = $(SCRIPTS) $(HOLHEAP) $(HOLHEAP).o
+
+BASE_HEAP = $(LEMDIR)/lemheap
+
+$(HOLHEAP):
+	$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) -b $(BASE_HEAP)
+
+all: $(HOLHEAP)
+
+endif
diff --git a/lib/hol/Makefile b/lib/hol/Makefile
new file mode 100644
index 00000000..b6be46b4
--- /dev/null
+++ b/lib/hol/Makefile
@@ -0,0 +1,31 @@
+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
+
+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
+
+all: sail-heap
+
+$(SCRIPTS): $(LEMSRC)
+	lem -hol -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $(LEMSRC)
+
+THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS))
+
+$(THYS) sail-heap: $(SCRIPTS)
+	Holmake
+
+# Holmake will also clear out the generated $(SCRIPTS) files
+clean:
+	Holmake cleanAll
+
+.PHONY: all clean
diff --git a/lib/hol/prompt.lem b/lib/hol/prompt.lem
new file mode 100644
index 00000000..a04e0a0a
--- /dev/null
+++ b/lib/hol/prompt.lem
@@ -0,0 +1,12 @@
+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
diff --git a/lib/hol/prompt_monad.lem b/lib/hol/prompt_monad.lem
new file mode 100644
index 00000000..b1ef4bcc
--- /dev/null
+++ b/lib/hol/prompt_monad.lem
@@ -0,0 +1,32 @@
+open import Pervasives_extra
+open import Sail_instr_kinds
+open import Sail_values
+open import State_monad
+
+(* Fake interface of the prompt monad by redirecting to the state monad, since
+   the former is not currently supported by HOL4 *)
+
+type monad 'rv 'a 'e = monadS 'rv 'a 'e
+type monadR 'rv 'a 'e 'r = monadRS 'rv 'a 'e 'r
+
+let inline return = returnS
+let inline bind = bindS
+let inline (>>=) = (>>$=)
+let inline (>>) = (>>$)
+
+let inline throw = throwS
+let inline try_catch = try_catchS
+
+let inline catch_early_return = catch_early_returnS
+let inline early_return = early_returnS
+
+let inline maybe_fail = maybe_failS
+
+let inline read_reg = read_regS
+let inline reg_deref = read_regS
+let inline read_mem = read_memS
+let inline read_tag = read_tagS
+let inline write_tag = write_tagS
+let inline write_mem_ea wk addr sz = write_mem_eaS wk addr (nat_of_int sz)
+let inline write_mem_val = write_mem_valS
+let barrier _ = return ()