Work on improving Sail error messages

- Modified how sail type error messages are displayed. The
  typechecker, rather than immediately outputing a string has a
  datatype for error types, which are the pretty-printed using a
  PPrint pretty-printer. Needs more work for all the error messages.

- Error messages now attempt to highlight the part of the file where
  the error occurred, by printing the line the error is on and
  highlighting where the error message is in red. Again, this needs to
  be made more robust, especially when the error messages span
  multiple lines.

Other things

- Improved new parser and lexer. Made the lexer & parser handling of
  colons simpler and more intuitive.

- Added some more typechecking test cases

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
 }