diff options
| author | Brian Campbell | 2018-05-17 12:12:02 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-05-17 12:12:02 +0100 |
| commit | c37130ba4ac69be6a298476b24b1f93811df4bb4 (patch) | |
| tree | 677f02c87d47f4ef354ad55a1a03b244651631d9 /mips/Makefile | |
| parent | fc99e8af769b98ffbc951b20c12fc9111f48cec5 (diff) | |
Clean up MIPS for HOL4 a little
Move mono_rewrites into lib
Diffstat (limited to 'mips/Makefile')
| -rw-r--r-- | mips/Makefile | 13 |
1 files changed, 10 insertions, 3 deletions
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 |