diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/.gitignore | 5 | ||||
| -rw-r--r-- | mips/Holmakefile | 11 | ||||
| -rw-r--r-- | mips/Makefile | 13 | ||||
| -rw-r--r-- | mips/prelude.sail | 2 |
4 files changed, 26 insertions, 5 deletions
diff --git a/mips/.gitignore b/mips/.gitignore new file mode 100644 index 00000000..2ee9fde0 --- /dev/null +++ b/mips/.gitignore @@ -0,0 +1,5 @@ +mips.lem +mips_types.lem +mipsScript.sml +mips_typesScript.sml +mips_extrasScript.sml
\ No newline at end of file diff --git a/mips/Holmakefile b/mips/Holmakefile new file mode 100644 index 00000000..a31bfd4f --- /dev/null +++ b/mips/Holmakefile @@ -0,0 +1,11 @@ +LEMDIR=../../lem/hol-lib + +INCLUDES = $(LEMDIR) ../lib/hol + +all: mipsTheory.uo +.PHONY: all + +ifdef POLY +BASE_HEAP = ../lib/hol/sail-heap + +endif diff --git a/mips/Makefile b/mips/Makefile index c0670380..100687e8 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -19,8 +19,7 @@ mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS) $(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ mips_no_tlb_types.lem: mips_no_tlb.lem -# TODO: Use monomorphisation so that we can switch to machine words -mips.lem: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) +mips.lem: $(MIPS_PRE) $(SAIL_LIB_DIR)/mono_rewrites.sail $(MIPS_TLB) $(MIPS_SAILS) $(SAIL) -lem -o mips -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ mips_types.lem: mips.lem @@ -28,8 +27,16 @@ M%.thy: m%.lem m%_types.lem mips_extras.lem lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy +%Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem + lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ + +%Theory.uo: %Script.sml + Holmake $@ + LOC_FILES:=$(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) include ../etc/loc.mk clean: - rm -rf mips Mips.thy mips.lem _sbuild + rm -rf mips Mips.thy mips.lem mips_types.lem _sbuild + rm -f mipsScript.sml mips_typesScript.sml mips_extrasScript.sml + -Holmake cleanAll diff --git a/mips/prelude.sail b/mips/prelude.sail index 5bb79f97..f805876a 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -310,5 +310,3 @@ val mask : forall 'm 'n , 'm >= 'n > 0 . bits('m) -> bits('n) function mask bs = bs['n - 1 .. 0] val "get_time_ns" : unit -> int - -$include <mono_rewrites.sail> |