9 files changed, 116 insertions, 4 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/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/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
 }