Support for more sail constructs

Added support for:

* Register type declarations
* Undefined literals
* Exit statement
* Toplevel let statements
* Vector literals i.e. [a, b, c]
* Binary bitvector literals
* Hex bitvector literals

Patched the parser so you can actually write 2**'n - 1 in a nexp. The
parser rules for nexps are a bit strange, and there didn't seem to be
anyway to write this before without it causing a parse error.

Can now typecheck up to line 332 of mips_prelude in mips/, but need to
add support for the implict passing of registers by names to go any
further, which should be fun...

17 files changed, 219 insertions, 0 deletions

diff --git a/test/typecheck/fail/mips_CauseReg1.sail b/test/typecheck/fail/mips_CauseReg1.sail
new file mode 100644
index 00000000..ae99e625
--- /dev/null
+++ b/test/typecheck/fail/mips_CauseReg1.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 30 : 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;*)
+}
diff --git a/test/typecheck/fail/mips_CauseReg2.sail b/test/typecheck/fail/mips_CauseReg2.sail
new file mode 100644
index 00000000..683f5a2a
--- /dev/null
+++ b/test/typecheck/fail/mips_CauseReg2.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 3 ] {
+  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;*)
+}
diff --git a/test/typecheck/fail/mips_CauseReg3.sail b/test/typecheck/fail/mips_CauseReg3.sail
new file mode 100644
index 00000000..09e27e27
--- /dev/null
+++ b/test/typecheck/fail/mips_CauseReg3.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+  31       : BD; (* branch delay *)
+  (*30       : Z0;*)
+  32 .. 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;*)
+}
diff --git a/test/typecheck/fail/mips_CauseReg4.sail b/test/typecheck/fail/mips_CauseReg4.sail
new file mode 100644
index 00000000..1f14981f
--- /dev/null
+++ b/test/typecheck/fail/mips_CauseReg4.sail
@@ -0,0 +1,14 @@
+
+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; *)
+  8 .. 15  : IP; (* interrupt pending bits *)
+  (*7        : Z3;*)
+  6 .. 2   : ExcCode; (* code of last exception *)
+  (*1 .. 0   : Z4;*)
+}
diff --git a/test/typecheck/fail/mips_CauseReg5.sail b/test/typecheck/fail/mips_CauseReg5.sail
new file mode 100644
index 00000000..98fc614a
--- /dev/null
+++ b/test/typecheck/fail/mips_CauseReg5.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+  31       : BD; (* branch delay *)
+  (*30       : Z0;*)
+  29 .. 28 : CE; (* for coprocessor enable exception *)
+  (*27 .. 24 : Z1;*)
+  22       : IV; (* special interrupt vector not supported *)
+  23       : 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;*)
+}
diff --git a/test/typecheck/fail/mips_CauseReg6.sail b/test/typecheck/fail/mips_CauseReg6.sail
new file mode 100644
index 00000000..ecb8322e
--- /dev/null
+++ b/test/typecheck/fail/mips_CauseReg6.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+  31       : BD; (* branch delay *)
+  (*30       : Z0;*)
+  29 .. 28 : BD; (* 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;*)
+}
diff --git a/test/typecheck/fail/my_unsigned1.sail b/test/typecheck/fail/my_unsigned1.sail
new file mode 100644
index 00000000..958340ff
--- /dev/null
+++ b/test/typecheck/fail/my_unsigned1.sail
@@ -0,0 +1,8 @@
+
+default Order inc
+
+val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o >= 0, 'o + 1 <= 2**'m. vector<'n,'m,'ord,bit> -> [:'o:] effect pure my_unsigned
+
+let MAX = my_unsigned(0xff)
+
+let ([:0:]) MIN = MAX
\ No newline at end of file
diff --git a/test/typecheck/pass/cast_lexp2].sail b/test/typecheck/pass/cast_lexp2.sail
index a6f6d299..a6f6d299 100644
--- a/test/typecheck/pass/cast_lexp2].sail
+++ b/test/typecheck/pass/cast_lexp2.sail
diff --git a/test/typecheck/pass/exit1.sail b/test/typecheck/pass/exit1.sail
new file mode 100644
index 00000000..fa1de7e0
--- /dev/null
+++ b/test/typecheck/pass/exit1.sail
@@ -0,0 +1,8 @@
+
+val unit -> [:6:] effect pure test
+
+function [:6:] test () =
+{
+  exit ();
+  6
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/exit2.sail b/test/typecheck/pass/exit2.sail
new file mode 100644
index 00000000..40bf7da3
--- /dev/null
+++ b/test/typecheck/pass/exit2.sail
@@ -0,0 +1,7 @@
+
+val unit -> [:6:] effect pure test
+
+function [:6:] test () =
+{
+  exit ();
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/exit3.sail b/test/typecheck/pass/exit3.sail
new file mode 100644
index 00000000..9ac0aa78
--- /dev/null
+++ b/test/typecheck/pass/exit3.sail
@@ -0,0 +1,7 @@
+
+val forall Type 'a. unit -> 'a effect pure test
+
+function forall Type 'a. 'a test () =
+{
+  exit ();
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/mips_CauseReg1.sail b/test/typecheck/pass/mips_CauseReg1.sail
new file mode 100644
index 00000000..e05d0af8
--- /dev/null
+++ b/test/typecheck/pass/mips_CauseReg1.sail
@@ -0,0 +1,14 @@
+
+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;*)
+}
diff --git a/test/typecheck/pass/mips_CauseReg2.sail b/test/typecheck/pass/mips_CauseReg2.sail
new file mode 100644
index 00000000..f62824f1
--- /dev/null
+++ b/test/typecheck/pass/mips_CauseReg2.sail
@@ -0,0 +1,14 @@
+
+typedef CauseReg = register bits [ 31 : 1 ] {
+  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;*)
+}
diff --git a/test/typecheck/pass/mips_CauseReg3.sail b/test/typecheck/pass/mips_CauseReg3.sail
new file mode 100644
index 00000000..24b07fcd
--- /dev/null
+++ b/test/typecheck/pass/mips_CauseReg3.sail
@@ -0,0 +1,14 @@
+
+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 *)
+  23       : 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;*)
+}
diff --git a/test/typecheck/pass/mips_regtyps.sail b/test/typecheck/pass/mips_regtyps.sail
new file mode 100644
index 00000000..f7a3ce91
--- /dev/null
+++ b/test/typecheck/pass/mips_regtyps.sail
@@ -0,0 +1,53 @@
+
+(* mips_prelude.sail: declarations of mips registers, and functions common 
+   to mips instructions (e.g. address translation) *)
+
+(* bit vectors have indices decreasing from left i.e. msb is highest index *)
+default Order dec
+
+register (bit[64]) PC
+register (bit[64]) nextPC
+
+(* CP0 Registers *)
+
+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;*)
+}
+
+typedef TLBEntryLoReg = register bits [63 : 0] {
+  63      : CapS;
+  62      : CapL;
+  29 .. 6 : PFN;
+  5  .. 3 : C;
+  2       : D;
+  1       : V;
+  0       : G;
+}
+
+typedef TLBEntryHiReg = register bits [63 : 0] {
+  63 .. 62 : R;
+  39 .. 13 : VPN2;
+  7  ..  0 : ASID;
+}
+
+typedef ContextReg = register bits [63 : 0] {
+  63 .. 23 : PTEBase;
+  22 .. 4  : BadVPN2;
+  (*3  .. 0  : ZR;*)
+}
+
+typedef XContextReg = register bits [63 : 0] {
+  63 .. 33: PTEBase;
+  32 .. 31: R;
+  30 ..  4: BadVPN2;
+}
diff --git a/test/typecheck/pass/mips_tlbindext_dec.sail b/test/typecheck/pass/mips_tlbindext_dec.sail
new file mode 100644
index 00000000..af98cd85
--- /dev/null
+++ b/test/typecheck/pass/mips_tlbindext_dec.sail
@@ -0,0 +1,5 @@
+
+default Order dec
+
+typedef TLBIndexT = (bit[6])
+let (TLBIndexT) TLBIndexMax = 0b111111
diff --git a/test/typecheck/pass/mips_tlbindext_inc.sail b/test/typecheck/pass/mips_tlbindext_inc.sail
new file mode 100644
index 00000000..d64ffd68
--- /dev/null
+++ b/test/typecheck/pass/mips_tlbindext_inc.sail
@@ -0,0 +1,5 @@
+
+default Order inc
+
+typedef TLBIndexT = (bit[6])
+let (TLBIndexT) TLBIndexMax = 0b111111