Merge branch 'sail2' into monads

109 files changed, 1344 insertions, 465 deletions

diff --git a/test/arm/run_tests.sh b/test/arm/run_tests.sh
index 30f955b0..b24cc584 100755
--- a/test/arm/run_tests.sh
+++ b/test/arm/run_tests.sh
@@ -5,9 +5,9 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 cd $DIR
 SAILDIR="$DIR/../.."
 
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
+RED='\033[0;91m'
+GREEN='\033[0;92m'
+YELLOW='\033[0;93m'
 NC='\033[0m'
 
 rm -f $DIR/tests.xml
diff --git a/test/builtins/get_slice_int.sail b/test/builtins/get_slice_int.sail
index b64526d2..ef673daf 100644
--- a/test/builtins/get_slice_int.sail
+++ b/test/builtins/get_slice_int.sail
@@ -199,7 +199,8 @@ function main (() : unit) -> unit = {
   assert(get_slice_int(4, 6, 0) == 4^0x6, "get_slice_int(4, 6, 0) == 4^0x6");
   assert(get_slice_int(4, 7, 0) == 4^0x7, "get_slice_int(4, 7, 0) == 4^0x7");
   assert(get_slice_int(4, 8, 0) == 4^0x8, "get_slice_int(4, 8, 0) == 4^0x8");
-  assert(get_slice_int(4, undefined, 0) == 4^0x0, "get_slice_int(4, undefined, 0) == 4^0x0");
+  // Not sure we want this property!
+  // assert(get_slice_int(4, undefined, 0) == 4^0x0, "get_slice_int(4, undefined, 0) == 4^0x0");
   assert(get_slice_int(5, 0, 0) == 5^0x0, "get_slice_int(5, 0, 0) == 5^0x0");
   assert(get_slice_int(5, 1, 0) == 5^0x1, "get_slice_int(5, 1, 0) == 5^0x1");
   assert(get_slice_int(5, 17, 0) == 5^0x11, "get_slice_int(5, 17, 0) == 5^0x11");
diff --git a/test/builtins/run_tests.py b/test/builtins/run_tests.py
index e1f2927e..b20d4224 100755
--- a/test/builtins/run_tests.py
+++ b/test/builtins/run_tests.py
@@ -13,9 +13,10 @@ from sailtest import *
 
 def test_c_builtins(name, sail_opts):
     banner('Testing builtins: {} Sail options: {}'.format(name, sail_opts))
-    tests = {}
-    for filename in os.listdir('.'):
-        if re.match('.+\.sail', filename):
+    results = Results(name)
+    for filenames in chunks(os.listdir('.'), parallel()):
+        tests = {}
+        for filename in filenames:
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
@@ -26,13 +27,16 @@ def test_c_builtins(name, sail_opts):
                 step('rm {}'.format(basename))
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
                 sys.exit()
+        results.collect(tests)
+    return results.finish()
     return collect_results(name, tests)
 
 def test_ocaml_builtins(name, sail_opts):
     banner('Testing builtins: {} Sail options: {}'.format(name, sail_opts))
-    tests = {}
-    for filename in os.listdir('.'):
-        if re.match('.+\.sail', filename):
+    results = Results(name)
+    for filenames in chunks(os.listdir('.'), parallel()):
+        tests = {}
+        for filename in filenames:
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
@@ -42,13 +46,16 @@ def test_ocaml_builtins(name, sail_opts):
                 step('rm {}'.format(basename))
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
                 sys.exit()
+        results.collect(tests)
+    return results.finish()
     return collect_results(name, tests)
 
 def test_lem_builtins(name):
     banner('Testing builtins: {}'.format(name))
-    tests = {}
-    for filename in os.listdir('.'):
-        if re.match('.+\.sail', filename):
+    results = Results(name)
+    for filenames in chunks(os.listdir('.'), parallel()):
+        tests = {}
+        for filename in filenames:
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
@@ -76,7 +83,8 @@ def test_lem_builtins(name):
 
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
                 sys.exit()
-    return collect_results(name, tests)
+        results.collect(tests)
+    return results.finish()
 
 xml = '<testsuites>\n'
 
diff --git a/test/builtins/run_tests.sh b/test/builtins/run_tests.sh
deleted file mode 100755
index eeb57a79..00000000
--- a/test/builtins/run_tests.sh
+++ /dev/null
@@ -1,140 +0,0 @@
-
-#!/usr/bin/env bash
-set -e
-
-DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
-cd $DIR
-SAILDIR="$DIR/../.."
-LEMBUILDDIR="$DIR/_lembuild"
-
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
-NC='\033[0m'
-
-rm -f $DIR/tests.xml
-
-pass=0
-fail=0
-XML=""
-
-function green {
-    (( pass += 1 ))
-    printf "$1: ${GREEN}$2${NC}\n"
-    XML+="    <testcase name=\"$1\"/>\n"
-}
-
-function yellow {
-    (( fail += 1 ))
-    printf "$1: ${YELLOW}$2${NC}\n"
-    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
-}
-
-function red {
-    (( fail += 1 ))
-    printf "$1: ${RED}$2${NC}\n"
-    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
-}
-
-function finish_suite {
-    printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n"
-    XML="  <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML  </testsuite>\n"
-    printf "$XML" >> $DIR/tests.xml
-    XML=""
-    pass=0
-    fail=0
-}
-
-printf "<testsuites>\n" >> $DIR/tests.xml
-
-shopt -s nullglob;
-for file in $DIR/*.sail;
-do
-    if $SAILDIR/sail -no_warn -c -O $file 1> ${file%.sail}.c 2> /dev/null;
-    then
-	green "compiling $(basename $file) (C)" "ok";
-	if gcc -I $SAILDIR/lib/ ${file%.sail}.c -lgmp;
-	then
-	    green "compiling $(basename ${file%.sail}.c)" "ok";
-	    if $DIR/a.out;
-	    then
-		green "tested $(basename ${file%.sail}) (C)" "ok"
-	    else
-		red "tested $(basename ${file%.sail}) (C)" "fail"
-	    fi
-	else
-	    red "compiling $file" "fail"
-	fi
-    else
-	red "compiling $file" "fail"
-    fi;
-
-    # if $SAILDIR/sail -no_warn -o out -ocaml $file 1> /dev/null 2> /dev/null;
-    # then
-    # 	green "compiling $(basename $file) (OCaml)" "ok"
-    # 	if $DIR/out;
-    # 	then
-    # 	    green "tested $(basename ${file%.sail}) (OCaml)" "ok"
-    # 	else
-    # 	    red "tested $(basename ${file%.sail}) (OCaml)" "fail"
-    # 	fi
-    # else
-    # 	red "compiling $(basename $file) (OCaml)" "fail"
-    # fi;
-
-    # mkdir -p "$LEMBUILDDIR"
-
-    # if "$SAILDIR/sail" -no_warn -lem -lem_mwords -lem_lib Test_extras -undefined_gen -o out "$file" 1> /dev/null 2> /dev/null;
-    # then
-    #     mv out.lem out_types.lem "$LEMBUILDDIR"
-    #     if lem -ocaml -lib "$SAILDIR/src/lem_interp" \
-    #            -outdir "$LEMBUILDDIR" \
-    #            "$SAILDIR/src/gen_lib/sail_values.lem" \
-    #            "$SAILDIR/src/gen_lib/sail_operators.lem" \
-    #            "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" \
-    #            "$SAILDIR/src/lem_interp/sail_instr_kinds.lem" \
-    #            "$SAILDIR/src/gen_lib/prompt.lem" \
-    #            "$SAILDIR/src/gen_lib/state_monad.lem" \
-    #            "$SAILDIR/src/gen_lib/state.lem" \
-    #            "$SAILDIR/src/gen_lib/prompt_monad.lem" \
-    #            "test_extras.lem" "$LEMBUILDDIR/out_types.lem" "$LEMBUILDDIR/out.lem" 1> /dev/null 2> /dev/null;
-    #     then
-    #         cd "$LEMBUILDDIR"
-    #         if ocamlfind ocamlc -linkpkg -package zarith -package lem \
-    #                      sail_values.ml sail_operators.ml \
-    #                      sail_instr_kinds.ml prompt_monad.ml prompt.ml \
-    #                      sail_operators_mwords.ml state_monad.ml state.ml \
-    #                      test_extras.ml out_types.ml out.ml ../test.ml \
-    #                      -o test 1> /dev/null 2> /dev/null
-    #         then
-    #             green "compiling $(basename $file) (Lem)" "ok"
-    #             if ./test 1> /dev/null 2> /dev/null
-    #             then
-    # 	            green "tested $(basename ${file%.sail}) (Lem)" "ok"
-    #             else
-    # 	            red "tested $(basename ${file%.sail}) (Lem)" "fail"
-    #             fi
-    #         else
-    #             red "compiling $(basename $file) (Sail->Lem->Ocaml->Bytecode)" "fail"
-    #         fi
-    #         cd "$DIR"
-    #     else
-    #         red "compiling $(basename $file) (Sail->Lem->Ocaml)" "fail"
-    #     fi
-    # else
-    #     red "compiling $(basename $file) (Sail->Lem)" "fail"
-    # fi;
-
-    rm -rf $DIR/_sbuild/;
-    rm -rf "$LEMBUILDDIR";
-    rm -f Out_lemmas.thy;
-    rm -f out_types.lem;
-    rm -f out.lem;
-    rm -f ${file%.sail}.c;
-    rm -f a.out;
-    rm -f out
-done
-
-finish_suite "builtin testing"
-
-printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/c/cfold_reg.expect b/test/c/cfold_reg.expect
new file mode 100644
index 00000000..27ba77dd
--- /dev/null
+++ b/test/c/cfold_reg.expect
@@ -0,0 +1 @@
+true
diff --git a/test/c/cfold_reg.sail b/test/c/cfold_reg.sail
new file mode 100644
index 00000000..a5090e91
--- /dev/null
+++ b/test/c/cfold_reg.sail
@@ -0,0 +1,30 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "eq_string" : (string, string) -> bool
+
+overload operator == = {eq_string}
+
+register R : bool
+
+val "print_endline" : string -> unit
+
+function IMPDEF(str : string) -> bool = {
+  if str == "A" then {
+    return(R)
+  } else if str == "B" then {
+    true
+  } else {
+    false
+  }
+}
+
+function main(() : unit) -> unit = {
+  R = true;
+  if IMPDEF("A") then {
+    print_endline("true")
+  } else {
+    print_endline("false")
+  }
+}
\ No newline at end of file
diff --git a/test/c/cheri128_hsb.expect b/test/c/cheri128_hsb.expect
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/test/c/cheri128_hsb.expect
diff --git a/test/c/cheri128_hsb.sail b/test/c/cheri128_hsb.sail
new file mode 100644
index 00000000..d8501d88
--- /dev/null
+++ b/test/c/cheri128_hsb.sail
@@ -0,0 +1,62 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <option.sail>
+$include <vector_dec.sail>
+$include <exception_basic.sail>
+
+val modulus = {ocaml: "modulus", lem: "hardware_mod", coq: "euclid_modulo", _ : "tmod_int"} : forall 'n, 'n > 0 .  (int, atom('n)) -> range(0, 'n - 1)
+
+val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range", c: "add_int"} : forall 'n 'm 'o 'p.
+  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
+
+val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
+  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
+
+val min = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c == 'a | 'c == 'b) & 'c <= 'a & 'c <= 'b . atom('c)}
+
+overload operator + = {add_range}
+overload operator - = {sub_range}
+
+infix 1 >>
+infix 1 <<
+
+val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
+val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
+
+val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
+val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
+
+overload operator >> = {shift_bits_right, shiftr}
+overload operator << = {shift_bits_left, shiftl}
+
+val HighestSetBit : forall 'N , 'N >= 2. bits('N) -> {'n, 0 <= 'n < 'N . (bool, atom('n))}
+
+function HighestSetBit x = {
+  foreach (i from ('N - 1) to 0 by 1 in dec)
+    if [x[i]] == 0b1 then return (true, i);
+  return (false, 0)
+}
+
+/* hw rounds up E to multiple of 4 */
+function roundUp(e) : range(0, 45) -> range(0, 48) =
+    let 'r = modulus(e, 4) in
+    if (r == 0)
+    then e
+    else (e - r + 4)
+
+function computeE (rlength) : bits(65) -> range(0, 48) =
+    let (nonzero, 'msb) = HighestSetBit((rlength + (rlength >> 6)) >> 19) in
+    if nonzero then
+      /* above will always return <= 45 because 19 bits of zero are shifted in from right */
+      {assert(0 <= msb & msb <= 45); roundUp (min(msb,45)) }
+    else
+      0
+
+val main : unit -> unit effect {escape}
+
+function main() = {
+  let _ = computeE(0xFFFF_FFFF_FFFF_FFFF @ 0b1);
+  ()
+}
\ No newline at end of file
diff --git a/test/c/cheri_capstruct_order.expect b/test/c/cheri_capstruct_order.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/cheri_capstruct_order.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/cheri_capstruct_order.sail b/test/c/cheri_capstruct_order.sail
new file mode 100644
index 00000000..6eb774dd
--- /dev/null
+++ b/test/c/cheri_capstruct_order.sail
@@ -0,0 +1,32 @@
+default Order dec
+
+val SignalException : unit -> unit effect {rreg}
+
+val SignalExceptionBadAddr : unit -> unit effect {rreg}
+
+function SignalExceptionBadAddr() = {
+    SignalException();
+}
+
+struct CapStruct = {
+    base : bool,
+}
+
+type CapReg = CapStruct
+
+function getCapBase(c)   : CapStruct -> bool = c.base
+
+register KCC : CapReg
+
+function SignalException () = {
+    base = getCapBase(KCC);
+    ();
+}
+
+val "print_endline" : string -> unit
+
+val main : unit -> unit
+
+function main() = {
+  print_endline("ok")
+}
\ No newline at end of file
diff --git a/test/c/config.expect b/test/c/config.expect
new file mode 100644
index 00000000..059a413f
--- /dev/null
+++ b/test/c/config.expect
@@ -0,0 +1,6 @@
+x = 3
+Hello
+z = 0xFF
+x = 4
+World
+z = 0xAA
diff --git a/test/c/config.sail b/test/c/config.sail
new file mode 100644
index 00000000..2902d259
--- /dev/null
+++ b/test/c/config.sail
@@ -0,0 +1,34 @@
+default Order dec
+
+$include <arith.sail>
+$include <vector_dec.sail>
+
+val "print" : string -> unit
+
+register q : int
+
+register configuration x : int = 3
+
+register configuration y : string = "Hello\n"
+
+register configuration z : bits(8) = 0xFF
+
+val init : unit -> unit effect {configuration}
+
+function init() = {
+  x = 4;
+  y = "World\n";
+  z = 0xAA;
+}
+
+val main : unit -> unit effect {configuration}
+
+function main() = {
+  print_int("x = ", x);
+  print(y);
+  print_bits("z = ", z);
+  init();
+  print_int("x = ", x);
+  print(y);
+  print_bits("z = ", z);
+}
\ No newline at end of file
diff --git a/test/c/config_register.expect b/test/c/config_register.expect
new file mode 100644
index 00000000..8d164b5c
--- /dev/null
+++ b/test/c/config_register.expect
@@ -0,0 +1 @@
+R = 0x00000000
diff --git a/test/c/config_register.sail b/test/c/config_register.sail
new file mode 100644
index 00000000..f4831ca5
--- /dev/null
+++ b/test/c/config_register.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+function zeros forall 'n. (() : unit) -> bits('n) = {
+  sail_zeros('n)
+}
+
+register configuration R : bits(32) = zeros()
+
+register S : bits(32)
+
+function main(() : unit) -> unit = {
+    R = zeros();
+    print_bits("R = ", R)
+}
\ No newline at end of file
diff --git a/test/c/custom_flow.expect b/test/c/custom_flow.expect
new file mode 100644
index 00000000..cf275436
--- /dev/null
+++ b/test/c/custom_flow.expect
@@ -0,0 +1,5 @@
+1
+2
+3
+4
+4
diff --git a/test/c/custom_flow.sail b/test/c/custom_flow.sail
new file mode 100644
index 00000000..43c980d6
--- /dev/null
+++ b/test/c/custom_flow.sail
@@ -0,0 +1,43 @@
+val "print_endline" : string -> unit
+
+val operator <= = {
+  coq: "Z.leb",
+  _: "lteq"
+} : forall 'n 'm. (int('n), int('m)) -> bool('n <= 'm)
+
+function test1 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  if n <= m then {
+    _prove(constraint('n <= 'm));
+    print_endline("1");
+  } else {
+    print_endline("2");
+    _prove(constraint('n > 'm));
+  }
+}
+
+val and_bool = {
+  coq: "andb",
+  _: "and_bool"
+} : forall ('p: Bool) ('q: Bool). (bool('p), bool('q)) -> bool('p & 'q)
+
+overload operator & = {and_bool}
+
+function test2 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  let x = n <= m & n <= 20;
+  if x then {
+    _prove(constraint('n <= 20));
+    _prove(constraint('n <= 'm));
+    print_endline("3")
+  } else {
+    _prove(constraint('n > 'm | 'n > 20));
+    print_endline("4")
+  }
+}
+
+function main((): unit) -> unit = {
+  test1(1, 2);
+  test1(2, 1);
+  test2(1, 2);
+  test2(2, 1);
+  test2(21, 0)
+}
\ No newline at end of file
diff --git a/test/c/list_test.sail b/test/c/list_test.sail
index c315d3bf..b89e0f47 100644
--- a/test/c/list_test.sail
+++ b/test/c/list_test.sail
@@ -20,8 +20,8 @@ val main : unit -> unit
 
 function main () = {
   let x : list(int) = [|1, 2, 3|];
-  let y = hd(0 : int, x);
+  let y : int = hd(0, x);
   print_int("y = ", y);
-  print_int("hd(tl(x)) = ", hd(0, tl(x)));
-  print_int("hd(tl(tl(x))) = ", hd(0, tl(tl(x))));
+  print_int("hd(tl(x)) = ", hd(0, tl(x)) : int);
+  print_int("hd(tl(tl(x))) = ", hd(0, tl(tl(x))) : int);
 }
\ No newline at end of file
diff --git a/test/c/non_unique.expect b/test/c/non_unique.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/non_unique.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/non_unique.sail b/test/c/non_unique.sail
new file mode 100644
index 00000000..eda7720d
--- /dev/null
+++ b/test/c/non_unique.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+function f(_: int) -> unit = ()
+function g(_: bits(1)) -> unit = ()
+
+function main(() : unit) -> unit = {
+  let y : int = {
+    let x : int = 3;
+    x
+  };
+  {
+    let x : bits(1) = 0b0;
+    g(x)
+  };
+  print_endline("ok");
+}
\ No newline at end of file
diff --git a/test/c/poly_pair.sail b/test/c/poly_pair.sail
index 6d0bdaad..c4989829 100644
--- a/test/c/poly_pair.sail
+++ b/test/c/poly_pair.sail
@@ -4,7 +4,7 @@ val print = "print_endline" : string -> unit
 
 val "eq_int" : (int, int) -> bool
 
-union test ('a : Type) ('b : Type) = {
+union test('a : Type, 'b : Type) = {
   Ctor1 : ('a, 'b),
   Ctor2 : int
 }
diff --git a/test/c/run_tests.py b/test/c/run_tests.py
index 6cd75981..4f221636 100755
--- a/test/c/run_tests.py
+++ b/test/c/run_tests.py
@@ -13,9 +13,10 @@ from sailtest import *
 
 def test_c(name, c_opts, sail_opts, valgrind):
     banner('Testing {} with C options: {} Sail options: {} valgrind: {}'.format(name, c_opts, sail_opts, valgrind))
-    tests = {}
-    for filename in os.listdir('.'):
-        if re.match('.+\.sail', filename):
+    results = Results(name)
+    for filenames in chunks(os.listdir('.'), parallel()):
+        tests = {}
+        for filename in filenames:
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
@@ -27,13 +28,15 @@ def test_c(name, c_opts, sail_opts, valgrind):
                     step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=1 ./{}".format(basename))
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
                 sys.exit()
-    return collect_results(name, tests)
+        results.collect(tests)
+    return results.finish()
 
 def test_interpreter(name):
     banner('Testing {}'.format(name))
-    tests = {}
-    for filename in os.listdir('.'):
-        if re.match('.+\.sail', filename):
+    results = Results(name)
+    for filenames in chunks(os.listdir('.'), parallel()):
+        tests = {}
+        for filename in filenames:
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
@@ -41,13 +44,15 @@ def test_interpreter(name):
                 step('diff {}.iresult {}.expect'.format(basename, basename))
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
                 sys.exit()
-    return collect_results(name, tests)
+        results.collect(tests)
+    return results.finish()
 
 def test_ocaml(name):
     banner('Testing {}'.format(name))
-    tests = {}
-    for filename in os.listdir('.'):
-        if re.match('.+\.sail', filename):
+    results = Results(name)
+    for filenames in chunks(os.listdir('.'), parallel()):
+        tests = {}
+        for filename in filenames:
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
@@ -56,13 +61,15 @@ def test_ocaml(name):
                 step('diff {}.oresult {}.expect'.format(basename, basename))
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
                 sys.exit()
-    return collect_results(name, tests)
+        results.collect(tests)
+    return results.finish()
 
 xml = '<testsuites>\n'
 
 xml += test_c('unoptimized C', '', '', True)
 xml += test_c('optimized C', '-O2', '-O', True)
 xml += test_c('constant folding', '', '-Oconstant_fold', True)
+xml += test_c('full optimizations', '-O2 -mbmi2 -DINTRINSICS', '-O -Oconstant_fold', True)
 xml += test_c('address sanitised', '-O2 -fsanitize=undefined', '-O', False)
 
 xml += test_interpreter('interpreter')
diff --git a/test/c/run_tests.sh b/test/c/run_tests.sh
deleted file mode 100755
index 37787605..00000000
--- a/test/c/run_tests.sh
+++ /dev/null
@@ -1,98 +0,0 @@
-
-#!/usr/bin/env bash
-set -e
-
-DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
-cd $DIR
-SAILDIR="$DIR/../.."
-
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
-NC='\033[0m'
-
-rm -f $DIR/tests.xml
-
-pass=0
-fail=0
-XML=""
-
-function green {
-    (( pass += 1 ))
-    printf "$1: ${GREEN}$2${NC}\n"
-    XML+="    <testcase name=\"$1\"/>\n"
-}
-
-function yellow {
-    (( fail += 1 ))
-    printf "$1: ${YELLOW}$2${NC}\n"
-    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
-}
-
-function red {
-    (( fail += 1 ))
-    printf "$1: ${RED}$2${NC}\n"
-    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
-}
-
-function finish_suite {
-    printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n"
-    XML="  <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML  </testsuite>\n"
-    printf "$XML" >> $DIR/tests.xml
-    XML=""
-    pass=0
-    fail=0
-}
-
-printf "<testsuites>\n" >> $DIR/tests.xml
-
-shopt -s nullglob;
-
-function run_c_tests {
-    for file in $DIR/*.sail;
-    do
-	if $SAILDIR/sail -no_warn -c $SAIL_OPTS $file 1> ${file%.sail}.c 2> /dev/null;
-	then
-	    green "compiling $(basename $file) ($SAIL_OPTS)" "ok";
-	    if gcc $CC_OPTS ${file%.sail}.c $SAILDIR/lib/*.c -lgmp -lz -I $SAILDIR/lib;
-	    then
-		green "compiling $(basename ${file%.sail}.c) ($CC_OPTS)" "ok";
-		$DIR/a.out 1> ${file%.sail}.result 2> /dev/null;
-		if diff ${file%.sail}.result ${file%.sail}.expect;
-		then
-		    green "executing $(basename ${file%.sail})" "ok"
-		else
-		    red "executing $(basename ${file%.sail})" "fail"
-		fi;
-		if valgrind -q --leak-check=full --errors-for-leak-kinds=all --error-exitcode=1 $DIR/a.out 1> /dev/null 2> /dev/null;
-		then
-		    green "executing $(basename ${file%.sail}) with valgrind" "ok"
-		else
-		    red "executing $(basename ${file%.sail}) with valgrind" "fail"
-		fi
-	    else
-		red "compiling generated C" "fail"
-	    fi
-	else
-	    red "compiling $file" "fail"
-	fi;
-	rm -f ${file%.sail}.c
-	rm -f ${file%.sail}.result
-    done
-}
-
-SAIL_OPTS=""
-CC_OPTS="-O0"
-run_c_tests
-
-SAIL_OPTS="-O"
-CC_OPTS="-O2"
-run_c_tests
-
-SAIL_OPTS="-O"
-CC_OPTS="-O2 -fsanitize=undefined"
-run_c_tests
-
-finish_suite "C testing"
-
-printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/c/small_slice.expect b/test/c/small_slice.expect
new file mode 100644
index 00000000..64d39581
--- /dev/null
+++ b/test/c/small_slice.expect
@@ -0,0 +1,2 @@
+v1 = 0x1234
+v2 = 0x34
diff --git a/test/c/small_slice.sail b/test/c/small_slice.sail
new file mode 100644
index 00000000..80878a80
--- /dev/null
+++ b/test/c/small_slice.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+function get_16((): unit) -> range(0, 16) = 16
+function get_8((): unit) -> range(0, 16) = 8
+
+function main((): unit) -> unit = {
+  let x = get_16();
+  let y = get_8();
+  let addr = 0x1234_ABCD;
+  let v1 = slice(addr, 16, x);
+  let v2 = slice(addr, 16, y);
+  print_bits("v1 = ", v1);
+  print_bits("v2 = ", v2);
+}
\ No newline at end of file
diff --git a/test/c/string_of_bits.expect b/test/c/string_of_bits.expect
new file mode 100644
index 00000000..e373cf38
--- /dev/null
+++ b/test/c/string_of_bits.expect
@@ -0,0 +1,6 @@
+HelloWorld0b11110000111 0xFF
+HelloWorld0b11110000111 0xFF
+HelloWorld0b11110000111 0xFF
+HelloWorld0b11110000111 0xFF
+HelloWorld0b11110000111 0xFF
+HelloWorld0b11110000111 0xFF
diff --git a/test/c/string_of_bits.sail b/test/c/string_of_bits.sail
new file mode 100644
index 00000000..fcaeb3e1
--- /dev/null
+++ b/test/c/string_of_bits.sail
@@ -0,0 +1,25 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "concat_str" : (string, string) -> string
+
+infixl 1 ++
+
+overload operator ++ = {concat_str}
+
+val "print_endline" : string -> unit
+
+val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
+
+val DecStr = "decimal_string_of_bits" : forall 'n. bits('n) -> string
+
+function main(() : unit) -> unit = {
+  foreach (i from 0 to 5) {
+    let x = "Hello";
+    let y = "World";
+    let z = 0b1111_0000_111;
+    let w = 0xFF;
+    print_endline(x ++ y ++ BitStr(z) ++ " " ++ BitStr(w))
+  }
+}
\ No newline at end of file
diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh
index 5a723a06..db73580f 100755
--- a/test/coq/run_tests.sh
+++ b/test/coq/run_tests.sh
@@ -56,7 +56,8 @@ function check_tests_dir {
     do
         if $SAILDIR/sail -coq -dcoq_undef_axioms -o out $TESTSDIR/$i &>/dev/null;
         then
-    	if coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out_types.v out.v &>/dev/null;
+    	if coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out_types.v &>/dev/null &&
+    	   coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out.v &>/dev/null;
     	then
     	    green "tested $i expecting pass" "pass"
     	else
diff --git a/test/lem/run_tests.sh b/test/lem/run_tests.sh
index 2cd97ab5..7660b250 100755
--- a/test/lem/run_tests.sh
+++ b/test/lem/run_tests.sh
@@ -5,9 +5,9 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 SAILDIR="$DIR/../.."
 TESTSDIR="$DIR/../typecheck/pass"
 
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
+RED='\033[0;91m'
+GREEN='\033[0;92m'
+YELLOW='\033[0;93m'
 NC='\033[0m'
 
 rm -f $DIR/tests.xml
diff --git a/test/mono/assert.sail b/test/mono/assert.sail
index ea286e93..46892956 100644
--- a/test/mono/assert.sail
+++ b/test/mono/assert.sail
@@ -24,7 +24,7 @@ function f(n,m) = {
 val f' : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}
 
 function f'(n,m) = {
-    assert(constraint(('n = 8 | 'n = 16) & 'm < 'n), "nconstraint");
+    assert(constraint(('n == 8 | 'n == 16) & 'm < 'n), "nconstraint");
     let 'p = 2 * n in
     let x : bits('p) = replicate_bits(0b0,'p) in
     ()
@@ -54,4 +54,4 @@ function run () = {
     f'(8,3);
     g(16,3);
     h(8,3);
-}
\ No newline at end of file
+}
diff --git a/test/mono/times8div8.sail b/test/mono/times8div8.sail
index 240bbfc6..31f63fda 100644
--- a/test/mono/times8div8.sail
+++ b/test/mono/times8div8.sail
@@ -35,7 +35,7 @@ function f(n) = {
     assert(constraint('n in {8,16}));
     x : bits('n) = undefined;
     let 'm : {'o, true. atom('o)} = ex_int(n / 8) in {
-        assert(constraint(8 * 'm = 'n));
+        assert(constraint(8 * 'm == 'n));
         x = replicate_bits(0b00000000,'m);
         accept(m,x);
         accept(m,replicate_bits(0b00000000,'m));
@@ -51,7 +51,7 @@ val g : forall 'm 'n. (atom('m), atom('n), bits('n)) -> unit effect {escape}
 function g(m,n,v) = {
   assert(constraint('m >= 0 & 'n >= 0));
   let 'o : {'p, true. atom('p)} = ex_int(m / n) in {
-    assert(constraint('o * 'n = 'm));
+    assert(constraint('o * 'n == 'm));
     accept2(replicate_bits(v,o))
   }
 }
diff --git a/test/ocaml/reg_ref/rr.sail b/test/ocaml/reg_ref/rr.sail
index 1e1f391c..f162d3a2 100644
--- a/test/ocaml/reg_ref/rr.sail
+++ b/test/ocaml/reg_ref/rr.sail
@@ -33,7 +33,7 @@ overload _mod_GPR = { rGPR, wGPR }
 /* Create a new type which is a pair of a bitvector and a start index
 
    slice('n, 'm) is equivalent to old-sail vector('n, 'm, dec, bit) */
-newtype slice ('n : Int) ('m : Int) = MkSlice : (atom('n), bits('m))
+newtype slice ('n : Int, 'm : Int) = MkSlice : (atom('n), bits('m))
 
 /* Extract the bitvector from a slice */
 val slice_bits : forall 'n 'm. slice('n, 'm) -> bits('m)
@@ -52,7 +52,7 @@ val slice_slice : forall 'n 'm 'o 'p, 0 <= 'p <= 'm <= 'o & 'o - 'p < 'n.
 function slice_slice (MkSlice(start, v), to, from) = MkSlice(from, v[to - start .. from - start])
 
 /* We can update a bitvector from another bitvector or a slice */
-val _set_slice : forall 'n 'm 'o, 0 <= 'm <= 'o <= 'n.
+val _set_slice : forall 'n 'm 'o, 0 <= 'm <= 'o < 'n.
   (register(bits('n)), atom('o), atom('m), bits('o - ('m - 1))) -> unit effect {wreg, rreg}
 
 function _set_slice (v, stop, start, update) = {
@@ -61,7 +61,7 @@ function _set_slice (v, stop, start, update) = {
   (*v) = v2;
 }
 
-val _set_slice2 : forall 'n 'm 'o 'p, 0 <= 'm <= 'o <= 'n.
+val _set_slice2 : forall 'n 'm 'o 'p, 0 <= 'm <= 'o < 'n.
   (register(bits('n)), atom('o), atom('m), slice('p, 'o - ('m - 1))) -> unit effect {wreg, rreg}
 
 function _set_slice2 (v, stop, start, MkSlice(_, update)) = _set_slice(v, stop, start, update)
@@ -76,7 +76,7 @@ overload _mod_slice = {_set_slice, _set_slice2, vector_slice, slice_slice}
 /* Set up a struct with an aliased LT bit in CR0, mimicing old-style syntax */
 infix 1 ...
 
-type operator ... ('n : Int) ('m : Int) = slice('m, 'n - ('m - 1))
+type operator ...('n : Int, 'm : Int) = slice('m, 'n - ('m - 1))
 
 struct cr = {
   CR0 : 7 ... 4,
diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh
index 39e34805..c160ef9f 100755
--- a/test/ocaml/run_tests.sh
+++ b/test/ocaml/run_tests.sh
@@ -5,9 +5,9 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 cd $DIR
 SAILDIR="$DIR/../.."
 
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
+RED='\033[0;91m'
+GREEN='\033[0;92m'
+YELLOW='\033[0;93m'
 NC='\033[0m'
 
 rm -f $DIR/tests.xml
diff --git a/test/ocaml/void/void.sail b/test/ocaml/void/void.sail
index 485ac019..4e8815f5 100644
--- a/test/ocaml/void/void.sail
+++ b/test/ocaml/void/void.sail
@@ -1,5 +1,5 @@
 
-val void : forall 'n, 'n = 'n + 1. atom('n) -> unit
+val void : forall 'n, 'n == 'n + 1. atom('n) -> unit
 
 function void _ = ()
 
diff --git a/test/riscv/run_tests.sh b/test/riscv/run_tests.sh
index 512feabf..c64c7dca 100755
--- a/test/riscv/run_tests.sh
+++ b/test/riscv/run_tests.sh
@@ -5,9 +5,9 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 cd $DIR
 SAILDIR="$DIR/../.."
 
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
+RED='\033[0;91m'
+GREEN='\033[0;92m'
+YELLOW='\033[0;93m'
 NC='\033[0m'
 
 rm -f $DIR/tests.xml
@@ -67,7 +67,7 @@ for test in $DIR/tests/*.elf; do
     fi
 done
 
-if make -C $SAILDIR/riscv riscv_c;
+if make -C $SAILDIR/riscv riscv_sim;
 then
     green "Building RISCV specification to C" "ok"
 else
@@ -75,8 +75,7 @@ else
 fi
 
 for test in $DIR/tests/*.elf; do
-    $SAILDIR/sail -elf $test -o ${test%.elf}.bin 2> /dev/null;
-    if timeout 5 $SAILDIR/riscv/riscv_c --binary=0x1000,reset_vec.bin --image=${test%.elf}.bin > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout
+    if timeout 5 $SAILDIR/riscv/riscv_sim $test > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout
     then
 	green "$(basename $test)" "ok"
     else
diff --git a/test/riscv/tests/.gitignore b/test/riscv/tests/.gitignore
index f47cb204..72a5e441 100644
--- a/test/riscv/tests/.gitignore
+++ b/test/riscv/tests/.gitignore
@@ -1 +1,2 @@
 *.out
+*.cout
diff --git a/test/run_tests.sh b/test/run_tests.sh
index 5e6fe691..ba0a2112 100755
--- a/test/run_tests.sh
+++ b/test/run_tests.sh
@@ -12,28 +12,28 @@ printf "==========================================\n"
 ./typecheck/run_tests.sh
 
 printf "\n==========================================\n"
-printf "Ocaml tests\n"
+printf "Lem tests\n"
 printf "==========================================\n"
 
-./ocaml/run_tests.sh
+./lem/run_tests.sh
 
 printf "\n==========================================\n"
-printf "C tests\n"
+printf "Ocaml tests\n"
 printf "==========================================\n"
 
-./c/run_tests.py
+./ocaml/run_tests.sh
 
 printf "\n==========================================\n"
-printf "Lem tests\n"
+printf "C tests\n"
 printf "==========================================\n"
 
-./lem/run_tests.sh
+TEST_PAR=8 ./c/run_tests.py
 
 printf "\n==========================================\n"
 printf "Builtins tests\n"
 printf "==========================================\n"
 
-./builtins/run_tests.py
+TEST_PAR=4 ./builtins/run_tests.py
 
 printf "\n==========================================\n"
 printf "ARM spec tests\n"
diff --git a/test/sailtest.py b/test/sailtest.py
index 612aba2b..5ee87b08 100644
--- a/test/sailtest.py
+++ b/test/sailtest.py
@@ -11,6 +11,24 @@ class color:
     FAIL = '\033[91m'
     END = '\033[0m'
 
+def parallel():
+    try:
+        return int(os.environ['TEST_PAR'])
+    except Exception, e:
+        print("Running 4 tests in parallel. Set TEST_PAR to configure")
+        return 4
+
+def chunks(filenames, cores):
+    ys = []
+    chunk = []
+    for filename in filenames:
+        if re.match('.+\.sail', filename):
+            chunk.append(filename)
+        if len(chunk) >= cores:
+            ys.append(list(chunk))
+            chunk = []
+    ys.append(list(chunk))
+    return ys
 
 def step(string):
     p = subprocess.Popen(string, shell=True, stderr=subprocess.PIPE, stdout=subprocess.PIPE)
@@ -28,24 +46,30 @@ def banner(string):
     print '-' * len(string)
     print string
     print '-' * len(string)
+    sys.stdout.flush()
+
+class Results:
+    def __init__(self, name):
+        self.passes = 0
+        self.failures = 0
+        self.xml = ""
+        self.name = name
+
+    def collect(self, tests):
+        for test in tests:
+            _, status = os.waitpid(tests[test], 0)
+            if status != 0:
+                self.failures += 1
+                self.xml += '    <testcase name="{}">\n      <error message="fail">fail</error>\n    </testcase>\n'.format(test)
+            else:
+                self.passes += 1
+                self.xml += '    <testcase name="{}"/>\n'.format(test)
+        sys.stdout.flush()
+
+    def finish(self):
+        print '{}{} passes and {} failures{}'.format(color.NOTICE, self.passes, self.failures, color.END)
 
-def collect_results(name, tests):
-    passes = 0
-    failures = 0
-    xml = ""
-
-    for test in tests:
-        _, status = os.waitpid(tests[test], 0)
-        if status != 0:
-            failures += 1
-            xml += '    <testcase name="{}">\n      <error message="fail">fail</error>\n    </testcase>\n'.format(test)
-        else:
-            passes += 1
-            xml += '    <testcase name="{}"/>\n'.format(test)
-
-    print '{}{} passes and {} failures{}'.format(color.NOTICE, passes, failures, color.END)
-
-    time = datetime.datetime.utcnow()
-    suite = '  <testsuite name="{}" tests="{}" failures="{}" timestamp="{}">\n{}  </testsuite>\n'
-    xml = suite.format(name, passes + failures, failures, time, xml)
-    return xml
+        time = datetime.datetime.utcnow()
+        suite = '  <testsuite name="{}" tests="{}" failures="{}" timestamp="{}">\n{}  </testsuite>\n'
+        self.xml = suite.format(self.name, self.passes + self.failures, self.failures, time, self.xml)
+        return self.xml
diff --git a/test/typecheck/pass/bind_typ_var.sail b/test/typecheck/pass/bind_typ_var.sail
index c442d6a8..ae340941 100644
--- a/test/typecheck/pass/bind_typ_var.sail
+++ b/test/typecheck/pass/bind_typ_var.sail
@@ -1,7 +1,7 @@
 
 val mk_vector : unit -> {'n, 'n in {32, 64}. vector('n, dec, bit)}
 
-val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}
+val mk_square : unit -> {'n 'm, 'n == 'm. vector('n, dec, vector('m, dec, bit))}
 
 val test : unit -> unit
 
@@ -10,8 +10,8 @@ function test () = {
   // could still be
   let v2 as 'len2 = mk_vector ();
   let matrix as vector('width, _, 'height) = mk_square ();
-  _prove(constraint('width = 'height));
-  _prove(constraint('len = 32 | 'len = 64));
-  _prove(constraint('len2 = 32 | 'len2 = 64));
+  _prove(constraint('width == 'height));
+  _prove(constraint('len == 32 | 'len == 64));
+  _prove(constraint('len2 == 32 | 'len2 == 64));
   ()
 }
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint.sail b/test/typecheck/pass/bool_constraint.sail
new file mode 100644
index 00000000..de6bf4b7
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    _not_prove(constraint('n <= 14));
+    _prove(constraint('n <= 15))
+  };
+
+  if my_not(cond) then {
+    _not_prove(constraint('n <= 14));
+    _prove(constraint('n <= 15))
+  } else {
+    _prove(constraint('n <= 14))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect
new file mode 100644
index 00000000..3e2c7bde
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v1.expect
@@ -0,0 +1,27 @@
+Type error at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20
+
+  if b then n else 4
+
+Tried performing type coercion from int(4) to {'m, ('b & 'm == 'n | not('b) & 'm == 3). int('m)} on 4
+Coercion failed because:
+  int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)}
+  in context
+  * 4 == 'ex41#m
+  * not('b)
+  where
+  * 'b bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1
+
+function foo(b, n) = {
+  if b then n else 4
+}
+
+  * 'ex41#m bound at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20
+
+  if b then n else 4
+
+  * 'n bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1
+
+function foo(b, n) = {
+  if b then n else 4
+}
+
diff --git a/test/typecheck/pass/bool_constraint/v1.sail b/test/typecheck/pass/bool_constraint/v1.sail
new file mode 100644
index 00000000..46badd52
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v1.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 4
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    ()
+  };
+
+  if my_not(cond) then {
+    ()
+  } else {
+    _prove(constraint('n <= 14))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint/v2.expect b/test/typecheck/pass/bool_constraint/v2.expect
new file mode 100644
index 00000000..847ef329
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v2.expect
@@ -0,0 +1,5 @@
+Type error at file "bool_constraint/v2.sail", line 38, character 5 to line 38, character 32
+
+    _prove(constraint('n <= 14))
+
+Cannot prove 'n <= 14
diff --git a/test/typecheck/pass/bool_constraint/v2.sail b/test/typecheck/pass/bool_constraint/v2.sail
new file mode 100644
index 00000000..1506bbbd
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v2.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 16 & implies('b, 'n <= 15).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    ()
+  };
+
+  if my_not(cond) then {
+    ()
+  } else {
+    _prove(constraint('n <= 14))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint/v3.expect b/test/typecheck/pass/bool_constraint/v3.expect
new file mode 100644
index 00000000..ca87fac1
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v3.expect
@@ -0,0 +1,5 @@
+Type error at file "bool_constraint/v3.sail", line 46, character 5 to line 46, character 32
+
+    _prove(constraint('n <= 14))
+
+Cannot prove 'n <= 14
diff --git a/test/typecheck/pass/bool_constraint/v3.sail b/test/typecheck/pass/bool_constraint/v3.sail
new file mode 100644
index 00000000..966ad2d5
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v3.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> 'q. bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    ()
+  };
+
+  if my_not(cond) then {
+    ()
+  } else {
+    _prove(constraint('n <= 14))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint/v4.expect b/test/typecheck/pass/bool_constraint/v4.expect
new file mode 100644
index 00000000..07363175
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v4.expect
@@ -0,0 +1,5 @@
+Type error at file "bool_constraint/v4.sail", line 46, character 5 to line 46, character 32
+
+    _prove(constraint('n <= 13))
+
+Cannot prove 'n <= 13
diff --git a/test/typecheck/pass/bool_constraint/v4.sail b/test/typecheck/pass/bool_constraint/v4.sail
new file mode 100644
index 00000000..9f68bf91
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v4.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    ()
+  };
+
+  if my_not(cond) then {
+    ()
+  } else {
+    _prove(constraint('n <= 13))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/commentfix.sail b/test/typecheck/pass/commentfix.sail
new file mode 100644
index 00000000..fd2cf0b2
--- /dev/null
+++ b/test/typecheck/pass/commentfix.sail
@@ -0,0 +1,7 @@
+/********/
+
+/*=====*/
+
+//////
+
+default Order inc
diff --git a/test/typecheck/pass/constrained_struct.sail b/test/typecheck/pass/constrained_struct.sail
new file mode 100644
index 00000000..87d55b65
--- /dev/null
+++ b/test/typecheck/pass/constrained_struct.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+struct MyStruct('n), 'n in {32, 64} = {
+  field: bits('n)
+}
+
+type MyStruct32 = MyStruct(32)
+type MyStruct64 = MyStruct(64)
+
+let x : MyStruct64 = struct { field = 0xFFFF_FFFF_FFFF_FFFF }
diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect
new file mode 100644
index 00000000..ab25cbc4
--- /dev/null
+++ b/test/typecheck/pass/constrained_struct/v1.expect
@@ -0,0 +1,5 @@
+Type error at file "constrained_struct/v1.sail", line 10, character 19 to line 10, character 26
+
+type MyStruct64 = MyStruct(65)
+
+Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct
diff --git a/test/typecheck/pass/constrained_struct/v1.sail b/test/typecheck/pass/constrained_struct/v1.sail
new file mode 100644
index 00000000..98daf59e
--- /dev/null
+++ b/test/typecheck/pass/constrained_struct/v1.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+struct MyStruct('n), 'n in {32, 64} = {
+  field: bits('n)
+}
+
+type MyStruct32 = MyStruct(32)
+type MyStruct64 = MyStruct(65)
+
+let x : MyStruct64 = struct { field = 0b1 @ 0xFFFF_FFFF_FFFF_FFFF }
diff --git a/test/typecheck/pass/constraint_ctor.sail b/test/typecheck/pass/constraint_ctor.sail
new file mode 100644
index 00000000..17ec74ce
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor.sail
@@ -0,0 +1,29 @@
+default Order dec
+
+$include <flow.sail>
+
+union Foo = {
+  Foo : {'n, 'n >= 3. int('n)}
+}
+
+function foo(Foo(x as int('x)): Foo) -> unit = {
+  _prove(constraint('x >= 3));
+}
+
+union Bar('m), 'm <= 100 = {
+  Bar : {'n, 'n >= 'm. int('n)}
+}
+
+function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+  _prove(constraint('x >= 23));
+  ()
+}
+
+union Quux('a : Type) = {
+  Quux : 'a
+}
+
+function quux(Quux(x as int('x)) : Quux({'n, 'n >= 3. int('n)})) -> unit = {
+  _prove(constraint('x >= 3));
+  ()
+}
diff --git a/test/typecheck/pass/constraint_ctor/v1.expect b/test/typecheck/pass/constraint_ctor/v1.expect
new file mode 100644
index 00000000..c3886af8
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v1.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_ctor/v1.sail", line 10, character 3 to line 10, character 29
+
+  _prove(constraint('x >= 4));
+
+Cannot prove 'x >= 4
diff --git a/test/typecheck/pass/constraint_ctor/v1.sail b/test/typecheck/pass/constraint_ctor/v1.sail
new file mode 100644
index 00000000..20df5480
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v1.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <flow.sail>
+
+union Foo = {
+  Foo : {'n, 'n >= 3. int('n)}
+}
+
+function foo(Foo(x as int('x)): Foo) -> unit = {
+  _prove(constraint('x >= 4));
+}
+
+union Bar('m), 'm <= 100 = {
+  Bar : {'n, 'n >= 'm. int('n)}
+}
+
+function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+  _prove(constraint('x >= 23));
+  ()
+}
diff --git a/test/typecheck/pass/constraint_ctor/v2.expect b/test/typecheck/pass/constraint_ctor/v2.expect
new file mode 100644
index 00000000..a315b3b7
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v2.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_ctor/v2.sail", line 18, character 3 to line 18, character 30
+
+  _prove(constraint('x >= 24));
+
+Cannot prove 'x >= 24
diff --git a/test/typecheck/pass/constraint_ctor/v2.sail b/test/typecheck/pass/constraint_ctor/v2.sail
new file mode 100644
index 00000000..76d9793d
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v2.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <flow.sail>
+
+union Foo = {
+  Foo : {'n, 'n >= 3. int('n)}
+}
+
+function foo(Foo(x as int('x)): Foo) -> unit = {
+  _prove(constraint('x >= 3));
+}
+
+union Bar('m), 'm <= 100 = {
+  Bar : {'n, 'n >= 'm. int('n)}
+}
+
+function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+  _prove(constraint('x >= 24));
+  ()
+}
diff --git a/test/typecheck/pass/constraint_ctor/v3.expect b/test/typecheck/pass/constraint_ctor/v3.expect
new file mode 100644
index 00000000..e0edd01a
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v3.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_ctor/v3.sail", line 18, character 3 to line 18, character 30
+
+  _prove(constraint('x >= 23));
+
+Cannot prove 'x >= 23
diff --git a/test/typecheck/pass/constraint_ctor/v3.sail b/test/typecheck/pass/constraint_ctor/v3.sail
new file mode 100644
index 00000000..a8f5bd13
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v3.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <flow.sail>
+
+union Foo = {
+  Foo : {'n, 'n >= 3. int('n)}
+}
+
+function foo(Foo(x as int('x)): Foo) -> unit = {
+  _prove(constraint('x >= 3));
+}
+
+union Bar('m), 'm <= 100 = {
+  Bar : {'n, 'n >= 'm. int('n)}
+}
+
+function bar(Bar(x as int('x)) : Bar(22)) -> unit = {
+  _prove(constraint('x >= 23));
+  ()
+}
diff --git a/test/typecheck/pass/constraint_ctor/v4.expect b/test/typecheck/pass/constraint_ctor/v4.expect
new file mode 100644
index 00000000..06eb9d22
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v4.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_ctor/v4.sail", line 17, character 34 to line 17, character 36
+
+function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+
+Could not prove 23 <= 22 for type constructor Bar
diff --git a/test/typecheck/pass/constraint_ctor/v4.sail b/test/typecheck/pass/constraint_ctor/v4.sail
new file mode 100644
index 00000000..d8dab178
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v4.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <flow.sail>
+
+union Foo = {
+  Foo : {'n, 'n >= 3. int('n)}
+}
+
+function foo(Foo(x as int('x)): Foo) -> unit = {
+  _prove(constraint('x >= 3));
+}
+
+union Bar('m), 'm <= 22 = {
+  Bar : {'n, 'n >= 'm. int('n)}
+}
+
+function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+  _prove(constraint('x >= 23));
+  ()
+}
diff --git a/test/typecheck/pass/constraint_ctor/v5.expect b/test/typecheck/pass/constraint_ctor/v5.expect
new file mode 100644
index 00000000..b6df0222
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v5.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_ctor/v5.sail", line 27, character 3 to line 27, character 29
+
+  _prove(constraint('x >= 4));
+
+Cannot prove 'x >= 4
diff --git a/test/typecheck/pass/constraint_ctor/v5.sail b/test/typecheck/pass/constraint_ctor/v5.sail
new file mode 100644
index 00000000..855044a5
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v5.sail
@@ -0,0 +1,29 @@
+default Order dec
+
+$include <flow.sail>
+
+union Foo = {
+  Foo : {'n, 'n >= 3. int('n)}
+}
+
+function foo(Foo(x as int('x)): Foo) -> unit = {
+  _prove(constraint('x >= 3));
+}
+
+union Bar('m), 'm <= 100 = {
+  Bar : {'n, 'n >= 'm. int('n)}
+}
+
+function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+  _prove(constraint('x >= 23));
+  ()
+}
+
+union Quux('a : Type) = {
+  Quux : 'a
+}
+
+function quux(Quux(x as int('x)) : Quux({'n, 'n >= 3. int('n)})) -> unit = {
+  _prove(constraint('x >= 4));
+  ()
+}
diff --git a/test/typecheck/pass/custom_flow.sail b/test/typecheck/pass/custom_flow.sail
new file mode 100644
index 00000000..43c980d6
--- /dev/null
+++ b/test/typecheck/pass/custom_flow.sail
@@ -0,0 +1,43 @@
+val "print_endline" : string -> unit
+
+val operator <= = {
+  coq: "Z.leb",
+  _: "lteq"
+} : forall 'n 'm. (int('n), int('m)) -> bool('n <= 'm)
+
+function test1 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  if n <= m then {
+    _prove(constraint('n <= 'm));
+    print_endline("1");
+  } else {
+    print_endline("2");
+    _prove(constraint('n > 'm));
+  }
+}
+
+val and_bool = {
+  coq: "andb",
+  _: "and_bool"
+} : forall ('p: Bool) ('q: Bool). (bool('p), bool('q)) -> bool('p & 'q)
+
+overload operator & = {and_bool}
+
+function test2 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  let x = n <= m & n <= 20;
+  if x then {
+    _prove(constraint('n <= 20));
+    _prove(constraint('n <= 'm));
+    print_endline("3")
+  } else {
+    _prove(constraint('n > 'm | 'n > 20));
+    print_endline("4")
+  }
+}
+
+function main((): unit) -> unit = {
+  test1(1, 2);
+  test1(2, 1);
+  test2(1, 2);
+  test2(2, 1);
+  test2(21, 0)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/exint.sail b/test/typecheck/pass/exint.sail
index ffa6d033..3e2acf28 100644
--- a/test/typecheck/pass/exint.sail
+++ b/test/typecheck/pass/exint.sail
@@ -1,8 +1,8 @@
 type MyInt = {'n, true. atom('n)}
 
-val add : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = 'n + 'm. atom('o)}
+val add : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == 'n + 'm. atom('o)}
 
-val mult : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = 'n * 'm. atom('o)}
+val mult : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == 'n * 'm. atom('o)}
 
 overload operator + = {add}
 
@@ -14,7 +14,7 @@ let y = x + x * x
 
 let z : atom(7 * 8) = y
 
-type Range ('n : Int) ('m : Int), 'n <= 'm = {'o, 'n <= 'o & 'o <= 'm. atom('o)}
+type Range('n: Int, 'm: Int), 'n <= 'm = {'o, 'n <= 'o & 'o <= 'm. atom('o)}
 
 let a : Range(3, 4) = 3
 
diff --git a/test/typecheck/pass/exist1.sail b/test/typecheck/pass/exist1.sail
index f6c0c073..6db518e8 100644
--- a/test/typecheck/pass/exist1.sail
+++ b/test/typecheck/pass/exist1.sail
@@ -22,6 +22,6 @@ function unit_fn x : atom(4) = ()
 
 val s_add : forall 'a. (atom('a), atom('a)) -> atom('a + 'a)
 
-let v7 : {'k, 'k = 4. atom('k)} = 4
+let v7 : {'k, 'k == 4. atom('k)} = 4
 
 let v8 = s_add(v7, 4)
diff --git a/test/typecheck/pass/exist2.sail b/test/typecheck/pass/exist2.sail
index 42ec8cb1..e518609d 100644
--- a/test/typecheck/pass/exist2.sail
+++ b/test/typecheck/pass/exist2.sail
@@ -22,13 +22,13 @@ function unit_fn x : atom(4) = ()
 
 val s_add : forall 'a. (atom('a), atom('a)) -> atom('a + 'a)
 
-let v7 : {'k, 'k = 4. atom('k)} = 4
+let v7 : {'k, 'k == 4. atom('k)} = 4
 
-let v9 : {'n, 0 = 0. atom('n)} = 100
+let v9 : {'n, 0 == 0. atom('n)} = 100
 
 let v10 : int = v9
 
-type MyInt = {'n, 0 = 0. atom('n)}
+type MyInt = {'n, 0 == 0. atom('n)}
 
 val existential_int : int -> MyInt
 
@@ -37,8 +37,8 @@ val existential_range : forall 'n 'm.
 
 overload existential = {existential_int, existential_range}
 
-let v11 : {'n, 0 = 0. atom('n)} = existential(v10)
+let v11 : {'n, 0 == 0. atom('n)} = existential(v10)
 
-let v12 : {'e, 0 <= 'e & 'e <= 3. atom('e)} = existential(2 : range(0, 3))
+let v12 : {'e, 0 <= 'e & 'e <= 3. atom('e)} = 2
 
 let v13 : MyInt = existential(v10)
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail
deleted file mode 100644
index ac41114f..00000000
--- a/test/typecheck/pass/exist_pattern.sail
+++ /dev/null
@@ -1,48 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-register n : nat
-
-register x : nat
-
-register y : nat
-
-type wordsize = {'n, 'n in {8, 16, 32}. range(0, 'n)}
-
-let word : wordsize = 8 : range(0, 8)
-
-val main : unit -> int effect {wreg, rreg}
-
-function main () = {
-  n = 1;
-  y = match n {
-    0 => {
-      x = 21;
-      x
-    },
-    1 => {
-      x = 42;
-      x
-    },
-    z => {
-      x = 99;
-      x
-    }
-  };
-  match word {
-    8  => x = 32,
-    16 => x = 64,
-    32 => x = 128
-  };
-  match 0b010101 {
-    0b01 @ _ : vector(1, dec, bit) @ 0b101 => n = 42,
-    _ => n = 0
-  };
-  n = 3;
-  match n {
-    0 => 21,
-    1 => 42,
-    u => 99
-  }
-}
diff --git a/test/typecheck/pass/exist_synonym.sail b/test/typecheck/pass/exist_synonym.sail
index 44382213..b251cbf8 100644
--- a/test/typecheck/pass/exist_synonym.sail
+++ b/test/typecheck/pass/exist_synonym.sail
@@ -1,6 +1,6 @@
 
 // Type synonym with a constraint.
-type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+type regno('n: Int), 0 <= 'n < 32 = atom('n)
 
 // Existential with constrained type synonym.
 let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect
index 9ee4b202..fb1b2619 100644
--- a/test/typecheck/pass/exist_synonym/v1.expect
+++ b/test/typecheck/pass/exist_synonym/v1.expect
@@ -2,6 +2,5 @@ Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, char
 
 let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
 
-Tried performing type coercion from atom(4) to {'n, 0 <= 'n & 'n <= 33. regno('n)} on 4
-Failed because
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 'n & 'n <= 33)
+Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 33). regno('n)} on 4
+Coercion failed because: Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33)
diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect
index e3414034..5bde04ba 100644
--- a/test/typecheck/pass/exist_synonym/v2.expect
+++ b/test/typecheck/pass/exist_synonym/v2.expect
@@ -2,6 +2,5 @@ Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, char
 
 let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
 
-Tried performing type coercion from atom(4) to {'n, 0 <= 'n & 'n <= 8. regno('n)} on 4
-Failed because
-Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym atom('n) with (0 <= 'n & 'n <= 8)
+Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 8). regno('n)} on 4
+Coercion failed because: Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8)
diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect
index c41f2c4b..a647ef00 100644
--- a/test/typecheck/pass/exist_synonym/v3.expect
+++ b/test/typecheck/pass/exist_synonym/v3.expect
@@ -1,3 +1,3 @@
 Type error at no location information available
 
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 'n & 'n <= 100), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 8)
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8)
diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect
index a17ed112..d8bad777 100644
--- a/test/typecheck/pass/exist_synonym/v4.expect
+++ b/test/typecheck/pass/exist_synonym/v4.expect
@@ -1,3 +1,3 @@
 Type error at no location information available
 
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 2 & 2 <= 4), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 8)
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 2 & 2 <= 4), (0 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8)
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index 33d6cbcd..e81c467e 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -2,23 +2,23 @@ Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23,
 
 let _ = test(32)
 
-Tried performing type coercion from atom(32) to atom('size) on 32
-Failed because
-atom(32) is not a subtype of atom('size)
-in context
-* 'size = 'ex8#
-* ('ex8# = 32 | 'ex8# = 64)
-* ('ex7# = 32 | 'ex7# = 64)
-where
-* 'ex7# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32
+Tried performing type coercion from int(32) to int('size) on 32
+Coercion failed because:
+  int(32) is not a subtype of int('size)
+  in context
+  * 'size == 'ex14#
+  * ('ex14# == 32 | 'ex14# == 64)
+  * ('ex13# == 32 | 'ex13# == 64)
+  where
+  * 'ex13# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32
 
 let (size as 'size) : {|32, 64|} = 32
 
-* 'ex8# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18
+  * 'ex14# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18
 
 let (size as 'size) : {|32, 64|} = 32
 
-* 'size bound at file "global_type_var/v1.sail", line 5, character 14 to line 5, character 18
+  * 'size bound at file "global_type_var/v1.sail", line 5, character 14 to line 5, character 18
 
 let (size as 'size) : {|32, 64|} = 32
 
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index 25304155..21c4b348 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -2,23 +2,23 @@ Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23,
 
 let _ = test(64)
 
-Tried performing type coercion from atom(64) to atom('size) on 64
-Failed because
-atom(64) is not a subtype of atom('size)
-in context
-* 'size = 'ex8#
-* ('ex8# = 32 | 'ex8# = 64)
-* ('ex7# = 32 | 'ex7# = 64)
-where
-* 'ex7# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32
+Tried performing type coercion from int(64) to int('size) on 64
+Coercion failed because:
+  int(64) is not a subtype of int('size)
+  in context
+  * 'size == 'ex14#
+  * ('ex14# == 32 | 'ex14# == 64)
+  * ('ex13# == 32 | 'ex13# == 64)
+  where
+  * 'ex13# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32
 
 let (size as 'size) : {|32, 64|} = 32
 
-* 'ex8# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18
+  * 'ex14# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18
 
 let (size as 'size) : {|32, 64|} = 32
 
-* 'size bound at file "global_type_var/v2.sail", line 5, character 14 to line 5, character 18
+  * 'size bound at file "global_type_var/v2.sail", line 5, character 14 to line 5, character 18
 
 let (size as 'size) : {|32, 64|} = 32
 
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
index 8014f88a..43096686 100644
--- a/test/typecheck/pass/global_type_var/v3.expect
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -2,4 +2,4 @@ Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, ch
 
 val test : forall 'size. atom('size) -> unit
 
-Kind identifier 'size is already bound
+type variable ('size : Int) is already bound
diff --git a/test/typecheck/pass/if_infer.sail b/test/typecheck/pass/if_infer.sail
new file mode 100644
index 00000000..f3fec1c4
--- /dev/null
+++ b/test/typecheck/pass/if_infer.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : bool
+
+val f : unit -> {'n, 1 <= 'n <= 3. int('n)}
+
+function main((): unit) -> unit = {
+  let _ = 0b1001[if R then 0 else f()];
+  ()
+}
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
new file mode 100644
index 00000000..95073799
--- /dev/null
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -0,0 +1,17 @@
+Type error at file "if_infer/v1.sail", line 10, character 11 to line 10, character 37
+
+  let _ = 0b100[if R then 0 else f()];
+
+No overloadings for vector_access, tried:
+  bitvector_access:
+    Could not resolve quantifiers for bitvector_access (0 <= 'ex42#ex41# & ('ex42#ex41# + 1) <= 3)
+    
+    Try adding named type variables for 
+    
+    
+  plain_vector_access:
+    Could not resolve quantifiers for plain_vector_access (0 <= 'ex45#ex44# & ('ex45#ex44# + 1) <= 3)
+    
+    Try adding named type variables for 
+    
+    
diff --git a/test/typecheck/pass/if_infer/v1.sail b/test/typecheck/pass/if_infer/v1.sail
new file mode 100644
index 00000000..0938aaed
--- /dev/null
+++ b/test/typecheck/pass/if_infer/v1.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : bool
+
+val f : unit -> {'n, 1 <= 'n <= 3. int('n)}
+
+function main((): unit) -> unit = {
+  let _ = 0b100[if R then 0 else f()];
+  ()
+}
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
new file mode 100644
index 00000000..afa04343
--- /dev/null
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -0,0 +1,17 @@
+Type error at file "if_infer/v2.sail", line 10, character 11 to line 10, character 38
+
+  let _ = 0b1001[if R then 0 else f()];
+
+No overloadings for vector_access, tried:
+  bitvector_access:
+    Could not resolve quantifiers for bitvector_access (0 <= 'ex42#ex41# & ('ex42#ex41# + 1) <= 4)
+    
+    Try adding named type variables for 
+    
+    
+  plain_vector_access:
+    Could not resolve quantifiers for plain_vector_access (0 <= 'ex45#ex44# & ('ex45#ex44# + 1) <= 4)
+    
+    Try adding named type variables for 
+    
+    
diff --git a/test/typecheck/pass/if_infer/v2.sail b/test/typecheck/pass/if_infer/v2.sail
new file mode 100644
index 00000000..a49e1ed7
--- /dev/null
+++ b/test/typecheck/pass/if_infer/v2.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : bool
+
+val f : unit -> {'n, 1 <= 'n <= 4. int('n)}
+
+function main((): unit) -> unit = {
+  let _ = 0b1001[if R then 0 else f()];
+  ()
+}
diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect
new file mode 100644
index 00000000..8b149bc8
--- /dev/null
+++ b/test/typecheck/pass/if_infer/v3.expect
@@ -0,0 +1,7 @@
+Type error at file "if_infer/v3.sail", line 10, character 11 to line 10, character 38
+
+  let _ = 0b1001[if R then 0 else f()];
+
+No overloadings for vector_access, tried:
+  bitvector_access: Numeric type is non-simple
+  plain_vector_access: Numeric type is non-simple
diff --git a/test/typecheck/pass/if_infer/v3.sail b/test/typecheck/pass/if_infer/v3.sail
new file mode 100644
index 00000000..0c3dec21
--- /dev/null
+++ b/test/typecheck/pass/if_infer/v3.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : bool
+
+val f : unit -> {'n 'm, 'm == 3 & 1 <= 'n <= 'm. int('n)}
+
+function main((): unit) -> unit = {
+  let _ = 0b1001[if R then 0 else f()];
+  ()
+}
diff --git a/test/typecheck/pass/inline_typ.sail b/test/typecheck/pass/inline_typ.sail
index dd761b83..95be790c 100644
--- a/test/typecheck/pass/inline_typ.sail
+++ b/test/typecheck/pass/inline_typ.sail
@@ -1,2 +1,2 @@
 
-function test (x : atom('n), y : atom('m)) -> forall 'n 'm. atom('m + 'n) = undefined
\ No newline at end of file
+function test forall 'n 'm. (x : int('n), y : int('m)) -> int('m + 'n) = undefined
\ No newline at end of file
diff --git a/test/typecheck/pass/lexp_vec.sail b/test/typecheck/pass/lexp_vec.sail
new file mode 100644
index 00000000..605c3855
--- /dev/null
+++ b/test/typecheck/pass/lexp_vec.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+register V : vector(1, dec, vector(32, dec, bit))
+
+val zeros : forall 'n, 'n >= 0. unit -> vector('n, dec, bit)
+
+function main() : unit -> unit = {
+  V[0] = zeros()
+}
diff --git a/test/typecheck/pass/nat_set.sail b/test/typecheck/pass/nat_set.sail
index a12e81da..f171eb9b 100644
--- a/test/typecheck/pass/nat_set.sail
+++ b/test/typecheck/pass/nat_set.sail
@@ -1,4 +1,4 @@
-function test x : atom('n) -> forall 'n. bool = true
+function test forall 'n, 'n in {1, 3}. x : atom('n) -> bool = true
 
 let x = test(1)
 
diff --git a/test/typecheck/pass/nlflow.sail b/test/typecheck/pass/nlflow.sail
new file mode 100644
index 00000000..95d2d280
--- /dev/null
+++ b/test/typecheck/pass/nlflow.sail
@@ -0,0 +1,16 @@
+$option -non_lexical_flow
+
+default Order dec
+
+$include <prelude.sail>
+$include <exception_basic.sail>
+
+val foo : forall 'n, 'n != 8. int('n) -> unit
+
+function test(xs: vector(4, dec, bit)) -> unit = {
+  if xs == 0b1000 then {
+    throw(Exception())
+  };
+  let y = unsigned(xs);
+  foo(y)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/option_either.sail b/test/typecheck/pass/option_either.sail
index de4458ed..ec4e72db 100644
--- a/test/typecheck/pass/option_either.sail
+++ b/test/typecheck/pass/option_either.sail
@@ -1,17 +1,17 @@
 default Order inc
 
-union option ('a : Type) = {None : unit, Some : 'a}
+union option('a: Type) = {None : unit, Some : 'a}
 
-function none () -> forall ('a : Type). option('a) = None()
+function none forall ('a : Type). () -> option('a) = None()
 
-function some x : 'a -> forall ('a : Type). option('a) = Some(x)
+function some forall ('a : Type). x : 'a -> option('a) = Some(x)
 
-function test x : option('a) -> forall ('a : Type). range(0, 1) = match x {
+function test forall ('a : Type). x : option('a) -> range(0, 1) = match x {
   None() => 0,
   Some(y) => 1
 }
 
-union either ('a : Type) ('b : Type) = {Left : 'a, Right : 'b}
+union either('a: Type, 'b: Type) = {Left : 'a, Right : 'b}
 
 val signed : forall ('n : Int), 'n >= 0. vector('n, inc, bit) -> int
 
diff --git a/test/typecheck/pass/or_pattern.sail b/test/typecheck/pass/or_pattern.sail
deleted file mode 100644
index a6e11ecd..00000000
--- a/test/typecheck/pass/or_pattern.sail
+++ /dev/null
@@ -1,16 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-let x : int = 5
-
-val main : unit -> unit
-
-function main() = {
-  match x {
-    3 | 4       => (),
-    (1 | 2) | 3 => (),
-    1 | (2 | 3) => (),
-    _           => ()
-  }
-}
\ No newline at end of file
diff --git a/test/typecheck/pass/or_pattern/v1.expect b/test/typecheck/pass/or_pattern/v1.expect
deleted file mode 100644
index edf07f03..00000000
--- a/test/typecheck/pass/or_pattern/v1.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-Type error at file "or_pattern/v1.sail", line 11, character 5 to line 11, character 5
-
-    y | z       => (),
-
-Bindings are not allowed in this context
diff --git a/test/typecheck/pass/or_pattern/v1.sail b/test/typecheck/pass/or_pattern/v1.sail
deleted file mode 100644
index 21bc87e8..00000000
--- a/test/typecheck/pass/or_pattern/v1.sail
+++ /dev/null
@@ -1,14 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-let x : int = 5
-
-val main : unit -> unit
-
-function main() = {
-  match x {
-    y | z       => (),
-    _           => ()
-  }
-}
\ No newline at end of file
diff --git a/test/typecheck/pass/patternrefinement.sail b/test/typecheck/pass/patternrefinement.sail
index 94b40885..86294543 100644
--- a/test/typecheck/pass/patternrefinement.sail
+++ b/test/typecheck/pass/patternrefinement.sail
@@ -3,20 +3,20 @@ default Order dec
 infix 4 ==
 
 val extz = {ocaml: "extz", lem: "extz_vec"}: forall ('n : Int) ('m : Int) ('ord : Order).
-  (atom('m), vector('n, 'ord, bit)) -> vector('m, 'ord, bit)
+  (int('m), vector('n, 'ord, bit)) -> vector('m, 'ord, bit)
 
 val length = {ocaml: "length", lem: "length"}: forall ('m : Int) ('ord : Order) ('a : Type).
-  vector('m, 'ord, 'a) -> atom('m)
+  vector('m, 'ord, 'a) -> int('m)
 
 val eq_vec = {ocaml: "eq_vec", lem: "eq_vec"}: forall ('m : Int) ('ord : Order).
   (vector('m, 'ord, bit), vector('m, 'ord, bit)) -> bool
 
-val eq_atom = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
-  (atom('n), atom('m)) -> bool
+val eq_int = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
+  (int('n), int('m)) -> bool
 
 val eq = {ocaml: "eq", lem: "eq"}: forall ('a : Type). ('a, 'a) -> bool
 
-overload operator == = {eq_vec, eq_atom, eq}
+overload operator == = {eq_vec, eq_int, eq}
 
 val test : forall 'n, 'n in {32, 64}.
   vector('n, dec, bit) -> vector(64, dec, bit)
diff --git a/test/typecheck/pass/poly_list.sail b/test/typecheck/pass/poly_list.sail
new file mode 100644
index 00000000..cb8e9b49
--- /dev/null
+++ b/test/typecheck/pass/poly_list.sail
@@ -0,0 +1,19 @@
+default Order dec
+
+$include <prelude.sail>
+
+function cons(x: int, xs: list(int)) -> list(int) = {
+  x :: xs
+}
+
+function poly_cons forall ('a : Type). (x: 'a, xs: list('a)) -> list('a) = {
+  x :: xs
+}
+
+function main((): unit) -> unit = {
+  let _ = cons(1, [|2, 3, 4|]);
+  let _ : list(int) = poly_cons(1, [|2, 3, 4|]);
+  // TODO: This fails due to different order of instantiation
+  // let _ = poly_cons(1 : int, [|2, 3, 4|]);
+  ()
+}
diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail
index cbdb2c9d..588fd324 100644
--- a/test/typecheck/pass/pure_record2.sail
+++ b/test/typecheck/pass/pure_record2.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-struct State ('a : Type) ('n : Int) = {
+struct State('a: Type, 'n: Int) = {
   N : vector('n, dec, 'a),
   Z : vector(1, dec, bit)
 }
diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail
index cd3e849a..de388c3e 100644
--- a/test/typecheck/pass/pure_record3.sail
+++ b/test/typecheck/pass/pure_record3.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-struct State ('a : Type) ('n : Int) = {
+struct State('a: Type, 'n: Int) = {
   N : vector('n, dec, 'a),
   Z : vector(1, dec, bit)
 }
diff --git a/test/typecheck/pass/reg_ref.sail b/test/typecheck/pass/reg_ref.sail
new file mode 100644
index 00000000..a81f6abf
--- /dev/null
+++ b/test/typecheck/pass/reg_ref.sail
@@ -0,0 +1,13 @@
+register reg : range(0, 10)
+
+val modify : register(range(0,10)) -> unit effect {wreg}
+
+function modify (r) = {
+  (*r) = 9;
+  (*r) = 10;
+  (*r) = 8
+}
+
+val test : unit -> unit effect {wreg}
+
+function test () = modify(ref reg)
diff --git a/test/typecheck/pass/simple_scattered.sail b/test/typecheck/pass/simple_scattered.sail
index bb4a1a14..01bf7ad8 100644
--- a/test/typecheck/pass/simple_scattered.sail
+++ b/test/typecheck/pass/simple_scattered.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-scattered union ast ('datasize : Int) ('destsize : Int) ('regsize : Int)
+scattered union ast('datasize : Int, 'destsize : Int, 'regsize : Int)
 
 val execute : forall ('datasize : Int) ('destsize : Int) ('regsize : Int).
   ast('datasize, 'destsize, 'regsize) -> unit
diff --git a/test/typecheck/pass/tautology.sail b/test/typecheck/pass/tautology.sail
new file mode 100644
index 00000000..f1c8bade
--- /dev/null
+++ b/test/typecheck/pass/tautology.sail
@@ -0,0 +1,65 @@
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val tautologies :  forall ('p : Bool) ('q : Bool) ('r : Bool). (bool('p), bool('q), bool('r)) -> unit effect {escape}
+
+function tautologies(p, q, r) = {
+  _not_prove(constraint('p));
+  _not_prove(constraint('q));
+  _not_prove(constraint('r));
+
+  // implication definition
+  _prove(constraint(not('p) | 'q --> ('p --> 'q)));
+  _prove(constraint(('p --> 'q) --> not('p) | 'q));
+  _prove(constraint(('p --> 'q) <--> not('p) | 'q));
+
+  // implication properties
+  _prove(constraint('p --> 'p));
+  _prove(constraint(('p --> 'q) & ('q --> 'r) --> ('p --> 'r)));
+  _prove(constraint(('p --> 'q) & 'p --> 'q));
+
+  _prove(constraint('p & 'q <--> 'q & 'p));
+  _prove(constraint('p | 'q <--> 'q | 'p));
+  _prove(constraint(('p <--> 'q) <--> ('q <--> 'p)));
+
+  // excluded middle
+  _prove(constraint('p | not('p)));
+
+  // de Morgan
+  _prove(constraint(not('p | 'q) <--> not('p) & not('q)));
+  _prove(constraint(not('p & 'q) <--> not('p) | not('q)));
+
+  // contradiction
+  _prove(constraint('p & not('p) --> false));
+  {
+    assert(constraint('p & not('p)));
+    _prove(constraint(false))
+  };
+  _not_prove(constraint(false));
+
+  _prove(constraint(('p <--> 'q) & ('p | 'q) --> ('p & 'q)));
+  _prove(constraint(('p & 'q --> 'r) <--> ('p --> 'q --> 'r)));
+
+  {
+    assert(constraint('p));
+    _prove(constraint('p))
+  };
+  _not_prove(constraint('p));
+
+  {
+    assert(constraint('p));
+    assert(constraint('p --> 'q));
+    _prove(constraint('q));
+    assert(constraint('q --> 'r));
+    _prove(constraint('r))
+  };
+  _not_prove(constraint('q));
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vec_length.sail b/test/typecheck/pass/vec_length.sail
new file mode 100644
index 00000000..21911b15
--- /dev/null
+++ b/test/typecheck/pass/vec_length.sail
@@ -0,0 +1,9 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 5 = y];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect
new file mode 100644
index 00000000..68a4ca70
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1.expect
@@ -0,0 +1,13 @@
+Type error at file "vec_length/v1.sail", line 6, character 11 to line 6, character 15
+
+  let y = x[10];
+
+No overloadings for vector_access, tried:
+  bitvector_access:
+    Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+  plain_vector_access:
+    Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
diff --git a/test/typecheck/pass/vec_length/v1.sail b/test/typecheck/pass/vec_length/v1.sail
new file mode 100644
index 00000000..735da89c
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1.sail
@@ -0,0 +1,8 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[10];
+  ()
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect
new file mode 100644
index 00000000..7ce8fd99
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1_inc.expect
@@ -0,0 +1,13 @@
+Type error at file "vec_length/v1_inc.sail", line 6, character 11 to line 6, character 15
+
+  let y = x[10];
+
+No overloadings for vector_access, tried:
+  bitvector_access:
+    Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+  plain_vector_access:
+    Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
diff --git a/test/typecheck/pass/vec_length/v1_inc.sail b/test/typecheck/pass/vec_length/v1_inc.sail
new file mode 100644
index 00000000..b72738d1
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1_inc.sail
@@ -0,0 +1,8 @@
+default Order inc
+$include <vector_inc.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[10];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect
new file mode 100644
index 00000000..d123cabd
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2.expect
@@ -0,0 +1,13 @@
+Type error at file "vec_length/v2.sail", line 7, character 11 to line 7, character 25
+
+  let z = [x with 10 = y];
+
+No overloadings for vector_update, tried:
+  bitvector_update:
+    Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+  plain_vector_update:
+    Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
diff --git a/test/typecheck/pass/vec_length/v2.sail b/test/typecheck/pass/vec_length/v2.sail
new file mode 100644
index 00000000..4df62e81
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2.sail
@@ -0,0 +1,9 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 10 = y];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect
new file mode 100644
index 00000000..e7d2b52f
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2_inc.expect
@@ -0,0 +1,13 @@
+Type error at file "vec_length/v2_inc.sail", line 7, character 11 to line 7, character 25
+
+  let z = [x with 10 = y];
+
+No overloadings for vector_update, tried:
+  bitvector_update:
+    Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+  plain_vector_update:
+    Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
diff --git a/test/typecheck/pass/vec_length/v2_inc.sail b/test/typecheck/pass/vec_length/v2_inc.sail
new file mode 100644
index 00000000..3f75fee1
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2_inc.sail
@@ -0,0 +1,9 @@
+default Order inc
+$include <vector_inc.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 10 = y];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length_inc.sail b/test/typecheck/pass/vec_length_inc.sail
new file mode 100644
index 00000000..a8dd707f
--- /dev/null
+++ b/test/typecheck/pass/vec_length_inc.sail
@@ -0,0 +1,9 @@
+default Order inc
+$include <vector_inc.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 5 = y];
+  ()
+}
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index ff70dc1b..ad2592df 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -4,9 +4,9 @@ set -e
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 SAILDIR="$DIR/../.."
 
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
+RED='\033[0;91m'
+GREEN='\033[0;92m'
+YELLOW='\033[0;93m'
 NC='\033[0m'
 
 mkdir -p $DIR/rtpass
@@ -50,9 +50,9 @@ printf "<testsuites>\n" >> $DIR/tests.xml
 
 for i in `ls $DIR/pass/ | grep sail`;
 do
-    if $SAILDIR/sail -ddump_tc_ast -dsanity $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i;
+    if $SAILDIR/sail -just_check -ddump_tc_ast -dsanity $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i;
     then
-	if $SAILDIR/sail -ddump_tc_ast -dmagic_hash -dno_cast -dsanity $DIR/rtpass/$i 2> /dev/null 1> $DIR/rtpass2/$i;
+	if $SAILDIR/sail -just_check -ddump_tc_ast -dmagic_hash -dno_cast -dsanity $DIR/rtpass/$i 2> /dev/null 1> $DIR/rtpass2/$i;
 	then
 	    if diff $DIR/rtpass/$i $DIR/rtpass2/$i;
 	    then
diff --git a/test/typecheck/update_errors.sh b/test/typecheck/update_errors.sh
new file mode 100755
index 00000000..ba436daf
--- /dev/null
+++ b/test/typecheck/update_errors.sh
@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+set -e
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+SAILDIR="$DIR/../.."
+
+
+for i in `ls $DIR/pass/ | grep sail`;
+do
+    shopt -s nullglob;
+    for file in $DIR/pass/${i%.sail}/*.sail;
+    do
+	pushd $DIR/pass > /dev/null;
+	$SAILDIR/sail ${i%.sail}/$(basename $file) 2> ${file%.sail}.expect || true;
+	popd > /dev/null
+    done
+done