From 823fe1d82e753add2d54ba010689a81af027ba6d Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 10 May 2018 14:52:31 +0100
Subject: RISC-V in HOL4

---
 lib/hol/prompt_monad.lem |  3 +++
 riscv/Holmakefile        | 11 +++++++++++
 riscv/Makefile           |  9 +++++++++
 3 files changed, 23 insertions(+)
 create mode 100644 riscv/Holmakefile

diff --git a/lib/hol/prompt_monad.lem b/lib/hol/prompt_monad.lem
index b1ef4bcc..4481f623 100644
--- a/lib/hol/prompt_monad.lem
+++ b/lib/hol/prompt_monad.lem
@@ -30,3 +30,6 @@ 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 ()
+
+let inline excl_result = excl_resultS
+let inline assert_exp = assert_expS
\ No newline at end of file
diff --git a/riscv/Holmakefile b/riscv/Holmakefile
new file mode 100644
index 00000000..626e6f2f
--- /dev/null
+++ b/riscv/Holmakefile
@@ -0,0 +1,11 @@
+LEMDIR=../../lem/hol-lib
+
+INCLUDES = $(LEMDIR) ../lib/hol
+
+all: riscv_sequentialTheory.uo
+.PHONY: all
+
+ifdef POLY
+BASE_HEAP = ../lib/hol/sail-heap
+
+endif
diff --git a/riscv/Makefile b/riscv/Makefile
index 781ec354..7173f24d 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -34,6 +34,15 @@ Riscv.thy: riscv.lem riscv_extras.lem
 riscv.lem: $(SAIL_SRCS) Makefile
 	$(SAIL_DIR)/sail -lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS)
 
+riscv_sequential.lem: $(SAIL_SRCS) Makefile
+	$(SAIL_DIR)/sail -lem -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS)
+
+riscv_sequentialScript.sml : riscv_sequential.lem riscv_extras_sequential.lem
+	lem -hol -outdir . -lib ../lib/hol -lib ../src/lem_interp -lib ../src/gen_lib \
+		riscv_extras_sequential.lem \
+		riscv_sequential_types.lem \
+		riscv_sequential.lem
+
 clean:
 	-rm -rf riscv _sbuild
 	-rm -f riscv.lem riscv_types.lem
-- 
cgit v1.2.3