Merge remote-tracking branch 'origin/mono-experiments' into experiments

19 files changed, 863 insertions, 337 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 955164a3..67381c52 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -297,6 +297,8 @@ let rec string_of_exp (E_aux (exp, _)) =
      ^ string_of_exp body
   | E_assert (test, msg) -> "assert(" ^ string_of_exp test ^ ", " ^ string_of_exp msg ^ ")"
   | E_exit exp -> "exit " ^ string_of_exp exp
+  | E_cons (x, xs) -> string_of_exp x ^ " :: " ^ string_of_exp xs
+  | E_list xs -> "[||" ^ string_of_list ", " string_of_exp xs ^ "||]"
   | _ -> "INTERNAL"
 and string_of_pexp (Pat_aux (pexp, _)) =
   match pexp with
@@ -400,6 +402,39 @@ let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) =
   | Nexp_neg n1, Nexp_neg n2 -> nexp_identical n1 n2
   | _, _ -> false
 
+let rec is_nexp_constant (Nexp_aux (nexp, _)) = match nexp with
+  | Nexp_id _ | Nexp_var _ -> false
+  | Nexp_constant _ -> true
+  | Nexp_times (n1, n2) | Nexp_sum (n1, n2) | Nexp_minus (n1, n2) ->
+    is_nexp_constant n1 && is_nexp_constant n2
+  | Nexp_exp n | Nexp_neg n -> is_nexp_constant n
+
+let rec simplify_nexp (Nexp_aux (nexp, l)) =
+  let rewrap n = Nexp_aux (n, l) in
+  let try_binop op n1 n2 c = (match simplify_nexp n1, simplify_nexp n2 with
+    | Nexp_aux (Nexp_constant i1, _), Nexp_aux (Nexp_constant i2, _) ->
+      rewrap (Nexp_constant (op i1 i2))
+    | n1, n2 -> rewrap (c n1 n2)) in
+  match nexp with
+  | 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 ->
+    (match simplify_nexp n with
+      | Nexp_aux (Nexp_constant i, _) ->
+        rewrap (Nexp_constant (power 2 i))
+      | n -> rewrap (Nexp_exp n))
+  | Nexp_neg n ->
+    (match simplify_nexp n with
+      | Nexp_aux (Nexp_constant i, _) ->
+        rewrap (Nexp_constant (-i))
+      | n -> rewrap (Nexp_neg n))
+  | _ -> rewrap nexp
+  (* | Nexp_sum of nexp * nexp (* sum *)
+  | Nexp_minus of nexp * nexp (* subtraction *)
+  | Nexp_exp of nexp (* exponential *)
+  | Nexp_neg of nexp (* For internal use *) *)
+
 let rec is_number (Typ_aux (t,_)) =
   match t with
   | Typ_app (Id_aux (Id "range", _),_)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 6e22d173..ae340839 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -119,6 +119,8 @@ end
 
 val nexp_frees : nexp -> KidSet.t
 val nexp_identical : nexp -> nexp -> bool
+val is_nexp_constant : nexp -> bool
+val simplify_nexp : nexp -> nexp
 
 val is_number : typ -> bool
 val is_vector_typ : typ -> bool
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 70850dc1..0944f42b 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -78,6 +78,8 @@ let read_reg_bitfield reg regfield =
   read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
   return (extract_only_element v)
 
+let reg_deref = read_reg
+
 val write_reg_aux : reg_name -> vector bitU -> M unit
 let write_reg_aux reg_name v =
   let regval = external_reg_value reg_name v in
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index f148c1ff..b4a15432 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -11,6 +11,12 @@ type nn = natural
 val pow : integer -> integer -> integer
 let pow m n = m ** (natFromInteger n)
 
+let bool_or (l, r) = (l || r)
+let bool_and (l, r) = (l && r)
+let bool_xor (l, r) = xor l r
+
+let list_append (l, r) = l ++ r
+
 let rec replace bs ((n : integer),b') = match bs with
   | [] -> []
   | b :: bs ->
@@ -18,6 +24,7 @@ let rec replace bs ((n : integer),b') = match bs with
               else b :: replace bs (n - 1,b')
   end
 
+let upper n = n
 
 (*** Bits *)
 type bitU = B0 | B1 | BU
@@ -39,6 +46,8 @@ let bitU_to_bool = function
   | BU -> failwith "to_bool applied to BU"
   end
 
+let cast_bit_bool = bitU_to_bool
+
 let bit_lifted_of_bitU = function
   | B0 -> Bitl_zero
   | B1 -> Bitl_one
@@ -196,6 +205,9 @@ let access (Vector bs start is_inc) n =
   if is_inc then List_extra.nth bs (natFromInteger (n - start))
   else List_extra.nth bs (natFromInteger (start - n))
 
+let vector_access_inc (v, i) = access v i
+let vector_access_dec (v, i) = access v i
+
 val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a
 let update_pos v n b =
   update_aux v n n [b]
@@ -238,9 +250,12 @@ let reset_bitvector_start v =
 let set_bitvector_start_to_length v =
   set_bitvector_start (bvlength v - 1) v
 
-let bitvector_concat (Bitvector bs start is_inc) (Bitvector bs' _ _) =
+let bitvector_concat (Bitvector bs start is_inc, Bitvector bs' _ _) =
   Bitvector (word_concat bs bs') start is_inc
 
+let norm_dec = reset_bitvector_start
+let adjust_dec = reset_bitvector_start
+
 let inline (^^^) = bitvector_concat
 
 val bvslice : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b
@@ -252,6 +267,13 @@ let bvslice (Bitvector bs start is_inc) i j =
   let subvector_bits = word_extract lo hi bs in
   Bitvector subvector_bits i is_inc
 
+let bitvector_subrange_inc (v, i, j) = bvslice v i j
+let bitvector_subrange_dec (v, i, j) = bvslice v i j
+
+let vector_subrange_bl (v, i, j) =
+  let v' = slice (bvec_to_vec v) i j in
+  get_elems v'
+
 (* this is for the vector slicing introduced in vector-concat patterns: i and j
 index into the "raw data", the list of bits. Therefore getting the bit list is
 easy, but the start index has to be transformed to match the old vector start
@@ -277,19 +299,20 @@ val bvupdate : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b
 let bvupdate v i j (Bitvector bs' _ _) =
   bvupdate_aux v i j bs'
 
-(* TODO: decide between nat/natural, change either here or in machine_word *)
-val getBit' : forall 'a. mword 'a -> nat -> bool
-let getBit' w n = getBit w (naturalFromNat n)
-
 val bvaccess : forall 'a. bitvector 'a -> integer -> bitU
 let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU (
-  if is_inc then getBit' bs (natFromInteger (n - start))
-  else getBit' bs (natFromInteger (start - n)))
+  if is_inc then getBit bs (natFromInteger (n - start))
+  else getBit bs (natFromInteger (start - n)))
 
 val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bitU -> bitvector 'a
 let bvupdate_pos v n b =
   bvupdate_aux v n n ((wordFromNatural (if bitU_to_bool b then 1 else 0)) : mword ty1)
 
+let bitvector_access_inc (v, i) = bvaccess v i
+let bitvector_access_dec (v, i) = bvaccess v i
+let bitvector_update_pos_dec (v, i, b) = bvupdate_pos v i b
+let bitvector_update_dec (v, i, j, v') = bvupdate v i j v'
+
 (*** Bit vector operations *)
 
 let extract_only_element (Vector elems _ _) = match elems with
@@ -308,6 +331,9 @@ let extract_only_bit (Bitvector elems _ _) =
   else
     failwith "extract_single_bit called for vector with more bits"*)
 
+let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
+let cast_bit_vec b = vec_to_bvec (Vector [b] 0 false)
+
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
   "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc
@@ -409,19 +435,25 @@ end
 let add_one_bit_ignore_overflow bits =
   List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
   
-let to_vec is_inc ((len : integer),(n : integer)) =
-  let start = if is_inc then 0 else len - 1 in
+let to_vec is_inc ((n : integer)) =
+  (* Bitvector length is determined by return type *)
   let bits = wordFromInteger n in
-  if integerFromNat (word_length bits) = len then
+  let len = integerFromNat (word_length bits) in
+  let start = if is_inc then 0 else len - 1 in
+  (*if integerFromNat (word_length bits) = len then*)
     Bitvector bits start is_inc
-  else
-    failwith "Vector length mismatch in to_vec"
+  (*else
+    failwith "Vector length mismatch in to_vec"*)
 
 let to_vec_big = to_vec
 
 let to_vec_inc = to_vec true
 let to_vec_dec = to_vec false
 
+let cast_0_vec = to_vec_dec
+let cast_1_vec = to_vec_dec
+let cast_01_vec = to_vec_dec
+
 (* TODO: Think about undefined bit(vector)s *)
 let to_vec_undef is_inc (len : integer) =
   Bitvector (failwith "undefined bitvector") (if is_inc then 0 else len-1) is_inc
@@ -429,19 +461,25 @@ let to_vec_undef is_inc (len : integer) =
 let to_vec_inc_undef = to_vec_undef true
 let to_vec_dec_undef = to_vec_undef false
 
-let exts (len, vec) = to_vec (bvget_dir vec) (len,signed vec)
-let extz (len, vec) = to_vec (bvget_dir vec) (len,unsigned vec)
+let exts (vec) = to_vec (bvget_dir vec) (signed vec)
+let extz (vec) = to_vec (bvget_dir vec) (unsigned vec)
+
+let exts_big (vec) = to_vec_big (bvget_dir vec) (signed_big vec)
+let extz_big (vec) = to_vec_big (bvget_dir vec) (unsigned_big vec)
 
-let exts_big (len, vec) = to_vec_big (bvget_dir vec) (len, signed_big vec)
-let extz_big (len, vec) = to_vec_big (bvget_dir vec) (len, unsigned_big vec)
+let extz_bl (bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
 
-let add = integerAdd
-let add_signed = integerAdd
-let minus = integerMinus
-let multiply = integerMult
-let modulo = hardware_mod
+let add (l,r) = integerAdd l r
+let add_signed (l,r) = integerAdd l r
+let sub (l,r) = integerMinus l r
+let multiply (l,r) = integerMult l r
+let quotient (l,r) = integerDiv l r
+let modulo (l,r) = hardware_mod l r
 let quot = hardware_quot
-let power = integerPow
+let power (l,r) = integerPow l r
+
+let sub_int = sub
+let mul_int = multiply
 
 (* TODO: this, and the definitions that use it, currently require Size for
    to_vec, which I'd rather avoid in favour of library versions; the
@@ -449,7 +487,7 @@ let power = integerPow
 let arith_op_vec op sign (size : integer) (Bitvector _ _ is_inc as l) r =
   let (l',r') = (to_num sign l, to_num sign r) in
   let n = op l' r' in
-  to_vec is_inc (size * (bvlength l),n)
+  to_vec is_inc (n)
 
 
 (* add_vec
@@ -464,9 +502,15 @@ let minus_VVV = arith_op_vec integerMinus false 1
 let mult_VVV = arith_op_vec integerMult false 2
 let multS_VVV = arith_op_vec integerMult true 2
 
+let mul_vec (l, r) = mult_VVV l r
+let mul_svec (l, r) = multS_VVV l r
+
+let add_vec (l, r) = add_VVV l r
+let sub_vec (l, r) = minus_VVV l r
+
 val arith_op_vec_range : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'b
 let arith_op_vec_range op sign size (Bitvector _ _ is_inc as l) r =
-  arith_op_vec op sign size l ((to_vec is_inc (bvlength l,r)) : bitvector 'a)
+  arith_op_vec op sign size l ((to_vec is_inc (r)) : bitvector 'a)
 
 (* add_vec_range
  * add_vec_range_signed
@@ -480,9 +524,12 @@ let minus_VIV = arith_op_vec_range integerMinus false 1
 let mult_VIV = arith_op_vec_range integerMult false 2
 let multS_VIV = arith_op_vec_range integerMult true 2
 
+let add_vec_int (l, r) = add_VIV l r
+let sub_vec_int (l, r) = minus_VIV l r
+
 val arith_op_range_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'b
 let arith_op_range_vec op sign size l (Bitvector _ _ is_inc as r) =
-  arith_op_vec op sign size ((to_vec is_inc (bvlength r, l)) : bitvector 'a) r
+  arith_op_vec op sign size ((to_vec is_inc (l)) : bitvector 'a) r
 
 (* add_range_vec
  * add_range_vec_signed
@@ -528,10 +575,10 @@ let arith_op_vec_vec_range op sign l r =
 let add_VVI = arith_op_vec_vec_range integerAdd false
 let addS_VVI = arith_op_vec_vec_range integerAdd true
 
-let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l)r =
+let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l) r =
   let l' = to_num sign l in
   let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
-  to_vec is_inc (bvlength l * size,n)
+  to_vec is_inc (n)
 
 (* add_vec_bit
  * add_vec_bit_signed
@@ -610,17 +657,19 @@ let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) =
   let n = natFromInteger n in
   match op with
   | LL_shift (*"<<"*) ->
-     Bitvector (shiftLeft bs (naturalFromNat n)) start is_inc
+     Bitvector (shiftLeft bs n) start is_inc
   | RR_shift (*">>"*) ->
-     Bitvector (shiftRight bs (naturalFromNat n)) start is_inc
+     Bitvector (shiftRight bs n) start is_inc
   | LLL_shift (*"<<<"*) ->
-     Bitvector (rotateLeft (naturalFromNat n) bs) start is_inc
+     Bitvector (rotateLeft n bs) start is_inc
   end
 
 let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*)
 let bitwise_rightshift = shift_op_vec RR_shift (*">>"*)
 let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*)
 
+let shiftl = bitwise_leftshift
+
 let rec arith_op_no0 (op : integer -> integer -> integer) l r =
   if r = 0
   then Nothing
@@ -681,19 +730,19 @@ let rec repeat xs n =
   if n = 0 then []
   else xs ++ repeat xs (n-1)
 
-(*
-let duplicate bit length =
-  Vector (repeat [bit] length) (if dir then 0 else length - 1) dir
- *)
 
-let compare_op op (l,r) = bool_to_bitU (op l r)
+let duplicate (bit, length) =
+  vec_to_bvec (Vector (repeat [bit] length) (length - 1) false)
+
+let duplicate_to_list (bit, length) = repeat [bit] length
+
+let compare_op op (l,r) = (op l r)
 
 let lt = compare_op (<)
 let gt = compare_op (>)
 let lteq = compare_op (<=)
 let gteq = compare_op (>=)
 
-
 let compare_op_vec op sign (l,r) =
   let (l',r') = (to_num sign l, to_num sign r) in
   compare_op op (l',r')
@@ -712,6 +761,8 @@ let gt_vec_unsigned = compare_op_vec (>) false
 let lteq_vec_unsigned = compare_op_vec (<=) false
 let gteq_vec_unsigned = compare_op_vec (>=) false
 
+let lt_svec = lt_vec_signed
+
 let compare_op_vec_range op sign (l,r) =
   compare_op op ((to_num sign l),r)
 
@@ -728,20 +779,23 @@ let gt_range_vec = compare_op_range_vec (>) true
 let lteq_range_vec = compare_op_range_vec (<=) true
 let gteq_range_vec = compare_op_range_vec (>=) true
 
-let eq (l,r) = bool_to_bitU (l = r)
-let eq_range (l,r) = bool_to_bitU (l = r)
-let eq_vec (l,r) = bool_to_bitU (l = r)
-let eq_bit (l,r) = bool_to_bitU (l = r)
+val eq : forall 'a. Eq 'a => 'a * 'a -> bool
+let eq (l,r) = (l = r)
+let eq_range (l,r) = (l = r)
+
+val eq_vec : forall 'a. bitvector 'a * bitvector 'a -> bool
+let eq_vec (l,r) = (l = r)
+let eq_bit (l,r) = (l = r)
 let eq_vec_range (l,r) = eq (to_num false l,r)
 let eq_range_vec (l,r) = eq (l, to_num false r)
 let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
 
-let neq (l,r) = bitwise_not_bit (eq (l,r))
-let neq_bit (l,r) = bitwise_not_bit (eq_bit (l,r))
-let neq_range (l,r) = bitwise_not_bit (eq_range (l,r))
-let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r))
-let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r))
-let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r))
+let neq (l,r) = not (eq (l,r))
+let neq_bit (l,r) = not (eq_bit (l,r))
+let neq_range (l,r) = not (eq_range (l,r))
+let neq_vec (l,r) = not (eq_vec_vec (l,r))
+let neq_vec_range (l,r) = not (eq_vec_range (l,r))
+let neq_range_vec (l,r) = not (eq_range_vec (l,r))
 
 
 val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
@@ -757,9 +811,9 @@ let make_bitvector_undef length =
 
 (* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
 
-let mask (n,bv) =
-  let len = bvlength bv in
-  bvslice_raw bv (len - n) (len - 1)
+(* TODO *)
+val mask : forall 'a 'b. Size 'b => bitvector 'a -> bitvector 'b
+let mask (Bitvector w i dir) = (Bitvector (zeroExtend w) i dir)
 
 
 val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
@@ -974,7 +1028,7 @@ let assert' b msg_opt =
   | Just msg -> msg
   | Nothing  -> "unspecified error"
   end in
-  if bitU_to_bool b then () else failwith msg
+  if b then () else failwith msg
 
 (* convert numbers unsafely to naturals *)
 
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 709052fe..2e11e8a9 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -14,12 +14,28 @@ type sequential_state = <| regstate : regstate;
                            write_ea : maybe (write_kind * integer * integer);
                            last_exclusive_operation_was_load : bool|>
 
-type M 'a = sequential_state -> list ((either 'a string) * sequential_state)
+(* State, nondeterminism and exception monad with result type 'a
+   and exception type 'e. *)
+type ME 'a 'e = sequential_state -> list ((either 'a 'e) * sequential_state)
 
-val return : forall 'a. 'a -> M 'a
+(* Most of the time, we don't distinguish between different types of exceptions *)
+type M 'a = ME 'a unit
+
+(* For early return, we abuse exceptions by throwing and catching
+   the return value. The exception type is "maybe 'r", where "Nothing"
+   represents a proper exception and "Just r" an early return of value "r". *)
+type MR 'a 'r = ME 'a (maybe 'r)
+
+val liftR : forall 'a 'r. M 'a -> MR 'a 'r
+let liftR m s = List.map (function
+  | (Left a, s') -> (Left a, s')
+  | (Right (), s') -> (Right Nothing, s')
+  end) (m s)
+
+val return : forall 'a 'e. 'a -> ME 'a 'e
 let return a s = [(Left a,s)]
 
-val bind : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b
+val bind : forall 'a 'b 'e. ME 'a 'e -> ('a -> ME 'b 'e) -> ME 'b 'e
 let bind m f (s : sequential_state) =
   List.concatMap (function
                   | (Left a, s') -> f a s'
@@ -27,12 +43,23 @@ let bind m f (s : sequential_state) =
                   end) (m s)
 
 let inline (>>=) = bind
-val (>>): forall 'b. M unit -> M 'b -> M 'b
+val (>>): forall 'b 'e. ME unit 'e -> ME 'b 'e -> ME 'b 'e
 let inline (>>) m n = m >>= fun _ -> n
 
 val exit : forall 'e 'a. 'e -> M 'a
-let exit _ s = [(Right "exit",s)]
+let exit _ s = [(Right (), s)]
 
+val early_return : forall 'r. 'r -> MR unit 'r
+let early_return r s = [(Right (Just r), s)]
+
+val catch_early_return : forall 'a 'r. MR 'a 'a -> M 'a
+let catch_early_return m s =
+  List.map
+    (function
+     | (Right (Just a), s') -> (Left a, s')
+     | (Right Nothing, s') -> (Right (), s')
+     | (Left a, s') -> (Left a, s')
+    end) (m s)
 
 val range : integer -> integer -> list integer
 let rec range i j = 
@@ -126,7 +153,7 @@ val read_reg : forall 'a. Size 'a => register -> M (bitvector 'a)
 let read_reg reg state =
   let v = get_reg state (name_of_reg reg) in
   [(Left (vec_to_bvec v),state)]
-let read_reg_range reg i j state =
+(*let read_reg_range reg i j state =
   let v = slice (get_reg state (name_of_reg reg)) i j in
   [(Left (vec_to_bvec v),state)]
 let read_reg_bit reg i state =
@@ -137,7 +164,9 @@ let read_reg_field reg regfield =
   read_reg_range reg i j
 let read_reg_bitfield reg regfield =
   let (i,_) = register_field_indices reg regfield in
-  read_reg_bit reg i 
+  read_reg_bit reg i *)
+
+let reg_deref = read_reg
 
 val write_reg : forall 'a. Size 'a => register -> bitvector 'a -> M unit
 let write_reg reg v state =
@@ -172,8 +201,8 @@ val footprint : M unit
 let footprint = return ()
 
 
-val foreachM_inc : forall 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'vars) -> M 'vars
+val foreachM_inc : forall 'vars 'e. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> ME 'vars 'e) -> ME 'vars 'e
 let rec foreachM_inc (i,stop,by) vars body =
   if i <= stop
   then
@@ -182,8 +211,8 @@ let rec foreachM_inc (i,stop,by) vars body =
   else return vars
 
 
-val foreachM_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'vars) -> M 'vars
+val foreachM_dec : forall 'vars 'e. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> ME 'vars 'e) -> ME 'vars 'e
 let rec foreachM_dec (i,stop,by) vars body =
   if i >= stop
   then
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 63be60b2..27b5237e 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -411,6 +411,91 @@ let remove_bound env pat =
   let bound = bindings_from_pat pat in
   List.fold_left (fun sub v -> ISubst.remove v env) env bound
 
+(* Remove explicit existential types from the AST, so that the sizes of
+   bitvectors will be filled in throughout.
+
+   Problems: there might be other existential types that we want to keep (e.g.
+   because they describe conditions needed for a vector index to be in range),
+   and inference might not be able to find a sufficiently precise type. *)
+let rec deexist_exp (E_aux (e,(l,(annot : Type_check.tannot))) as exp) =
+  let re e = E_aux (e,(l,annot)) in
+  match e with
+  | E_block es -> re (E_block (List.map deexist_exp es))
+  | E_nondet es -> re (E_nondet (List.map deexist_exp es))
+  | E_id _
+  | E_lit _
+  | E_sizeof _
+  | E_constraint _
+    -> (*Type_check.strip_exp*) exp
+  | E_cast (Typ_aux (Typ_exist (kids, nc, ty),l),(E_aux (_,(l',annot')) as e)) ->
+(*     let env,_ = env_typ_expected l' annot' in
+     let plain_e = deexist_exp e in
+     let E_aux (_,(_,annot'')) = Type_check.infer_exp env plain_e in
+*)
+     deexist_exp e
+  | E_cast (ty,e) -> re (E_cast (ty,deexist_exp e))
+  | E_app (id,args) -> re (E_app (id,List.map deexist_exp args))
+  | E_app_infix (e1,id,e2) -> re (E_app_infix (deexist_exp e1,id,deexist_exp e2))
+  | E_tuple es -> re (E_tuple (List.map deexist_exp es))
+  | E_if (e1,e2,e3) -> re (E_if (deexist_exp e1,deexist_exp e2,deexist_exp e3))
+  | E_for (id,e1,e2,e3,ord,e4) ->
+     re (E_for (id,deexist_exp e1,deexist_exp e2,deexist_exp e3,ord,deexist_exp e4))
+  | E_vector es -> re (E_vector (List.map deexist_exp es))
+  | E_vector_indexed (ies,def) ->
+     re (E_vector_indexed
+           (List.map (fun (i,e) -> (i,deexist_exp e)) ies,
+            match def with
+            | Def_val_aux (Def_val_empty,(l,ann)) -> Def_val_aux (Def_val_empty,(l,ann))
+            | Def_val_aux (Def_val_dec e,(l,ann)) -> Def_val_aux (Def_val_dec (deexist_exp e),(l,ann))))
+  | E_vector_access (e1,e2) -> re (E_vector_access (deexist_exp e1,deexist_exp e2))
+  | E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (deexist_exp e1,deexist_exp e2,deexist_exp e3))
+  | E_vector_update (e1,e2,e3) -> re (E_vector_update (deexist_exp e1,deexist_exp e2,deexist_exp e3))
+  | E_vector_update_subrange (e1,e2,e3,e4) ->
+     re (E_vector_update_subrange (deexist_exp e1,deexist_exp e2,deexist_exp e3,deexist_exp e4))
+  | E_vector_append (e1,e2) -> re (E_vector_append (deexist_exp e1,deexist_exp e2))
+  | E_list es -> re (E_list (List.map deexist_exp es))
+  | E_cons (e1,e2) -> re (E_cons (deexist_exp e1,deexist_exp e2))
+  | E_record _ -> (*Type_check.strip_exp*) exp (* TODO *)
+  | E_record_update  _ -> (*Type_check.strip_exp*) exp (* TODO *)
+  | E_field (e1,fld) -> re (E_field (deexist_exp e1,fld))
+  | E_case (e1,cases) -> re (E_case (deexist_exp e1, List.map deexist_pexp cases))
+  | E_let (lb,e1) -> re (E_let (deexist_letbind lb, deexist_exp e1))
+  | E_assign (le,e1) -> re (E_assign (deexist_lexp le, deexist_exp e1))
+  | E_exit e1 -> re (E_exit (deexist_exp e1))
+  | E_return e1 -> re (E_return (deexist_exp e1))
+  | E_assert (e1,e2) -> re (E_assert (deexist_exp e1,deexist_exp e2))
+and deexist_pexp (Pat_aux (pe,(l,annot))) =
+  match pe with
+  | Pat_exp (p,e) -> Pat_aux (Pat_exp ((*Type_check.strip_pat*) p,deexist_exp e),(l,annot))
+  | Pat_when (p,e1,e2) -> Pat_aux (Pat_when ((*Type_check.strip_pat*) p,deexist_exp e1,deexist_exp e2),(l,annot))
+and deexist_letbind (LB_aux (lb,(l,annot))) =
+  match lb with (* TODO, drop tysc if there's an exist? Do they even appear here? *)
+  | LB_val_explicit (tysc,p,e) -> LB_aux (LB_val_explicit (tysc,(*Type_check.strip_pat*) p,deexist_exp e),(l,annot))
+  | LB_val_implicit (p,e) -> LB_aux (LB_val_implicit ((*Type_check.strip_pat*) p,deexist_exp e),(l,annot))
+and deexist_lexp (LEXP_aux (le,(l,annot))) =
+  let re le = LEXP_aux (le,(l,annot)) in
+  match le with
+  | LEXP_id id -> re (LEXP_id id)
+  | LEXP_memory (id,es) -> re (LEXP_memory (id,List.map deexist_exp es))
+  | LEXP_cast (Typ_aux (Typ_exist _,_),id) -> re (LEXP_id id)
+  | LEXP_cast (ty,id) -> re (LEXP_cast (ty,id))
+  | LEXP_tup lexps -> re (LEXP_tup (List.map deexist_lexp lexps))
+  | LEXP_vector (le,e) -> re (LEXP_vector (deexist_lexp le, deexist_exp e))
+  | LEXP_vector_range (le,e1,e2) -> re (LEXP_vector_range (deexist_lexp le, deexist_exp e1, deexist_exp e2))
+  | LEXP_field (le,id) -> re (LEXP_field (deexist_lexp le, id))
+
+let deexist_funcl (FCL_aux (FCL_Funcl (id,p,e),(l,annot))) =
+  FCL_aux (FCL_Funcl (id, (*Type_check.strip_pat*) p, deexist_exp e),(l,annot))
+
+let deexist_def = function
+  | DEF_kind kd -> DEF_kind kd
+  | DEF_type td -> DEF_type td
+  | DEF_fundef (FD_aux (FD_function (recopt,topt,effopt,fcls),(l,annot))) ->
+     DEF_fundef (FD_aux (FD_function (recopt,topt,effopt,List.map deexist_funcl fcls),(l,annot)))
+  | x -> x
+
+let deexist (Defs defs) = Defs (List.map deexist_def defs)
+
 
 (* Attempt simple pattern matches *)
 let lit_match = function
@@ -1056,5 +1141,5 @@ let split_defs splits defs =
     in
     Defs (List.concat (List.map map_def defs))
   in
-  map_locs splits defs'
+  deexist (map_locs splits defs')
 
diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml
index 765553d3..697ee9bd 100644
--- a/src/myocamlbuild.ml
+++ b/src/myocamlbuild.ml
@@ -101,5 +101,11 @@ dispatch begin function
         mv (basename (env "%.lem")) (dirname (env "%.lem"))
       ]);
 
+    rule "old parser"
+    ~insert:(`top)
+    ~prods: ["parser.ml"; "parser.mli"]
+    ~dep: "parser.mly"
+    (fun env builder -> Cmd(S[V"OCAMLYACC"; T(tags_of_pathname "parser.mly"++"ocaml"++"parser"++"ocamlyacc"); Px "parser.mly"]));
+
 | _ -> ()
 end ;;
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 57a06e74..bd43c1a7 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -46,6 +46,7 @@ open PPrint
 let pipe = string "|"
 let arrow = string "->"
 let dotdot = string ".."
+let coloncolon = string "::"
 let coloneq = string ":="
 let lsquarebar = string "[|"
 let rsquarebar = string "|]"
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 2619cc51..586773ca 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -160,7 +160,7 @@ let doc_typ_lem, doc_atomic_typ_lem =
          let tpp = separate_map (space ^^ star ^^ space) (app_typ regtypes false) typs in
          if atyp_needed then parens tpp else tpp
       | _ -> app_typ regtypes atyp_needed ty
-    and app_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+    and app_typ regtypes atyp_needed ((Typ_aux (t, l)) as ty) = match t with
       | Typ_app(Id_aux (Id "vector", _), [
           Typ_arg_aux (Typ_arg_nexp n, _);
           Typ_arg_aux (Typ_arg_nexp m, _);
@@ -168,19 +168,17 @@ let doc_typ_lem, doc_atomic_typ_lem =
           Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
          let tpp = match elem_typ with
            | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) ->
-               let len = match m with
-                 | (Nexp_aux(Nexp_constant i,_)) -> string "ty" ^^ doc_int i
-                 | _ -> doc_nexp m in
-               string "bitvector" ^^ space ^^ len
+             (match simplify_nexp m with
+               | (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i
+               | (Nexp_aux(Nexp_var _, _)) -> separate space [string "bitvector"; doc_nexp m]
+               | _ -> raise (Reporting_basic.err_unreachable l
+                 "cannot pretty-print bitvector type with non-constant length"))
            | _ -> string "vector" ^^ space ^^ typ regtypes elem_typ in
          if atyp_needed then parens tpp else tpp
       | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
-         (* TODO: Better distinguish register names and contents?
-            The former are represented in the Lem library using a type
-            "register" (without parameters), the latter just using the content
-            type (e.g. "bitvector ty64").  We assume the latter is meant here
-            and drop the "register" keyword. *)
-         fn_typ regtypes atyp_needed etyp
+         (* TODO: Better distinguish register names and contents? *)
+         (* fn_typ regtypes atyp_needed etyp *)
+         (string "register")
       | Typ_app(Id_aux (Id "range", _),_) ->
          (string "integer")
       | Typ_app(Id_aux (Id "implicit", _),_) ->
@@ -192,13 +190,13 @@ let doc_typ_lem, doc_atomic_typ_lem =
          if atyp_needed then parens tpp else tpp
       | _ -> atomic_typ regtypes atyp_needed ty
     and atomic_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
-      | Typ_id (Id_aux (Id "bool",_)) -> string "bitU"
-      | Typ_id (Id_aux (Id "boolean",_)) -> string "bitU"
+      | Typ_id (Id_aux (Id "bool",_)) -> string "bool"
+      | Typ_id (Id_aux (Id "boolean",_)) -> string "bool"
       | Typ_id (Id_aux (Id "bit",_)) -> string "bitU"
       | Typ_id (id) ->
-         if List.exists ((=) (string_of_id id)) regtypes
+         (*if List.exists ((=) (string_of_id id)) regtypes
          then string "register"
-         else doc_id_lem_type id
+         else*) doc_id_lem_type id
       | Typ_var v -> doc_var v
       | Typ_wild -> underscore
       | Typ_app _ | Typ_tup _ | Typ_fn _ ->
@@ -213,46 +211,86 @@ let doc_typ_lem, doc_atomic_typ_lem =
       | Typ_arg_effect e -> empty
   in typ', atomic_typ
 
+(* Check for variables in types that would be pretty-printed.
+   In particular, in case of vector types, only the element type and the
+   length argument are checked for variables, and the latter only if it is
+   a bitvector; for other types of vectors, the length is not pretty-printed
+   in the type, and the start index is never pretty-printed in vector types. *)
+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_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) ->
+      if Ast_util.is_number typ then false
+      else if is_bitvector_typ typ then
+        let (_,length,_,_) = vector_typ_args_of typ in
+        not (is_nexp_constant (simplify_nexp length))
+      else List.exists contains_t_arg_pp_var targs
+and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with
+  | Typ_arg_typ t -> contains_t_pp_var t
+  | Typ_arg_nexp nexp -> not (is_nexp_constant (simplify_nexp nexp))
+  | _ -> false
+
 let doc_tannot_lem regtypes eff typ =
-  let ta = doc_typ_lem regtypes typ in
-  if eff then string " : M " ^^ parens ta
-  else string " : " ^^ ta
+  if contains_t_pp_var typ then empty
+  else
+    let ta = doc_typ_lem regtypes typ in
+    if eff then string " : M " ^^ parens ta
+    else string " : " ^^ ta
 
 (* doc_lit_lem gets as an additional parameter the type information from the
  * expression around it: that's a hack, but how else can we distinguish between
  * undefined values of different types ? *)
-let doc_lit_lem in_pat (L_aux(lit,l)) a =
-  utf8string (match lit with
-  | L_unit  -> "()"
-  | L_zero  -> "B0"
-  | L_one   -> "B1"
-  | L_false -> "B0"
-  | L_true  -> "B1"
+let doc_lit_lem regtypes in_pat (L_aux(lit,l)) a =
+  match lit with
+  | L_unit  -> utf8string "()"
+  | L_zero  -> utf8string "B0"
+  | L_one   -> utf8string "B1"
+  | L_false -> utf8string "false"
+  | L_true  -> utf8string "true"
   | L_num i ->
      let ipp = string_of_int i in
-     if in_pat then "("^ipp^":nn)"
-     else if i < 0 then "((0"^ipp^"):ii)"
-     else "("^ipp^":ii)"
+     utf8string (
+       if in_pat then "("^ipp^":nn)"
+       else if i < 0 then "((0"^ipp^"):ii)"
+       else "("^ipp^":ii)")
   | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_undef ->
      (match a with
-       | Some (_, Typ_aux (t,_), _) ->
+       | Some (_, (Typ_aux (t,_) as typ), _) ->
          (match t with
           | Typ_id (Id_aux (Id "bit", _))
-          | Typ_app (Id_aux (Id "register", _),_) -> "UndefinedRegister 0"
-          | Typ_id (Id_aux (Id "string", _)) -> "\"\""
-          | _ -> "(failwith \"undefined value of unsupported type\")")
-       | _ -> "(failwith \"undefined value of unsupported type\")")
-  | L_string s -> "\"" ^ s ^ "\""
-  | L_real s -> s (* TODO What's the Lem syntax for reals? *))
+          | Typ_app (Id_aux (Id "register", _),_) -> utf8string "UndefinedRegister 0"
+          | Typ_id (Id_aux (Id "string", _)) -> utf8string "\"\""
+          | _ ->
+            parens
+              ((utf8string "(failwith \"undefined value of unsupported type\")") ^^
+              (doc_tannot_lem regtypes false typ)))
+       | _ -> utf8string "(failwith \"undefined value of unsupported type\")")
+  | L_string s -> utf8string ("\"" ^ s ^ "\"")
+  | L_real s -> utf8string s (* TODO What's the Lem syntax for reals? *)
 
 (* typ_doc is the doc for the type being quantified *)
+let doc_quant_item (QI_aux (qi, _)) = match qi with
+| QI_id (KOpt_aux (KOpt_none kid, _))
+| QI_id (KOpt_aux (KOpt_kind (_, kid), _)) -> doc_var kid
+| _ -> empty
 
-let doc_typquant_lem (TypQ_aux(tq,_)) typ_doc = typ_doc
+let doc_typquant_items_lem (TypQ_aux(tq,_)) = match tq with
+| TypQ_tq qs -> separate_map space doc_quant_item qs
+| _ -> empty
 
-let doc_typschm_lem regtypes (TypSchm_aux(TypSchm_ts(tq,t),_)) =
-  (doc_typquant_lem tq (doc_typ_lem regtypes t))
+let doc_typquant_lem (TypQ_aux(tq,_)) typ = match tq with
+| TypQ_tq ((_ :: _) as qs) ->
+  string "forall " ^^ separate_map space doc_quant_item qs ^^ string ". " ^^ typ
+| _ -> empty
+
+let doc_typschm_lem regtypes quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
+  if quants then (doc_typquant_lem tq (doc_typ_lem regtypes t))
+  else doc_typ_lem regtypes t
 
 let is_ctor env id = match Env.lookup_id id env with
 | Enum _ | Union _ -> true
@@ -267,14 +305,17 @@ let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p w
                        (parens (separate_map comma (doc_pat_lem regtypes true) pats)) in
     if apat_needed then parens ppp else ppp
   | P_app(id,[]) -> doc_id_lem_ctor id
-  | P_lit lit  -> doc_lit_lem true lit annot
+  | P_lit lit  -> doc_lit_lem regtypes true lit annot
   | P_wild -> underscore
   | P_id id ->
      begin match id with
      | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
      | _ -> doc_id_lem id end
   | P_as(p,id) -> parens (separate space [doc_pat_lem regtypes true p; string "as"; doc_id_lem id])
-  | P_typ(typ,p) -> parens (doc_op colon (doc_pat_lem regtypes true p) (doc_typ_lem regtypes typ))
+  | P_typ(typ,p) ->
+    let doc_p = doc_pat_lem regtypes true p in
+    if contains_t_pp_var typ then doc_p
+    else parens (doc_op colon doc_p (doc_typ_lem regtypes typ))
   | P_vector pats ->
      let ppp =
        (separate space)
@@ -300,38 +341,23 @@ and contains_bitvector_typ_arg (Typ_arg_aux (targ, _)) = match targ with
   | Typ_arg_typ t -> contains_bitvector_typ t
   | _ -> false
 
-let const_nexp (Nexp_aux (nexp,_)) = match nexp with
-  | Nexp_constant _ -> true
-  | _ -> false
-
-(* Check for variables in types that would be pretty-printed.
-   In particular, in case of vector types, only the element type and the
-   length argument are checked for variables, and the latter only if it is
-   a bitvector; for other types of vectors, the length is not pretty-printed
-   in the type, and the start index is never pretty-printed in vector types. *)
-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_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) ->
-      if is_bitvector_typ typ then
-        let (_,length,_,_) = vector_typ_args_of typ in
-        not (const_nexp ((*normalize_nexp*) length))
-      else List.exists contains_t_arg_pp_var targs
-and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with
-  | Typ_arg_typ t -> contains_t_pp_var t
-  | Typ_arg_nexp nexp -> not (const_nexp ((*normalize_nexp*) nexp))
-  | _ -> false
+let contains_early_return exp =
+  fst (fold_exp
+  { (Rewriter.compute_exp_alg false (||))
+    with e_return = (fun (_, r) -> (true, E_return r)) } exp)
 
 let prefix_recordtype = true
 let report = Reporting_basic.err_unreachable
 let doc_exp_lem, doc_let_lem =
-  let rec top_exp regtypes (aexp_needed : bool) (E_aux (e, (l,annot)) as full_exp) =
-    let expY = top_exp regtypes true in
-    let expN = top_exp regtypes false in
-    let expV = top_exp regtypes in
+  let rec top_exp regtypes (early_ret : bool) (aexp_needed : bool)
+    (E_aux (e, (l,annot)) as full_exp) =
+    let expY = top_exp regtypes early_ret true in
+    let expN = top_exp regtypes early_ret false in
+    let expV = top_exp regtypes early_ret in
+    let liftR doc =
+      if early_ret && effectful (effect_of full_exp)
+      then separate space [string "liftR"; parens (doc)]
+      else doc in
     match e with
     | E_assign((LEXP_aux(le_act,tannot) as le), e) ->
        (* can only be register writes *)
@@ -343,14 +369,14 @@ let doc_exp_lem, doc_let_lem =
                if is_bit_typ (typ_of_annot lannot) then
                  raise (report l "indexing a register's (single bit) bitfield not supported")
                else
-                 (prefix 2 1)
+                 liftR ((prefix 2 1)
                    (string "write_reg_field_range")
-                   (align (doc_lexp_deref_lem regtypes le ^^ space^^
-                             string_lit (doc_id_lem id) ^/^ expY e2 ^/^ expY e3 ^/^ expY e))
+                   (align (doc_lexp_deref_lem regtypes early_ret le ^^ space^^
+                             string_lit (doc_id_lem id) ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
             | _ ->
-               (prefix 2 1)
+               liftR ((prefix 2 1)
                  (string "write_reg_range")
-                 (align (doc_lexp_deref_lem regtypes le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e))
+                 (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e)))
            )
         | LEXP_vector (le,e2) when is_bit_typ t ->
            (match le with
@@ -358,23 +384,23 @@ let doc_exp_lem, doc_let_lem =
                if is_bit_typ (typ_of_annot lannot) then
                  raise (report l "indexing a register's (single bit) bitfield not supported")
                else
-                 (prefix 2 1)
+                 liftR ((prefix 2 1)
                    (string "write_reg_field_bit")
-                   (align (doc_lexp_deref_lem regtypes le ^^ space ^^ doc_id_lem id ^/^ expY e2 ^/^ expY e))
+                   (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ doc_id_lem id ^/^ expY e2 ^/^ expY e)))
             | _ ->
-               (prefix 2 1)
+               liftR ((prefix 2 1)
                  (string "write_reg_bit")
-                 (doc_lexp_deref_lem regtypes le ^^ space ^^ expY e2 ^/^ expY e)
+                 (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ expY e2 ^/^ expY e))
            )
         | LEXP_field (le,id) when is_bit_typ t ->
-           (prefix 2 1)
+           liftR ((prefix 2 1)
              (string "write_reg_bitfield")
-             (doc_lexp_deref_lem regtypes le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)
+             (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e))
         | LEXP_field (le,id) ->
-           (prefix 2 1)
+           liftR ((prefix 2 1)
              (string "write_reg_field")
-             (doc_lexp_deref_lem regtypes le ^^ space ^^
-                string_lit(doc_id_lem id) ^/^ expY e)
+             (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^
+                string_lit(doc_id_lem id) ^/^ expY e))
         (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info ->
            (match alias_info with
             | Alias_field(reg,field) ->
@@ -389,9 +415,11 @@ let doc_exp_lem, doc_let_lem =
                string "write_two_regs" ^^ space ^^ string reg1 ^^ space ^^
                  string reg2 ^^ space ^^ expY e) *)
         | _ ->
-           (prefix 2 1) (string "write_reg") (doc_lexp_deref_lem regtypes le ^/^ expY e))
+           liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem regtypes early_ret le ^/^ expY e)))
     | E_vector_append(le,re) ->
-       let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
+      raise (Reporting_basic.err_unreachable l
+        "E_vector_access should have been rewritten before pretty-printing")
+       (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let (call,ta,aexp_needed) =
          if is_bitvector_typ t then
            if not (contains_t_pp_var t)
@@ -400,12 +428,12 @@ let doc_exp_lem, doc_let_lem =
          else ("vector_concat",empty,aexp_needed) in
        let epp =
          align (group (separate space [string call;expY le;expY re])) ^^ ta in
-       if aexp_needed then parens epp else epp
+       if aexp_needed then parens epp else epp *)
     | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re)
     | E_if(c,t,e) ->
        let (E_aux (_,(_,cannot))) = c in
        let epp =
-         separate space [string "if";group (align (string "bitU_to_bool" ^//^ group (expY c)))] ^^
+         separate space [string "if";group (expY c)] ^^
            break 1 ^^
              (prefix 2 1 (string "then") (expN t)) ^^ (break 1) ^^
                (prefix 2 1 (string "else") (expN e)) in
@@ -413,7 +441,7 @@ let doc_exp_lem, doc_let_lem =
     | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
        raise (report l "E_for should have been removed till now")
     | E_let(leb,e) ->
-       let epp = let_exp regtypes leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
+       let epp = let_exp regtypes early_ret leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
        if aexp_needed then parens epp else epp
     | E_app(f,args) ->
        begin match f with
@@ -438,7 +466,7 @@ let doc_exp_lem, doc_let_lem =
                    (prefix 1 1 (separate space [string "fun";expY id;varspp;arrow]) (expN body))
                 )
             )
-       | Id_aux (Id "append",_) ->
+       (* | Id_aux (Id "append",_) ->
           let [e1;e2] = args in
           let epp = align (expY e1 ^^ space ^^ string "++" ^//^ expY e2) in
           if aexp_needed then parens (align epp) else epp
@@ -464,7 +492,7 @@ let doc_exp_lem, doc_let_lem =
        | Id_aux (Id "bool_not", _) ->
           let [a] = args in
           let epp = align (string "~" ^^ expY a) in
-          if aexp_needed then parens (align epp) else epp
+          if aexp_needed then parens (align epp) else epp *)
        | _ ->
           begin match annot with
           | Some (env, _, _) when (is_ctor env f) ->
@@ -477,24 +505,28 @@ let doc_exp_lem, doc_let_lem =
                     parens (separate_map comma (expV false) args) in
              if aexp_needed then parens (align epp) else epp
           | _ ->
-             let call = (*match annot with
-               | Base(_,External (Some n),_,_,_,_) -> string n
-               | _ ->*) doc_id_lem f in
+             let call = match annot with
+               | Some (env, _, _) when Env.is_extern f env ->
+                 string (Env.get_extern f env)
+               | _ -> doc_id_lem f in
              let argspp = match args with
                | [arg] -> expV true arg
                | args -> parens (align (separate_map (comma ^^ break 0) (expV false) args)) in
              let epp = align (call ^//^ argspp) in
              let (taepp,aexp_needed) =
-               let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
+               let t = (*Env.base_typ_of (env_of full_exp)*) (typ_of full_exp) in
                let eff = effect_of full_exp in
-               if contains_bitvector_typ t && not (contains_t_pp_var t)
+               if contains_bitvector_typ (Env.base_typ_of (env_of full_exp) t) &&
+                  not (contains_t_pp_var t)
                then (align epp ^^ (doc_tannot_lem regtypes (effectful eff) t), true)
                else (epp, aexp_needed) in
-             if aexp_needed then parens (align taepp) else taepp
+             liftR (if aexp_needed then parens (align taepp) else taepp)
           end
        end
     | E_vector_access (v,e) ->
-       let eff = effect_of full_exp in
+      raise (Reporting_basic.err_unreachable l
+        "E_vector_access should have been rewritten before pretty-printing")
+       (* let eff = effect_of full_exp in
        let epp =
          if has_effect eff BE_rreg then
            separate space [string "read_reg_bit";expY v;expY e]
@@ -502,9 +534,11 @@ let doc_exp_lem, doc_let_lem =
            let tv = typ_of v in
            let call = if is_bitvector_typ tv then "bvaccess" else "access" in
            separate space [string call;expY v;expY e] in
-       if aexp_needed then parens (align epp) else epp
+       if aexp_needed then parens (align epp) else epp*)
     | E_vector_subrange (v,e1,e2) ->
-       let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
+      raise (Reporting_basic.err_unreachable l
+        "E_vector_access should have been rewritten before pretty-printing")
+       (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let eff = effect_of full_exp in
        let (epp,aexp_needed) =
          if has_effect eff BE_rreg then
@@ -519,22 +553,22 @@ let doc_exp_lem, doc_let_lem =
              then (bepp ^^ doc_tannot_lem regtypes false t, true)
              else (bepp, aexp_needed)
            else (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2, aexp_needed) in
-       if aexp_needed then parens (align epp) else epp
+       if aexp_needed then parens (align epp) else epp *)
     | E_field((E_aux(_,(l,fannot)) as fexp),id) ->
        let ft = typ_of_annot (l,fannot) in
        (match fannot with
-        | Some(env, ftyp, _) when is_regtyp ftyp env ->
-           let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
+        | Some(env, (Typ_aux (Typ_id tid, _)), _)
+        | Some(env, (Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]), _)), _)
+          when Env.is_regtyp tid env ->
+           let t = (* Env.base_typ_of (env_of full_exp) *) (typ_of full_exp) in
            let eff = effect_of full_exp in
-           let field_f = string
-             (if is_bit_typ t
-             then "read_reg_bitfield"
-             else "read_reg_field") in
+           let field_f = string "get" ^^ underscore ^^
+             doc_id_lem tid ^^ underscore ^^ doc_id_lem id in
            let (ta,aexp_needed) =
              if contains_bitvector_typ t && not (contains_t_pp_var t)
              then (doc_tannot_lem regtypes (effectful eff) t, true)
              else (empty, aexp_needed) in
-           let epp = field_f ^^ space ^^ (expY fexp) ^^ space ^^ string_lit (doc_id_lem id) in
+           let epp = field_f ^^ space ^^ (expY fexp) in
            if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta)
         | Some(env, (Typ_aux (Typ_id tid, _)), _) when Env.is_record tid env ->
            let fname =
@@ -554,9 +588,9 @@ let doc_exp_lem, doc_let_lem =
        let base_typ = Env.base_typ_of env typ in
        if has_effect eff BE_rreg then
          let epp = separate space [string "read_reg";doc_id_lem id] in
-         if contains_bitvector_typ base_typ && not (contains_t_pp_var base_typ)
-         then parens (epp ^^ doc_tannot_lem regtypes true base_typ)
-         else epp
+         if is_bitvector_typ base_typ && not (contains_t_pp_var base_typ)
+         then liftR (parens (epp ^^ doc_tannot_lem regtypes true base_typ))
+         else liftR epp
        else if is_ctor env id then doc_id_lem_ctor id
        else doc_id_lem id
         (*| Base((_,t),Alias alias_info,_,eff,_,_) ->
@@ -592,7 +626,7 @@ let doc_exp_lem, doc_let_lem =
                     separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in
                 if aexp_needed then parens (align epp) else epp
            )*)
-    | E_lit lit -> doc_lit_lem false lit annot
+    | E_lit lit -> doc_lit_lem regtypes false lit annot
     | E_cast(typ,e) ->
        expV aexp_needed e (*
        (match annot with
@@ -633,14 +667,14 @@ let doc_exp_lem, doc_let_lem =
          | _ ->  raise (report l "cannot get record type") in
        let epp = anglebars (space ^^ (align (separate_map
                                           (semi_sp ^^ break 1)
-                                          (doc_fexp regtypes recordtyp) fexps)) ^^ space) in
+                                          (doc_fexp regtypes early_ret recordtyp) fexps)) ^^ space) in
        if aexp_needed then parens epp else epp
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
        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
-       anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp regtypes recordtyp) fexps))
+       anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp regtypes early_ret recordtyp) fexps))
     | E_vector exps ->
        let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let (start, len, order, etyp) =
@@ -653,7 +687,7 @@ let doc_exp_lem, doc_let_lem =
            | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])
              | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])}) ->*)
               let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
-              let start = match start with
+              let start = match simplify_nexp start with
                 | Nexp_aux (Nexp_constant i, _) -> string_of_int i
                 | _ -> if dir then "0" else string_of_int (List.length exps) in
               let expspp =
@@ -685,10 +719,10 @@ let doc_exp_lem, doc_let_lem =
         if is_vector_typ t then vector_typ_args_of t
         else raise (Reporting_basic.err_unreachable l "E_vector_indexed of non-vector type") in
        let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
-       let start = match start with
+       let start = match simplify_nexp start with
          | Nexp_aux (Nexp_constant i, _) -> string_of_int i
          | _ -> if dir then "0" else string_of_int (List.length iexps) in
-       let size = match len with
+       let size = match simplify_nexp len with
          | Nexp_aux (Nexp_constant i, _)-> string_of_int i
          | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) ->
            string_of_int (Util.power 2 i)
@@ -769,10 +803,10 @@ let doc_exp_lem, doc_let_lem =
         pattern-matching on integers *)
        let epp =
          group ((separate space [string "match"; only_integers e; string "with"]) ^/^
-                  (separate_map (break 1) (doc_case regtypes) pexps) ^/^
+                  (separate_map (break 1) (doc_case regtypes early_ret) pexps) ^/^
                     (string "end")) in
        if aexp_needed then parens (align epp) else align epp
-    | E_exit e -> separate space [string "exit"; expY e;]
+    | 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
@@ -889,46 +923,45 @@ let doc_exp_lem, doc_let_lem =
     | E_internal_return (e1) ->
        separate space [string "return"; expY e1;]
     | E_sizeof nexp ->
-      (match nexp with
-        | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem false (L_aux (L_num i, l)) annot
+      (match simplify_nexp nexp with
+        | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem regtypes false (L_aux (L_num i, l)) annot
         | _ ->
           raise (Reporting_basic.err_unreachable l
             "pretty-printing non-constant sizeof expressions to Lem not supported"))
-    | E_return _ ->
-      raise (Reporting_basic.err_todo l
-        "pretty-printing early return statements to Lem not yet supported")
+    | E_return r ->
+      align (string "early_return" ^//^ expV true r)
     | E_constraint _ | E_comment _ | E_comment_struc _ -> empty
     | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ | E_internal_exp_user _ ->
       raise (Reporting_basic.err_unreachable l
         "unsupported internal expression encountered while pretty-printing")
-  and let_exp regtypes (LB_aux(lb,_)) = match lb with
+  and let_exp regtypes early_ret (LB_aux(lb,_)) = match lb with
     | LB_val_explicit(_,pat,e)
       | LB_val_implicit(pat,e) ->
        prefix 2 1
               (separate space [string "let"; doc_pat_lem regtypes true pat; equals])
-              (top_exp regtypes false e)
+              (top_exp regtypes early_ret false e)
 
-  and doc_fexp regtypes recordtyp (FE_aux(FE_Fexp(id,e),_)) =
+  and doc_fexp regtypes early_ret recordtyp (FE_aux(FE_Fexp(id,e),_)) =
     let fname =
       if prefix_recordtype
       then (string (string_of_id recordtyp ^ "_")) ^^ doc_id_lem id
       else doc_id_lem id in
-    group (doc_op equals fname (top_exp regtypes true e))
+    group (doc_op equals fname (top_exp regtypes early_ret true e))
 
-  and doc_case regtypes = function
+  and doc_case regtypes early_ret = function
   | Pat_aux(Pat_exp(pat,e),_) ->
     group (prefix 3 1 (separate space [pipe; doc_pat_lem regtypes false pat;arrow])
-                  (group (top_exp regtypes false e)))
+                  (group (top_exp regtypes early_ret false e)))
   | Pat_aux(Pat_when(_,_,_),(l,_)) ->
     raise (Reporting_basic.err_unreachable l
       "guarded pattern expression should have been rewritten before pretty-printing")
 
-  and doc_lexp_deref_lem regtypes ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
+  and doc_lexp_deref_lem regtypes early_ret ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
     | LEXP_field (le,id) ->
-       parens (separate empty [doc_lexp_deref_lem regtypes le;dot;doc_id_lem id])
+       parens (separate empty [doc_lexp_deref_lem regtypes early_ret le;dot;doc_id_lem id])
     | LEXP_vector(le,e) ->
-       parens ((separate space) [string "access";doc_lexp_deref_lem regtypes le;
-                                 top_exp regtypes true e])
+       parens ((separate space) [string "access";doc_lexp_deref_lem regtypes early_ret le;
+                                 top_exp regtypes early_ret true e])
     | LEXP_id id -> doc_id_lem id
     | LEXP_cast (typ,id) -> doc_id_lem id
     | _ ->
@@ -947,10 +980,10 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with
   | BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2))
   | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
 
-let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
+let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
   | TD_abbrev(id,nm,typschm) ->
      doc_op equals (concat [string "type"; space; doc_id_lem_type id])
-            (doc_typschm_lem regtypes typschm)
+            (doc_typschm_lem regtypes false typschm)
   | TD_record(id,nm,typq,fs,_) ->
      let f_pp (typ,fid) =
        let fname = if prefix_recordtype
@@ -960,7 +993,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
       let fs_doc = group (separate_map (break 1) f_pp fs) in
       doc_op equals
              (concat [string "type"; space; doc_id_lem_type id;])
-             (doc_typquant_lem typq (anglebars (space ^^ align fs_doc ^^ space)))
+             ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space)))
   | TD_variant(id,nm,typq,ar,_) ->
      (match id with
       | Id_aux ((Id "read_kind"),_) -> empty
@@ -971,13 +1004,14 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
       | Id_aux ((Id "regfp"),_) -> empty
       | Id_aux ((Id "niafp"),_) -> empty
       | Id_aux ((Id "diafp"),_) -> empty
+      | Id_aux ((Id "option"),_) -> empty
       | _ ->
          let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in
          let typ_pp =
 
            (doc_op equals)
-             (concat [string "type"; space; doc_id_lem_type id;])
-             (doc_typquant_lem typq ar_doc) in
+             (concat [string "type"; space; doc_id_lem_type id; space; doc_typquant_items_lem typq])
+             ((*doc_typquant_lem typq*) ar_doc) in
          let make_id pat id =
            separate space [string "SIA.Id_aux";
                            parens (string "SIA.Id " ^^ string_lit (doc_id id));
@@ -1142,7 +1176,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
                 fromToInterpValuePP ^^ hardline
             else empty)
   | TD_register(id,n1,n2,rs) ->
-    match n1,n2 with
+    match n1, n2 with
     | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
        let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id);
                                                        doc_range_lem r;]) in
@@ -1153,25 +1187,64 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
            (string "Register_field" ^^ space ^^ string_lit(doc_id_lem id)) in*)
        let dir_b = i1 < i2 in
        let dir = string (if dir_b then "true" else "false") in
+       let dir_suffix = (if dir_b then "_inc" else "_dec") in
+       let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in
        let size = if dir_b then i2-i1 +1 else i1-i2 + 1 in
-       (doc_op equals)
+       let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in
+       let tannot = doc_tannot_lem regtypes false vtyp in
+       let doc_field (fr, fid) =
+         let i, j = match fr with
+         | BF_aux (BF_single i, _) -> (i, i)
+         | BF_aux (BF_range (i, j), _) -> (i, j)
+         | _ -> raise (Reporting_basic.err_unreachable l "unsupported field type") in
+         let get, set =
+           "bitvector_subrange" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ")",
+           "bitvector_update" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ", v)" in
+         doc_op equals
+           (concat [string "let get_"; doc_id_lem id; underscore; doc_id_lem fid;
+             space; parens (string "reg" ^^ tannot)]) (string get) ^^
+         hardline ^^
+         doc_op equals
+           (concat [string "let set_"; doc_id_lem id; underscore; doc_id_lem fid;
+             space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set)
+       in
+       doc_op equals
+         (concat [string "type";space;doc_id_lem id])
+         (doc_typ_lem regtypes vtyp)
+       ^^ hardline ^^
+       doc_op equals
          (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
          (string "Register" ^^ space ^^
             align (separate space [string "regname"; doc_int size; doc_int i1; dir;
                                    break 0 ^^ brackets (align doc_rids)]))
-       (*^^ hardline ^^
-         separate_map hardline doc_rfield rs *)
+       ^^ hardline ^^
+       doc_op equals
+         (concat [string "let";space;string "cast_";doc_id_lem id;space;string "reg"])
+         (string "reg")
+       ^^ hardline ^^
+       doc_op equals
+         (concat [string "let";space;string "cast_to_";doc_id_lem id;space;string "reg"])
+         (string "reg")
+       ^^ hardline ^^
+         separate_map hardline doc_field rs
 
 let doc_rec_lem (Rec_aux(r,_)) = match r with
   | Rec_nonrec -> space
   | Rec_rec -> space ^^ string "rec" ^^ space
 
 let doc_tannot_opt_lem regtypes (Typ_annot_opt_aux(t,_)) = match t with
-  | Typ_annot_opt_some(tq,typ) -> doc_typquant_lem tq (doc_typ_lem regtypes typ)
+  | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem regtypes typ)
+
+let doc_fun_body_lem regtypes exp =
+  let early_ret = contains_early_return exp in
+  let doc_exp = doc_exp_lem regtypes early_ret false exp in
+  if early_ret
+  then align (string "catch_early_return" ^//^ parens (doc_exp))
+  else doc_exp
 
 let doc_funcl_lem regtypes (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
   group (prefix 3 1 ((doc_pat_lem regtypes false pat) ^^ space ^^ arrow)
-                (doc_exp_lem regtypes false exp))
+    (doc_fun_body_lem regtypes exp))
 
 let get_id = function
   | [] -> failwith "FD_function with empty list"
@@ -1188,7 +1261,7 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot))
           [(string "let") ^^ (doc_rec_lem r) ^^ (doc_id_lem id);
            (doc_pat_lem regtypes true pat);
            equals])
-       (doc_exp_lem regtypes false exp)
+       (doc_fun_body_lem regtypes exp)
   | _ ->
     let id = get_id fcls in
     (*    let sep = hardline ^^ pipe ^^ space in *)
@@ -1230,7 +1303,7 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot))
                let named_pat = P_aux (P_app (Id_aux (Id ctor,l),named_argspat),pannot) in
                let doc_arg idx (P_aux (p,(l,a))) = match p with
                  | P_as (pat,id) -> doc_id_lem id
-                 | P_lit lit -> doc_lit_lem false lit a
+                 | P_lit lit -> doc_lit_lem regtypes false lit a
                  | P_id id -> doc_id_lem id
                  | _ -> string ("arg" ^ string_of_int idx) in
                let clauses =
@@ -1256,37 +1329,33 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot))
       
 
 
-let doc_dec_lem (DEC_aux (reg,(l,annot))) =
+let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
   match reg with
   | DEC_reg(typ,id) ->
+     let env = env_of_annot annot in
      (match typ with
-      | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ rt, _)]), _)
-        when string_of_id r = "register" && is_vector_typ rt ->
-        let env = env_of_annot (l,annot) in
-        let (start, size, order, etyp) = vector_typ_args_of (Env.base_typ_of env rt) in
-        (match is_bit_typ (Env.base_typ_of env etyp), start, size with
-          | true, Nexp_aux (Nexp_constant start, _), Nexp_aux (Nexp_constant size, _) ->
-             let o = if is_order_inc order then "true" else "false" in
-             (doc_op equals)
-             (string "let" ^^ space ^^ doc_id_lem id)
-             (string "Register" ^^ space ^^
-                align (separate space [string_lit(doc_id_lem id);
-                                       doc_int (size);
-                                       doc_int (start);
-                                       string o;
-                                       string "[]"]))
-                ^/^ hardline
-           | _ ->
-              let (Id_aux (Id name,_)) = id in
-              failwith ("can't deal with register " ^ name))
-      | Typ_aux (Typ_app(r, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id idt, _)), _)]), _)
-        when string_of_id r = "register" ->
-         separate space [string "let";doc_id_lem id;equals;
-                         string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline
-      | Typ_aux (Typ_id idt, _) ->
-         separate space [string "let";doc_id_lem id;equals;
-                         string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline
-      |_-> empty)
+      | Typ_aux (Typ_id idt, _) when Env.is_regtyp idt env ->
+        separate space [string "let";doc_id_lem id;equals;
+                        string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline
+      | _ ->
+        let rt = Env.base_typ_of env typ in
+        if is_vector_typ rt then
+          let (start, size, order, etyp) = vector_typ_args_of rt in
+          if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then
+            let o = if is_order_inc order then "true" else "false" in
+            (doc_op equals)
+            (string "let" ^^ space ^^ doc_id_lem id)
+            (string "Register" ^^ space ^^
+               align (separate space [string_lit(doc_id_lem id);
+                                      doc_nexp (size);
+                                      doc_nexp (start);
+                                      string o;
+                                      string "[]"]))
+               ^/^ hardline
+          else raise (Reporting_basic.err_unreachable l
+            ("can't deal with register type " ^ string_of_typ typ))
+        else raise (Reporting_basic.err_unreachable l
+          ("can't deal with register type " ^ string_of_typ typ)))
   | DEC_alias(id,alspec) -> empty
   | DEC_typ_alias(typ,id,alspec) -> empty
 
@@ -1306,7 +1375,7 @@ let rec doc_def_lem regtypes def = match def with
 
   | DEF_default df -> (empty,empty)
   | DEF_fundef f_def -> (empty,group (doc_fundef_lem regtypes f_def) ^/^ hardline)
-  | DEF_val lbind -> (empty,group (doc_let_lem regtypes lbind) ^/^ hardline)
+  | DEF_val lbind -> (empty,group (doc_let_lem regtypes false lbind) ^/^ hardline)
   | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point"
 
   | DEF_kind _ -> (empty,empty)
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 0875aee7..018a93f5 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -154,6 +154,7 @@ let rec pp_format_typ_lem (Typ_aux(t,l)) =
                               (pp_format_effects_lem efct) ^ ")"
     | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])"
     | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])"
+    | Typ_exist(kids,nc,typ) -> "(Typ_exist ([" ^ list_format ";" pp_format_var_lem kids ^ "], " ^ pp_format_nexp_constraint_lem nc ^ ", " ^ pp_format_typ_lem typ ^ "))"
     | Typ_wild -> "Typ_wild") ^ " " ^
     (pp_format_l_lem l) ^ ")"
 and pp_format_nexp_lem (Nexp_aux(n,l)) =
@@ -212,14 +213,7 @@ and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) =
   | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")"
   | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")") ^ " " ^
   (pp_format_l_lem l) ^ ")"
-
-let pp_lem_typ ppf t = base ppf (pp_format_typ_lem t)
-let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n)
-let pp_lem_ord ppf o = base ppf (pp_format_ord_lem o)
-let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e)
-let pp_lem_beffect ppf be = base ppf (pp_format_base_effect_lem be)
-
-let rec pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
+and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
   "(NC_aux " ^
   (match nc with
   | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
@@ -235,6 +229,12 @@ let rec pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
       "])") ^ " " ^
   (pp_format_l_lem l) ^ ")"
 
+let pp_lem_typ ppf t = base ppf (pp_format_typ_lem t)
+let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n)
+let pp_lem_ord ppf o = base ppf (pp_format_ord_lem o)
+let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e)
+let pp_lem_beffect ppf be = base ppf (pp_format_base_effect_lem be)
+
 let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc)
 
 let pp_format_qi_lem (QI_aux(qi,lq)) =
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml
index 66252d94..fc02f568 100644
--- a/src/pretty_print_ocaml.ml
+++ b/src/pretty_print_ocaml.ml
@@ -741,28 +741,23 @@ let doc_dec_ocaml (DEC_aux (reg,(l,annot))) =
   | DEC_reg(typ,id) ->
     if is_vector_typ typ then
       let (start, size, order, itemt) = vector_typ_args_of typ in
-    (* (match annot with
-     | Base((_,t),_,_,_,_,_) ->
-       (match t.t with
-        | Tapp("register", [TA_typ {t= Tapp("vector", [TA_nexp start; TA_nexp size; TA_ord order; TA_typ itemt])}]) 
-        | Tapp("register", [TA_typ {t= Tabbrev(_,{t=Tapp("vector", [TA_nexp start; TA_nexp size; TA_ord order; TA_typ itemt])})}]) -> *)
-          (match is_bit_typ itemt, start, size with
-           | true, Nexp_aux (Nexp_constant start, _), Nexp_aux (Nexp_constant size, _) ->
-             let o = if is_order_inc order then string "true" else string "false" in
-             separate space [string "let";
-                             doc_id_ocaml id;
-                             equals;
-                             string "Vregister";
-                             parens (separate comma [separate space [string "ref";
-                                                                     parens (separate space
-                                                                               [string "Array.make";
-                                                                                doc_int size;
-                                                                                string "Vzero";])];
-                                                     doc_int start;
-                                                     o;
-                                                     string_lit (doc_id id);
-                                                     brackets empty])]
-           | _ -> empty)
+      if is_bit_typ itemt && is_nexp_constant start && is_nexp_constant size then
+        let o = if is_order_inc order then string "true" else string "false" in
+        separate space [string "let";
+                        doc_id_ocaml id;
+                        equals;
+                        string "Vregister";
+                        parens (separate comma [separate space [string "ref";
+                                                                parens (separate space
+                                                                          [string "Array.make";
+                                                                           doc_nexp size;
+                                                                           string "Vzero";])];
+                                                doc_nexp start;
+                                                o;
+                                                string_lit (doc_id id);
+                                                brackets empty])]
+      else raise (Reporting_basic.err_unreachable l
+        ("can't deal with register type " ^ string_of_typ typ))
     else
       (match typ with
         | Typ_aux (Typ_id idt, _) ->
@@ -773,7 +768,8 @@ let doc_dec_ocaml (DEC_aux (reg,(l,annot))) =
                           equals;
                           doc_id_ocaml idt;
                           string "None"]
-        |_-> failwith "type was not handled in register declaration")
+        |_-> raise (Reporting_basic.err_unreachable l
+          ("can't deal with register type " ^ string_of_typ typ)))
      (* | _ -> failwith "annot was not Base") *)
     | DEC_alias(id,alspec) -> empty (*
         doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec) *)
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index aff3a976..a63df7ea 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -117,7 +117,7 @@ let doc_pat, doc_atomic_pat =
   | P_vector_indexed ipats  -> brackets (separate_map comma_sp npat ipats)
   | P_tup pats  -> parens (separate_map comma_sp atomic_pat pats)
   | P_list pats  -> squarebarbars (separate_map semi_sp atomic_pat pats)
-  | P_cons (pat1, pat2) -> separate space [atomic_pat pat1; string "::"; pat pat2]
+  | P_cons (pat1, pat2) -> separate space [atomic_pat pat1; coloncolon; pat pat2]
   | P_app(_, _ :: _) | P_vector_concat _ ->
       group (parens (pat pa))
   and fpat (FP_aux(FP_Fpat(id,fpat),_)) = doc_op equals (doc_id id) (pat fpat)
@@ -155,7 +155,7 @@ let doc_exp, doc_let =
   | E_vector_append(l,r) ->
       doc_op colon (shift_exp l) (cons_exp r)
   | E_cons(l,r) ->
-      doc_op colon (shift_exp l) (cons_exp r)
+      doc_op coloncolon (shift_exp l) (cons_exp r)
   | _ -> shift_exp expr
   and shift_exp ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id (">>" | ">>>" | "<<" | "<<<"),_) as op),r) ->
diff --git a/src/process_file.ml b/src/process_file.ml
index 91262ce9..6d4bcea0 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -98,6 +98,7 @@ let load_file order env f =
 
 let opt_just_check = ref false
 let opt_ddump_tc_ast = ref false
+let opt_ddump_rewrite_ast = ref None
 let opt_dno_cast = ref false
 
 let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t =
@@ -112,10 +113,6 @@ let monomorphise_ast locs ast =
   let ienv = Type_check.Env.no_casts Type_check.initial_env in
   Type_check.check ienv ast
 
-let rewrite_ast (defs: Type_check.tannot Ast.defs) = Rewriter.rewrite_defs defs
-let rewrite_ast_lem (defs: Type_check.tannot Ast.defs) = Rewriter.rewrite_defs_lem defs
-let rewrite_ast_ocaml (defs: Type_check.tannot Ast.defs) = Rewriter.rewrite_defs_ocaml defs
-
 let open_output_with_check file_name =
   let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
   let o' = Format.formatter_of_out_channel o in
@@ -235,3 +232,20 @@ let output libpath out_arg files =
     (fun (f, defs) ->
        output1 libpath out_arg f defs)
     files
+
+let rewrite_step defs rewriter =
+  let defs = rewriter defs in
+  let _ = match !(opt_ddump_rewrite_ast) with
+    | Some (f, i) ->
+      begin
+        output "" Lem_ast_out [f ^ "_rewrite_" ^ string_of_int i ^ ".sail",defs];
+        opt_ddump_rewrite_ast := Some (f, i + 1)
+      end
+    | _ -> () in
+  defs
+
+let rewrite rewriters defs = List.fold_left rewrite_step defs rewriters
+
+let rewrite_ast = rewrite [Rewriter.rewrite_defs]
+let rewrite_ast_lem = rewrite Rewriter.rewrite_defs_lem
+let rewrite_ast_ocaml = rewrite Rewriter.rewrite_defs_ocaml
diff --git a/src/process_file.mli b/src/process_file.mli
index 7972c689..cd867b0d 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -54,6 +54,7 @@ val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast
 val opt_new_parser : bool ref
 val opt_just_check : bool ref
 val opt_ddump_tc_ast : bool ref
+val opt_ddump_rewrite_ast : ((string * int) option) ref
 val opt_dno_cast : bool ref
 
 type out_type =
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 8cf682bf..8da8aacf 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -66,7 +66,13 @@ let effect_of_fexp (FE_aux (_,(_,a))) = effect_of_annot a
 let effect_of_fexps (FES_aux (FES_Fexps (fexps,_),_)) =
   List.fold_left union_effects no_effect (List.map effect_of_fexp fexps)
 let effect_of_opt_default (Def_val_aux (_,(_,a))) = effect_of_annot a
-let effect_of_pexp (Pat_aux (_,(_,a))) = effect_of_annot a
+(* The typechecker does not seem to annotate pexps themselves *)
+let effect_of_pexp (Pat_aux (pexp,(_,a))) = match a with
+  | Some (_, _, eff) -> eff
+  | None ->
+    (match pexp with
+    | Pat_exp (_, e) -> effect_of e
+    | Pat_when (_, g, e) -> union_effects (effect_of g) (effect_of e))
 let effect_of_lb (LB_aux (_,(_,a))) = effect_of_annot a
 
 let get_loc_exp (E_aux (_,(l,_))) = l
@@ -143,8 +149,8 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
       List.fold_left union_effects (effect_of e) (List.map effect_of_pexp pexps)
     | E_let (lb,e) -> union_effects (effect_of_lb lb) (effect_of e)
     | E_assign (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e)
-    | E_exit e -> effect_of e
-    | E_return e -> effect_of e
+    | E_exit e -> union_effects eff (effect_of e)
+    | E_return e -> union_effects eff (effect_of e)
     | E_sizeof _ | E_sizeof_internal _ | E_constraint _ -> no_effect
     | E_assert (c,m) -> eff
     | E_comment _ | E_comment_struc _ -> no_effect
@@ -1048,6 +1054,7 @@ let rewrite_sizeof (Defs defs) =
         Id_aux (Id op, Parse_ast.Unknown),
         E_aux (e_sizeof nmap nexp2, simple_annot l (atom_typ nexp2))
         ) in
+      let (Nexp_aux (nexp, l) as nexp_aux) = simplify_nexp nexp_aux in
       (match nexp with
       | Nexp_constant i -> E_lit (L_aux (L_num i, l))
       | Nexp_times (nexp1, nexp2) -> binop nexp1 "*" nexp2
@@ -1058,14 +1065,15 @@ let rewrite_sizeof (Defs defs) =
   (* Rewrite calls to functions which have had parameters added to pass values
      of type-level variables; these are added as sizeof expressions first, and
      then further rewritten as above. *)
-  let e_app_aux param_map (exp, ((l,_) as annot)) =
+  let e_app_aux param_map ((exp, exp_orig), ((l,_) as annot)) =
     let full_exp = E_aux (exp, annot) in
+    let orig_exp = E_aux (exp_orig, annot) in
     match exp with
     | E_app (f, args) ->
       if Bindings.mem f param_map then
         (* Retrieve instantiation of the type variables of the called function
-           for the given parameters in the current environment *)
-        let inst = instantiation_of full_exp in
+           for the given parameters in the original environment *)
+        let inst = instantiation_of orig_exp in
         let kid_exp kid = begin
           match KBindings.find kid inst with
           | U_nexp nexp -> E_aux (E_sizeof nexp, simple_annot l (atom_typ nexp))
@@ -1075,9 +1083,75 @@ let rewrite_sizeof (Defs defs) =
               " of function " ^ string_of_id f))
         end in
         let kid_exps = List.map kid_exp (KidSet.elements (Bindings.find f param_map)) in
-        E_aux (E_app (f, kid_exps @ args), annot)
-      else full_exp
-    | _ -> full_exp in
+        (E_aux (E_app (f, kid_exps @ args), annot), orig_exp)
+      else (full_exp, orig_exp)
+    | _ -> (full_exp, orig_exp) in
+
+  (* Plug this into a folding algorithm that also keeps around a copy of the
+  original expressions, which we use to infer instantiations of type variables
+  in the original environments *)
+  let copy_exp_alg =
+    { e_block = (fun es -> let (es, es') = List.split es in (E_block es, E_block es'))
+    ; e_nondet = (fun es -> let (es, es') = List.split es in (E_nondet es, E_nondet es'))
+    ; e_id = (fun id -> (E_id id, E_id id))
+    ; e_lit = (fun lit -> (E_lit lit, E_lit lit))
+    ; e_cast = (fun (typ,(e,e')) -> (E_cast (typ,e), E_cast (typ,e')))
+    ; e_app = (fun (id,es) -> let (es, es') = List.split es in (E_app (id,es), E_app (id,es')))
+    ; e_app_infix = (fun ((e1,e1'),id,(e2,e2')) -> (E_app_infix (e1,id,e2), E_app_infix (e1',id,e2')))
+    ; e_tuple = (fun es -> let (es, es') = List.split es in (E_tuple es, E_tuple es'))
+    ; e_if = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_if (e1,e2,e3), E_if (e1',e2',e3')))
+    ; e_for = (fun (id,(e1,e1'),(e2,e2'),(e3,e3'),order,(e4,e4')) -> (E_for (id,e1,e2,e3,order,e4), E_for (id,e1',e2',e3',order,e4')))
+    ; e_vector = (fun es -> let (es, es') = List.split es in (E_vector es, E_vector es'))
+    ; e_vector_indexed = (fun (es,(opt2,opt2')) -> let (is, es) = List.split es in let (es, es') = List.split es in let (es, es') = (List.combine is es, List.combine is es') in (E_vector_indexed (es,opt2), E_vector_indexed (es',opt2')))
+    ; e_vector_access = (fun ((e1,e1'),(e2,e2')) -> (E_vector_access (e1,e2), E_vector_access (e1',e2')))
+    ; e_vector_subrange =  (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_vector_subrange (e1,e2,e3), E_vector_subrange (e1',e2',e3')))
+    ; e_vector_update = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_vector_update (e1,e2,e3), E_vector_update (e1',e2',e3')))
+    ; e_vector_update_subrange =  (fun ((e1,e1'),(e2,e2'),(e3,e3'),(e4,e4')) -> (E_vector_update_subrange (e1,e2,e3,e4), E_vector_update_subrange (e1',e2',e3',e4')))
+    ; e_vector_append = (fun ((e1,e1'),(e2,e2')) -> (E_vector_append (e1,e2), E_vector_append (e1',e2')))
+    ; e_list = (fun es -> let (es, es') = List.split es in (E_list es, E_list es'))
+    ; e_cons = (fun ((e1,e1'),(e2,e2')) -> (E_cons (e1,e2), E_cons (e1',e2')))
+    ; e_record = (fun (fexps, fexps') -> (E_record fexps, E_record fexps'))
+    ; e_record_update = (fun ((e1,e1'),(fexp,fexp')) -> (E_record_update (e1,fexp), E_record_update (e1',fexp')))
+    ; e_field = (fun ((e1,e1'),id) -> (E_field (e1,id), E_field (e1',id)))
+    ; e_case = (fun ((e1,e1'),pexps) -> let (pexps, pexps') = List.split pexps in (E_case (e1,pexps), E_case (e1',pexps')))
+    ; e_let = (fun ((lb,lb'),(e2,e2')) -> (E_let (lb,e2), E_let (lb',e2')))
+    ; e_assign = (fun ((lexp,lexp'),(e2,e2')) -> (E_assign (lexp,e2), E_assign (lexp',e2')))
+    ; e_sizeof = (fun nexp -> (E_sizeof nexp, E_sizeof nexp))
+    ; e_exit = (fun (e1,e1') -> (E_exit (e1), E_exit (e1')))
+    ; e_return = (fun (e1,e1') -> (E_return e1, E_return e1'))
+    ; e_assert = (fun ((e1,e1'),(e2,e2')) -> (E_assert(e1,e2), E_assert(e1',e2')) )
+    ; e_internal_cast = (fun (a,(e1,e1')) -> (E_internal_cast (a,e1), E_internal_cast (a,e1')))
+    ; e_internal_exp = (fun a -> (E_internal_exp a, E_internal_exp a))
+    ; e_internal_exp_user = (fun (a1,a2) -> (E_internal_exp_user (a1,a2), E_internal_exp_user (a1,a2)))
+    ; e_comment = (fun c -> (E_comment c, E_comment c))
+    ; e_comment_struc = (fun (e,e') -> (E_comment_struc e, E_comment_struc e'))
+    ; e_internal_let = (fun ((lexp,lexp'), (e2,e2'), (e3,e3')) -> (E_internal_let (lexp,e2,e3), E_internal_let (lexp',e2',e3')))
+    ; e_internal_plet = (fun (pat, (e1,e1'), (e2,e2')) -> (E_internal_plet (pat,e1,e2), E_internal_plet (pat,e1',e2')))
+    ; e_internal_return = (fun (e,e') -> (E_internal_return e, E_internal_return e'))
+    ; e_aux = (fun ((e,e'),annot) -> (E_aux (e,annot), E_aux (e',annot)))
+    ; lEXP_id = (fun id -> (LEXP_id id, LEXP_id id))
+    ; lEXP_memory = (fun (id,es) -> let (es, es') = List.split es in (LEXP_memory (id,es), LEXP_memory (id,es')))
+    ; lEXP_cast = (fun (typ,id) -> (LEXP_cast (typ,id), LEXP_cast (typ,id)))
+    ; lEXP_tup = (fun tups -> let (tups,tups') = List.split tups in (LEXP_tup tups, LEXP_tup tups'))
+    ; lEXP_vector = (fun ((lexp,lexp'),(e2,e2')) -> (LEXP_vector (lexp,e2), LEXP_vector (lexp',e2')))
+    ; lEXP_vector_range = (fun ((lexp,lexp'),(e2,e2'),(e3,e3')) -> (LEXP_vector_range (lexp,e2,e3), LEXP_vector_range (lexp',e2',e3')))
+    ; lEXP_field = (fun ((lexp,lexp'),id) -> (LEXP_field (lexp,id), LEXP_field (lexp',id)))
+    ; lEXP_aux = (fun ((lexp,lexp'),annot) -> (LEXP_aux (lexp,annot), LEXP_aux (lexp',annot)))
+    ; fE_Fexp = (fun (id,(e,e')) -> (FE_Fexp (id,e), FE_Fexp (id,e')))
+    ; fE_aux = (fun ((fexp,fexp'),annot) -> (FE_aux (fexp,annot), FE_aux (fexp',annot)))
+    ; fES_Fexps = (fun (fexps,b) -> let (fexps, fexps') = List.split fexps in (FES_Fexps (fexps,b), FES_Fexps (fexps',b)))
+    ; fES_aux = (fun ((fexp,fexp'),annot) -> (FES_aux (fexp,annot), FES_aux (fexp',annot)))
+    ; def_val_empty = (Def_val_empty, Def_val_empty)
+    ; def_val_dec = (fun (e,e') -> (Def_val_dec e, Def_val_dec e'))
+    ; def_val_aux = (fun ((defval,defval'),aux) -> (Def_val_aux (defval,aux), Def_val_aux (defval',aux)))
+    ; pat_exp = (fun (pat,(e,e')) -> (Pat_exp (pat,e), Pat_exp (pat,e')))
+    ; pat_when = (fun (pat,(e1,e1'),(e2,e2')) -> (Pat_when (pat,e1,e2), Pat_when (pat,e1',e2')))
+    ; pat_aux = (fun ((pexp,pexp'),a) -> (Pat_aux (pexp,a), Pat_aux (pexp',a)))
+    ; lB_val_explicit = (fun (typ,pat,(e,e')) -> (LB_val_explicit (typ,pat,e), LB_val_explicit (typ,pat,e')))
+    ; lB_val_implicit = (fun (pat,(e,e')) -> (LB_val_implicit (pat,e), LB_val_implicit (pat,e')))
+    ; lB_aux = (fun ((lb,lb'),annot) -> (LB_aux (lb,annot), LB_aux (lb',annot)))
+    ; pat_alg = id_pat_alg
+    } in
 
   let rewrite_sizeof_fun params_map
     (FD_aux (FD_function (rec_opt,tannot,eff,funcls),((l,_) as annot))) =
@@ -1086,7 +1160,7 @@ let rewrite_sizeof (Defs defs) =
       let body_typ = typ_of exp in
       let nmap = nexps_from_params pat in
       (* first rewrite calls to other functions... *)
-      let exp' = fold_exp { id_exp_alg with e_aux = e_app_aux params_map } exp in
+      let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in
       (* ... then rewrite sizeof expressions in current function body *)
       let exp'' = fold_exp { id_exp_alg with e_sizeof = e_sizeof nmap } exp' in
       (FCL_aux (FCL_Funcl (id,pat,exp''), annot) :: funcls,
@@ -1133,9 +1207,10 @@ let rewrite_sizeof (Defs defs) =
   let rewrite_sizeof_fundef (params_map, defs) = function
   | DEF_fundef fd ->
     let (nvars, fd') = rewrite_sizeof_fun params_map fd in
+    let id = id_of_fundef fd in
     let params_map' =
       if KidSet.is_empty nvars then params_map
-      else Bindings.add (id_of_fundef fd) nvars params_map in
+      else Bindings.add id nvars params_map in
     (params_map', defs @ [DEF_fundef fd'])
   | def ->
     (params_map, defs @ [def]) in
@@ -1947,7 +2022,7 @@ let rewrite_defs_remove_bitvector_pats (Defs defs) =
        let defvals = List.map (fun lb -> DEF_val lb) letbinds in
        [DEF_val (LB_aux (LB_val_implicit (pat',exp),a))] @ defvals
     | d -> [d] in
-  Defs (List.flatten (List.map rewrite_def defs))
+  fst (check initial_env (Defs (List.flatten (List.map rewrite_def defs))))
 
 
 (* Remove pattern guards by rewriting them to if-expressions within the
@@ -1999,7 +2074,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
       | (E_aux(E_assign((LEXP_aux ((LEXP_id id | LEXP_cast (_,id)),_)) as le,e),
                ((l, Some (env,typ,eff)) as annot)) as exp)::exps ->
         (match Env.lookup_id id env with
-         | Unbound ->
+         | Unbound | Local _ ->
             let le' = rewriters.rewrite_lexp rewriters le in
             let e' = rewrite_base e in
             let exps' = walker exps in
@@ -2136,12 +2211,72 @@ let rewrite_defs_separate_numbs defs = rewrite_defs_base
      rewrite_def = rewrite_def;
      rewrite_defs = rewrite_defs_base} defs*)
 
-let rewrite_defs_ocaml =
-  top_sort_defs >>
-  rewrite_defs_remove_vector_concat >>
-  rewrite_sizeof >>
-  rewrite_defs_exp_lift_assign (* >>
+let rewrite_defs_early_return =
+  let is_return (E_aux (exp, _)) = match exp with
+  | E_return _ -> true
+  | _ -> false in
+
+  let get_return (E_aux (e, (l, _)) as exp) = match e with
+  | E_return e -> e
+  | _ -> 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
+    | _ -> E_block es in
+
+  let e_if (e1, e2, e3) =
+    if is_return e2 && is_return e3 then E_if (e1, get_return e2, get_return e3)
+    else E_if (e1, e2, e3) in
+
+  let e_case (e, pes) =
+    let is_return_pexp (Pat_aux (pexp, _)) = match pexp with
+    | Pat_exp (_, e) | Pat_when (_, _, e) -> is_return e in
+    let get_return_pexp (Pat_aux (pexp, a)) = match pexp with
+    | Pat_exp (p, e) -> Pat_aux (Pat_exp (p, get_return e), a)
+    | Pat_when (p, g, e) -> Pat_aux (Pat_when (p, g, get_return e), a) in
+    if List.for_all is_return_pexp pes
+    then E_return (E_aux (E_case (e, List.map get_return_pexp pes), (Parse_ast.Unknown, None)))
+    else E_case (e, pes) in
+
+  let e_aux (exp, (l, annot)) =
+    let full_exp = fix_eff_exp (E_aux (exp, (l, annot))) in
+    match annot with
+    | Some (env, typ, eff) when is_return full_exp ->
+      (* Add escape effect annotation, since we use the exception mechanism
+         of the state monad to implement early return in the Lem backend *)
+      let annot' = Some (env, typ, union_effects eff (mk_effect [BE_escape])) in
+      E_aux (exp, (l, annot'))
+    | _ -> 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 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
+
+  let rewrite_fun_early_return rewriters
+    (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), a)) =
+    FD_aux (FD_function (rec_opt, tannot_opt, effect_opt,
+      List.map (rewrite_funcl_early_return rewriters) funcls), a) in
+
+  rewrite_defs_base { rewriters_base with rewrite_fun = rewrite_fun_early_return }
+
+let rewrite_defs_ocaml = [
+  top_sort_defs;
+  rewrite_defs_remove_vector_concat;
+  rewrite_sizeof;
+  rewrite_defs_exp_lift_assign (* ;
   rewrite_defs_separate_numbs *)
+  ]
 
 let rewrite_defs_remove_blocks =
   let letbind_wild v body =
@@ -2398,7 +2533,7 @@ let rewrite_defs_letbind_effects  =
     | E_case (exp1,pexps) ->
        let newreturn =
          List.fold_left
-           (fun b (Pat_aux (_,(_,annot))) -> b || effectful_effs (effect_of_annot annot))
+           (fun b pexp -> b || effectful_effs (effect_of_pexp pexp))
            false pexps in
        n_exp_name exp1 (fun exp1 -> 
        n_pexpL newreturn pexps (fun pexps ->
@@ -2766,7 +2901,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          | _ ->
            raise (Reporting_basic.err_unreachable l
              "assignment without effects annotation") in
-       if not (List.exists (function BE_aux (BE_lset,_) -> true | _ -> false) effs) then
+       if effectful exp then
          Same_vars (E_aux (E_assign (lexp,vexp),annot))
        else 
          (match lexp with
@@ -2968,18 +3103,22 @@ let rewrite_defs_remove_e_assign =
     ; rewrite_defs = rewrite_defs_base
     }
 
-
-let rewrite_defs_lem =
-  top_sort_defs >>
-  rewrite_sizeof >>
-  rewrite_defs_remove_vector_concat >>
-  rewrite_defs_remove_bitvector_pats >>
-  rewrite_defs_guarded_pats >>
-  rewrite_defs_exp_lift_assign >> 
-  rewrite_defs_remove_blocks >> 
-  rewrite_defs_letbind_effects >> 
-  rewrite_defs_remove_e_assign >> 
-  rewrite_defs_effectful_let_expressions >> 
-  rewrite_defs_remove_superfluous_letbinds >>
+let recheck_defs defs = fst (check initial_env defs)
+
+let rewrite_defs_lem =[
+  top_sort_defs;
+  rewrite_sizeof;
+  rewrite_defs_remove_vector_concat;
+  rewrite_defs_remove_bitvector_pats;
+  rewrite_defs_guarded_pats;
+  (* recheck_defs; *)
+  rewrite_defs_early_return;
+  rewrite_defs_exp_lift_assign;
+  rewrite_defs_remove_blocks;
+  rewrite_defs_letbind_effects;
+  rewrite_defs_remove_e_assign;
+  rewrite_defs_effectful_let_expressions;
+  rewrite_defs_remove_superfluous_letbinds;
   rewrite_defs_remove_superfluous_returns
+  ]
   
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 473456f6..9dbdee3d 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -56,8 +56,8 @@ type 'a rewriters = { rewrite_exp  : 'a rewriters -> 'a exp -> 'a exp;
                     
 val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp
 val rewrite_defs : tannot defs -> tannot defs
-val rewrite_defs_ocaml : tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for ocaml out*)
-val rewrite_defs_lem : tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for lem out*)
+val rewrite_defs_ocaml : (tannot defs -> tannot defs) list (*Perform rewrites to exclude AST nodes not supported for ocaml out*)
+val rewrite_defs_lem : (tannot defs -> tannot defs) list (*Perform rewrites to exclude AST nodes not supported for lem out*)
 
 (* the type of interpretations of pattern-matching expressions *)
 type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
@@ -154,3 +154,10 @@ val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_a
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp
 
 val id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg
+
+val compute_exp_alg : 'b -> ('b -> 'b -> 'b) ->
+  ('a,('b * 'a exp),('b * 'a exp_aux),('b * 'a lexp),('b * 'a lexp_aux),('b * 'a fexp),
+  ('b * 'a fexp_aux),('b * 'a fexps),('b * 'a fexps_aux),
+  ('b * 'a opt_default_aux),('b * 'a opt_default),('b * 'a pexp),('b * 'a pexp_aux),
+  ('b * 'a letbind_aux),('b * 'a letbind),
+  ('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) exp_alg
diff --git a/src/sail.ml b/src/sail.ml
index d03060dc..cf366d42 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -97,6 +97,9 @@ let options = Arg.align ([
   ( "-ddump_tc_ast",
     Arg.Set opt_ddump_tc_ast,
     " (debug) dump the typechecked ast to stdout");
+  ( "-ddump_rewrite_ast",
+    Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0)),
+    " <prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem");
   ( "-dtc_verbose",
     Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity),
     " (debug) verbose typechecker output: 0 is silent");
diff --git a/src/type_check.ml b/src/type_check.ml
index bd2db570..e69a40e8 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -157,6 +157,12 @@ let is_range (Typ_aux (typ_aux, _)) =
        when string_of_id f = "range" -> Some (n1, n2)
   | _ -> None
 
+let is_list (Typ_aux (typ_aux, _)) =
+  match typ_aux with
+  | Typ_app (f, [Typ_arg_aux (Typ_arg_typ typ, _)])
+       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)
@@ -406,6 +412,7 @@ module Env : sig
   val add_union_id : id -> typquant * typ -> t -> t
   val add_flow : id -> (typ -> typ) -> t -> t
   val get_flow : id -> t -> typ -> typ
+  val is_register : id -> t -> bool
   val get_register : id -> t -> typ
   val add_register : id -> typ -> t -> t
   val add_regtyp : id -> int -> int -> (index_range * id) list -> t -> t
@@ -423,6 +430,9 @@ module Env : sig
   val get_typ_synonym : id -> t -> t -> typ_arg list -> typ
   val add_overloads : id -> id list -> t -> t
   val get_overloads : id -> t -> id list
+  val is_extern : id -> t -> bool
+  val add_extern : id -> string -> t -> t
+  val get_extern : id -> t -> string
   val get_default_order : t -> order
   val set_default_order_inc : t -> t
   val set_default_order_dec : t -> t
@@ -453,6 +463,7 @@ end = struct
       enums : IdSet.t Bindings.t;
       records : (typquant * (typ * id) list) Bindings.t;
       accessors : (typquant * typ) Bindings.t;
+      externs : string Bindings.t;
       casts : id list;
       allow_casts : bool;
       constraints : n_constraint list;
@@ -474,6 +485,7 @@ end = struct
       enums = Bindings.empty;
       records = Bindings.empty;
       accessors = Bindings.empty;
+      externs = Bindings.empty;
       casts = [];
       allow_casts = true;
       constraints = [];
@@ -694,6 +706,9 @@ end = struct
       { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow }
     end
 
+  let is_register id env =
+    Bindings.mem id env.registers
+
   let get_register id env =
     try Bindings.find id env.registers with
     | Not_found -> typ_error (id_loc id) ("No register binding found for " ^ string_of_id id)
@@ -706,6 +721,16 @@ end = struct
     typ_print ("Adding overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]");
     { env with overloads = Bindings.add id ids env.overloads }
 
+  let is_extern id env =
+    Bindings.mem id env.externs
+
+  let add_extern id ext env =
+    { env with externs = Bindings.add id ext env.externs }
+
+  let get_extern id env =
+    try Bindings.find id env.externs with
+    | Not_found -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id)
+
   let get_casts env = env.casts
 
   let check_index_range cmp f t (BF_aux (ir, l)) =
@@ -863,6 +888,19 @@ end = struct
     | Typ_arg_typ typ -> Typ_arg_aux (Typ_arg_typ (expand_synonyms env typ), l)
     | arg -> Typ_arg_aux (arg, l)
 
+  let get_default_order env =
+    match env.default_order with
+    | None -> typ_error Parse_ast.Unknown ("No default order has been set")
+    | Some ord -> ord
+
+  let set_default_order o env =
+    match env.default_order with
+    | None -> { env with default_order = Some (Ord_aux (o, Parse_ast.Unknown)) }
+    | Some _ -> typ_error Parse_ast.Unknown ("Cannot change default order once already set")
+
+  let set_default_order_inc = set_default_order Ord_inc
+  let set_default_order_dec = set_default_order Ord_dec
+
   let base_typ_of env typ =
     let rec aux (Typ_aux (t,a)) =
       let rewrap t = Typ_aux (t,a) in
@@ -876,6 +914,11 @@ end = struct
         aux rtyp
       | Typ_app (id, targs) ->
         rewrap (Typ_app (id, List.map aux_arg targs))
+      | Typ_id id when is_regtyp id env ->
+        let base, top, ranges = get_regtyp id env in
+        let len = abs(top - base) + 1 in
+        vector_typ (nconstant base) (nconstant len) (get_default_order env) bit_typ
+        (* TODO registers with non-default order? non-bitvector registers? *)
       | t -> rewrap t
     and aux_arg (Typ_arg_aux (targ,a)) =
       let rewrap targ = Typ_arg_aux (targ,a) in
@@ -884,19 +927,6 @@ end = struct
       | targ -> rewrap targ in
     aux (expand_synonyms env typ)
 
-  let get_default_order env =
-    match env.default_order with
-    | None -> typ_error Parse_ast.Unknown ("No default order has been set")
-    | Some ord -> ord
-
-  let set_default_order o env =
-    match env.default_order with
-    | None -> { env with default_order = Some (Ord_aux (o, Parse_ast.Unknown)) }
-    | Some _ -> typ_error Parse_ast.Unknown ("Cannot change default order once already set")
-
-  let set_default_order_inc = set_default_order Ord_inc
-  let set_default_order_dec = set_default_order Ord_dec
-
 end
 
 
@@ -1320,6 +1350,13 @@ let rec unify_nexps l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (ne
            match nexp_aux2 with
            | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_fixed (n1a, n2a), Parse_ast.Unknown)) ->
               unify_nexps l env goals n1b n2b
+           | Nexp_constant c2 ->
+              begin
+                match n1a with
+                | Nexp_aux (Nexp_constant c1,_) when c2 mod c1 = 0 ->
+                   unify_nexps l env goals n1b (mk_nexp (Nexp_constant (c2 / c1)))
+                | _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2)
+              end
            | _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2)
          end
        else if KidSet.is_empty (nexp_frees n1b)
@@ -1837,13 +1874,30 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
           Pat_aux (Pat_when (tpat, checked_guard, crule check_exp env case typ), (l, None))
      in
      annot_exp (E_case (inferred_exp, List.map (fun case -> check_case case typ) cases)) typ
+  | E_cons (x, xs), _ ->
+     begin
+       match is_list (Env.expand_synonyms env typ) with
+       | Some elem_typ ->
+          let checked_xs = crule check_exp env xs typ in
+          let checked_x = crule check_exp env x elem_typ in
+          annot_exp (E_cons (checked_x, checked_xs)) typ
+       | None -> typ_error l ("Cons " ^ string_of_exp exp ^ " must have list type, got " ^ string_of_typ typ)
+     end
+  | E_list xs, _ ->
+     begin
+       match is_list (Env.expand_synonyms env typ) with
+       | Some elem_typ ->
+          let checked_xs = List.map (fun x -> crule check_exp env x elem_typ) xs in
+          annot_exp (E_list checked_xs) typ
+       | None -> typ_error l ("List " ^ string_of_exp exp ^ " must have list type, got " ^ string_of_typ typ)
+     end
   | E_let (LB_aux (letbind, (let_loc, _)), exp), _ ->
      begin
        match letbind with
        | LB_val_explicit (typschm, pat, bind) -> assert false
        | LB_val_implicit (P_aux (P_typ (ptyp, _), _) as pat, bind) ->
           let checked_bind = crule check_exp env bind ptyp in
-          let tpat, env = bind_pat env pat (typ_of checked_bind) in
+          let tpat, env = bind_pat env pat ptyp in
           annot_exp (E_let (LB_aux (LB_val_implicit (tpat, checked_bind), (let_loc, None)), crule check_exp env exp typ)) typ
        | LB_val_implicit (pat, bind) ->
           let inferred_bind = irule infer_exp env bind in
@@ -1897,7 +1951,8 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
   | E_lit (L_aux (L_undef, _) as lit), _ ->
      annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef])
   (* This rule allows registers of type t to be passed by name with type register<t>*)
-  | E_id reg, Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) when string_of_id id = "register" ->
+  | E_id reg, Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)])
+    when string_of_id id = "register" && Env.is_register reg env ->
      let rtyp = Env.get_register reg env in
      subtyp l env rtyp typ; annot_exp (E_id reg) typ (* CHECK: is this subtyp the correct way around? *)
   | E_id id, _ when is_union_id id env ->
@@ -1975,7 +2030,7 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
   end
 
 and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) =
-  typ_print ("Binding " ^ string_of_typ typ);
+  typ_print ("Binding " ^ string_of_pat pat ^  " to " ^ string_of_typ typ);
   let annot_pat pat typ = P_aux (pat, (l, Some (env, typ, no_effect))) in
   let switch_typ (P_aux (pat_aux, (l, Some (env, _, eff)))) typ = P_aux (pat_aux, (l, Some (env, typ, eff))) in
   let bind_tuple_pat (tpats, env) pat typ =
@@ -2161,10 +2216,11 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
             end
        in
        let regtyp, inferred_flexp, is_register = infer_flexp flexp in
-       let eff = if is_register then mk_effect [BE_wreg] else no_effect in
        typ_debug ("REGTYP: " ^ string_of_typ regtyp ^ " / " ^ string_of_typ (Env.expand_synonyms env regtyp));
        match Env.expand_synonyms env regtyp with
+       | Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id regtyp_id, _)), _)]), _)
        | Typ_aux (Typ_id regtyp_id, _) when Env.is_regtyp regtyp_id env ->
+          let eff = mk_effect [BE_wreg] in
           let base, top, ranges = Env.get_regtyp regtyp_id env in
           let range, _ =
             try List.find (fun (_, id) -> Id.compare id field = 0) ranges with
@@ -2180,6 +2236,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
           let checked_exp = crule check_exp env exp vec_typ in
           annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp regtyp eff, field)) vec_typ) checked_exp, env
        | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
+          let eff = if is_register then mk_effect [BE_wreg] else no_effect in
           let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor rectyp_id field env in
           let unifiers, _, _ (* FIXME *) = try unify l env rectyp_q regtyp with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
           let field_typ' = subst_unifiers unifiers field_typ in
@@ -2282,11 +2339,12 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
   (* Not sure about this case... can the left lexp be anything other than an identifier? *)
   | LEXP_vector (LEXP_aux (LEXP_id v, _), exp) ->
      begin
-       let is_immutable, vtyp = match Env.lookup_id v env with
+       let is_immutable, is_register, vtyp = match Env.lookup_id v env with
          | Unbound -> typ_error l "Cannot assign to element of unbound vector"
          | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
-         | Local (Immutable, vtyp) -> true, vtyp
-         | Local (Mutable, vtyp) | Register vtyp -> false, vtyp
+         | Local (Immutable, vtyp) -> true, false, vtyp
+         | Local (Mutable, vtyp) -> false, false, vtyp
+         | Register vtyp -> false, true, vtyp
        in
        let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in
        let E_aux (E_app (_, [_; inferred_exp]), _) = access in
@@ -2294,6 +2352,9 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
        | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" ->
           subtyp l env typ deref_typ;
           annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env
+       | _ when not is_immutable && is_register ->
+          subtyp l env typ (typ_of access);
+          annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env
        | _ when not is_immutable ->
           subtyp l env typ (typ_of access);
           annot_lexp (LEXP_vector (annot_lexp (LEXP_id v) vtyp, inferred_exp)) typ, env
@@ -2336,26 +2397,28 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        let inferred_exp = irule infer_exp env exp in
        match Env.expand_synonyms env (typ_of inferred_exp) with
        (* Accessing a (bit) field of a register *)
-       | Typ_aux (Typ_id regtyp, _) when Env.is_regtyp regtyp env ->
+       | Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ ((Typ_aux (Typ_id regtyp, _) as regtyp_aux)), _)]), _)
+       | (Typ_aux (Typ_id regtyp, _) as regtyp_aux) when Env.is_regtyp regtyp env ->
           let base, top, ranges = Env.get_regtyp regtyp env in
           let range, _ =
             try List.find (fun (_, id) -> Id.compare id field = 0) ranges with
             | Not_found -> typ_error l ("Field " ^ string_of_id field ^ " doesn't exist for register type " ^ string_of_id regtyp)
           in
+          let checked_exp = crule check_exp env (strip_exp inferred_exp) regtyp_aux in
           begin
             match range, Env.get_default_order env with
             | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) ->
                let vec_typ = dvector_typ env (nconstant n) (nconstant 1) bit_typ in
-               annot_exp (E_field (inferred_exp, field)) vec_typ
+               annot_exp (E_field (checked_exp, field)) vec_typ
             | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) ->
                let vec_typ = dvector_typ env (nconstant n) (nconstant (n - m + 1)) bit_typ in
-               annot_exp (E_field (inferred_exp, field)) vec_typ
+               annot_exp (E_field (checked_exp, field)) vec_typ
             | BF_aux (BF_single n, _), Ord_aux (Ord_inc, _) ->
                let vec_typ = dvector_typ env (nconstant n) (nconstant 1) bit_typ in
-               annot_exp (E_field (inferred_exp, field)) vec_typ
+               annot_exp (E_field (checked_exp, field)) vec_typ
             | BF_aux (BF_range (n, m), _), Ord_aux (Ord_inc, _) ->
                let vec_typ = dvector_typ env (nconstant n) (nconstant (m - n + 1)) bit_typ in
-               annot_exp (E_field (inferred_exp, field)) vec_typ
+               annot_exp (E_field (checked_exp, field)) vec_typ
             | _, _ -> typ_error l "Invalid register field type"
           end
        (* Accessing a field of a record *)
@@ -2674,6 +2737,13 @@ and propagate_exp_effect_aux = function
      let p_lb, eff = propagate_letbind_effect letbind in
      let p_exp = propagate_exp_effect exp in
      E_let (p_lb, p_exp), union_effects (effect_of p_exp) eff
+  | E_cons (x, xs) ->
+     let p_x = propagate_exp_effect x in
+     let p_xs = propagate_exp_effect xs in
+     E_cons (p_x, p_xs), union_effects (effect_of p_x) (effect_of p_xs)
+  | E_list xs ->
+     let p_xs = List.map propagate_exp_effect xs in
+     E_list p_xs, collect_effects p_xs
   | E_assign (lexp, exp) ->
      let p_lexp = propagate_lexp_effect lexp in
      let p_exp = propagate_exp_effect exp in
@@ -2908,8 +2978,12 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
   let (id, quants, typ, env) = match vs with
     | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ, env)
     | VS_cast_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ, Env.add_cast id env)
-    | VS_extern_no_rename (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ, env)
-    | VS_extern_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, _) -> (id, quants, typ, env) in
+    | VS_extern_no_rename (TypSchm_aux (TypSchm_ts (quants, typ), _), id) ->
+      let env = Env.add_extern id (string_of_id id) env in
+      (id, quants, typ, env)
+    | VS_extern_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, ext) ->
+      let env = Env.add_extern id ext env in
+      (id, quants, typ, env) in
   [DEF_spec (VS_aux (vs, (l, None)))], Env.add_val_spec id (quants, typ) env
 
 let check_default env (DT_aux (ds, l)) =
@@ -2957,7 +3031,11 @@ let check_type_union env variant typq (Tu_aux (tu, l)) =
   let ret_typ = app_typ variant (List.fold_left fold_union_quant [] (quant_items typq)) in
   match tu with
   | Tu_id v -> Env.add_union_id v (typq, ret_typ) env
-  | Tu_ty_id (typ, v) -> Env.add_val_spec v (typq, mk_typ (Typ_fn (typ, ret_typ, no_effect))) env
+  | Tu_ty_id (typ, v) ->
+     let typ' = mk_typ (Typ_fn (typ, ret_typ, no_effect)) in
+     env
+     |> Env.add_union_id v (typq, typ')
+     |> Env.add_val_spec v (typq, typ')
 
 let mk_synonym typq typ =
   let kopts, ncs = quant_split typq in
@@ -3012,7 +3090,8 @@ let rec check_def env def =
   | DEF_default default -> check_default env default
   | DEF_overload (id, ids) -> [DEF_overload (id, ids)], Env.add_overloads id ids env
   | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, _))) ->
-     [DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, None)))], Env.add_register id typ env
+     let env = Env.add_register id typ env in
+     [DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, Some (env, typ, no_effect))))], env
   | DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err ()
   | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err ()
   | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker")
diff --git a/src/type_check.mli b/src/type_check.mli
index de825d06..0a85624c 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -101,6 +101,10 @@ module Env : sig
 
   val get_overloads : id -> t -> id list
 
+  val is_extern : id -> t -> bool
+
+  val get_extern : id -> t -> string
+
   (* Lookup id searchs for a specified id in the environment, and
      returns it's type and what kind of identifier it is, using the
      lvar type. Returns Unbound if the identifier is unbound, and