reduce number of unknown identifiers and get one step closer to actually decoding an ARM instruction.

(Note: may fix issue #2, haven't checked yet)

4 files changed, 150 insertions, 119 deletions

diff --git a/src/rewriter.ml b/src/rewriter.ml
index 4fad78e7..9e28f6f5 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -6,59 +6,61 @@ type 'a exp = 'a Ast.exp
 type 'a emap = 'a Envmap.t
 type envs = Type_check.envs
 
-let rec partial_assoc (v: 'a) (ls : ('a *'b) list ) : 'b option  = match ls with
+let rec partial_assoc (eq: 'a -> 'a -> bool) (v: 'a) (ls : ('a *'b) list ) : 'b option  = match ls with
   | [] -> None
-  | (v1,v2)::ls -> if v1 = v then Some v2 else partial_assoc v ls
+  | (v1,v2)::ls -> if (eq v1 v) then Some v2 else partial_assoc eq v ls
 
 let mk_atom_typ i = {t=Tapp("atom",[TA_nexp i])}
 
 let rec rewrite_nexp_to_exp program_vars l nexp = 
   let rewrite n = rewrite_nexp_to_exp program_vars l n in
   let typ = mk_atom_typ nexp in
-  match nexp.nexp with
-    | Nconst i -> E_aux (E_lit (L_aux (L_num (int_of_big_int i),l)), (l,simple_annot typ))
-    | Nadd (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "+",l)),rewrite n2),
-			     (l, (tag_annot typ (External (Some "add")))))
-    | Nmult (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "*",l)),rewrite n2),
-			      (l, tag_annot typ (External (Some "multiply"))))
-    | Nsub (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "-",l)),rewrite n2),
-			     (l, tag_annot typ (External (Some "minus"))))
-    | N2n (n, _) -> E_aux (E_app_infix (E_aux (E_lit (L_aux (L_num 2,l)), (l, simple_annot (mk_atom_typ n_two))),
-					(Id_aux (Id "**",l)),
-					rewrite n), (l, tag_annot typ (External (Some "power"))))
-    | Npow(n,i) -> E_aux (E_app_infix 
-			    (rewrite n, (Id_aux (Id "**",l)),
-			     E_aux (E_lit (L_aux (L_num i,l)),
-				    (l, simple_annot (mk_atom_typ {nexp = Nconst (big_int_of_int i)})))),
-			  (l, tag_annot typ (External (Some "power"))))
-    | Nneg(n) -> E_aux (E_app_infix (E_aux (E_lit (L_aux (L_num 0,l)), (l, simple_annot (mk_atom_typ n_zero))),
-				     (Id_aux (Id "-",l)),
-				     rewrite n),
-			(l, tag_annot typ (External (Some "minus"))))
-    | Nvar v -> 
-      match program_vars with
-	| None -> assert false
-	| Some program_vars ->
-	  (match partial_assoc v program_vars with
-	    | None ->
-	      (*TODO these need to generate an error as it's a place where there's insufficient specification. 
-		But, for now I need to permit this to make power.sail compile, and most errors are in trap 
-		or vectors *)
-	      (*let _ = Printf.printf "unbound variable here %s\n" v in *)
-	      E_aux (E_id (Id_aux (Id v,l)),(l,simple_annot typ))
-	    | Some(None,ev) ->
-	      (*let _ = Printf.printf "var case of nvar rewrite, %s\n" ev in*)
-	      E_aux (E_id (Id_aux (Id ev,l)), (l, simple_annot typ))
-	    | Some(Some f,ev) -> 
-	      E_aux (E_app ((Id_aux (Id f,l)), [ (E_aux (E_id (Id_aux (Id ev,l)), (l,simple_annot typ)))]),
-		     (l, tag_annot typ (External (Some f)))))
+  let actual_rewrite_n nexp = 
+    match nexp.nexp with
+      | Nconst i -> E_aux (E_lit (L_aux (L_num (int_of_big_int i),l)), (l,simple_annot typ))
+      | Nadd (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "+",l)),rewrite n2),
+			       (l, (tag_annot typ (External (Some "add")))))
+      | Nmult (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "*",l)),rewrite n2),
+				(l, tag_annot typ (External (Some "multiply"))))
+      | Nsub (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "-",l)),rewrite n2),
+			       (l, tag_annot typ (External (Some "minus"))))
+      | N2n (n, _) -> E_aux (E_app_infix (E_aux (E_lit (L_aux (L_num 2,l)), (l, simple_annot (mk_atom_typ n_two))),
+					  (Id_aux (Id "**",l)),
+					  rewrite n), (l, tag_annot typ (External (Some "power"))))
+      | Npow(n,i) -> E_aux (E_app_infix 
+			      (rewrite n, (Id_aux (Id "**",l)),
+			       E_aux (E_lit (L_aux (L_num i,l)),
+				      (l, simple_annot (mk_atom_typ {nexp = Nconst (big_int_of_int i)})))),
+			    (l, tag_annot typ (External (Some "power"))))
+      | Nneg(n) -> E_aux (E_app_infix (E_aux (E_lit (L_aux (L_num 0,l)), (l, simple_annot (mk_atom_typ n_zero))),
+				       (Id_aux (Id "-",l)),
+				       rewrite n),
+			  (l, tag_annot typ (External (Some "minus"))))
+      | Nvar v -> (*TODO these need to generate an error as it's a place where there's insufficient specification. 
+		    But, for now I need to permit this to make power.sail compile, and most errors are in trap 
+		    or vectors *)
+	      (*let _ = Printf.eprintf "unbound variable here %s\n" v in *)
+	E_aux (E_id (Id_aux (Id v,l)),(l,simple_annot typ)) in
+  match program_vars with
+    | None -> actual_rewrite_n nexp
+    | Some program_vars ->
+      (match partial_assoc nexp_eq_check nexp program_vars with
+	| None -> actual_rewrite_n nexp
+	| Some(None,ev) ->
+	  (*let _ = Printf.eprintf "var case of rewrite, %s\n" ev in*)
+	  E_aux (E_id (Id_aux (Id ev,l)), (l, simple_annot typ))
+	| Some(Some f,ev) -> 
+	  E_aux (E_app ((Id_aux (Id f,l)), [ (E_aux (E_id (Id_aux (Id ev,l)), (l,simple_annot typ)))]),
+		 (l, tag_annot typ (External (Some f)))))
 
-let rec match_to_program_vars vs bounds =
-  match vs with
+let rec match_to_program_vars ns bounds =
+  match ns with
     | [] -> []
-    | v::vs -> match find_var_from_nvar v bounds with
-	| None -> match_to_program_vars vs bounds
-	| Some(augment,ev) -> (v,(augment,ev))::(match_to_program_vars vs bounds)
+    | n::ns -> match find_var_from_nexp n bounds with
+	| None -> match_to_program_vars ns bounds
+	| Some(augment,ev) -> 
+	  (*let _ = Printf.eprintf "adding n %s to program var %s\n" (n_to_string n) ev in*)
+	  (n,(augment,ev))::(match_to_program_vars ns bounds)
 
 let rec rewrite_exp (E_aux (exp,(l,annot))) = 
   let rewrap e = E_aux (e,(l,annot)) in
@@ -128,34 +130,36 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) =
 		| _ -> new_exp)
 	    | _ -> new_exp))
     | E_internal_exp (l,impl) ->
-      (*let _ = Printf.printf "Rewriting internal expression\n" in*) 
       (match impl with
 	| Base((_,t),_,_,_,bounds) ->
+	  (*let _ = Printf.eprintf "Rewriting internal expression, with type %s\n" (t_to_string t) in *)
 	  match t.t with
 	    (*Old case; should possibly be removed*)
 	    | Tapp("register",[TA_typ {t= Tapp("vector",[ _; TA_nexp r;_;_])}])
 	    | Tapp("vector", [_;TA_nexp r;_;_]) ->
-	      let vars = get_all_nvar r in
-	      (match vars with
+	      (*let _ = Printf.eprintf "vector case with %s, bounds are %s\n" (n_to_string r) (bounds_to_string bounds) in*)
+	      let nexps = expand_nexp r in
+	      (match (match_to_program_vars nexps bounds) with
 		| [] -> rewrite_nexp_to_exp None l r
-		| vars -> rewrite_nexp_to_exp (Some (match_to_program_vars vars bounds)) l r)
+		| map -> rewrite_nexp_to_exp (Some map) l r)
 	    | Tapp("implicit", [TA_nexp i]) ->
-	      (*let _ = Printf.printf "Implicit case with %s\n" (n_to_string i) in*)
-	      let vars = get_all_nvar i in
-	      (match vars with
+	      (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*)
+	      let nexps = expand_nexp i in
+	      (match (match_to_program_vars nexps bounds) with
 		| [] -> rewrite_nexp_to_exp None l i
-		| vars -> rewrite_nexp_to_exp (Some (match_to_program_vars vars bounds)) l i))
+		| map -> rewrite_nexp_to_exp (Some map) l i))
     | E_internal_exp_user ((l,user_spec),(_,impl)) -> 
       (match (user_spec,impl) with
 	| (Base((_,tu),_,_,_,_), Base((_,ti),_,_,_,bounds)) ->
 	  (*let _ = Printf.eprintf "E_interal_user getting rewritten two types are %s and %s\n" (t_to_string tu) (t_to_string ti) in*)
 	  match (tu.t,ti.t) with
 	    | (Tapp("implicit", [TA_nexp u]),Tapp("implicit",[TA_nexp i])) ->
-	      let vars = get_all_nvar i in
-	      (match vars with
+	      (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*)
+	      let nexps = expand_nexp i in
+	      (match (match_to_program_vars nexps bounds) with
 		| [] -> rewrite_nexp_to_exp None l i
 		  (*add u to program_vars env; for now it will work out properly by accident*)
-		| vars -> rewrite_nexp_to_exp (Some (match_to_program_vars vars bounds)) l i))
+		| map -> rewrite_nexp_to_exp (Some map) l i))
 
 and rewrite_let (LB_aux(letbind,(l,annot))) = match letbind with
   | LB_val_explicit (typschm, pat,exp) ->
@@ -175,7 +179,7 @@ and rewrite_lexp (LEXP_aux(lexp,(l,annot))) =
 
 let rewrite_fun (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,annot))) = 
   let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),(l,annot))) = 
-    (*let _ = Printf.printf "Rewriting function %s\n" (match id with (Id_aux (Id i,_)) -> i) in*)
+    (*let _ = Printf.eprintf "Rewriting function %s\n" (match id with (Id_aux (Id i,_)) -> i) in*)
     (FCL_aux (FCL_Funcl (id,pat,rewrite_exp exp),(l,annot))) 
   in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,annot))
 
diff --git a/src/type_check.ml b/src/type_check.ml
index e76f40be..a4466acb 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -470,7 +470,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	let t,cs,ef,_ = subst params false t cs ef in
         (match t.t with
         | Tfn({t = Tid "unit"},t',IP_none,ef) -> 
-          let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false t' 
+          let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false b_env t' 
 	    (rebuild (Base(([],{t=Tfn(unit_t,t',IP_none,ef)}),Constructor,cs,ef,bounds))) expect_t in
           (e',t',t_env,cs@cs',nob,union_effects ef ef')
         | Tfn(t1,t',IP_none,e) -> 
@@ -479,7 +479,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       | Some(Base((params,t),(Enum max),cs,ef,bounds)) ->
         let t',cs,_,_ = subst params false t cs ef in
         let t',cs',ef',e' = 
-	  type_coerce (Expr l) d_env Require false false t' (rebuild (cons_tag_annot t' (Enum max) cs)) expect_t in
+	  type_coerce (Expr l) d_env Require false false b_env t' (rebuild (cons_tag_annot t' (Enum max) cs)) expect_t in
         (e',t',t_env,cs@cs',nob,ef')
       | Some(Base(tp,Default,cs,ef,_)) | Some(Base(tp,Spec,cs,ef,_)) ->
         typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use")
@@ -506,20 +506,20 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
         | Tapp("register",[TA_typ(t')]),Tuvar _ ->
 	  let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
           let tannot = Base(([],t),(if is_alias then Alias else External (Some i)),cs,ef',bounds) in
-          let t',cs',_,e' = type_coerce (Expr l) d_env Require false false t' (rebuild tannot) expect_actual in
+          let t',cs',_,e' = type_coerce (Expr l) d_env Require false false b_env t' (rebuild tannot) expect_actual in
           (e',t,t_env,cs@cs',bounds,ef')
         | Tapp("register",[TA_typ(t')]),_ ->
 	  let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
           let tannot = Base(([],t),(if is_alias then Alias else External (Some i)),cs,ef',bounds) in
-          let t',cs',_,e' = type_coerce (Expr l) d_env Require false false t' (rebuild tannot) expect_actual in
+          let t',cs',_,e' = type_coerce (Expr l) d_env Require false false b_env t' (rebuild tannot) expect_actual in
           (e',t',t_env,cs@cs',bounds,ef')
         | Tapp("reg",[TA_typ(t')]),_ ->
           let tannot = cons_bs_annot t cs bounds in
-          let t',cs',_,e' = type_coerce (Expr l) d_env Require false false t' (rebuild tannot) expect_actual in
+          let t',cs',_,e' = type_coerce (Expr l) d_env Require false false b_env t' (rebuild tannot) expect_actual in
           (e',t',t_env,cs@cs',bounds,pure_e)
         | _ -> 
           let t',cs',ef',e' = 
-	    type_coerce (Expr l) d_env Require false false t (rebuild (Base(([],t),tag,cs,pure_e,bounds))) expect_t in
+	    type_coerce (Expr l) d_env Require false false b_env t (rebuild (Base(([],t),tag,cs,pure_e,bounds))) expect_t in
           (e',t',t_env,cs@cs',bounds,union_effects ef ef')
         )
       | Some NoTyp | Some Overload _ | None -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is unbound"))
@@ -552,6 +552,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
             let t = {t=Tapp("atom", [TA_nexp n;])} in
             let cs = [LtEq(Expr l,Guarantee,n,mk_sub {nexp = N2n(rise,None)} n_one)] in
             let f = match o.order with | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec" | _ -> "to_vec_inc" in
+	    (*let _ = Printf.eprintf "adding a call to to_vec_*: bounds are %s\n" (bounds_to_string b_env) in*)
 	    let internal_tannot = (l,(cons_bs_annot {t = Tapp("implicit",[TA_nexp rise])} [] b_env)) in
 	    let tannot = (l,cons_tag_annot expect_t (External (Some f)) cs) in
             E_aux(E_app((Id_aux((Id f),l)),
@@ -573,11 +574,11 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	    | Tapp ("register",[TA_typ {t=Tapp ("vector",[TA_nexp base;TA_nexp {nexp=Nconst rise};
 							  TA_ord o;(TA_typ {t=Tid "bit"})])}])->
               let f = match o.order with | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec" | _ -> "to_vec_inc" (*Change to follow a default?*) in
-	      let tannot = (l,Base(([],expect_t),External (Some f),[],ef,nob)) in
+	      let tannot = (l,Base(([],expect_t),External (Some f),[],ef,b_env)) in
               E_aux(E_app((Id_aux((Id f),l)),
 			  [(E_aux (E_internal_exp(tannot), tannot));simp_exp e l bit_t]),tannot),[],ef
             | _ -> simp_exp e l (new_t ()),[],ef)) in
-      let t',cs',_,e' = type_coerce (Expr l) d_env Require false true (get_e_typ e) e expect_t in
+      let t',cs',_,e' = type_coerce (Expr l) d_env Require false true b_env (get_e_typ e) e expect_t in
       (e',t',t_env,cs@cs',nob,effect)
     | E_cast(typ,e) ->
       let cast_t = typ_to_t false false typ in
@@ -586,9 +587,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let ct = {t = Toptions(cast_t,None)} in
       let (e',u,t_env,cs,bounds,ef) = check_exp envs imp_param ct e in
       (*let _ = Printf.eprintf "Type checking cast: cast_t is %s constraints after checking e are %s\n" (t_to_string cast_t) (constraints_to_string cs) in*)
-      let t',cs2,ef',e' = type_coerce (Expr l) d_env Require true false u e' cast_t in
+      let t',cs2,ef',e' = type_coerce (Expr l) d_env Require true false b_env u e' cast_t in
       (*let _ = Printf.eprintf "Type checking cast: after first coerce with u at %s, and final t' %s is and constraints are %s\n" (t_to_string u) (t_to_string t') (constraints_to_string cs2) in*)
-      let t',cs3,ef'',e'' = type_coerce (Expr l) d_env Guarantee false false cast_t e' expect_t in 
+      let t',cs3,ef'',e'' = type_coerce (Expr l) d_env Guarantee false false b_env cast_t e' expect_t in 
       (*let _ = Printf.eprintf "Type checking cast: after second coerce expect_t is %s, t' %s is and constraints are %s\n" (t_to_string expect_t) (t_to_string t') (constraints_to_string cs3) in*)
       (e'',t',t_env,cs_a@cs@cs2@cs3,bounds,union_effects ef' (union_effects ef'' ef))
     | E_app(id,parms) -> 
@@ -606,9 +607,11 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	(match parms with
 	| [] | [(E_aux (E_lit (L_aux(L_unit, _)), _))] -> [],pure_e,[]
 	| [parm] -> 
-	  let _,cs,ef,parm' = type_coerce (Expr l) d_env Guarantee false false arg_t parm expect_arg_t in [parm'],ef,cs
+	  let _,cs,ef,parm' = 
+	    type_coerce (Expr l) d_env Guarantee false false b_env arg_t parm expect_arg_t in [parm'],ef,cs
 	| parms ->
-          (match type_coerce (Expr l) d_env Guarantee false false arg_t (E_aux (E_tuple parms,(l,NoTyp))) expect_arg_t
+          (match 
+	   type_coerce (Expr l) d_env Guarantee false false b_env arg_t (E_aux (E_tuple parms,(l,NoTyp))) expect_arg_t
 	   with
           | (_,cs,ef,(E_aux(E_tuple parms',tannot'))) -> (parms',ef,cs)
           | _ -> raise (Reporting_basic.err_unreachable l "type coerce given tuple and tuple type returned non-tuple"))) 
@@ -621,7 +624,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	      let implicit = {t= Tapp("implicit",[TA_nexp n])} in
 	      let annot_i = Base(([],implicit),Emp_local,[],pure_e,b_env) in
 	      E_aux(E_internal_exp((l,annot_i)),(l,simple_annot nat_t)) in
-            type_coerce (Expr l) d_env Require false false ret 
+            type_coerce (Expr l) d_env Require false false b_env ret 
 	      (E_aux (E_app(id, internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t
 	  | (IP_length n ,Some ne) | (IP_user n,Some ne) | (IP_start n,Some ne) ->
 	    (*let _ = Printf.eprintf "implicit length or var required %s with imp_param %s\n" (n_to_string n) (n_to_string ne) in
@@ -633,11 +636,11 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	      let annot_i = Base(([],implicit),Emp_local,[],pure_e,b_env) in
 	      E_aux (E_internal_exp_user((l, annot_iu),(l,annot_i)), (l,simple_annot nat_t))
 	    in
-	    type_coerce (Expr l) d_env Require false false ret 
+	    type_coerce (Expr l) d_env Require false false b_env ret 
 	      (E_aux (E_app(id,internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t
           | (IP_none,_) -> 
 	    (*let _ = Printf.printf "no implicit length or var required\n" in*)
-            type_coerce (Expr l) d_env Require false false ret 
+            type_coerce (Expr l) d_env Require false false b_env ret 
 	      (E_aux (E_app(id, parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t
       in
       (match Envmap.apply t_env i with
@@ -711,7 +714,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
               | _ -> typ_error l (i ^ " expected either the return type or the expected type to be a vector") in
             type_coerce (Expr l) d_env false false ret (E_aux (E_app(op, [internal_exp;lft;rht]),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t*)
           | IP_none -> 
-            type_coerce (Expr l) d_env Require false false ret 
+            type_coerce (Expr l) d_env Require false false b_env ret 
 	      (E_aux (E_app_infix(lft,op,rht),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t 
       in
       (match Envmap.apply t_env i with
@@ -799,7 +802,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	    exps ([],[],[],pure_e) in
         let t = { t=Ttup typs } in
         let t',cs',ef',e' = 
-	  type_coerce (Expr l) d_env Guarantee false false t (E_aux(E_tuple(exps),(l,simple_annot t))) expect_t in
+	  type_coerce (Expr l) d_env Guarantee false false b_env
+	    t (E_aux(E_tuple(exps),(l,simple_annot t))) expect_t in
         (e',t',t_env,consts@cs',nob,union_effects ef' effect))
     | E_if(cond,then_,else_) ->
       let (cond',_,_,c1,_,ef1) = check_exp envs imp_param bit_t cond in
@@ -865,7 +869,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
           {t = Tapp("vector",[TA_nexp {nexp=Nconst (big_int_of_int (len-1))};
                               TA_nexp {nexp=Nconst (big_int_of_int len)};
                               TA_ord {order= Odec}; TA_typ item_t])} in
-      let t',cs',ef',e' = type_coerce (Expr l) d_env Guarantee false false t 
+      let t',cs',ef',e' = type_coerce (Expr l) d_env Guarantee false false b_env t 
 	(E_aux(E_vector es,(l,simple_annot t))) expect_t in
       (e',t',t_env,cs@cs',nob,union_effects effect ef')
     | E_vector_indexed(eis,(Def_val_aux(default,(ld,annot)))) ->
@@ -905,7 +909,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let t = {t = Tapp("vector",
 			[TA_nexp(base_bound);TA_nexp length_bound;
 			 TA_ord({order= if is_increasing then Oinc else Odec});TA_typ item_t])} in
-      let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false t 
+      let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false b_env t 
 	                          (E_aux (E_vector_indexed(es,default'),(l,simple_annot t))) expect_t in
       (e',t',t_env,cs@cs_d@cs_bounds@cs',nob,union_effects ef_d (union_effects ef' effect))
     | E_vector_access(vec,i) ->
@@ -936,7 +940,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	  | _ -> typ_error l "A vector must be either increasing or decreasing to access a single element"
       in 
       (*let _ = Printf.eprintf "Type checking vector access. item_t is %s and expect_t is %s\n" (t_to_string item_t) (t_to_string expect_t) in*)
-      let t',cs',ef',e'=type_coerce (Expr l) d_env Require false false item_t 
+      let t',cs',ef',e'=type_coerce (Expr l) d_env Require false false b_env item_t 
 	(E_aux(E_vector_access(vec',i'),(l,simple_annot item_t))) expect_t in
       (e',t',t_env,cs_loc@cs_i@cs@cs',nob,union_effects ef (union_effects ef' ef_i))
     | E_vector_subrange(vec,i1,i2) ->
@@ -994,7 +998,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	  | _ -> typ_error l "A vector must be either increasing or decreasing to access a slice" in
       let nt = {t=Tapp("vector",[TA_nexp new_base;TA_nexp new_rise; TA_ord ord;TA_typ item_t])} in
       let (t,cs3,ef3,e') = 
-	type_coerce (Expr l) d_env Require false false nt 
+	type_coerce (Expr l) d_env Require false false b_env nt 
 	  (E_aux(E_vector_subrange(vec',i1',i2'),(l,constrained_annot nt cs_loc))) expect_t in
       (e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc,nob,(union_effects ef (union_effects ef3 (union_effects ef_i1 ef_i2))))
     | E_vector_update(vec,i,e) ->
@@ -1022,7 +1026,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       in      
       let nt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise; TA_ord ord;TA_typ item_t])} in
       let (t,cs3,ef3,e') = 
-	type_coerce (Expr l) d_env Require false false nt 
+	type_coerce (Expr l) d_env Require false false b_env nt 
 	  (E_aux(E_vector_update(vec',i',e'),(l,constrained_annot nt cs_loc))) expect_t in
       (e',t,t_env,cs3@cs@cs_i@cs_e@cs_loc,nob,(union_effects ef (union_effects ef3 (union_effects ef_i ef_e))))
     | E_vector_update_subrange(vec,i1,i2,e) ->
@@ -1066,7 +1070,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	  | _ -> typ_error l "A vector must be either increasing or decreasing to modify a slice" in
       let nt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise; TA_ord ord;TA_typ item_t])} in
       let (t,cs3,ef3,e') = 
-       type_coerce (Expr l) d_env Require false false nt (E_aux(E_vector_update_subrange(vec',i1',i2',e'),(l,constrained_annot  nt cs_loc))) expect_t in
+       type_coerce (Expr l) d_env Require false false b_env nt (E_aux(E_vector_update_subrange(vec',i1',i2',e'),(l,constrained_annot  nt cs_loc))) expect_t in
       (e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc@cs_e,nob,(union_effects ef (union_effects ef3 (union_effects ef_i1 (union_effects ef_i2 ef_e)))))
     | E_vector_append(v1,v2) -> 
       let item_t,ord = match expect_t.t with
@@ -1084,7 +1088,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
         | Odec -> [GtEq((Expr l),Require,base1,mk_add rise1 rise2)]
         | _ -> [] in
       let (t,cs_c,ef_c,e') = 
-        type_coerce (Expr l) d_env Require false false ti 
+        type_coerce (Expr l) d_env Require false false b_env ti 
 	  (E_aux(E_vector_append(v1',v2'),(l,constrained_annot ti cs_loc))) expect_t in
       (e',t,t_env,cs_loc@cs_1@cs_2,nob,(union_effects ef_c (union_effects ef_1 ef_2)))
     | E_list(es) ->
@@ -1095,7 +1099,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	(List.fold_right (fun (e,_,_,c,_,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect) 
 	   (List.map (check_exp envs imp_param item_t) es) ([],[],pure_e)) in
       let t = {t = Tapp("list",[TA_typ item_t])} in
-      let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false t 
+      let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false b_env t 
 	(E_aux(E_list es,(l,simple_annot t))) expect_t in
       (e',t',t_env,cs@cs',nob,union_effects ef' effect)
     | E_cons(ls,i) ->
@@ -1106,7 +1110,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let (ls',t',_,cs,_,ef) = check_exp envs imp_param lt ls in
       let (i', ti, _,cs_i,_,ef_i) = check_exp envs imp_param item_t i in
       let (t',cs',ef',e') = 
-	type_coerce (Expr l) d_env Require false false lt (E_aux(E_cons(ls',i'),(l,simple_annot lt))) expect_t in
+	type_coerce (Expr l) d_env Require false false b_env lt (E_aux(E_cons(ls',i'),(l,simple_annot lt))) expect_t in
       (e',t',t_env,cs@cs'@cs_i,nob,union_effects ef' (union_effects ef ef_i))
     | E_record(FES_aux(FES_Fexps(fexps,_),l')) -> 
       let u,_ = get_abbrev d_env expect_t in
@@ -1217,7 +1221,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 		| Base((params,et),tag,cs,ef,bounds) ->
 		  let et,cs,ef,_ = subst params false et cs ef in
 		  let (et',c',ef',acc) = 
-		    type_coerce (Expr l) d_env Require false false et 
+		    type_coerce (Expr l) d_env Require false false b_env et 
 		      (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef,bounds)))) expect_t in
 		  (acc,et',t_env,cs@c'@c_sub,nob,union_effects ef' ef_sub)))
       | Tid i ->
@@ -1233,7 +1237,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 		| Base((params,et),tag,cs,ef,bounds) ->
 		  let et,cs,ef,_ = subst params false et cs ef in
 		  let (et',c',ef',acc) =
-		    type_coerce (Expr l) d_env Require false false et 
+		    type_coerce (Expr l) d_env Require false false b_env et 
 		      (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef,bounds)))) expect_t in
 		  (acc,et',t_env,cs@c'@c_sub,nob,union_effects ef' ef_sub)))
 	| Tuvar _ ->
@@ -1249,7 +1253,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 		| Base((params,et),tag,cs,ef,bounds) ->
 		  let et,cs,ef,_ = subst params false et cs ef in
 		  let (et',c',ef',acc) = 
-		    type_coerce (Expr l) d_env Guarantee false false et 
+		    type_coerce (Expr l) d_env Guarantee false false b_env et 
 		      (E_aux(E_field(e',id),
 			     (l,Base(([],et),tag,cs,ef,bounds)))) expect_t in
                   equate_t t' {t=Tid i};
@@ -1600,7 +1604,7 @@ and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) :
 	else (Base ((params,t),tag,cs,ef,bounds))
       in
       (*let _ = Printf.eprintf "done checking tannot in let1\n" in*)
-      (LB_aux (LB_val_explicit(typ,pat',e),(l,tannot)),env,cs,bounds,ef)
+      (LB_aux (LB_val_explicit(typ,pat',e),(l,tannot)),env,cs,merge_bounds b_env bounds,ef)
     | NoTyp | Overload _ -> raise (Reporting_basic.err_unreachable l "typschm_to_tannot failed to produce a Base"))
   | LB_val_implicit(pat,e) -> 
     let t = new_t () in
@@ -1610,10 +1614,10 @@ and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) :
     (*let _ = Printf.eprintf "checking tannot in let2\n" in*)
     let tannot = 
       if is_top_level then check_tannot l (Base(([],t'),emp_tag,cs,ef,bounds)) None cs ef (* see above *)
-      else (Base (([],t'),emp_tag,cs,ef,bounds))
+      else (Base (([],t'),emp_tag,cs,ef,merge_bounds bounds b_env))
     in
     (*let _ = Printf.eprintf "done checking tannot in let2\n" in*)
-    (LB_aux (LB_val_implicit(pat',e),(l,tannot)), env,cs,bounds,ef)
+    (LB_aux (LB_val_implicit(pat',e),(l,tannot)), env,cs,merge_bounds bounds b_env,ef)
 
 (*val check_type_def : envs -> (tannot type_def) -> (tannot type_def) envs_out*)
 let check_type_def envs (TD_aux(td,(l,annot))) =
diff --git a/src/type_internal.ml b/src/type_internal.ml
index a459c78e..a760c9d4 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -246,10 +246,21 @@ let rec constraint_to_string = function
     "BranchCons(" ^ co_to_string co ^ ", [" ^ constraints_to_string consts ^ "])"
 and constraints_to_string l = string_of_list "; " constraint_to_string l
 
+let variable_range_to_string v = match v with
+  | VR_eq (s,n) -> "vr_eq(" ^ s ^ ", " ^ n_to_string n ^ ")"
+  | VR_range (s,cs) -> "vr_range(" ^ s ^ ", " ^ constraints_to_string cs ^ ")"
+  | VR_vec_eq (s,n) -> "vr_vec_eq(" ^ s ^ ", " ^ n_to_string n ^ ")"
+  | VR_vec_r (s,cs) -> "vr_vec_r(" ^ s ^ ", "^ constraints_to_string cs ^ ")"
+  | VR_recheck (s,t) -> "vr_recheck(" ^ s ^ ", "^ t_to_string t ^ ")"
+
+let bounds_to_string b = match b with
+  | No_bounds -> "Nobounds"
+  | Bounds vs -> "Bounds(" ^ string_of_list "; " variable_range_to_string vs ^ ")"
+
 let rec tannot_to_string = function
   | NoTyp -> "No tannot"
   | Base((vars,t),tag,ncs,ef,bv) ->
-    "Tannot: type = " ^ (t_to_string t) ^ " tag = " ^ tag_to_string tag ^ " constraints = " ^ constraints_to_string ncs ^ " effect = " ^ e_to_string ef ^ "boundv = not printing"
+    "Tannot: type = " ^ (t_to_string t) ^ " tag = " ^ tag_to_string tag ^ " constraints = " ^ constraints_to_string ncs ^ " effect = " ^ e_to_string ef ^ "boundv = " ^ bounds_to_string bv
   | Overload(poly,_,variants) ->
     "Overloaded: poly = " ^ tannot_to_string poly
 
@@ -2050,22 +2061,30 @@ let find_bounds v bounds = match bounds with
       | b::bs -> if (get_vr_var b) = v then Some(b) else find_rec bs in
     find_rec bs
 
-let find_var_from_nvar v bounds = match bounds with
-  | No_bounds -> None
-  | Bounds bs ->
-    let rec find_rec bs = match bs with
-      | [] -> None
-      | b::bs -> (match b with
-	  | VR_eq(ev,n) ->
-	    (match n.nexp with 
-	      | Nvar nv -> if nv = v then Some (None,ev) else find_rec bs
-	      | _ -> find_rec bs)
-	  | VR_vec_eq (ev,n)->
-	    (match n.nexp with 
-	      | Nvar nv -> if nv = v then Some (Some "length",ev) else find_rec bs
-	      | _ -> find_rec bs)
-	  | _ -> find_rec bs) in
-    find_rec bs
+let rec expand_nexp n = match n.nexp with
+  | Nvar _ | Nconst _ | Nuvar _ | Npos_inf | Nneg_inf | Ninexact -> [n]
+  | Nadd (n1,n2) | Nsub (n1,n2) | Nmult (n1,n2) -> n::((expand_nexp n1)@(expand_nexp n2))
+  | N2n (n1,_) | Npow (n1,_) | Nneg n1 -> n::(expand_nexp n1)
+
+let is_nconst n = match n.nexp with | Nconst _ -> true | _ -> false
+
+let find_var_from_nexp n bounds = 
+  (*let _ = Printf.eprintf "finding %s in bounds\n" (n_to_string n) in*)
+  if is_nconst n then None 
+  else match bounds with
+    | No_bounds -> None
+    | Bounds bs ->
+      let rec find_rec bs = match bs with
+	| [] -> None
+	| b::bs -> (match b with
+	    | VR_eq(ev,n1) ->
+	      (*let _ = Printf.eprintf "checking if %s is eq to %s\n" (n_to_string n) (n_to_string n1) in*)
+	      if nexp_eq_check n1 n then Some (None,ev) else find_rec bs
+	    | VR_vec_eq (ev,n1)->
+	      (*let _ = Printf.eprintf "checking if %s is eq to %s\n" (n_to_string n) (n_to_string n1) in*)
+	      if nexp_eq_check n1 n then Some (Some "length",ev) else find_rec bs
+	    | _ -> find_rec bs) in
+      find_rec bs
 
 let merge_bounds b1 b2 =
   match b1,b2 with
@@ -2228,7 +2247,7 @@ and type_arg_eq co d_env enforce widen ta1 ta2 =
 and type_consistent co d_env enforce widen t1 t2 =
   type_consistent_internal co d_env enforce widen t1 [] t2 []
 
-let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2 = 
+let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e t2 cs2 = 
   let l = get_c_loc co in
   let t1,cs1' = get_abbrev d_env t1 in
   let t2,cs2' = get_abbrev d_env t2 in
@@ -2245,7 +2264,7 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2
 		     " nor " ^ (t_to_string to2) ^ " can match expected type " ^ (t_to_string t2))
   | Toptions(to1,None),_ -> 
     if is_explicit 
-    then type_coerce_internal co d_env enforce is_explicit widen to1 cs1 e t2 cs2
+    then type_coerce_internal co d_env enforce is_explicit widen bounds to1 cs1 e t2 cs2
     else (t2,csp,pure_e,e)
   | _,Toptions(to1,Some to2) -> 
     if (conforms_to_t d_env false true to1 t1_actual || conforms_to_t d_env false true to2 t1_actual)
@@ -2253,7 +2272,7 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2
     else eq_error l ((t_to_string t1) ^ " can match neither expexted type " ^ (t_to_string to1) ^ " nor " ^ (t_to_string to2))
   | _,Toptions(to1,None) -> 
     if is_explicit
-    then type_coerce_internal co d_env enforce is_explicit widen t1_actual cs1 e to1 cs2
+    then type_coerce_internal co d_env enforce is_explicit widen bounds t1_actual cs1 e to1 cs2
     else (t1,csp,pure_e,e)
   | Ttup t1s, Ttup t2s ->
     let tl1,tl2 = List.length t1s,List.length t2s in
@@ -2262,7 +2281,7 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2
       let vars = List.map2 (fun i t -> E_aux(E_id(i),(l,Base(([],t),Emp_local,[],pure_e,nob)))) ids t1s in
       let (coerced_ts,cs,efs,coerced_vars,any_coerced) = 
         List.fold_right2 (fun v (t1,t2) (ts,cs,efs,es,coerced) ->
-	  let (t',c',ef,e') = type_coerce co d_env enforce is_explicit widen t1 v t2 in
+	  let (t',c',ef,e') = type_coerce co d_env enforce is_explicit widen bounds t1 v t2 in
 	  ((t'::ts),c'@cs,union_effects ef efs,(e'::es), coerced || (v == e')))
           vars (List.combine t1s t2s) ([],[],pure_e,[],false) in
       if (not any_coerced) then (t2,cs,pure_e,e)
@@ -2330,13 +2349,14 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
 	let cs = [] (*[LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] (*This constraint failing should be a warning, but truncation is ok*)*)  in
-	let tannot = (l,Base(([],t2),External None, cs,pure_e,nob)) in
+	let tannot = (l,Base(([],t2),External None, cs,pure_e,bounds)) in
 	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),
 				  [(E_aux(E_internal_exp(tannot), tannot));e]),tannot))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
 	let cs = [] (* See above [LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in
-	let tannot = (l,Base(([],t2),External None,cs,pure_e,nob)) in
+	let tannot = (l,Base(([],t2),External None,cs,pure_e,bounds)) in
+	(*let _ = Printf.eprintf "Generating to_vec_dec call: bounds are %s\n" (bounds_to_string bounds) in*)
 	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),
 				  [(E_aux(E_internal_exp(tannot), tannot)); e]),tannot))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
@@ -2349,13 +2369,13 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
         [TA_nexp b2] -> 
 	let cs = [](*[LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in
-	let tannot = (l,Base(([],t2),External None, cs,pure_e,nob)) in
+	let tannot = (l,Base(([],t2),External None, cs,pure_e,bounds)) in
 	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),
 				  [(E_aux(E_internal_exp(tannot), tannot));e]),tannot))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
         [TA_nexp b2] -> 
 	let cs = [](*[LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in
-	let tannot = (l,Base(([],t2),External None,cs,pure_e,nob)) in
+	let tannot = (l,Base(([],t2),External None,cs,pure_e,bounds)) in
 	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),
 				  [(E_aux(E_internal_exp(tannot), tannot)); e]),tannot))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
@@ -2371,7 +2391,7 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2
           (*let _ = Printf.eprintf "Adding cast to remove register read\n" in*)
           let ef = add_effect (BE_aux (BE_rreg, l)) pure_e in
 	  let new_e = E_aux(E_cast(t_to_typ unit_t,e),(l,Base(([],t),External None,[],ef,nob))) in
-	  let (t',cs,ef',e) = type_coerce co d_env Guarantee is_explicit widen t new_e t2 in
+	  let (t',cs,ef',e) = type_coerce co d_env Guarantee is_explicit widen bounds t new_e t2 in
 	  (t',cs,union_effects ef ef',e)
 	| _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded"))
     | _,_,_ -> 
@@ -2453,8 +2473,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2
     | None -> eq_error l ("Type mismatch: " ^ (t_to_string t1) ^ " , " ^ (t_to_string t2)))
   | _,_ -> let t',cs = type_consistent co d_env enforce widen t1 t2 in (t',cs,pure_e,e)
 
-and type_coerce co d_env enforce is_explicit widen t1 e t2 = 
-  type_coerce_internal co d_env enforce is_explicit widen t1 [] e t2 [];;
+and type_coerce co d_env enforce is_explicit widen bounds t1 e t2 = 
+  type_coerce_internal co d_env enforce is_explicit widen bounds t1 [] e t2 [];;
 
 let rec select_overload_variant d_env params_check get_all variants actual_type =
   match variants with
@@ -2623,7 +2643,7 @@ let rec simple_constraint_check in_env cs =
 	  if (equate_n n1' n2') then None else Some(Eq(co,n1',n2')) end
 	else if occurs then eq_to_zero ok_to_set n1' n2'
         else Some(Eq(co,n1',n2'))
-      | _, Nuvar u ->
+      | _, Nuvar u -> 
 	(*let _ = Printf.eprintf "setting right nuvar\n" in*)
 	let occurs = occurs_in_nexp n1' n2' in
 	let leave = leave_nu_as_var n2' in
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 0cfa5089..fac69bb1 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -173,6 +173,7 @@ val cons_bs_annot : t -> nexp_range list -> bounds_env -> tannot
 val t_to_string : t -> string
 val n_to_string : nexp -> string
 val constraints_to_string : nexp_range list -> string
+val bounds_to_string : bounds_env -> string
 val tannot_to_string : tannot -> string
 val t_to_typ : t -> Ast.typ
 
@@ -193,8 +194,9 @@ val get_abbrev : def_envs -> t -> (t * nexp_range list)
 
 val extract_bounds : def_envs -> string -> t -> bounds_env
 val merge_bounds : bounds_env -> bounds_env -> bounds_env
-val find_var_from_nvar : string -> bounds_env -> (string option * string) option
+val find_var_from_nexp : nexp -> bounds_env -> (string option * string) option
 
+val expand_nexp : nexp -> nexp list
 val normalize_nexp : nexp -> nexp
 val get_index : nexp -> int (*TEMPORARILY expose nindex through this for debugging purposes*)
 val get_all_nvar : nexp -> string list (*Pull out all of the contained nvar and nuvars in nexp*)
@@ -209,6 +211,7 @@ val do_resolve_constraints : bool ref
 (*May raise an exception if effects do not match tannot effects, will lift unification variables to fresh type variables *)
 val check_tannot : Parse_ast.l -> tannot -> nexp option -> nexp_range list -> effect -> tannot
 
+val nexp_eq_check : nexp -> nexp -> bool (*structural equality only*)
 val nexp_eq : nexp -> nexp -> bool
 val nexp_one_more_than : nexp -> nexp -> bool
 
@@ -226,7 +229,7 @@ val type_consistent : constraint_origin -> def_envs -> range_enforcement -> bool
 (* type_coerce mutates to unify variables, and will raise an exception if the first type cannot
    be coerced into the second and is additionally inconsistent with the second; 
    bool specifices whether this has arisen from an implicit or explicit type coercion request *)
-val type_coerce : constraint_origin -> def_envs -> range_enforcement -> bool -> bool -> t -> exp -> t -> t * nexp_range list * effect * exp
+val type_coerce : constraint_origin -> def_envs -> range_enforcement -> bool -> bool -> bounds_env -> t -> exp -> t -> t * nexp_range list * effect * exp
 
 (* Merge tannots when intersection or unioning two environments. In case of default types, defer to tannot on right 
    When merging atoms, use bool to control widening.