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.

2 files changed, 81 insertions, 27 deletions

diff --git a/lib/prelude.sail b/lib/prelude.sail
index 795fe8fc..fe5d7d5b 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -3,9 +3,9 @@ val cast forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m
 
 val forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0 - (2**('m - 1)):2**('m - 1) - 1|] effect pure signed
 
-val extern forall Num 'n, Num 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec = "to_vec_dec"
+val forall Num 'n, Num 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec
 
-val extern forall Num 'm. int -> vector<'m - 1,'m,dec,bit> effect pure to_svec = "to_vec_dec"
+val forall Num 'm. int -> vector<'m - 1,'m,dec,bit> effect pure to_svec
 
 (* Vector access can't actually be properly polymorphic on vector
    direction because of the ranges being different for each type, so
@@ -39,14 +39,14 @@ overload vector_subrange [bitvector_subrange_inc; bitvector_subrange_dec; vector
 
 (* Type safe vector append *)
 val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
-  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vec_append = "vector_concat"
-
-val (list<bit>, list<bit>) -> list<bit> effect pure list_append
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vector_append = "vector_concat"
 
 val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0.
-  (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,bit> effect pure bitvec_append = "bitvector_concat"
+  (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,bit> effect pure bitvector_append = "bitvector_concat"
+
+val (list<bit>, list<bit>) -> list<bit> effect pure list_append
 
-overload vector_append [bitvec_append; vec_append; list_append]
+overload append [bitvector_append; vector_append; list_append]
 
 (* Implicit register dereferencing *)
 val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref
@@ -65,27 +65,27 @@ val forall Num 'n, Num 'o, Order 'ord.
 overload (deinfix ^^) [duplicate; duplicate_bits; duplicate_to_list; duplicate_bits_to_list]
 
 (* Bitvector extension *)
-val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
     vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz
 
-val forall Num 'm, Num 'p, Order 'ord.
+val extern forall Num 'm, Num 'p, Order 'ord.
     list<bit> -> vector<'p, 'm, 'ord, bit> effect pure extz_bl
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
     vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts
 
-val forall Num 'm, Num 'p, Order 'ord.
+val extern forall Num 'm, Num 'p, Order 'ord.
     list<bit> -> vector<'p, 'm, 'ord, bit> effect pure exts_bl
 
 (* If we want an automatic bitvector extension, then this is the function to
    use, but I've disabled the cast because it hides signedness bugs. *)
-val (*cast*) forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'n.
+val extern (*cast*) forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'n.
     vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extzi
 
 overload EXTZ [extz; extz_bl]
 overload EXTS [exts; exts_bl]
 
-val forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o.
+val extern forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o.
     vector<'n, 'm, 'ord, 'a> -> vector<'p, 'o, 'ord, 'a> effect pure mask
 
 (* Adjust the start index of a decreasing bitvector *)
@@ -98,9 +98,12 @@ val cast forall Num 'n, Num 'm, Num 'o, 'n >= 'm - 1, 'o >= 'm - 1.
   effect pure adjust_dec
 
 (* Various casts from 0 and 1 to bitvectors *)
-val cast forall Num 'n, Num 'l, Order 'ord. [:0:] -> vector<'n,'l,'ord,bit> effect pure cast_0_vec
-val cast forall Num 'n, Num 'l, Order 'ord. [:1:] -> vector<'n,'l,'ord,bit> effect pure cast_1_vec
-val cast forall Num 'n, Num 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec
+val cast forall Num 'n, Num 'l. [:0:] -> vector<'n,'l,dec,bit> effect pure cast_0_vec_dec
+val cast forall Num 'n, Num 'l. [:1:] -> vector<'n,'l,dec,bit> effect pure cast_1_vec_dec
+val cast forall Num 'n, Num 'l. [|0:1|] -> vector<'n,'l,dec,bit> effect pure cast_01_vec_dec
+val cast forall Num 'n, Num 'l. [:0:] -> vector<'n,'l,inc,bit> effect pure cast_0_vec_inc
+val cast forall Num 'n, Num 'l. [:1:] -> vector<'n,'l,inc,bit> effect pure cast_1_vec_inc
+val cast forall Num 'n, Num 'l. [|0:1|] -> vector<'n,'l,inc,bit> effect pure cast_01_vec_inc
 
 val cast forall Num 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool
 val cast bit -> bool effect pure cast_bit_bool
@@ -113,7 +116,7 @@ val forall Num 'n, Num 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect p
 (* Arithmetic *)
 
 val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
-    ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add
+    ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add"
 
 val extern (nat, nat) -> nat effect pure add_nat = "add"
 
@@ -129,7 +132,7 @@ val forall Num 'n, Num 'o, Order 'ord.
     (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec
 
 val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
-    ([|'n:'m|], [|'o:'p|]) -> [|'n - 'p:'m - 'o|] effect pure sub
+    ([|'n:'m|], [|'o:'p|]) -> [|'n - 'p:'m - 'o|] effect pure sub_range = "sub"
 
 val extern (int, int) -> int effect pure sub_int = "sub"
 
@@ -146,7 +149,7 @@ overload (deinfix +) [
   add_vec;
   add_overflow_vec;
   add_vec_int;
-  add;
+  add_range;
   add_nat;
   add_int
 ]
@@ -155,26 +158,28 @@ overload (deinfix -) [
   sub_vec_int;
   sub_vec;
   sub_underflow_vec;
-  sub;
+  sub_range;
   sub_int
 ]
 
 val extern bool -> bit effect pure bool_to_bit = "bool_to_bitU"
 
-val (int, int) -> int effect pure mul_int
+val (int, int) -> int effect pure mult_int
+val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> [:'n * 'm:] effect pure mult_range = "mult_int"
 val forall Num 'n, Num 'o, Order 'ord.
-    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mul_vec
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mult_vec
 
 overload (deinfix * ) [
-  mul_vec;
-  mul_int
+  mult_vec;
+  mult;
+  mult_int
 ]
 
 val forall Num 'n, Num 'o, Order 'ord.
-    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mul_svec
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mult_svec
 
 overload (deinfix *_s) [
-  mul_svec
+  mult_svec
 ]
 
 val extern (bool, bool) -> bool effect pure bool_xor
@@ -281,7 +286,7 @@ val (int, int) -> int effect pure modulo
 
 overload (deinfix mod) [modulo]
 
-val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure vec_length = "length"
+val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure vector_length = "length"
 val forall Type 'a. list<'a> -> nat effect pure list_length
 
 val extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [:'m:] effect pure bitvector_length = "bvlength"
diff --git a/lib/prelude_wrappers.sail b/lib/prelude_wrappers.sail
new file mode 100644
index 00000000..4568f6ab
--- /dev/null
+++ b/lib/prelude_wrappers.sail
@@ -0,0 +1,49 @@
+val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,inc,bit> effect pure to_vec_inc
+function forall Num 'n, Num 'm. (vector<'m - 1,'m,dec,bit>) to_vec (n) = to_vec_dec ((sizeof 'm) - 1, sizeof 'm, n)
+
+function forall Num 'm. (vector<'m - 1,'m,dec,bit>) to_svec (n) = to_vec_dec ((sizeof 'm) - 1, sizeof 'm, n)
+
+(* Bitvector extension *)
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
+    ([:'p:], [:'m:], vector<'o, 'n, 'ord, bit>) -> vector<'p, 'm, 'ord, bit> effect pure extz' = "extz"
+function forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
+    (vector<'p, 'm, 'ord, bit>) extz (v) = extz' (sizeof 'p, sizeof 'm, v)
+
+val extern forall Num 'm, Num 'p, Order 'ord.
+    ([:'p:], [:'m:], list<bit>) -> vector<'p, 'm, 'ord, bit> effect pure extz_bl' = "extz_bl"
+function forall Num 'm, Num 'p, Order 'ord.
+    (vector<'p, 'm, 'ord, bit>) extz_bl (v) = extz_bl' (sizeof 'p, sizeof 'm, v)
+
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
+    ([:'p:], [:'m:], vector<'o, 'n, 'ord, bit>) -> vector<'p, 'm, 'ord, bit> effect pure exts' = "exts"
+function forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
+    (vector<'p, 'm, 'ord, bit>) exts (v) = exts' (sizeof 'p, sizeof 'm, v)
+
+val extern forall Num 'm, Num 'p, Order 'ord.
+    ([:'p:], [:'m:], list<bit>) -> vector<'p, 'm, 'ord, bit> effect pure exts_bl' = "exts_bl"
+function forall Num 'm, Num 'p, Order 'ord.
+    vector<'p, 'm, 'ord, bit> exts_bl (v) = exts_bl' (sizeof 'p, sizeof 'm, v)
+
+val extern forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o.
+    ([:'p:], [:'o:], vector<'n, 'm, 'ord, 'a>) -> vector<'p, 'o, 'ord, 'a> effect pure mask' = "extz"
+function forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o.
+    (vector<'p, 'o, 'ord, 'a>) mask (v) = mask' (sizeof 'p, sizeof 'o, v)
+
+(* Adjust the start index of a decreasing bitvector *)
+val extern forall Num 'n, Num 'm, Num 'o, 'n >= 'm - 1, 'o >= 'm - 1.
+  ([:'o:], vector<'n,'m,dec,bit>) -> vector<'o,'m,dec,bit>
+  effect pure adjust_dec' = "adjust_start_index"
+function forall Num 'n, Num 'm, Num 'o, 'n >= 'm - 1, 'o >= 'm - 1.
+  (vector<'o,'m,dec,bit>) adjust_dec (v) = adjust_dec' (sizeof 'o, v)
+
+(* Various casts from 0 and 1 to bitvectors *)
+function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_0_vec_dec i = to_vec_dec (sizeof 'n, sizeof 'l, i)
+function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_1_vec_dec i = to_vec_dec (sizeof 'n, sizeof 'l, i)
+function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_01_vec_dec i = to_vec_dec (sizeof 'n, sizeof 'l, i)
+function forall Num 'n, Num 'l. (vector<'n,'l,inc,bit>) cast_0_vec_inc i = to_vec_inc (sizeof 'n, sizeof 'l, i)
+function forall Num 'n, Num 'l. (vector<'n,'l,inc,bit>) cast_1_vec_inc i = to_vec_inc (sizeof 'n, sizeof 'l, i)
+function forall Num 'n, Num 'l. (vector<'n,'l,inc,bit>) cast_01_vec_inc i = to_vec_inc (sizeof 'n, sizeof 'l, i)
+
+val extern forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. ([:'n:], [:'m:], bit) -> vector<'n,'m,dec,bit> effect pure cast_bit_vec' = "cast_bit_vec"
+function forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. (vector<'n,'m,dec,bit>) cast_bit_vec b = cast_bit_vec' (sizeof 'n, sizeof 'm, b)