Merge branch 'experiments' into mono-experiments

16 files changed, 152 insertions, 12 deletions

diff --git a/test/typecheck/fail/mismatch_return.sail b/test/typecheck/fail/mismatch_return.sail
new file mode 100644
index 00000000..85b8b636
--- /dev/null
+++ b/test/typecheck/fail/mismatch_return.sail
@@ -0,0 +1,7 @@
+
+val unit -> unit effect pure test
+
+function int test () =
+{
+  ()
+}
diff --git a/test/typecheck/fail/pure_record_arity.sail b/test/typecheck/fail/pure_record_arity.sail
new file mode 100644
index 00000000..846df2c3
--- /dev/null
+++ b/test/typecheck/fail/pure_record_arity.sail
@@ -0,0 +1,25 @@
+default Order dec
+
+typedef State = const struct forall Type 'a, Nat 'n. {
+  vector<0, 'n, dec, 'a> N;
+  vector<0, 1, dec, bit> Z;
+}
+
+register State procState
+
+let (State<bit,1>) myStateM = {
+  (State<bit,1>) r := undefined;
+  r.N := 0b1;
+  r.Z := 0b1;
+  r
+}
+
+let (State<bit,1>) myState = { N = 0b1; Z = 0b1 }
+
+val unit -> unit effect {undef} test
+
+function test () = {
+  (State<bit,1>) myState1 := undefined;
+  (State<bit,1>) myState2 := { N = undefined; Z = 0b1 };
+  (State<bit,1>) myState3 := { myState2 with N = 0b0 }
+}
diff --git a/test/typecheck/fail/vector_append_old.sail b/test/typecheck/fail/vector_append_old.sail
new file mode 100644
index 00000000..fb6018b9
--- /dev/null
+++ b/test/typecheck/fail/vector_append_old.sail
@@ -0,0 +1,14 @@
+
+val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat"
+
+default Order inc
+
+val (bit[4], bit[4]) -> bit[8] effect pure test
+
+function bit[8] test (v1, v2) =
+{
+  zv := vector_append(v1, v2);
+  zv := v1 : v2;
+  zv
+}
diff --git a/test/typecheck/pass/exist_subrange.sail b/test/typecheck/pass/exist_subrange.sail
new file mode 100644
index 00000000..de867b75
--- /dev/null
+++ b/test/typecheck/pass/exist_subrange.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+val forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *).
+  (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange
+
+function unit test ((bit[6]) xs) =
+{
+  (int) len := 4;
+  (exist 'n. [:'n:]) len := 5;
+  ys := xs[len .. 0];
+  ()
+}
diff --git a/test/typecheck/pass/exist_true.sail b/test/typecheck/pass/exist_true.sail
new file mode 100644
index 00000000..a30fb87b
--- /dev/null
+++ b/test/typecheck/pass/exist_true.sail
@@ -0,0 +1,7 @@
+
+function unit test () =
+{
+  (exist 'n. [:'n:]) x := 4;
+  (exist 'n, true. [:'n:]) y := 5;
+  ()
+}
diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail
index 83313ac7..cc84130f 100644
--- a/test/typecheck/pass/lexp_memory.sail
+++ b/test/typecheck/pass/lexp_memory.sail
@@ -48,7 +48,10 @@ val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'or
 
 overload (deinfix ==) [eq_vec]
 
-val cast forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec
+val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+
+val cast forall Nat 'n, Nat 'l. [|0:1|] -> vector<'n,'l,dec,bit> effect pure cast_01_vec
+function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_01_vec i = to_vec_dec (sizeof 'n, sizeof 'l, i)
 val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned
 val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref
 
diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
index 7808b2c0..0160dd8a 100644
--- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
+++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
@@ -1,5 +1,10 @@
-val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec
-val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec
+val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec
+val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec
+
+val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+
+function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i)
+function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i)
 
 default Order dec
 
diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
index 26f161e2..847bca60 100644
--- a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
+++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
@@ -1,6 +1,11 @@
-val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec
-val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec
+val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec
+val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec
     
+val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+
+function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i)
+function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i)
+
 default Order dec
 
 typedef CauseReg = register bits [ 31 : 0 ] {
diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail
new file mode 100644
index 00000000..a0a85313
--- /dev/null
+++ b/test/typecheck/pass/pure_record2.sail
@@ -0,0 +1,22 @@
+default Order dec
+
+typedef State = const struct forall Type 'a, Nat 'n. {
+  vector<0, 'n, dec, 'a> N;
+  vector<0, 1, dec, bit> Z;
+}
+
+let (State<bit,1>) myStateM = {
+  (State<bit,1>) r := undefined;
+  r.N := 0b1;
+  r.Z := 0b1;
+  r
+}
+
+let (State<bit,1>) myState = { N = 0b1; Z = 0b1 }
+
+val unit -> unit effect {undef} test
+
+function test () = {
+  (State<bit,1>) myState2 := { N = undefined; Z = 0b1 };
+  (State<bit,1>) myState3 := { myState2 with N = 0b0 }
+}
diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail
new file mode 100644
index 00000000..61d74ebf
--- /dev/null
+++ b/test/typecheck/pass/pure_record3.sail
@@ -0,0 +1,25 @@
+default Order dec
+
+typedef State = const struct forall Type 'a, Nat 'n. {
+  vector<0, 'n, dec, 'a> N;
+  vector<0, 1, dec, bit> Z;
+}
+
+register State<bit,1> procState
+
+let (State<bit,1>) myStateM = {
+  (State<bit,1>) r := undefined;
+  r.N := 0b1;
+  r.Z := 0b1;
+  r
+}
+
+let (State<bit,1>) myState = { N = 0b1; Z = 0b1 }
+
+val unit -> unit effect {undef} test
+
+function test () = {
+  (State<bit,1>) myState1 := undefined;
+  (State<bit,1>) myState2 := { N = undefined; Z = 0b1 };
+  (State<bit,1>) myState3 := { myState2 with N = 0b0 }
+}
diff --git a/test/typecheck/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail
index 7bc7370b..af0b5ba2 100644
--- a/test/typecheck/pass/set_mark.sail
+++ b/test/typecheck/pass/set_mark.sail
@@ -1,5 +1,10 @@
 
-val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec
+val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+
+val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec
+function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i)
+
+default Order dec
 
 function forall Num 'N, 'N IN {32}. bit['N] Foo32( (bit['N]) x) = x
 
diff --git a/test/typecheck/pass/set_mark2.sail b/test/typecheck/pass/set_mark2.sail
index cabfb1af..591c17ad 100644
--- a/test/typecheck/pass/set_mark2.sail
+++ b/test/typecheck/pass/set_mark2.sail
@@ -1,4 +1,10 @@
-val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec
+
+val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+
+val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec
+function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i)
+
+default Order dec
 
 function forall Nat 'N, 'N IN {32, 64}. bit['N] Foo32( (bit['N]) x) = x
 
diff --git a/test/typecheck/pass/varity.sail b/test/typecheck/pass/varity.sail
index d196f777..750d70eb 100644
--- a/test/typecheck/pass/varity.sail
+++ b/test/typecheck/pass/varity.sail
@@ -3,6 +3,10 @@ val int -> unit effect pure f1
 val (int, int) -> unit effect pure f2
 val (int, int, int) -> unit effect pure f3
 
+function f1 (i1) = ()
+function f2 (i1, i2) = ()
+function f3 (i1, i2, i3) = ()
+
 overload f [f1; f2; f3]
 
 val unit -> unit effect pure test
diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail
index fe9b4a0a..b22f0029 100644
--- a/test/typecheck/pass/vec_pat1.sail
+++ b/test/typecheck/pass/vec_pat1.sail
@@ -10,7 +10,7 @@ val forall Num 'n, Num 'm, Num 'o, Num 'p.
   effect pure bitvector_concat
 
 overload (deinfix +) [bv_add]
-overload vector_append [bitvector_concat]
+overload append [bitvector_concat]
 
 val (bit[3], bit[3]) -> bit[3] effect pure test
 
diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail
index 17db3fbd..df610fb1 100644
--- a/test/typecheck/pass/vector_append.sail
+++ b/test/typecheck/pass/vector_append.sail
@@ -1,14 +1,14 @@
 
 val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0.
-  (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat"
+  (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure append = "bitvector_concat"
 
 default Order inc
 
 val (bit[4], bit[4]) -> bit[8] effect pure test
-    
+
 function bit[8] test (v1, v2) =
 {
-  zv := vector_append(v1, v2);
+  zv := append(v1, v2);
   zv := v1 : v2;
   zv
 }
diff --git a/test/typecheck/pass/vector_synonym_cast.sail b/test/typecheck/pass/vector_synonym_cast.sail
index f1de42e9..bd0acaa6 100644
--- a/test/typecheck/pass/vector_synonym_cast.sail
+++ b/test/typecheck/pass/vector_synonym_cast.sail
@@ -1,7 +1,7 @@
 
 typedef vecsyn = vector<0,1,dec,bit>
 
-val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure adjust_dec
+val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure norm_dec
 
 val vector<1,1,dec,bit> -> vecsyn effect pure test