make sail produce prompt and state version of shallow embedding files at the same time with the types both have in common factored out into separate file, rename one mips shallow embedding _extras file as required by this

1 files changed, 0 insertions, 49 deletions

diff --git a/mips/mips_extras_sequential_embed.lem b/mips/mips_extras_sequential_embed.lem
deleted file mode 100644
index e765bd23..00000000
--- a/mips/mips_extras_sequential_embed.lem
+++ /dev/null
@@ -1,49 +0,0 @@
-open import Pervasives
-open import Sail_impl_base
-open import Sail_values
-open import State
-
-let endian = E_big_endian
-
-val MEMr             : (vector bitU * integer) -> M (vector bitU)
-val MEMr_reserve     : (vector bitU * integer) -> M (vector bitU)
-val MEMr_tag         : (vector bitU * integer) -> M (vector bitU)
-val MEMr_tag_reserve : (vector bitU * integer) -> M (vector bitU)
-
-let MEMr (addr,size)             = read_mem endian false Read_plain addr size
-let MEMr_reserve (addr,size)     = read_mem endian false Read_reserve addr size
-let MEMr_tag (addr,size)         = read_mem endian false Read_tag addr size
-let MEMr_tag_reserve (addr,size) = read_mem endian false Read_tag_reserve addr size
-
-
-val MEMea                 : (vector bitU * integer) -> M unit
-val MEMea_conditional     : (vector bitU * integer) -> M unit
-val MEMea_tag             : (vector bitU * integer) -> M unit
-val MEMea_tag_conditional : (vector bitU * integer) -> M unit
-
-let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
-let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
-let MEMea_tag (addr,size)             = write_mem_ea Write_tag addr size
-let MEMea_tag_conditional (addr,size) = write_mem_ea Write_tag_conditional addr size
-
-
-val MEMval                 : (vector bitU * integer * vector bitU) -> M unit
-val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
-val MEMval_tag             : (vector bitU * integer * vector bitU) -> M unit
-val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bitU
-
-let MEMval (_,_,v)                 = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v)     = write_mem_val endian v >>= fun b -> return (if b then I else O)
-let MEMval_tag (_,_,v)             = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then I else O)
-
-
-val MEM_sync  : unit -> M unit
-
-let MEM_sync () = barrier Barrier_Isync
-
-
-let duplicate (bit,len) =
-  let bits = repeat [bit] len in
-  let start = len - 1 in
-  Vector bits start false