From f7a642bd3f8a5436873d0163114a30dad23ba9c2 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Thu, 17 Dec 2015 16:48:54 +0000
Subject: Remove external functions that the library provides, having added
 them to the type environment finally. (Also small cleaning of the new
 makefile)

---
 mips/Makefile  | 12 ++++++------
 mips/mips.sail |  4 ++--
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'mips')

diff --git a/mips/Makefile b/mips/Makefile
index f8417c67..7bd20737 100644
--- a/mips/Makefile
+++ b/mips/Makefile
@@ -15,9 +15,9 @@ endif
 # the order of the files is important
 MIPSSOURCES= mips.sail
 
-all: $(BUILDDIR)/mips.ml $(BUILDDIR)/mips_extras.ml
+all: $(BUILDDIR)mips.ml $(BUILDDIR)mips_extras.ml
 
-lem: $(BUILDDIR)/mips.lem
+lem: $(BUILDDIR)mips.lem
 
 # this will force build everything, including the tools
 full:
@@ -38,7 +38,7 @@ $(LEM):
 $(BUILDDIR):
 	mkdir -p $@
 
-$(BUILDDIR)/mips.lem: $(MIPSSOURCES) $(SAIL) | $(BUILDDIR)
+$(BUILDDIR)mips.lem: $(MIPSSOURCES) $(SAIL) | $(BUILDDIR)
 # if bash is detected we can print nicer errors
 ifeq ($(SHELL),/bin/bash)
 # 	the test at the end is so we return the exit code of sail and not parse_sail.sh
@@ -49,13 +49,13 @@ endif
 #       sail uses the name of the first file on the list
 	@mv $(<:.sail=.lem) $(BUILDDIR)mips.lem
 
-$(BUILDDIR)/mips.ml: $(BUILDDIR)mips.lem $(LEM)
+$(BUILDDIR)mips.ml: $(BUILDDIR)mips.lem $(LEM)
 	$(LEM) -ocaml -only_changed_output -lib $(SAILDIR)/src/lem_interp/ $<
 # 	FIXME: lem bug, does not change modification time
 	touch $@
 
-$(BUILDDIR)/mips_extras.ml: $(BUILDDIR)mips_extras.lem $(LEM)
-	cp mips_extras.lem $<
+$(BUILDDIR)mips_extras.ml: 
+	cp mips_extras.lem $@
 	$(LEM) -ocaml -only_changed_output -lib $(SAILDIR)/src/lem_interp/ $<
 	touch $@
 
diff --git a/mips/mips.sail b/mips/mips.sail
index 4f468354..16a607a9 100644
--- a/mips/mips.sail
+++ b/mips/mips.sail
@@ -1,10 +1,10 @@
 (* bit vectors have indices decreasing from left i.e. msb is highest index *)
 default Order dec
 
-(* external functions *)
+(*(* external functions *)
 val extern forall Nat 'm, Nat 'n. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTS (* Sign extend *)
 val extern forall Nat 'n, Nat 'm. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTZ (* Zero extend *)
-
+*)
 register (bit[64]) PC
 
 (* CP0 Registers *)
-- 
cgit v1.2.3