Merge branch 'experiments' into mono-experiments

18 files changed, 1302 insertions, 1652 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/lexer2.mll b/src/lexer2.mll
index 561adcfd..a51067aa 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -49,37 +49,50 @@ let r = fun s -> s (* Ulib.Text.of_latin1 *)
 (* Available as Scanf.unescaped since OCaml 4.0 but 3.12 is still common *)
 let unescaped s = Scanf.sscanf ("\"" ^ s ^ "\"") "%S%!" (fun x -> x)
 
+let mk_operator n op =
+  match n with
+  | 0 -> Op0 op
+  | 1 -> Op1 op
+  | 2 -> Op2 op
+  | 3 -> Op3 op
+  | 4 -> Op4 op
+  | 5 -> Op5 op
+  | 6 -> Op6 op
+  | 7 -> Op7 op
+  | 8 -> Op8 op
+  | 9 -> Op9 op
+
+let operators = ref M.empty
+
 let kw_table =
   List.fold_left
     (fun r (x,y) -> M.add x y r)
     M.empty
     [
      ("and",                     (fun _ -> And));
-     ("alias",                   (fun _ -> Alias));
      ("as",                      (fun _ -> As));
      ("assert",                  (fun _ -> Assert));
      ("bitzero",                 (fun _ -> Bitzero));
      ("bitone",                  (fun _ -> Bitone));
-     ("bits",                    (fun _ -> Bits));
      ("by",                      (fun _ -> By));
-     ("case",			 (fun _ -> Case));
+     ("match",			 (fun _ -> Match));
      ("clause",                  (fun _ -> Clause));
      ("const",			 (fun _ -> Const));
      ("dec",                     (fun _ -> Dec));
      ("def",                     (fun _ -> Def));
+     ("op",                      (fun _ -> Op));
      ("default",		 (fun _ -> Default));
      ("deinfix",                 (fun _ -> Deinfix));
      ("effect",                  (fun _ -> Effect));
      ("Effect",                  (fun _ -> EFFECT));
      ("end",                     (fun _ -> End));
-     ("enumerate",		 (fun _ -> Enumerate));
+     ("enum",		         (fun _ -> Enum));
      ("else",                    (fun _ -> Else));
      ("exit",                    (fun _ -> Exit));
      ("extern",                  (fun _ -> Extern));
      ("cast",                    (fun _ -> Cast));
      ("false",                   (fun _ -> False));
      ("forall",                  (fun _ -> Forall));
-     ("exist",                   (fun _ -> Exist));
      ("foreach",                 (fun _ -> Foreach));
      ("function",                (fun x -> Function_));
      ("overload",                (fun _ -> Overload));
@@ -89,8 +102,7 @@ let kw_table =
      ("IN",                      (fun x -> IN));
      ("let",                     (fun x -> Let_));
      ("member",                  (fun x -> Member));
-     ("Nat",                     (fun x -> Nat));
-     ("Num",                     (fun x -> NatNum));
+     ("Int",                     (fun x -> Int));
      ("Order",                   (fun x -> Order));
      ("pure",                    (fun x -> Pure));
      ("rec",			 (fun x -> Rec));
@@ -104,7 +116,7 @@ let kw_table =
      ("then",                    (fun x -> Then));
      ("true",                    (fun x -> True));
      ("Type",                    (fun x -> TYPE));
-     ("typedef",		 (fun x -> Typedef));
+     ("type",		         (fun x -> Typedef));
      ("undefined",               (fun x -> Undefined));
      ("union",			 (fun x -> Union));
      ("with",                    (fun x -> With));
@@ -160,158 +172,51 @@ rule token = parse
   | "\n"
     { Lexing.new_line lexbuf;
       token lexbuf }
-
   | "&"					{ (Amp(r"&")) }
-  | "@"					{ (At(r"@")) }
   | "|"                                 { Bar }
-  | "^"					{ (Carrot(r"^")) }
+  | "2" ws "^"                          { TwoCaret }
+  | "^"					{ (Caret(r"^")) }
   | ":"                                 { Colon(r ":") }
   | ","                                 { Comma }
   | "."                                 { Dot }
   | "="                                 { (Eq(r"=")) }
-  | "!"					{ (Excl(r"!")) }
   | ">"					{ (Gt(r">")) }
   | "-"					{ Minus }
   | "<"					{ (Lt(r"<")) }
   | "+"					{ (Plus(r"+")) }
   | ";"                                 { Semi }
   | "*"                                 { (Star(r"*")) }
-  | "~"					{ (Tilde(r"~")) }
   | "_"                                 { Under }
   | "{"                                 { Lcurly }
   | "}"                                 { Rcurly }
+  | "()"                                { Unit(r"()") }
   | "("                                 { Lparen }
   | ")"                                 { Rparen }
   | "["                                 { Lsquare }
   | "]"                                 { Rsquare }
-  | "&&" as i                           { (AmpAmp(r i)) }
-  | "||"                                { BarBar }
-  | "||]"                               { BarBarSquare }
-  | "|]"				{ BarSquare }
-  | "^^"				{ (CarrotCarrot(r"^^")) }
-  | "::" as i                           { (ColonColon(r i)) }
-  | ":="                                { ColonEq }
-  | ":>"                                { ColonGt }
-  | ":]"                                { ColonSquare }
-  | ".."				{ DotDot }
-  | "=="				{ (EqEq(r"==")) }
   | "!="				{ (ExclEq(r"!=")) }
-  | "!!"				{ (ExclExcl(r"!!")) }
   | ">="				{ (GtEq(r">=")) }
-  | ">=+"				{ (GtEqPlus(r">=+")) }
-  | ">>"				{ (GtGt(r">>")) }
-  | ">>>"				{ (GtGtGt(r">>>")) }
-  | ">+"				{ (GtPlus(r">+")) }
-  | "#>>"				{ (HashGtGt(r"#>>")) }
-  | "#<<"				{ (HashLtLt(r"#<<")) }
   | "->"                                { MinusGt }
-  | "<:"                                { LtColon }
+  | "=>"                                { EqGt(r "=>") }
   | "<="				{ (LtEq(r"<=")) }
-  | "<=+"				{ (LtEqPlus(r"<=+")) }
-  | "<>"				{ (LtGt(r"<>")) }
-  | "<<"				{ (LtLt(r"<<")) }
-  | "<<<"				{ (LtLtLt(r"<<<")) }
-  | "<+"				{ (LtPlus(r"<+")) }
-  | "**"				{ (StarStar(r"**")) }
-  | "[|"                                { SquareBar }
-  | "[||"                               { SquareBarBar }
-  | "[:"                                { SquareColon }
-  | "~^"				{ (TildeCarrot(r"~^")) }
-
-  | "+_s"                               { (PlusUnderS(r"+_s")) }
-  | "-_s"                               { (MinusUnderS(r"-_s")) }
-  | ">=_s"				{ (GtEqUnderS(r">=_s")) }
-  | ">=_si"				{ (GtEqUnderSi(r">=_si")) }
-  | ">=_u"				{ (GtEqUnderU(r">=_u")) }
-  | ">=_ui"				{ (GtEqUnderUi(r">=_ui")) }
-  | ">>_u"				{ (GtGtUnderU(r">>_u")) }
-  | ">_s"				{ (GtUnderS(r">_s")) }
-  | ">_si"				{ (GtUnderSi(r">_si")) }
-  | ">_u"				{ (GtUnderU(r">_u")) }
-  | ">_ui"				{ (GtUnderUi(r">_ui")) }
-  | "<=_s"				{ (LtEqUnderS(r"<=_s")) }
-  | "<=_si"				{ (LtEqUnderSi(r"<=_si")) }
-  | "<=_u"				{ (LtEqUnderU(r"<=_u")) }
-  | "<=_ui"				{ (LtEqUnderUi(r"<=_ui")) }
-  | "<_s"				{ (LtUnderS(r"<_s")) }
-  | "<_si"				{ (LtUnderSi(r"<_si")) }
-  | "<_u"				{ (LtUnderU(r"<_u")) }
-  | "<_ui"				{ (LtUnderUi(r"<_ui")) }
-  | "*_s"                               { (StarUnderS(r"*_s")) }
-  | "**_s"				{ (StarStarUnderS(r"**_s")) }
-  | "**_si"				{ (StarStarUnderSi(r"**_si")) }
-  | "*_u"				{ (StarUnderU(r"*_u")) }
-  | "*_ui"				{ (StarUnderUi(r"*_ui")) }
-  | "2^"				{ (TwoCarrot(r"2^")) }
-  | "2**"				{ TwoStarStar }
-
-
+  | "infix" ws (digit as p) ws (oper_char+ as op)
+    { operators := M.add op (mk_operator (int_of_string (Char.escaped p)) op) !operators;
+      token lexbuf }
+  | oper_char+ as op
+    { try M.find op !operators
+      with Not_found -> raise (LexError ("Operator fixity undeclared", Lexing.lexeme_start_p lexbuf)) }
   | "(*"        { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
   | "*)"        { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
-
+  | (tyvar_start startident ident* as i) ":" { TyDecl(r i) }
+  | (startident ident* as i) ":"        { Decl(r i) }
   | tyvar_start startident ident* as i  { TyVar(r i) }
   | startident ident* as i              { if M.mem i kw_table then
                                             (M.find i kw_table) ()
-                                          else if
+					  (* else if
                                             List.mem i default_type_names ||
                                             List.mem i !custom_type_names then
-					    TyId(r i)
-                                          else Id(r i) }
-  | "&" oper_char+ as i                 { (AmpI(r i)) }
-  | "@" oper_char+ as i                 { (AtI(r i)) }
-  | "^" oper_char+ as i                 { (CarrotI(r i)) }
-  | "/" oper_char+ as i                 { (DivI(r i)) }
-  | "=" oper_char+ as i			{ (EqI(r i)) }
-  | "!" oper_char+ as i                 { (ExclI(r i)) }
-  | ">" oper_char+ as i                 { (GtI(r i)) }
-  | "<" oper_char+ as i			{ (LtI(r i)) }
-  | "+"	oper_char+ as i			{ (PlusI(r i)) }
-  | "*" oper_char+ as i                 { (StarI(r i)) }
-  | "~"	oper_char+ as i			{ (TildeI(r i)) }
-  | "&&" oper_char+ as i                { (AmpAmpI(r i)) }
-  | "^^" oper_char+ as i		{ (CarrotCarrotI(r i)) }
-  | "::" oper_char+ as i                { (ColonColonI(r i)) }
-  | "==" oper_char+ as i		{ (EqEqI(r i)) }
-  | "!=" oper_char+ as i		{ (ExclEqI(r i)) }
-  | "!!" oper_char+ as i		{ (ExclExclI(r i)) }
-  | ">=" oper_char+ as i		{ (GtEqI(r i)) }
-  | ">=+" oper_char+ as i		{ (GtEqPlusI(r i)) }
-  | ">>" oper_char+ as i		{ (GtGtI(r i)) }
-  | ">>>" oper_char+ as i		{ (GtGtGtI(r i)) }
-  | ">+" oper_char+ as i		{ (GtPlusI(r i)) }
-  | "#>>" oper_char+ as i		{ (HashGtGt(r i)) }
-  | "#<<" oper_char+ as i		{ (HashLtLt(r i)) }
-  | "<=" oper_char+ as i		{ (LtEqI(r i)) }
-  | "<=+" oper_char+ as i		{ (LtEqPlusI(r i)) }
-  | "<<" oper_char+ as i		{ (LtLtI(r i)) }
-  | "<<<" oper_char+ as i		{ (LtLtLtI(r i)) }
-  | "<+" oper_char+ as i		{ (LtPlusI(r i)) }
-  | "**" oper_char+ as i		{ (StarStarI(r i)) }
-  | "~^" oper_char+ as i		{ (TildeCarrot(r i)) }
-
-  | ">=_s" oper_char+ as i				{ (GtEqUnderSI(r i)) }
-  | ">=_si" oper_char+ as i				{ (GtEqUnderSiI(r i)) }
-  | ">=_u" oper_char+ as i				{ (GtEqUnderUI(r i)) }
-  | ">=_ui" oper_char+ as i				{ (GtEqUnderUiI(r i)) }
-  | ">>_u" oper_char+ as i				{ (GtGtUnderUI(r i)) }
-  | ">_s" oper_char+ as i				{ (GtUnderSI(r i)) }
-  | ">_si" oper_char+ as i				{ (GtUnderSiI(r i)) }
-  | ">_u" oper_char+ as i				{ (GtUnderUI(r i)) }
-  | ">_ui" oper_char+ as i				{ (GtUnderUiI(r i)) }
-  | "<=_s" oper_char+ as i				{ (LtEqUnderSI(r i)) }
-  | "<=_si" oper_char+ as i				{ (LtEqUnderSiI(r i)) }
-  | "<=_u" oper_char+ as i				{ (LtEqUnderUI(r i)) }
-  | "<=_ui" oper_char+ as i				{ (LtEqUnderUiI(r i)) }
-  | "<_s" oper_char+ as i				{ (LtUnderSI(r i)) }
-  | "<_si" oper_char+ as i				{ (LtUnderSiI(r i)) }
-  | "<_u" oper_char+ as i				{ (LtUnderUI(r i)) }
-  | "<_ui" oper_char+ as i				{ (LtUnderUiI(r i)) }
-  | "**_s" oper_char+ as i				{ (StarStarUnderSI(r i)) }
-  | "**_si" oper_char+ as i				{ (StarStarUnderSiI(r i)) }
-  | "*_u" oper_char+ as i				{ (StarUnderUI(r i)) }
-  | "*_ui" oper_char+ as i				{ (StarUnderUiI(r i)) }
-  | "2^" oper_char+ as i				{ (TwoCarrotI(r i)) }
-
+					    TyId(r i) *)
+					  else Id(r i) }
   | (digit+ as i1) "." (digit+ as i2)     { (Real (i1 ^ "." ^ i2)) }
   | "-" (digit* as i1) "." (digit+ as i2) { (Real ("-" ^ i1 ^ "." ^ i2)) }
   | digit+ as i                           { (Num(int_of_string i)) }
diff --git a/src/parser2.mly b/src/parser2.mly
index d6da6e63..c67fad59 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -46,96 +46,84 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *)
 
 open Parse_ast
 
-let loc () = Range(Parsing.symbol_start_pos(),Parsing.symbol_end_pos())
-let locn m n = Range(Parsing.rhs_start_pos m,Parsing.rhs_end_pos n)
-
-let idl i = Id_aux(i, loc())
-
-let efl e = BE_aux(e, loc())
-
-let ploc p = P_aux(p,loc ())
-let eloc e = E_aux(e,loc ())
-let peloc pe = Pat_aux(pe,loc ())
-let lbloc lb = LB_aux(lb,loc ())
-
-let bkloc k = BK_aux(k,loc ())
-let kloc k = K_aux(k,loc ())
-let kiloc ki = KOpt_aux(ki,loc ())
-let tloc t = ATyp_aux(t,loc ())
-let tlocl t l1 l2 = ATyp_aux(t,locn l1 l2)
-let lloc l = L_aux(l,loc ())
-let ploc p = P_aux(p,loc ())
-let fploc p = FP_aux(p,loc ())
-
-let funclloc f = FCL_aux(f,loc ())
-let typql t = TypQ_aux(t, loc())
-let irloc r = BF_aux(r, loc())
-let defloc df = DT_aux(df, loc())
-
-let tdloc td = TD_aux(td, loc())
-let kdloc kd = KD_aux(kd, loc())
-let funloc fn = FD_aux(fn, loc())
-let vloc v = VS_aux(v, loc ())
-let sdloc sd = SD_aux(sd, loc ())
-let dloc d = d
-
-let mk_typschm tq t s e = TypSchm_aux((TypSchm_ts(tq,t)),(locn s e))
-let mk_rec i = (Rec_aux((Rec_rec), locn i i))
-let mk_recn _ = (Rec_aux((Rec_nonrec), Unknown))
-let mk_typqn _ = (TypQ_aux(TypQ_no_forall,Unknown))
-let mk_tannot tq t s e = Typ_annot_opt_aux(Typ_annot_opt_some(tq,t),(locn s e))
-let mk_tannotn _ = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
-let mk_eannot e i = Effect_opt_aux((Effect_opt_effect(e)),(locn i i))
-let mk_eannotn _ = Effect_opt_aux(Effect_opt_pure,Unknown)
-let mk_namesectn _ = Name_sect_aux(Name_sect_none,Unknown)
-
-let make_range_sugar_bounded typ1 typ2 =
-  ATyp_app(Id_aux(Id("range"),Unknown),[typ1; typ2;])
-let make_range_sugar typ1 =
-  make_range_sugar_bounded (ATyp_aux(ATyp_constant(0), Unknown)) typ1
-let make_atom_sugar typ1 =
-  ATyp_app(Id_aux(Id("atom"),Unknown),[typ1])
-
-let make_r bot top =
-  match bot,top with
-    | ATyp_aux(ATyp_constant b,_),ATyp_aux(ATyp_constant t,l) ->
-      ATyp_aux(ATyp_constant ((t-b)+1),l)
-    | bot,(ATyp_aux(_,l) as top) ->
-      ATyp_aux((ATyp_sum ((ATyp_aux (ATyp_sum (top, ATyp_aux(ATyp_constant 1,Unknown)), Unknown)),
-			  (ATyp_aux ((ATyp_neg bot),Unknown)))), l)				   
-
-let make_vector_sugar_bounded order_set is_inc name typ typ1 typ2 = 
-  let (rise,ord,name) = 
-    if order_set 
-    then if is_inc 
-      then (make_r typ1 typ2,ATyp_inc,name) 
-      else (make_r typ2 typ1,ATyp_dec,name) 
-    else if name = "vector" 
-    then (typ2, ATyp_default_ord,"vector_sugar_tb") (* rise not calculated, but top and bottom came from specification *)
-    else (typ2, ATyp_default_ord,"vector_sugar_r") (* rise and base not calculated, rise only from specification *) in
-  ATyp_app(Id_aux(Id(name),Unknown),[typ1;rise;ATyp_aux(ord,Unknown);typ])
-let make_vector_sugar order_set is_inc typ typ1 =
-  let zero = (ATyp_aux(ATyp_constant 0,Unknown)) in
-  let (typ1,typ2) = match (order_set,is_inc,typ1) with
-    | (true,true,ATyp_aux(ATyp_constant t,l)) -> zero,ATyp_aux(ATyp_constant (t-1),l)
-    | (true,true,ATyp_aux(_, l)) -> zero,ATyp_aux (ATyp_sum (typ1,
-    ATyp_aux(ATyp_neg(ATyp_aux(ATyp_constant 1,Unknown)), Unknown)), l)
-    | (true,false,_) -> typ1,zero 
-    | (false,_,_) -> zero,typ1 in
-  make_vector_sugar_bounded order_set is_inc "vector_sugar_r" typ typ1 typ2
+let loc n m = Range (m, n)
+
+let mk_id i n m = Id_aux (i, loc m n)
+let mk_kid str n m = Kid_aux (Var str, loc n m)
+
+let deinfix (Id_aux (Id v, l)) = Id_aux (DeIid v, l)
+
+let mk_typ t n m = ATyp_aux (t, loc n m)
+let mk_pat p n m = P_aux (p, loc n m)
+let mk_pexp p n m = Pat_aux (p, loc n m)
+let mk_exp e n m = E_aux (e, loc n m)
+let mk_lit l n m = L_aux (l, loc n m)
+let mk_lit_exp l n m = mk_exp (E_lit (mk_lit l n m)) n m
+let mk_typschm tq t n m = TypSchm_aux (TypSchm_ts (tq, t), loc n m)
+let mk_nc nc n m = NC_aux (nc, loc n m)
+
+let mk_funcl f n m = FCL_aux (f, loc n m)
+let mk_fun fn n m = FD_aux (fn, loc n m)
+let mk_td t n m = TD_aux (t, loc n m)
+let mk_vs v n m = VS_aux (v, loc n m)
+let mk_reg_dec d n m = DEC_aux (d, loc n m)
+
+let qi_id_of_kopt (KOpt_aux (kopt_aux, l) as kopt) = QI_aux (QI_id kopt, l)
+
+let mk_recn = (Rec_aux((Rec_nonrec), Unknown))
+let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown))
+let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
+let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown)
+let mk_namesectn = Name_sect_aux(Name_sect_none,Unknown)
+
+type lchain =
+  LC_lt
+| LC_lteq
+| LC_nexp of atyp
+
+let rec desugar_lchain chain s e =
+  match chain with
+  | [LC_nexp n1; LC_lteq; LC_nexp n2] ->
+    mk_nc (NC_bounded_le (n1, n2)) s e
+  | [LC_nexp n1; LC_lt; LC_nexp n2] ->
+    mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant 1) s e)) s e, n2)) s e
+  | (LC_nexp n1 :: LC_lteq :: LC_nexp n2 :: chain) ->
+    let nc1 = mk_nc (NC_bounded_le (n1, n2)) s e in
+    mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e
+  | (LC_nexp n1 :: LC_lt :: LC_nexp n2 :: chain) ->
+    let nc1 = mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant 1) s e)) s e, n2)) s e in
+    mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e
+  | _ -> assert false
+
+type rchain =
+  RC_gt
+| RC_gteq
+| RC_nexp of atyp
+
+let rec desugar_rchain chain s e =
+  match chain with
+  | [RC_nexp n1; RC_gteq; RC_nexp n2] ->
+    mk_nc (NC_bounded_ge (n1, n2)) s e
+  | [RC_nexp n1; RC_gt; RC_nexp n2] ->
+    mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant 1) s e)) s e)) s e
+  | (RC_nexp n1 :: RC_gteq :: RC_nexp n2 :: chain) ->
+    let nc1 = mk_nc (NC_bounded_ge (n1, n2)) s e in
+    mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e
+  | (RC_nexp n1 :: RC_gt :: RC_nexp n2 :: chain) ->
+    let nc1 = mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant 1) s e)) s e)) s e in
+    mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e
+  | _ -> assert false
 
 %}
 
 /*Terminals with no content*/
 
-%token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Def Default Deinfix Effect EFFECT End 
-%token Enumerate Else Exit Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast
-%token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
+%token And As Assert Bitzero Bitone Bits By Match Clause Const Dec Def Default Deinfix Effect EFFECT End Op
+%token Enum Else Exit Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Int Order Cast
+%token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoCaret Type TYPE Typedef
 %token Undefined Union With When Val Constraint
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 
-
-/* Avoid shift/reduce conflict - see right_atomic_exp rule */
 %nonassoc Then
 %nonassoc Else
 
@@ -148,1203 +136,531 @@ let make_vector_sugar order_set is_inc typ typ1 =
 
 /*Terminals with content*/
 
-%token <string> Id TyVar TyId
+%token <string> Id TyVar Decl TyDecl
 %token <int> Num
 %token <string> String Bin Hex Real
 
-%token <string> Amp At Carrot  Div Eq Excl Gt Lt Plus Star Tilde
-%token <string> AmpAmp CarrotCarrot Colon ColonColon EqEq ExclEq ExclExcl
+%token <string> Amp At Caret Div Eq Excl Gt Lt Plus Star Tilde EqGt Unit
+%token <string> Colon ExclEq
 %token <string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt
-%token <string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot
+%token <string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar
 
 %token <string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS
 %token <string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU
 %token <string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS
-%token <string> StarUnderSi StarUnderU StarUnderUi TwoCarrot PlusUnderS MinusUnderS 
-
-%token <string> AmpI AtI CarrotI  DivI EqI ExclI GtI LtI PlusI StarI TildeI
-%token <string> AmpAmpI CarrotCarrotI ColonColonI EqEqI ExclEqI ExclExclI
-%token <string> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI
-%token <string> LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI
-
-%token <string> GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI
-%token <string> GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI
-%token <string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarStarUnderSI StarStarUnderSiI StarUnderSI
-%token <string> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI
+%token <string> StarUnderSi StarUnderU StarUnderUi PlusUnderS MinusUnderS
 
+%token <string> Op0 Op1 Op2 Op3 Op4 Op5 Op6 Op7 Op8 Op9
 
-%start file nonempty_exp_list
+%start file
 %type <Parse_ast.defs> defs
-%type <Parse_ast.atyp> typ
-%type <Parse_ast.pat> pat
-%type <Parse_ast.exp> exp
-%type <Parse_ast.exp list> nonempty_exp_list
 %type <Parse_ast.defs> file
 
-
 %%
 
 id:
   | Id
-    { idl (Id($1)) }
-  | Tilde
-    { idl (Id($1)) }
-  | Lparen Deinfix Amp Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix At Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Carrot Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Div Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Quot Rparen
-    { idl (DeIid("quot")) }
-  | Lparen Deinfix QuotUnderS Rparen
-    { idl (DeIid("quot_s")) }
-  | Lparen Deinfix Eq Rparen
-    { Id_aux(DeIid($3),loc ()) }
-  | Lparen Deinfix Excl Lparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Gt Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Lt Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix GtUnderS Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix LtUnderS Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Minus Rparen
-    { idl (DeIid("-")) }
-  | Lparen Deinfix MinusUnderS Rparen
-    { idl (DeIid("-_s")) }
-  | Lparen Deinfix Mod Rparen
-    { idl (DeIid("mod")) }
-  | Lparen Deinfix Plus Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix PlusUnderS Rparen
-    { idl (DeIid("+_s")) }
-  | Lparen Deinfix Star Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix StarUnderS Rparen
-    { idl (DeIid("*_s")) }
-  | Lparen Deinfix AmpAmp Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Bar Rparen
-    { idl (DeIid("|")) }
-  | Lparen Deinfix BarBar Rparen
-    { idl (DeIid("||")) }
-  | Lparen Deinfix CarrotCarrot Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Colon Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix ColonColon Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix EqEq Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix ExclEq Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix ExclExcl Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix GtEq Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix GtEqUnderS Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix GtEqPlus Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix GtGt Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix GtGtGt Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix GtPlus Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix HashGtGt Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix HashLtLt Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix LtEq Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix LtEqUnderS Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix LtLt Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix LtLtLt Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix LtPlus Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix StarStar Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Tilde Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix TildeCarrot Rparen
-    { idl (DeIid($3)) }
-
-tid:
-  | TyId
-    { (idl (Id($1))) }
-
-tyvar:
-  | TyVar
-    { (Kid_aux((Var($1)),loc ())) }
-
-tyvars:
-  | tyvar
+    { mk_id (Id $1) $startpos $endpos }
+  | Op Op1
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op2
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op3
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op4
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op5
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op6
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op7
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op8
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op9
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Plus
+    { mk_id (DeIid "+") $startpos $endpos }
+  | Op Minus
+    { mk_id (DeIid "-") $startpos $endpos }
+  | Op Star
+    { mk_id (DeIid "*") $startpos $endpos }
+
+op0: Op0 { mk_id (Id $1) $startpos $endpos }
+op1: Op1 { mk_id (Id $1) $startpos $endpos }
+op2: Op2 { mk_id (Id $1) $startpos $endpos }
+op3: Op3 { mk_id (Id $1) $startpos $endpos }
+op4: Op4 { mk_id (Id $1) $startpos $endpos }
+op5: Op5 { mk_id (Id $1) $startpos $endpos }
+op6: Op6 { mk_id (Id $1) $startpos $endpos }
+op7: Op7 { mk_id (Id $1) $startpos $endpos }
+op8: Op8 { mk_id (Id $1) $startpos $endpos }
+op9: Op9 { mk_id (Id $1) $startpos $endpos }
+
+decl:
+  | Decl
+    { mk_id (Id $1) $startpos $endpos }
+
+id_list:
+  | id
     { [$1] }
-  | tyvar tyvars
-    { $1 :: $2 }
+  | id Comma id_list
+    { $1 :: $3 }
 
-atomic_kind:
-  | TYPE
-    { bkloc BK_type }
-  | Nat
-    { bkloc BK_nat }
-  | NatNum
-    { bkloc BK_nat }
-  | Order
-    { bkloc BK_order }
-  | EFFECT
-    { bkloc BK_effect }
+kid:
+  | TyVar
+    { mk_kid $1 $startpos $endpos }
 
-kind_help:
-  | atomic_kind
-    { [ $1 ] }
-  | atomic_kind MinusGt kind_help
-    { $1::$3 }
+tydecl:
+  | TyDecl
+    { mk_kid $1 $startpos $endpos }
 
-kind:
-  | kind_help
-    { K_aux(K_kind($1), loc ()) }
-
-effect:
-  | Barr
-    { efl BE_barr }
-  | Depend
-    { efl BE_depend }
-  | Rreg 
-    { efl BE_rreg }
-  | Wreg
-    { efl BE_wreg }
-  | Rmem
-    { efl BE_rmem } 
-  | Rmemt
-    { efl BE_rmemt } 
-  | Wmem
-    { efl BE_wmem }
-  | Wmv
-    { efl BE_wmv }
-  | Wmvt
-    { efl BE_wmvt }
-  | Eamem
-    { efl BE_eamem }
-  | Exmem
-    { efl BE_exmem }
-  | Undef
-    { efl BE_undef }
-  | Unspec
-    { efl BE_unspec }
-  | Nondet
-      { efl BE_nondet }
-  | Escape
-      { efl BE_escape }
-
-effect_list:
-  | effect
+kid_list:
+  | kid
     { [$1] }
-  | effect Comma effect_list
-    { $1::$3 }
-
-effect_typ:
-  | Lcurly effect_list Rcurly
-    { tloc (ATyp_set($2)) }
-  | Pure
-    { tloc (ATyp_set([])) }
-
-vec_typ:
-  | tid Lsquare nexp_typ Rsquare
-      { tloc (make_vector_sugar false false (ATyp_aux ((ATyp_id $1), locn 1 1)) $3) }
-  | tid Lsquare nexp_typ Colon nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded false false "vector" (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
-  | tid Lsquare nexp_typ LtColon nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded true true "vector" (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
-  | tid Lsquare nexp_typ ColonGt nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded true false "vector" (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
-  | tyvar Lsquare nexp_typ Rsquare
-      { tloc (make_vector_sugar false false (ATyp_aux ((ATyp_var $1), locn 1 1)) $3) }
-  | tyvar Lsquare nexp_typ Colon nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded false false "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
-  | tyvar Lsquare nexp_typ LtColon nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded true true "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
-  | tyvar Lsquare nexp_typ ColonGt nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded true false "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
-
-app_typs:
-  | atomic_typ
-    { [$1] }
-  | atomic_typ Comma app_typs
-    { $1::$3 }
+  | kid kid_list
+    { $1 :: $2 }
 
-atomic_typ:
-  | vec_typ
-    { $1 }
-  | range_typ
-    { $1 }
-  | nexp_typ
-    { $1 }
-  | Inc
-    { tloc (ATyp_inc) }
-  | Dec
-    { tloc (ATyp_dec) }
-  | tid Lt app_typs Gt
-    { tloc (ATyp_app($1,$3)) }
-  | Register Lt app_typs Gt
-    { tloc (ATyp_app(Id_aux(Id "register", locn 1 1),$3)) }
-
-range_typ:
-  | SquareBar nexp_typ BarSquare
-      { tloc (make_range_sugar $2) }
-  | SquareBar nexp_typ Colon nexp_typ BarSquare
-      { tloc (make_range_sugar_bounded $2 $4) }
-  | SquareColon nexp_typ ColonSquare
-      { tloc (make_atom_sugar $2) }
-
-nexp_typ:
-  | nexp_typ Plus nexp_typ2
-    { tloc (ATyp_sum ($1, $3)) }
-  | nexp_typ Minus nexp_typ2
-    { tloc (ATyp_minus ($1, $3)) }
-  | Minus nexp_typ2
-    { tloc (ATyp_neg $2) }
-  | nexp_typ2
+nc:
+  | nc Bar nc_and
+    { mk_nc (NC_or ($1, $3)) $startpos $endpos }
+  | nc_and
     { $1 }
 
-nexp_typ2:
-  | nexp_typ2 Star nexp_typ3
-    { tloc (ATyp_times ($1, $3)) }
-  | nexp_typ3
+nc_and:
+  | nc_and Amp atomic_nc
+    { mk_nc (NC_and ($1, $3)) $startpos $endpos }
+  | atomic_nc
     { $1 }
 
-nexp_typ3:
-  | TwoStarStar nexp_typ4
-     { tloc (ATyp_exp $2) }
-  | nexp_typ4
-     { $1 }
-
-nexp_typ4:
-  | Num
-    { tlocl (ATyp_constant $1) 1 1 }
-  | tid
-    { tloc (ATyp_id $1) }
-  | Lcurly id Rcurly
-    { tloc (ATyp_id $2) }
-  | tyvar
-    { tloc (ATyp_var $1) }
-  | Lparen exist_typ Rparen
+atomic_nc:
+  | True
+    { mk_nc NC_true $startpos $endpos }
+  | False
+    { mk_nc NC_false $startpos $endpos }
+  | typ Eq typ
+    { mk_nc (NC_fixed ($1, $3)) $startpos $endpos }
+  | typ ExclEq typ
+    { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
+  | nc_lchain
+    { desugar_lchain $1 $startpos $endpos }
+  | nc_rchain
+    { desugar_rchain $1 $startpos $endpos }
+  | Lparen nc Rparen
     { $2 }
+  | kid In Lcurly num_list Rcurly
+    { mk_nc (NC_nat_set_bounded ($1, $4)) $startpos $endpos }
 
-tup_typ_list:
-   | atomic_typ Comma atomic_typ
-       { [$1;$3] }
-   | atomic_typ Comma tup_typ_list
-       { $1::$3 }
-
-tup_typ:
-   | atomic_typ
-     { $1 }
-   | Lparen tup_typ_list Rparen
-     { tloc (ATyp_tup $2) }
-
-exist_typ:
-  | Exist tyvars Comma nexp_constraint Dot tup_typ
-    { tloc (ATyp_exist ($2, $4, $6)) }
-  | Exist tyvars Dot tup_typ
-    { tloc (ATyp_exist ($2, NC_aux (NC_true, loc ()), $4)) }
-  | tup_typ
-    { $1 }
+num_list:
+  | Num
+    { [$1] }
+  | Num Comma num_list
+    { $1 :: $3 }
+
+nc_lchain:
+  | typ LtEq typ
+    { [LC_nexp $1; LC_lteq; LC_nexp $3] }
+  | typ Lt typ
+    { [LC_nexp $1; LC_lt; LC_nexp $3] }
+  | typ LtEq nc_lchain
+    { LC_nexp $1 :: LC_lteq :: $3 }
+  | typ Lt nc_lchain
+    { LC_nexp $1 :: LC_lt :: $3 }
+
+nc_rchain:
+  | typ GtEq typ
+    { [RC_nexp $1; RC_gteq; RC_nexp $3] }
+  | typ Gt typ
+    { [RC_nexp $1; RC_gt; RC_nexp $3] }
+  | typ GtEq nc_rchain
+    { RC_nexp $1 :: RC_gteq :: $3 }
+  | typ Gt nc_rchain
+    { RC_nexp $1 :: RC_gt :: $3 }
 
 typ:
-  | exist_typ
+  | typ0
     { $1 }
-  | tup_typ MinusGt exist_typ Effect effect_typ
-    { tloc (ATyp_fn($1,$3,$5)) }
 
-lit:
-  | True
-    { lloc L_true }
-  | False
-    { lloc L_false }
-  | Num
-    { lloc (L_num $1) }
-  | String
-    { lloc (L_string $1) }
-  | Lparen Rparen
-    { lloc L_unit }
-  | Bin
-    { lloc (L_bin $1) }
-  | Hex
-    { lloc (L_hex $1) }
-  | Real
-    { lloc (L_real $1) }
-  | Undefined
-    { lloc L_undef }
-  | Bitzero
-    { lloc L_zero }
-  | Bitone
-    { lloc L_one }
+typ0:
+  | typ1 op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ1 { $1 }
 
-atomic_pat:
-  | lit
-    { ploc (P_lit $1) }
-  | Under
-    { ploc P_wild }
-  | Lparen pat As id Rparen
-    { ploc (P_as($2,$4)) }
-  | Lparen exist_typ Rparen atomic_pat
-    { ploc (P_typ($2,$4)) }
-  | id
-    { ploc (P_app($1,[])) }
-  | Lcurly fpats Rcurly
-    { ploc (P_record((fst $2, snd $2))) }
-  | Lsquare comma_pats Rsquare
-    { ploc (P_vector($2)) }
-  | Lsquare pat Rsquare
-    { ploc (P_vector([$2])) }
-  | Lsquare Rsquare
-    { ploc (P_vector []) }
-  | Lsquare npats Rsquare
-    { ploc (P_vector_indexed($2)) }
-  | Lparen comma_pats Rparen
-    { ploc (P_tup($2)) }
-  | SquareBarBar BarBarSquare
-    { ploc (P_list([])) }
-  | SquareBarBar pat BarBarSquare
-    { ploc (P_list([$2])) }
-  | SquareBarBar comma_pats BarBarSquare
-    { ploc (P_list($2)) }
-  | atomic_pat ColonColon pat
-    { ploc (P_cons ($1, $3)) }
-  | Lparen pat Rparen
-    { $2 }
+typ1:
+  | typ2 op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ2 { $1 }
 
-app_pat:
-  | atomic_pat
-    { $1 }
-  | id Lparen comma_pats Rparen
-    { ploc (P_app($1,$3)) }
-  | id Lparen pat Rparen
-    { ploc (P_app($1,[$3])) }
+typ2:
+  | typ3 op2 typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ3 { $1 }
 
-pat_colons:
-  | atomic_pat Colon atomic_pat
-    { ([$1;$3]) }
-  | atomic_pat Colon pat_colons
-    { ($1::$3) }
+typ3:
+  | typ4 op3 typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ4 { $1 }
 
-pat:
-  | app_pat
-    { $1 }
-  | pat_colons
-    { ploc (P_vector_concat($1)) }
-
-comma_pats:
-  | atomic_pat Comma atomic_pat
-    { [$1;$3] }
-  | atomic_pat Comma comma_pats
-    { $1::$3 }
-
-fpat:
-  | id Eq pat
-    { fploc (FP_Fpat($1,$3)) }
-
-fpats:
-  | fpat
-    { ([$1], false) }
-  | fpat Semi
-    { ([$1], true) }
-  | fpat Semi fpats
-    { ($1::fst $3, snd $3) }
-
-npat:
-  | Num Eq pat
-    { ($1,$3) }
-
-npats:
-  | npat
-    { [$1] }
-  | npat Comma npats
-    { ($1::$3) }
+typ4:
+  | typ5 op4 typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ5 { $1 }
 
-atomic_exp:
-  | Lcurly semi_exps Rcurly
-    { eloc (E_block $2) }
-  | Nondet Lcurly semi_exps Rcurly
-    { eloc (E_nondet $3) }
+typ5:
+  | typ6 op5 typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ6 { $1 }
+
+typ6:
+  | typ7 op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ6 Plus typ7 { mk_typ (ATyp_sum ($1, $3)) $startpos $endpos }
+  | typ6 Minus typ7 { mk_typ (ATyp_minus ($1, $3)) $startpos $endpos }
+  | typ7 { $1 }
+
+typ7:
+  | typ8 op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ7 Star typ8 { mk_typ (ATyp_times ($1, $3)) $startpos $endpos }
+  | typ8 { $1 }
+
+typ8:
+  | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+  | typ9 { $1 }
+
+typ9:
+  | atomic_typ op9 atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | atomic_typ { $1 }
+
+atomic_typ:
   | id
-    { eloc (E_id($1)) }
-  | lit
-    { eloc (E_lit($1)) }
-  | Lparen exp Rparen
+    { mk_typ (ATyp_id $1) $startpos $endpos }
+  | kid
+    { mk_typ (ATyp_var $1) $startpos $endpos }
+  | Num
+    { mk_typ (ATyp_constant $1) $startpos $endpos }
+  | Dec
+    { mk_typ ATyp_dec $startpos $endpos }
+  | Inc
+    { mk_typ ATyp_inc $startpos $endpos }
+  | id Lparen typ_list Rparen
+    { mk_typ (ATyp_app ($1, $3)) $startpos $endpos }
+  | Lparen typ Rparen
     { $2 }
-  | Lparen exist_typ Rparen atomic_exp
-    { eloc (E_cast($2,$4)) }
-  | Lparen comma_exps Rparen
-    { eloc (E_tuple($2)) }
-  | Lcurly exp With semi_exps Rcurly
-    { eloc (E_record_update($2,$4)) } 
-  | Lsquare Rsquare
-    { eloc (E_vector([])) }
-  | Lsquare exp Rsquare
-    { eloc (E_vector([$2])) }
-  | Lsquare comma_exps Rsquare
-    { eloc (E_vector($2)) }
-  | Lsquare comma_exps Semi Default Eq exp Rsquare
-    { eloc (E_vector_indexed($2,(Def_val_aux(Def_val_dec $6, locn 3 6)))) }
-  | Lsquare exp With atomic_exp Eq exp Rsquare
-    { eloc (E_vector_update($2,$4,$6)) }
-  | Lsquare exp With atomic_exp Colon atomic_exp Eq exp Rsquare
-    { eloc (E_vector_update_subrange($2,$4,$6,$8)) }
-  | SquareBarBar BarBarSquare
-      { eloc (E_list []) }
-  | SquareBarBar exp BarBarSquare
-      { eloc (E_list [$2]) }
-  | SquareBarBar comma_exps BarBarSquare
-    { eloc (E_list($2)) }
-  | Switch exp Lcurly case_exps Rcurly
-    { eloc (E_case($2,$4)) }
-  | Sizeof atomic_typ
-    { eloc (E_sizeof($2)) }
-  | Constraint Lparen nexp_constraint Rparen
-    { eloc (E_constraint $3) }
-  | Exit atomic_exp
-      { eloc (E_exit $2) }
-  | Return atomic_exp
-      { eloc (E_return $2) }
-  | Assert Lparen exp Comma exp Rparen
-      { eloc (E_assert ($3,$5)) }
-
-field_exp:
-  | atomic_exp
-    { $1 }
-  | atomic_exp Dot id
-    { eloc (E_field($1,$3)) }
-
-vaccess_exp:
-  | field_exp
-    { $1 }
-  | atomic_exp Lsquare exp Rsquare
-    { eloc (E_vector_access($1,$3)) }
-  | atomic_exp Lsquare exp DotDot exp Rsquare
-    { eloc (E_vector_subrange($1,$3,$5)) }
+  | Lparen typ Comma typ_list Rparen
+    { mk_typ (ATyp_tup ($2 :: $4)) $startpos $endpos }
+  | Lcurly kid_list Dot typ Rcurly
+    { mk_typ (ATyp_exist ($2, NC_aux (NC_true, loc $startpos $endpos), $4)) $startpos $endpos }
+  | Lcurly kid_list Comma nc Dot typ Rcurly
+    { mk_typ (ATyp_exist ($2, $4, $6)) $startpos $endpos }
+
+typ_list:
+  | typ
+    { [$1] }
+  | typ Comma typ_list
+    { $1 :: $3 }
 
-app_exp:
-  | vaccess_exp
-    { $1 }
-  | id Lparen Rparen
-    { eloc (E_app($1, [eloc (E_lit (lloc L_unit))])) }
-  /* we wrap into a tuple here, but this is unwrapped in initial_check.ml */
-  | id Lparen exp Rparen
-    { eloc (E_app($1,[ E_aux((E_tuple [$3]),locn 3 3)])) }
-  | id Lparen comma_exps Rparen
-    { eloc (E_app($1,[E_aux (E_tuple $3,locn 3 3)])) }
-
-right_atomic_exp:
-  | If_ exp Then exp Else exp
-    { eloc (E_if($2,$4,$6)) }
-  | If_ exp Then exp
-    { eloc (E_if($2,$4, eloc (E_lit(lloc L_unit)))) }
-  | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp In typ Rparen exp
-    { if $4 <> "from" then
-       raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop"));
-      if $6 <> "to" then
-       raise (Parse_error_locn ((loc ()),"Missing \"to\" in foreach loop"));
-      eloc (E_for($3,$5,$7,$9,$11,$13)) }
-  | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp Rparen exp
-    { if $4 <> "from" then
-       raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop"));
-      if $6 <> "to" && $6 <> "downto" then
-       raise (Parse_error_locn ((loc ()),"Missing \"to\" or \"downto\" in foreach loop"));
-      let order =
-        if $6 = "to"
-        then ATyp_aux(ATyp_inc,(locn 6 6))
-        else ATyp_aux(ATyp_dec,(locn 6 6)) in
-      eloc (E_for($3,$5,$7,$9,order,$11)) }
-  | Foreach Lparen id Id atomic_exp Id atomic_exp Rparen exp
-    { if $4 <> "from" then
-       raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop"));
-      if $6 <> "to" && $6 <> "downto" then
-       raise (Parse_error_locn ((loc ()),"Missing \"to\" or \"downto\" in foreach loop"));
-      let step = eloc (E_lit(lloc (L_num 1))) in
-      let ord =
-        if $6 = "to"
-        then ATyp_aux(ATyp_inc,(locn 6 6))
-        else ATyp_aux(ATyp_dec,(locn 6 6)) in
-      eloc (E_for($3,$5,$7,step,ord,$9)) }
-  | letbind In exp
-    { eloc (E_let($1,$3)) }
-
-starstar_exp:
-  | app_exp
-    { $1 }
-  | starstar_exp StarStar app_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-
-/* this is where we diverge from the non-right_atomic path;
-   here we go directly to right_atomic whereas the other one
-   goes through app_exp, vaccess_exp and field_exp too. */
-starstar_right_atomic_exp:
-  | right_atomic_exp
-    { $1 }
-  | starstar_exp StarStar right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+base_kind:
+  | Int
+    { BK_aux (BK_nat, loc $startpos $endpos) }
+  | TYPE
+    { BK_aux (BK_type, loc $startpos $endpos) }
+  | Order
+    { BK_aux (BK_order, loc $startpos $endpos) }
 
-star_exp:
-  | starstar_exp
-    { $1 }
-  | star_exp Star starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp Div starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp Div_ starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id("div"), locn 2 2), $3)) }
-  | star_exp Quot starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id("quot"), locn 2 2), $3)) }
-  | star_exp QuotUnderS starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id("quot_s"), locn 2 2), $3)) }
-  | star_exp Rem starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id("rem"), locn 2 2), $3)) }
-  | star_exp Mod starstar_exp
-      { eloc (E_app_infix($1,Id_aux(Id("mod"), locn 2 2), $3)) }
-  | star_exp ModUnderS starstar_exp
-      { eloc (E_app_infix($1,Id_aux(Id("mod_s"), locn 2 2), $3)) }
-  | star_exp StarUnderS starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp StarUnderSi starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp StarUnderU starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp StarUnderUi starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-
-star_right_atomic_exp:
-  | starstar_right_atomic_exp
-    { $1 }
-  | star_exp Star starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp Div starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp Div_ starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("div"), locn 2 2), $3)) }
-  | star_exp Quot starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("quot"), locn 2 2), $3)) }
-  | star_exp QuotUnderS starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("quot_s"), locn 2 2), $3)) }
-  | star_exp Rem starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("rem"), locn 2 2), $3)) }
-  | star_exp Mod starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("mod"), locn 2 2), $3)) }
-  | star_exp ModUnderS starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("mod_s"), locn 2 2), $3)) }
-  | star_exp StarUnderS starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp StarUnderSi starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp StarUnderU starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp StarUnderUi starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-
-plus_exp:
-  | star_exp
-    { $1 }
-  | plus_exp Plus star_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | plus_exp PlusUnderS star_exp
-    { eloc (E_app_infix($1, Id_aux(Id($2), locn 2 2), $3)) }
-  | plus_exp Minus star_exp
-    { eloc (E_app_infix($1,Id_aux(Id("-"), locn 2 2), $3)) }
-  | plus_exp MinusUnderS star_exp
-    { eloc (E_app_infix($1,Id_aux(Id("-_s"),locn 2 2), $3)) }
-
-plus_right_atomic_exp:
-  | star_right_atomic_exp
-    { $1 }
-  | plus_exp Plus star_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | plus_exp Minus star_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("-"), locn 2 2), $3)) }
-  | plus_exp PlusUnderS star_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | plus_exp MinusUnderS star_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("-_s"), locn 2 2), $3)) }
-
-shift_exp:
-  | plus_exp
-    { $1 }
-  | shift_exp GtGt plus_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | shift_exp GtGtGt plus_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | shift_exp LtLt plus_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | shift_exp LtLtLt plus_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-
-shift_right_atomic_exp:
-  | plus_right_atomic_exp
-    { $1 }
-  | shift_exp GtGt plus_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | shift_exp GtGtGt plus_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | shift_exp LtLt plus_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | shift_exp LtLtLt plus_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-
-
-cons_exp:
-  | shift_exp
-    { $1 }
-  | shift_exp ColonColon cons_exp
-    { eloc (E_cons($1,$3)) }
-  | shift_exp Colon cons_exp
-    { eloc (E_vector_append($1, $3)) }
+kind:
+  | base_kind
+    { K_aux (K_kind [$1], loc $startpos $endpos) }
+
+kopt:
+  | tydecl kind
+    { KOpt_aux (KOpt_kind ($2, $1), loc $startpos $endpos) }
+  | Lparen kid Colon kind Rparen
+    { KOpt_aux (KOpt_kind ($4, $2), loc $startpos $endpos) }
+  | kid
+    { KOpt_aux (KOpt_none $1, loc $startpos $endpos) }
+
+kopt_list:
+  | kopt
+    { [$1] }
+  | kopt kopt_list
+    { $1 :: $2 }
 
-cons_right_atomic_exp:
-  | shift_right_atomic_exp
-    { $1 }
-  | shift_exp ColonColon cons_right_atomic_exp
-    { eloc (E_cons($1,$3)) }
-  | shift_exp Colon cons_right_atomic_exp
-    { eloc (E_vector_append($1, $3)) }
+typquant:
+  | kopt_list Comma nc
+    { let qi_nc = QI_aux (QI_const $3, loc $startpos($3) $endpos($3)) in
+      TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1 @ [qi_nc]), loc $startpos $endpos) }
+  | kopt_list
+    { TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1), loc $startpos $endpos) }
+
+typschm:
+  | typ MinusGt typ
+    { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_fn ($1, $3, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos }
+  | Forall typquant Dot typ MinusGt typ
+    { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos }
 
-at_exp:
-  | cons_exp
-    { $1 }
-  | cons_exp At at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | cons_exp CarrotCarrot at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | cons_exp Carrot at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | cons_exp TildeCarrot at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-
-at_right_atomic_exp:
-  | cons_right_atomic_exp
-    { $1 }
-  | cons_exp At at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | cons_exp CarrotCarrot at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | cons_exp Carrot at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | cons_exp TildeCarrot at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-
-eq_exp:
-  | at_exp
-    { $1 }
-  /* XXX check for consistency */
-  | eq_exp Eq at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp EqEq at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp ExclEq at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtEq at_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtEqUnderS at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtEqUnderU at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp Gt at_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtUnderS at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtUnderU at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtEq at_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtEqUnderS at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp Lt at_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtUnderS at_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtUnderSi at_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtUnderU at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  /* XXX assignement should not have the same precedence as equal,
-  otherwise a := b > c requires extra parens... */
-  | eq_exp ColonEq at_exp
-    { eloc (E_assign($1,$3)) }
-
-eq_right_atomic_exp:
-  | at_right_atomic_exp
-    { $1 }
-  | eq_exp Eq at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp EqEq at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp ExclEq at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtEq at_right_atomic_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtEqUnderS at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtEqUnderU at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp Gt at_right_atomic_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtUnderS at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtUnderU at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtEq at_right_atomic_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtEqUnderS at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp Lt at_right_atomic_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtUnderS at_right_atomic_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtUnderSi at_right_atomic_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtUnderU at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp ColonEq at_right_atomic_exp
-    { eloc (E_assign($1,$3)) }
-
-and_exp:
-  | eq_exp
+pat:
+  | atomic_pat
     { $1 }
-  | eq_exp Amp and_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp AmpAmp and_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+  | atomic_pat As id
+    { mk_pat (P_as ($1, $3)) $startpos $endpos }
+  | Lparen pat Comma pat_list Rparen
+    { mk_pat (P_tup ($2 :: $4)) $startpos $endpos }
 
-and_right_atomic_exp:
-  | eq_right_atomic_exp
-    { $1 }
-  | eq_exp Amp and_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp AmpAmp and_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+pat_list:
+  | pat
+    { [$1] }
+  | pat Comma pat_list
+    { $1 :: $3 }
 
-or_exp:
-  | and_exp
-    { $1 }
-  | and_exp Bar or_exp
-    { eloc (E_app_infix($1,Id_aux(Id("|"), locn 2 2), $3)) }
-  | and_exp BarBar or_exp
-    { eloc (E_app_infix($1,Id_aux(Id("||"), locn 2 2), $3)) }
+atomic_pat:
+  | Under
+    { mk_pat (P_wild) $startpos $endpos }
+  | lit
+    { mk_pat (P_lit $1) $startpos $endpos }
+  | id
+    { mk_pat (P_id $1) $startpos $endpos }
+  | pat Colon typ
+    { mk_pat (P_typ ($3, $1)) $startpos $endpos }
+  | decl typ
+    { mk_pat (P_typ ($2, mk_pat (P_id $1) $startpos $endpos($1))) $startpos $endpos }
+  | Lparen pat Rparen
+    { $2 }
 
-or_right_atomic_exp:
-  | and_right_atomic_exp
-    { $1 }
-  | and_exp Bar or_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("|"), locn 2 2), $3)) }
-  | and_exp BarBar or_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("||"), locn 2 2), $3)) }
+lit:
+  | True
+    { mk_lit L_true $startpos $endpos }
+  | False
+    { mk_lit L_false $startpos $endpos }
+  | Unit
+    { mk_lit L_unit $startpos $endpos }
+  | Num
+    { mk_lit (L_num $1) $startpos $endpos }
+  | Undefined
+    { mk_lit L_undef $startpos $endpos }
 
 exp:
-  | or_exp
-    { $1 }
-  | or_right_atomic_exp
-    { $1 }
-
-comma_exps:
-  | exp Comma exp
-    { [$1;$3] }
-  | exp Comma comma_exps
-    { $1::$3 }
+  | cast_exp Colon typ
+    { mk_exp (E_cast ($3, $1)) $startpos $endpos }
+  | cast_exp
+    { $1 }
+
+cast_exp:
+  | exp0
+    { $1 }
+  | atomic_exp Eq cast_exp
+    { mk_exp (E_assign ($1, $3)) $startpos $endpos }
+  | Let_ letbind In cast_exp
+    { mk_exp (E_let ($2, $4)) $startpos $endpos }
+  | Lcurly block Rcurly
+    { mk_exp (E_block $2) $startpos $endpos }
+  | Return cast_exp
+    { mk_exp (E_return $2) $startpos $endpos }
+  | If_ exp Then cast_exp Else cast_exp
+    { mk_exp (E_if ($2, $4, $6)) $startpos $endpos }
+  | Match exp0 Lcurly case_list Rcurly
+    { mk_exp (E_case ($2, $4)) $startpos $endpos }
+  | Lparen exp Comma exp_list Rparen
+    { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos }
+
+exp0:
+  | exp1 op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp1 { $1 }
+
+exp1:
+  | exp2 op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp2 { $1 }
+
+exp2:
+  | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp3 { $1 }
+
+exp3:
+  | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp4 { $1 }
+
+exp4:
+  | exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp5 { $1 }
+
+exp5:
+  | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp6 { $1 }
+
+exp6:
+  | exp7 op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp6 Plus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "+") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp6 Minus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "-") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp7 { $1 }
+
+exp7:
+  | exp8 op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp7 Star exp8 { mk_exp (E_app_infix ($1, mk_id (Id "*") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp8 { $1 }
+
+exp8:
+  | exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos }
+  | exp9 { $1 }
+
+exp9:
+  | atomic_exp op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | atomic_exp { $1 }
+
+case:
+  | pat EqGt exp
+    { mk_pexp (Pat_exp ($1, $3)) $startpos $endpos }
+  | pat If_ exp EqGt exp
+    { mk_pexp (Pat_when ($1, $3, $5)) $startpos $endpos }
+
+case_list:
+  | case
+    { [$1] }
+  | case Comma case_list
+    { $1 :: $3 }
 
-semi_exps_help:
+block:
   | exp
     { [$1] }
-  | exp Semi
+  | If_ exp Then exp Semi block
+    { mk_exp (E_if ($2, $4, mk_lit_exp L_unit $startpos($5) $endpos($5))) $startpos $endpos($5) :: $6 }
+  | Let_ letbind Semi block
+    { [mk_exp (E_let ($2, mk_exp (E_block $4) $startpos($4) $endpos)) $startpos $endpos] }
+  | exp Semi /* Allow trailing semicolon in block */
     { [$1] }
-  | exp Semi semi_exps_help
-    { $1::$3 }
+  | exp Semi block
+    { $1 :: $3 }
 
-semi_exps:
-  |
-    { [] }
-  | semi_exps_help
-    { $1 }
+%inline letbind:
+  | pat Eq exp
+    { LB_aux (LB_val_implicit ($1, $3), loc $startpos $endpos) }
 
-case_exp:
-  | Case patsexp
+atomic_exp:
+  | lit
+    { mk_exp (E_lit $1) $startpos $endpos }
+  | decl atomic_typ
+    { mk_exp (E_cast ($2, mk_exp (E_id $1) $startpos $endpos($1))) $startpos $endpos }
+  | id
+    { mk_exp (E_id $1) $startpos $endpos }
+  | id Unit
+    { mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
+  | id Lparen exp_list Rparen
+    { mk_exp (E_app ($1, $3)) $startpos $endpos }
+  | Lparen exp Rparen
     { $2 }
 
-case_exps:
-  | case_exp
+exp_list:
+  | exp
     { [$1] }
-  | case_exp case_exps
-    { $1::$2 }
+  | exp Comma exp_list
+    { $1 :: $3 }
 
-patsexp:
-  | atomic_pat MinusGt exp
-    { peloc (Pat_exp($1,$3)) }
-  | atomic_pat When exp MinusGt exp
-    { peloc (Pat_when ($1, $3, $5)) }
-
-letbind:
-  | Let_ atomic_pat Eq exp
-    { lbloc (LB_val_implicit($2,$4)) }
-  | Let_ typquant atomic_typ atomic_pat Eq exp
-    { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,$6)) }
-/* This introduces one shift reduce conflict, that basically points out that an atomic_pat with a type declared is the Same as this
-  | Let_ Lparen typ Rparen atomic_pat Eq exp 
-    { assert false (* lbloc (LB_val_explicit((mk_typschm (mk_typqn ()) $2 2 2),$3,$5)) *)} */
+cast_exp_list:
+  | cast_exp
+    { [$1] }
+  | cast_exp Comma exp_list
+    { $1 :: $3 }
 
 funcl:
-  | id atomic_pat Eq exp
-    { funclloc (FCL_Funcl($1,$2,$4)) }
+  | id pat Eq exp
+    { mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos }
 
-funcl_ands:
-  | funcl
-    { [$1] }
-  | funcl And funcl_ands
-    { $1::$3 }
-
-/* This causes ambiguity because without a type quantifier it's unclear whether the first id is a function name or a type name for the optional types.*/
-fun_def:
-  | Function_ Rec typquant typ Effect effect_typ funcl_ands
-    { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $6 6, $7)) }
-  | Function_ Rec typquant typ funcl_ands
-    { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
-  | Function_ Rec typ Effect effect_typ funcl_ands
-    { funloc (FD_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $5 5, $6)) }
-  | Function_ Rec Effect effect_typ funcl_ands 
-    { funloc (FD_function(mk_rec 2,mk_tannotn (), mk_eannot $4 4, $5)) }
-  | Function_ Rec typ funcl_ands
-    { funloc (FD_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
-  | Function_ Rec funcl_ands
-    { funloc (FD_function(mk_rec 2, mk_tannotn (), mk_eannotn (), $3)) }
-  | Function_ typquant typ Effect effect_typ funcl_ands
-    { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $5 5, $6)) }
-  | Function_ typquant typ funcl_ands
-    { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) }
-  | Function_ typ Effect effect_typ funcl_ands
-    { funloc (FD_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $4 4, $5)) }
-  | Function_ Effect effect_typ funcl_ands
-    { funloc (FD_function(mk_recn (),mk_tannotn (), mk_eannot $3 3, $4)) }
-  | Function_ typ funcl_ands
-    { funloc (FD_function(mk_recn (),mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
-  | Function_ funcl_ands
-    { funloc (FD_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
-
-
-val_spec:
-  | Val typquant typ id
-    { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) }
-  | Val typ id
-    { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3)) }
-  | Val Cast typquant typ id
-    { vloc (VS_cast_spec (mk_typschm $3 $4 3 4,$5)) }
-  | Val Cast typ id
-    { vloc (VS_cast_spec (mk_typschm (mk_typqn ()) $3 3 3, $4)) }
-  | Val Extern typquant typ id
-    { vloc (VS_extern_no_rename (mk_typschm $3 $4 3 4,$5)) }
-  | Val Extern typ id
-    { vloc (VS_extern_no_rename (mk_typschm (mk_typqn ()) $3 3 3, $4)) }
-  | Val Extern typquant typ id Eq String
-    { vloc (VS_extern_spec (mk_typschm $3 $4 3 4,$5,$7)) }
-  | Val Extern typ id Eq String
-    { vloc (VS_extern_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, $6)) }
-
-kinded_id:
-  | tyvar
-    { kiloc (KOpt_none $1) }
-  | kind tyvar
-    { kiloc (KOpt_kind($1,$2))}
-
-/*kinded_ids:
-  | kinded_id
+type_def:
+  | Typedef id typquant Eq typ
+    { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm $3 $5 $startpos($3) $endpos)) $startpos $endpos }
+  | Typedef id Eq typ
+    { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm mk_typqn $4 $startpos($4) $endpos)) $startpos $endpos }
+  | Struct id typquant Eq Lcurly struct_fields Rcurly
+    { mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
+  | Enum id Eq enum_bar
+    { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos }
+  | Enum id Eq Lcurly enum Rcurly
+    { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos }
+  | Union id typquant Eq Lcurly type_unions Rcurly
+    { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
+
+enum_bar:
+  | id
     { [$1] }
-  | kinded_id kinded_ids
-    { $1::$2 }*/
+  | id Bar enum_bar
+    { $1 :: $3 }
 
-nums:
-  | Num
+enum:
+  | id
     { [$1] }
-  | Num Comma nums
-    { $1::$3 }
+  | id Comma enum
+    { $1 :: $3 }
 
-nexp_constraint:
-  | nexp_constraint1
-    { $1 }
-  | nexp_constraint1 Bar nexp_constraint
-    { NC_aux (NC_or ($1, $3), loc ()) }
+struct_field:
+  | decl typ
+    { ($2, $1) }
+  | id Colon typ
+    { ($3, $1) }
 
-nexp_constraint1:
-  | nexp_constraint2
-    { $1 }
-  | nexp_constraint2 Amp nexp_constraint1
-    { NC_aux (NC_and ($1, $3), loc ()) }
-
-nexp_constraint2:
-  | nexp_typ Eq nexp_typ
-    { NC_aux(NC_fixed($1,$3), loc () ) }
-  | nexp_typ ExclEq nexp_typ
-    { NC_aux (NC_not_equal ($1, $3), loc ()) }
-  | nexp_typ GtEq nexp_typ
-    { NC_aux(NC_bounded_ge($1,$3), loc () ) }
-  | nexp_typ LtEq nexp_typ
-    { NC_aux(NC_bounded_le($1,$3), loc () ) }
-  | tyvar In Lcurly nums Rcurly
-    { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
-  | tyvar IN Lcurly nums Rcurly
-    { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
-  | True
-    { NC_aux (NC_true, loc ()) }
-  | False
-    { NC_aux (NC_false, loc ()) }
-  | Lparen nexp_constraint Rparen
-    { $2 }
+struct_fields:
+  | struct_field
+    { [$1] }
+  | struct_field Comma
+    { [$1] }
+  | struct_field Comma struct_fields
+    { $1 :: $3 }
+
+type_union:
+  | decl typ
+    { Tu_aux (Tu_ty_id ($2, $1), loc $startpos $endpos) }
+  | id Colon typ
+    { Tu_aux (Tu_ty_id ($3, $1), loc $startpos $endpos) }
+  | id
+    { Tu_aux (Tu_id $1, loc $startpos $endpos) }
 
-id_constraint:
-  | nexp_constraint
-      { QI_aux((QI_const $1), loc())}
-  | kinded_id
-      { QI_aux((QI_id $1), loc()) }
+type_unions:
+  | type_union
+    { [$1] }
+  | type_union Comma
+    { [$1] }
+  | type_union Comma type_unions
+    { $1 :: $3 }
 
-id_constraints:
-  | id_constraint
-      { [$1] }
-  | id_constraint Comma id_constraints
-      { $1::$3 }
+fun_def:
+  | Function_ funcl
+    { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, [$2])) $startpos $endpos }
 
-typquant:
-  | Forall id_constraints Dot
-    { typql(TypQ_tq($2)) }
-
-name_sect:
-  | Lsquare Id Eq String Rsquare
-    {
-      if $2 <> "name" then
-       raise (Parse_error_locn ((loc ()),"Unexpected id \""^$2^"\" in name_sect (should be \"name\")"));
-      Name_sect_aux(Name_sect_some($4), loc ()) }
-
-c_def_body:
-  | typ id
-    { [($1,$2)],false }
-  | typ id Semi
-    { [($1,$2)],true }
-  | typ id Semi c_def_body
-    { ($1,$2)::(fst $4), snd $4 }
-
-union_body:
-  | id
-    { [Tu_aux( Tu_id $1, loc())],false }
-  | typ id
-    { [Tu_aux( Tu_ty_id ($1,$2), loc())],false }
-  | id Semi
-    { [Tu_aux( Tu_id $1, loc())],true }
-  | typ id Semi
-    { [Tu_aux( Tu_ty_id ($1,$2),loc())],true }
-  | id Semi union_body
-    { (Tu_aux( Tu_id $1, loc()))::(fst $3), snd $3 }
-  | typ id Semi union_body
-    { (Tu_aux(Tu_ty_id($1,$2),loc()))::(fst $4), snd $4 }
-
-index_range_atomic:
-  | Num
-    { irloc (BF_single($1)) }
-  | Num DotDot Num
-    { irloc (BF_range($1,$3)) }
-  | Lparen index_range Rparen
+let_def:
+  | Let_ letbind
     { $2 }
 
-enum_body:
-  | id
-  { [$1] }
-  | id Semi
-  { [$1] }
-  | id Semi enum_body
-  { $1::$3 }
-
-index_range:
-  | index_range_atomic
-    { $1 }
-  | index_range_atomic Comma index_range
-    { irloc(BF_concat($1,$3)) }
-
-r_id_def:
-  | index_range Colon id
-    { $1,$3 }
+val_spec_def:
+  | Val decl typschm
+    { mk_vs (VS_val_spec ($3, $2)) $startpos $endpos }
+  | Val id Colon typschm
+    { mk_vs (VS_val_spec ($4, $2)) $startpos $endpos }
 
-r_def_body:
-  | r_id_def
-    { [$1] }
-  | r_id_def Semi
-    { [$1] }
-  | r_id_def Semi r_def_body
-    { $1::$3 }
+register_def:
+  | Register decl typ
+    { mk_reg_dec (DEC_reg ($3, $2)) $startpos $endpos }
+  | Register id Colon typ
+    { mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos }
 
-type_def:
-  | Typedef tid name_sect Eq typquant typ
-    { tdloc (TD_abbrev($2,$3,mk_typschm $5 $6 5 6)) }
-  | Typedef tid name_sect Eq typ
-    { tdloc (TD_abbrev($2,$3,mk_typschm (mk_typqn ()) $5 5 5)) }
-  | Typedef tid Eq typquant typ
-    { tdloc (TD_abbrev($2,mk_namesectn (), mk_typschm $4 $5 4 5))}
-  | Typedef tid Eq typ
-    { tdloc (TD_abbrev($2,mk_namesectn (),mk_typschm (mk_typqn ()) $4 4 4)) }
-  /* The below adds 4 shift/reduce conflicts. Due to c_def_body and confusions in id id and parens  */
-  | Typedef tid name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly
-    { tdloc (TD_record($2,$3,$7,fst $9, snd $9)) }
-  | Typedef tid name_sect Eq Const Struct Lcurly c_def_body Rcurly
-    { tdloc (TD_record($2,$3,(mk_typqn ()), fst $8, snd $8)) }
-  | Typedef tid Eq Const Struct typquant Lcurly c_def_body Rcurly
-    { tdloc (TD_record($2,mk_namesectn (), $6, fst $8, snd $8)) }
-  | Typedef tid Eq Const Struct Lcurly c_def_body Rcurly
-    { tdloc (TD_record($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) }
-  | Typedef tid name_sect Eq Const Union typquant Lcurly union_body Rcurly
-    { tdloc (TD_variant($2,$3, $7, fst $9, snd $9)) }
-  | Typedef tid Eq Const Union typquant Lcurly union_body Rcurly
-    { tdloc (TD_variant($2,mk_namesectn (), $6, fst $8, snd $8)) }
-  | Typedef tid name_sect Eq Const Union Lcurly union_body Rcurly
-    { tdloc (TD_variant($2, $3, mk_typqn (), fst $8, snd $8)) }
-  | Typedef tid Eq Const Union Lcurly union_body Rcurly
-    { tdloc (TD_variant($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) }
-  | Typedef tid Eq Enumerate Lcurly enum_body Rcurly
-    { tdloc (TD_enum($2, mk_namesectn (), $6,false)) }
-  | Typedef tid name_sect Eq Enumerate Lcurly enum_body Rcurly
-    { tdloc (TD_enum($2,$3,$7,false)) }
-  | Typedef tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
-    { tdloc (TD_register($2, $7, $9, $12)) }
-
-default_typ:
-  | Default atomic_kind tyvar
-    { defloc (DT_kind($2,$3)) }
-  | Default atomic_kind Inc
-    { defloc (DT_order($2, tloc (ATyp_inc))) }
-  | Default atomic_kind Dec
-    { defloc (DT_order($2, tloc (ATyp_dec))) }
-  | Default typquant typ id
-    { defloc (DT_typ((mk_typschm $2 $3 2 3),$4)) }
-  | Default typ id
-    { defloc (DT_typ((mk_typschm (mk_typqn ()) $2 2 2),$3)) }
-
-scattered_def:
-  | Function_ Rec typquant typ Effect effect_typ id
-    { sdloc (SD_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $6 6, $7)) }
-  | Function_ Rec typ Effect effect_typ id
-    { sdloc (SD_scattered_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $5 5, $6)) }
-  | Function_ Rec typquant typ id
-    { sdloc (SD_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
-  | Function_ Rec Effect effect_typ id
-    { sdloc (SD_scattered_function (mk_rec 2, mk_tannotn (), mk_eannot $4 4, $5)) }
-  | Function_ Rec typ id
-    { sdloc (SD_scattered_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
-  | Function_ Rec id
-    { sdloc (SD_scattered_function(mk_rec 2,mk_tannotn (), mk_eannotn (),$3)) }
-  | Function_ typquant typ Effect effect_typ id
-    { sdloc (SD_scattered_function(mk_recn (),mk_tannot $2 $3 2 3, mk_eannot $5 5, $6)) }
-  | Function_ typ Effect effect_typ id
-    { sdloc (SD_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $4 4, $5)) }
-  | Function_ typquant typ id
-    { sdloc (SD_scattered_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) }
-  | Function_ Effect effect_typ id
-    { sdloc (SD_scattered_function(mk_recn (), mk_tannotn (), mk_eannot $3 3, $4)) }
-  | Function_ typ id
-    { sdloc (SD_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
-  | Function_ id
-    { sdloc (SD_scattered_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
-  | Typedef tid name_sect Eq Const Union typquant
-    { sdloc (SD_scattered_variant($2,$3,$7)) }
-  | Typedef tid Eq Const Union typquant
-    { sdloc (SD_scattered_variant($2,(mk_namesectn ()),$6)) }
-  | Typedef tid name_sect Eq Const Union
-    { sdloc (SD_scattered_variant($2,$3,mk_typqn ())) }
-  | Typedef tid Eq Const Union
-    { sdloc (SD_scattered_variant($2,mk_namesectn (),mk_typqn ())) }
-
-ktype_def:
-  | Def kind tid name_sect Eq typquant typ
-    { kdloc (KD_abbrev($2,$3,$4,mk_typschm $6 $7 6 7)) }
-  | Def kind tid name_sect Eq typ
-    { kdloc (KD_abbrev($2,$3,$4,mk_typschm (mk_typqn ()) $6 6 6)) }
-  | Def kind tid Eq typquant typ
-    { kdloc (KD_abbrev($2,$3,mk_namesectn (), mk_typschm $5 $6 5 6)) }
-  | Def kind tid Eq typ
-    { kdloc (KD_abbrev($2,$3,mk_namesectn (),mk_typschm (mk_typqn ()) $5 5 5)) }
-  | Def kind tid Eq Num
-    { kdloc (KD_abbrev($2,$3,mk_namesectn (),mk_typschm (mk_typqn ()) (tlocl (ATyp_constant $5) 5 5) 5 5)) }
-  | Def kind tid name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly
-    { kdloc (KD_record($2,$3,$4,$8,fst $10, snd $10)) }
-  | Def kind tid name_sect Eq Const Struct Lcurly c_def_body Rcurly
-    { kdloc (KD_record($2,$3,$4,(mk_typqn ()), fst $9, snd $9)) }
-  | Def kind tid Eq Const Struct typquant Lcurly c_def_body Rcurly
-    { kdloc (KD_record($2,$3,mk_namesectn (), $7, fst $9, snd $9)) }
-  | Def kind tid Eq Const Struct Lcurly c_def_body Rcurly
-    { kdloc (KD_record($2,$3, mk_namesectn (), mk_typqn (), fst $8, snd $8)) }
-  | Def kind tid name_sect Eq Const Union typquant Lcurly union_body Rcurly
-    { kdloc (KD_variant($2,$3,$4, $8, fst $10, snd $10)) }
-  | Def kind tid Eq Const Union typquant Lcurly union_body Rcurly
-    { kdloc (KD_variant($2,$3,mk_namesectn (), $7, fst $9, snd $9)) }
-  | Def kind tid name_sect Eq Const Union Lcurly union_body Rcurly
-    { kdloc (KD_variant($2, $3,$4, mk_typqn (), fst $9, snd $9)) }
-  | Def kind tid Eq Const Union Lcurly union_body Rcurly
-    { kdloc (KD_variant($2,$3, mk_namesectn (), mk_typqn (), fst $8, snd $8)) }
-  | Def kind tid Eq Enumerate Lcurly enum_body Rcurly
-    { kdloc (KD_enum($2,$3, mk_namesectn (), $7,false)) }
-  | Def kind tid name_sect Eq Enumerate Lcurly enum_body Rcurly
-    { kdloc (KD_enum($2,$3,$4,$8,false)) }
-  | Def kind tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
-    { kdloc (KD_register($2,$3, $8, $10, $13)) }
-
-    
 def:
-  | type_def
-      { dloc (DEF_type($1)) }
-  | ktype_def
-      { dloc (DEF_kind($1)) }
   | fun_def
-    { dloc (DEF_fundef($1)) }
-  | letbind
-    { dloc (DEF_val($1)) }
-  | val_spec
-    { dloc (DEF_spec($1)) }
-  | default_typ
-    { dloc (DEF_default($1)) }
-  | Overload id Lsquare enum_body Rsquare
-    { dloc (DEF_overload($2,$4)) }
-  | Register typ id
-    { dloc (DEF_reg_dec(DEC_aux(DEC_reg($2,$3),loc ()))) }
-  | Register Alias id Eq exp
-    { dloc (DEF_reg_dec(DEC_aux(DEC_alias($3,$5),loc ()))) }
-  | Register Alias typ id Eq exp
-    { dloc (DEF_reg_dec(DEC_aux(DEC_typ_alias($3,$4,$6), loc ()))) }
-  | Scattered scattered_def
-    { dloc (DEF_scattered $2) }
-  | Function_ Clause funcl
-    { dloc (DEF_scattered (sdloc (SD_scattered_funcl($3)))) }
-  | Union tid Member typ id
-    { dloc (DEF_scattered (sdloc (SD_scattered_unioncl($2,Tu_aux(Tu_ty_id($4,$5), locn 4 5))))) }
-  | Union tid Member id
-    { dloc (DEF_scattered (sdloc (SD_scattered_unioncl($2,Tu_aux(Tu_id($4), locn 4 4))))) }
-  | End id
-    { dloc (DEF_scattered (sdloc (SD_scattered_end($2)))) }
-  | End tid
-    { dloc (DEF_scattered (sdloc (SD_scattered_end($2)))) }
-
-defs_help:
+    { DEF_fundef $1 }
+  | val_spec_def
+    { DEF_spec $1 }
+  | type_def
+    { DEF_type $1 }
+  | let_def
+    { DEF_val $1 }
+  | register_def
+    { DEF_reg_dec $1 }
+  | Overload id Eq Lcurly id_list Rcurly
+    { DEF_overload ($2, $5) }
+  | Overload id Eq enum_bar
+    { DEF_overload ($2, $4) }
+
+defs_list:
   | def
     { [$1] }
-  | def defs_help
+  | def defs_list
     { $1::$2 }
 
 defs:
-  | defs_help
+  | defs_list
     { (Defs $1) }
 
 file:
   | defs Eof
     { $1 }
 
-nonempty_exp_list:
-  | semi_exps_help Eof { $1 }
-
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_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 1cf710bc..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 =
@@ -72,3 +73,4 @@ val output :
     files existed before. If it is set to [false] and an output file already exists,
     the output file is only updated, if its content really changes. *)
 val always_replace_files : bool ref
+
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 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 c4f700b0..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
 
 
@@ -1844,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
@@ -1904,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 ->
@@ -1982,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 =
@@ -2168,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
@@ -2187,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
@@ -2289,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
@@ -2301,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
@@ -2343,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 *)
@@ -2681,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
@@ -2915,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)) =
@@ -2964,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
@@ -3019,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