Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-experiments

21 files changed, 1035 insertions, 355 deletions

diff --git a/src/Makefile b/src/Makefile
index 53acec6a..6cfcf874 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -78,11 +78,11 @@ ZARITH_LIB=$(ZARITH_DIR)/zarith.cmxa
 SAIL_LIB_DIR:=$(SAIL_DIR)/lib
 MIPS_SAIL_DIR:=$(SAIL_DIR)/mips_new_tc
 
-MIPS_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+MIPS_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
 MIPS_SAILS:=$(MIPS_SAILS_PRE) $(SAIL_DIR)/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
 
-MIPS_NOTLB_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+MIPS_NOTLB_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
 MIPS_NOTLB_SAILS:=$(MIPS_NOTLB_SAILS_PRE) $(SAIL_DIR)/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
 
@@ -170,14 +170,14 @@ _build/cheri_notlb.lem: $(CHERI_NOTLB_SAILS) ./sail.native
 	cd _build ;\
 	../sail.native -lem_ast -o cheri_notlb $(CHERI_NOTLB_SAILS)
 
-_build/cheri_embed_types.lem: $(CHERI_SAILS) ./sail.native
+_build/cheri_embed_types_sequential.lem: $(CHERI_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ;\
-	../sail.native -lem_lib "Mips_extras_embed" -lem -o cheri $(CHERI_SAILS)
+	../sail.native -lem_lib "Mips_extras_embed" -lem -lem_sequential -lem_mwords -o cheri $(CHERI_SAILS)
 
-_build/Cheri_embed_sequential.thy: _build/cheri_embed_types.lem
+_build/Cheri_embed_sequential.thy: _build/cheri_embed_types_sequential.lem
 	cd _build ;\
-	lem -isa -outdir . ../lem_interp/sail_impl_base.lem ../gen_lib/state.lem ../../mips/mips_extras_embed_sequential.lem cheri_embed_types.lem cheri_embed_sequential.lem
+	lem -isa -outdir . ../lem_interp/sail_impl_base.lem ../gen_lib/state.lem $(MIPS_SAIL_DIR)/mips_extras_embed_sequential.lem cheri_embed_types_sequential.lem cheri_embed_sequential.lem
 
 _build/mips_all.sail: $(MIPS_SAILS)
 	cat $(MIPS_SAILS) > $@
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 7d8797f9..aef1a05d 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -51,6 +51,8 @@ let no_annot = (Parse_ast.Unknown, ())
 let inc_ord = Ord_aux (Ord_inc, Parse_ast.Unknown)
 let dec_ord = Ord_aux (Ord_dec, Parse_ast.Unknown)
 
+let mk_id str = Id_aux (Id str, Parse_ast.Unknown)
+
 let mk_nc nc_aux = NC_aux (nc_aux, Parse_ast.Unknown)
 
 let mk_nexp nexp_aux = Nexp_aux (nexp_aux, Parse_ast.Unknown)
@@ -60,6 +62,8 @@ let unaux_exp (E_aux (exp_aux, _)) = exp_aux
 
 let mk_pat pat_aux = P_aux (pat_aux, no_annot)
 
+let mk_lexp lexp_aux = LEXP_aux (lexp_aux, no_annot)
+
 let mk_lit lit_aux = L_aux (lit_aux, Parse_ast.Unknown)
 
 let mk_lit_exp lit_aux = mk_exp (E_lit (mk_lit lit_aux))
@@ -73,9 +77,127 @@ let mk_fundef funcls =
   DEF_fundef
    (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), no_annot))
 
+let mk_letbind pat exp = LB_aux (LB_val_implicit (pat, exp), no_annot)
+
 let mk_val_spec vs_aux =
   DEF_spec (VS_aux (vs_aux, no_annot))
 
+let kopt_kid (KOpt_aux (kopt_aux, _)) =
+  match kopt_aux with
+  | KOpt_none kid | KOpt_kind (_, kid) -> kid
+
+let is_nat_kopt = function
+  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), _), _) -> true
+  | KOpt_aux (KOpt_none _, _) -> true
+  | _ -> false
+
+let is_order_kopt = function
+  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), _), _) -> true
+  | _ -> false
+
+let is_typ_kopt = function
+  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), _), _) -> true
+  | _ -> false
+
+let rec nexp_simp (Nexp_aux (nexp, l)) = Nexp_aux (nexp_simp_aux nexp, l)
+and nexp_simp_aux = function
+  | Nexp_minus (Nexp_aux (Nexp_sum (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 ->
+     nexp_simp_aux n1
+  | Nexp_sum (Nexp_aux (Nexp_minus (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 ->
+     nexp_simp_aux n1
+  | Nexp_sum (n1, n2) ->
+     begin
+       let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
+       let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
+       match n1_simp, n2_simp with
+       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 + c2)
+       | _, Nexp_neg n2 -> Nexp_minus (n1, n2)
+       | _, _ -> Nexp_sum (n1, n2)
+     end
+  | Nexp_times (n1, n2) ->
+     begin
+       let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
+       let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
+       match n1_simp, n2_simp with
+       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 * c2)
+       | _, _ -> Nexp_times (n1, n2)
+     end
+  | Nexp_minus (n1, n2) ->
+     begin
+       let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
+       let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
+       match n1_simp, n2_simp with
+       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 - c2)
+       | _, _ -> Nexp_minus (n1, n2)
+     end
+  | nexp -> nexp
+
+let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown)
+let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown)
+let mk_kid str = Kid_aux (Var ("'" ^ str), Parse_ast.Unknown)
+let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown)
+
+let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown)
+
+let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown)
+
+let int_typ = mk_id_typ (mk_id "int")
+let nat_typ = mk_id_typ (mk_id "nat")
+let unit_typ = mk_id_typ (mk_id "unit")
+let bit_typ = mk_id_typ (mk_id "bit")
+let real_typ = mk_id_typ (mk_id "real")
+let app_typ id args = mk_typ (Typ_app (id, args))
+let atom_typ nexp =
+  mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))]))
+let range_typ nexp1 nexp2 =
+  mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp1));
+                                   mk_typ_arg (Typ_arg_nexp (nexp_simp nexp2))]))
+let bool_typ = mk_id_typ (mk_id "bool")
+let string_typ = mk_id_typ (mk_id "string")
+let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)]))
+
+let vector_typ n m ord typ =
+  mk_typ (Typ_app (mk_id "vector",
+                   [mk_typ_arg (Typ_arg_nexp (nexp_simp n));
+                    mk_typ_arg (Typ_arg_nexp (nexp_simp m));
+                    mk_typ_arg (Typ_arg_order ord);
+                    mk_typ_arg (Typ_arg_typ typ)]))
+
+let exc_typ = mk_id_typ (mk_id "exception")
+
+let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown)
+let nminus n1 n2 = Nexp_aux (Nexp_minus (n1, n2), Parse_ast.Unknown)
+let nsum n1 n2 = Nexp_aux (Nexp_sum (n1, n2), Parse_ast.Unknown)
+let ntimes n1 n2 = Nexp_aux (Nexp_times (n1, n2), Parse_ast.Unknown)
+let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown)
+let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
+let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown)
+
+let nc_eq n1 n2 = mk_nc (NC_fixed (n1, n2))
+let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2))
+let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
+let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown)
+let nc_lt n1 n2 = nc_lteq n1 (nsum n2 (nconstant 1))
+let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nconstant 1))
+let nc_and nc1 nc2 = mk_nc (NC_and (nc1, nc2))
+let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2))
+let nc_true = mk_nc NC_true
+let nc_false = mk_nc NC_false
+
+let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown)
+
+let mk_fexp id exp = FE_aux (FE_Fexp (id, exp), no_annot)
+let mk_fexps fexps = FES_aux (FES_Fexps (fexps, false), no_annot)
+
+let mk_effect effs =
+  Effect_aux (Effect_set (List.map (fun be_aux -> BE_aux (be_aux, Parse_ast.Unknown)) effs), Parse_ast.Unknown)
+
+let no_effect = mk_effect []
+
+let quant_items : typquant -> quant_item list = function
+  | TypQ_aux (TypQ_tq qis, _) -> qis
+  | TypQ_aux (TypQ_no_forall, _) -> []
+
 let rec map_exp_annot f (E_aux (exp, annot)) = E_aux (map_exp_annot_aux f exp, f annot)
 and map_exp_annot_aux f = function
   | E_block xs -> E_block (List.map (map_exp_annot f) xs)
@@ -270,6 +392,11 @@ and string_of_n_constraint = function
   | NC_aux (NC_true, _) -> "true"
   | NC_aux (NC_false, _) -> "false"
 
+let string_of_annot = function
+  | Some (_, typ, eff) ->
+     "Some (_, " ^ string_of_typ typ ^ ", " ^ string_of_effect eff ^ ")"
+  | None -> "None"
+
 let string_of_quant_item_aux = function
   | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid
   | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> string_of_kind k ^ " " ^ string_of_kid kid
@@ -321,6 +448,8 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_cast (typ, exp) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_exp exp
   | E_vector vec -> "[" ^ string_of_list ", " string_of_exp vec ^ "]"
   | E_vector_access (v, n) -> string_of_exp v ^ "[" ^ string_of_exp n ^ "]"
+  | E_vector_update (v, n, exp) -> "[" ^ string_of_exp v ^ " with " ^ string_of_exp n ^ " = " ^ string_of_exp exp ^ "]"
+  | E_vector_update_subrange (v, n, m, exp) -> "[" ^ string_of_exp v ^ " with " ^ string_of_exp n ^ " .. " ^ string_of_exp m ^ " = " ^ string_of_exp exp ^ "]"
   | E_vector_subrange (v, n1, n2) -> string_of_exp v ^ "[" ^ string_of_exp n1 ^ " .. " ^ string_of_exp n2 ^ "]"
   | E_vector_append (v1, v2) -> string_of_exp v1 ^ " : " ^ string_of_exp v2
   | E_if (cond, then_branch, else_branch) ->
@@ -348,6 +477,8 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_comment _ -> "INTERNAL COMMENT"
   | E_comment_struc _ -> "INTERNAL COMMENT STRUC"
   | E_internal_let _ -> "INTERNAL LET"
+  | E_internal_return _ -> "INTERNAL RETURN"
+  | E_internal_plet _ -> "INTERNAL PLET"
   | _ -> "INTERNAL"
 and string_of_fexp (FE_aux (FE_Fexp (field, exp), _)) =
   string_of_id field ^ " = " ^ string_of_exp exp
@@ -471,11 +602,11 @@ let rec simplify_nexp (Nexp_aux (nexp, l)) =
   | Nexp_times (n1, n2) -> try_binop ( * ) n1 n2 (fun n1 n2 -> Nexp_times (n1, n2))
   | Nexp_sum (n1, n2) -> try_binop ( + ) n1 n2 (fun n1 n2 -> Nexp_sum (n1, n2))
   | Nexp_minus (n1, n2) -> try_binop ( - ) n1 n2 (fun n1 n2 -> Nexp_minus (n1, n2))
-  | Nexp_exp n ->
+  (* | Nexp_exp n ->
     (match simplify_nexp n with
       | Nexp_aux (Nexp_constant i, _) ->
         rewrap (Nexp_constant (power 2 i))
-      | n -> rewrap (Nexp_exp n))
+      | n -> rewrap (Nexp_exp n)) *)
   | Nexp_neg n ->
     (match simplify_nexp n with
       | Nexp_aux (Nexp_constant i, _) ->
@@ -503,13 +634,17 @@ let rec is_vector_typ = function
 let typ_app_args_of = function
   | Typ_aux (Typ_app (Id_aux (Id c,_), targs), l) ->
     (c, List.map (fun (Typ_arg_aux (a,_)) -> a) targs, l)
-  | Typ_aux (_, l) -> raise (Reporting_basic.err_typ l "typ_app_args_of called on non-app type")
+  | Typ_aux (_, l) as typ ->
+     raise (Reporting_basic.err_typ l
+       ("typ_app_args_of called on non-app type " ^ string_of_typ typ))
 
 let rec vector_typ_args_of typ = match typ_app_args_of typ with
   | ("vector", [Typ_arg_nexp start; Typ_arg_nexp len; Typ_arg_order ord; Typ_arg_typ etyp], _) ->
-    (start, len, ord, etyp)
+    (simplify_nexp start, simplify_nexp len, ord, etyp)
   | ("register", [Typ_arg_typ rtyp], _) -> vector_typ_args_of rtyp
-  | (_, _, l) -> raise (Reporting_basic.err_typ l "vector_typ_args_of called on non-vector type")
+  | (_, _, l) ->
+     raise (Reporting_basic.err_typ l
+       ("vector_typ_args_of called on non-vector type " ^ string_of_typ typ))
 
 let is_order_inc = function
   | Ord_aux (Ord_inc, _) -> true
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 7580404d..e6823ee9 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -44,21 +44,83 @@
 
 open Ast
 
+val mk_id : string -> id
+val mk_kid : string -> kid
+val mk_ord : order_aux -> order
 val mk_nc : n_constraint_aux -> n_constraint
 val mk_nexp : nexp_aux -> nexp
 val mk_exp : unit exp_aux -> unit exp
 val mk_pat : unit pat_aux -> unit pat
+val mk_lexp : unit lexp_aux -> unit lexp
 val mk_lit : lit_aux -> lit
 val mk_lit_exp : lit_aux -> unit exp
 val mk_funcl : id -> unit pat -> unit exp -> unit funcl
 val mk_fundef : (unit funcl) list -> unit def
 val mk_val_spec : val_spec_aux -> unit def
+val mk_typschm : typquant -> typ -> typschm
+val mk_fexp : id -> unit exp -> unit fexp
+val mk_fexps : (unit fexp) list -> unit fexps
+val mk_letbind : unit pat -> unit exp -> unit letbind
 
 val unaux_exp : 'a exp -> 'a exp_aux
 
 val inc_ord : order
 val dec_ord : order
 
+(* Utilites for working with kinded_ids *)
+val kopt_kid : kinded_id -> kid
+val is_nat_kopt : kinded_id -> bool
+val is_order_kopt : kinded_id -> bool
+val is_typ_kopt : kinded_id -> bool
+
+(* Some handy utility functions for constructing types. *)
+val mk_typ : typ_aux -> typ
+val mk_typ_arg : typ_arg_aux -> typ_arg
+val mk_id_typ : id -> typ
+
+(* Sail builtin types. *)
+val int_typ : typ
+val nat_typ : typ
+val atom_typ : nexp -> typ
+val range_typ : nexp -> nexp -> typ
+val bit_typ : typ
+val bool_typ : typ
+val app_typ : id -> typ_arg list -> typ
+val unit_typ : typ
+val string_typ : typ
+val real_typ : typ
+val vector_typ : nexp -> nexp -> order -> typ -> typ
+val list_typ : typ -> typ
+val exc_typ : typ
+
+val no_effect : effect
+val mk_effect : base_effect_aux list -> effect
+
+val nexp_simp : nexp -> nexp
+
+(* Utilities for building n-expressions *)
+val nconstant : int -> nexp
+val nminus : nexp -> nexp -> nexp
+val nsum : nexp -> nexp -> nexp
+val ntimes : nexp -> nexp -> nexp
+val npow2 : nexp -> nexp
+val nvar : kid -> nexp
+val nid : id -> nexp (* NOTE: Nexp_id's don't do anything currently *)
+
+(* Numeric constraint builders *)
+val nc_eq : nexp -> nexp -> n_constraint
+val nc_neq : nexp -> nexp -> n_constraint
+val nc_lteq : nexp -> nexp -> n_constraint
+val nc_gteq : nexp -> nexp -> n_constraint
+val nc_lt : nexp -> nexp -> n_constraint
+val nc_gt : nexp -> nexp -> n_constraint
+val nc_and : n_constraint -> n_constraint -> n_constraint
+val nc_or : n_constraint -> n_constraint -> n_constraint
+val nc_true : n_constraint
+val nc_false : n_constraint
+
+val quant_items : typquant -> quant_item list
+
 (* Functions to map over the annotations in sub-expressions *)
 val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
 val map_pat_annot : ('a annot -> 'b annot) -> 'a pat -> 'b pat
@@ -84,6 +146,7 @@ val string_of_order : order -> string
 val string_of_nexp : nexp -> string
 val string_of_typ : typ -> string
 val string_of_typ_arg : typ_arg -> string
+val string_of_annot : ('a * typ * effect) option -> string
 val string_of_n_constraint : n_constraint -> string
 val string_of_quant_item : quant_item -> string
 val string_of_typquant : typquant -> string
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 3919d540..a760fb42 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -34,6 +34,8 @@ let adjust_start_index (start, v) = set_vector_start (start, v)
 
 let cast_vec_bool v = bitU_to_bool (extract_only_element v)
 let cast_bit_vec (start, len, b) = Vector (repeat [b] len) start false
+let cast_boolvec_bitvec (Vector bs start inc) =
+  Vector (List.map bool_to_bitU bs) start inc
 
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
@@ -203,6 +205,7 @@ let modulo (l,r) = hardware_mod l r
 let quot = hardware_quot
 let power (l,r) = integerPow l r
 
+let add_int = add
 let sub_int = sub
 let mult_int = mult
 
@@ -450,6 +453,9 @@ let rec repeat xs n =
 let duplicate (bit, length) =
   Vector (repeat [bit] length) (length - 1) false
 
+let replicate_bits (v, count) =
+  Vector (repeat (get_elems v) count) ((length v * count) - 1) false
+
 let compare_op op (l,r) = (op l r)
 
 let lt = compare_op (<)
@@ -529,3 +535,17 @@ let make_bitvector_undef length =
 let mask' (start, n, Vector bits _ dir) =
   let current_size = List.length bits in
   Vector (drop (current_size - (natFromInteger n)) bits) start dir
+
+
+(* Register operations *)
+
+let update_reg_range i j reg_val new_val = update reg_val i j new_val
+let update_reg_bit i reg_val bit = update_pos reg_val i bit
+let update_reg_field_range regfield i j reg_val new_val =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = update current_field_value i j new_val in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_bit regfield i reg_val bit =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = update_pos current_field_value i bit in
+  regfield.set_field reg_val new_field_value
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 8f44b2b5..f10ed9f7 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -96,6 +96,8 @@ let adjust_start_index (start, v) = set_bitvector_start (start, v)
 
 let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
 let cast_bit_vec (start, len, b) = vec_to_bvec (Vector [b] start false)
+let cast_boolvec_bitvec (Vector bs start inc) =
+  vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc)
 
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
@@ -243,6 +245,7 @@ let modulo (l,r) = hardware_mod l r
 let quot = hardware_quot
 let power (l,r) = integerPow l r
 
+let add_int = add
 let sub_int = sub
 let mult_int = mult
 
@@ -572,3 +575,16 @@ let make_bitvector_undef length =
 (* TODO *)
 val mask : forall 'a 'b. Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b
 let mask (start, _, Bitvector w _ dir) = (Bitvector (zeroExtend w) start dir)
+
+(* Register operations *)
+
+let update_reg_range i j reg_val new_val = bvupdate reg_val i j new_val
+let update_reg_bit i reg_val bit = bvupdate_pos reg_val i bit
+let update_reg_field_range regfield i j reg_val new_val =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = bvupdate current_field_value i j new_val in
+  regfield.set_field reg_val new_field_value
+let write_reg_field_bit regfield i reg_val bit =
+  let current_field_value = regfield.get_field reg_val in
+  let new_field_value = bvupdate_pos current_field_value i bit in
+  regfield.set_field reg_val new_field_value
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index b7b87b97..4d3ddbce 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -11,6 +11,8 @@ type nn = natural
 val pow : integer -> integer -> integer
 let pow m n = m ** (natFromInteger n)
 
+let pow2 n = pow 2 n
+
 let bool_or (l, r) = (l || r)
 let bool_and (l, r) = (l && r)
 let bool_xor (l, r) = xor l r
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 879b092f..0ea65551 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,7 +1,6 @@
 open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
-open import Sail_operators_mwords
 
 (* 'a is result type *)
 
@@ -51,7 +50,7 @@ let inline (>>) m n = m >>= fun _ -> n
 val exit : forall 'regs 'e 'a. 'e -> M 'regs 'a
 let exit _ s = [(Right (), s)]
 
-val early_return : forall 'regs 'r. 'r -> MR 'regs unit 'r
+val early_return : forall 'regs 'a 'r. 'r -> MR 'regs 'a 'r
 let early_return r s = [(Right (Just r), s)]
 
 val catch_early_return : forall 'regs 'a. MR 'regs 'a 'a -> M 'regs 'a
@@ -76,12 +75,11 @@ let set_reg state reg v =
   <| state with regstate = reg.write_to state.regstate v |>
 
 
-val read_mem : forall 'regs 'a 'b. Size 'b => bool -> read_kind -> bitvector 'a -> integer -> M 'regs (bitvector 'b)
+val read_mem : forall 'regs 'a 'b. Size 'b => bool -> read_kind -> integer -> integer -> M 'regs (vector bitU)
 let read_mem dir read_kind addr sz state =
-  let addr = unsigned addr in
   let addrs = range addr (addr+sz-1) in
   let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in
-  let value = vec_to_bvec (Sail_values.internal_mem_value dir memory_value) in
+  let value = Sail_values.internal_mem_value dir memory_value in
   let is_exclusive = match read_kind with
     | Sail_impl_base.Read_plain -> false
     | Sail_impl_base.Read_reserve -> true
@@ -98,9 +96,9 @@ let read_mem dir read_kind addr sz state =
 (* caps are aligned at 32 bytes *)
 let cap_alignment = (32 : integer)
 
-val read_tag : forall 'regs 'a. bool -> read_kind -> bitvector 'a -> M 'regs bitU
+val read_tag : forall 'regs 'a. bool -> read_kind -> integer -> M 'regs bitU
 let read_tag dir read_kind addr state =
-  let addr = (unsigned addr) / cap_alignment in
+  let addr = addr / cap_alignment in
   let tag = match (Map.lookup addr state.tagstate) with
     | Just t -> t
     | Nothing -> B0
@@ -125,18 +123,17 @@ let excl_result () state =
     (Left true,  <| state with last_exclusive_operation_was_load = false |>) in
   (Left false, state) :: if state.last_exclusive_operation_was_load then [success] else []
 
-val write_mem_ea : forall 'regs 'a. write_kind -> bitvector 'a -> integer -> M 'regs unit
+val write_mem_ea : forall 'regs 'a. write_kind -> integer -> integer -> M 'regs unit
 let write_mem_ea write_kind addr sz state = 
-  let addr = unsigned addr in
   [(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)]
 
-val write_mem_val : forall 'regs 'b. bitvector 'b -> M 'regs bool
+val write_mem_val : forall 'regs 'b. vector bitU -> M 'regs bool
 let write_mem_val v state =
   let (write_kind,addr,sz) = match state.write_ea with
     | Nothing -> failwith "write ea has not been announced yet"
     | Just write_ea -> write_ea end in
   let addrs = range addr (addr+sz-1) in
-  let v = external_mem_value (bvec_to_vec v) in
+  let v = external_mem_value v in
   let addresses_with_value = List.zip addrs v in
   let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
                             state.memstate addresses_with_value in
@@ -178,28 +175,6 @@ let update_reg reg f v state =
   let current_value = get_reg state reg in
   let new_value = f current_value v in
   [(Left (), set_reg state reg new_value)]
-let write_reg_range reg i j v state =
-  let current_value = get_reg state reg in
-  let new_value = bvupdate current_value i j v in
-  [(Left (), set_reg state reg new_value)]
-let write_reg_bit reg i bit state =
-  let current_value = get_reg state reg in
-  let new_value = bvupdate_pos current_value i bit in
-  [(Left (), set_reg state reg new_value)]
-let write_reg_field reg regfield =
-  update_reg reg regfield.set_field
-let write_reg_field_range reg regfield i j =
-  let upd regval v =
-    let current_field_value = regfield.get_field regval in
-    let new_field_value = bvupdate current_field_value i j v in
-    regfield.set_field regval new_field_value in
-  update_reg reg upd
-let write_reg_field_bit reg regfield i =
-  let upd regval v =
-    let current_field_value = regfield.get_field regval in
-    let new_field_value = bvupdate_pos current_field_value i v in
-    regfield.set_field regval new_field_value in
-  update_reg reg upd
 
 
 val barrier : forall 'regs. barrier_kind -> M 'regs unit
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 8e5fd35f..74faba25 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1012,6 +1012,8 @@ let typschm_of_string order str =
   let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
   typschm
 
+let val_spec_of_string order id str = mk_val_spec (VS_extern_no_rename (typschm_of_string order str, id))
+
 let val_spec_ids (Defs defs) =
   let val_spec_id (VS_aux (vs_aux, _)) =
     match vs_aux with
@@ -1027,14 +1029,56 @@ let val_spec_ids (Defs defs) =
   in
   IdSet.of_list (vs_ids defs)
 
+let quant_item_param = function
+  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))]
+  | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [prepend_id "typ_" (id_of_kid (kopt_kid kopt))]
+  | _ -> []
+let quant_item_typ = function
+  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [atom_typ (nvar (kopt_kid kopt))]
+  | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ (Typ_var (kopt_kid kopt))]
+  | _ -> []
+let quant_item_arg = function
+  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [mk_typ_arg (Typ_arg_nexp (nvar (kopt_kid kopt)))]
+  | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var (kopt_kid kopt))))]
+  | _ -> []
+let undefined_typschm id typq =
+  let qis = quant_items typq in
+  if qis = [] then
+    mk_typschm typq (mk_typ (Typ_fn (unit_typ, mk_typ (Typ_id id), mk_effect [BE_undef])))
+  else
+    let arg_typ = mk_typ (Typ_tup (List.concat (List.map quant_item_typ qis))) in
+    let ret_typ = app_typ id (List.concat (List.map quant_item_arg qis)) in
+    mk_typschm typq (mk_typ (Typ_fn (arg_typ, ret_typ, mk_effect [BE_undef])))
+
 let generate_undefineds vs_ids (Defs defs) =
+  let gen_vs id str =
+    if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str]
+  in
+  let undefined_builtins = List.concat
+    [gen_vs (mk_id "internal_pick") "forall 'a:Type. list('a) -> 'a effect {undef}";
+     gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}";
+     gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}";
+     gen_vs (mk_id "undefined_int") "unit -> int effect {undef}";
+     gen_vs (mk_id "undefined_string") "unit -> string effect {undef}";
+     gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
+     (* FIXME: How to handle inc/dec order correctly? *)
+     gen_vs (mk_id "undefined_vector") "forall 'n 'm 'a:Type. (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}";
+     gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
+  in
   let undefined_td = function
     | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in
        [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             (mk_pat (P_lit (mk_lit L_unit)))
-                            (mk_exp (E_lit (mk_lit L_undef)))]]
+                            (mk_exp (E_app (mk_id "internal_pick",
+                                            [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
+    | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
+       let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
+       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id));
+        mk_fundef [mk_funcl (prepend_id "undefined_" id)
+                            pat
+                            (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]]
     | _ -> []
   in
   let rec undefined_defs = function
@@ -1044,9 +1088,28 @@ let generate_undefineds vs_ids (Defs defs) =
        def :: undefined_defs defs
     | [] -> []
   in
-  Defs (undefined_defs defs)
+  Defs (undefined_builtins @ undefined_defs defs)
+
+let rec get_registers = function
+  | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) :: defs -> (typ, id) :: get_registers defs
+  | def :: defs -> get_registers defs
+  | [] -> []
+
+let generate_initialize_registers vs_ids (Defs defs) =
+  let regs = get_registers defs in
+  let initialize_registers =
+    if IdSet.mem (mk_id "initialize_registers") vs_ids || regs = [] then []
+    else
+      [val_spec_of_string dec_ord (mk_id "initialize_registers") "unit -> unit effect {undef, wreg}";
+       mk_fundef [mk_funcl (mk_id "initialize_registers")
+                           (mk_pat (P_lit (mk_lit L_unit)))
+                           (mk_exp (E_block (List.map (fun (typ, id) -> mk_exp (E_assign (mk_lexp (LEXP_cast (typ, id)), mk_lit_exp L_undef))) regs)))]]
+  in
+  Defs (defs @ initialize_registers)
+
 
 let process_ast order defs =
   let (ast, _, _) = to_ast Nameset.empty initial_kind_env order defs in
   let vs_ids = val_spec_ids ast in
-  generate_undefineds vs_ids ast
+  let ast = generate_undefineds vs_ids ast in
+  generate_initialize_registers vs_ids ast
diff --git a/src/initial_check.mli b/src/initial_check.mli
index ed4eb0bf..86b5ca3b 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -41,6 +41,8 @@
 (**************************************************************************)
 
 open Ast
+open Ast_util
 
 val process_ast : order -> Parse_ast.defs -> unit defs
 
+val val_spec_ids : 'a defs -> IdSet.t
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
new file mode 100644
index 00000000..8b88a07e
--- /dev/null
+++ b/src/ocaml_backend.ml
@@ -0,0 +1,347 @@
+open Ast
+open Ast_util
+open PPrint
+open Type_check
+
+type ctx =
+  { register_inits : tannot exp list;
+    externs : id Bindings.t
+  }
+
+let empty_ctx =
+  { register_inits = [];
+    externs = Bindings.empty
+  }
+
+let zchar c =
+  let zc c = "z" ^ String.make 1 c in
+  if Char.code c <= 41 then zc (Char.chr (Char.code c + 16))
+  else if Char.code c <= 47 then zc (Char.chr (Char.code c + 23))
+  else if Char.code c <= 57 then String.make 1 c
+  else if Char.code c <= 64 then zc (Char.chr (Char.code c + 13))
+  else if Char.code c <= 90 then String.make 1 c
+  else if Char.code c <= 94 then zc (Char.chr (Char.code c - 13))
+  else if Char.code c <= 95 then "_"
+  else if Char.code c <= 96 then zc (Char.chr (Char.code c - 13))
+  else if Char.code c <= 121 then String.make 1 c
+  else if Char.code c <= 122 then "zz"
+  else if Char.code c <= 126 then zc (Char.chr (Char.code c - 39))
+  else raise (Invalid_argument "zchar")
+
+let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (Util.string_to_list str))
+
+let zencode_upper_string str = "Z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (Util.string_to_list str))
+
+let zencode ctx id =
+  try string (string_of_id (Bindings.find id ctx.externs)) with
+  | Not_found -> string (zencode_string (string_of_id id))
+
+let zencode_upper ctx id =
+  try string (string_of_id (Bindings.find id ctx.externs)) with
+  | Not_found -> string (zencode_upper_string (string_of_id id))
+
+let zencode_kid kid = string ("'" ^ zencode_string (string_of_id (id_of_kid kid)))
+
+let ocaml_typ_id ctx = function
+  | id when Id.compare id (mk_id "string") = 0 -> string "string"
+  | id when Id.compare id (mk_id "list") = 0 -> string "list"
+  | id when Id.compare id (mk_id "bit") = 0 -> string "bit"
+  | id when Id.compare id (mk_id "int") = 0 -> string "big_int"
+  | id when Id.compare id (mk_id "bool") = 0 -> string "bool"
+  | id -> zencode ctx id
+
+let rec ocaml_typ ctx (Typ_aux (typ_aux, _)) =
+  match typ_aux with
+  | Typ_id id -> ocaml_typ_id ctx id
+  | Typ_app (id, []) -> ocaml_typ_id ctx id
+  | Typ_app (id, typs) -> parens (separate_map (string " * ") (ocaml_typ_arg ctx) typs) ^^ space ^^ ocaml_typ_id ctx id
+  | Typ_tup typs -> parens (separate_map (string " * ") (ocaml_typ ctx) typs)
+  | Typ_fn (typ1, typ2, _) -> separate space [ocaml_typ ctx typ1; string "->"; ocaml_typ ctx typ2]
+  | Typ_var kid -> zencode_kid kid
+  | Typ_exist _ | Typ_wild -> assert false
+and ocaml_typ_arg ctx (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
+  match typ_arg_aux with
+  | Typ_arg_typ typ -> ocaml_typ ctx typ
+  | _ -> failwith ("OCaml: unexpected type argument " ^ string_of_typ_arg typ_arg)
+
+let ocaml_typquant typq =
+  let ocaml_qi = function
+    | QI_aux (QI_id kopt, _) -> zencode_kid (kopt_kid kopt)
+    | QI_aux (QI_const _, _) -> failwith "Ocaml type quantifiers should no longer contain constraints"
+  in
+  match quant_items typq with
+  | [] -> empty
+  | [qi] -> ocaml_qi qi
+  | qis -> parens (separate_map (string " * ") ocaml_qi qis)
+
+let ocaml_lit (L_aux (lit_aux, _)) =
+  match lit_aux with
+  | L_unit -> string "()"
+  | L_zero -> string "B0"
+  | L_one -> string "B1"
+  | L_true -> string "true"
+  | L_false -> string "false"
+  | L_num n -> parens (string "big_int_of_int" ^^ space ^^ string (string_of_int n))
+  | L_undef -> failwith "undefined should have been re-written prior to ocaml backend"
+  | L_string str -> dquotes (string (String.escaped str))
+  | _ -> string "LIT"
+
+let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
+  match pat_aux with
+  | P_id id -> zencode ctx id
+  | P_lit lit -> ocaml_lit lit
+  | P_typ (_, pat) -> ocaml_pat ctx pat
+  | P_tup pats -> parens (separate_map (comma ^^ space) (ocaml_pat ctx) pats)
+  | P_list pats -> brackets (separate_map (semi ^^ space) (ocaml_pat ctx) pats)
+  | P_wild -> string "_"
+  | P_as (pat, id) -> separate space [ocaml_pat ctx pat; string "as"; zencode ctx id]
+  | _ -> string ("PAT<" ^ string_of_pat pat ^ ">")
+
+let begin_end doc = group (string "begin" ^^ nest 2 (break 1 ^^ doc) ^/^ string "end")
+
+let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
+  match exp_aux with
+  | E_app (f, [x]) -> zencode ctx f ^^ space ^^ ocaml_atomic_exp ctx x
+  | E_app (f, xs) -> zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+  | E_return exp -> separate space [string "r.return"; ocaml_atomic_exp ctx exp]
+  | E_assert (exp, _) -> separate space [string "assert"; ocaml_atomic_exp ctx exp]
+  | E_cast (_, exp) -> ocaml_exp ctx exp
+  | E_block [exp] -> ocaml_exp ctx exp
+  | E_block [] -> string "()"
+  | E_block exps -> begin_end (ocaml_block ctx exps)
+  | E_field (exp, id) -> ocaml_atomic_exp ctx exp ^^ dot ^^ zencode ctx id
+  | E_exit exp -> string "failwith" ^^ space ^^ dquotes (string (String.escaped (string_of_exp exp)))
+  | E_case (exp, pexps) ->
+     begin_end (separate space [string "match"; ocaml_atomic_exp ctx exp; string "with"]
+                ^/^ ocaml_pexps ctx pexps)
+  | E_assign (lexp, exp) -> separate space [ocaml_lexp ctx lexp; string ":="; ocaml_exp ctx exp]
+  | E_if (c, t, e) -> separate space [string "if"; ocaml_atomic_exp ctx c;
+                                      string "then"; ocaml_atomic_exp ctx t;
+                                      string "else"; ocaml_atomic_exp ctx e]
+  | E_record (FES_aux (FES_Fexps (fexps, _), _)) ->
+     enclose lbrace rbrace (group (separate_map (semi ^^ break 1) (ocaml_fexp ctx) fexps))
+  | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) ->
+     enclose lbrace rbrace (separate space [ocaml_atomic_exp ctx exp;
+                                            string "with";
+                                            separate_map (semi ^^ space) (ocaml_fexp ctx) fexps])
+  | E_let (lb, exp) ->
+     separate space [string "let"; ocaml_letbind ctx lb; string "in"]
+     ^/^ ocaml_exp ctx exp
+  | E_internal_let (lexp, exp1, exp2) ->
+     separate space [string "let"; ocaml_atomic_lexp ctx lexp;
+                     equals; string "ref"; ocaml_atomic_exp ctx exp1; string "in"]
+     ^/^ ocaml_exp ctx exp2
+  | E_lit _ | E_list _ | E_id _ | E_tuple _ -> ocaml_atomic_exp ctx exp
+  | _ -> string ("EXP(" ^ string_of_exp exp ^ ")")
+and ocaml_letbind ctx (LB_aux (lb_aux, _)) =
+  match lb_aux with
+  | LB_val_implicit (pat, exp) -> separate space [ocaml_pat ctx pat; equals; ocaml_atomic_exp ctx exp]
+  | _ -> failwith "Ocaml: Explicit letbind found"
+and ocaml_pexps ctx = function
+  | [pexp] -> ocaml_pexp ctx pexp
+  | pexp :: pexps -> ocaml_pexp ctx pexp ^/^ ocaml_pexps ctx pexps
+  | [] -> empty
+and ocaml_pexp ctx = function
+  | Pat_aux (Pat_exp (pat, exp), _) ->
+     separate space [bar; ocaml_pat ctx pat; string "->"]
+     ^//^ group (ocaml_exp ctx exp)
+  | Pat_aux (Pat_when (pat, wh, exp), _) ->
+     separate space [bar; ocaml_pat ctx pat; string "when"; ocaml_atomic_exp ctx exp; string "->"]
+     ^//^ group (ocaml_exp ctx exp)
+and ocaml_block ctx = function
+  | [exp] -> ocaml_exp ctx exp
+  | exp :: exps -> ocaml_exp ctx exp ^^ semi ^/^ ocaml_block ctx exps
+  | _ -> assert false
+and ocaml_fexp ctx (FE_aux (FE_Fexp (id, exp), _)) =
+  separate space [zencode ctx id; equals; ocaml_exp ctx exp]
+and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
+  match exp_aux with
+  | E_lit lit -> ocaml_lit lit
+  | E_id id ->
+     begin
+       match Env.lookup_id id (env_of exp) with
+       | Local (Immutable, _) | Unbound -> zencode ctx id
+       | Enum _ -> zencode_upper ctx id
+       | Register _ | Local (Mutable, _) -> bang ^^ zencode ctx id
+       | _ -> failwith ("Union constructor: " ^ zencode_string (string_of_id id))
+     end
+  | E_list exps -> enclose lbracket rbracket (separate_map (semi ^^ space) (ocaml_exp ctx) exps)
+  | E_tuple exps -> parens (separate_map (comma ^^ space) (ocaml_exp ctx) exps)
+  | _ -> parens (ocaml_exp ctx exp)
+and ocaml_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) =
+  match lexp_aux with
+  | LEXP_cast _ | LEXP_id _ -> ocaml_atomic_lexp ctx lexp
+  | _ -> string ("LEXP<" ^ string_of_lexp lexp ^ ">")
+and ocaml_atomic_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) =
+  match lexp_aux with
+  | LEXP_cast (_, id) -> zencode ctx id
+  | LEXP_id id -> zencode ctx id
+  | _ -> parens (ocaml_lexp ctx lexp)
+
+let rec get_initialize_registers = function
+  | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _, E_aux (E_block inits, _)), _)]), _)) :: defs
+       when Id.compare id (mk_id "initialize_registers") = 0 ->
+     inits
+  | _ :: defs -> get_initialize_registers defs
+  | [] -> []
+
+let initial_value_for id inits =
+  let find_reg = function
+    | E_aux (E_assign (LEXP_aux (LEXP_cast (_, reg_id), _), init), _) when Id.compare id reg_id = 0 -> Some init
+    | _ -> None
+  in
+  match Util.option_first find_reg inits with
+  | Some init -> init
+  | None -> failwith ("No assignment to register ^ " ^ string_of_id id ^ " in initialize_registers")
+
+let ocaml_dec_spec ctx (DEC_aux (reg, _)) =
+  match reg with
+  | DEC_reg (typ, id) ->
+     separate space [string "let"; zencode ctx id; colon;
+                     parens (ocaml_typ ctx typ); string "ref"; equals;
+                     string "ref"; parens (ocaml_exp ctx (initial_value_for id ctx.register_inits))]
+  | _ -> failwith "Unsupported register declaration"
+
+let funcls_id = function
+  | [] -> failwith "Ocaml: empty function"
+  | FCL_aux (FCL_Funcl (id, pat, exp),_) :: _ -> id
+
+let ocaml_funcl_match ctx (FCL_aux (FCL_Funcl (id, pat, exp), _)) =
+  separate space [bar; ocaml_pat ctx pat; string "->"]
+  ^//^ group (string "with_return (fun r ->" ^//^ ocaml_exp ctx exp ^^ rparen)
+
+let rec ocaml_funcl_matches ctx = function
+  | [] -> failwith "Ocaml: empty function"
+  | [clause] -> ocaml_funcl_match ctx clause
+  | (clause :: clauses) -> ocaml_funcl_match ctx clause ^/^ ocaml_funcl_matches ctx clauses
+
+let ocaml_funcls ctx = function
+  | [] -> failwith "Ocaml: empty function"
+  | [FCL_aux (FCL_Funcl (id, pat, exp),_)] ->
+     separate space [string "let"; zencode ctx id; ocaml_pat ctx pat; equals; string "with_return (fun r ->"]
+     ^//^ ocaml_exp ctx exp
+     ^^ rparen
+  | funcls ->
+     let id = funcls_id funcls in
+     separate space [string "let"; zencode ctx id; equals; string "function"]
+     ^//^ ocaml_funcl_matches ctx funcls
+
+let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) =
+  ocaml_funcls ctx funcls
+
+let rec ocaml_fields ctx =
+  let ocaml_field typ id =
+    separate space [zencode ctx id; colon; ocaml_typ ctx typ]
+  in
+  function
+  | [(typ, id)] -> ocaml_field typ id
+  | (typ, id) :: fields -> ocaml_field typ id ^^ semi ^/^ ocaml_fields ctx fields
+  | [] -> empty
+
+let rec ocaml_cases ctx =
+  let ocaml_case = function
+    | Tu_aux (Tu_id id, _) -> separate space [bar; zencode ctx id]
+    | Tu_aux (Tu_ty_id (typ, id), _) -> separate space [bar; zencode ctx id; string "of"; ocaml_typ ctx typ]
+  in
+  function
+  | [tu] -> ocaml_case tu
+  | tu :: tus -> ocaml_case tu ^/^ ocaml_cases ctx tus
+  | [] -> empty
+
+let rec ocaml_enum ctx = function
+  | [id] -> zencode_upper ctx id
+  | id :: ids -> zencode_upper ctx id ^/^ (bar ^^ space ^^ ocaml_enum ctx ids)
+  | [] -> empty
+
+let ocaml_typedef ctx (TD_aux (td_aux, _)) =
+  match td_aux with
+  | TD_record (id, _, typq, fields, _) ->
+     (separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals; lbrace]
+      ^//^ ocaml_fields ctx fields)
+     ^/^ rbrace
+  | TD_variant (id, _, typq, cases, _) ->
+     separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals]
+     ^//^ ocaml_cases ctx cases
+  | TD_enum (id, _, ids, _) ->
+     separate space [string "type"; zencode ctx id; equals]
+     ^//^ (bar ^^ space ^^ ocaml_enum ctx ids)
+  | TD_abbrev (id, _, TypSchm_aux (TypSchm_ts (typq, typ), _)) ->
+     separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals; ocaml_typ ctx typ]
+  | _ -> failwith "Unsupported typedef"
+
+let get_externs (Defs defs) =
+  let extern_id (VS_aux (vs_aux, _)) =
+    match vs_aux with
+    | VS_val_spec (typschm, id) -> []
+    | VS_extern_no_rename (typschm, id) -> [(id, id)]
+    | VS_extern_spec (typschm, id, name) -> [(id, mk_id name)]
+    | VS_cast_spec (typschm, id) -> []
+  in
+  let rec extern_ids = function
+    | DEF_spec vs :: defs -> extern_id vs :: extern_ids defs
+    | def :: defs -> extern_ids defs
+    | [] -> []
+  in
+  List.fold_left (fun exts (id, name) -> Bindings.add id name exts) Bindings.empty (List.concat (extern_ids defs))
+
+let ocaml_def_end = string ";;" ^^ twice hardline
+
+let ocaml_def ctx def = match def with
+  | DEF_reg_dec ds -> group (ocaml_dec_spec ctx ds) ^^ ocaml_def_end
+  | DEF_fundef fd -> group (ocaml_fundef ctx fd) ^^ ocaml_def_end
+  | DEF_type td -> group (ocaml_typedef ctx td) ^^ ocaml_def_end
+  | _ -> empty
+
+let ocaml_defs (Defs defs) =
+  let ctx = { register_inits = get_initialize_registers defs;
+              externs = get_externs (Defs defs)
+            }
+  in
+  let empty_reg_init =
+    if ctx.register_inits = []
+    then
+      separate space [string "let"; string "initialize_registers"; string "()"; equals; string "()"]
+      ^^ ocaml_def_end
+    else empty
+  in
+  (string "open Sail_lib;;" ^^ hardline)
+  ^^ (string "open Big_int" ^^ ocaml_def_end)
+  ^^ concat (List.map (ocaml_def ctx) defs)
+  ^^ empty_reg_init
+
+let ocaml_main spec =
+  concat [separate space [string "open"; string (String.capitalize spec)] ^^ ocaml_def_end;
+          separate space [string "let"; string "()"; equals]
+          ^//^ (string "Random.self_init ();"
+                ^/^ string "initialize_registers ();"
+                ^/^ string "zmain ()")
+         ]
+
+let ocaml_pp_defs f defs =
+  ToChannel.pretty 1. 80 f (ocaml_defs defs)
+
+let ocaml_compile spec defs =
+  let sail_lib_dir =
+    try Sys.getenv "SAILLIBDIR" with
+    | Not_found -> failwith "Environment variable SAILLIBDIR needs to be set"
+  in
+  if Sys.file_exists "_sbuild" then () else Unix.mkdir "_sbuild" 0o775;
+  let cwd = Unix.getcwd () in
+  Unix.chdir "_sbuild";
+  let _ = Unix.system ("cp " ^ sail_lib_dir ^ "/sail_lib.ml .") in
+  let out_chan = open_out (spec ^ ".ml") in
+  ocaml_pp_defs out_chan defs;
+  close_out out_chan;
+  if IdSet.mem (mk_id "main") (Initial_check.val_spec_ids defs)
+  then
+    let out_chan = open_out "main.ml" in
+    ToChannel.pretty 1. 80 out_chan (ocaml_main spec);
+    close_out out_chan;
+    let _ = Unix.system "ocamlbuild -lib nums main.native" in
+    let _ = Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec) in
+    ()
+  else
+    let _ = Unix.system ("ocamlbuild -lib nums " ^ spec ^ ".cmo") in
+    ();
+  Unix.chdir cwd
+
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 3951ab51..b259611d 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -288,6 +288,7 @@ exp_aux =  (* Expression *)
  | E_try of exp * pexp list
  | E_return of exp
  | E_assert of exp * exp
+ | E_internal_let of exp * exp * exp
 
 and exp = 
    E_aux of exp_aux * l
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 7671c26b..5e0d39a0 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -58,7 +58,11 @@ let langlebar = string "<|"
 let ranglebar = string "|>"
 let anglebars = enclose langlebar ranglebar
 
-let fix_id name = match name with
+let is_number_char c =
+  c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' ||
+  c = '6' || c = '7' || c = '8' || c = '9'
+
+let fix_id remove_tick name = match name with
   | "assert"
   | "lsl"
   | "lsr"
@@ -76,22 +80,17 @@ let fix_id name = match name with
   | "EQ"
   | "integer"
     -> name ^ "'"
-  | _ -> name
-
-let is_number char =
-  char = '0' || char = '1' || char = '2' || char = '3' || char = '4' || char = '5' ||
-  char = '6' || char = '7' || char = '8' || char = '9'
+  | _ ->
+     if name.[0] = '\'' then
+       let var = String.sub name 1 (String.length name - 1) in
+       if remove_tick then var else (var ^ "'")
+     else if is_number_char(name.[0]) then
+       ("v" ^ name ^ "'")
+     else name
 
 let doc_id_lem (Id_aux(i,_)) =
   match i with
-  | Id i ->
-     (* this not the right place to do this, just a workaround *)
-     if i.[0] = '\'' then
-       string ((String.sub i 1 (String.length i - 1)) ^ "'")
-     else if is_number(i.[0]) then
-       string ("v" ^ i ^ "'")
-     else
-       string (fix_id i)
+  | Id i -> string (fix_id false i)
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
@@ -102,7 +101,7 @@ let doc_id_lem_type (Id_aux(i,_)) =
   | Id("int") -> string "ii"
   | Id("nat") -> string "ii"
   | Id("option") -> string "maybe"
-  | Id i -> string (fix_id i)
+  | Id i -> string (fix_id false i)
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
@@ -115,12 +114,14 @@ let doc_id_lem_ctor (Id_aux(i,_)) =
   | Id("nat") -> string "integer"
   | Id("Some") -> string "Just"
   | Id("None") -> string "Nothing"
-  | Id i -> string (fix_id (String.capitalize i))
+  | Id i -> string (fix_id false (String.capitalize i))
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
      separate space [colon; string (String.capitalize x); empty]
 
+let doc_var_lem kid = string (fix_id true (string_of_kid kid))
+
 let effectful_set =
   List.exists
     (fun (BE_aux (eff,_)) ->
@@ -230,6 +231,7 @@ let rec contains_t_pp_var (Typ_aux (t,a) as typ) = match t with
   | Typ_wild -> true
   | Typ_id _ -> false
   | Typ_var _ -> true
+  | Typ_exist _ -> true
   | Typ_fn (t1,t2,_) -> contains_t_pp_var t1 || contains_t_pp_var t2
   | Typ_tup ts -> List.exists contains_t_pp_var ts
   | Typ_app (c,targs) ->
@@ -321,6 +323,7 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) =
      begin match id with
      | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
      | _ -> doc_id_lem id end
+  | P_var kid -> doc_var_lem kid
   | P_as(p,id) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_id_lem id])
   | P_typ(typ,p) ->
     let doc_p = doc_pat_lem sequential mwords true p in
@@ -391,15 +394,16 @@ let doc_exp_lem, doc_let_lem =
                    underscore ^^
                    doc_id_lem id in
                  liftR ((prefix 2 1)
-                   (string "write_reg_field_range")
+                   (string "update_reg")
                    (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space^^
-                             field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
+                      parens (string "update_reg_field_range" ^/^ field_ref ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
             | _ ->
                liftR ((prefix 2 1)
-                 (string "write_reg_range")
-                 (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e)))
+                 (string "update_reg")
+                 (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+                   parens (string "update_reg_range" ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
            )
-        | LEXP_vector (le,e2) when is_bit_typ t ->
+        | LEXP_vector (le,e2) ->
            (match le with
             | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) ->
                if is_bit_typ (typ_of_annot fannot) then
@@ -410,12 +414,14 @@ let doc_exp_lem, doc_let_lem =
                    underscore ^^
                    doc_id_lem id in
                  liftR ((prefix 2 1)
-                   (string "write_reg_field_bit")
-                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ field_ref ^/^ expY e2 ^/^ expY e)))
+                   (string "update_reg")
+                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+                     parens (string "update_reg_field_bit" ^/^ field_ref ^/^ expY e2) ^/^ expY e)))
             | _ ->
                liftR ((prefix 2 1)
-                 (string "write_reg_bit")
-                 (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e))
+                 (string "update_reg")
+                 (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+                   parens (string "update_reg_bit" ^/^ expY e2) ^/^ expY e))
            )
         (* | LEXP_field (le,id) when is_bit_typ t ->
            liftR ((prefix 2 1)
@@ -425,9 +431,11 @@ let doc_exp_lem, doc_let_lem =
           let field_ref =
             doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^
             underscore ^^
-            doc_id_lem id in
+            doc_id_lem id ^^
+            dot ^^
+            string "set_field" in
            liftR ((prefix 2 1)
-             (string "write_reg_field")
+             (string "update_reg")
              (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
                 field_ref ^/^ expY e))
         (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info ->
@@ -692,7 +700,7 @@ let doc_exp_lem, doc_let_lem =
        let recordtyp = match annot with
          | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
            tid
-         | _ ->  raise (report l "cannot get record type") in
+         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        let epp = anglebars (space ^^ (align (separate_map
                                           (semi_sp ^^ break 1)
                                           (doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in
@@ -702,7 +710,7 @@ let doc_exp_lem, doc_let_lem =
        let recordtyp = match eannot with
          | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
            tid
-         | _ ->  raise (report l "cannot get record type") in
+         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps))
     | E_vector exps ->
        let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
@@ -801,21 +809,26 @@ let doc_exp_lem, doc_let_lem =
        if aexp_needed then parens (align bepp) else bepp
     | E_vector_update(v,e1,e2) ->
        let t = typ_of full_exp in
+       let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+       let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
        let call =
          if is_bitvector_typ t (*&& mwords*)
-         then "bitvector_update_pos"
-         else "update_pos" in
-       let epp = separate space [string call;expY v;expY e1;expY e2] in
+         then "bitvector_update_pos" ^ ord_suffix
+         else "update_pos" ^ ord_suffix in
+       let epp = string call ^^ space ^^ parens (separate comma_sp [expY v;expY e1;expY e2]) in
        if aexp_needed then parens (align epp) else epp
     | E_vector_update_subrange(v,e1,e2,e3) ->
        let t = typ_of full_exp in
+       let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+       let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
        let call =
          if is_bitvector_typ t (*&& mwords*)
-         then "bitvector_update"
-         else "update" in
-       let epp = align (string call ^//^
-                          group (group (expY v) ^/^ group (expY e1) ^/^ group (expY e2)) ^/^
-                            group (expY e3)) in
+         then "bitvector_update" ^ ord_suffix
+         else "update" ^ ord_suffix in
+       let epp =
+         align (string call ^//^
+           parens (separate comma_sp
+             [group (expY v); group (expY e1); group (expY e2); group (expY e3)])) in
        if aexp_needed then parens (align epp) else epp
     | E_list exps ->
        brackets (separate_map semi (expN) exps)
@@ -843,8 +856,10 @@ let doc_exp_lem, doc_let_lem =
        if aexp_needed then parens (align epp) else align epp
     | E_exit e -> liftR (separate space [string "exit"; expY e;])
     | E_assert (e1,e2) ->
-       let epp = separate space [string "assert'"; expY e1; expY e2] in
-       if aexp_needed then parens (align epp) else align epp
+       (* FIXME needs pretty-printing of E_constraint; ignore for now *)
+       string "()"
+       (* let epp = separate space [string "assert'"; expY e1; expY e2] in
+       if aexp_needed then parens (align epp) else align epp *)
     | E_app_infix (e1,id,e2) ->
        (* TODO: Should have been removed by the new type checker; check with Alasdair *)
        raise (Reporting_basic.err_unreachable l
@@ -999,6 +1014,7 @@ let doc_exp_lem, doc_let_lem =
                                  top_exp sequential mwords early_ret true e])
     | LEXP_id id -> doc_id_lem id
     | LEXP_cast (typ,id) -> doc_id_lem id
+    | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem sequential mwords early_ret) lexps)
     | _ ->
        raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Shouldn't happen"))
              (* expose doc_exp_lem and doc_let *)
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index adddcee6..5edf9d12 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -221,6 +221,8 @@ and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
   | NC_not_equal(n1,n2) -> "(NC_not_equal " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
   | NC_or(nc1,nc2) -> "(NC_or " ^ pp_format_nexp_constraint_lem nc1 ^ " " ^ pp_format_nexp_constraint_lem nc2 ^ ")"
   | NC_and(nc1,nc2) -> "(NC_and " ^ pp_format_nexp_constraint_lem nc1 ^ " " ^ pp_format_nexp_constraint_lem nc2 ^ ")"
+  | NC_true -> "NC_true"
+  | NC_false -> "NC_false"
   | NC_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^
     pp_format_var_lem id ^
       " [" ^
@@ -326,6 +328,7 @@ let rec pp_format_pat_lem (P_aux(p,(l,annot))) =
   | P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")"
   | P_wild -> "P_wild"
   | P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")"
+  | P_var(kid) -> "(P_var " ^ pp_format_var_lem kid ^ ")"
   | P_as(pat,id) -> "(P_as " ^ pp_format_pat_lem pat ^ " " ^ pp_format_id_lem id ^ ")"
   | P_typ(typ,pat) -> "(P_typ " ^ pp_format_typ_lem typ ^ " " ^ pp_format_pat_lem pat ^ ")"
   | P_app(id,pats) -> "(P_app " ^ pp_format_id_lem id ^ " [" ^
diff --git a/src/process_file.ml b/src/process_file.ml
index b91f6e70..22f25f6e 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -41,6 +41,8 @@
 (**************************************************************************)
 
 let opt_new_parser = ref false
+let opt_lem_sequential = ref false
+let opt_lem_mwords = ref false
 
 type out_type =
   | Lem_ast_out
@@ -139,31 +141,28 @@ let generated_line f =
 
 let output_lem filename libs defs =
   let generated_line = generated_line filename in
-  let types_module = (filename ^ "_embed_types") in
-  let types_module_seq = (filename ^ "_embed_types_sequential") in
-  let libs_seq = List.map (fun lib -> lib ^ "_sequential") libs in
+  let seq_suffix = if !opt_lem_sequential then "_sequential" else "" in
+  let types_module = (filename ^ "_embed_types" ^ seq_suffix) in
+  let monad_module = if !opt_lem_sequential then "State" else "Prompt" in
+  let operators_module = if !opt_lem_mwords then "Sail_operators_mwords" else "Sail_operators" in
+  let libs = List.map (fun lib -> lib ^ seq_suffix) libs in
+  let base_imports = [
+      "Pervasives_extra";
+      "Sail_impl_base";
+      "Sail_values";
+      operators_module;
+      monad_module
+    ] in
   let ((ot,_, _) as ext_ot) =
-    open_output_with_check_unformatted (filename ^ "_embed_types.lem") in
-  let ((ots,_, _) as ext_ots) =
-    open_output_with_check_unformatted (filename ^ "_embed_types_sequential.lem") in
+    open_output_with_check_unformatted (filename ^ "_embed_types" ^ seq_suffix ^ ".lem") in
   let ((o,_, _) as ext_o) =
-    open_output_with_check_unformatted (filename ^ "_embed.lem") in
-  let ((os,_, _) as ext_os) =
-    open_output_with_check_unformatted (filename ^ "_embed_sequential.lem") in
-  (Pretty_print.pp_defs_lem false false
-     (ot,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt"])
-     (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt";
-       String.capitalize types_module] @ libs)
-     defs generated_line);
-  (Pretty_print.pp_defs_lem true true
-     (ots,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State"])
-     (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State";
-       String.capitalize types_module_seq] @ libs_seq)
+    open_output_with_check_unformatted (filename ^ "_embed" ^ seq_suffix ^ ".lem") in
+  (Pretty_print.pp_defs_lem !opt_lem_sequential !opt_lem_mwords
+     (ot, base_imports)
+     (o, base_imports @ (String.capitalize types_module :: libs))
      defs generated_line);
   close_output_with_check ext_ot;
-  close_output_with_check ext_ots;
-  close_output_with_check ext_o;
-  close_output_with_check ext_os
+  close_output_with_check ext_o
 
 let output1 libpath out_arg filename defs  =
   let f' = Filename.basename (Filename.chop_extension filename) in
diff --git a/src/process_file.mli b/src/process_file.mli
index 5bcd9e03..c477d185 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -52,6 +52,8 @@ val load_file_no_check : Ast.order -> string -> unit Ast.defs
 val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t
 
 val opt_new_parser : bool ref
+val opt_lem_sequential : bool ref
+val opt_lem_mwords : bool ref
 val opt_just_check : bool ref
 val opt_ddump_tc_ast : bool ref
 val opt_ddump_rewrite_ast : ((string * int) option) ref
@@ -74,4 +76,3 @@ val output :
     files existed before. If it is set to [false] and an output file already exists,
     the output file is only updated, if its content really changes. *)
 val always_replace_files : bool ref
-
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 79519af6..2b096609 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1029,6 +1029,14 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
     | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_range", [split_nexp nexp]))
     | _ -> mk_exp (E_sizeof nexp)
   in
+  let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with
+    | Nexp_id id -> rewrite_nexp_ids env (Env.get_num_def id env)
+    | Nexp_times (nexp1, nexp2) -> Nexp_aux (Nexp_times (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
+    | Nexp_sum (nexp1, nexp2) -> Nexp_aux (Nexp_sum (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
+    | Nexp_minus (nexp1, nexp2) -> Nexp_aux (Nexp_minus (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
+    | Nexp_exp nexp -> Nexp_aux (Nexp_exp (rewrite_nexp_ids env nexp), l)
+    | Nexp_neg nexp -> Nexp_aux (Nexp_neg (rewrite_nexp_ids env nexp), l)
+    | _ -> nexp_aux in
   let rec rewrite_e_aux split_sizeof (E_aux (e_aux, (l, _)) as orig_exp) =
     let env = env_of orig_exp in
     match e_aux with
@@ -1036,17 +1044,21 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
        E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect)))
     | E_sizeof nexp ->
        begin
-         let locals = Env.get_locals env in
-         let exps = Bindings.bindings locals
-                    |> List.map (extract_typ_var l env nexp)
-                    |> List.map (fun opt -> match opt with Some x -> [x] | None -> [])
-                    |> List.concat
-         in
-         match exps with
-         | (exp :: _) -> exp
-         | [] when split_sizeof ->
-            fold_exp (rewrite_e_sizeof false) (check_exp env (split_nexp nexp) (typ_of orig_exp))
-         | [] -> orig_exp
+         match simplify_nexp (rewrite_nexp_ids (env_of orig_exp) nexp) with
+         | Nexp_aux (Nexp_constant c, _) ->
+            E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect)))
+         | _ ->
+            let locals = Env.get_locals env in
+            let exps = Bindings.bindings locals
+                       |> List.map (extract_typ_var l env nexp)
+                       |> List.map (fun opt -> match opt with Some x -> [x] | None -> [])
+                       |> List.concat
+            in
+            match exps with
+            | (exp :: _) -> exp
+            | [] when split_sizeof ->
+               fold_exp (rewrite_e_sizeof false) (check_exp env (split_nexp nexp) (typ_of orig_exp))
+            | [] -> orig_exp
        end
     | _ -> orig_exp
   and rewrite_e_sizeof split_sizeof =
@@ -1274,7 +1286,7 @@ let rewrite_sizeof (Defs defs) =
     let funcls = List.map rewrite_funcl_params funcls in
     (nvars, FD_aux (FD_function (rec_opt,tannot,eff,funcls),annot)) in
 
-  let rewrite_sizeof_fundef (params_map, defs) = function
+  let rewrite_sizeof_def (params_map, defs) = function
     | DEF_fundef fd as def ->
        let (nvars, fd') = rewrite_sizeof_fun params_map fd in
        let id = id_of_fundef fd in
@@ -1282,6 +1294,17 @@ let rewrite_sizeof (Defs defs) =
          if KidSet.is_empty nvars then params_map
          else Bindings.add id nvars params_map in
        (params_map', defs @ [DEF_fundef fd'])
+    | DEF_val (LB_aux (lb, annot)) ->
+       begin
+         let lb' = match lb with
+         | LB_val_explicit (typschm, pat, exp) ->
+           let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in
+           LB_val_explicit (typschm, pat, exp')
+         | LB_val_implicit (pat, exp) ->
+           let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in
+           LB_val_implicit (pat, exp') in
+         (params_map, defs @ [DEF_val (LB_aux (lb', annot))])
+       end
     | def ->
        (params_map, defs @ [def]) in
 
@@ -1314,7 +1337,7 @@ let rewrite_sizeof (Defs defs) =
        DEF_spec (VS_aux (VS_cast_spec (rewrite_typschm typschm id, id), a))
     | _ -> def in
 
-  let (params_map, defs) = List.fold_left rewrite_sizeof_fundef
+  let (params_map, defs) = List.fold_left rewrite_sizeof_def
                                           (Bindings.empty, []) defs in
   let defs = List.map (rewrite_sizeof_valspec params_map) defs in
   Defs defs
@@ -1941,7 +1964,12 @@ let remove_bitvector_pat pat =
     (letexp, letbind) in
 
   let compose_guards guards =
-    List.fold_right (Util.option_binop bitwise_and_exp) guards None in
+    let conj g1 g2 = match g1, g2 with
+      | Some g1, Some g2 -> Some (bitwise_and_exp g1 g2)
+      | Some g1, None -> Some g1
+      | None, Some g2 -> Some g2
+      | None, None -> None in
+    List.fold_right conj guards None in
 
   let flatten_guards_decls gd =
     let (guards,decls,letbinds) = Util.split3 gd in
@@ -2152,7 +2180,7 @@ let rewrite_defs_guarded_pats =
 
 
 let id_is_local_var id env = match Env.lookup_id id env with
-  | Local _ | Unbound -> true
+  | Local _ -> true
   | _ -> false
 
 let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
@@ -2164,6 +2192,19 @@ let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
   | LEXP_vector_range (lexp,_,_)
   | LEXP_field (lexp,_) -> lexp_is_local lexp env
 
+let id_is_unbound id env = match Env.lookup_id id env with
+  | Unbound -> true
+  | _ -> false
+
+let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with
+  | LEXP_memory _ -> false
+  | LEXP_id id
+  | LEXP_cast (_, id) -> id_is_unbound id env
+  | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps
+  | LEXP_vector (lexp,_)
+  | LEXP_vector_range (lexp,_,_)
+  | LEXP_field (lexp,_) -> lexp_is_local_intro lexp env
+
 let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with
   | Some (_, _, eff) -> effectful_effs eff
   | _ -> false
@@ -2171,6 +2212,13 @@ let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with
 let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = match lexp with
   | LEXP_id id | LEXP_cast (_, id) ->
     (le, E_aux (E_id id, annot), (fun exp -> exp))
+  | LEXP_tup les ->
+    let get_id (LEXP_aux(lexp,((l,_) as annot)) as le) = match lexp with
+      | LEXP_id id | LEXP_cast (_, id) -> E_aux (E_id id, annot)
+      | _ ->
+        raise (Reporting_basic.err_unreachable l
+          ("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in
+    (le, E_aux (E_tuple (List.map get_id les), annot), (fun exp -> exp))
   | LEXP_vector (lexp, e) ->
     let (lexp, access, rexp) = rewrite_local_lexp lexp in
     (lexp, E_aux (E_vector_access (access, e), annot),
@@ -2184,7 +2232,7 @@ let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = match lex
     let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in
     (lexp, E_aux (E_field (access, id), annot),
     (fun exp -> rexp (E_aux (E_record_update (access, field_update exp), annot))))
-  | _ -> raise (Reporting_basic.err_unreachable l "unsupported lexp")
+  | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le))
 
 (*Expects to be called after rewrite_defs; thus the following should not appear:
   internal_exp of any form
@@ -2201,7 +2249,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
     let rec walker exps = match exps with
       | [] -> []
       | (E_aux(E_assign(le,e), ((l, Some (env,typ,eff)) as annot)) as exp)::exps
-        when lexp_is_local le env && not (lexp_is_effectful le)->
+        when lexp_is_local_intro le env && not (lexp_is_effectful le) ->
         let (le', _, re') = rewrite_local_lexp le in
         let e' = re' (rewrite_base e) in
         let exps' = walker exps in
@@ -2254,7 +2302,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
     in
     rewrap (E_block (walker exps))
   | E_assign(le,e)
-    when lexp_is_local le (env_of full_exp) && not (lexp_is_effectful le) ->
+    when lexp_is_local_intro le (env_of full_exp) && not (lexp_is_effectful le) ->
     let (le', _, re') = rewrite_local_lexp le in
     let e' = re' (rewrite_base e) in
     let block = E_aux (E_block [], simple_annot l unit_typ) in
@@ -2339,12 +2387,11 @@ let rewrite_defs_early_return =
   | _ -> exp in
 
   let e_block es =
-    (* let rec walker = function
-    | e :: es -> if is_return e then [e] else e :: walker es
-    | [] -> [] in
-    let es = walker es in *)
     match es with
     | [E_aux (e, _)] -> e
+    | _ :: _ when is_return (Util.last es) ->
+       let (E_aux (_, annot) as e) = Util.last es in
+       E_return (E_aux (E_block (Util.butlast es @ [get_return e]), annot))
     | _ -> E_block es in
 
   let e_if (e1, e2, e3) =
@@ -2372,14 +2419,19 @@ let rewrite_defs_early_return =
     | _ -> full_exp in
 
   let rewrite_funcl_early_return _ (FCL_aux (FCL_Funcl (id, pat, exp), a)) =
-    let exp = fold_exp
-      { id_exp_alg with e_block = e_block; e_if = e_if; e_case = e_case;
-        e_aux = e_aux } exp in
+    let exp =
+      exp
+      (* Pull early returns out as far as possible *)
+      |> fold_exp { id_exp_alg with e_block = e_block; e_if = e_if; e_case = e_case }
+      (* Remove singleton E_return *)
+      |> get_return
+      (* Fix effect annotations *)
+      |> fold_exp { id_exp_alg with e_aux = e_aux } in
     let a = match a with
     | (l, Some (env, typ, eff)) ->
       (l, Some (env, typ, union_effects eff (effect_of exp)))
     | _ -> a in
-    FCL_aux (FCL_Funcl (id, pat, get_return exp), a) in
+    FCL_aux (FCL_Funcl (id, pat, exp), a) in
 
   let rewrite_fun_early_return rewriters
     (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), a)) =
@@ -2441,7 +2493,7 @@ let rewrite_overload_cast (Defs defs) =
   let remove_cast_vs (VS_aux (vs_aux, annot)) =
     match vs_aux with
     | VS_val_spec (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot)
-    | VS_extern_no_rename (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot)
+    | VS_extern_no_rename (typschm, id) -> VS_aux (VS_extern_no_rename (typschm, id), annot)
     | VS_extern_spec (typschm, id, e) -> VS_aux (VS_extern_spec (typschm, id, e), annot)
     | VS_cast_spec (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot)
   in
@@ -2463,6 +2515,11 @@ let rewrite_undefined =
        mk_exp (E_app (prepend_id "undefined_" id, [mk_lit_exp L_unit]))
     | Typ_app (id, args) ->
        mk_exp (E_app (prepend_id "undefined_" id, List.concat (List.map undefined_of_typ_args args)))
+    | Typ_var kid ->
+       (* FIXME: bit of a hack, need to add a restriction to how
+          polymorphic undefined can be in the type checker to
+          guarantee this always works. *)
+       mk_exp (E_id (prepend_id "typ_" (id_of_kid kid)))
     | Typ_fn _ -> assert false
   and undefined_of_typ_args (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
     match typ_arg_aux with
@@ -2473,7 +2530,6 @@ let rewrite_undefined =
   let rewrite_e_aux (E_aux (e_aux, _) as exp) =
     match e_aux with
     | E_lit (L_aux (L_undef, l)) ->
-       print_endline ("Undefined: " ^ string_of_typ (typ_of exp));
        check_exp (env_of exp) (undefined_of_typ (typ_of exp)) (typ_of exp)
     | _ -> exp
   in
@@ -2501,10 +2557,15 @@ let rewrite_simple_types (Defs defs) =
        Typ_id (mk_id "int")
     | Typ_app (id, [_; _]) when Id.compare id (mk_id "range") = 0 ->
        Typ_id (mk_id "int")
+    | Typ_app (id, args) -> Typ_app (id, List.concat (List.map simple_typ_arg args))
     | Typ_fn (typ1, typ2, effs) -> Typ_fn (simple_typ typ1, simple_typ typ2, effs)
     | Typ_tup typs -> Typ_tup (List.map simple_typ typs)
     | Typ_exist (_, _, Typ_aux (typ, l)) -> simple_typ_aux typ
     | typ_aux -> typ_aux
+  and simple_typ_arg (Typ_arg_aux (typ_arg_aux, l)) =
+    match typ_arg_aux with
+    | Typ_arg_typ typ -> [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)]
+    | _ -> []
   in
   let simple_typschm (TypSchm_aux (TypSchm_ts (typq, typ), annot)) =
     TypSchm_aux (TypSchm_ts (simple_typquant typq, simple_typ typ), annot)
@@ -2512,7 +2573,7 @@ let rewrite_simple_types (Defs defs) =
   let simple_vs (VS_aux (vs_aux, annot)) =
     match vs_aux with
     | VS_val_spec (typschm, id) -> VS_aux (VS_val_spec (simple_typschm typschm, id), annot)
-    | VS_extern_no_rename (typschm, id) -> VS_aux (VS_val_spec (simple_typschm typschm, id), annot)
+    | VS_extern_no_rename (typschm, id) -> VS_aux (VS_extern_no_rename (simple_typschm typschm, id), annot)
     | VS_extern_spec (typschm, id, e) -> VS_aux (VS_extern_spec (simple_typschm typschm, id, e), annot)
     | VS_cast_spec (typschm, id) -> VS_aux (VS_cast_spec (simple_typschm typschm, id), annot)
   in
@@ -2549,6 +2610,43 @@ let rewrite_simple_types (Defs defs) =
   let defs = Defs (List.map simple_def defs) in
   rewrite_defs_base simple_defs defs
 
+let rewrite_tuple_assignments defs =
+  let assign_tuple e_aux annot =
+    let env = env_of_annot annot in
+    match e_aux with
+    | E_assign (LEXP_aux (LEXP_tup lexps, _), exp) ->
+       let (_, ids) = List.fold_left (fun (n, ids) _ -> (n + 1, ids @ [mk_id ("tup__" ^ string_of_int n)])) (0, []) lexps in
+       let block_assign i lexp = mk_exp (E_assign (strip_lexp lexp, mk_exp (E_id (mk_id ("tup__" ^ string_of_int i))))) in
+       let block = mk_exp (E_block (List.mapi block_assign lexps)) in
+       let letbind = mk_letbind (mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids))) (strip_exp exp) in
+       let let_exp = mk_exp (E_let (letbind, block)) in
+       check_exp env let_exp unit_typ
+    | _ -> E_aux (e_aux, annot)
+  in
+  let assign_exp = {
+      id_exp_alg with
+      e_aux = (fun (e_aux, annot) -> assign_tuple e_aux annot)
+    } in
+  let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in
+  rewrite_defs_base assign_defs defs
+
+let rewrite_simple_assignments defs =
+  let assign_e_aux e_aux annot =
+    let env = env_of_annot annot in
+    match e_aux with
+    | E_assign (lexp, exp) ->
+       let (lexp, _, rhs) = rewrite_local_lexp lexp in
+       let assign = mk_exp (E_assign (strip_lexp lexp, strip_exp (rhs exp))) in
+       check_exp env assign unit_typ
+    | _ -> E_aux (e_aux, annot)
+  in
+  let assign_exp = {
+      id_exp_alg with
+      e_aux = (fun (e_aux, annot) -> assign_e_aux e_aux annot)
+    } in
+  let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in
+  rewrite_defs_base assign_defs defs
+
 let rewrite_defs_remove_blocks =
   let letbind_wild v body =
     let (E_aux (_,(l,tannot))) = v in
@@ -2814,7 +2912,8 @@ let rewrite_defs_letbind_effects  =
        rewrap (E_let (lb,n_exp body k)))
     | E_sizeof nexp ->
        k (rewrap (E_sizeof nexp))
-    | E_constraint nc -> failwith "E_constraint should have been removed till now"
+    | E_constraint nc ->
+       k (rewrap (E_constraint nc))
     | E_sizeof_internal annot ->
        k (rewrap (E_sizeof_internal annot))
     | E_assign (lexp,exp1) ->
@@ -2869,14 +2968,25 @@ let rewrite_defs_letbind_effects  =
 
 let rewrite_defs_effectful_let_expressions =
 
-  let e_let (lb,body) = 
+  let rec pat_of_local_lexp (LEXP_aux (lexp, ((l, _) as annot))) = match lexp with
+    | LEXP_id id -> P_aux (P_id id, annot)
+    | LEXP_cast (typ, id) -> P_aux (P_typ (typ, P_aux (P_id id, annot)), annot)
+    | LEXP_tup lexps -> P_aux (P_tup (List.map pat_of_local_lexp lexps), annot)
+    | _ -> raise (Reporting_basic.err_unreachable l "unexpected local lexp") in
+
+  let e_let (lb,body) =
     match lb with
+    | LB_aux (LB_val_implicit (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _)
+      when lexp_is_local le (env_of_annot annot) ->
+      (* Rewrite assignments to local variables into let bindings *)
+      let (lhs, _, rhs) = rewrite_local_lexp le in
+      E_let (LB_aux (LB_val_implicit (pat_of_local_lexp lhs, rhs exp), annot), body)
     | LB_aux (LB_val_explicit (_,pat,exp'),annot')
     | LB_aux (LB_val_implicit (pat,exp'),annot') ->
        if effectful exp'
        then E_internal_plet (pat,exp',body)
        else E_let (lb,body) in
-                             
+
   let e_internal_let = fun (lexp,exp1,exp2) ->
     match lexp with
     | LEXP_aux (LEXP_id id,annot)
@@ -2890,7 +3000,7 @@ let rewrite_defs_effectful_let_expressions =
 
   let alg = { id_exp_alg with e_let = e_let; e_internal_let = e_internal_let } in
   rewrite_defs_base
-    {rewrite_exp = (fun _ -> fold_exp alg)
+    { rewrite_exp = (fun _ -> fold_exp alg)
     ; rewrite_pat = rewrite_pat
     ; rewrite_let = rewrite_let
     ; rewrite_lexp = rewrite_lexp
@@ -2912,13 +3022,25 @@ let eqidtyp (id1,_) (id2,_) =
   let name2 = match id2 with Id_aux ((Id name | DeIid name),_) -> name in
   name1 = name2
 
+let find_introduced_vars exp =
+  let lEXP_aux ((ids,lexp),annot) =
+    let ids = match lexp, annot with
+    | LEXP_id id, (_, Some (env, _, _))
+    | LEXP_cast (_, id), (_, Some (env, _, _))
+      when id_is_unbound id env -> IdSet.add id ids
+    | _ -> ids in
+    (ids, LEXP_aux (lexp, annot)) in
+  fst (fold_exp
+    { (compute_exp_alg IdSet.empty IdSet.union) with lEXP_aux = lEXP_aux } exp)
+
 let find_updated_vars exp =
+  let intros = find_introduced_vars exp in
   let lEXP_aux ((ids,lexp),annot) =
     let ids = match lexp, annot with
-    | LEXP_id id, (_, Some (env, _, _)) ->
-      (match Env.lookup_id id env with
-      | Local (Mutable, _) -> (id, annot) :: ids
-      | _ -> ids)
+    | LEXP_id id, (_, Some (env, _, _))
+    | LEXP_cast (_, id), (_, Some (env, _, _))
+      when id_is_local_var id env && not (IdSet.mem id intros) ->
+      (id, annot) :: ids
     | _ -> ids in
     (ids, LEXP_aux (lexp, annot)) in
   dedup eqidtyp (fst (fold_exp
@@ -3170,7 +3292,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
      "tail-position": check the definition nexp_term and where it is used. *)
   | _ -> exp
 
-let replace_memwrite_e_assign exp = 
+let replace_memwrite_e_assign exp =
   let e_aux = fun (expaux,annot) ->
     match expaux with
     | E_assign (LEXP_aux (LEXP_memory (id,args),_),v) -> E_aux (E_app (id,args @ [v]),annot)
@@ -3278,7 +3400,7 @@ let rewrite_defs_remove_superfluous_returns =
 
   let alg = { id_exp_alg with e_aux = e_aux } in
   rewrite_defs_base
-    {rewrite_exp = (fun _ -> fold_exp alg)
+    { rewrite_exp = (fun _ -> fold_exp alg)
     ; rewrite_pat = rewrite_pat
     ; rewrite_let = rewrite_let
     ; rewrite_lexp = rewrite_lexp
@@ -3304,7 +3426,8 @@ let rewrite_defs_remove_e_assign =
 let recheck_defs defs = fst (check initial_env defs)
 
 let rewrite_defs_lem =[
-  top_sort_defs;
+  (* top_sort_defs; *)
+  rewrite_trivial_sizeof;
   rewrite_sizeof;
   rewrite_defs_remove_vector_concat;
   rewrite_defs_remove_bitvector_pats;
@@ -3323,13 +3446,15 @@ let rewrite_defs_lem =[
 let rewrite_defs_ocaml = [
     (* top_sort_defs; *)
   rewrite_undefined;
+  rewrite_tuple_assignments;
+  rewrite_simple_assignments;
   rewrite_defs_remove_vector_concat;
   rewrite_constraint;
   rewrite_trivial_sizeof;
-  (* rewrite_sizeof; *)
-  (* rewrite_simple_types; *)
-  (* rewrite_overload_cast; *)
-  (* rewrite_defs_exp_lift_assign; *)
+  rewrite_sizeof;
+  rewrite_simple_types;
+  rewrite_overload_cast;
+  rewrite_defs_exp_lift_assign;
   (* rewrite_defs_exp_lift_assign *)
   (* rewrite_defs_separate_numbs *)
   ]
diff --git a/src/sail.ml b/src/sail.ml
index 2f1e5c4a..04e1a6fd 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -73,6 +73,12 @@ let options = Arg.align ([
   ( "-ocaml_lib",
     Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml),
     "<filename> provide additional library to open in OCaml output");
+  ( "-lem_sequential",
+    Arg.Set Process_file.opt_lem_sequential,
+    " use sequential state monad for Lem output");
+  ( "-lem_mwords",
+    Arg.Set Process_file.opt_lem_mwords,
+    " use native machine word library for Lem output");
 (*
   ( "-i",
     Arg.String (fun l -> lib := l::!lib),
@@ -160,11 +166,10 @@ let main() =
        then output "" Lem_ast_out [out_name,ast]
        else ());
       (if !(opt_print_ocaml)
-       then let ast_ocaml = rewrite_ast_ocaml ast in
-         Pretty_print_sail.pp_defs stdout ast_ocaml;
-         if !(opt_libs_ocaml) = []
-         then output "" (Ocaml_out None) [out_name,ast_ocaml]
-         else output "" (Ocaml_out (Some (List.hd !opt_libs_ocaml))) [out_name,ast_ocaml]
+       then
+         let ast_ocaml = rewrite_ast_ocaml ast in
+         let out = match !opt_file_out with None -> "out" | Some s -> s in
+         Ocaml_backend.ocaml_compile out ast_ocaml
        else ());
       (if !(opt_print_lem)
        then let ast_lem = rewrite_ast_lem ast in
diff --git a/src/type_check.ml b/src/type_check.ml
index a3c4f767..4eb0688b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -91,74 +91,6 @@ let orig_kid (Kid_aux (Var v, l) as kid) =
   with
   | Not_found -> kid
 
-let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown)
-let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown)
-let mk_id str = Id_aux (Id str, Parse_ast.Unknown)
-let mk_kid str = Kid_aux (Var ("'" ^ str), Parse_ast.Unknown)
-let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown)
-
-let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown)
-
-let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown)
-
-let rec nexp_simp (Nexp_aux (nexp, l)) = Nexp_aux (nexp_simp_aux nexp, l)
-and nexp_simp_aux = function
-  | Nexp_minus (Nexp_aux (Nexp_sum (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 ->
-     nexp_simp_aux n1
-  | Nexp_sum (Nexp_aux (Nexp_minus (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 ->
-     nexp_simp_aux n1
-  | Nexp_sum (n1, n2) ->
-     begin
-       let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
-       let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
-       match n1_simp, n2_simp with
-       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 + c2)
-       | _, Nexp_neg n2 -> Nexp_minus (n1, n2)
-       | _, _ -> Nexp_sum (n1, n2)
-     end
-  | Nexp_times (n1, n2) ->
-     begin
-       let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
-       let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
-       match n1_simp, n2_simp with
-       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 * c2)
-       | _, _ -> Nexp_times (n1, n2)
-     end
-  | Nexp_minus (n1, n2) ->
-     begin
-       let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
-       let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
-       typ_debug ("SIMP: " ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2);
-       match n1_simp, n2_simp with
-       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 - c2)
-       | _, _ -> Nexp_minus (n1, n2)
-     end
-  | nexp -> nexp
-
-let int_typ = mk_id_typ (mk_id "int")
-let nat_typ = mk_id_typ (mk_id "nat")
-let unit_typ = mk_id_typ (mk_id "unit")
-let bit_typ = mk_id_typ (mk_id "bit")
-let real_typ = mk_id_typ (mk_id "real")
-let app_typ id args = mk_typ (Typ_app (id, args))
-let atom_typ nexp =
-  mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))]))
-let range_typ nexp1 nexp2 =
-  mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp1));
-                                   mk_typ_arg (Typ_arg_nexp (nexp_simp nexp2))]))
-let bool_typ = mk_id_typ (mk_id "bool")
-let string_typ = mk_id_typ (mk_id "string")
-let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)]))
-
-let vector_typ n m ord typ =
-  mk_typ (Typ_app (mk_id "vector",
-                   [mk_typ_arg (Typ_arg_nexp (nexp_simp n));
-                    mk_typ_arg (Typ_arg_nexp (nexp_simp m));
-                    mk_typ_arg (Typ_arg_order ord);
-                    mk_typ_arg (Typ_arg_typ typ)]))
-
-let exc_typ = mk_id_typ (mk_id "exception")
-
 let is_range (Typ_aux (typ_aux, _)) =
   match typ_aux with
   | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)])
@@ -173,25 +105,6 @@ let is_list (Typ_aux (typ_aux, _)) =
        when string_of_id f = "list" -> Some typ
   | _ -> None
 
-let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown)
-let nminus n1 n2 = Nexp_aux (Nexp_minus (n1, n2), Parse_ast.Unknown)
-let nsum n1 n2 = Nexp_aux (Nexp_sum (n1, n2), Parse_ast.Unknown)
-let ntimes n1 n2 = Nexp_aux (Nexp_times (n1, n2), Parse_ast.Unknown)
-let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown)
-let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
-let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown)
-
-let nc_eq n1 n2 = mk_nc (NC_fixed (n1, n2))
-let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2))
-let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
-let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown)
-let nc_lt n1 n2 = nc_lteq n1 (nsum n2 (nconstant 1))
-let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nconstant 1))
-let nc_and nc1 nc2 = mk_nc (NC_and (nc1, nc2))
-let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2))
-let nc_true = mk_nc NC_true
-let nc_false = mk_nc NC_false
-
 let mk_lit l = E_aux (E_lit (L_aux (l, Parse_ast.Unknown)), (Parse_ast.Unknown, ()))
 
 let rec nc_negate (NC_aux (nc, _)) =
@@ -211,10 +124,6 @@ let rec nc_negate (NC_aux (nc, _)) =
 
 (* Utilities for constructing effect sets *)
 
-let mk_effect effs =
-  Effect_aux (Effect_set (List.map (fun be_aux -> BE_aux (be_aux, Parse_ast.Unknown)) effs), Parse_ast.Unknown)
-
-let no_effect = mk_effect []
 
 module BESet = Set.Make(BE)
 
@@ -246,10 +155,6 @@ let string_of_index_sort = function
      ^ string_of_list " & " (fun (x, y) -> string_of_nexp x ^ " <= " ^ string_of_nexp y) constraints
      ^ "}"
 
-let quant_items : typquant -> quant_item list = function
-  | TypQ_aux (TypQ_tq qis, _) -> qis
-  | TypQ_aux (TypQ_no_forall, _) -> []
-
 let quant_split typq =
   let qi_kopt = function
     | QI_aux (QI_id kopt, _) -> [kopt]
@@ -262,23 +167,6 @@ let quant_split typq =
   let qis = quant_items typq in
   List.concat (List.map qi_kopt qis), List.concat (List.map qi_nc qis)
 
-let kopt_kid (KOpt_aux (kopt_aux, _)) =
-  match kopt_aux with
-  | KOpt_none kid | KOpt_kind (_, kid) -> kid
-
-let is_nat_kopt = function
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), _), _) -> true
-  | KOpt_aux (KOpt_none _, _) -> true
-  | _ -> false
-
-let is_order_kopt = function
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), _), _) -> true
-  | _ -> false
-
-let is_typ_kopt = function
-  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), _), _) -> true
-  | _ -> false
-
 (**************************************************************************)
 (* 1. Substitutions                                                       *)
 (**************************************************************************)
@@ -768,6 +656,7 @@ end = struct
          end
 
   let add_register id typ env =
+    wf_typ env typ;
     if Bindings.mem id env.registers
     then typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound")
     else
@@ -1686,13 +1575,31 @@ let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
 
 (* Flow typing *)
 
+let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with
+  | Nexp_constant c -> Some (big_int_of_int c)
+  | Nexp_times (n1, n2) ->
+     Util.option_binop add_big_int (big_int_of_nexp n1) (big_int_of_nexp n2)
+  | Nexp_sum (n1, n2) ->
+     Util.option_binop add_big_int (big_int_of_nexp n1) (big_int_of_nexp n2)
+  | Nexp_minus (n1, n2) ->
+     Util.option_binop add_big_int (big_int_of_nexp n1) (big_int_of_nexp n2)
+  | Nexp_exp n ->
+     Util.option_map (power_int_positive_big_int 2) (big_int_of_nexp n)
+  | _ -> None
+
 let destruct_atom (Typ_aux (typ_aux, _)) =
   match typ_aux with
-  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant c, _)), _)])
-       when string_of_id f = "atom" -> c
-  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant c1, _)), _); Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant c2, _)), _)])
-       when string_of_id f = "range" && c1 = c2 -> c1
-  | _ -> assert false
+  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp, _)])
+       when string_of_id f = "atom" ->
+     Util.option_map (fun c -> (c, nexp)) (big_int_of_nexp nexp)
+  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp1, _); Typ_arg_aux (Typ_arg_nexp nexp2, _)])
+       when string_of_id f = "range" ->
+     begin
+       match big_int_of_nexp nexp1, big_int_of_nexp nexp2 with
+       | Some c1, Some c2 -> if eq_big_int c1 c2 then Some (c1, nexp1) else None
+       | _ -> None
+     end
+  | _ -> None
 
 let destruct_atom_nexp env typ =
   match Env.expand_synonyms env typ with
@@ -1702,20 +1609,6 @@ let destruct_atom_nexp env typ =
        when string_of_id f = "range" -> Some n
   | _ -> None
 
-let restrict_range_upper c1 (Typ_aux (typ_aux, l) as typ) =
-  match typ_aux with
-  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp, _); Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant c2, _)), _)])
-     when string_of_id f = "range" ->
-     range_typ nexp (nconstant (min c1 c2))
-  | _ -> typ
-
-let restrict_range_lower c1 (Typ_aux (typ_aux, l) as typ) =
-  match typ_aux with
-  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant c2, _)), _); Typ_arg_aux (Typ_arg_nexp nexp, _)])
-     when string_of_id f = "range" ->
-     range_typ (nconstant (max c1 c2)) nexp
-  | _ -> typ
-
 exception Not_a_constraint;;
 
 let rec assert_nexp (E_aux (exp_aux, l)) =
@@ -1737,12 +1630,42 @@ let rec assert_constraint (E_aux (exp_aux, l)) =
   | _ -> nc_true
 
 type flow_constraint =
-  | Flow_lteq of int
-  | Flow_gteq of int
+  | Flow_lteq of big_int * nexp
+  | Flow_gteq of big_int * nexp
+
+let restrict_range_upper c1 nexp1 (Typ_aux (typ_aux, l) as typ) =
+  match typ_aux with
+  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp, _); Typ_arg_aux (Typ_arg_nexp nexp2, _)])
+     when string_of_id f = "range" ->
+     begin
+       match big_int_of_nexp nexp2 with
+       | Some c2 ->
+          let upper = if (lt_big_int c1 c2) then nexp1 else nexp2 in
+          range_typ nexp upper
+       | _ -> typ
+     end
+  | _ -> typ
+
+let restrict_range_lower c1 nexp1 (Typ_aux (typ_aux, l) as typ) =
+  match typ_aux with
+  | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp2, _); Typ_arg_aux (Typ_arg_nexp nexp, _)])
+     when string_of_id f = "range" ->
+     begin
+       match big_int_of_nexp nexp2 with
+       | Some c2 ->
+          let lower = if (gt_big_int c1 c2) then nexp1 else nexp2 in
+          range_typ lower nexp
+       | _ -> typ
+     end
+  | _ -> typ
 
 let apply_flow_constraint = function
-  | Flow_lteq c -> (restrict_range_upper c, restrict_range_lower (c + 1))
-  | Flow_gteq c -> (restrict_range_lower c, restrict_range_upper (c - 1))
+  | Flow_lteq (c, nexp) ->
+     (restrict_range_upper c nexp,
+      restrict_range_lower (succ_big_int c) (nexp_simp (nsum nexp (nconstant 1))))
+  | Flow_gteq (c, nexp) ->
+     (restrict_range_lower c nexp,
+      restrict_range_upper (pred_big_int c) (nexp_simp (nminus nexp (nconstant 1))))
 
 let rec infer_flow env (E_aux (exp_aux, (l, _))) =
   match exp_aux with
@@ -1764,20 +1687,34 @@ let rec infer_flow env (E_aux (exp_aux, (l, _))) =
      [], [nc_gt n1 n2]
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lt_range_atom" ->
      let kid = Env.fresh_kid env in
-     let c = destruct_atom (typ_of y) in
-     [(v, Flow_lteq (c - 1))], []
+     begin
+       match destruct_atom (typ_of y) with
+       | Some (c, nexp) ->
+          [(v, Flow_lteq (pred_big_int c, nexp_simp (nminus nexp (nconstant 1))))], []
+       | _ -> [], []
+     end
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lteq_range_atom" ->
      let kid = Env.fresh_kid env in
-     let c = destruct_atom (typ_of y) in
-     [(v, Flow_lteq c)], []
+     begin
+       match destruct_atom (typ_of y) with
+       | Some (c, nexp) -> [(v, Flow_lteq (c, nexp))], []
+       | _ -> [], []
+     end
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "gt_range_atom" ->
      let kid = Env.fresh_kid env in
-     let c = destruct_atom (typ_of y) in
-     [(v, Flow_gteq (c + 1))], []
+     begin
+       match destruct_atom (typ_of y) with
+       | Some (c, nexp) ->
+          [(v, Flow_gteq (succ_big_int c, nexp_simp (nsum nexp (nconstant 1))))], []
+       | _ -> [], []
+     end
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "gteq_range_atom" ->
      let kid = Env.fresh_kid env in
-     let c = destruct_atom (typ_of y) in
-     [(v, Flow_gteq c)], []
+     begin
+       match destruct_atom (typ_of y) with
+       | Some (c, nexp) -> [(v, Flow_gteq (c, nexp))], []
+       | _ -> [], []
+     end
   | _ -> [], []
 
 let rec add_flows b flows env =
@@ -1857,6 +1794,7 @@ let irule r env exp =
 
 let strip_exp : 'a exp -> unit exp = function exp -> map_exp_annot (fun (l, _) -> (l, ())) exp
 let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) -> (l, ())) pat
+let strip_lexp : 'a lexp -> unit lexp = function lexp -> map_lexp_annot (fun (l, _) -> (l, ())) lexp
 
 let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ_aux, _) as typ) : tannot exp =
   let annot_exp_effect exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in
@@ -2599,6 +2537,8 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      let else_branch' = crule check_exp (add_constraints (List.map nc_negate constrs) (add_flows false flows env)) else_branch (typ_of then_branch') in
      annot_exp (E_if (cond', then_branch', else_branch')) (typ_of then_branch')
   | E_vector_access (v, n) -> infer_exp env (E_aux (E_app (mk_id "vector_access", [v; n]), (l, ())))
+  | E_vector_update (v, n, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update", [v; n; exp]), (l, ())))
+  | E_vector_update_subrange (v, n, m, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update_subrange", [v; n; m; exp]), (l, ())))
   | E_vector_append (v1, v2) -> infer_exp env (E_aux (E_app (mk_id "append", [v1; v2]), (l, ())))
   | E_vector_subrange (v, n, m) -> infer_exp env (E_aux (E_app (mk_id "vector_subrange", [v; n; m]), (l, ())))
   | E_vector [] -> typ_error l "Cannot infer type of empty vector"
diff --git a/src/type_check.mli b/src/type_check.mli
index e3b9b81b..857e0019 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -103,6 +103,8 @@ module Env : sig
 
   val get_overloads : id -> t -> id list
 
+  val get_num_def : id -> t -> nexp
+
   val is_extern : id -> t -> bool
 
   val get_extern : id -> t -> string
@@ -151,73 +153,28 @@ val add_typquant : typquant -> Env.t -> Env.t
    not of this form. *)
 val orig_kid : kid -> kid
 
-(* Some handy utility functions for constructing types. *)
-val mk_typ : typ_aux -> typ
-val mk_typ_arg : typ_arg_aux -> typ_arg
-val mk_id : string -> id
-val mk_id_typ : id -> typ
-
-val no_effect : effect
-val mk_effect : base_effect_aux list -> effect
-
 val union_effects : effect -> effect -> effect
 val equal_effects : effect -> effect -> bool
 
-val nconstant : int -> nexp
-val nminus : nexp -> nexp -> nexp
-val nsum : nexp -> nexp -> nexp
-val ntimes : nexp -> nexp -> nexp
-val npow2 : nexp -> nexp
-val nvar : kid -> nexp
-val nid : id -> nexp (* NOTE: Nexp_id's don't do anything currently *)
-
-(* Numeric constraint builders *)
-val nc_eq : nexp -> nexp -> n_constraint
-val nc_neq : nexp -> nexp -> n_constraint
-val nc_lteq : nexp -> nexp -> n_constraint
-val nc_gteq : nexp -> nexp -> n_constraint
-val nc_lt : nexp -> nexp -> n_constraint
-val nc_gt : nexp -> nexp -> n_constraint
-val nc_and : n_constraint -> n_constraint -> n_constraint
-val nc_or : n_constraint -> n_constraint -> n_constraint
-val nc_true : n_constraint
-val nc_false : n_constraint
-
 (* Negate a n_constraint. Note that there's no NC_not constructor, so
    this flips all the inequalites a the n_constraint leaves and uses
    de-morgans to switch and to or and vice versa. *)
 val nc_negate : n_constraint -> n_constraint
 
-val is_nat_kopt : kinded_id -> bool
-val is_order_kopt : kinded_id -> bool
-val is_typ_kopt : kinded_id -> bool
-
-(* Sail builtin types. *)
-val int_typ : typ
-val nat_typ : typ
-val atom_typ : nexp -> typ
-val range_typ : nexp -> nexp -> typ
-val bit_typ : typ
-val bool_typ : typ
-val unit_typ : typ
-val string_typ : typ
-val real_typ : typ
-val vector_typ : nexp -> nexp -> order -> typ -> typ
-val list_typ : typ -> typ
-val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ
-val exc_typ : typ
-
 (* Vector with default order. *)
 val dvector_typ : Env.t -> nexp -> nexp -> typ -> typ
 
 (* Vector of specific length with default order, i.e. lvector_typ env n bit_typ = bit[n]. *)
 val lvector_typ : Env.t -> nexp -> typ -> typ
 
+val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ
+
 type tannot = (Env.t * typ * effect) option
 
 (* Strip the type annotations from an expression. *)
 val strip_exp : 'a exp -> unit exp
 val strip_pat : 'a pat -> unit pat
+val strip_lexp : 'a lexp -> unit lexp
 
 (* Check an expression has some type. Returns a fully annotated
    version of the expression, where each subexpression is annotated
diff --git a/src/util.ml b/src/util.ml
index 75732376..335fd36f 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -86,6 +86,15 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
+let rec last = function
+  | [x] -> x
+  | _ :: xs -> last xs
+  | [] -> raise (Failure "last")
+
+let rec butlast = function
+  | [x] -> []
+  | x :: xs -> x :: butlast xs
+  | [] -> []
 
 module Duplicate(S : Set.S) = struct
 
@@ -204,10 +213,8 @@ let option_bind f = function
   | Some(o) -> f o
 
 let rec option_binop f x y = match x, y with
-  | None, None -> None
-  | Some x, None -> Some x
-  | None, Some y -> Some y
   | Some x, Some y -> Some (f x y)
+  | _ -> None
 
 let changed2 f g x h y =
   match (g x, h y) with
diff --git a/src/util.mli b/src/util.mli
index aa442ada..11588de2 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -40,6 +40,11 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+(* Last element of a list *)
+val last : 'a list -> 'a
+
+val butlast : 'a list -> 'a list
+
 (** Mixed useful things *)
 module Duplicate(S : Set.S) : sig 
   type dups = 
@@ -77,10 +82,8 @@ val option_bind : ('a -> 'b option) -> 'a option -> 'b option
     whereas [option_default d (Some x)] returns [x]. *)
 val option_default : 'a -> 'a option -> 'a
 
-(** [option_binop f None None] returns [None], while
-    [option_binop f (Some x) None] and [option_binop f None (Some x)]
-    return [Some x], and [option_binop f (Some x) (Some y)] returns
-    [Some (f x y)] *)
+(** [option_binop f (Some x) (Some y)] returns [Some (f x y)],
+    and in all other cases, [option_binop] returns [None]. *)
 val option_binop : ('a -> 'a -> 'a) -> 'a option -> 'a option -> 'a option
 
 (** [option_get_exn exn None] throws the exception [exn],