8 files changed, 138 insertions, 4 deletions
diff --git a/test/typecheck/pass/mips_CauseReg3.sail b/test/typecheck/fail/mips_CauseReg7.sail
index 48acd4f5..48acd4f5 100644
--- a/test/typecheck/pass/mips_CauseReg3.sail
+++ b/test/typecheck/fail/mips_CauseReg7.sail
diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
index 68a6ee95..4dc63e71 100644
--- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
+++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
@@ -1,8 +1,6 @@
 val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv
 val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv
 
-val cast forall Type 'a, Type 'b. 'a -> 'b effect pure cast_anything
-    
 default Order dec
 
 typedef CauseReg = register bits [ 31 : 0 ] {
diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
index 9f3663d1..b35a0767 100644
--- a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
+++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
@@ -1,5 +1,5 @@
-val forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv
-val forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv
+val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv
+val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv
     
 default Order dec
 
diff --git a/test/typecheck/pass/mips_CP0Cause_access.sail b/test/typecheck/pass/mips_CP0Cause_access.sail
new file mode 100644
index 00000000..0ae1bb6f
--- /dev/null
+++ b/test/typecheck/pass/mips_CP0Cause_access.sail
@@ -0,0 +1,34 @@
+(* val forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1.
+  vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit>
+  effect pure ADJUST
+*)
+
+val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
+(*
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+*)
+    
+default Order dec
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+  31       : BD; (* branch delay *)
+  (*30       : Z0;*)
+  29 .. 28 : CE; (* for coprocessor enable exception *)
+  (*27 .. 24 : Z1;*)
+  23       : IV; (* special interrupt vector not supported *)
+  22       : WP; (* watchpoint exception occurred *)
+  (*21 .. 16 : Z2; *)
+  15 .. 8  : IP; (* interrupt pending bits *)
+  (*7        : Z3;*)
+  6 .. 2   : ExcCode; (* code of last exception *)
+  (*1 .. 0   : Z4;*)
+}
+
+register (CauseReg) CP0Cause
+
+val unit -> bit effect {rreg} test
+
+function bit test () =
+{
+  CP0Cause[30]
+}
diff --git a/test/typecheck/pass/mips_reg_field_bit.sail b/test/typecheck/pass/mips_reg_field_bit.sail
new file mode 100644
index 00000000..33560bde
--- /dev/null
+++ b/test/typecheck/pass/mips_reg_field_bit.sail
@@ -0,0 +1,28 @@
+val cast forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1.
+  vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit>
+  effect pure ADJUST
+
+default Order dec
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+  31       : BD; (* branch delay *)
+  (*30       : Z0;*)
+  29 .. 28 : CE; (* for coprocessor enable exception *)
+  (*27 .. 24 : Z1;*)
+  23       : IV; (* special interrupt vector not supported *)
+  22       : WP; (* watchpoint exception occurred *)
+  (*21 .. 16 : Z2; *)
+  15 .. 8  : IP; (* interrupt pending bits *)
+  (*7        : Z3;*)
+  6 .. 2   : ExcCode; (* code of last exception *)
+  (*1 .. 0   : Z4;*)
+}
+
+register (CauseReg) CP0Cause
+
+val unit -> unit effect {wreg} test
+
+function unit test () =
+{
+  (CP0Cause.CE)[28] := bitone
+}
diff --git a/test/typecheck/pass/mips_reg_field_bv.sail b/test/typecheck/pass/mips_reg_field_bv.sail
new file mode 100644
index 00000000..4b82d4de
--- /dev/null
+++ b/test/typecheck/pass/mips_reg_field_bv.sail
@@ -0,0 +1,28 @@
+val cast forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1.
+  vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit>
+  effect pure ADJUST
+
+default Order dec
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+  31       : BD; (* branch delay *)
+  (*30       : Z0;*)
+  29 .. 28 : CE; (* for coprocessor enable exception *)
+  (*27 .. 24 : Z1;*)
+  23       : IV; (* special interrupt vector not supported *)
+  22       : WP; (* watchpoint exception occurred *)
+  (*21 .. 16 : Z2; *)
+  15 .. 8  : IP; (* interrupt pending bits *)
+  (*7        : Z3;*)
+  6 .. 2   : ExcCode; (* code of last exception *)
+  (*1 .. 0   : Z4;*)
+}
+
+register (CauseReg) CP0Cause
+
+val unit -> unit effect {wreg} test
+
+function unit test () =
+{
+  CP0Cause.CE := 0b11
+}
diff --git a/test/typecheck/pass/overload_plus.sail b/test/typecheck/pass/overload_plus.sail
new file mode 100644
index 00000000..5390a5a4
--- /dev/null
+++ b/test/typecheck/pass/overload_plus.sail
@@ -0,0 +1,12 @@
+default Order inc
+
+val extern forall Nat 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc"
+  
+overload (deinfix +) [bv_add]
+
+val (bit[3], bit[3]) -> bit[3] effect pure test
+
+function bit[3] test (x, y) =
+{
+  x + y
+}
diff --git a/test/typecheck/pass/regtyp_vec.sail b/test/typecheck/pass/regtyp_vec.sail
new file mode 100644
index 00000000..5142208e
--- /dev/null
+++ b/test/typecheck/pass/regtyp_vec.sail
@@ -0,0 +1,34 @@
+(* val forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1.
+  vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit>
+  effect pure ADJUST
+*)
+
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
+(*
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+*)
+
+default Order dec
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+  31       : BD; (* branch delay *)
+  (*30       : Z0;*)
+  29 .. 28 : CE; (* for coprocessor enable exception *)
+  (*27 .. 24 : Z1;*)
+  23       : IV; (* special interrupt vector not supported *)
+  22       : WP; (* watchpoint exception occurred *)
+  (*21 .. 16 : Z2; *)
+  15 .. 8  : IP; (* interrupt pending bits *)
+  (*7        : Z3;*)
+  6 .. 2   : ExcCode; (* code of last exception *)
+  (*1 .. 0   : Z4;*)
+}
+
+register (CauseReg) CP0Cause
+
+val unit -> bit effect {rreg} test
+
+function bit test () =
+{
+  CP0Cause[30]
+}