Begin refactoring Sail library

- Add back support for bit list representation of bit vectors, for backwards
  compatibility in order to ease integration with the interpreter.  For this
purpose, split out a file sail_operators.lem from sail_values.lem, and add a
variant sail_operators_mwords.lem for the machine word representation of
bitvectors.  Currently, Sail is hardcoded to use machine words for the
sequential state monad, and bit lists for the free monad, but this could be
turned into a command line flag.

- Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem
  library.  The wrappers make use of sizeof expressions to extract type
information from bitvectors (length, start index) in order to pass it to the
Lem functions.

- Add early return support to the free monad, using a new constructor "Return
  of 'r".  As with the sequential monad, functions with early return are
wrapped into "catch_early_return", which extracts the return value at the end
of the function execution.

1 files changed, 47 insertions, 0 deletions

diff --git a/mips_new_tc/mips_extras_embed.lem b/mips_new_tc/mips_extras_embed.lem
new file mode 100644
index 00000000..74bec64b
--- /dev/null
+++ b/mips_new_tc/mips_extras_embed.lem
@@ -0,0 +1,47 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail_impl_base
+open import Sail_values
+open import Prompt
+
+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 false Read_plain addr size
+let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
+
+let MEMr_tag (addr,size)         = read_mem false Read_plain addr size
+let MEMr_tag_reserve (addr,size) = read_mem false Read_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_plain addr size
+let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size
+
+
+val MEMval                 : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bool
+val MEMval_tag             : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bool
+
+let MEMval (_,_,v)                 = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional (_,_,v)     = write_mem_val v >>= fun b -> return (if b then true else false)
+let MEMval_tag (_,_,v)             = write_mem_val v >>= fun _ -> return ()
+let MEMval_tag_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then true else false)
+
+(* TODO *)
+val TAGw : (vector bitU * vector bitU) -> M unit
+let TAGw (addr, tag) = failwith "TAGw not implemented"
+
+val MEM_sync  : unit -> M unit
+
+let MEM_sync () = barrier Barrier_Isync