Extract constant propagation and related functions from monomorphisation.

This shouldn't change any functionality.

8 files changed, 1218 insertions, 1040 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 158b40a8..79b5b0eb 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -1822,6 +1822,77 @@ let typquant_subst_kid_aux sv subst = function
 
 let typquant_subst_kid sv subst (TypQ_aux (typq, l)) = TypQ_aux (typquant_subst_kid_aux sv subst typq, l)
 
+
+let subst_kids_nexp substs nexp =
+  let rec s_snexp substs (Nexp_aux (ne,l) as nexp) =
+    let re ne = Nexp_aux (ne,l) in
+    let s_snexp = s_snexp substs in
+    match ne with
+    | Nexp_var (Kid_aux (_,l) as kid) ->
+       (try KBindings.find kid substs
+       with Not_found -> nexp)
+    | Nexp_id _
+    | Nexp_constant _ -> nexp
+    | Nexp_times (n1,n2) -> re (Nexp_times (s_snexp n1, s_snexp n2))
+    | Nexp_sum (n1,n2)   -> re (Nexp_sum   (s_snexp n1, s_snexp n2))
+    | Nexp_minus (n1,n2) -> re (Nexp_minus (s_snexp n1, s_snexp n2))
+    | Nexp_exp ne -> re (Nexp_exp (s_snexp ne))
+    | Nexp_neg ne -> re (Nexp_neg (s_snexp ne))
+    | Nexp_app (id,args) -> re (Nexp_app (id,List.map s_snexp args))
+  in s_snexp substs nexp
+
+let subst_kids_nc, subst_kids_typ, subst_kids_typ_arg =
+  let rec subst_kids_nc substs (NC_aux (nc,l) as n_constraint) =
+    let snexp nexp = subst_kids_nexp substs nexp in
+    let snc nc = subst_kids_nc substs nc in
+    let re nc = NC_aux (nc,l) in
+    match nc with
+    | NC_equal (n1,n2) -> re (NC_equal (snexp n1, snexp n2))
+    | NC_bounded_ge (n1,n2) -> re (NC_bounded_ge (snexp n1, snexp n2))
+    | NC_bounded_le (n1,n2) -> re (NC_bounded_le (snexp n1, snexp n2))
+    | NC_not_equal (n1,n2) -> re (NC_not_equal (snexp n1, snexp n2))
+    | NC_set (kid,is) ->
+       begin
+         match KBindings.find kid substs with
+         | Nexp_aux (Nexp_constant i,_) ->
+            if List.exists (fun j -> Big_int.equal i j) is then re NC_true else re NC_false
+         | nexp -> 
+            raise (Reporting.err_general l
+                     ("Unable to substitute " ^ string_of_nexp nexp ^
+                        " into set constraint " ^ string_of_n_constraint n_constraint))
+         | exception Not_found -> n_constraint
+       end
+    | NC_or (nc1,nc2) -> re (NC_or (snc nc1, snc nc2))
+    | NC_and (nc1,nc2) -> re (NC_and (snc nc1, snc nc2))
+    | NC_true
+      | NC_false
+      -> n_constraint
+    | NC_var kid -> re (NC_var kid)
+    | NC_app (f, args) ->
+       re (NC_app (f, List.map (s_starg substs) args))
+  and  s_styp substs ((Typ_aux (t,l)) as ty) =
+    let re t = Typ_aux (t,l) in
+    match t with
+    | Typ_id _
+    | Typ_var _
+      -> ty
+    | Typ_fn (t1,t2,e) -> re (Typ_fn (List.map (s_styp substs) t1, s_styp substs t2,e))
+    | Typ_bidir (t1, t2) -> re (Typ_bidir (s_styp substs t1, s_styp substs t2))
+    | Typ_tup ts -> re (Typ_tup (List.map (s_styp substs) ts))
+    | Typ_app (id,tas) -> re (Typ_app (id,List.map (s_starg substs) tas))
+    | Typ_exist (kopts,nc,t) ->
+       let substs = List.fold_left (fun sub kopt -> KBindings.remove (kopt_kid kopt) sub) substs kopts in
+       re (Typ_exist (kopts,subst_kids_nc substs nc,s_styp substs t))
+    | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
+  and s_starg substs (A_aux (ta,l) as targ) =
+    match ta with
+    | A_nexp ne -> A_aux (A_nexp (subst_kids_nexp substs ne),l)
+    | A_typ t -> A_aux (A_typ (s_styp substs t),l)
+    | A_order _ -> targ
+    | A_bool nc -> A_aux (A_bool (subst_kids_nc substs nc), l)
+  in subst_kids_nc, s_styp, s_starg
+
+
 let rec simp_loc = function
   | Parse_ast.Unknown -> None
   | Parse_ast.Unique (_, l) -> simp_loc l
@@ -1953,3 +2024,4 @@ let rec find_annot_defs sl = function
   | [] -> None
 
 let rec find_annot_ast sl (Defs defs) = find_annot_defs sl defs
+
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 0c42d9d3..750d3730 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -439,6 +439,12 @@ val typ_arg_subst : kid -> typ_arg -> typ_arg -> typ_arg
 
 val subst_kid : (kid -> typ_arg -> 'a -> 'a) -> kid -> kid -> 'a -> 'a
 
+(* Multiple type-level substitution *)
+val subst_kids_nexp : nexp KBindings.t -> nexp -> nexp
+val subst_kids_nc : nexp KBindings.t -> n_constraint -> n_constraint
+val subst_kids_typ : nexp KBindings.t -> typ -> typ
+val subst_kids_typ_arg : nexp KBindings.t -> typ_arg -> typ_arg
+
 val quant_item_subst_kid : kid -> kid -> quant_item -> quant_item
 val typquant_subst_kid : kid -> kid -> typquant -> typquant
 
diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
new file mode 100644
index 00000000..c44692b3
--- /dev/null
+++ b/src/constant_propagation.ml
@@ -0,0 +1,825 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+open Spec_analysis
+open Type_check
+
+(* COULD DO: dead code is only eliminated at if expressions, but we could
+   also cut out impossible case branches and code after assertions. *)
+
+(* Constant propogation.
+   Takes maps of immutable/mutable variables to subsitute.
+   The substs argument also contains the current type-level kid refinements
+   so that we can check for dead code.
+   Extremely conservative about evaluation order of assignments in
+   subexpressions, dropping assignments rather than committing to
+   any particular order *)
+
+
+let kbindings_from_list = List.fold_left (fun s (v,i) -> KBindings.add v i s) KBindings.empty
+let bindings_from_list = List.fold_left (fun s (v,i) -> Bindings.add v i s) Bindings.empty
+(* union was introduced in 4.03.0, a bit too recently *)
+let bindings_union s1 s2 =
+  Bindings.merge (fun _ x y -> match x,y with
+  |  _, (Some x) -> Some x
+  |  (Some x), _ -> Some x
+  |  _,  _ -> None) s1 s2
+let kbindings_union s1 s2 =
+  KBindings.merge (fun _ x y -> match x,y with
+  |  _, (Some x) -> Some x
+  |  (Some x), _ -> Some x
+  |  _,  _ -> None) s1 s2
+
+let rec list_extract f = function
+  | [] -> None
+  | h::t -> match f h with None -> list_extract f t | Some v -> Some v
+
+
+
+let is_pure e =
+  match e with
+  | Effect_aux (Effect_set [],_) -> true
+  | _ -> false
+
+let remove_bound (substs,ksubsts) pat =
+  let bound = bindings_from_pat pat in
+  List.fold_left (fun sub v -> Bindings.remove v sub) substs bound, ksubsts
+
+let rec is_value (E_aux (e,(l,annot))) =
+  let is_constructor id =
+    match destruct_tannot annot with
+    | None ->
+       (Reporting.print_err l "Monomorphisation"
+          ("Missing type information for identifier " ^ string_of_id id);
+        false) (* Be conservative if we have no info *)
+    | Some (env,_,_) ->
+       Env.is_union_constructor id env ||
+         (match Env.lookup_id id env with
+         | Enum _ -> true
+         | Unbound | Local _ | Register _ -> false)
+  in
+  match e with
+  | E_id id -> is_constructor id
+  | E_lit _ -> true
+  | E_tuple es -> List.for_all is_value es
+  | E_app (id,es) -> is_constructor id && List.for_all is_value es
+  (* We add casts to undefined to keep the type information in the AST *)
+  | E_cast (typ,E_aux (E_lit (L_aux (L_undef,_)),_)) -> true
+(* TODO: more? *)
+  | _ -> false
+
+let isubst_minus_set subst set =
+  IdSet.fold Bindings.remove set subst
+
+let threaded_map f state l =
+  let l',state' =
+    List.fold_left (fun (tl,state) element -> let (el',state') = f state element in (el'::tl,state'))
+      ([],state) l
+  in List.rev l',state'
+
+
+(* Attempt simple pattern matches *)
+let lit_match = function
+  | (L_zero | L_false), (L_zero | L_false) -> true
+  | (L_one  | L_true ), (L_one  | L_true ) -> true
+  | L_num i1, L_num i2 -> Big_int.equal i1 i2
+  | l1,l2 -> l1 = l2
+
+(* There's no undefined nexp, so replace undefined sizes with a plausible size.
+   32 is used as a sensible default. *)
+
+let fabricate_nexp_exist env l typ kids nc typ' =
+  match kids,nc,Env.expand_synonyms env typ' with
+  | ([kid],NC_aux (NC_set (kid',i::_),_),
+     Typ_aux (Typ_app (Id_aux (Id "atom",_),
+                       [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_))
+      when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 ->
+     Nexp_aux (Nexp_constant i,Unknown)
+  | ([kid],NC_aux (NC_true,_),
+     Typ_aux (Typ_app (Id_aux (Id "atom",_),
+                       [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_))
+      when Kid.compare kid kid'' = 0 ->
+     nint 32
+  | ([kid],NC_aux (NC_set (kid',i::_),_),
+     Typ_aux (Typ_app (Id_aux (Id "range",_),
+                       [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_);
+                        A_aux (A_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_))
+      when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 &&
+        Kid.compare kid kid''' = 0 ->
+     Nexp_aux (Nexp_constant i,Unknown)
+  | ([kid],NC_aux (NC_true,_),
+     Typ_aux (Typ_app (Id_aux (Id "range",_),
+                       [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_);
+                        A_aux (A_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_))
+      when Kid.compare kid kid'' = 0 &&
+        Kid.compare kid kid''' = 0 ->
+     nint 32
+  | ([], _, typ) -> nint 32
+  | (kids, nc, typ) ->
+     raise (Reporting.err_general l
+              ("Undefined value at unsupported type " ^ string_of_typ typ ^ " with " ^ Util.string_of_list ", " string_of_kid kids))
+
+let fabricate_nexp l tannot =
+  match destruct_tannot tannot with
+  | None -> nint 32
+  | Some (env,typ,_) ->
+     match Type_check.destruct_exist (Type_check.Env.expand_synonyms env typ) with
+     | None -> nint 32
+     (* TODO: check this *)
+     | Some (kopts,nc,typ') -> fabricate_nexp_exist env l typ (List.map kopt_kid kopts) nc typ'
+
+let atom_typ_kid kid = function
+  | Typ_aux (Typ_app (Id_aux (Id "atom",_),
+                      [A_aux (A_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_) ->
+     Kid.compare kid kid' = 0
+  | _ -> false
+
+(* We reduce casts in a few cases, in particular to ensure that where the
+   type checker has added a ({'n, true. atom('n)}) ex_int(...) cast we can
+   fill in the 'n.  For undefined we fabricate a suitable value for 'n. *)
+
+let reduce_cast typ exp l annot =
+  let env = env_of_annot (l,annot) in
+  let typ' = Env.base_typ_of env typ in
+  match exp, destruct_exist (Env.expand_synonyms env typ') with
+  | E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' ->
+     let nc_env = Env.add_typ_var l kopt env in
+     let nc_env = Env.add_constraint (nc_eq (nvar (kopt_kid kopt)) (nconstant n)) nc_env in
+     if prove __POS__ nc_env nc
+     then exp
+     else raise (Reporting.err_unreachable l __POS__
+                   ("Constant propagation error: literal " ^ Big_int.to_string n ^
+                       " does not satisfy constraint " ^ string_of_n_constraint nc))
+  | E_aux (E_lit (L_aux (L_undef,_)),_), Some ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' ->
+     let nexp = fabricate_nexp_exist env Unknown typ [kopt_kid kopt] nc typ'' in
+     let newtyp = subst_kids_typ (KBindings.singleton (kopt_kid kopt) nexp) typ'' in
+     E_aux (E_cast (newtyp, exp), (Generated l,replace_typ newtyp annot))
+  | E_aux (E_cast (_,
+                   (E_aux (E_lit (L_aux (L_undef,_)),_) as exp)),_),
+     Some ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' ->
+     let nexp = fabricate_nexp_exist env Unknown typ [kopt_kid kopt] nc typ'' in
+     let newtyp = subst_kids_typ (KBindings.singleton (kopt_kid kopt) nexp) typ'' in
+     E_aux (E_cast (newtyp, exp), (Generated l,replace_typ newtyp annot))
+  | _ -> E_aux (E_cast (typ,exp),(l,annot))
+
+(* Used for constant propagation in pattern matches *)
+type 'a matchresult =
+  | DoesMatch of 'a
+  | DoesNotMatch
+  | GiveUp
+
+(* Remove top-level casts from an expression.  Useful when we need to look at
+   subexpressions to reduce something, but could break type-checking if we used
+   it everywhere. *)
+let rec drop_casts = function
+  | E_aux (E_cast (_,e),_) -> drop_casts e
+  | exp -> exp
+
+let int_of_str_lit = function
+  | L_hex hex -> Big_int.of_string ("0x" ^ hex)
+  | L_bin bin -> Big_int.of_string ("0b" ^ bin)
+  | _ -> assert false
+
+let bits_of_lit = function
+  | L_bin bin -> bin
+  | L_hex hex -> hex_to_bin hex
+  | _ -> assert false
+
+let slice_lit (L_aux (lit,ll)) i len (Ord_aux (ord,_)) =
+  let i = Big_int.to_int i in
+  let len = Big_int.to_int len in
+  let bin = bits_of_lit lit in
+  match match ord with
+  | Ord_inc -> Some i
+  | Ord_dec -> Some (String.length bin - i - len)
+  | Ord_var _ -> None
+  with
+  | None -> None
+  | Some i ->
+     Some (L_aux (L_bin (String.sub bin i len),Generated ll))
+
+let concat_vec lit1 lit2 =
+  let bits1 = bits_of_lit lit1 in
+  let bits2 = bits_of_lit lit2 in
+  L_bin (bits1 ^ bits2)
+
+let lit_eq (L_aux (l1,_)) (L_aux (l2,_)) =
+  match l1,l2 with
+  | (L_zero|L_false), (L_zero|L_false)
+  | (L_one |L_true ), (L_one |L_true)
+    -> Some true
+  | (L_hex _| L_bin _), (L_hex _|L_bin _)
+    -> Some (Big_int.equal (int_of_str_lit l1) (int_of_str_lit l2))
+  | L_undef, _ | _, L_undef -> None
+  | L_num i1, L_num i2 -> Some (Big_int.equal i1 i2)
+  | _ -> Some (l1 = l2)
+
+let try_app (l,ann) (id,args) =
+  let new_l = Parse_ast.Generated l in
+  let env = env_of_annot (l,ann) in
+  let get_overloads f = List.map string_of_id
+    (Env.get_overloads (Id_aux (Id f, Parse_ast.Unknown)) env @
+    Env.get_overloads (Id_aux (DeIid f, Parse_ast.Unknown)) env) in
+  let is_id f = List.mem (string_of_id id) (f :: get_overloads f) in
+  if is_id "==" || is_id "!=" then
+    match args with
+    | [E_aux (E_lit l1,_); E_aux (E_lit l2,_)] ->
+       let lit b = if b then L_true else L_false in
+       let lit b = lit (if is_id "==" then b else not b) in
+       (match lit_eq l1 l2 with
+       | None -> None
+       | Some b -> Some (E_aux (E_lit (L_aux (lit b,new_l)),(l,ann))))
+    | _ -> None
+  else if is_id "cast_bit_bool" then
+    match args with
+    | [E_aux (E_lit L_aux (L_zero,_),_)] -> Some (E_aux (E_lit (L_aux (L_false,new_l)),(l,ann)))
+    | [E_aux (E_lit L_aux (L_one ,_),_)] -> Some (E_aux (E_lit (L_aux (L_true ,new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "UInt" || is_id "unsigned" then
+    match args with
+    | [E_aux (E_lit L_aux ((L_hex _| L_bin _) as lit,_), _)] ->
+       Some (E_aux (E_lit (L_aux (L_num (int_of_str_lit lit),new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "slice" then
+    match args with
+    | [E_aux (E_lit (L_aux ((L_hex _| L_bin _),_) as lit), annot);
+       E_aux (E_lit L_aux (L_num i,_), _);
+       E_aux (E_lit L_aux (L_num len,_), _)] ->
+       (match Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) with
+       | Typ_aux (Typ_app (_,[_;A_aux (A_order ord,_);_]),_) ->
+          (match slice_lit lit i len ord with
+          | Some lit' -> Some (E_aux (E_lit lit',(l,ann)))
+          | None -> None)
+       | _ -> None)
+    | _ -> None
+  else if is_id "bitvector_concat" then
+    match args with
+    | [E_aux (E_lit L_aux ((L_hex _| L_bin _) as lit1,_), _);
+       E_aux (E_lit L_aux ((L_hex _| L_bin _) as lit2,_), _)] ->
+       Some (E_aux (E_lit (L_aux (concat_vec lit1 lit2,new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "shl_int" then
+    match args with
+    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
+       Some (E_aux (E_lit (L_aux (L_num (Big_int.shift_left i (Big_int.to_int j)),new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "mult_atom" || is_id "mult_int" || is_id "mult_range" then
+    match args with
+    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
+       Some (E_aux (E_lit (L_aux (L_num (Big_int.mul i j),new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "quotient_nat" then
+    match args with
+    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
+       Some (E_aux (E_lit (L_aux (L_num (Big_int.div i j),new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "add_atom" || is_id "add_int" || is_id "add_range" then
+    match args with
+    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
+       Some (E_aux (E_lit (L_aux (L_num (Big_int.add i j),new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "negate_range" then
+    match args with
+    | [E_aux (E_lit L_aux (L_num i,_),_)] ->
+       Some (E_aux (E_lit (L_aux (L_num (Big_int.negate i),new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "ex_int" then
+    match args with
+    | [E_aux (E_lit lit,(l,_))] -> Some (E_aux (E_lit lit,(l,ann)))
+    | [E_aux (E_cast (_,(E_aux (E_lit (L_aux (L_undef,_)),_) as e)),(l,_))] ->
+       Some (reduce_cast (typ_of_annot (l,ann)) e l ann)
+    | _ -> None
+  else if is_id "vector_access" || is_id "bitvector_access" then
+    match args with
+    | [E_aux (E_lit L_aux ((L_hex _ | L_bin _) as lit,_),_);
+       E_aux (E_lit L_aux (L_num i,_),_)] ->
+       let v = int_of_str_lit lit in
+       let b = Big_int.bitwise_and (Big_int.shift_right v (Big_int.to_int i)) (Big_int.of_int 1) in
+       let lit' = if Big_int.equal b (Big_int.of_int 1) then L_one else L_zero in
+       Some (E_aux (E_lit (L_aux (lit',new_l)),(l,ann)))
+    | _ -> None
+  else None
+
+
+let construct_lit_vector args =
+  let rec aux l = function
+    | [] -> Some (L_aux (L_bin (String.concat "" (List.rev l)),Unknown))
+    | E_aux (E_lit (L_aux ((L_zero | L_one) as lit,_)),_)::t ->
+       aux ((if lit = L_zero then "0" else "1")::l) t
+    | _ -> None
+  in aux [] args
+
+(* Add a cast to undefined so that it retains its type, otherwise it can't be
+   substituted safely *)
+let keep_undef_typ value =
+  match value with
+  | E_aux (E_lit (L_aux (L_undef,lann)),eann) ->
+     E_aux (E_cast (typ_of_annot eann,value),(Generated Unknown,snd eann))
+  | _ -> value
+
+(* Check whether the current environment with the given kid assignments is
+   inconsistent (and hence whether the code is dead) *)
+let is_env_inconsistent env ksubsts =
+  let env = KBindings.fold (fun k nexp env ->
+    Env.add_constraint (nc_eq (nvar k) nexp) env) ksubsts env in
+  prove __POS__ env nc_false
+
+
+let const_prop defs =
+  let rec const_prop_exp ref_vars substs assigns ((E_aux (e,(l,annot))) as exp) =
+    (* Functions to treat lists and tuples of subexpressions as possibly
+       non-deterministic: that is, we stop making any assumptions about
+       variables that are assigned to in any of the subexpressions *)
+    let non_det_exp_list es =
+      let assigned_in =
+        List.fold_left (fun vs exp -> IdSet.union vs (assigned_vars exp))
+          IdSet.empty es in
+      let assigns = isubst_minus_set assigns assigned_in in
+      let es' = List.map (fun e -> fst (const_prop_exp ref_vars substs assigns e)) es in
+      es',assigns
+    in
+    let non_det_exp_2 e1 e2 =
+       let assigned_in_e12 = IdSet.union (assigned_vars e1) (assigned_vars e2) in
+       let assigns = isubst_minus_set assigns assigned_in_e12 in
+       let e1',_ = const_prop_exp ref_vars substs assigns e1 in
+       let e2',_ = const_prop_exp ref_vars substs assigns e2 in
+       e1',e2',assigns
+    in
+    let non_det_exp_3 e1 e2 e3 =
+       let assigned_in_e12 = IdSet.union (assigned_vars e1) (assigned_vars e2) in
+       let assigned_in_e123 = IdSet.union assigned_in_e12 (assigned_vars e3) in
+       let assigns = isubst_minus_set assigns assigned_in_e123 in
+       let e1',_ = const_prop_exp ref_vars substs assigns e1 in
+       let e2',_ = const_prop_exp ref_vars substs assigns e2 in
+       let e3',_ = const_prop_exp ref_vars substs assigns e3 in
+       e1',e2',e3',assigns
+    in
+    let non_det_exp_4 e1 e2 e3 e4 =
+       let assigned_in_e12 = IdSet.union (assigned_vars e1) (assigned_vars e2) in
+       let assigned_in_e123 = IdSet.union assigned_in_e12 (assigned_vars e3) in
+       let assigned_in_e1234 = IdSet.union assigned_in_e123 (assigned_vars e4) in
+       let assigns = isubst_minus_set assigns assigned_in_e1234 in
+       let e1',_ = const_prop_exp ref_vars substs assigns e1 in
+       let e2',_ = const_prop_exp ref_vars substs assigns e2 in
+       let e3',_ = const_prop_exp ref_vars substs assigns e3 in
+       let e4',_ = const_prop_exp ref_vars substs assigns e4 in
+       e1',e2',e3',e4',assigns
+    in
+    let re e assigns = E_aux (e,(l,annot)),assigns in
+    match e with
+      (* TODO: are there more circumstances in which we should get rid of these? *)
+    | E_block [e] -> const_prop_exp ref_vars substs assigns e
+    | E_block es ->
+       let es',assigns = threaded_map (const_prop_exp ref_vars substs) assigns es in
+       re (E_block es') assigns
+    | E_nondet es ->
+       let es',assigns = non_det_exp_list es in
+       re (E_nondet es') assigns
+    | E_id id ->
+       let env = Type_check.env_of_annot (l, annot) in
+       (try
+         match Env.lookup_id id env with
+         | Local (Immutable,_) -> Bindings.find id (fst substs)
+         | Local (Mutable,_)   -> Bindings.find id assigns
+         | _ -> exp
+       with Not_found -> exp),assigns
+    | E_lit _
+    | E_sizeof _
+    | E_constraint _
+      -> exp,assigns
+    | E_cast (t,e') ->
+       let e'',assigns = const_prop_exp ref_vars substs assigns e' in
+       if is_value e''
+       then reduce_cast t e'' l annot, assigns
+       else re (E_cast (t, e'')) assigns
+    | E_app (id,es) ->
+       let es',assigns = non_det_exp_list es in
+       let env = Type_check.env_of_annot (l, annot) in
+       (match try_app (l,annot) (id,es') with
+       | None ->
+          (match const_prop_try_fn ref_vars l env (id,es') with
+          | None -> re (E_app (id,es')) assigns
+          | Some r -> r,assigns)
+       | Some r -> r,assigns)
+    | E_tuple es ->
+       let es',assigns = non_det_exp_list es in
+       re (E_tuple es') assigns
+    | E_if (e1,e2,e3) ->
+       let e1',assigns = const_prop_exp ref_vars substs assigns e1 in
+       let e1_no_casts = drop_casts e1' in
+       (match e1_no_casts with
+       | E_aux (E_lit (L_aux ((L_true|L_false) as lit ,_)),_) ->
+          (match lit with
+          | L_true -> const_prop_exp ref_vars substs assigns e2
+          |  _     -> const_prop_exp ref_vars substs assigns e3)
+       | _ ->
+          (* If the guard is an equality check, propagate the value. *)
+          let env1 = env_of e1_no_casts in
+          let is_equal id =
+            List.exists (fun id' -> Id.compare id id' == 0)
+              (Env.get_overloads (Id_aux (DeIid "==", Parse_ast.Unknown))
+                 env1)
+          in
+          let substs_true =
+            match e1_no_casts with
+            | E_aux (E_app (id, [E_aux (E_id var,_); vl]),_)
+            | E_aux (E_app (id, [vl; E_aux (E_id var,_)]),_)
+                when is_equal id ->
+               if is_value vl then
+                 (match Env.lookup_id var env1 with
+                 | Local (Immutable,_) -> Bindings.add var vl (fst substs),snd substs
+                 | _ -> substs)
+               else substs
+            | _ -> substs
+          in
+          (* Discard impossible branches *)
+          if is_env_inconsistent (env_of e2) (snd substs) then
+            const_prop_exp ref_vars substs assigns e3
+          else if is_env_inconsistent (env_of e3) (snd substs) then
+            const_prop_exp ref_vars substs_true assigns e2
+          else
+            let e2',assigns2 = const_prop_exp ref_vars substs_true assigns e2 in
+            let e3',assigns3 = const_prop_exp ref_vars substs assigns e3 in
+            let assigns = isubst_minus_set assigns (assigned_vars e2) in
+            let assigns = isubst_minus_set assigns (assigned_vars e3) in
+            re (E_if (e1',e2',e3')) assigns)
+    | E_for (id,e1,e2,e3,ord,e4) ->
+       (* Treat e1, e2 and e3 (from, to and by) as a non-det tuple *)
+       let e1',e2',e3',assigns = non_det_exp_3 e1 e2 e3 in
+       let assigns = isubst_minus_set assigns (assigned_vars e4) in
+       let e4',_ = const_prop_exp ref_vars (Bindings.remove id (fst substs),snd substs) assigns e4 in
+       re (E_for (id,e1',e2',e3',ord,e4')) assigns
+    | E_loop (loop,e1,e2) ->
+       let assigns = isubst_minus_set assigns (IdSet.union (assigned_vars e1) (assigned_vars e2)) in
+       let e1',_ = const_prop_exp ref_vars substs assigns e1 in
+       let e2',_ = const_prop_exp ref_vars substs assigns e2 in
+       re (E_loop (loop,e1',e2')) assigns
+    | E_vector es ->
+       let es',assigns = non_det_exp_list es in
+       begin
+         match construct_lit_vector es' with
+         | None -> re (E_vector es') assigns
+         | Some lit -> re (E_lit lit) assigns
+       end
+    | E_vector_access (e1,e2) ->
+       let e1',e2',assigns = non_det_exp_2 e1 e2 in
+       re (E_vector_access (e1',e2')) assigns
+    | E_vector_subrange (e1,e2,e3) ->
+       let e1',e2',e3',assigns = non_det_exp_3 e1 e2 e3 in
+       re (E_vector_subrange (e1',e2',e3')) assigns
+    | E_vector_update (e1,e2,e3) ->
+       let e1',e2',e3',assigns = non_det_exp_3 e1 e2 e3 in
+       re (E_vector_update (e1',e2',e3')) assigns
+    | E_vector_update_subrange (e1,e2,e3,e4) ->
+       let e1',e2',e3',e4',assigns = non_det_exp_4 e1 e2 e3 e4 in
+       re (E_vector_update_subrange (e1',e2',e3',e4')) assigns
+    | E_vector_append (e1,e2) ->
+       let e1',e2',assigns = non_det_exp_2 e1 e2 in
+       re (E_vector_append (e1',e2')) assigns
+    | E_list es ->
+       let es',assigns = non_det_exp_list es in
+       re (E_list es') assigns
+    | E_cons (e1,e2) ->
+       let e1',e2',assigns = non_det_exp_2 e1 e2 in
+       re (E_cons (e1',e2')) assigns
+    | E_record fes ->
+       let assigned_in_fes = assigned_vars_in_fexps fes in
+       let assigns = isubst_minus_set assigns assigned_in_fes in
+       re (E_record (const_prop_fexps ref_vars substs assigns fes)) assigns
+    | E_record_update (e,fes) ->
+       let assigned_in = IdSet.union (assigned_vars_in_fexps fes) (assigned_vars e) in
+       let assigns = isubst_minus_set assigns assigned_in in
+       let e',_ = const_prop_exp ref_vars substs assigns e in
+       re (E_record_update (e', const_prop_fexps ref_vars substs assigns fes)) assigns
+    | E_field (e,id) ->
+       let e',assigns = const_prop_exp ref_vars substs assigns e in
+       re (E_field (e',id)) assigns
+    | E_case (e,cases) ->
+       let e',assigns = const_prop_exp ref_vars substs assigns e in
+       (match can_match ref_vars e' cases substs assigns with
+       | None ->
+          let assigned_in =
+            List.fold_left (fun vs pe -> IdSet.union vs (assigned_vars_in_pexp pe))
+              IdSet.empty cases
+          in
+          let assigns' = isubst_minus_set assigns assigned_in in
+          re (E_case (e', List.map (const_prop_pexp ref_vars substs assigns) cases)) assigns'
+       | Some (E_aux (_,(_,annot')) as exp,newbindings,kbindings) ->
+          let exp = nexp_subst_exp (kbindings_from_list kbindings) exp in
+          let newbindings_env = bindings_from_list newbindings in
+          let substs' = bindings_union (fst substs) newbindings_env, snd substs in
+          const_prop_exp ref_vars substs' assigns exp)
+    | E_let (lb,e2) ->
+       begin
+         match lb with
+         | LB_aux (LB_val (p,e), annot) ->
+            let e',assigns = const_prop_exp ref_vars substs assigns e in
+            let substs' = remove_bound substs p in
+            let plain () =
+              let e2',assigns = const_prop_exp ref_vars substs' assigns e2 in
+              re (E_let (LB_aux (LB_val (p,e'), annot),
+                         e2')) assigns in
+            if is_value e' && not (is_value e) then
+              match can_match ref_vars e' [Pat_aux (Pat_exp (p,e2),(Unknown,empty_tannot))] substs assigns with
+              | None -> plain ()
+              | Some (e'',bindings,kbindings) ->
+                 let e'' = nexp_subst_exp (kbindings_from_list kbindings) e'' in
+                 let bindings = bindings_from_list bindings in
+                 let substs'' = bindings_union (fst substs') bindings, snd substs' in
+                 const_prop_exp ref_vars substs'' assigns e''
+            else plain ()
+       end
+    (* TODO maybe - tuple assignments *)
+    | E_assign (le,e) ->
+       let env = Type_check.env_of_annot (l, annot) in
+       let assigned_in = IdSet.union (assigned_vars_in_lexp le) (assigned_vars e) in
+       let assigns = isubst_minus_set assigns assigned_in in
+       let le',idopt = const_prop_lexp ref_vars substs assigns le in
+       let e',_ = const_prop_exp ref_vars substs assigns e in
+       let assigns =
+         match idopt with
+         | Some id ->
+            begin
+              match Env.lookup_id id env with
+              | Local (Mutable,_) | Unbound ->
+                 if is_value e' && not (IdSet.mem id ref_vars)
+                 then Bindings.add id (keep_undef_typ e') assigns
+                 else Bindings.remove id assigns
+              | _ -> assigns
+            end
+         | None -> assigns
+       in
+       re (E_assign (le', e')) assigns
+    | E_exit e ->
+       let e',_ = const_prop_exp ref_vars substs assigns e in
+       re (E_exit e') Bindings.empty
+    | E_ref id -> re (E_ref id) Bindings.empty
+    | E_throw e ->
+       let e',_ = const_prop_exp ref_vars substs assigns e in
+       re (E_throw e') Bindings.empty
+    | E_try (e,cases) ->
+       (* TODO: try and preserve *any* assignment info *)
+       let e',_ = const_prop_exp ref_vars substs assigns e in
+       re (E_case (e', List.map (const_prop_pexp ref_vars substs Bindings.empty) cases)) Bindings.empty
+    | E_return e ->
+       let e',_ = const_prop_exp ref_vars substs assigns e in
+       re (E_return e') Bindings.empty
+    | E_assert (e1,e2) ->
+       let e1',e2',assigns = non_det_exp_2 e1 e2 in
+       re (E_assert (e1',e2')) assigns
+  
+    | E_app_infix _
+    | E_var _
+    | E_internal_plet _
+    | E_internal_return _
+    | E_internal_value _
+      -> raise (Reporting.err_unreachable l __POS__
+                  ("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp))
+  and const_prop_fexps ref_vars substs assigns fes =
+    List.map (const_prop_fexp ref_vars substs assigns) fes
+  and const_prop_fexp ref_vars substs assigns (FE_aux (FE_Fexp (id,e), annot)) =
+    FE_aux (FE_Fexp (id,fst (const_prop_exp ref_vars substs assigns e)),annot)
+  and const_prop_pexp ref_vars substs assigns = function
+    | (Pat_aux (Pat_exp (p,e),l)) ->
+       Pat_aux (Pat_exp (p,fst (const_prop_exp ref_vars (remove_bound substs p) assigns e)),l)
+    | (Pat_aux (Pat_when (p,e1,e2),l)) ->
+       let substs' = remove_bound substs p in
+       let e1',assigns = const_prop_exp ref_vars substs' assigns e1 in
+       Pat_aux (Pat_when (p, e1', fst (const_prop_exp ref_vars substs' assigns e2)),l)
+  and const_prop_lexp ref_vars substs assigns ((LEXP_aux (e,annot)) as le) =
+    let re e = LEXP_aux (e,annot), None in
+    match e with
+    | LEXP_id id (* shouldn't end up substituting here *)
+    | LEXP_cast (_,id)
+      -> le, Some id
+    | LEXP_memory (id,es) ->
+       re (LEXP_memory (id,List.map (fun e -> fst (const_prop_exp ref_vars substs assigns e)) es)) (* or here *)
+    | LEXP_tup les -> re (LEXP_tup (List.map (fun le -> fst (const_prop_lexp ref_vars substs assigns le)) les))
+    | LEXP_vector (le,e) -> re (LEXP_vector (fst (const_prop_lexp ref_vars substs assigns le), fst (const_prop_exp ref_vars substs assigns e)))
+    | LEXP_vector_range (le,e1,e2) ->
+       re (LEXP_vector_range (fst (const_prop_lexp ref_vars substs assigns le),
+                              fst (const_prop_exp ref_vars substs assigns e1),
+                              fst (const_prop_exp ref_vars substs assigns e2)))
+    | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map (fun le -> fst (const_prop_lexp ref_vars substs assigns le)) les))
+    | LEXP_field (le,id) -> re (LEXP_field (fst (const_prop_lexp ref_vars substs assigns le), id))
+    | LEXP_deref e ->
+       re (LEXP_deref (fst (const_prop_exp ref_vars substs assigns e)))
+  (* Reduce a function when
+     1. all arguments are values,
+     2. the function is pure,
+     3. the result is a value
+     (and 4. the function is not scattered, but that's not terribly important)
+     to try and keep execution time and the results managable.
+  *)
+  and const_prop_try_fn ref_vars l env (id,args) =
+    if not (List.for_all is_value args) then
+      None
+    else
+      let (tq,typ) = Env.get_val_spec_orig id env in
+      let eff = match typ with
+        | Typ_aux (Typ_fn (_,_,eff),_) -> Some eff
+        | _ -> None
+      in
+      let Defs ds = defs in
+      match eff, list_extract (function
+      | (DEF_fundef (FD_aux (FD_function (_,_,eff,((FCL_aux (FCL_Funcl (id',_),_))::_ as fcls)),_)))
+        -> if Id.compare id id' = 0 then Some fcls else None
+      | _ -> None) ds with
+      | None,_ | _,None -> None
+      | Some eff,_ when not (is_pure eff) -> None
+      | Some _,Some fcls ->
+         let arg = match args with
+           | [] -> E_aux (E_lit (L_aux (L_unit,Generated l)),(Generated l,empty_tannot))
+           | [e] -> e
+           | _ -> E_aux (E_tuple args,(Generated l,empty_tannot)) in
+         let cases = List.map (function
+           | FCL_aux (FCL_Funcl (_,pexp), ann) -> pexp)
+           fcls in
+         match can_match_with_env ref_vars env arg cases (Bindings.empty,KBindings.empty) Bindings.empty with
+         | Some (exp,bindings,kbindings) ->
+            let substs = bindings_from_list bindings, kbindings_from_list kbindings in
+            let result,_ = const_prop_exp ref_vars substs Bindings.empty exp in
+            let result = match result with
+              | E_aux (E_return e,_) -> e
+              | _ -> result
+            in
+            if is_value result then Some result else None
+         | None -> None
+  
+  and can_match_with_env ref_vars env (E_aux (e,(l,annot)) as exp0) cases (substs,ksubsts) assigns =
+    let rec findpat_generic check_pat description assigns = function
+      | [] -> (Reporting.print_err l "Monomorphisation"
+                 ("Failed to find a case for " ^ description); None)
+      | [Pat_aux (Pat_exp (P_aux (P_wild,_),exp),_)] -> Some (exp,[],[])
+      | (Pat_aux (Pat_exp (P_aux (P_typ (_,p),_),exp),ann))::tl ->
+         findpat_generic check_pat description assigns ((Pat_aux (Pat_exp (p,exp),ann))::tl)
+      | (Pat_aux (Pat_exp (P_aux (P_id id',_),exp),_))::tlx
+          when pat_id_is_variable env id' ->
+         Some (exp, [(id', exp0)], [])
+      | (Pat_aux (Pat_when (P_aux (P_id id',_),guard,exp),_))::tl
+          when pat_id_is_variable env id' -> begin
+            let substs = Bindings.add id' exp0 substs, ksubsts in
+            let (E_aux (guard,_)),assigns = const_prop_exp ref_vars substs assigns guard in
+            match guard with
+            | E_lit (L_aux (L_true,_)) -> Some (exp,[(id',exp0)],[])
+            | E_lit (L_aux (L_false,_)) -> findpat_generic check_pat description assigns tl
+            | _ -> None
+          end
+      | (Pat_aux (Pat_when (p,guard,exp),_))::tl -> begin
+        match check_pat p with
+        | DoesNotMatch -> findpat_generic check_pat description assigns tl
+        | DoesMatch (vsubst,ksubst) -> begin
+          let guard = nexp_subst_exp (kbindings_from_list ksubst) guard in
+          let substs = bindings_union substs (bindings_from_list vsubst),
+                       kbindings_union ksubsts (kbindings_from_list ksubst) in
+          let (E_aux (guard,_)),assigns = const_prop_exp ref_vars substs assigns guard in
+          match guard with
+          | E_lit (L_aux (L_true,_)) -> Some (exp,vsubst,ksubst)
+          | E_lit (L_aux (L_false,_)) -> findpat_generic check_pat description assigns tl
+          | _ -> None
+        end
+        | GiveUp -> None
+      end
+      | (Pat_aux (Pat_exp (p,exp),_))::tl ->
+         match check_pat p with
+         | DoesNotMatch -> findpat_generic check_pat description assigns tl
+         | DoesMatch (subst,ksubst) -> Some (exp,subst,ksubst)
+         | GiveUp -> None
+    in
+    match e with
+    | E_id id ->
+       (match Env.lookup_id id env with
+       | Enum _ ->
+          let checkpat = function
+            | P_aux (P_id id',_)
+            | P_aux (P_app (id',[]),_) ->
+               if Id.compare id id' = 0 then DoesMatch ([],[]) else DoesNotMatch
+            | P_aux (_,(l',_)) ->
+               (Reporting.print_err l' "Monomorphisation"
+                  "Unexpected kind of pattern for enumeration"; GiveUp)
+          in findpat_generic checkpat (string_of_id id) assigns cases
+       | _ -> None)
+    | E_lit (L_aux (lit_e, lit_l)) ->
+       let checkpat = function
+         | P_aux (P_lit (L_aux (lit_p, _)),_) ->
+            if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch
+         | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)),_) ->
+            begin
+              match lit_e with
+              | L_num i ->
+                 DoesMatch ([id, E_aux (e,(l,annot))],
+                            [kid,Nexp_aux (Nexp_constant i,Unknown)])
+              (* For undefined we fix the type-level size (because there's no good
+                 way to construct an undefined size), but leave the term as undefined
+                 to make the meaning clear. *)
+              | L_undef ->
+                 let nexp = fabricate_nexp l annot in
+                 let typ = subst_kids_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in
+                 DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,empty_tannot))),(l,empty_tannot))],
+                            [kid,nexp])
+              | _ ->
+                 (Reporting.print_err lit_l "Monomorphisation"
+                    "Unexpected kind of literal for var match"; GiveUp)
+            end
+         | P_aux (_,(l',_)) ->
+            (Reporting.print_err l' "Monomorphisation"
+               "Unexpected kind of pattern for literal"; GiveUp)
+       in findpat_generic checkpat "literal" assigns cases
+    | E_vector es when List.for_all (function (E_aux (E_lit _,_)) -> true | _ -> false) es ->
+       let checkpat = function
+         | P_aux (P_vector ps,_) ->
+            let matches = List.map2 (fun e p ->
+              match e, p with
+              | E_aux (E_lit (L_aux (lit,_)),_), P_aux (P_lit (L_aux (lit',_)),_) ->
+                 if lit_match (lit,lit') then DoesMatch ([],[]) else DoesNotMatch
+              | E_aux (E_lit l,_), P_aux (P_id var,_) when pat_id_is_variable env var ->
+                 DoesMatch ([var, e],[])
+              | _ -> GiveUp) es ps in
+            let final = List.fold_left (fun acc m -> match acc, m with
+              | _, GiveUp -> GiveUp
+              | GiveUp, _ -> GiveUp
+              | DoesMatch (sub,ksub), DoesMatch(sub',ksub') -> DoesMatch(sub@sub',ksub@ksub')
+              | _ -> DoesNotMatch) (DoesMatch ([],[])) matches in
+            (match final with
+            | GiveUp ->
+               (Reporting.print_err l "Monomorphisation"
+                  "Unexpected kind of pattern for vector literal"; GiveUp)
+            | _ -> final)
+         | _ ->
+            (Reporting.print_err l "Monomorphisation"
+               "Unexpected kind of pattern for vector literal"; GiveUp)
+       in findpat_generic checkpat "vector literal" assigns cases
+  
+    | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)) ->
+       let checkpat = function
+         | P_aux (P_lit (L_aux (lit_p, _)),_) -> DoesNotMatch
+         | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)),_) ->
+              (* For undefined we fix the type-level size (because there's no good
+                 way to construct an undefined size), but leave the term as undefined
+                 to make the meaning clear. *)
+            let nexp = fabricate_nexp l annot in
+            let kids = equal_kids (env_of_annot p_id_annot) kid in
+            let ksubst = KidSet.fold (fun k b -> KBindings.add k nexp b) kids KBindings.empty in
+            let typ = subst_kids_typ ksubst (typ_of_annot p_id_annot) in
+            DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,empty_tannot))],
+                       KBindings.bindings ksubst)
+         | P_aux (_,(l',_)) ->
+            (Reporting.print_err l' "Monomorphisation"
+               "Unexpected kind of pattern for literal"; GiveUp)
+       in findpat_generic checkpat "literal" assigns cases
+    | _ -> None
+  
+  and can_match ref_vars exp =
+    let env = Type_check.env_of exp in
+    can_match_with_env ref_vars env exp
+
+in const_prop_exp
diff --git a/src/constant_propagation.mli b/src/constant_propagation.mli
new file mode 100644
index 00000000..291ec056
--- /dev/null
+++ b/src/constant_propagation.mli
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+open Type_check
+
+(** [const_prop defs ref_vars substs assigns exp] performs constant propagation
+    on [exp] where [substs] is a pair of substitutions on immutable variables
+    and type variables, [assigns] is a substitution on mutable variables, and
+    [ref_vars] is the set of variable which may have had a reference taken
+    (and hence we cannot reliably track). *)
+
+val const_prop :
+  tannot defs ->
+  IdSet.t ->
+  tannot exp Bindings.t * nexp KBindings.t ->
+  tannot exp Bindings.t ->
+  tannot exp ->
+  tannot exp * tannot exp Bindings.t
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index f0472385..56349989 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -81,75 +81,6 @@ let kbindings_union s1 s2 =
   |  (Some x), _ -> Some x
   |  _,  _ -> None) s1 s2
 
-let subst_nexp substs nexp =
-  let rec s_snexp substs (Nexp_aux (ne,l) as nexp) =
-    let re ne = Nexp_aux (ne,l) in
-    let s_snexp = s_snexp substs in
-    match ne with
-    | Nexp_var (Kid_aux (_,l) as kid) ->
-       (try KBindings.find kid substs
-       with Not_found -> nexp)
-    | Nexp_id _
-    | Nexp_constant _ -> nexp
-    | Nexp_times (n1,n2) -> re (Nexp_times (s_snexp n1, s_snexp n2))
-    | Nexp_sum (n1,n2)   -> re (Nexp_sum   (s_snexp n1, s_snexp n2))
-    | Nexp_minus (n1,n2) -> re (Nexp_minus (s_snexp n1, s_snexp n2))
-    | Nexp_exp ne -> re (Nexp_exp (s_snexp ne))
-    | Nexp_neg ne -> re (Nexp_neg (s_snexp ne))
-    | Nexp_app (id,args) -> re (Nexp_app (id,List.map s_snexp args))
-  in s_snexp substs nexp
-
-let subst_nc, subst_src_typ, subst_src_typ_arg =
-  let rec subst_nc substs (NC_aux (nc,l) as n_constraint) =
-    let snexp nexp = subst_nexp substs nexp in
-    let snc nc = subst_nc substs nc in
-    let re nc = NC_aux (nc,l) in
-    match nc with
-    | NC_equal (n1,n2) -> re (NC_equal (snexp n1, snexp n2))
-    | NC_bounded_ge (n1,n2) -> re (NC_bounded_ge (snexp n1, snexp n2))
-    | NC_bounded_le (n1,n2) -> re (NC_bounded_le (snexp n1, snexp n2))
-    | NC_not_equal (n1,n2) -> re (NC_not_equal (snexp n1, snexp n2))
-    | NC_set (kid,is) ->
-       begin
-         match KBindings.find kid substs with
-         | Nexp_aux (Nexp_constant i,_) ->
-            if List.exists (fun j -> Big_int.equal i j) is then re NC_true else re NC_false
-         | nexp -> 
-            raise (Reporting.err_general l
-                     ("Unable to substitute " ^ string_of_nexp nexp ^
-                        " into set constraint " ^ string_of_n_constraint n_constraint))
-         | exception Not_found -> n_constraint
-       end
-    | NC_or (nc1,nc2) -> re (NC_or (snc nc1, snc nc2))
-    | NC_and (nc1,nc2) -> re (NC_and (snc nc1, snc nc2))
-    | NC_true
-      | NC_false
-      -> n_constraint
-    | NC_var kid -> re (NC_var kid)
-    | NC_app (f, args) ->
-       re (NC_app (f, List.map (s_starg substs) args))
-  and  s_styp substs ((Typ_aux (t,l)) as ty) =
-    let re t = Typ_aux (t,l) in
-    match t with
-    | Typ_id _
-    | Typ_var _
-      -> ty
-    | Typ_fn (t1,t2,e) -> re (Typ_fn (List.map (s_styp substs) t1, s_styp substs t2,e))
-    | Typ_bidir (t1, t2) -> re (Typ_bidir (s_styp substs t1, s_styp substs t2))
-    | Typ_tup ts -> re (Typ_tup (List.map (s_styp substs) ts))
-    | Typ_app (id,tas) -> re (Typ_app (id,List.map (s_starg substs) tas))
-    | Typ_exist (kopts,nc,t) ->
-       let substs = List.fold_left (fun sub kopt -> KBindings.remove (kopt_kid kopt) sub) substs kopts in
-       re (Typ_exist (kopts,subst_nc substs nc,s_styp substs t))
-    | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
-  and s_starg substs (A_aux (ta,l) as targ) =
-    match ta with
-    | A_nexp ne -> A_aux (A_nexp (subst_nexp substs ne),l)
-    | A_typ t -> A_aux (A_typ (s_styp substs t),l)
-    | A_order _ -> targ
-    | A_bool nc -> A_aux (A_bool (subst_nc substs nc), l)
-  in subst_nc, s_styp, s_starg
-
 let make_vector_lit sz i =
   let f j = if Big_int.equal (Big_int.modulus (Big_int.shift_right i (sz-j-1)) (Big_int.of_int 2)) Big_int.zero then '0' else '1' in
   let s = String.init sz f in
@@ -164,50 +95,6 @@ let tabulate f n =
 let make_vectors sz =
   tabulate (make_vector_lit sz) (Big_int.shift_left (Big_int.of_int 1) sz)
 
-let pat_id_is_variable env id =
-  match Env.lookup_id id env with
-  (* Unbound is returned for both variables and constructors which take
-     arguments, but the latter only don't appear in a P_id *)
-  | Unbound
-  (* Shadowing of immutable locals is allowed; mutable locals and registers
-     are rejected by the type checker, so don't matter *)
-  | Local _
-  | Register _
-    -> true
-  | Enum _ -> false
-
-let rec is_value (E_aux (e,(l,annot))) =
-  let is_constructor id =
-    match destruct_tannot annot with
-    | None ->
-       (Reporting.print_err l "Monomorphisation"
-          ("Missing type information for identifier " ^ string_of_id id);
-        false) (* Be conservative if we have no info *)
-    | Some (env,_,_) ->
-       Env.is_union_constructor id env ||
-         (match Env.lookup_id id env with
-         | Enum _ -> true
-         | Unbound | Local _ | Register _ -> false)
-  in
-  match e with
-  | E_id id -> is_constructor id
-  | E_lit _ -> true
-  | E_tuple es -> List.for_all is_value es
-  | E_app (id,es) -> is_constructor id && List.for_all is_value es
-  (* We add casts to undefined to keep the type information in the AST *)
-  | E_cast (typ,E_aux (E_lit (L_aux (L_undef,_)),_)) -> true
-(* TODO: more? *)
-  | _ -> false
-
-let is_pure e =
-  match e with
-  | Effect_aux (Effect_set [],_) -> true
-  | _ -> false
-
-let rec list_extract f = function
-  | [] -> None
-  | h::t -> match f h with None -> list_extract f t | Some v -> Some v
-
 let rec cross = function
   | [] -> failwith "cross"
   | [(x,l)] -> List.map (fun y -> [(x,y)]) l
@@ -232,33 +119,9 @@ let kidset_bigunion = function
   | [] -> KidSet.empty
   | h::t -> List.fold_left KidSet.union h t
 
-let rec flatten_constraints = function
-  | [] -> []
-  | (NC_aux (NC_and (nc1,nc2),_))::t -> flatten_constraints (nc1::nc2::t)
-  | h::t -> h::(flatten_constraints t)
-
-(* NB: this only looks for direct equalities with the given kid.  It would be
-   better in principle to find the entire set of equal kids, but it isn't
-   necessary to deal with the fresh kids produced by the type checker while
-   checking P_var patterns, so we don't do it for now. *)
-let equal_kids_ncs kid ncs =
-  let is_eq = function
-    | NC_aux (NC_equal (Nexp_aux (Nexp_var var1,_), Nexp_aux (Nexp_var var2,_)),_) ->
-       if Kid.compare kid var1 == 0 then Some var2 else
-         if Kid.compare kid var2 == 0 then Some var1 else
-           None
-    | _ -> None
-  in
-  let kids = Util.map_filter is_eq ncs in
-  List.fold_left (fun s k -> KidSet.add k s) (KidSet.singleton kid) kids
-
-let equal_kids env kid =
-  let ncs = flatten_constraints (Env.get_constraints env) in
-  equal_kids_ncs kid ncs
-
 (* TODO: deal with non-set constraints, intersections, etc somehow *)
 let extract_set_nc l var nc =
-  let vars = equal_kids_ncs var [nc] in
+  let vars = Spec_analysis.equal_kids_ncs var [nc] in
   let rec aux_or (NC_aux (nc,l)) =
     match nc with
     | NC_equal (Nexp_aux (Nexp_var id,_), Nexp_aux (Nexp_constant n,_))
@@ -306,7 +169,7 @@ let apply_kid_insts kid_insts t =
   let kid_insts, kids' = split_insts kid_insts in
   let kid_insts = List.map (fun (v,i) -> (v,Nexp_aux (Nexp_constant i,Generated Unknown))) kid_insts in
   let subst = kbindings_from_list kid_insts in
-  kids', subst_src_typ subst t
+  kids', subst_kids_typ subst t
 
 let rec inst_src_type insts (Typ_aux (ty,l) as typ) =
   match ty with
@@ -555,374 +418,6 @@ let refine_constructor refinements l env id args =
   | exception Not_found -> None
 
 
-(* Substitute found nexps for variables in an expression, and rename constructors to reflect
-   specialisation *)
-
-(* TODO: kid shadowing *)
-let nexp_subst_fns substs =
-
-  let s_t t = subst_src_typ substs t in
-(*  let s_typschm (TypSchm_aux (TypSchm_ts (q,t),l)) = TypSchm_aux (TypSchm_ts (q,s_t t),l) in
-   hopefully don't need this anyway *)(*
-  let s_typschm tsh = tsh in*)
-  let s_tannot tannot =
-    match destruct_tannot tannot with
-    | None -> empty_tannot
-    | Some (env,t,eff) -> mk_tannot env (s_t t) eff (* TODO: what about env? *)
-  in
-  let rec s_pat (P_aux (p,(l,annot))) =
-    let re p = P_aux (p,(l,s_tannot annot)) in
-    match p with
-    | P_lit _ | P_wild | P_id _ -> re p
-    | P_or (p1, p2) -> re (P_or (s_pat p1, s_pat p2))
-    | P_not (p) -> re (P_not (s_pat p))
-    | P_var (p',tpat) -> re (P_var (s_pat p',tpat))
-    | P_as (p',id) -> re (P_as (s_pat p', id))
-    | P_typ (ty,p') -> re (P_typ (s_t ty,s_pat p'))
-    | P_app (id,ps) -> re (P_app (id, List.map s_pat ps))
-    | P_record (fps,flag) -> re (P_record (List.map s_fpat fps, flag))
-    | P_vector ps -> re (P_vector (List.map s_pat ps))
-    | P_vector_concat ps -> re (P_vector_concat (List.map s_pat ps))
-    | P_string_append ps -> re (P_string_append (List.map s_pat ps))
-    | P_tup ps -> re (P_tup (List.map s_pat ps))
-    | P_list ps -> re (P_list (List.map s_pat ps))
-    | P_cons (p1,p2) -> re (P_cons (s_pat p1, s_pat p2))
-  and s_fpat (FP_aux (FP_Fpat (id, p), (l,annot))) =
-    FP_aux (FP_Fpat (id, s_pat p), (l,s_tannot annot))
-  in
-  let rec s_exp (E_aux (e,(l,annot))) =
-    let re e = E_aux (e,(l,s_tannot annot)) in
-      match e with
-      | E_block es -> re (E_block (List.map s_exp es))
-      | E_nondet es -> re (E_nondet (List.map s_exp es))
-      | E_id _
-      | E_ref _
-      | E_lit _
-      | E_internal_value _
-        -> re e
-      | E_sizeof ne -> begin
-         let ne' = subst_nexp substs ne in
-         match ne' with
-         | Nexp_aux (Nexp_constant i,l) -> re (E_lit (L_aux (L_num i,l)))
-         | _ -> re (E_sizeof ne')
-      end
-      | E_constraint nc -> re (E_constraint (subst_nc substs nc))
-      | E_cast (t,e') -> re (E_cast (s_t t, s_exp e'))
-      | E_app (id,es) -> re (E_app (id, List.map s_exp es))
-      | E_app_infix (e1,id,e2) -> re (E_app_infix (s_exp e1,id,s_exp e2))
-      | E_tuple es -> re (E_tuple (List.map s_exp es))
-      | E_if (e1,e2,e3) -> re (E_if (s_exp e1, s_exp e2, s_exp e3))
-      | E_for (id,e1,e2,e3,ord,e4) -> re (E_for (id,s_exp e1,s_exp e2,s_exp e3,ord,s_exp e4))
-      | E_loop (loop,e1,e2) -> re (E_loop (loop,s_exp e1,s_exp e2))
-      | E_vector es -> re (E_vector (List.map s_exp es))
-      | E_vector_access (e1,e2) -> re (E_vector_access (s_exp e1,s_exp e2))
-      | E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (s_exp e1,s_exp e2,s_exp e3))
-      | E_vector_update (e1,e2,e3) -> re (E_vector_update (s_exp e1,s_exp e2,s_exp e3))
-      | E_vector_update_subrange (e1,e2,e3,e4) -> re (E_vector_update_subrange (s_exp e1,s_exp e2,s_exp e3,s_exp e4))
-      | E_vector_append (e1,e2) -> re (E_vector_append (s_exp e1,s_exp e2))
-      | E_list es -> re (E_list (List.map s_exp es))
-      | E_cons (e1,e2) -> re (E_cons (s_exp e1,s_exp e2))
-      | E_record fes -> re (E_record (List.map s_fexp fes))
-      | E_record_update (e,fes) -> re (E_record_update (s_exp e, List.map s_fexp fes))
-      | E_field (e,id) -> re (E_field (s_exp e,id))
-      | E_case (e,cases) -> re (E_case (s_exp e, List.map s_pexp cases))
-      | E_let (lb,e) -> re (E_let (s_letbind lb, s_exp e))
-      | E_assign (le,e) -> re (E_assign (s_lexp le, s_exp e))
-      | E_exit e -> re (E_exit (s_exp e))
-      | E_return e -> re (E_return (s_exp e))
-      | E_assert (e1,e2) -> re (E_assert (s_exp e1,s_exp e2))
-      | E_var (le,e1,e2) -> re (E_var (s_lexp le, s_exp e1, s_exp e2))
-      | E_internal_plet (p,e1,e2) -> re (E_internal_plet (s_pat p, s_exp e1, s_exp e2))
-      | E_internal_return e -> re (E_internal_return (s_exp e))
-      | E_throw e -> re (E_throw (s_exp e))
-      | E_try (e,cases) -> re (E_try (s_exp e, List.map s_pexp cases))
-    and s_fexp (FE_aux (FE_Fexp (id,e), (l,annot))) =
-      FE_aux (FE_Fexp (id,s_exp e),(l,s_tannot annot))
-    and s_pexp = function
-      | (Pat_aux (Pat_exp (p,e),(l,annot))) ->
-         Pat_aux (Pat_exp (s_pat p, s_exp e),(l,s_tannot annot))
-      | (Pat_aux (Pat_when (p,e1,e2),(l,annot))) ->
-         Pat_aux (Pat_when (s_pat p, s_exp e1, s_exp e2),(l,s_tannot annot))
-    and s_letbind (LB_aux (lb,(l,annot))) =
-      match lb with
-      | LB_val (p,e) -> LB_aux (LB_val (s_pat p,s_exp e), (l,s_tannot annot))
-    and s_lexp (LEXP_aux (e,(l,annot))) =
-      let re e = LEXP_aux (e,(l,s_tannot annot)) in
-      match e with
-      | LEXP_id _ -> re e
-      | LEXP_cast (typ,id) -> re (LEXP_cast (s_t typ, id))
-      | LEXP_memory (id,es) -> re (LEXP_memory (id,List.map s_exp es))
-      | LEXP_tup les -> re (LEXP_tup (List.map s_lexp les))
-      | LEXP_vector (le,e) -> re (LEXP_vector (s_lexp le, s_exp e))
-      | LEXP_vector_range (le,e1,e2) -> re (LEXP_vector_range (s_lexp le, s_exp e1, s_exp e2))
-      | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map s_lexp les))
-      | LEXP_field (le,id) -> re (LEXP_field (s_lexp le, id))
-      | LEXP_deref e -> re (LEXP_deref (s_exp e))
-  in (s_pat,s_exp)
-let nexp_subst_pat substs = fst (nexp_subst_fns substs)
-let nexp_subst_exp substs = snd (nexp_subst_fns substs)
-
-let bindings_from_pat p =
-  let rec aux_pat (P_aux (p,(l,annot))) =
-    let env = Type_check.env_of_annot (l, annot) in
-    match p with
-    | P_lit _
-    | P_wild
-      -> []
-    | P_or (p1, p2) -> aux_pat p1 @ aux_pat p2
-    | P_not (p) -> aux_pat p
-    | P_as (p,id) -> id::(aux_pat p)
-    | P_typ (_,p) -> aux_pat p
-    | P_id id ->
-       if pat_id_is_variable env id then [id] else []
-    | P_var (p,kid) -> aux_pat p
-    | P_vector ps
-    | P_vector_concat ps
-    | P_string_append ps
-    | P_app (_,ps)
-    | P_tup ps
-    | P_list ps
-      -> List.concat (List.map aux_pat ps)
-    | P_record (fps,_) -> List.concat (List.map aux_fpat fps)
-    | P_cons (p1,p2) -> aux_pat p1 @ aux_pat p2
-  and aux_fpat (FP_aux (FP_Fpat (_,p), _)) = aux_pat p
-  in aux_pat p
-
-let remove_bound (substs,ksubsts) pat =
-  let bound = bindings_from_pat pat in
-  List.fold_left (fun sub v -> Bindings.remove v sub) substs bound, ksubsts
-
-(* Attempt simple pattern matches *)
-let lit_match = function
-  | (L_zero | L_false), (L_zero | L_false) -> true
-  | (L_one  | L_true ), (L_one  | L_true ) -> true
-  | L_num i1, L_num i2 -> Big_int.equal i1 i2
-  | l1,l2 -> l1 = l2
-
-(* There's no undefined nexp, so replace undefined sizes with a plausible size.
-   32 is used as a sensible default. *)
-
-let fabricate_nexp_exist env l typ kids nc typ' =
-  match kids,nc,Env.expand_synonyms env typ' with
-  | ([kid],NC_aux (NC_set (kid',i::_),_),
-     Typ_aux (Typ_app (Id_aux (Id "atom",_),
-                       [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_))
-      when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 ->
-     Nexp_aux (Nexp_constant i,Unknown)
-  | ([kid],NC_aux (NC_true,_),
-     Typ_aux (Typ_app (Id_aux (Id "atom",_),
-                       [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_))
-      when Kid.compare kid kid'' = 0 ->
-     nint 32
-  | ([kid],NC_aux (NC_set (kid',i::_),_),
-     Typ_aux (Typ_app (Id_aux (Id "range",_),
-                       [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_);
-                        A_aux (A_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_))
-      when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 &&
-        Kid.compare kid kid''' = 0 ->
-     Nexp_aux (Nexp_constant i,Unknown)
-  | ([kid],NC_aux (NC_true,_),
-     Typ_aux (Typ_app (Id_aux (Id "range",_),
-                       [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_);
-                        A_aux (A_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_))
-      when Kid.compare kid kid'' = 0 &&
-        Kid.compare kid kid''' = 0 ->
-     nint 32
-  | ([], _, typ) -> nint 32
-  | (kids, nc, typ) ->
-     raise (Reporting.err_general l
-              ("Undefined value at unsupported type " ^ string_of_typ typ ^ " with " ^ Util.string_of_list ", " string_of_kid kids))
-
-let fabricate_nexp l tannot =
-  match destruct_tannot tannot with
-  | None -> nint 32
-  | Some (env,typ,_) ->
-     match Type_check.destruct_exist (Type_check.Env.expand_synonyms env typ) with
-     | None -> nint 32
-     (* TODO: check this *)
-     | Some (kopts,nc,typ') -> fabricate_nexp_exist env l typ (List.map kopt_kid kopts) nc typ'
-
-let atom_typ_kid kid = function
-  | Typ_aux (Typ_app (Id_aux (Id "atom",_),
-                      [A_aux (A_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_) ->
-     Kid.compare kid kid' = 0
-  | _ -> false
-
-(* We reduce casts in a few cases, in particular to ensure that where the
-   type checker has added a ({'n, true. atom('n)}) ex_int(...) cast we can
-   fill in the 'n.  For undefined we fabricate a suitable value for 'n. *)
-
-let reduce_cast typ exp l annot =
-  let env = env_of_annot (l,annot) in
-  let typ' = Env.base_typ_of env typ in
-  match exp, destruct_exist (Env.expand_synonyms env typ') with
-  | E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' ->
-     let nc_env = Env.add_typ_var l kopt env in
-     let nc_env = Env.add_constraint (nc_eq (nvar (kopt_kid kopt)) (nconstant n)) nc_env in
-     if prove __POS__ nc_env nc
-     then exp
-     else raise (Reporting.err_unreachable l __POS__
-                   ("Constant propagation error: literal " ^ Big_int.to_string n ^
-                       " does not satisfy constraint " ^ string_of_n_constraint nc))
-  | E_aux (E_lit (L_aux (L_undef,_)),_), Some ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' ->
-     let nexp = fabricate_nexp_exist env Unknown typ [kopt_kid kopt] nc typ'' in
-     let newtyp = subst_src_typ (KBindings.singleton (kopt_kid kopt) nexp) typ'' in
-     E_aux (E_cast (newtyp, exp), (Generated l,replace_typ newtyp annot))
-  | E_aux (E_cast (_,
-                   (E_aux (E_lit (L_aux (L_undef,_)),_) as exp)),_),
-     Some ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' ->
-     let nexp = fabricate_nexp_exist env Unknown typ [kopt_kid kopt] nc typ'' in
-     let newtyp = subst_src_typ (KBindings.singleton (kopt_kid kopt) nexp) typ'' in
-     E_aux (E_cast (newtyp, exp), (Generated l,replace_typ newtyp annot))
-  | _ -> E_aux (E_cast (typ,exp),(l,annot))
-
-(* Used for constant propagation in pattern matches *)
-type 'a matchresult =
-  | DoesMatch of 'a
-  | DoesNotMatch
-  | GiveUp
-
-(* Remove top-level casts from an expression.  Useful when we need to look at
-   subexpressions to reduce something, but could break type-checking if we used
-   it everywhere. *)
-let rec drop_casts = function
-  | E_aux (E_cast (_,e),_) -> drop_casts e
-  | exp -> exp
-
-let int_of_str_lit = function
-  | L_hex hex -> Big_int.of_string ("0x" ^ hex)
-  | L_bin bin -> Big_int.of_string ("0b" ^ bin)
-  | _ -> assert false
-
-let bits_of_lit = function
-  | L_bin bin -> bin
-  | L_hex hex -> hex_to_bin hex
-  | _ -> assert false
-
-let slice_lit (L_aux (lit,ll)) i len (Ord_aux (ord,_)) =
-  let i = Big_int.to_int i in
-  let len = Big_int.to_int len in
-  let bin = bits_of_lit lit in
-  match match ord with
-  | Ord_inc -> Some i
-  | Ord_dec -> Some (String.length bin - i - len)
-  | Ord_var _ -> None
-  with
-  | None -> None
-  | Some i ->
-     Some (L_aux (L_bin (String.sub bin i len),Generated ll))
-
-let concat_vec lit1 lit2 =
-  let bits1 = bits_of_lit lit1 in
-  let bits2 = bits_of_lit lit2 in
-  L_bin (bits1 ^ bits2)
-
-let lit_eq (L_aux (l1,_)) (L_aux (l2,_)) =
-  match l1,l2 with
-  | (L_zero|L_false), (L_zero|L_false)
-  | (L_one |L_true ), (L_one |L_true)
-    -> Some true
-  | (L_hex _| L_bin _), (L_hex _|L_bin _)
-    -> Some (Big_int.equal (int_of_str_lit l1) (int_of_str_lit l2))
-  | L_undef, _ | _, L_undef -> None
-  | L_num i1, L_num i2 -> Some (Big_int.equal i1 i2)
-  | _ -> Some (l1 = l2)
-
-let try_app (l,ann) (id,args) =
-  let new_l = Generated l in
-  let env = env_of_annot (l,ann) in
-  let get_overloads f = List.map string_of_id
-    (Env.get_overloads (Id_aux (Id f, Parse_ast.Unknown)) env @
-    Env.get_overloads (Id_aux (DeIid f, Parse_ast.Unknown)) env) in
-  let is_id f = List.mem (string_of_id id) (f :: get_overloads f) in
-  if is_id "==" || is_id "!=" then
-    match args with
-    | [E_aux (E_lit l1,_); E_aux (E_lit l2,_)] ->
-       let lit b = if b then L_true else L_false in
-       let lit b = lit (if is_id "==" then b else not b) in
-       (match lit_eq l1 l2 with
-       | None -> None
-       | Some b -> Some (E_aux (E_lit (L_aux (lit b,new_l)),(l,ann))))
-    | _ -> None
-  else if is_id "cast_bit_bool" then
-    match args with
-    | [E_aux (E_lit L_aux (L_zero,_),_)] -> Some (E_aux (E_lit (L_aux (L_false,new_l)),(l,ann)))
-    | [E_aux (E_lit L_aux (L_one ,_),_)] -> Some (E_aux (E_lit (L_aux (L_true ,new_l)),(l,ann)))
-    | _ -> None
-  else if is_id "UInt" || is_id "unsigned" then
-    match args with
-    | [E_aux (E_lit L_aux ((L_hex _| L_bin _) as lit,_), _)] ->
-       Some (E_aux (E_lit (L_aux (L_num (int_of_str_lit lit),new_l)),(l,ann)))
-    | _ -> None
-  else if is_id "slice" then
-    match args with
-    | [E_aux (E_lit (L_aux ((L_hex _| L_bin _),_) as lit), annot);
-       E_aux (E_lit L_aux (L_num i,_), _);
-       E_aux (E_lit L_aux (L_num len,_), _)] ->
-       (match Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) with
-       | Typ_aux (Typ_app (_,[_;A_aux (A_order ord,_);_]),_) ->
-          (match slice_lit lit i len ord with
-          | Some lit' -> Some (E_aux (E_lit lit',(l,ann)))
-          | None -> None)
-       | _ -> None)
-    | _ -> None
-  else if is_id "bitvector_concat" then
-    match args with
-    | [E_aux (E_lit L_aux ((L_hex _| L_bin _) as lit1,_), _);
-       E_aux (E_lit L_aux ((L_hex _| L_bin _) as lit2,_), _)] ->
-       Some (E_aux (E_lit (L_aux (concat_vec lit1 lit2,new_l)),(l,ann)))
-    | _ -> None
-  else if is_id "shl_int" then
-    match args with
-    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
-       Some (E_aux (E_lit (L_aux (L_num (Big_int.shift_left i (Big_int.to_int j)),new_l)),(l,ann)))
-    | _ -> None
-  else if is_id "mult_atom" || is_id "mult_int" || is_id "mult_range" then
-    match args with
-    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
-       Some (E_aux (E_lit (L_aux (L_num (Big_int.mul i j),new_l)),(l,ann)))
-    | _ -> None
-  else if is_id "quotient_nat" then
-    match args with
-    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
-       Some (E_aux (E_lit (L_aux (L_num (Big_int.div i j),new_l)),(l,ann)))
-    | _ -> None
-  else if is_id "add_atom" || is_id "add_int" || is_id "add_range" then
-    match args with
-    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
-       Some (E_aux (E_lit (L_aux (L_num (Big_int.add i j),new_l)),(l,ann)))
-    | _ -> None
-  else if is_id "negate_range" then
-    match args with
-    | [E_aux (E_lit L_aux (L_num i,_),_)] ->
-       Some (E_aux (E_lit (L_aux (L_num (Big_int.negate i),new_l)),(l,ann)))
-    | _ -> None
-  else if is_id "ex_int" then
-    match args with
-    | [E_aux (E_lit lit,(l,_))] -> Some (E_aux (E_lit lit,(l,ann)))
-    | [E_aux (E_cast (_,(E_aux (E_lit (L_aux (L_undef,_)),_) as e)),(l,_))] ->
-       Some (reduce_cast (typ_of_annot (l,ann)) e l ann)
-    | _ -> None
-  else if is_id "vector_access" || is_id "bitvector_access" then
-    match args with
-    | [E_aux (E_lit L_aux ((L_hex _ | L_bin _) as lit,_),_);
-       E_aux (E_lit L_aux (L_num i,_),_)] ->
-       let v = int_of_str_lit lit in
-       let b = Big_int.bitwise_and (Big_int.shift_right v (Big_int.to_int i)) (Big_int.of_int 1) in
-       let lit' = if Big_int.equal b (Big_int.of_int 1) then L_one else L_zero in
-       Some (E_aux (E_lit (L_aux (lit',new_l)),(l,ann)))
-    | _ -> None
-  else None
-
-
-let construct_lit_vector args =
-  let rec aux l = function
-    | [] -> Some (L_aux (L_bin (String.concat "" (List.rev l)),Unknown))
-    | E_aux (E_lit (L_aux ((L_zero | L_one) as lit,_)),_)::t ->
-       aux ((if lit = L_zero then "0" else "1")::l) t
-    | _ -> None
-  in aux [] args
-
 type pat_choice = Parse_ast.l * (int * int * (id * tannot exp) list)
 
 (* We may need to split up a pattern match if (1) we've been told to case split
@@ -937,64 +432,15 @@ type split =
       list
   | ConstrSplit of (tannot pat * nexp KBindings.t) list
 
-let threaded_map f state l =
-  let l',state' =
-    List.fold_left (fun (tl,state) element -> let (el',state') = f state element in (el'::tl,state'))
-      ([],state) l
-  in List.rev l',state'
-
 let isubst_minus subst subst' =
   Bindings.merge (fun _ x y -> match x,y with (Some a), None -> Some a | _, _ -> None) subst subst'
 
-let isubst_minus_set subst set =
-  IdSet.fold Bindings.remove set subst
-
-let assigned_vars exp =
-  fst (Rewriter.fold_exp
-         { (Rewriter.compute_exp_alg IdSet.empty IdSet.union) with
-           Rewriter.lEXP_id = (fun id -> IdSet.singleton id, LEXP_id id);
-           Rewriter.lEXP_cast = (fun (ty,id) -> IdSet.singleton id, LEXP_cast (ty,id)) }
-         exp)
-
 let referenced_vars exp =
   let open Rewriter in
   fst (fold_exp
          { (compute_exp_alg IdSet.empty IdSet.union) with
            e_ref = (fun id -> IdSet.singleton id, E_ref id) } exp)
 
-let assigned_vars_in_fexps fes =
-  List.fold_left
-    (fun vs (FE_aux (FE_Fexp (_,e),_)) -> IdSet.union vs (assigned_vars e))
-    IdSet.empty
-    fes
-
-let assigned_vars_in_pexp (Pat_aux (p,_)) =
-  match p with
-  | Pat_exp (_,e) -> assigned_vars e
-  | Pat_when (p,e1,e2) -> IdSet.union (assigned_vars e1) (assigned_vars e2)
-
-let rec assigned_vars_in_lexp (LEXP_aux (le,_)) =
-  match le with
-  | LEXP_id id
-  | LEXP_cast (_,id) -> IdSet.singleton id
-  | LEXP_tup lexps
-  | LEXP_vector_concat lexps -> 
-     List.fold_left (fun vs le -> IdSet.union vs (assigned_vars_in_lexp le)) IdSet.empty lexps
-  | LEXP_memory (_,es) -> List.fold_left (fun vs e -> IdSet.union vs (assigned_vars e)) IdSet.empty es
-  | LEXP_vector (le,e) -> IdSet.union (assigned_vars_in_lexp le) (assigned_vars e)
-  | LEXP_vector_range (le,e1,e2) ->
-     IdSet.union (assigned_vars_in_lexp le) (IdSet.union (assigned_vars e1) (assigned_vars e2))
-  | LEXP_field (le,_) -> assigned_vars_in_lexp le
-  | LEXP_deref e -> assigned_vars e
-
-(* Add a cast to undefined so that it retains its type, otherwise it can't be
-   substituted safely *)
-let keep_undef_typ value =
-  match value with
-  | E_aux (E_lit (L_aux (L_undef,lann)),eann) ->
-     E_aux (E_cast (typ_of_annot eann,value),(Generated Unknown,snd eann))
-  | _ -> value
-
 let freshen_id =
   let counter = ref 0 in
   fun id ->
@@ -1174,13 +620,6 @@ let apply_pat_choices choices =
     e_assert = rewrite_assert;
     e_case = rewrite_case }
 
-(* Check whether the current environment with the given kid assignments is
-   inconsistent (and hence whether the code is dead) *)
-let is_env_inconsistent env ksubsts =
-  let env = KBindings.fold (fun k nexp env ->
-    Env.add_constraint (nc_eq (nvar k) nexp) env) ksubsts env in
-  prove __POS__ env nc_false
-
 let split_defs all_errors splits defs =
   let no_errors_happened = ref true in
   let split_constructors (Defs defs) =
@@ -1209,467 +648,9 @@ let split_defs all_errors splits defs =
 
   let (refinements, defs') = split_constructors defs in
 
-  (* COULD DO: dead code is only eliminated at if expressions, but we could
-     also cut out impossible case branches and code after assertions. *)
-
-  (* Constant propogation.
-     Takes maps of immutable/mutable variables to subsitute.
-     The substs argument also contains the current type-level kid refinements
-     so that we can check for dead code.
-     Extremely conservative about evaluation order of assignments in
-     subexpressions, dropping assignments rather than committing to
-     any particular order *)
-  let rec const_prop_exp ref_vars substs assigns ((E_aux (e,(l,annot))) as exp) =
-    (* Functions to treat lists and tuples of subexpressions as possibly
-       non-deterministic: that is, we stop making any assumptions about
-       variables that are assigned to in any of the subexpressions *)
-    let non_det_exp_list es =
-      let assigned_in =
-        List.fold_left (fun vs exp -> IdSet.union vs (assigned_vars exp))
-          IdSet.empty es in
-      let assigns = isubst_minus_set assigns assigned_in in
-      let es' = List.map (fun e -> fst (const_prop_exp ref_vars substs assigns e)) es in
-      es',assigns
-    in
-    let non_det_exp_2 e1 e2 =
-       let assigned_in_e12 = IdSet.union (assigned_vars e1) (assigned_vars e2) in
-       let assigns = isubst_minus_set assigns assigned_in_e12 in
-       let e1',_ = const_prop_exp ref_vars substs assigns e1 in
-       let e2',_ = const_prop_exp ref_vars substs assigns e2 in
-       e1',e2',assigns
-    in
-    let non_det_exp_3 e1 e2 e3 =
-       let assigned_in_e12 = IdSet.union (assigned_vars e1) (assigned_vars e2) in
-       let assigned_in_e123 = IdSet.union assigned_in_e12 (assigned_vars e3) in
-       let assigns = isubst_minus_set assigns assigned_in_e123 in
-       let e1',_ = const_prop_exp ref_vars substs assigns e1 in
-       let e2',_ = const_prop_exp ref_vars substs assigns e2 in
-       let e3',_ = const_prop_exp ref_vars substs assigns e3 in
-       e1',e2',e3',assigns
-    in
-    let non_det_exp_4 e1 e2 e3 e4 =
-       let assigned_in_e12 = IdSet.union (assigned_vars e1) (assigned_vars e2) in
-       let assigned_in_e123 = IdSet.union assigned_in_e12 (assigned_vars e3) in
-       let assigned_in_e1234 = IdSet.union assigned_in_e123 (assigned_vars e4) in
-       let assigns = isubst_minus_set assigns assigned_in_e1234 in
-       let e1',_ = const_prop_exp ref_vars substs assigns e1 in
-       let e2',_ = const_prop_exp ref_vars substs assigns e2 in
-       let e3',_ = const_prop_exp ref_vars substs assigns e3 in
-       let e4',_ = const_prop_exp ref_vars substs assigns e4 in
-       e1',e2',e3',e4',assigns
-    in
-    let re e assigns = E_aux (e,(l,annot)),assigns in
-    match e with
-      (* TODO: are there more circumstances in which we should get rid of these? *)
-    | E_block [e] -> const_prop_exp ref_vars substs assigns e
-    | E_block es ->
-       let es',assigns = threaded_map (const_prop_exp ref_vars substs) assigns es in
-       re (E_block es') assigns
-    | E_nondet es ->
-       let es',assigns = non_det_exp_list es in
-       re (E_nondet es') assigns
-    | E_id id ->
-       let env = Type_check.env_of_annot (l, annot) in
-       (try
-         match Env.lookup_id id env with
-         | Local (Immutable,_) -> Bindings.find id (fst substs)
-         | Local (Mutable,_)   -> Bindings.find id assigns
-         | _ -> exp
-       with Not_found -> exp),assigns
-    | E_lit _
-    | E_sizeof _
-    | E_constraint _
-      -> exp,assigns
-    | E_cast (t,e') ->
-       let e'',assigns = const_prop_exp ref_vars substs assigns e' in
-       if is_value e''
-       then reduce_cast t e'' l annot, assigns
-       else re (E_cast (t, e'')) assigns
-    | E_app (id,es) ->
-       let es',assigns = non_det_exp_list es in
-       let env = Type_check.env_of_annot (l, annot) in
-       (match try_app (l,annot) (id,es') with
-       | None ->
-          (match const_prop_try_fn ref_vars l env (id,es') with
-          | None -> re (E_app (id,es')) assigns
-          | Some r -> r,assigns)
-       | Some r -> r,assigns)
-    | E_tuple es ->
-       let es',assigns = non_det_exp_list es in
-       re (E_tuple es') assigns
-    | E_if (e1,e2,e3) ->
-       let e1',assigns = const_prop_exp ref_vars substs assigns e1 in
-       let e1_no_casts = drop_casts e1' in
-       (match e1_no_casts with
-       | E_aux (E_lit (L_aux ((L_true|L_false) as lit ,_)),_) ->
-          (match lit with
-          | L_true -> const_prop_exp ref_vars substs assigns e2
-          |  _     -> const_prop_exp ref_vars substs assigns e3)
-       | _ ->
-          (* If the guard is an equality check, propagate the value. *)
-          let env1 = env_of e1_no_casts in
-          let is_equal id =
-            List.exists (fun id' -> Id.compare id id' == 0)
-              (Env.get_overloads (Id_aux (DeIid "==", Parse_ast.Unknown))
-                 env1)
-          in
-          let substs_true =
-            match e1_no_casts with
-            | E_aux (E_app (id, [E_aux (E_id var,_); vl]),_)
-            | E_aux (E_app (id, [vl; E_aux (E_id var,_)]),_)
-                when is_equal id ->
-               if is_value vl then
-                 (match Env.lookup_id var env1 with
-                 | Local (Immutable,_) -> Bindings.add var vl (fst substs),snd substs
-                 | _ -> substs)
-               else substs
-            | _ -> substs
-          in
-          (* Discard impossible branches *)
-          if is_env_inconsistent (env_of e2) (snd substs) then
-            const_prop_exp ref_vars substs assigns e3
-          else if is_env_inconsistent (env_of e3) (snd substs) then
-            const_prop_exp ref_vars substs_true assigns e2
-          else
-            let e2',assigns2 = const_prop_exp ref_vars substs_true assigns e2 in
-            let e3',assigns3 = const_prop_exp ref_vars substs assigns e3 in
-            let assigns = isubst_minus_set assigns (assigned_vars e2) in
-            let assigns = isubst_minus_set assigns (assigned_vars e3) in
-            re (E_if (e1',e2',e3')) assigns)
-    | E_for (id,e1,e2,e3,ord,e4) ->
-       (* Treat e1, e2 and e3 (from, to and by) as a non-det tuple *)
-       let e1',e2',e3',assigns = non_det_exp_3 e1 e2 e3 in
-       let assigns = isubst_minus_set assigns (assigned_vars e4) in
-       let e4',_ = const_prop_exp ref_vars (Bindings.remove id (fst substs),snd substs) assigns e4 in
-       re (E_for (id,e1',e2',e3',ord,e4')) assigns
-    | E_loop (loop,e1,e2) ->
-       let assigns = isubst_minus_set assigns (IdSet.union (assigned_vars e1) (assigned_vars e2)) in
-       let e1',_ = const_prop_exp ref_vars substs assigns e1 in
-       let e2',_ = const_prop_exp ref_vars substs assigns e2 in
-       re (E_loop (loop,e1',e2')) assigns
-    | E_vector es ->
-       let es',assigns = non_det_exp_list es in
-       begin
-         match construct_lit_vector es' with
-         | None -> re (E_vector es') assigns
-         | Some lit -> re (E_lit lit) assigns
-       end
-    | E_vector_access (e1,e2) ->
-       let e1',e2',assigns = non_det_exp_2 e1 e2 in
-       re (E_vector_access (e1',e2')) assigns
-    | E_vector_subrange (e1,e2,e3) ->
-       let e1',e2',e3',assigns = non_det_exp_3 e1 e2 e3 in
-       re (E_vector_subrange (e1',e2',e3')) assigns
-    | E_vector_update (e1,e2,e3) ->
-       let e1',e2',e3',assigns = non_det_exp_3 e1 e2 e3 in
-       re (E_vector_update (e1',e2',e3')) assigns
-    | E_vector_update_subrange (e1,e2,e3,e4) ->
-       let e1',e2',e3',e4',assigns = non_det_exp_4 e1 e2 e3 e4 in
-       re (E_vector_update_subrange (e1',e2',e3',e4')) assigns
-    | E_vector_append (e1,e2) ->
-       let e1',e2',assigns = non_det_exp_2 e1 e2 in
-       re (E_vector_append (e1',e2')) assigns
-    | E_list es ->
-       let es',assigns = non_det_exp_list es in
-       re (E_list es') assigns
-    | E_cons (e1,e2) ->
-       let e1',e2',assigns = non_det_exp_2 e1 e2 in
-       re (E_cons (e1',e2')) assigns
-    | E_record fes ->
-       let assigned_in_fes = assigned_vars_in_fexps fes in
-       let assigns = isubst_minus_set assigns assigned_in_fes in
-       re (E_record (const_prop_fexps ref_vars substs assigns fes)) assigns
-    | E_record_update (e,fes) ->
-       let assigned_in = IdSet.union (assigned_vars_in_fexps fes) (assigned_vars e) in
-       let assigns = isubst_minus_set assigns assigned_in in
-       let e',_ = const_prop_exp ref_vars substs assigns e in
-       re (E_record_update (e', const_prop_fexps ref_vars substs assigns fes)) assigns
-    | E_field (e,id) ->
-       let e',assigns = const_prop_exp ref_vars substs assigns e in
-       re (E_field (e',id)) assigns
-    | E_case (e,cases) ->
-       let e',assigns = const_prop_exp ref_vars substs assigns e in
-       (match can_match ref_vars e' cases substs assigns with
-       | None ->
-          let assigned_in =
-            List.fold_left (fun vs pe -> IdSet.union vs (assigned_vars_in_pexp pe))
-              IdSet.empty cases
-          in
-          let assigns' = isubst_minus_set assigns assigned_in in
-          re (E_case (e', List.map (const_prop_pexp ref_vars substs assigns) cases)) assigns'
-       | Some (E_aux (_,(_,annot')) as exp,newbindings,kbindings) ->
-          let exp = nexp_subst_exp (kbindings_from_list kbindings) exp in
-          let newbindings_env = bindings_from_list newbindings in
-          let substs' = bindings_union (fst substs) newbindings_env, snd substs in
-          const_prop_exp ref_vars substs' assigns exp)
-    | E_let (lb,e2) ->
-       begin
-         match lb with
-         | LB_aux (LB_val (p,e), annot) ->
-            let e',assigns = const_prop_exp ref_vars substs assigns e in
-            let substs' = remove_bound substs p in
-            let plain () =
-              let e2',assigns = const_prop_exp ref_vars substs' assigns e2 in
-              re (E_let (LB_aux (LB_val (p,e'), annot),
-                         e2')) assigns in
-            if is_value e' && not (is_value e) then
-              match can_match ref_vars e' [Pat_aux (Pat_exp (p,e2),(Unknown,empty_tannot))] substs assigns with
-              | None -> plain ()
-              | Some (e'',bindings,kbindings) ->
-                 let e'' = nexp_subst_exp (kbindings_from_list kbindings) e'' in
-                 let bindings = bindings_from_list bindings in
-                 let substs'' = bindings_union (fst substs') bindings, snd substs' in
-                 const_prop_exp ref_vars substs'' assigns e''
-            else plain ()
-       end
-    (* TODO maybe - tuple assignments *)
-    | E_assign (le,e) ->
-       let env = Type_check.env_of_annot (l, annot) in
-       let assigned_in = IdSet.union (assigned_vars_in_lexp le) (assigned_vars e) in
-       let assigns = isubst_minus_set assigns assigned_in in
-       let le',idopt = const_prop_lexp ref_vars substs assigns le in
-       let e',_ = const_prop_exp ref_vars substs assigns e in
-       let assigns =
-         match idopt with
-         | Some id ->
-            begin
-              match Env.lookup_id id env with
-              | Local (Mutable,_) | Unbound ->
-                 if is_value e' && not (IdSet.mem id ref_vars)
-                 then Bindings.add id (keep_undef_typ e') assigns
-                 else Bindings.remove id assigns
-              | _ -> assigns
-            end
-         | None -> assigns
-       in
-       re (E_assign (le', e')) assigns
-    | E_exit e ->
-       let e',_ = const_prop_exp ref_vars substs assigns e in
-       re (E_exit e') Bindings.empty
-    | E_ref id -> re (E_ref id) Bindings.empty
-    | E_throw e ->
-       let e',_ = const_prop_exp ref_vars substs assigns e in
-       re (E_throw e') Bindings.empty
-    | E_try (e,cases) ->
-       (* TODO: try and preserve *any* assignment info *)
-       let e',_ = const_prop_exp ref_vars substs assigns e in
-       re (E_case (e', List.map (const_prop_pexp ref_vars substs Bindings.empty) cases)) Bindings.empty
-    | E_return e ->
-       let e',_ = const_prop_exp ref_vars substs assigns e in
-       re (E_return e') Bindings.empty
-    | E_assert (e1,e2) ->
-       let e1',e2',assigns = non_det_exp_2 e1 e2 in
-       re (E_assert (e1',e2')) assigns
-
-    | E_app_infix _
-    | E_var _
-    | E_internal_plet _
-    | E_internal_return _
-    | E_internal_value _
-      -> raise (Reporting.err_unreachable l __POS__
-                  ("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp))
-  and const_prop_fexps ref_vars substs assigns fes =
-    List.map (const_prop_fexp ref_vars substs assigns) fes
-  and const_prop_fexp ref_vars substs assigns (FE_aux (FE_Fexp (id,e), annot)) =
-    FE_aux (FE_Fexp (id,fst (const_prop_exp ref_vars substs assigns e)),annot)
-  and const_prop_pexp ref_vars substs assigns = function
-    | (Pat_aux (Pat_exp (p,e),l)) ->
-       Pat_aux (Pat_exp (p,fst (const_prop_exp ref_vars (remove_bound substs p) assigns e)),l)
-    | (Pat_aux (Pat_when (p,e1,e2),l)) ->
-       let substs' = remove_bound substs p in
-       let e1',assigns = const_prop_exp ref_vars substs' assigns e1 in
-       Pat_aux (Pat_when (p, e1', fst (const_prop_exp ref_vars substs' assigns e2)),l)
-  and const_prop_lexp ref_vars substs assigns ((LEXP_aux (e,annot)) as le) =
-    let re e = LEXP_aux (e,annot), None in
-    match e with
-    | LEXP_id id (* shouldn't end up substituting here *)
-    | LEXP_cast (_,id)
-      -> le, Some id
-    | LEXP_memory (id,es) ->
-       re (LEXP_memory (id,List.map (fun e -> fst (const_prop_exp ref_vars substs assigns e)) es)) (* or here *)
-    | LEXP_tup les -> re (LEXP_tup (List.map (fun le -> fst (const_prop_lexp ref_vars substs assigns le)) les))
-    | LEXP_vector (le,e) -> re (LEXP_vector (fst (const_prop_lexp ref_vars substs assigns le), fst (const_prop_exp ref_vars substs assigns e)))
-    | LEXP_vector_range (le,e1,e2) ->
-       re (LEXP_vector_range (fst (const_prop_lexp ref_vars substs assigns le),
-                              fst (const_prop_exp ref_vars substs assigns e1),
-                              fst (const_prop_exp ref_vars substs assigns e2)))
-    | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map (fun le -> fst (const_prop_lexp ref_vars substs assigns le)) les))
-    | LEXP_field (le,id) -> re (LEXP_field (fst (const_prop_lexp ref_vars substs assigns le), id))
-    | LEXP_deref e ->
-       re (LEXP_deref (fst (const_prop_exp ref_vars substs assigns e)))
-  (* Reduce a function when
-     1. all arguments are values,
-     2. the function is pure,
-     3. the result is a value
-     (and 4. the function is not scattered, but that's not terribly important)
-     to try and keep execution time and the results managable.
-  *)
-  and const_prop_try_fn ref_vars l env (id,args) =
-    if not (List.for_all is_value args) then
-      None
-    else
-      let (tq,typ) = Env.get_val_spec_orig id env in
-      let eff = match typ with
-        | Typ_aux (Typ_fn (_,_,eff),_) -> Some eff
-        | _ -> None
-      in
-      let Defs ds = defs in
-      match eff, list_extract (function
-      | (DEF_fundef (FD_aux (FD_function (_,_,eff,((FCL_aux (FCL_Funcl (id',_),_))::_ as fcls)),_)))
-        -> if Id.compare id id' = 0 then Some fcls else None
-      | _ -> None) ds with
-      | None,_ | _,None -> None
-      | Some eff,_ when not (is_pure eff) -> None
-      | Some _,Some fcls ->
-         let arg = match args with
-           | [] -> E_aux (E_lit (L_aux (L_unit,Generated l)),(Generated l,empty_tannot))
-           | [e] -> e
-           | _ -> E_aux (E_tuple args,(Generated l,empty_tannot)) in
-         let cases = List.map (function
-           | FCL_aux (FCL_Funcl (_,pexp), ann) -> pexp)
-           fcls in
-         match can_match_with_env ref_vars env arg cases (Bindings.empty,KBindings.empty) Bindings.empty with
-         | Some (exp,bindings,kbindings) ->
-            let substs = bindings_from_list bindings, kbindings_from_list kbindings in
-            let result,_ = const_prop_exp ref_vars substs Bindings.empty exp in
-            let result = match result with
-              | E_aux (E_return e,_) -> e
-              | _ -> result
-            in
-            if is_value result then Some result else None
-         | None -> None
-
-  and can_match_with_env ref_vars env (E_aux (e,(l,annot)) as exp0) cases (substs,ksubsts) assigns =
-    let rec findpat_generic check_pat description assigns = function
-      | [] -> (Reporting.print_err l "Monomorphisation"
-                 ("Failed to find a case for " ^ description); None)
-      | [Pat_aux (Pat_exp (P_aux (P_wild,_),exp),_)] -> Some (exp,[],[])
-      | (Pat_aux (Pat_exp (P_aux (P_typ (_,p),_),exp),ann))::tl ->
-         findpat_generic check_pat description assigns ((Pat_aux (Pat_exp (p,exp),ann))::tl)
-      | (Pat_aux (Pat_exp (P_aux (P_id id',_),exp),_))::tlx
-          when pat_id_is_variable env id' ->
-         Some (exp, [(id', exp0)], [])
-      | (Pat_aux (Pat_when (P_aux (P_id id',_),guard,exp),_))::tl
-          when pat_id_is_variable env id' -> begin
-            let substs = Bindings.add id' exp0 substs, ksubsts in
-            let (E_aux (guard,_)),assigns = const_prop_exp ref_vars substs assigns guard in
-            match guard with
-            | E_lit (L_aux (L_true,_)) -> Some (exp,[(id',exp0)],[])
-            | E_lit (L_aux (L_false,_)) -> findpat_generic check_pat description assigns tl
-            | _ -> None
-          end
-      | (Pat_aux (Pat_when (p,guard,exp),_))::tl -> begin
-        match check_pat p with
-        | DoesNotMatch -> findpat_generic check_pat description assigns tl
-        | DoesMatch (vsubst,ksubst) -> begin
-          let guard = nexp_subst_exp (kbindings_from_list ksubst) guard in
-          let substs = bindings_union substs (bindings_from_list vsubst),
-                       kbindings_union ksubsts (kbindings_from_list ksubst) in
-          let (E_aux (guard,_)),assigns = const_prop_exp ref_vars substs assigns guard in
-          match guard with
-          | E_lit (L_aux (L_true,_)) -> Some (exp,vsubst,ksubst)
-          | E_lit (L_aux (L_false,_)) -> findpat_generic check_pat description assigns tl
-          | _ -> None
-        end
-        | GiveUp -> None
-      end
-      | (Pat_aux (Pat_exp (p,exp),_))::tl ->
-         match check_pat p with
-         | DoesNotMatch -> findpat_generic check_pat description assigns tl
-         | DoesMatch (subst,ksubst) -> Some (exp,subst,ksubst)
-         | GiveUp -> None
-    in
-    match e with
-    | E_id id ->
-       (match Env.lookup_id id env with
-       | Enum _ ->
-          let checkpat = function
-            | P_aux (P_id id',_)
-            | P_aux (P_app (id',[]),_) ->
-               if Id.compare id id' = 0 then DoesMatch ([],[]) else DoesNotMatch
-            | P_aux (_,(l',_)) ->
-               (Reporting.print_err l' "Monomorphisation"
-                  "Unexpected kind of pattern for enumeration"; GiveUp)
-          in findpat_generic checkpat (string_of_id id) assigns cases
-       | _ -> None)
-    | E_lit (L_aux (lit_e, lit_l)) ->
-       let checkpat = function
-         | P_aux (P_lit (L_aux (lit_p, _)),_) ->
-            if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch
-         | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)),_) ->
-            begin
-              match lit_e with
-              | L_num i ->
-                 DoesMatch ([id, E_aux (e,(l,annot))],
-                            [kid,Nexp_aux (Nexp_constant i,Unknown)])
-              (* For undefined we fix the type-level size (because there's no good
-                 way to construct an undefined size), but leave the term as undefined
-                 to make the meaning clear. *)
-              | L_undef ->
-                 let nexp = fabricate_nexp l annot in
-                 let typ = subst_src_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in
-                 DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,empty_tannot))),(l,empty_tannot))],
-                            [kid,nexp])
-              | _ ->
-                 (Reporting.print_err lit_l "Monomorphisation"
-                    "Unexpected kind of literal for var match"; GiveUp)
-            end
-         | P_aux (_,(l',_)) ->
-            (Reporting.print_err l' "Monomorphisation"
-               "Unexpected kind of pattern for literal"; GiveUp)
-       in findpat_generic checkpat "literal" assigns cases
-    | E_vector es when List.for_all (function (E_aux (E_lit _,_)) -> true | _ -> false) es ->
-       let checkpat = function
-         | P_aux (P_vector ps,_) ->
-            let matches = List.map2 (fun e p ->
-              match e, p with
-              | E_aux (E_lit (L_aux (lit,_)),_), P_aux (P_lit (L_aux (lit',_)),_) ->
-                 if lit_match (lit,lit') then DoesMatch ([],[]) else DoesNotMatch
-              | E_aux (E_lit l,_), P_aux (P_id var,_) when pat_id_is_variable env var ->
-                 DoesMatch ([var, e],[])
-              | _ -> GiveUp) es ps in
-            let final = List.fold_left (fun acc m -> match acc, m with
-              | _, GiveUp -> GiveUp
-              | GiveUp, _ -> GiveUp
-              | DoesMatch (sub,ksub), DoesMatch(sub',ksub') -> DoesMatch(sub@sub',ksub@ksub')
-              | _ -> DoesNotMatch) (DoesMatch ([],[])) matches in
-            (match final with
-            | GiveUp ->
-               (Reporting.print_err l "Monomorphisation"
-                  "Unexpected kind of pattern for vector literal"; GiveUp)
-            | _ -> final)
-         | _ ->
-            (Reporting.print_err l "Monomorphisation"
-               "Unexpected kind of pattern for vector literal"; GiveUp)
-       in findpat_generic checkpat "vector literal" assigns cases
-
-    | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)) ->
-       let checkpat = function
-         | P_aux (P_lit (L_aux (lit_p, _)),_) -> DoesNotMatch
-         | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)),_) ->
-              (* For undefined we fix the type-level size (because there's no good
-                 way to construct an undefined size), but leave the term as undefined
-                 to make the meaning clear. *)
-            let nexp = fabricate_nexp l annot in
-            let kids = equal_kids (env_of_annot p_id_annot) kid in
-            let ksubst = KidSet.fold (fun k b -> KBindings.add k nexp b) kids KBindings.empty in
-            let typ = subst_src_typ ksubst (typ_of_annot p_id_annot) in
-            DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,empty_tannot))],
-                       KBindings.bindings ksubst)
-         | P_aux (_,(l',_)) ->
-            (Reporting.print_err l' "Monomorphisation"
-               "Unexpected kind of pattern for literal"; GiveUp)
-       in findpat_generic checkpat "literal" assigns cases
-    | _ -> None
-
-  and can_match ref_vars exp =
-    let env = Type_check.env_of exp in
-    can_match_with_env ref_vars env exp
-  in
-
   let subst_exp ref_vars substs ksubsts exp =
     let substs = bindings_from_list substs, ksubsts in
-    fst (const_prop_exp ref_vars substs Bindings.empty exp)
+    fst (Constant_propagation.const_prop defs ref_vars substs Bindings.empty exp)
   in
 
   (* Split a variable pattern into every possible value *)
@@ -1824,7 +805,7 @@ let split_defs all_errors splits defs =
            (match spl p' with
            | None -> None
            | Some ps ->
-              let kids = equal_kids (env_of_pat p') kid in
+              let kids = Spec_analysis.equal_kids (env_of_pat p') kid in
               Some (List.map (fun (p,sub,pchoices,ksub) ->
                 P_aux (P_var (p,tp),(l,annot)), sub, pchoices,
                 List.concat
@@ -1949,7 +930,7 @@ let split_defs all_errors splits defs =
       match match_l l with
       | [] -> p
       | lvs ->
-         let pvs = bindings_from_pat p in
+         let pvs = Spec_analysis.bindings_from_pat p in
          let pvs = List.map string_of_id pvs in
          let overlap = List.exists (fun (v,_) -> List.mem v pvs) lvs in
          let () =
@@ -2033,7 +1014,7 @@ let split_defs all_errors splits defs =
               if check_split_size patsubsts (pat_loc p) then
                 List.map (fun (pat',substs,pchoices,ksubsts) ->
                   let ksubsts = kbindings_from_list ksubsts in
-                  let exp' = nexp_subst_exp ksubsts e in
+                  let exp' = Spec_analysis.nexp_subst_exp ksubsts e in
                   let exp' = subst_exp ref_vars substs ksubsts exp' in
                   let exp' = apply_pat_choices pchoices exp' in
                   let exp' = stop_at_false_assertions exp' in
@@ -2042,8 +1023,8 @@ let split_defs all_errors splits defs =
               else nosplit
            | ConstrSplit patnsubsts ->
               List.map (fun (pat',nsubst) ->
-                let pat' = nexp_subst_pat nsubst pat' in
-                let exp' = nexp_subst_exp nsubst e in
+                let pat' = Spec_analysis.nexp_subst_pat nsubst pat' in
+                let exp' = Spec_analysis.nexp_subst_exp nsubst e in
                 Pat_aux (Pat_exp (pat', map_exp exp'),l)
               ) patnsubsts)
         | Pat_aux (Pat_when (p,e1,e2),l) ->
@@ -2054,10 +1035,10 @@ let split_defs all_errors splits defs =
               if check_split_size patsubsts (pat_loc p) then
                 List.map (fun (pat',substs,pchoices,ksubsts) ->
                   let ksubsts = kbindings_from_list ksubsts in
-                  let exp1' = nexp_subst_exp ksubsts e1 in
+                  let exp1' = Spec_analysis.nexp_subst_exp ksubsts e1 in
                   let exp1' = subst_exp ref_vars substs ksubsts exp1' in
                   let exp1' = apply_pat_choices pchoices exp1' in
-                  let exp2' = nexp_subst_exp ksubsts e2 in
+                  let exp2' = Spec_analysis.nexp_subst_exp ksubsts e2 in
                   let exp2' = subst_exp ref_vars substs ksubsts exp2' in
                   let exp2' = apply_pat_choices pchoices exp2' in
                   let exp2' = stop_at_false_assertions exp2' in
@@ -2066,9 +1047,9 @@ let split_defs all_errors splits defs =
               else nosplit
            | ConstrSplit patnsubsts ->
               List.map (fun (pat',nsubst) ->
-                let pat' = nexp_subst_pat nsubst pat' in
-                let exp1' = nexp_subst_exp nsubst e1 in
-                let exp2' = nexp_subst_exp nsubst e2 in
+                let pat' = Spec_analysis.nexp_subst_pat nsubst pat' in
+                let exp1' = Spec_analysis.nexp_subst_exp nsubst e1 in
+                let exp2' = Spec_analysis.nexp_subst_exp nsubst e2 in
                 Pat_aux (Pat_when (pat', map_exp exp1', map_exp exp2'),l)
               ) patnsubsts)
       and map_letbind (LB_aux (lb,annot)) =
@@ -2798,12 +1779,12 @@ let update_env_new_kids env deps typ_env_pre typ_env_post =
    plus any new type variables. *)
 
 let update_env env deps pat typ_env_pre typ_env_post =
-  let bound = bindings_from_pat pat in
+  let bound = Spec_analysis.bindings_from_pat pat in
   let var_deps = List.fold_left (fun ds v -> Bindings.add v deps ds) env.var_deps bound in
   update_env_new_kids { env with var_deps = var_deps } deps typ_env_pre typ_env_post
 
 let assigned_vars_exps es =
-  List.fold_left (fun vs exp -> IdSet.union vs (assigned_vars exp))
+  List.fold_left (fun vs exp -> IdSet.union vs (Spec_analysis.assigned_vars exp))
     IdSet.empty es
 
 (* For adding control dependencies to mutable variables *)
@@ -3290,7 +2271,7 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions =
     let Typ_aux (typ,_) = Env.base_typ_of env (typ_of_annot annot) in
     match typ with
     | Typ_app (Id_aux (Id "atom",_),[A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]) ->
-       equal_kids env kid
+       Spec_analysis.equal_kids env kid
     | _ -> KidSet.empty
   in
   let default_split annot kids =
@@ -3365,7 +2346,7 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions =
          let s,v,k = aux pat in
          let kids = kids_bound_by_typ_pat tpat in
          let kids = KidSet.fold (fun kid s ->
-           KidSet.union s (equal_kids (env_of_annot (l,annot)) kid))
+           KidSet.union s (Spec_analysis.equal_kids (env_of_annot (l,annot)) kid))
            kids kids in
          s,v,KidSet.fold (fun kid k -> KBindings.add kid (Have (s, ExtraSplits.empty)) k) kids k
       | P_app (_,pats) -> of_list pats
@@ -4137,7 +3118,7 @@ let make_bitvector_cast_fns cast_name env quant_kids src_typ target_typ =
 
 (* TODO: bound vars *)
 let make_bitvector_env_casts env quant_kids (kid,i) exp =
-  let mk_cast var typ exp = (fst (make_bitvector_cast_fns "bitvector_cast_in" env quant_kids typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in
+  let mk_cast var typ exp = (fst (make_bitvector_cast_fns "bitvector_cast_in" env quant_kids typ (subst_kids_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in
   let locals = Env.get_locals env in
   Bindings.fold (fun var (mut,typ) exp ->
     if mut = Immutable then mk_cast var typ exp else exp) locals exp
@@ -4209,7 +3190,7 @@ let fill_in_type env typ =
        (match solve_unique env (nvar kid) with
        | None -> subst
        | Some n -> KBindings.add kid (nconstant n) subst)) tyvars KBindings.empty in
-  subst_src_typ subst typ
+  subst_kids_typ subst typ
 
 (* TODO: top-level patterns *)
 (* TODO: proper environment tracking for variables.  Currently we pretend that
@@ -4280,7 +3261,7 @@ let add_bitvector_casts (Defs defs) =
            make_bitvector_env_casts env quant_kids inst body) e2 insts in
          let insts = List.fold_left (fun insts (kid,i) ->
            KBindings.add kid (nconstant i) insts) KBindings.empty insts in
-         let src_typ = subst_src_typ insts result_typ in
+         let src_typ = subst_kids_typ insts result_typ in
          let e2' = make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ e2' in
          E_aux (E_if (e1,e2',e3), ann)
       | E_return e' ->
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 89f64401..edf0d4a5 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -52,7 +52,6 @@ module Big_int = Nat_big_num
 open Ast
 open Ast_util
 open Type_check
-open Spec_analysis
 
 type 'a rewriters = {
     rewrite_exp  : 'a rewriters -> 'a exp -> 'a exp;
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index e26ea8a2..80bff0dd 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -662,3 +662,212 @@ let top_sort_defs (Defs defs) =
     List.fold_left add_def_to_graph ([], [], Namemap.empty, Namemap.empty) defs in
   let components = scc ~original_order:original_order graph in
   Defs (prelude @ List.concat (List.map (def_of_component graph defset) components))
+
+
+(* Functions for finding the set of variables assigned to.  Used in constant propagation
+   and monomorphisation. *)
+
+
+let assigned_vars exp =
+  fst (Rewriter.fold_exp
+         { (Rewriter.compute_exp_alg IdSet.empty IdSet.union) with
+           Rewriter.lEXP_id = (fun id -> IdSet.singleton id, LEXP_id id);
+           Rewriter.lEXP_cast = (fun (ty,id) -> IdSet.singleton id, LEXP_cast (ty,id)) }
+         exp)
+
+let assigned_vars_in_fexps fes =
+  List.fold_left
+    (fun vs (FE_aux (FE_Fexp (_,e),_)) -> IdSet.union vs (assigned_vars e))
+    IdSet.empty
+    fes
+
+let assigned_vars_in_pexp (Pat_aux (p,_)) =
+  match p with
+  | Pat_exp (_,e) -> assigned_vars e
+  | Pat_when (p,e1,e2) -> IdSet.union (assigned_vars e1) (assigned_vars e2)
+
+let rec assigned_vars_in_lexp (LEXP_aux (le,_)) =
+  match le with
+  | LEXP_id id
+  | LEXP_cast (_,id) -> IdSet.singleton id
+  | LEXP_tup lexps
+  | LEXP_vector_concat lexps -> 
+     List.fold_left (fun vs le -> IdSet.union vs (assigned_vars_in_lexp le)) IdSet.empty lexps
+  | LEXP_memory (_,es) -> List.fold_left (fun vs e -> IdSet.union vs (assigned_vars e)) IdSet.empty es
+  | LEXP_vector (le,e) -> IdSet.union (assigned_vars_in_lexp le) (assigned_vars e)
+  | LEXP_vector_range (le,e1,e2) ->
+     IdSet.union (assigned_vars_in_lexp le) (IdSet.union (assigned_vars e1) (assigned_vars e2))
+  | LEXP_field (le,_) -> assigned_vars_in_lexp le
+  | LEXP_deref e -> assigned_vars e
+
+
+let pat_id_is_variable env id =
+  match Type_check.Env.lookup_id id env with
+  (* Unbound is returned for both variables and constructors which take
+     arguments, but the latter only don't appear in a P_id *)
+  | Unbound
+  (* Shadowing of immutable locals is allowed; mutable locals and registers
+     are rejected by the type checker, so don't matter *)
+  | Local _
+  | Register _
+    -> true
+  | Enum _ -> false
+
+let bindings_from_pat p =
+  let rec aux_pat (P_aux (p,(l,annot))) =
+    let env = Type_check.env_of_annot (l, annot) in
+    match p with
+    | P_lit _
+    | P_wild
+      -> []
+    | P_or (p1, p2) -> aux_pat p1 @ aux_pat p2
+    | P_not (p) -> aux_pat p
+    | P_as (p,id) -> id::(aux_pat p)
+    | P_typ (_,p) -> aux_pat p
+    | P_id id ->
+       if pat_id_is_variable env id then [id] else []
+    | P_var (p,kid) -> aux_pat p
+    | P_vector ps
+    | P_vector_concat ps
+    | P_string_append ps
+    | P_app (_,ps)
+    | P_tup ps
+    | P_list ps
+      -> List.concat (List.map aux_pat ps)
+    | P_record (fps,_) -> List.concat (List.map aux_fpat fps)
+    | P_cons (p1,p2) -> aux_pat p1 @ aux_pat p2
+  and aux_fpat (FP_aux (FP_Fpat (_,p), _)) = aux_pat p
+  in aux_pat p
+
+
+(* TODO: replace the below with solutions that don't depend so much on the
+   structure of the environment. *)
+
+let rec flatten_constraints = function
+  | [] -> []
+  | (NC_aux (NC_and (nc1,nc2),_))::t -> flatten_constraints (nc1::nc2::t)
+  | h::t -> h::(flatten_constraints t)
+
+(* NB: this only looks for direct equalities with the given kid.  It would be
+   better in principle to find the entire set of equal kids, but it isn't
+   necessary to deal with the fresh kids produced by the type checker while
+   checking P_var patterns, so we don't do it for now. *)
+let equal_kids_ncs kid ncs =
+  let is_eq = function
+    | NC_aux (NC_equal (Nexp_aux (Nexp_var var1,_), Nexp_aux (Nexp_var var2,_)),_) ->
+       if Kid.compare kid var1 == 0 then Some var2 else
+         if Kid.compare kid var2 == 0 then Some var1 else
+           None
+    | _ -> None
+  in
+  let kids = Util.map_filter is_eq ncs in
+  List.fold_left (fun s k -> KidSet.add k s) (KidSet.singleton kid) kids
+
+let equal_kids env kid =
+  let ncs = flatten_constraints (Type_check.Env.get_constraints env) in
+  equal_kids_ncs kid ncs
+
+
+
+(* TODO: kid shadowing *)
+let nexp_subst_fns substs =
+  let s_t t = subst_kids_typ substs t in
+(*  let s_typschm (TypSchm_aux (TypSchm_ts (q,t),l)) = TypSchm_aux (TypSchm_ts (q,s_t t),l) in
+   hopefully don't need this anyway *)(*
+  let s_typschm tsh = tsh in*)
+  let s_tannot tannot =
+    match Type_check.destruct_tannot tannot with
+    | None -> Type_check.empty_tannot
+    | Some (env,t,eff) -> Type_check.mk_tannot env (s_t t) eff (* TODO: what about env? *)
+  in
+  let rec s_pat (P_aux (p,(l,annot))) =
+    let re p = P_aux (p,(l,s_tannot annot)) in
+    match p with
+    | P_lit _ | P_wild | P_id _ -> re p
+    | P_or (p1, p2) -> re (P_or (s_pat p1, s_pat p2))
+    | P_not (p) -> re (P_not (s_pat p))
+    | P_var (p',tpat) -> re (P_var (s_pat p',tpat))
+    | P_as (p',id) -> re (P_as (s_pat p', id))
+    | P_typ (ty,p') -> re (P_typ (s_t ty,s_pat p'))
+    | P_app (id,ps) -> re (P_app (id, List.map s_pat ps))
+    | P_record (fps,flag) -> re (P_record (List.map s_fpat fps, flag))
+    | P_vector ps -> re (P_vector (List.map s_pat ps))
+    | P_vector_concat ps -> re (P_vector_concat (List.map s_pat ps))
+    | P_string_append ps -> re (P_string_append (List.map s_pat ps))
+    | P_tup ps -> re (P_tup (List.map s_pat ps))
+    | P_list ps -> re (P_list (List.map s_pat ps))
+    | P_cons (p1,p2) -> re (P_cons (s_pat p1, s_pat p2))
+  and s_fpat (FP_aux (FP_Fpat (id, p), (l,annot))) =
+    FP_aux (FP_Fpat (id, s_pat p), (l,s_tannot annot))
+  in
+  let rec s_exp (E_aux (e,(l,annot))) =
+    let re e = E_aux (e,(l,s_tannot annot)) in
+      match e with
+      | E_block es -> re (E_block (List.map s_exp es))
+      | E_nondet es -> re (E_nondet (List.map s_exp es))
+      | E_id _
+      | E_ref _
+      | E_lit _
+      | E_internal_value _
+        -> re e
+      | E_sizeof ne -> begin
+         let ne' = subst_kids_nexp substs ne in
+         match ne' with
+         | Nexp_aux (Nexp_constant i,l) -> re (E_lit (L_aux (L_num i,l)))
+         | _ -> re (E_sizeof ne')
+      end
+      | E_constraint nc -> re (E_constraint (subst_kids_nc substs nc))
+      | E_cast (t,e') -> re (E_cast (s_t t, s_exp e'))
+      | E_app (id,es) -> re (E_app (id, List.map s_exp es))
+      | E_app_infix (e1,id,e2) -> re (E_app_infix (s_exp e1,id,s_exp e2))
+      | E_tuple es -> re (E_tuple (List.map s_exp es))
+      | E_if (e1,e2,e3) -> re (E_if (s_exp e1, s_exp e2, s_exp e3))
+      | E_for (id,e1,e2,e3,ord,e4) -> re (E_for (id,s_exp e1,s_exp e2,s_exp e3,ord,s_exp e4))
+      | E_loop (loop,e1,e2) -> re (E_loop (loop,s_exp e1,s_exp e2))
+      | E_vector es -> re (E_vector (List.map s_exp es))
+      | E_vector_access (e1,e2) -> re (E_vector_access (s_exp e1,s_exp e2))
+      | E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (s_exp e1,s_exp e2,s_exp e3))
+      | E_vector_update (e1,e2,e3) -> re (E_vector_update (s_exp e1,s_exp e2,s_exp e3))
+      | E_vector_update_subrange (e1,e2,e3,e4) -> re (E_vector_update_subrange (s_exp e1,s_exp e2,s_exp e3,s_exp e4))
+      | E_vector_append (e1,e2) -> re (E_vector_append (s_exp e1,s_exp e2))
+      | E_list es -> re (E_list (List.map s_exp es))
+      | E_cons (e1,e2) -> re (E_cons (s_exp e1,s_exp e2))
+      | E_record fes -> re (E_record (List.map s_fexp fes))
+      | E_record_update (e,fes) -> re (E_record_update (s_exp e, List.map s_fexp fes))
+      | E_field (e,id) -> re (E_field (s_exp e,id))
+      | E_case (e,cases) -> re (E_case (s_exp e, List.map s_pexp cases))
+      | E_let (lb,e) -> re (E_let (s_letbind lb, s_exp e))
+      | E_assign (le,e) -> re (E_assign (s_lexp le, s_exp e))
+      | E_exit e -> re (E_exit (s_exp e))
+      | E_return e -> re (E_return (s_exp e))
+      | E_assert (e1,e2) -> re (E_assert (s_exp e1,s_exp e2))
+      | E_var (le,e1,e2) -> re (E_var (s_lexp le, s_exp e1, s_exp e2))
+      | E_internal_plet (p,e1,e2) -> re (E_internal_plet (s_pat p, s_exp e1, s_exp e2))
+      | E_internal_return e -> re (E_internal_return (s_exp e))
+      | E_throw e -> re (E_throw (s_exp e))
+      | E_try (e,cases) -> re (E_try (s_exp e, List.map s_pexp cases))
+    and s_fexp (FE_aux (FE_Fexp (id,e), (l,annot))) =
+      FE_aux (FE_Fexp (id,s_exp e),(l,s_tannot annot))
+    and s_pexp = function
+      | (Pat_aux (Pat_exp (p,e),(l,annot))) ->
+         Pat_aux (Pat_exp (s_pat p, s_exp e),(l,s_tannot annot))
+      | (Pat_aux (Pat_when (p,e1,e2),(l,annot))) ->
+         Pat_aux (Pat_when (s_pat p, s_exp e1, s_exp e2),(l,s_tannot annot))
+    and s_letbind (LB_aux (lb,(l,annot))) =
+      match lb with
+      | LB_val (p,e) -> LB_aux (LB_val (s_pat p,s_exp e), (l,s_tannot annot))
+    and s_lexp (LEXP_aux (e,(l,annot))) =
+      let re e = LEXP_aux (e,(l,s_tannot annot)) in
+      match e with
+      | LEXP_id _ -> re e
+      | LEXP_cast (typ,id) -> re (LEXP_cast (s_t typ, id))
+      | LEXP_memory (id,es) -> re (LEXP_memory (id,List.map s_exp es))
+      | LEXP_tup les -> re (LEXP_tup (List.map s_lexp les))
+      | LEXP_vector (le,e) -> re (LEXP_vector (s_lexp le, s_exp e))
+      | LEXP_vector_range (le,e1,e2) -> re (LEXP_vector_range (s_lexp le, s_exp e1, s_exp e2))
+      | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map s_lexp les))
+      | LEXP_field (le,id) -> re (LEXP_field (s_lexp le, id))
+      | LEXP_deref e -> re (LEXP_deref (s_exp e))
+  in (s_pat,s_exp)
+let nexp_subst_pat substs = fst (nexp_subst_fns substs)
+let nexp_subst_exp substs = snd (nexp_subst_fns substs)
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli
index f13dd596..8586ac15 100644
--- a/src/spec_analysis.mli
+++ b/src/spec_analysis.mli
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_util
 open Util
 open Type_check
 
@@ -76,3 +77,21 @@ val is_within_machine64 : typ -> nexp_range list -> triple *)
 (* val restrict_defs : 'a defs -> string list -> 'a defs *)
 
 val top_sort_defs : tannot defs -> tannot defs
+
+(** Return the set of mutable variables assigned to in the given AST. *)
+val assigned_vars : 'a exp -> IdSet.t
+val assigned_vars_in_fexps : 'a fexp list -> IdSet.t
+val assigned_vars_in_pexp : 'a pexp -> IdSet.t
+val assigned_vars_in_lexp : 'a lexp -> IdSet.t
+
+(** Variable bindings in patterns *)
+val pat_id_is_variable : env -> id -> bool
+val bindings_from_pat : tannot pat -> id list
+
+val equal_kids_ncs : kid -> n_constraint list -> KidSet.t
+val equal_kids : env -> kid -> KidSet.t
+
+(** Type-level substitutions into patterns and expressions.  Also attempts to
+    update type annotations, but not the associated environments. *)
+val nexp_subst_pat : nexp KBindings.t -> tannot pat -> tannot pat
+val nexp_subst_exp : nexp KBindings.t -> tannot exp -> tannot exp