Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into experiments

2 files changed, 96 insertions, 30 deletions

diff --git a/lib/prelude.sail b/lib/prelude.sail
index 795fe8fc..b211def1 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"
 
-overload vector_append [bitvec_append; vec_append; list_append]
+val (list<bit>, list<bit>) -> list<bit> effect pure 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"
 
@@ -126,10 +129,13 @@ val forall Num 'n, Num 'o, Order 'ord.
     (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure add_vec_int
 
 val forall Num 'n, Num 'o, Order 'ord.
+    (int, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_int_vec
+
+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 +152,8 @@ overload (deinfix +) [
   add_vec;
   add_overflow_vec;
   add_vec_int;
-  add;
+  add_int_vec;
+  add_range;
   add_nat;
   add_int
 ]
@@ -155,26 +162,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
@@ -259,9 +268,9 @@ val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lt_atom_a
 val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gt_atom_atom = "gt"
 
 overload (deinfix >=) [gteq_atom_atom; gteq_range_atom; gteq_atom_range; gteq_vec; gteq_int]
-overload (deinfix >) [gt_atom_atom; gt_vec; gt_int]
+overload (deinfix >) [gt_atom_atom; gt_range_atom; gt_vec; gt_int]
 overload (deinfix <=) [lteq_atom_atom; lteq_range_atom; lteq_atom_range; lteq_vec; lteq_int]
-overload (deinfix <) [lt_atom_atom; lt_vec; lt_int]
+overload (deinfix <) [lt_atom_atom; lt_range_atom; lt_vec; lt_int]
 
 val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gteq_svec
 val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gt_svec
@@ -273,15 +282,23 @@ overload (deinfix <=_s) [lteq_svec]
 overload (deinfix >_s) [gt_svec]
 overload (deinfix >=_s) [gteq_svec]
 
+val extern forall Num 'n, Num 'm, Num 'o, 'o >= 'n. ([|'n:'m|], [:'o:]) -> [|'n:'o|] effect pure min_range_atom = "min"
+val extern (int, int) -> int effect pure min_int = "min"
+
+overload min [min_range_atom; min_int]
+
 val (int, int) -> int effect pure quotient
 
 overload (deinfix quot) [quotient]
 
 val (int, int) -> int effect pure modulo
+val extern forall Num 'm. (int, [:'m:]) -> [|0:'m - 1|] effect pure modulo_atom = "modulo"
+
+overload (deinfix mod) [modulo_atom; modulo]
 
-overload (deinfix mod) [modulo]
+val extern forall Num 'n. [:'n:] -> [:2** 'n:] effect pure pow2
 
-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)