Merge branch 'experiments' into mono-experiments

3 files changed, 235 insertions, 80 deletions

diff --git a/test/typecheck/pass/mips400.sail b/test/typecheck/pass/mips400.sail
index 1e8691d9..951f5126 100644
--- a/test/typecheck/pass/mips400.sail
+++ b/test/typecheck/pass/mips400.sail
@@ -1,148 +1,300 @@
 (* New typechecker prelude *)
 
-val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned
+val cast forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned
+
+val forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0 - (2**('m - 1)):2**('m - 1) - 1|] effect pure signed
+
+val extern forall Num 'n, Num 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec = "to_vec_dec"
+
+val extern forall Num 'm. int -> vector<'m - 1,'m,dec,bit> effect pure to_svec = "to_vec_dec"
 
 (* Vector access can't actually be properly polymorphic on vector
    direction because of the ranges being different for each type, so
    we overload it instead *)
-val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
-val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
+val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+val forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec
+val forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc
+
+overload vector_access [bitvector_access_inc; bitvector_access_dec; vector_access_inc; vector_access_dec]
 
 (* Type safe vector subrange *)
-val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
-  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+(* vector_subrange(v, m, o) returns the subvector of v with elements with
+   indices from m up to and *including* o. *)
+val forall Num 'n, Num 'l, Num 'm, Num 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,('o - 'm) + 1,inc,'a> effect pure vector_subrange_inc
+
+val forall Num 'n, Num 'l, Num 'm, Num 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,('m - 'o) + 1,dec,'a> effect pure vector_subrange_dec
 
-val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
-  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - ('o - 1),dec,'a> effect pure vector_subrange_dec
+val forall Num 'n, Num 'l, Order 'ord.
+  (vector<'n,'l,'ord,bit>, int, int) -> list<bit> effect pure vector_subrange_bl
 
-overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+val forall Num 'n, Num 'l, Num 'm, Num 'o, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,bit>, [:'m:], [:'o:]) -> vector<'m,('o - 'm) + 1,inc,bit> effect pure bitvector_subrange_inc
+
+val forall Num 'n, Num 'l, Num 'm, Num 'o, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,bit>, [:'m:], [:'o:]) -> vector<'m,('m - 'o) + 1,dec,bit> effect pure bitvector_subrange_dec
+
+overload vector_subrange [bitvector_subrange_inc; bitvector_subrange_dec; vector_subrange_inc; vector_subrange_dec; vector_subrange_bl]
 
 (* Type safe vector append *)
-val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
-  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vec_append = "vector_concat"
+
+val (list<bit>, list<bit>) -> list<bit> effect pure list_append
+
+val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,bit> effect pure bitvec_append = "bitvector_concat"
+
+overload vector_append [bitvec_append; vec_append; list_append]
 
 (* Implicit register dereferencing *)
 val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref
 
-overload vector_access [vector_access_inc; vector_access_dec]
-
 (* Bitvector duplication *)
-val forall Nat 'n. (bit, [:'n:]) -> vector<'n - 1,'n,dec,bit> effect pure duplicate
+val forall Num 'n. (bit, [:'n:]) -> vector<'n - 1,'n,dec,bit> effect pure duplicate
 
-val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord.
+val (bit, int) -> list<bit> effect pure duplicate_to_list
+
+val forall Num 'n, Num 'm, Num 'o, Order 'ord.
   (vector<'o,'n,'ord,bit>, [:'m:]) -> vector<'o,'m*'n,'ord,bit> effect pure duplicate_bits
 
-overload (deinfix ^^) [duplicate; duplicate_bits]
+val forall Num 'n, Num 'o, Order 'ord.
+  (vector<'o,'n,'ord,bit>, int) -> list<bit> effect pure duplicate_bits_to_list
+
+overload (deinfix ^^) [duplicate; duplicate_bits; duplicate_to_list; duplicate_bits_to_list]
 
 (* Bitvector extension *)
-val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
+val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
     vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz
 
-val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
+val forall Num 'm, Num 'p, Order 'ord.
+    list<bit> -> vector<'p, 'm, 'ord, bit> effect pure extz_bl
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
     vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts
 
-overload EXTZ [extz]
-overload EXTS [exts]
+val forall Num 'm, Num 'p, Order 'ord.
+    list<bit> -> vector<'p, 'm, 'ord, bit> effect pure exts_bl
+
+(* If we want an automatic bitvector extension, then this is the function to
+   use, but I've disabled the cast because it hides signedness bugs. *)
+val (*cast*) forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'n.
+    vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extzi
 
-val forall Type 'a, Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord, 'm >= 'o.
+overload EXTZ [extz; extz_bl]
+overload EXTS [exts; exts_bl]
+
+val forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o.
     vector<'n, 'm, 'ord, 'a> -> vector<'p, 'o, 'ord, 'a> effect pure mask
 
 (* Adjust the start index of a decreasing bitvector *)
-val cast forall Nat 'n, Nat 'm, Nat 'o, 'n >= 'm - 1, 'o >= 'm - 1.
+val cast forall Num 'n, Num 'm, 'n >= 'm - 1.
+  vector<'n,'m,dec,bit> -> vector<'m - 1,'m,dec,bit>
+  effect pure norm_dec
+
+val cast forall Num 'n, Num 'm, Num 'o, 'n >= 'm - 1, 'o >= 'm - 1.
   vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit>
   effect pure adjust_dec
 
 (* Various casts from 0 and 1 to bitvectors *)
-val cast forall Nat 'n, Nat 'l, Order 'ord. [:0:] -> vector<'n,'l,'ord,bit> effect pure cast_0_vec
-val cast forall Nat 'n, Nat 'l, Order 'ord. [:1:] -> vector<'n,'l,'ord,bit> effect pure cast_1_vec
-val cast forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec
+val cast forall Num 'n, Num 'l, Order 'ord. [:0:] -> vector<'n,'l,'ord,bit> effect pure cast_0_vec
+val cast forall Num 'n, Num 'l, Order 'ord. [:1:] -> vector<'n,'l,'ord,bit> effect pure cast_1_vec
+val cast forall Num 'n, Num 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec
 
-val cast forall Nat 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool
+val cast forall Num 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool
 val cast bit -> bool effect pure cast_bit_bool
 
+val cast forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. bit -> vector<'n,'m,dec,bit> effect pure cast_bit_vec
+
 (* MSB *)
-val forall Nat 'n, Nat 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect pure most_significant
+val forall Num 'n, Num 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect pure most_significant
 
 (* Arithmetic *)
 
-val forall Nat 'n, Nat 'm.
-    (atom<'n>, atom<'m>) -> atom<'n+'m> effect pure add
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
+    ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add
 
-val forall Nat 'n, Nat 'o, Nat 'p, Order 'ord.
-    (vector<'o, 'n, 'ord, bit>, vector<'p, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec
+val extern (nat, nat) -> nat effect pure add_nat = "add"
 
-val forall Nat 'n, Nat 'o, Nat 'p, Nat 'q, Order 'ord.
-    (vector<'o, 'n, 'ord, bit>, vector<'p, 'n, 'ord, bit>) -> range<'q, 2**'n> effect pure add_vec_vec_range
+val extern (int, int) -> int effect pure add_int = "add"
 
-(* FIXME: the parser is broken for 2**... it's just been hacked to work for this common case *)
-val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o <= 2** 'm - 1.
-    (vector<'n, 'm, 'ord, bit>, atom<'o>) -> vector<'n, 'm, 'ord, bit> effect pure add_vec_range
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec
 
-val forall Nat 'n, Nat 'o, Nat 'p, Order 'ord.
-    (vector<'o, 'n, 'ord, bit>, vector<'p, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure add_vec_int
 
-(* but it doesn't parse this
-val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o <= 2** 'm - 1.
-    (vector<'n, 'm, 'ord, bit>, atom<'o>) -> range<'o, 'o+2** 'm> effect pure add_vec_range_range
-    *)
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec
 
-val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o <= 2** 'm - 1.
-    (atom<'o>, vector<'n, 'm, 'ord, bit>) -> vector<'n, 'm, 'ord, bit> effect pure add_range_vec
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
+    ([|'n:'m|], [|'o:'p|]) -> [|'n - 'p:'m - 'o|] effect pure sub
 
-(* or this
-val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o <= 2** 'm - 1.
-    (atom<'o>, vector<'n, 'm, 'ord, bit>) -> range<'o, 'o+2**'m-1> effect pure add_range_vec_range
-*)
+val extern (int, int) -> int effect pure sub_int = "sub"
 
-val forall Nat 'o, Nat 'p, Order 'ord.
-    (vector<'o, 'p, 'ord, bit>, bit) -> vector<'o, 'p, 'ord, bit> effect pure add_vec_bit
+val forall Num 'n, Num 'm, Order 'ord.
+    (vector<'n,'m,'ord,bit>, int) -> vector<'n,'m,'ord,bit> effect pure sub_vec_int
 
-val forall Nat 'o, Nat 'p, Order 'ord.
-    (bit, vector<'o, 'p, 'ord, bit>) -> vector<'o, 'p, 'ord, bit> effect pure add_bit_vec
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure sub_vec
 
-val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure sub_exact
-val forall Nat 'n, Nat 'm, Nat 'o, 'o <= 'm - 'n. ([|'n:'m|], [:'o:]) -> [|'n:'m - 'o|] effect pure sub_range
-val forall Nat 'n, Nat 'm, Order 'ord. (vector<'n,'m,'ord,bit>, int) -> vector<'n,'m,'ord,bit> effect pure sub_bv
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure sub_underflow_vec
 
 overload (deinfix +) [
-  add;
   add_vec;
-  add_vec_vec_range;
-  add_vec_range;
   add_overflow_vec;
-  add_vec_range_range;
-  add_range_vec;
-  add_range_vec_range;
-  add_vec_bit;
-  add_bit_vec;
+  add_vec_int;
+  add;
+  add_nat;
+  add_int
 ]
 
 overload (deinfix -) [
-  sub_exact;
-  sub_bv;
-  sub_range;
+  sub_vec_int;
+  sub_vec;
+  sub_underflow_vec;
+  sub;
+  sub_int
 ]
 
-(* Equality *)
+val extern bool -> bit effect pure bool_to_bit = "bool_to_bitU"
 
-(* Sail gives a bunch of overloads for equality, but apparantly also
-gives an equality and inequality for any type 'a, so why bother
-overloading? *)
+val (int, int) -> int effect pure mul_int
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mul_vec
 
-val forall Type 'a. ('a, 'a) -> bool effect pure eq
-val forall Type 'a. ('a, 'a) -> bool effect pure neq
+overload (deinfix * ) [
+  mul_vec;
+  mul_int
+]
+
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mul_svec
+
+overload (deinfix *_s) [
+  mul_svec
+]
+
+val extern (bool, bool) -> bool effect pure bool_xor
+
+val extern forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure xor_vec = "bitwise_xor"
+
+overload (deinfix ^) [
+  bool_xor;
+  xor_vec
+]
+
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure shiftl
+
+overload (deinfix <<) [
+  shiftl
+]
 
-overload (deinfix ==) [eq]
-overload (deinfix !=) [neq]
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure shiftr
+
+overload (deinfix >>) [
+  shiftr
+]
 
 (* Boolean operators *)
-val bool -> bool effect pure bool_not
+val extern bool -> bool effect pure bool_not = "not"
 val (bool, bool) -> bool effect pure bool_or
 val (bool, bool) -> bool effect pure bool_and
 
-overload ~ [bool_not]
-overload (deinfix &) [bool_and]
-overload (deinfix |) [bool_or]
+val forall Num 'n, Num 'm, Order 'ord.
+    vector<'n,'m,'ord,bit> -> vector<'n,'m,'ord,bit> effect pure bitwise_not
+
+val forall Num 'n, Num 'm, Order 'ord.
+    (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> vector<'n,'m,'ord,bit> effect pure bitwise_and
+
+val forall Num 'n, Num 'm, Order 'ord.
+    (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> vector<'n,'m,'ord,bit> effect pure bitwise_or
+
+overload ~ [bool_not; bitwise_not]
+overload (deinfix &) [bool_and; bitwise_and]
+overload (deinfix |) [bool_or; bitwise_or]
+
+(* Equality *)
+
+val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure eq_vec
+
+val forall Type 'a. ('a, 'a) -> bool effect pure eq
+
+val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure neq_vec
+
+val forall Type 'a. ('a, 'a) -> bool effect pure neq
+
+function forall Num 'n, Num 'm, Order 'ord. bool neq_vec (v1, v2) = bool_not(eq_vec(v1, v2))
+
+overload (deinfix ==) [eq_vec; eq]
+overload (deinfix !=) [neq_vec; neq]
+
+val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gteq_vec
+val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gt_vec
+val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lteq_vec
+val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lt_vec
+
+val extern (int, int) -> bool effect pure gteq_int = "gteq"
+val extern (int, int) -> bool effect pure gt_int = "gt"
+val extern (int, int) -> bool effect pure lteq_int = "lteq"
+val extern (int, int) -> bool effect pure lt_int = "lt"
+
+val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt"
+val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq"
+val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt"
+val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq"
+val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt"
+val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq"
+val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt"
+val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq"
+
+val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lteq_atom_atom = "lteq"
+val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gteq_atom_atom = "gteq"
+val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lt_atom_atom = "lt"
+val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gt_atom_atom = "gt"
+
+overload (deinfix >=) [gteq_atom_atom; gteq_range_atom; gteq_atom_range; gteq_vec; gteq_int]
+overload (deinfix >) [gt_atom_atom; gt_vec; gt_int]
+overload (deinfix <=) [lteq_atom_atom; lteq_range_atom; lteq_atom_range; lteq_vec; lteq_int]
+overload (deinfix <) [lt_atom_atom; lt_vec; lt_int]
+
+val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gteq_svec
+val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gt_svec
+val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lteq_svec
+val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lt_svec
+
+overload (deinfix <_s) [lt_svec]
+overload (deinfix <=_s) [lteq_svec]
+overload (deinfix >_s) [gt_svec]
+overload (deinfix >=_s) [gteq_svec]
+
+val (int, int) -> int effect pure quotient
+
+overload (deinfix quot) [quotient]
+
+val (int, int) -> int effect pure modulo
+
+overload (deinfix mod) [modulo]
+
+val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure vec_length = "length"
+val forall Type 'a. list<'a> -> nat effect pure list_length
+
+val extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [:'m:] effect pure bitvector_length = "bvlength"
+
+overload length [bitvector_length; vector_length; list_length]
+
+val cast forall Num 'n. [:'n:] -> [|'n|] effect pure upper
+
+typedef option = const union forall Type 'a. {
+    None;
+    'a Some
+}
 
 (* Mips spec starts here *)
 
@@ -338,7 +490,7 @@ register (TLBEntry) TLBEntry61
 register (TLBEntry) TLBEntry62
 register (TLBEntry) TLBEntry63
 
-let (vector <0, 64, inc, (TLBEntry)>) TLBEntries = [
+let (vector <0, 64, inc, (register<TLBEntry>)>) TLBEntries = [
 TLBEntry00,
 TLBEntry01,
 TLBEntry02,
@@ -629,3 +781,5 @@ function unit checkCP0Access () =
         SignalException(CpU);
       }
   }
+
+function forall Type 'o. 'o SignalException ((Exception) ex) = SignalExceptionMIPS(ex, 0x0000000000000000)
diff --git a/test/typecheck/pass/phantom_num.sail b/test/typecheck/pass/phantom_num.sail
index c4ff8b13..c676807d 100644
--- a/test/typecheck/pass/phantom_num.sail
+++ b/test/typecheck/pass/phantom_num.sail
@@ -1,5 +1,5 @@
 
-val extern (int, int) -> bool effect pure gt_int
+val extern (int, int) -> bool effect pure gt_int = "gt"
 
 (* val cast forall Num 'n, Num 'm. [|'n:'m|] -> int effect pure cast_range_int *)
 
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index 073a6251..12e6acc0 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -109,11 +109,12 @@ function test_lem {
 
 	    cp $MIPS/mips_extras_embed_sequential.lem $DIR/lem/
 	    mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/
+	    mv $SAILDIR/${i%%.*}_embed_types_sequential.lem $DIR/lem/
 	    mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/
 	    mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/
 	    # Test sequential embedding for now
 	    # TODO: Add tests for the free monad
-	    if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/mips_extras_embed_sequential.lem $DIR/lem/${i%%.*}_embed_types.lem $DIR/lem/${i%%.*}_embed_sequential.lem 2> /dev/null
+	    if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/mips_extras_embed_sequential.lem $DIR/lem/${i%%.*}_embed_types_sequential.lem $DIR/lem/${i%%.*}_embed_sequential.lem 2> /dev/null
 	    then
 		green "typechecking lem for $1/$i" "pass"
 	    else