More features in bi-directional typechecker

Can now typecheck:

* register fields in expressions, e.g. CP0Status.IM
* register fields in l-expressions, e.g. CP0Cause.CE := 0b00
* functions without valspecs, provided their types are easily inferable

Still need to be able to treat a register-typed register as a vector
for most of mips model to typecheck, as well as bitvector patterns,
but it's like 90% there.

6 files changed, 116 insertions, 0 deletions

diff --git a/test/typecheck/fail/mips_CP0Cause_BD_assign1.sail b/test/typecheck/fail/mips_CP0Cause_BD_assign1.sail
new file mode 100644
index 00000000..2f599aa9
--- /dev/null
+++ b/test/typecheck/fail/mips_CP0Cause_BD_assign1.sail
@@ -0,0 +1,27 @@
+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
+    
+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.BD := 2
+}
diff --git a/test/typecheck/fail/vector_append3.sail b/test/typecheck/fail/vector_append3.sail
new file mode 100644
index 00000000..82f0a861
--- /dev/null
+++ b/test/typecheck/fail/vector_append3.sail
@@ -0,0 +1,18 @@
+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
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val (bit[4], bit[4]) -> bit[7] effect pure test
+    
+function bit[7] test (v1, v2) =
+{
+  z := vector_access(v1, 3);
+  z := v1[0];
+  zv := vector_append(v1, v2);
+  zv := v1 : v2;
+  zv
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_arity.sail b/test/typecheck/fail/vector_arity.sail
new file mode 100644
index 00000000..6ecc9565
--- /dev/null
+++ b/test/typecheck/fail/vector_arity.sail
@@ -0,0 +1,4 @@
+
+val vector<0,5,inc,bit,bit> -> vector<0,5,inc,bit,bit> effect pure test
+
+function vector<0,5,inc,bit,bit> test x = x
\ No newline at end of file
diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
new file mode 100644
index 00000000..a3036e1f
--- /dev/null
+++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
@@ -0,0 +1,27 @@
+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
+    
+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.BD := 1
+}
diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
new file mode 100644
index 00000000..9f3663d1
--- /dev/null
+++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
@@ -0,0 +1,27 @@
+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
+    
+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.BD := 0
+}
diff --git a/test/typecheck/pass/vector_access_dec.sail b/test/typecheck/pass/vector_access_dec.sail
new file mode 100644
index 00000000..7516ba91
--- /dev/null
+++ b/test/typecheck/pass/vector_access_dec.sail
@@ -0,0 +1,13 @@
+
+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
+
+val bit[4] -> unit effect pure test
+    
+function unit test v =
+{
+  z := vector_access(v,3);
+  z := v[3]
+}
\ No newline at end of file