From 6100aecd642766252b73d3271a026d17de605fa0 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 8 Aug 2017 13:52:49 +0100
Subject: Fix Lem bindings in test cases

Add a test case with the MIPS spec using the TLB stub.
Use the sequential monad for Lem testing for now; the free monad (in
"prompt.lem") has not been updated for machine words yet.
---
 mips_new_tc/mips_extras_embed_sequential.lem      | 51 +++++++++++++++++++++++
 mips_new_tc/mips_insts.sail                       | 28 ++++++-------
 src/pretty_print_lem.ml                           | 28 +++++++++----
 test/typecheck/pass/add_vec_lit.sail              |  2 +-
 test/typecheck/pass/arm_FPEXC1.sail               |  6 +--
 test/typecheck/pass/bv_simple_index.sail          |  6 +--
 test/typecheck/pass/bv_simple_index_bit.sail      |  6 +--
 test/typecheck/pass/case_simple_constraints.sail  |  6 +--
 test/typecheck/pass/deinfix_plus.sail             |  2 +-
 test/typecheck/pass/flow_gt1.sail                 | 20 ++++-----
 test/typecheck/pass/flow_gteq1.sail               | 20 ++++-----
 test/typecheck/pass/flow_lt1.sail                 | 14 +++++--
 test/typecheck/pass/flow_lt2.sail                 | 14 +++++--
 test/typecheck/pass/flow_lt_assign.sail           | 14 +++++--
 test/typecheck/pass/flow_lteq1.sail               | 20 ++++-----
 test/typecheck/pass/mips_CP0Cause_BD_assign1.sail |  4 +-
 test/typecheck/pass/mips_CP0Cause_BD_assign2.sail |  4 +-
 test/typecheck/pass/mips_CP0Cause_access.sail     |  6 +--
 test/typecheck/pass/mips_reg_field_bit.sail       |  6 +--
 test/typecheck/pass/mips_reg_field_bv.sail        |  6 +--
 test/typecheck/pass/overload_plus.sail            |  2 +-
 test/typecheck/pass/regtyp_vec.sail               |  4 +-
 test/typecheck/pass/set_mark.sail                 |  2 +-
 test/typecheck/pass/set_mark2.sail                |  2 +-
 test/typecheck/pass/vec_pat1.sail                 | 14 +++----
 test/typecheck/pass/vector_append.sail            |  7 ++--
 test/typecheck/pass/vector_append_gen.sail        |  8 ++--
 test/typecheck/pass/vector_subrange_gen.sail      | 15 +++----
 test/typecheck/pass/vector_synonym_cast.sail      |  2 +-
 test/typecheck/run_tests.sh                       | 11 ++++-
 30 files changed, 208 insertions(+), 122 deletions(-)
 create mode 100644 mips_new_tc/mips_extras_embed_sequential.lem

diff --git a/mips_new_tc/mips_extras_embed_sequential.lem b/mips_new_tc/mips_extras_embed_sequential.lem
new file mode 100644
index 00000000..ad567598
--- /dev/null
+++ b/mips_new_tc/mips_extras_embed_sequential.lem
@@ -0,0 +1,51 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail_impl_base
+open import Sail_values
+open import State
+
+val MEMr             : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitvector 'b)
+val MEMr_reserve     : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitvector 'b)
+val MEMr_tag         : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitU * bitvector 'b)
+val MEMr_tag_reserve : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitU * bitvector 'b)
+
+let MEMr (addr,size)             = read_mem false Read_plain addr size
+let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
+
+let MEMr_tag (addr,size) =
+  read_mem false Read_plain addr size >>= fun v ->
+  read_tag false Read_plain addr >>= fun t ->
+  return (t, v)
+
+let MEMr_tag_reserve (addr,size) =
+  read_mem false Read_plain addr size >>= fun v ->
+  read_tag false Read_plain addr >>= fun t ->
+  return (t, v)
+
+
+val MEMea                 : forall 'a. (bitvector 'a * integer) -> M unit
+val MEMea_conditional     : forall 'a. (bitvector 'a * integer) -> M unit
+val MEMea_tag             : forall 'a. (bitvector 'a * integer) -> M unit
+val MEMea_tag_conditional : forall 'a. (bitvector 'a * integer) -> M unit
+
+let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
+let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
+
+let MEMea_tag (addr,size)             = write_mem_ea Write_plain addr size
+let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size
+
+
+val MEMval                 : forall 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M unit
+val MEMval_conditional     : forall 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M bool
+val MEMval_tag             : forall 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M unit
+val MEMval_tag_conditional : forall 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M bool
+
+let MEMval (_,_,v)                   = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional (_,_,v)       = write_mem_val v >>= fun b -> return (if b then true else false)
+let MEMval_tag (_,_,t,v)             = write_mem_val v >>= fun _ -> write_tag t >>= fun _ -> return ()
+let MEMval_tag_conditional (_,_,t,v) = write_mem_val v >>= fun b -> write_tag t >>= fun _ -> return (if b then true else false)
+
+val MEM_sync  : unit -> M unit
+
+let MEM_sync () = barrier Barrier_MIPS_SYNC
+
diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail
index 1d3c5f4a..96826dae 100644
--- a/mips_new_tc/mips_insts.sail
+++ b/mips_new_tc/mips_insts.sail
@@ -1136,24 +1136,24 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) =
     else
       let pAddr = (TLBTranslate(vAddr, LoadData)) in
           {
-	    (bit[64]) memResult := if (linked) then
+            (bit[64]) memResult := if (linked) then
                 {
                   CP0LLBit  := 0b1;
-		  CP0LLAddr := pAddr;
-		  switch wordWidthBytes(width) {
-		    case ([:1:]) w -> extendLoad(MEMr_reserve_wrapper(pAddr, w), signed)
-		    case ([:2:]) w -> extendLoad(MEMr_reserve_wrapper(pAddr, w), signed)
-		    case ([:4:]) w -> extendLoad(MEMr_reserve_wrapper(pAddr, w), signed)
-		    case ([:8:]) w -> extendLoad(MEMr_reserve_wrapper(pAddr, w), signed)
-		  }
+                  CP0LLAddr := pAddr;
+                  w := wordWidthBytes(width);
+                  if w == 1 then extendLoad(MEMr_reserve_wrapper(pAddr, 1), signed)
+                  else if w == 2 then extendLoad(MEMr_reserve_wrapper(pAddr, 2), signed)
+                  else if w == 4 then extendLoad(MEMr_reserve_wrapper(pAddr, 4), signed)
+                  else extendLoad(MEMr_reserve_wrapper(pAddr, 8), signed)
                 }
               else
-		switch wordWidthBytes(width) {
-		  case ([:1:]) w -> extendLoad(MEMr_wrapper(pAddr, w), signed)
-		  case ([:2:]) w -> extendLoad(MEMr_wrapper(pAddr, w), signed)
-		  case ([:4:]) w -> extendLoad(MEMr_wrapper(pAddr, w), signed)
-		  case ([:8:]) w -> extendLoad(MEMr_wrapper(pAddr, w), signed)
-		};
+                {
+                  w := wordWidthBytes(width);
+                  if w == 1 then extendLoad(MEMr_reserve_wrapper(pAddr, 1), signed)
+                  else if w == 2 then extendLoad(MEMr_reserve_wrapper(pAddr, 2), signed)
+                  else if w == 4 then extendLoad(MEMr_reserve_wrapper(pAddr, 4), signed)
+                  else extendLoad(MEMr_reserve_wrapper(pAddr, 8), signed);
+                };
             wGPR(rt) := memResult
           }
   }
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 09f1a466..955a148c 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -273,11 +273,23 @@ let doc_lit_lem regtypes in_pat (L_aux(lit,l)) a =
   | L_real s -> utf8string s (* TODO What's the Lem syntax for reals? *)
 
 (* typ_doc is the doc for the type being quantified *)
+let doc_quant_item (QI_aux (qi, _)) = match qi with
+| QI_id (KOpt_aux (KOpt_none kid, _))
+| QI_id (KOpt_aux (KOpt_kind (_, kid), _)) -> doc_var kid
+| _ -> empty
 
-let doc_typquant_lem (TypQ_aux(tq,_)) typ_doc = typ_doc
+let doc_typquant_items_lem (TypQ_aux(tq,_)) = match tq with
+| TypQ_tq qs -> separate_map space doc_quant_item qs
+| _ -> empty
 
-let doc_typschm_lem regtypes (TypSchm_aux(TypSchm_ts(tq,t),_)) =
-  (doc_typquant_lem tq (doc_typ_lem regtypes t))
+let doc_typquant_lem (TypQ_aux(tq,_)) typ = match tq with
+| TypQ_tq ((_ :: _) as qs) ->
+  string "forall " ^^ separate_map space doc_quant_item qs ^^ string ". " ^^ typ
+| _ -> empty
+
+let doc_typschm_lem regtypes quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
+  if quants then (doc_typquant_lem tq (doc_typ_lem regtypes t))
+  else doc_typ_lem regtypes t
 
 let is_ctor env id = match Env.lookup_id id env with
 | Enum _ | Union _ -> true
@@ -960,7 +972,7 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with
 let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
   | TD_abbrev(id,nm,typschm) ->
      doc_op equals (concat [string "type"; space; doc_id_lem_type id])
-            (doc_typschm_lem regtypes typschm)
+            (doc_typschm_lem regtypes false typschm)
   | TD_record(id,nm,typq,fs,_) ->
      let f_pp (typ,fid) =
        let fname = if prefix_recordtype
@@ -970,7 +982,7 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
       let fs_doc = group (separate_map (break 1) f_pp fs) in
       doc_op equals
              (concat [string "type"; space; doc_id_lem_type id;])
-             (doc_typquant_lem typq (anglebars (space ^^ align fs_doc ^^ space)))
+             ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space)))
   | TD_variant(id,nm,typq,ar,_) ->
      (match id with
       | Id_aux ((Id "read_kind"),_) -> empty
@@ -987,8 +999,8 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
          let typ_pp =
 
            (doc_op equals)
-             (concat [string "type"; space; doc_id_lem_type id;])
-             (doc_typquant_lem typq ar_doc) in
+             (concat [string "type"; space; doc_id_lem_type id; space; doc_typquant_items_lem typq])
+             ((*doc_typquant_lem typq*) ar_doc) in
          let make_id pat id =
            separate space [string "SIA.Id_aux";
                            parens (string "SIA.Id " ^^ string_lit (doc_id id));
@@ -1210,7 +1222,7 @@ let doc_rec_lem (Rec_aux(r,_)) = match r with
   | Rec_rec -> space ^^ string "rec" ^^ space
 
 let doc_tannot_opt_lem regtypes (Typ_annot_opt_aux(t,_)) = match t with
-  | Typ_annot_opt_some(tq,typ) -> doc_typquant_lem tq (doc_typ_lem regtypes typ)
+  | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem regtypes typ)
 
 let doc_funcl_lem regtypes (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
   group (prefix 3 1 ((doc_pat_lem regtypes false pat) ^^ space ^^ arrow)
diff --git a/test/typecheck/pass/add_vec_lit.sail b/test/typecheck/pass/add_vec_lit.sail
index be897021..4d662a8d 100644
--- a/test/typecheck/pass/add_vec_lit.sail
+++ b/test/typecheck/pass/add_vec_lit.sail
@@ -3,7 +3,7 @@ default Order inc
 val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure add_vec = "add_vec"
 val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add_range"
 
-val cast forall Num 'n. bit['n] -> [|0: 2** 'n - 1|] effect pure cast_vec_range
+val cast forall Num 'n. bit['n] -> [|0: 2** 'n - 1|] effect pure unsigned
 
 overload (deinfix +) [add_vec; add_range]
 
diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail
index cfae86a1..f711a5ad 100644
--- a/test/typecheck/pass/arm_FPEXC1.sail
+++ b/test/typecheck/pass/arm_FPEXC1.sail
@@ -1,9 +1,9 @@
 default Order dec
 
-val forall Num 'n. (bit['n], int) -> bit effect pure vector_access
+val extern forall Num 'n. (bit['n], int) -> bit effect pure vector_access = "bitvector_access_dec"
 
-val forall Num 'n, Num 'm, Num 'o, 'm >= 'o, 'o >= 0, 'n >= 'm + 1.
-  (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange
+val extern forall Num 'n, Num 'm, Num 'o, 'm >= 'o, 'o >= 0, 'n >= 'm + 1.
+  (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange = "bitvector_subrange_dec"
 
 register vector<32 - 1, 32, dec, bit>  _FPEXC32_EL2
 
diff --git a/test/typecheck/pass/bv_simple_index.sail b/test/typecheck/pass/bv_simple_index.sail
index 72e1b094..811b3a5b 100644
--- a/test/typecheck/pass/bv_simple_index.sail
+++ b/test/typecheck/pass/bv_simple_index.sail
@@ -1,7 +1,7 @@
-val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
-val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec
+val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc
 
-overload vector_access [vector_access_inc; vector_access_dec]
+overload vector_access [bitvector_access_inc; bitvector_access_dec]
 
 val cast bit -> bool effect pure cast_bit_bool
 
diff --git a/test/typecheck/pass/bv_simple_index_bit.sail b/test/typecheck/pass/bv_simple_index_bit.sail
index 2ba5b928..46bc19d6 100644
--- a/test/typecheck/pass/bv_simple_index_bit.sail
+++ b/test/typecheck/pass/bv_simple_index_bit.sail
@@ -1,7 +1,7 @@
-val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
-val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec
+val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc
 
-overload vector_access [vector_access_inc; vector_access_dec]
+overload vector_access [bitvector_access_inc; bitvector_access_dec]
 
 function bit bv ((bit[64]) x) =
 {
diff --git a/test/typecheck/pass/case_simple_constraints.sail b/test/typecheck/pass/case_simple_constraints.sail
index f1b87235..335e10ee 100644
--- a/test/typecheck/pass/case_simple_constraints.sail
+++ b/test/typecheck/pass/case_simple_constraints.sail
@@ -1,9 +1,9 @@
 
-val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
+val extern forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus = "add"
 
-val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id 
+val extern forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id = "id"
 
-val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+val extern forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id = "id"
 
 val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
 
diff --git a/test/typecheck/pass/deinfix_plus.sail b/test/typecheck/pass/deinfix_plus.sail
index c5a0f1ee..8fc7c00e 100644
--- a/test/typecheck/pass/deinfix_plus.sail
+++ b/test/typecheck/pass/deinfix_plus.sail
@@ -1,6 +1,6 @@
 default Order inc
 
-val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc"
+val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "add_vec"
   
 overload (deinfix +) [bv_add]
 
diff --git a/test/typecheck/pass/flow_gt1.sail b/test/typecheck/pass/flow_gt1.sail
index acfbab68..ddeefd53 100644
--- a/test/typecheck/pass/flow_gt1.sail
+++ b/test/typecheck/pass/flow_gt1.sail
@@ -1,17 +1,17 @@
 default Order inc
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add"
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub"
 
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
+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"
 
 overload (deinfix +) [add_range]
 overload (deinfix -) [sub_range]
diff --git a/test/typecheck/pass/flow_gteq1.sail b/test/typecheck/pass/flow_gteq1.sail
index 8918438c..47f7aa0f 100644
--- a/test/typecheck/pass/flow_gteq1.sail
+++ b/test/typecheck/pass/flow_gteq1.sail
@@ -1,17 +1,17 @@
 default Order inc
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add"
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub"
 
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
+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"
 
 overload (deinfix +) [add_range]
 overload (deinfix -) [sub_range]
diff --git a/test/typecheck/pass/flow_lt1.sail b/test/typecheck/pass/flow_lt1.sail
index 0f3c1bbc..c210ed7a 100644
--- a/test/typecheck/pass/flow_lt1.sail
+++ b/test/typecheck/pass/flow_lt1.sail
@@ -1,11 +1,17 @@
 default Order inc
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add"
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub"
 
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
+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"
 
 overload (deinfix +) [add_range]
 overload (deinfix -) [sub_range]
diff --git a/test/typecheck/pass/flow_lt2.sail b/test/typecheck/pass/flow_lt2.sail
index effe0bc4..cccebaa3 100644
--- a/test/typecheck/pass/flow_lt2.sail
+++ b/test/typecheck/pass/flow_lt2.sail
@@ -1,11 +1,17 @@
 default Order inc
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add"
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub"
 
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
+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"
 
 overload (deinfix +) [add_range]
 overload (deinfix -) [sub_range]
diff --git a/test/typecheck/pass/flow_lt_assign.sail b/test/typecheck/pass/flow_lt_assign.sail
index 4e787741..9601f48f 100644
--- a/test/typecheck/pass/flow_lt_assign.sail
+++ b/test/typecheck/pass/flow_lt_assign.sail
@@ -1,11 +1,17 @@
 default Order inc
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add"
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub"
 
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
+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"
 
 overload (deinfix +) [add_range]
 overload (deinfix -) [sub_range]
diff --git a/test/typecheck/pass/flow_lteq1.sail b/test/typecheck/pass/flow_lteq1.sail
index d32831a2..ffa4dd8b 100644
--- a/test/typecheck/pass/flow_lteq1.sail
+++ b/test/typecheck/pass/flow_lteq1.sail
@@ -1,17 +1,17 @@
 default Order inc
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add"
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub"
 
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
-val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
+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"
 
 overload (deinfix +) [add_range]
 overload (deinfix -) [sub_range]
diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
index 4dc63e71..7808b2c0 100644
--- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
+++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail
@@ -1,5 +1,5 @@
-val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv
-val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv
+val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec
+val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec
 
 default Order dec
 
diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
index b35a0767..26f161e2 100644
--- a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
+++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail
@@ -1,5 +1,5 @@
-val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv
-val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv
+val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec
+val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec
     
 default Order dec
 
diff --git a/test/typecheck/pass/mips_CP0Cause_access.sail b/test/typecheck/pass/mips_CP0Cause_access.sail
index c0e318c4..eb3b9389 100644
--- a/test/typecheck/pass/mips_CP0Cause_access.sail
+++ b/test/typecheck/pass/mips_CP0Cause_access.sail
@@ -3,10 +3,10 @@
   effect pure ADJUST
 *)
 
-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 Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+val extern forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec
+val extern forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc
 
-overload vector_access [vector_access_inc; vector_access_dec]
+overload vector_access [bitvector_access_inc; bitvector_access_dec]
     
 default Order dec
 
diff --git a/test/typecheck/pass/mips_reg_field_bit.sail b/test/typecheck/pass/mips_reg_field_bit.sail
index 33560bde..4c37a6e9 100644
--- a/test/typecheck/pass/mips_reg_field_bit.sail
+++ b/test/typecheck/pass/mips_reg_field_bit.sail
@@ -1,8 +1,8 @@
+default Order dec
+
 val cast forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1.
   vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit>
-  effect pure ADJUST
-
-default Order dec
+  effect pure adjust_dec
 
 typedef CauseReg = register bits [ 31 : 0 ] {
   31       : BD; (* branch delay *)
diff --git a/test/typecheck/pass/mips_reg_field_bv.sail b/test/typecheck/pass/mips_reg_field_bv.sail
index 4b82d4de..0ce19b4f 100644
--- a/test/typecheck/pass/mips_reg_field_bv.sail
+++ b/test/typecheck/pass/mips_reg_field_bv.sail
@@ -1,8 +1,8 @@
+default Order dec
+
 val cast forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1.
   vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit>
-  effect pure ADJUST
-
-default Order dec
+  effect pure adjust_dec
 
 typedef CauseReg = register bits [ 31 : 0 ] {
   31       : BD; (* branch delay *)
diff --git a/test/typecheck/pass/overload_plus.sail b/test/typecheck/pass/overload_plus.sail
index 5390a5a4..2aa8ecc5 100644
--- a/test/typecheck/pass/overload_plus.sail
+++ b/test/typecheck/pass/overload_plus.sail
@@ -1,6 +1,6 @@
 default Order inc
 
-val extern forall Nat 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc"
+val extern forall Nat 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "add_vec"
   
 overload (deinfix +) [bv_add]
 
diff --git a/test/typecheck/pass/regtyp_vec.sail b/test/typecheck/pass/regtyp_vec.sail
index c939cce8..28978882 100644
--- a/test/typecheck/pass/regtyp_vec.sail
+++ b/test/typecheck/pass/regtyp_vec.sail
@@ -3,12 +3,12 @@
   effect pure ADJUST
 *)
 
-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, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_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
 *)
 
-overload vector_access [vector_access_dec]
+overload vector_access [bitvector_access_dec]
 
 default Order dec
 
diff --git a/test/typecheck/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail
index 59710c46..7bc7370b 100644
--- a/test/typecheck/pass/set_mark.sail
+++ b/test/typecheck/pass/set_mark.sail
@@ -1,5 +1,5 @@
 
-val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_zero_bv
+val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec
 
 function forall Num 'N, 'N IN {32}. bit['N] Foo32( (bit['N]) x) = x
 
diff --git a/test/typecheck/pass/set_mark2.sail b/test/typecheck/pass/set_mark2.sail
index c1433058..cabfb1af 100644
--- a/test/typecheck/pass/set_mark2.sail
+++ b/test/typecheck/pass/set_mark2.sail
@@ -1,4 +1,4 @@
-val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_zero_bv
+val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec
 
 function forall Nat 'N, 'N IN {32, 64}. bit['N] Foo32( (bit['N]) x) = x
 
diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail
index 95c8880e..fe9b4a0a 100644
--- a/test/typecheck/pass/vec_pat1.sail
+++ b/test/typecheck/pass/vec_pat1.sail
@@ -1,16 +1,16 @@
 default Order inc
 
-val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc"
+val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "add_vec"
 
-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 + 1 - 'm,inc,'a> effect pure vector_subrange
+val extern 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 + 1 - 'm,inc,bit> effect pure vector_subrange = "bitvector_subrange_inc"
 
-val forall Num 'n, Num 'm, Num 'o, Num 'p, Type 'a.
-  (vector<'n,'m,inc,'a>, vector<'o,'p,inc,'a>) -> vector<'n,'m + 'p,inc,'a>
-  effect pure vector_append_inc
+val forall Num 'n, Num 'm, Num 'o, Num 'p.
+  (vector<'n,'m,inc,bit>, vector<'o,'p,inc,bit>) -> vector<'n,'m + 'p,inc,bit>
+  effect pure bitvector_concat
 
 overload (deinfix +) [bv_add]
-overload vector_append [vector_append_inc]
+overload vector_append [bitvector_concat]
 
 val (bit[3], bit[3]) -> bit[3] effect pure test
 
diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail
index af83c44d..17db3fbd 100644
--- a/test/typecheck/pass/vector_append.sail
+++ b/test/typecheck/pass/vector_append.sail
@@ -1,7 +1,6 @@
 
-
-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 Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat"
 
 default Order inc
 
@@ -12,4 +11,4 @@ function bit[8] test (v1, v2) =
   zv := vector_append(v1, v2);
   zv := v1 : v2;
   zv
-}
\ No newline at end of file
+}
diff --git a/test/typecheck/pass/vector_append_gen.sail b/test/typecheck/pass/vector_append_gen.sail
index ddb027ee..ce63ed87 100644
--- a/test/typecheck/pass/vector_append_gen.sail
+++ b/test/typecheck/pass/vector_append_gen.sail
@@ -1,8 +1,6 @@
 
-val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
-
-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 Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat"
 
 default Order inc
 
@@ -11,4 +9,4 @@ val forall 'n, 'm, 'n >= 0, 'm >= 0. (bit['n], bit['m]) -> bit['n + 'm] effect p
 function forall 'n, 'm. bit['n + 'm] test (v1, v2) =
 {
   vector_append(v1, v2);
-}
\ No newline at end of file
+}
diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail
index 8857bd18..4ec067de 100644
--- a/test/typecheck/pass/vector_subrange_gen.sail
+++ b/test/typecheck/pass/vector_subrange_gen.sail
@@ -4,17 +4,18 @@ val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'
 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 forall Nat 'n, Nat 'l, Nat 'm, Nat 'u, Order 'o, Type 'a, 'l >= 0, 'm <= 'u, 'u <= 'l. (vector<'n,'l,'o,'a>, [:'m:], [:'u:]) -> vector<'m,'u - 'm,'o,'a> effect pure vector_subrange
+val extern 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 vector_subrange = "bitvector_subrange_inc"
 
-val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure minus
+val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure sub
 
 default Order inc
 
-val forall 'n, 'm, 'n >= 5. bit['n] -> bit['n - 2] effect pure test
+val forall 'n, 'm, 'n >= 5. bit['n] -> bit['n - 1] effect pure test
 
-function forall 'n, 'n >= 5. bit['n - 2] test v =
+function forall 'n, 'n >= 5. bit['n - 1] test v =
 {
-  z := vector_subrange(v, 0, minus(sizeof 'n, 2));
-  z := v[0 .. minus(sizeof 'n, 2)];
+  z := vector_subrange(v, 0, sub(sizeof 'n, 2));
+  z := v[0 .. sub(sizeof 'n, 2)];
   z
-}
\ No newline at end of file
+}
diff --git a/test/typecheck/pass/vector_synonym_cast.sail b/test/typecheck/pass/vector_synonym_cast.sail
index 72a7e9d0..f1de42e9 100644
--- a/test/typecheck/pass/vector_synonym_cast.sail
+++ b/test/typecheck/pass/vector_synonym_cast.sail
@@ -1,7 +1,7 @@
 
 typedef vecsyn = vector<0,1,dec,bit>
 
-val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure test_cast
+val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure adjust_dec
 
 val vector<1,1,dec,bit> -> vecsyn effect pure test
 
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index 5cca3a3a..073a6251 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -22,6 +22,7 @@ cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail > $DIR/pass/mips_prelude.s
 cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail > $DIR/pass/mips_tlb.sail
 cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail > $DIR/pass/mips_wrappers.sail
 cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_insts.sail
+cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb_stub.sail $MIPS/mips_wrappers.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_notlb.sail
 
 pass=0
 fail=0
@@ -99,14 +100,20 @@ finish_suite "Expecting fail"
 function test_lem {
     for i in `ls $DIR/pass/`;
     do
-	if $SAILDIR/sail -lem $DIR/$1/$i 2> /dev/null
+	# MIPS requires an additional library, Mips_extras_embed.
+	# It might be useful to allow adding options for specific test cases.
+	# For now, include the library for all test cases, which doesn't seem to hurt.
+	if $SAILDIR/sail -lem -lem_lib Mips_extras_embed $DIR/$1/$i 2> /dev/null
 	then
 	    green "generated lem for $1/$i" "pass"
 
+	    cp $MIPS/mips_extras_embed_sequential.lem $DIR/lem/
 	    mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/
 	    mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/
 	    mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/
-	    if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/${i%%.*}_embed_types.lem $DIR/lem/${i%%.*}_embed.lem 2> /dev/null
+	    # 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
 	    then
 		green "typechecking lem for $1/$i" "pass"
 	    else
-- 
cgit v1.2.3