Support new memory write events in the sail front end and pretty printer

Events are eamem to signal the memory address to write to and wmv to pass the value to write

12 files changed, 220 insertions, 164 deletions

diff --git a/src/_tags b/src/_tags
index f188b454..334566bd 100644
--- a/src/_tags
+++ b/src/_tags
@@ -8,4 +8,4 @@ true: -traverse, debug
 <test/*> and not <test/*.cmxa>: use_nums, use_lem, use_str
 
 # disable partial match and unused variable warnings
-<**/*.ml>: warn_p, warn_y
+<**/*.ml>: warn_y
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 47810801..07fe01fd 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -20,6 +20,7 @@ let rec kind_to_string kind = match kind.k with
   | K_Ord -> "Order"
   | K_Efct -> "Effect"
   | K_infer -> "Infer"
+  | K_Val -> "Val"
   | K_Lam (kinds,kind) -> "Lam ... -> " ^ (kind_to_string kind)
 
 
@@ -234,6 +235,8 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect =
                                | Parse_ast.BE_wreg   -> BE_wreg
                                | Parse_ast.BE_rmem   -> BE_rmem
                                | Parse_ast.BE_wmem   -> BE_wmem
+			       | Parse_ast.BE_wmv    -> BE_wmv
+			       | Parse_ast.BE_eamem  -> BE_eamem
 			       | Parse_ast.BE_depend -> BE_depend
                                | Parse_ast.BE_undef  -> BE_undef
                                | Parse_ast.BE_unspec -> BE_unspec
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 76e696f9..3703940a 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -81,6 +81,8 @@ let doc_effect (BE_aux (e,_)) =
   | BE_wreg -> "wreg"
   | BE_rmem -> "rmem"
   | BE_wmem -> "wmem"
+  | BE_wmv  -> "wmv"
+  | BE_eamem -> "eamem"
   | BE_barr -> "barr"
   | BE_depend -> "depend"
   | BE_undef -> "undef"
diff --git a/src/lexer.mll b/src/lexer.mll
index 2f07eeb9..cab2e3be 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -117,6 +117,8 @@ let kw_table =
      ("wreg",                    (fun x -> Wreg));
      ("rmem",                    (fun x -> Rmem));
      ("wmem",                    (fun x -> Wmem));
+     ("wmv",                     (fun x -> Wmv));
+     ("eamem",                   (fun x -> Eamem));
      ("undef",                   (fun x -> Undef));
      ("unspec",                  (fun x -> Unspec));
      ("nondet",                  (fun x -> Nondet));
diff --git a/src/parser.mly b/src/parser.mly
index eb2ba153..733bb83c 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -135,7 +135,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token Enumerate Else Exit Extern False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order 
 %token Pure Rec Register Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef 
 %token Undefined Union With Val
-%token Barr Depend Rreg Wreg Rmem Wmem Undef Unspec Nondet
+%token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Undef Unspec Nondet
 
 
 /* Avoid shift/reduce conflict - see right_atomic_exp rule */
@@ -316,6 +316,10 @@ effect:
     { efl BE_rmem } 
   | Wmem
     { efl BE_wmem }
+  | Wmv
+    { efl BE_wmv }
+  | Eamem
+    { efl BE_eamem }
   | Undef
     { efl BE_undef }
   | Unspec
diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll
index b8869812..8987c0fd 100644
--- a/src/pre_lexer.mll
+++ b/src/pre_lexer.mll
@@ -146,7 +146,7 @@ rule token = parse
                                             (M.find i kw_table) ()
                                           else
                                             Id(r i) }
-  | tyvar_start startident ident* as i   { Other }
+  | tyvar_start startident ident*   { Other }
   | "&" oper_char+ | "@" oper_char+  | "^" oper_char+ | "/" oper_char+ | "=" oper_char+ |
     "!" oper_char+ | ">" oper_char+  | "<" oper_char+ | "+" oper_char+ | "*" oper_char+ |
     "~"	oper_char+ | "&&" oper_char+ | "^^" oper_char+| "::" oper_char+| "=/=" oper_char+ |
@@ -158,9 +158,9 @@ rule token = parse
     ">_ui" oper_char+ | "<=_s" oper_char+ | "<=_si" oper_char+ | "<=_u" oper_char+ | "<=_ui" oper_char+ |
     "<_s" oper_char+ | "<_si" oper_char+ | "<_u" oper_char+ | "<_ui" oper_char+ | "**_s" oper_char+ |
     "**_si" oper_char+ | "*_u" oper_char+ | "*_ui" oper_char+ | "2^" oper_char+  { Other }			
-  | digit+ as i                         { Other }
-  | "0b" (binarydigit+ as i)		{ Other }
-  | "0x" (hexdigit+ as i) 		{ Other }
+  | digit+                              { Other }
+  | "0b" (binarydigit+) 		{ Other }
+  | "0x" (hexdigit+)     		{ Other }
   | '"'                                 { let _ = string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf in Other }
   | eof                                 { Eof }
   | _  as c                             { raise (LexError(
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index c56293ad..182c1929 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -142,6 +142,8 @@ and pp_format_base_effect_lem (BE_aux(e,l)) =
     | BE_wreg -> "BE_wreg"
     | BE_rmem -> "BE_rmem"
     | BE_wmem -> "BE_wmem"
+    | BE_wmv  -> "BE_wmv"
+    | BE_eamem -> "BE_eamem"
     | BE_barr -> "BE_barr"
     | BE_depend -> "BE_depend"
     | BE_undef -> "BE_undef"
@@ -265,6 +267,7 @@ and pp_format_n n =
     | Nuvar _ -> "(Ne_var \"fresh_v_" ^ string_of_int (get_index n) ^ "\")"
     | Nneg_inf -> "(Ne_unary Ne_inf)"
     | Npow _ -> "power_not_implemented"
+    | Ninexact -> "(Ne_add Ne_inf (Ne_unary Ne_inf)"
 and pp_format_e e = 
   "(Effect_aux " ^
   (match e.effect with
@@ -440,6 +443,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
 	    | _ -> raise (Reporting_basic.err_unreachable l "Internal_exp given implicit without variable or const"))
         | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given non-vector or implicit"))
     | E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ ->  raise (Reporting_basic.err_unreachable l "Found internal cast or exp with overload")
+   | E_internal_exp_user _ -> (raise (Reporting_basic.err_unreachable l "Found non-rewritten internal_exp_user"))
   in
   print_e ppf e
 
@@ -641,6 +645,8 @@ let doc_effect (BE_aux (e,_)) =
   | BE_wreg -> "wreg"
   | BE_rmem -> "rmem"
   | BE_wmem -> "wmem"
+  | BE_wmv  -> "wmv"
+  | BE_eamem -> "eamem"
   | BE_barr -> "barr"
   | BE_depend -> "depend"
   | BE_undef -> "undef"
@@ -932,7 +938,11 @@ let doc_exp, doc_let =
 	  | E_lit (L_aux(L_one, _)) | E_lit (L_aux(L_zero, _)) ->
 	    utf8string
 	      ("0b" ^ 
-		  (List.fold_right (fun (E_aux(E_lit(L_aux(l, _)),_)) rst -> match l with | L_one -> "1"^rst | L_zero -> "0"^rst) exps "")) 
+		  (List.fold_right (fun (E_aux( e,_)) rst ->
+		    (match e with 
+		      | E_lit(L_aux(l, _)) ->
+			((match l with | L_one -> "1" | L_zero -> "0" | L_undef -> "u" | _ -> assert false) ^ rst)
+		      | _ -> assert false)) exps "")) 
 	  | _ -> default_print ()))
   | E_vector_indexed (iexps, (Def_val_aux (default,_))) ->
     let default_string = 
@@ -996,9 +1006,7 @@ let doc_exp, doc_let =
 	  | Nvar v -> utf8string v
 	  | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given implicit without var or const"))
       | _ ->  raise (Reporting_basic.err_unreachable l ("Internal exp given non-vector, non-implicit " ^ t_to_string t)))
-
-  (* XXX missing case
-     AAA internal_cast should never have an overload, if it's been seen it's a bug *)
+  | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable Unknown ("internal_exp_user not rewritten away"))
   | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false
 
   and let_exp (LB_aux(lb,_)) = match lb with
diff --git a/src/process_file.ml b/src/process_file.ml
index 3b10aef8..c36f9381 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -97,7 +97,8 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.
 		Type_internal.rec_env = []; Type_internal.alias_env = Envmap.empty; 
 		Type_internal.default_o = 
                 {Type_internal.order = (match o with | (Ast.Ord_aux(Ast.Ord_inc,_)) -> Type_internal.Oinc 
-		                                     | (Ast.Ord_aux(Ast.Ord_dec,_)) -> Type_internal.Odec)};} in
+		                                     | (Ast.Ord_aux(Ast.Ord_dec,_)) -> Type_internal.Odec
+						     | _ -> Type_internal.Oinc)};} in
   Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env,Type_internal.nob,Envmap.empty)) defs 
 
 let rewrite_ast (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs defs
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 93908eee..7999c3b4 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -40,7 +40,8 @@ let rec rewrite_nexp_to_exp program_vars l nexp =
 		    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
+	E_aux (E_id (Id_aux (Id v,l)),(l,simple_annot typ))
+      | _ -> raise (Reporting_basic.err_unreachable l ("rewrite_nexp given n that can't be rewritten: " ^ (n_to_string nexp))) in
   match program_vars with
     | None -> actual_rewrite_n nexp
     | Some program_vars ->
@@ -113,7 +114,6 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) =
     | E_internal_cast ((_,casted_annot),exp) -> 
       let new_exp = rewrite_exp exp in
       (match casted_annot,exp with
-	| NoTyp,_ | Overload _,_ -> new_exp
 	| Base((_,t),_,_,_,_),E_aux(ec,(ecl,Base((_,exp_t),_,_,_,_))) ->
 	  (match t.t,exp_t.t with
 	    (*TODO should pass d_env into here so that I can look at the abbreviations if there are any here*)
@@ -122,18 +122,19 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) =
 	      (match n1.nexp with
 		| Nconst i1 -> if nexp_eq n1 n2 then new_exp else rewrap (E_cast (t_to_typ t,new_exp))
 		| Nadd _ | Nsub _ -> (match o1.order with
-		    | Oinc -> new_exp
 		    | Odec -> 
 		      if nexp_one_more_than nw1 n1 
 		      then rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Unknown)), Unknown), new_exp))
-		      else new_exp)
+		      else new_exp
+		    | _ -> new_exp)
 		| _ -> new_exp)
-	    | _ -> new_exp))
+	    | _ -> new_exp)
+	| _ -> new_exp)
     | E_internal_exp (l,impl) ->
       (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
+	  (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;_;_]) ->
@@ -147,19 +148,27 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) =
 	      let nexps = expand_nexp i in
 	      (match (match_to_program_vars nexps bounds) with
 		| [] -> rewrite_nexp_to_exp None l i
-		| map -> rewrite_nexp_to_exp (Some map) l i))
+		| map -> rewrite_nexp_to_exp (Some map) l i)
+	    | _ -> 
+	      raise (Reporting_basic.err_unreachable l 
+		       ("Internal_exp given unexpected types " ^ (t_to_string t))))
+	| _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp given none Base annot")))
     | 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
+	  (match (tu.t,ti.t) with
 	    | (Tapp("implicit", [TA_nexp u]),Tapp("implicit",[TA_nexp i])) ->
 	      (*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*)
-		| map -> rewrite_nexp_to_exp (Some map) l i))
+		| map -> rewrite_nexp_to_exp (Some map) l i)
+	    | _ -> 
+	      raise (Reporting_basic.err_unreachable l 
+		       ("Internal_exp_user given unexpected types " ^ (t_to_string tu) ^ ", " ^ (t_to_string ti))))
+	| _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given none Base annot")))
 
 and rewrite_let (LB_aux(letbind,(l,annot))) = match letbind with
   | LB_val_explicit (typschm, pat,exp) ->
@@ -187,6 +196,7 @@ let rewrite_def d = match d with
   | DEF_type _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ -> d
   | DEF_fundef fdef -> DEF_fundef (rewrite_fun fdef)
   | DEF_val letbind -> DEF_val (rewrite_let letbind)
+  | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter")
 
 let rewrite_defs (Defs defs) = 
   let rec rewrite ds = match ds with
diff --git a/src/type_check.ml b/src/type_check.ml
index f1b44395..0c6cbf46 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -146,7 +146,8 @@ let rec quants_to_consts ((Env (d_env,t_env,b_env,tp_env)) as env) qis : (t_para
                     | K_Typ  -> TA_typ {t = Tvar i}
                     | K_Nat  -> TA_nexp { nexp = Nvar i}                      
                     | K_Ord  -> TA_ord { order = Ovar i}
-                    | K_Efct -> TA_eft { effect = Evar i} in
+                    | K_Efct -> TA_eft { effect = Evar i}
+		    | _ -> raise (Reporting_basic.err_unreachable l'' "illegal kind allowed") in
                   ((i,k)::ids,targ::typarms,cs)
 		| None -> raise (Reporting_basic.err_unreachable l'' "Unkinded id without default after initial check"))
 	    | KOpt_kind(kind,Kid_aux((Var i),l'')) -> 
@@ -155,7 +156,9 @@ let rec quants_to_consts ((Env (d_env,t_env,b_env,tp_env)) as env) qis : (t_para
                 | K_Typ  -> TA_typ {t = Tvar i}
                 | K_Nat  -> TA_nexp { nexp = Nvar i}                      
                 | K_Ord  -> TA_ord { order = Ovar i}
-                | K_Efct -> TA_eft { effect = Evar i} in
+                | K_Efct -> TA_eft { effect = Evar i}
+		| K_Lam _ -> typ_error l'' "kind -> kind not permitted here"
+		| _ -> raise (Reporting_basic.err_unreachable l'' "Kind either infer or internal here")  in
               ((i,k)::ids,targ::typarms,cs))
 	| QI_const(NC_aux(nconst,l')) -> 
 	  (*TODO: somehow the requirement vs best guarantee needs to be derived from user or context*)
@@ -227,7 +230,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 		       TA_ord d_env.default_o;TA_typ{t = Tid"bit"}])},lit
 	  | L_string s -> {t = Tid "string"},lit
 	  | L_undef -> typ_error l' "Cannot pattern match on undefined") in
-(*      let _ = Printf.eprintf "checking pattern literal. expected type is %s. t is %s\n" (t_to_string expect_t) (t_to_string t) in*)
+      (*let _ = Printf.eprintf "checking pattern literal. expected type is %s. t is %s\n" (t_to_string expect_t) (t_to_string t) in*)
       let t',cs' = type_consistent (Patt l) d_env Require true t expect_t in
       let cs_l = cs@cs' in
       (P_aux(P_lit(L_aux(lit,l')),(l,cons_tag_annot t emp_tag cs_l)),Envmap.empty,cs_l,nob,t)
@@ -315,7 +318,9 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 	      let tup = {t = Ttup(List.map (fun (t,_,_,_) -> t) typ_pats)} in
 	      let ft = {t = Tfn(tup,t, IP_none,pure_e) } in
 	      let (ft_subst,cs,_,_) = subst vs false t cs pure_e in
-	      let subst_rtyp,subst_typs = match ft_subst.t with | Tfn({t=Ttup tups},rt,_,_) -> rt,tups in
+	      let subst_rtyp,subst_typs = 
+		match ft_subst.t with | Tfn({t=Ttup tups},rt,_,_) -> rt,tups 
+		  | _ -> raise (Reporting_basic.err_unreachable l "fields_to_rec gave a non function type") in
 	      let pat_checks = 
 		List.map2 (fun (_,id,l,pat) styp -> 
 		  let (pat,env,constraints,new_bounds,u) = check_pattern envs emp_tag styp pat in
@@ -327,7 +332,8 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 	      let constraints = (List.fold_right (fun (_,_,cs,_) cons -> cs@cons) pat_checks [])@cs in
 	      let bounds = List.fold_right (fun (_,_,_,bounds) b_env -> merge_bounds bounds b_env) pat_checks nob in
               let t',cs' = type_consistent (Patt l) d_env Guarantee false ft_subst expect_t in
-	      (P_aux((P_record(pats',false)),(l,cons_tag_annot t' emp_tag (cs@cs'))),env,constraints@cs',bounds,t')))
+	      (P_aux((P_record(pats',false)),(l,cons_tag_annot t' emp_tag (cs@cs'))),env,constraints@cs',bounds,t')
+	    | _ -> raise (Reporting_basic.err_unreachable l "fields_to_rec returned a non Base tannot")))
     | P_vector pats -> 
       let (item_t, base, rise, ord) = match expect_actual.t with 
 	| Tapp("vector",[TA_nexp b;TA_nexp r;TA_ord o;TA_typ i]) -> (i,b,r,o)
@@ -711,15 +717,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       in
       let check_result ret imp tag cs ef lft rht =
         match imp with
-	  (*| IP_length _ ->  
-            let internal_exp =  match expect_t.t,ret.t with 
-              | Tapp("vector",_),_ -> 
-		E_aux (E_internal_exp (l,simple_annot expect_t), (l, simple_annot nat_t))
-              | _,Tapp("vector",_) -> 
-		E_aux (E_internal_exp (l,simple_annot ret), (l,simple_annot nat_t))
-              | _ -> 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 -> 
+          | _ -> (*implicit isn't allowed at the moment on any infix functions *)
             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
@@ -874,7 +872,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
         | (Odec,_) | (Ouvar _,Odec) | (Ovar _,Odec) -> 
           {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
+                              TA_ord {order= Odec}; TA_typ item_t])} 
+	| _ -> raise (Reporting_basic.err_unreachable l "Default order was neither inc or dec") in
       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')
@@ -886,7 +885,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let is_increasing = first <= last in
       let es,cs,effect,contains_skip,_ = (List.fold_right 
 			      (fun ((i,e),c,ef) (es,cs,effect,skips,prev) -> 
-				(*let _ = Printf.printf "Checking increasing %b %i %i\n" is_increasing prev i in*)
+				(*let _ = Printf.eprintf "Checking increasing %b %i %i\n" is_increasing prev i in*)
                                 let (esn, csn, efn) = (((i,e)::es), (c@cs), union_effects ef effect) in
 				if (is_increasing && prev > i)
 				then (esn,csn,efn,(((prev-i) > 1) || skips),i)
@@ -950,59 +949,44 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	(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) ->
-      let base,rise,ord = new_n(),new_n(),new_o() in
-      let new_base,new_rise = new_n(),new_n() in
-      let n1,min1,max1 = new_n(), new_n(),new_n() in
-      let n2,min2,max2 = new_n(), new_n(),new_n() in
-      let base_e,rise_e,ord_e,item_t = match expect_t.t with
-	| Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> base_n,rise_n,ord_n,item_t
-	| _ -> new_n(),new_n(),new_o(),new_t() in
-      let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t])} in
-      let (vec',t',_,cs,_,ef) = check_exp envs imp_param vt vec in
-      let i1t = {t=Tapp("atom",[TA_nexp n1])} in
+      (*let _ = Printf.eprintf "checking e_vector_subrange: expect_t is %s\n" (t_to_string expect_t) in*)
+      let base,length,ord = new_n(),new_n(),new_o() in
+      let new_length = new_n() in
+      let n1_size = new_n() in
+      let n2_size = new_n() in
+      let item_t = match expect_t.t with
+	| Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> item_t
+	| _ -> new_t() in
+      let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp length;TA_ord ord;TA_typ item_t])} in
+      let (vec',vt',_,cs,_,ef) = check_exp envs imp_param vt vec in      
+      let i1t = {t=Tapp("atom",[TA_nexp n1_size])} in
       let (i1', ti1, _,cs_i1,_,ef_i1) = check_exp envs imp_param i1t i1 in
-      let i2t = {t=Tapp("atom",[TA_nexp n2])} in
+      let i2t = {t=Tapp("atom",[TA_nexp n2_size])} in
       let (i2', ti2, _,cs_i2,_,ef_i2) = check_exp envs imp_param i2t i2 in
       let cs_loc =
 	match (ord.order,d_env.default_o.order) with
 	  | (Oinc,_) -> 
-	    [Eq((Expr l), new_base, n1);
-	     Eq((Expr l), new_rise, mk_sub n2 n1);
-	     LtEq((Expr l),Require, min1, n1); LtEq((Expr l),Require, n1,max1);
-	     LtEq((Expr l),Require, min2, n2); LtEq((Expr l),Require, n2,max2);
-	     LtEq((Expr l),Require,base,n1); 
-	     LtEq((Expr l),Require,base,max1); 
-	     LtEq((Expr l),Require,n2,mk_add base rise);
-	     LtEq((Expr l),Require,max2,mk_add base rise);]
+	    [LtEq((Expr l), Require, base, n1_size);
+	     LtEq((Expr l), Require, n1_size, n2_size);
+	     LtEq((Expr l), Require, n2_size, mk_sub (mk_add base length) n_one);
+	     Eq((Expr l), new_length, mk_add (mk_sub n2_size n1_size) n_one)]
 	  | (Odec,_) ->
-	    [Eq((Expr l), new_base, n1);
-	     Eq((Expr l), new_rise, mk_add (mk_sub n1 n2) n_one);
-	     LtEq((Expr l), Require, min1, n1); LtEq((Expr l),Require, n1,max1);
-	     LtEq((Expr l), Require, min2, n2); LtEq((Expr l),Require, n2,max2);
-	     GtEq((Expr l),Require,base,n1); 
-	     GtEq((Expr l),Require,base,max1); 
-	     LtEq((Expr l),Require,n2,mk_add (mk_sub base rise) n_one);
-	     LtEq((Expr l),Require,max2,mk_add (mk_sub base rise) n_one);]	     
+	    [GtEq((Expr l), Require, base, n1_size);
+	     GtEq((Expr l), Require, n1_size, n2_size);
+	     GtEq((Expr l), Require, n2_size, mk_add (mk_sub base length) n_one);
+	     Eq((Expr l), new_length, mk_add (mk_sub n1_size n2_size) n_one)]	    
 	  | (_,Oinc) ->
-	    [Eq((Expr l), new_base, n1);
-	     Eq((Expr l), new_rise, mk_sub n2 n1);
-	     LtEq((Expr l),Require, min1, n1); LtEq((Expr l),Require, n1,max1);
-	     LtEq((Expr l),Require, min2, n2); LtEq((Expr l),Require, n2,max2);
-	     LtEq((Expr l),Require,base,n1); 
-	     LtEq((Expr l),Require,base,max1); 
-	     LtEq((Expr l),Require,n2,mk_add base rise);
-	     LtEq((Expr l),Require,max2,mk_add base rise);]
+	    [LtEq((Expr l), Require, base, n1_size);
+	     LtEq((Expr l), Require, n1_size, n2_size);
+	     LtEq((Expr l), Require, n2_size, mk_sub (mk_add base length) n_one);
+	     Eq((Expr l), new_length, mk_add (mk_sub n2_size n1_size) n_one)]
 	  | (_,Odec) -> 
-	    [Eq((Expr l), new_base, n1);
-	     Eq((Expr l), new_rise, mk_add (mk_sub n1 n2) n_one);
-	     LtEq((Expr l), Require, min1, n1); LtEq((Expr l),Require, n1,max1);
-	     LtEq((Expr l), Require, min2, n2); LtEq((Expr l),Require, n2,max2);
-	     GtEq((Expr l),Require,base,n1); 
-	     GtEq((Expr l),Require,base,max1); 
-	     LtEq((Expr l),Require,n2,mk_add (mk_sub base rise) n_one);
-	     LtEq((Expr l),Require,max2,mk_add (mk_sub base rise) n_one);]	     
+	    [GtEq((Expr l), Require, base, n1_size);
+	     GtEq((Expr l), Require, n1_size, n2_size);
+	     GtEq((Expr l), Require, n2_size, mk_add (mk_sub base length) n_one);
+	     Eq((Expr l), new_length, mk_add (mk_sub n1_size n2_size) n_one)]
 	  | _ -> 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 nt = {t = Tapp("vector", [TA_nexp n1_size; TA_nexp new_length; TA_ord ord; TA_typ item_t]) } in
       let (t,cs3,ef3,e') = 
 	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
@@ -1134,7 +1118,6 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       (match u_actual.t with
 	| Tid(n) | Tapp(n,_)->
 	  (match lookup_record_typ n d_env.rec_env with 
-	    | None -> typ_error l ("Expected a value of type " ^ n ^ " but found a struct")
 	    | Some(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) -> 
 	      let (ts,cs,eft,subst_env) = subst params false t cs eft in
 	      if (List.length fexps = List.length fields) 
@@ -1143,18 +1126,19 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 		   let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in
 		   (e',t',t_env,cs@cons@cs',nob,union_effects ef ef')
 	      else typ_error l ("Expected a struct of type " ^ n ^ ", which should have " ^ string_of_int (List.length fields) ^ " fields")
-	    | Some(i,Register,tannot,fields) -> typ_error l ("Expected a value with register type, found a struct"))
+	    | Some(i,Register,tannot,fields) -> typ_error l ("Expected a value with register type, found a struct")
+	    | _ -> typ_error l ("Expected a value of type " ^ n ^ " but found a struct"))	    
 	| Tuvar _ ->
 	  let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in
 	  (match lookup_record_fields field_names d_env.rec_env with
-	    | None -> typ_error l "No struct type matches the set of fields given"
 	    | Some(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) ->
 	      let (ts,cs,eft,subst_env) = subst params false t cs eft in
 	      let fexps,cons,ef = List.fold_right (field_walker r subst_env bounds tag i) fexps ([],[],pure_e) in 
 	      let e = E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,simple_annot ts)) in
 	      let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in
 	      (e',t',t_env,cs@cons@cs',nob,union_effects ef ef')
-	    | Some(i,Register,tannot,fields) -> typ_error l "Expected a value with register type, found a struct")
+	    | Some(i,Register,tannot,fields) -> typ_error l "Expected a value with register type, found a struct"
+	    | _ -> typ_error l "No struct type matches the set of fields given")
 	| _ -> typ_error l ("Expected an expression of type " ^ t_to_string expect_t ^ " but found a struct"))
     | E_record_update(exp,FES_aux(FES_Fexps(fexps,_),l')) -> 
       let (e',t',_,c,_,ef) = check_exp envs imp_param expect_t exp in
@@ -1170,7 +1154,6 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       (match t'.t with
 	| Tid i | Tabbrev(_, {t=Tid i}) | Tapp(i,_) ->
 	  (match lookup_record_typ i d_env.rec_env with
-	    | None -> typ_error l ("Expected a struct for this update, instead found an expression with type " ^ i)
 	    | Some((i,Register,tannot,fields)) -> typ_error l "Expected a struct for this update, instead found a register"
 	    | Some(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) ->
 	      if (List.length fexps <= List.length fields) 
@@ -1180,7 +1163,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 		let e = E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')), (l,simple_annot ts)) in
 		let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in
 		(e',t',t_env,cs@cons@cs',nob,union_effects ef ef')
-	      else typ_error l ("Expected fields from struct " ^ i ^ ", given more fields than struct includes"))
+	      else typ_error l ("Expected fields from struct " ^ i ^ ", given more fields than struct includes")
+	    | _ -> 
+	      typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i))
 	| Tuvar _ ->
 	  let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in
 	  (match lookup_possible_records field_names d_env.rec_env with
@@ -1200,8 +1185,6 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       (match t'.t with
       | Tabbrev({t=Tid i}, _) | Tabbrev({t=Tapp(i,_)},_) | Tid i | Tapp(i,_) ->
 	  (match lookup_record_typ i d_env.rec_env with
-	    | None -> 
-	      typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i)
 	    | Some(((i,rec_kind,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) ->
 	      let (ts,cs,eft,subst_env) = subst params false t cs eft in
 	      (match lookup_field_type fi r with
@@ -1212,7 +1195,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 		  let (et',c',ef',acc) = 
 		    type_coerce (Expr l) d_env Require false false b_env ft 
 		      (E_aux(E_field(e',id),(l,Base(([],ft),tag,cs,eft,bounds)))) expect_t in
-		  (acc,et',t_env,cs@c'@c_sub@cs_sub',nob,union_effects ef' ef_sub)))
+		  (acc,et',t_env,cs@c'@c_sub@cs_sub',nob,union_effects ef' ef_sub))
+	    | _ -> 
+	      typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i))
 	| Tuvar _ ->
 	  (match lookup_possible_records [fi] d_env.rec_env with
 	    | [] -> typ_error l ("No struct or register has a field " ^ fi)
@@ -1252,12 +1237,12 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let (lexp',t',_,t_env',tag,cs,b_env',ef) = check_lexp envs imp_param true lexp in
       let (exp',t'',_,cs',_,ef') = check_exp envs imp_param t' exp in
       let (t',c') = type_consistent (Expr l) d_env Require false unit_t expect_t in
-      (*let _ = Printf.eprintf "Constraints for E_assign %s\n" (constraints_to_string (cs@cs'@c')) in*)
       (E_aux(E_assign(lexp',exp'),(l,(Base(([],unit_t),tag,[],ef,nob)))),unit_t,t_env',cs@cs'@c',b_env',union_effects ef ef')
     | E_exit e ->
       let (e',t',_,_,_,_) = check_exp envs imp_param (new_t ()) e in
       (E_aux (E_exit e',(l,(simple_annot expect_t))),expect_t,t_env,[],nob,pure_e)
-    | E_internal_cast _ | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
+    | E_internal_cast _ | E_internal_exp _ | E_internal_exp_user _ -> 
+      raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
 		    
 and check_block envs imp_param expect_t exps:((tannot exp) list * tannot * nexp_range list * t * effect) =
   let Env(d_env,t_env,b_env,tp_env) = envs in
@@ -1313,7 +1298,8 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
               (LEXP_aux(lexp,(l,(Base(([],t'),Alias,[],ef,nob)))), t, false, Envmap.empty, External (Some reg),[],nob,ef)
             | Some(TwoReg(reg1,reg2, (Base(([],t'),_,_,_,_)))) ->
 	      let u = match t.t with
-		| Tapp("register", [TA_typ u]) -> u in
+		| Tapp("register", [TA_typ u]) -> u 
+		| _ -> raise (Reporting_basic.err_unreachable l "TwoReg didn't contain a register type") in
               (LEXP_aux(lexp,(l,Base(([],t'),Alias,[],ef,nob))), u, false, Envmap.empty, External None,[],nob,ef)
             | _ -> assert false)
 	| Some(Base((parms,t),tag,cs,_,b)) ->
@@ -1369,8 +1355,9 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
 	      (match ef'.effect with
 		| Eset effects ->
                   let mem_write = List.exists (fun (BE_aux(b,_)) -> match b with | BE_wmem -> true | _ -> false) effects in
+		  let memv_write = List.exists (fun (BE_aux(b,_)) -> match b with |BE_wmv -> true | _ -> false) effects in
                   let reg_write = List.exists (fun (BE_aux(b,_)) -> match b with | BE_wreg -> true | _ -> false) effects in
-		  if  (mem_write || reg_write)
+		  if  (mem_write || memv_write || reg_write)
 		  then
                     let app,cs_a = get_abbrev d_env apps in
                     let out,cs_o = get_abbrev d_env out in
@@ -1406,8 +1393,8 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
 			let ef_all = union_effects ef ef_e in
 			(LEXP_aux(LEXP_memory(id,[e]),(l,Base(([],out),tag,cs_call,ef,nob))),
 			 app,false,Envmap.empty,tag,cs_call@cs_e,nob,ef_all))
-		  else typ_error l ("Assignments require functions with a wmem or wreg effect")
-		| _ -> typ_error l ("Assignments require functions with a wmem or wreg effect"))
+		  else typ_error l ("Assignments require functions with a wmem, wmv, or wreg effect")
+		| _ -> typ_error l ("Assignments require functions with a wmem, wmv, or wreg effect"))
 	    | _ -> typ_error l ("Assignments require a function here, found " ^ i ^ " which has type " ^ (t_to_string t)))
 	| _ -> typ_error l ("Unbound identifier " ^ i))
     | LEXP_cast(typ,id) -> 
@@ -1485,55 +1472,49 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
 	  typ_error l "Assignment expected a vector with a known order, try adding an annotation."
 	| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t))) 
     | LEXP_vector_range(vec,e1,e2)-> 
-      let (vec',item_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in
-      let item_t,cs = get_abbrev d_env item_t in
-      let item_actual = match item_t.t with | Tabbrev(_,t) -> t | _ -> item_t in
-      let item_actual,add_reg_write,reg_still_required,cs = 
-	match item_actual.t with
+      let (vec',vec_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in
+      let vec_t,cs = get_abbrev d_env vec_t in
+      let vec_actual = match vec_t.t with | Tabbrev(_,t) -> t | _ -> vec_t in
+      let vec_actual,add_reg_write,reg_still_required,cs = 
+	match vec_actual.t with
 	  | Tapp("register",[TA_typ t]) ->
 	    (match get_abbrev d_env t with | {t=Tabbrev(_,t)},cs' | t,cs' -> t,true,false,cs@cs')
 	  | Tapp("reg",[TA_typ t]) ->
 	    (match get_abbrev d_env t with | {t=Tabbrev(_,t)},cs' | t,cs' -> t,false,false,cs@cs')
-	  | _ -> item_actual,false,true,cs in
-      (match item_actual.t with
+	  | _ -> vec_actual,false,true,cs in
+      (match vec_actual.t with
 	| Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ t]) ->
-	  let base_e1,range_e1,base_e2,range_e2 = new_n(),new_n(),new_n(),new_n() in
-	  let base_t = {t=Tapp("range",[TA_nexp base_e1;TA_nexp range_e1])} in
-	  let range_t = {t=Tapp("range",[TA_nexp base_e2;TA_nexp range_e2])} in
-	  let (e1',base_t',_,cs1,_,ef_e) = check_exp envs imp_param base_t e1 in
-	  let (e2',range_t',_,cs2,_,ef_e') = check_exp envs imp_param range_t e2 in
-	  let base_e1,range_e1,base_e2,range_e2 = match base_t'.t,range_t'.t with
-	    | (Tapp("range",[TA_nexp base_e1;TA_nexp range_e1]),
-	       Tapp("range",[TA_nexp base_e2;TA_nexp range_e2])) -> base_e1,range_e1,base_e2,range_e2
-	    | _ -> base_e1,range_e1,base_e2,range_e2 in
-          let len = new_n() in
+	  let size_e1,size_e2 = new_n(),new_n() in
+	  let e1_t = {t=Tapp("atom",[TA_nexp size_e1])} in
+	  let e2_t = {t=Tapp("atom",[TA_nexp size_e2])} in
+	  let (e1',e1_t',_,cs1,_,ef_e) = check_exp envs imp_param e1_t e1 in
+	  let (e2',e2_t',_,cs2,_,ef_e') = check_exp envs imp_param e2_t e2 in
+	  let len = new_n() in
 	  let needs_reg = match t.t with
 	    | Tapp("reg",_) -> false
 	    | Tapp("register",_) -> false
 	    | _ -> true in
 	  let cs_t,res_t = match ord.order with
-	    | Oinc ->  ([LtEq((Expr l),Require,base,base_e1);
-			 LtEq((Expr l),Require,mk_add base_e1 range_e1, mk_add base_e2 range_e2);
-			 LtEq((Expr l),Require,mk_add base_e1 range_e2, mk_add base rise);
-                         LtEq((Expr l),Require,len, mk_sub (mk_add (mk_add base_e2 range_e2) n_one) 
-			                                   (mk_add base_e1 range_e1))],
-			{t=Tapp("vector",[TA_nexp base_e1;TA_nexp len;TA_ord ord;TA_typ t])})
-	    | Odec -> ([GtEq((Expr l),Require,base,base_e1);
-			GtEq((Expr l),Require,mk_add base_e1 range_e1,mk_add base_e2 range_e2);
-			GtEq((Expr l),Require,mk_add base_e1 range_e2,mk_sub base rise);                         
-                        LtEq((Expr l),Require,len, mk_sub (mk_add (mk_add base_e2 range_e2) n_one)
-			                                  (mk_add base_e1 range_e1));],
-                       {t=Tapp("vector",[TA_nexp {nexp=Nadd(base_e1,range_e1)};TA_nexp len;TA_ord ord; TA_typ t])})
+	    | Oinc ->  ([LtEq((Expr l),Require,base,size_e1);
+			 LtEq((Expr l),Require,size_e1, size_e2);
+			 LtEq((Expr l),Require,size_e2, rise);
+                         Eq((Expr l),len, mk_add (mk_sub size_e2 size_e1) n_one)],
+			{t=Tapp("vector",[TA_nexp size_e1;TA_nexp len;TA_ord ord;TA_typ t])})
+	    | Odec -> ([GtEq((Expr l),Require,base,size_e1);
+			GtEq((Expr l),Require,size_e1,size_e2);
+			GtEq((Expr l),Require,size_e2,mk_sub base rise);                         
+                        Eq((Expr l),len, mk_add (mk_sub size_e1 size_e2) n_one)],
+                       {t=Tapp("vector",[TA_nexp size_e1;TA_nexp len;TA_ord ord; TA_typ t])})
 	    | _ -> typ_error l ("Assignment to a range of vector elements requires either inc or dec order")
 	  in
 	  let cs = cs_t@cs@cs1@cs2 in
 	  let ef = union_effects ef (union_effects ef_e ef_e') in
 	  if is_top && reg_required && reg_still_required && needs_reg 
 	  then typ_error l "Assignment requires a register or a non-parameter, non-letbound local identifier"
-	  else (LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Base(([],item_t),tag,cs,ef,nob))),res_t,reg_required&&reg_still_required && needs_reg
-		,env,tag,cs,bounds,ef)
+	  else (LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Base(([],res_t),tag,cs,ef,nob))),
+		res_t,reg_required&&reg_still_required && needs_reg,env,tag,cs,bounds,ef)
 	| Tuvar _ -> typ_error l "Assignement to a range of elements requires a vector with a known order, try adding an annotation."
-	| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string item_t))) 
+	| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t))) 
     | LEXP_field(vec,id)-> 
       let (vec',item_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in
       let vec_t = match vec' with
@@ -1543,8 +1524,6 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
       (match vec_t.t with
 	| Tid i | Tabbrev({t=Tid i},_) | Tabbrev({t=Tapp(i,_)},_) | Tapp(i,_)->
 	  (match lookup_record_typ i d_env.rec_env with
-	    | None -> 
-	      typ_error l ("Expected a register or struct for this update, instead found an expression with type " ^ i)
 	    | Some(((i,rec_kind,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) ->
 	      let (ts,cs,eft,subst_env) = subst params false t cs eft in
 	      (match lookup_field_type fi r with
@@ -1552,7 +1531,9 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
                 | Some t ->
 		  let ft = typ_subst subst_env false t in
 		  let (_,cs_sub') = type_consistent (Expr l) d_env Guarantee false ts vec_t in
-		  (LEXP_aux(LEXP_field(vec',id),(l,(Base(([],ft),tag,csi@cs,eft,nob)))),ft,false,env,tag,csi@cs@cs_sub',bounds,ef)))
+		  (LEXP_aux(LEXP_field(vec',id),(l,(Base(([],ft),tag,csi@cs,eft,nob)))),ft,false,env,tag,csi@cs@cs_sub',bounds,ef))
+	    | _ -> 
+	      typ_error l ("Expected a register or struct for this update, instead found an expression with type " ^ i))
 	| _ -> typ_error l ("Expected a register binding here, found " ^ (t_to_string item_t)))
 
 and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * nexp_range list * bounds_env * effect =
@@ -1723,23 +1704,25 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
   let is_rec = match recopt with
               | Rec_aux(Rec_nonrec,_) -> false
 	      | Rec_aux(Rec_rec,_) -> true in
-  let Some(id) = List.fold_right 
-    (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) id' ->
-      match id' with
-	| Some(id') -> if id' = id_to_string id then Some(id') 
-	  else typ_error l ("Function declaration expects all definitions to have the same name, " 
-			    ^ id_to_string id ^ " differs from other definitions of " ^ id')
-	| None -> Some(id_to_string id)) funcls None in
+  let id = match (List.fold_right 
+		    (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) id' ->
+		      match id' with
+			| Some(id') -> if id' = id_to_string id then Some(id') 
+			  else typ_error l ("Function declaration expects all definitions to have the same name, " 
+					    ^ id_to_string id ^ " differs from other definitions of " ^ id')
+			| None -> Some(id_to_string id)) funcls None) with
+    | Some id -> id 
+    | None -> raise (Reporting_basic.err_unreachable l "funcl list might be empty") in
   let in_env = Envmap.apply t_env id in 
-  let typ_params = match in_env with
-    | Some(Base( (params,u),Spec,constraints,eft,_)) -> params
-    | None -> [] in
+  let (typ_params,has_spec) = match in_env with
+    | Some(Base( (params,u),Spec,constraints,eft,_)) -> params,true
+    | _ -> [],false in
   let ret_t,param_t,tannot,t_param_env = match tannotopt with
     | Typ_annot_opt_aux(Typ_annot_opt_some(typq,typ),l') ->
       let (ids,_,constraints) = typq_to_params envs typq in
       let t = typ_to_t false false typ in
-      (*TODO add check that ids == typ_params*)
-      let t,constraints,_,t_param_env = subst typ_params true t constraints pure_e in
+      (*TODO add check that ids == typ_params when has_spec*)
+      let t,constraints,_,t_param_env = subst (if has_spec then typ_params else ids) true t constraints pure_e in
       let p_t = new_t () in
       let ef = new_e () in
       t,p_t,Base((ids,{t=Tfn(p_t,t,IP_none,ef)}),Emp_global,constraints,ef,nob),t_param_env in
@@ -1753,7 +1736,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
 	  check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env t_env', 
 			 merge_bounds b_env b_env',tp_env)) imp_param ret_t exp in
 	(*let _ = Printf.eprintf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in
-	let _ = Printf.eprintf "constraints were %s\n" (constraints_to_string (cs_p@cs_e)) in*)
+	let _ = Printf.eprintf "constraints were pattern: %s\n expression: %s\n" (constraints_to_string cs_p) (constraints_to_string cs_e) in*)
 	let cs = [CondCons(Fun l,cs_p,cs_e)] in
 	(FCL_aux((FCL_Funcl(id,pat',exp')),(l,(Base(([],ret_t),Emp_global,cs,ef,nob)))),(cs,ef))) funcls) in
   let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),annot)) = 
@@ -1832,13 +1815,13 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
 		  let tannot = Base(([],et),Alias,[],pure_e,nob) in
 		  let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in
 		  (AL_aux(AL_subreg(reg_a,subreg),(l,tannot)),tannot,d_env)))
-	| _ -> let _ = Printf.eprintf "%s\n" (t_to_string reg_t) in assert false)
+	| _ -> typ_error l ("Expected a register with fields, given " ^ (t_to_string reg_t)))
     | AL_bit(reg_a,bit) -> 
       let (reg,reg_a,reg_t,t) = check_reg reg_a in
       let (E_aux(bit,(le,eannot)),_,_,_,_,_) = check_exp envs None (new_t ()) bit in
       (match t.t with
 	| Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) ->
-	  match (base.nexp,len.nexp,order.order, bit) with
+	  (match (base.nexp,len.nexp,order.order, bit) with
 	    | (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll))) ->
 	      if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k 
 	      then let tannot = Base(([],item_t),Alias,[],pure_e,nob) in
@@ -1846,14 +1829,15 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
 		     {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in
 		   (AL_aux(AL_bit(reg_a,(E_aux(bit,(le,eannot)))), (l,tannot)), tannot,d_env)
 	      else typ_error ll ("Alias bit lookup must be in the range of the vector in the register")
-	    | _ -> assert false)
+	    | _ -> typ_error l ("Alias bit lookup must have a constant index"))
+	| _ -> typ_error l ("Alias bit lookup must refer to a register with type vector, found " ^ (t_to_string t)))
     | AL_slice(reg_a,sl1,sl2) -> 
       let (reg,reg_a,reg_t,t) = check_reg reg_a in 
       let (E_aux(sl1,(le1,eannot1)),_,_,_,_,_) = check_exp envs None (new_t ()) sl1 in
       let (E_aux(sl2,(le2,eannot2)),_,_,_,_,_) = check_exp envs None (new_t ()) sl2 in
       (match t.t with
 	| Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) ->
-	  match (base.nexp,len.nexp,order.order, sl1,sl2) with
+	  (match (base.nexp,len.nexp,order.order, sl1,sl2) with
 	    | (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll)),E_lit (L_aux((L_num k2), ll2))) ->
 	      if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k2 && k < k2 
 	      then let t = {t = Tapp("vector",[TA_nexp (int_to_nexp k);TA_nexp (int_to_nexp ((k2-k) +1));
@@ -1864,7 +1848,8 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
 		   (AL_aux(AL_slice(reg_a,(E_aux(sl1,(le1,eannot1))),(E_aux(sl2,(le2,eannot2)))),
 			   (l,tannot)), tannot,d_env)
 	      else typ_error ll ("Alias slices must be in the range of the vector in the register")
-	    | _ -> assert false)
+	    | _ -> typ_error l ("Alias slices must have constant slices"))
+	| _ -> typ_error l ("Alias slices must point to a register with a vector type: found " ^ (t_to_string t)))
     | AL_concat(reg1_a,reg2_a) -> 
       let (reg1,reg1_a,reg_t,t1) = check_reg reg1_a in
       let (reg2,reg2_a,reg_t,t2) = check_reg reg2_a in
@@ -1875,7 +1860,9 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
 	  let t = {t= Tapp("register",[TA_typ {t= Tapp("vector",[TA_nexp b1; TA_nexp {nexp = Nadd(r,r2)}; TA_ord {order = Oinc}; TA_typ item_t])}])} in
 	  let tannot = Base(([],t),Alias,[],pure_e,nob) in
 	  let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, TwoReg(reg1,reg2,tannot))} in
-	  (AL_aux (AL_concat(reg1_a,reg2_a), (l,tannot)), tannot, d_env))
+	  (AL_aux (AL_concat(reg1_a,reg2_a), (l,tannot)), tannot, d_env)
+	| _ -> typ_error l 
+	  ("Alias concatentaion must connect two registers with vector type, found " ^ t_to_string t1 ^ " and " ^ t_to_string t2))
 
 (*val check_def : envs -> tannot def -> (tannot def) envs_out*)
 let check_def envs def = 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index b1a7ec9f..af1d31c7 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -97,6 +97,7 @@ type nexp_range =
   | GtEq of constraint_origin * range_enforcement * nexp * nexp
   | In of constraint_origin * string * int list
   | InS of constraint_origin * nexp * int list (* This holds the given value for string after a substitution *)
+  | Predicate of constraint_origin * nexp_range (* This will treat the inner constraint as holding in positive condcons positions*)
   | CondCons of constraint_origin * nexp_range list * nexp_range list
   | BranchCons of constraint_origin * nexp_range list
 
@@ -162,10 +163,10 @@ let get_c_loc = function
 let debug_mode = ref true;;
 
 let co_to_string = function
-  | Patt l -> "Pattern " 
-  | Expr l -> "Expression " 
-  | Fun l -> "Function def " 
-  | Specc l -> "Specification " 
+  | Patt l -> "Pattern " (*^ Reporting_basic.loc_to_string l *)
+  | Expr l -> "Expression " (*^ Reporting_basic.loc_to_string l *)
+  | Fun l -> "Function def " (*^ Reporting_basic.loc_to_string l *)
+  | Specc l -> "Specification " (*^ Reporting_basic.loc_to_string l *)
 
 let rec t_to_string t = 
   match t.t with
@@ -194,6 +195,7 @@ and n_to_string n =
     | Nconst i -> string_of_big_int i
     | Npos_inf -> "infinity"
     | Nneg_inf -> "-infinity"
+    | Ninexact -> "infinity - infinity"
     | Nadd(n1,n2) -> "("^ (n_to_string n1) ^ " + " ^ (n_to_string n2) ^")"
     | Nsub(n1,n2) -> "("^ (n_to_string n1) ^ " - " ^ (n_to_string n2) ^ ")"
     | Nmult(n1,n2) -> "(" ^ (n_to_string n1) ^ " * " ^ (n_to_string n2) ^ ")"
@@ -208,8 +210,11 @@ and ef_to_string (Ast.BE_aux(b,l)) =
       | Ast.BE_wreg  -> "wreg"
       | Ast.BE_rmem  -> "rmem"
       | Ast.BE_wmem  -> "wmem"
+      | Ast.BE_wmv   -> "wmv"
+      | Ast.BE_eamem -> "eamem"
       | Ast.BE_barr  -> "barr"
       | Ast.BE_undef -> "undef"
+      | Ast.BE_depend -> "depend"
       | Ast.BE_unspec-> "unspec"
       | Ast.BE_nondet-> "nondet"
 and efs_to_string es = 
@@ -253,6 +258,7 @@ let rec constraint_to_string = function
     "GtEq(" ^ co_to_string co ^ ", " ^ enforce_to_string enforce ^ ", " ^ n_to_string nexp1 ^ ", " ^ n_to_string nexp2 ^ ")"
   | In(co,var,ints) -> "In of " ^ var
   | InS(co,n,ints) -> "InS of " ^ n_to_string n
+  | Predicate(co,cs) -> "Pred(" ^ co_to_string co ^ ", " ^ constraint_to_string cs ^ ")"
   | CondCons(co,pats,exps) ->
     "CondCons(" ^ co_to_string co ^ ", [" ^ constraints_to_string pats ^ "], [" ^ constraints_to_string exps ^ "])"
   | BranchCons(co,consts) ->
@@ -372,6 +378,8 @@ let rec compare_nexps n1 n2 =
     (match compare_nexps n1 n2 with
       | 0 -> compare_nexps n12 n22
       | a -> a)
+  | Nsub _   , _         -> -1
+  | _        , Nsub _    -> 1
   | Npow(n1,_),Npow(n2,_)-> compare_nexps n1 n2
   | Npow _   , _        -> -1
   | _        , Npow _   ->  1
@@ -383,6 +391,9 @@ let rec compare_nexps n1 n2 =
   | Nneg _   , _        -> -1
   | _        , Nneg _   -> 1
   | Npos_inf , Npos_inf -> 0
+  | Npos_inf , _        -> -1
+  | _        , Npos_inf -> 1
+  | Ninexact , Ninexact -> 0
 
 
 let rec pow_i i n =
@@ -394,7 +405,7 @@ let two_pow = pow_i 2
 (* predicate to determine if pushing a constant in for addition or multiplication could change the form *)
 let rec contains_const n =
   match n.nexp with
-  | Nvar _ | Nuvar _ | Npow _ | N2n _ | Npos_inf | Nneg_inf -> false
+  | Nvar _ | Nuvar _ | Npow _ | N2n _ | Npos_inf | Nneg_inf | Ninexact -> false
   | Nconst _ -> true
   | Nneg n -> contains_const n
   | Nmult(n1,n2) | Nadd(n1,n2) | Nsub(n1,n2) -> (contains_const n1) || (contains_const n2)
@@ -446,7 +457,7 @@ let negate n = match n.nexp with
 let rec normalize_nexp n =
   (*let _ = Printf.eprintf "Working on normalizing %s\n" (n_to_string n) in *)
   match n.nexp with
-  | Nconst _ | Nvar _ | Nuvar _ | Npos_inf | Nneg_inf -> n
+  | Nconst _ | Nvar _ | Nuvar _ | Npos_inf | Nneg_inf | Ninexact -> n
   | Nneg n -> 
     let n',to_recur,add_neg = (match n.nexp with
       | Nconst i -> negate n,false,false
@@ -579,8 +590,13 @@ let rec normalize_nexp n =
     let n1',n2' = normalize_nexp n1, normalize_nexp n2 in
     (match n1'.nexp,n2'.nexp with
     | Nneg_inf,Nneg_inf -> {nexp = Npos_inf}
+    | Npos_inf, Nconst i | Nconst i, Npos_inf ->
+      if eq_big_int i zero then n_zero else {nexp = Npos_inf}
+    | Nneg_inf, Nconst i | Nconst i, Nneg_inf ->
+      if eq_big_int i zero then n_zero else {nexp = Nneg_inf}
     | Nneg_inf, _ | _, Nneg_inf -> {nexp = Nneg_inf} (*TODO write a is_negative predicate*)
     | Npos_inf, _ | _, Npos_inf -> {nexp = Npos_inf}
+    | Ninexact, _ | _, Ninexact -> {nexp = Ninexact}
     | Nconst i1, Nconst i2 -> mk_c (mult_big_int i1 i2)
     | Nconst i1, N2n(n,Some i2) | N2n(n,Some i2),Nconst i1 ->
       if eq_big_int i1 two 
@@ -650,6 +666,8 @@ let rec normalize_nexp n =
 	    | _ -> mk_mult n2' n1')
 	| _ -> mk_mult (normalize_nexp (mk_mult n1' n21)) n22)
     | Nmult _ ,Nmult(n21,n22) -> mk_mult (mk_mult n21 n1') (mk_mult n22 n1')
+    | Nsub _, _ | _, Nsub _ -> 
+      let _ = Printf.eprintf "nsub case still around %s\n" (n_to_string n) in assert false 
     | Nneg _,_ | _,Nneg _ -> 
       let _ = Printf.eprintf "neg case still around %s\n" (n_to_string n) in assert false
     (* If things are normal, neg should be gone. *)
@@ -852,7 +870,7 @@ and occurs_in_nexp n_box nuvar : bool =
 let rec reduce_n_unifications n = 
   (*let _ = Printf.eprintf "reduce_n_unifications %s\n" (n_to_string n) in*)
   (match n.nexp with
-    | Nvar _ | Nconst _ | Npos_inf | Nneg_inf -> ()
+    | Nvar _ | Nconst _ | Npos_inf | Nneg_inf | Ninexact-> ()
     | N2n(n1,_) | Npow(n1,_) | Nneg n1 -> reduce_n_unifications n1
     | Nadd(n1,n2) | Nsub(n1,n2) | Nmult(n1,n2) -> reduce_n_unifications n1; reduce_n_unifications n2
     | Nuvar nu ->
@@ -884,7 +902,7 @@ let equate_n (n_box : nexp) (n : nexp) : bool =
 	  | Some({nexp = Nuvar(u)}) -> set_bottom_nsubst swap u new_bot
 	  | Some(n_new) -> 
 	    if swap 
-	    then set_bottom_nsubst false (match new_bot.nexp with | Nuvar u -> u) n_new
+	    then set_bottom_nsubst false (match new_bot.nexp with | Nuvar u -> u | _ -> assert false) n_new
 	    else if nexp_eq n_new new_bot then true
 	    else false in
       match n_box.nexp,n.nexp with
@@ -1004,6 +1022,11 @@ let rec contains_nuvar n cs = match cs with
     (match contains_nuvar n b_cs with
       | [] -> contains_nuvar n cs
       | b -> BranchCons(so,b)::contains_nuvar n cs)
+  | (Predicate(so,c) as co)::cs ->
+    (match contains_nuvar n [c] with
+      | [] -> contains_nuvar n cs
+      | [c] -> co::contains_nuvar n cs
+      | _ -> assert false)
   | _::cs -> contains_nuvar n cs
 
 let rec refine_guarantees max_lt min_gt id cs =
@@ -1790,7 +1813,7 @@ and n_subst s_env n =
       | Some(TA_nexp n1) -> n1
       | _ -> mk_nv i)
   | Nuvar _ -> new_n()
-  | Nconst _ | Npos_inf | Nneg_inf -> n
+  | Nconst _ | Npos_inf | Nneg_inf | Ninexact -> n
   | N2n(n1,None) -> mk_2n (n_subst s_env n1) 
   | N2n(n1,Some(i)) -> n
   | Npow(n1,i) -> mk_pow (n_subst s_env n1) i
@@ -1826,6 +1849,7 @@ let rec cs_subst t_env cs =
       | _ -> ()); 
       InS(l,nexp,ns)::(cs_subst t_env cs)
     | InS(l,n,ns)::cs -> InS(l,n_subst t_env n,ns)::(cs_subst t_env cs)
+    | Predicate(l, c)::cs -> Predicate(l, List.hd(cs_subst t_env [c]))::(cs_subst t_env cs)
     | CondCons(l,cs_p,cs_e)::cs -> CondCons(l,cs_subst t_env cs_p,cs_subst t_env cs_e)::(cs_subst t_env cs)
     | BranchCons(l,bs)::cs -> BranchCons(l,cs_subst t_env bs)::(cs_subst t_env cs)
 
@@ -1888,7 +1912,7 @@ and ta_remove_unifications s_env ta =
 and n_remove_unifications s_env n =
   (*let _ = Printf.eprintf "n_remove_unifications %s\n" (n_to_string n) in*)
   match n.nexp with
-  | Nvar _ | Nconst _ | Npos_inf | Nneg_inf -> s_env
+  | Nvar _ | Nconst _ | Npos_inf | Nneg_inf | Ninexact -> s_env
   | Nuvar nu -> 
     let n' = match nu.nsubst with
       | None -> n
@@ -1952,6 +1976,7 @@ and n_to_nexp n =
     | Nconst i -> Nexp_constant (int_of_big_int i) (*TODO: Push more bigint around*) 
     | Npos_inf -> Nexp_constant max_int (*TODO: Not right*)
     | Nneg_inf -> Nexp_constant min_int (* see above *)
+    | Ninexact -> Nexp_constant min_int (*and above*)
     | Nmult(n1,n2) -> Nexp_times(n_to_nexp n1,n_to_nexp n2) 
     | Nadd(n1,n2) -> Nexp_sum(n_to_nexp n1,n_to_nexp n2) 
     | Nsub(n1,n2) -> Nexp_minus(n_to_nexp n1,n_to_nexp n2)
@@ -2021,6 +2046,12 @@ let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) =
   | (BE_wmem,BE_wmem) -> 0
   | (BE_wmem,_) -> -1
   | (_,BE_wmem) -> 1
+  | (BE_wmv,BE_wmv) -> 0
+  | (BE_wmv, _ ) -> -1
+  | (_,BE_wmv) -> 1
+  | (BE_eamem,BE_eamem) -> 0
+  | (BE_eamem,_) -> -1
+  | (_,BE_eamem) -> 1
   | (BE_barr,BE_barr) -> 0
   | (BE_barr,_) -> 1
   | (_,BE_barr) -> -1
@@ -2031,6 +2062,9 @@ let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) =
   | (BE_unspec,_) -> -1
   | (_,BE_unspec) -> 1
   | (BE_nondet,BE_nondet) -> 0
+  | (BE_nondet,_) -> -1
+  | (_,BE_nondet) -> 1
+  | (BE_depend,BE_depend) -> 0
 
 let effect_sort = List.sort compare_effect
 
@@ -2128,7 +2162,7 @@ let merge_bounds b1 b2 =
 	  match compare_variable_range b1 b2 with
 	    | -1 -> b1::(merge b1s (b2::b2s))
 	    | 1  -> b2::(merge (b1::b1s) b2s)
-	    | 0  -> (match b1,b2 with
+	    | _  -> (match b1,b2 with
 		| VR_eq(v,n1),VR_eq(_,n2) -> 
 		  if nexp_eq n1 n2 then b1 else VR_range(v,[Eq((Patt Unknown),n1,n2)])
 		| VR_eq(v,n),VR_range(_,ranges) | 
@@ -2182,7 +2216,7 @@ and conforms_to_ta d_env loosely within_coercion spec actual =
     | TA_eft  s, TA_eft  a -> conforms_to_e loosely s a
     | _ -> false
 and conforms_to_n loosely within_coercion op spec actual =
-(*  let _ = Printf.printf "conforms_to_n called, evaluated loosely? %b, with coercion? %b with %s and %s\n" 
+(*  let _ = Printf.eprintf "conforms_to_n called, evaluated loosely? %b, with coercion? %b with %s and %s\n" 
     loosely within_coercion (n_to_string spec) (n_to_string actual) in*)
   match (spec.nexp,actual.nexp,loosely,within_coercion) with
     | (Nconst si,Nconst ai,_,_) -> op si ai
@@ -2236,9 +2270,13 @@ let rec type_consistent_internal co d_env enforce widen t1 cs1 t2 cs2 =
 	if i1 < i2 
 	then ({t= Tapp("range",[TA_nexp a1;TA_nexp a2])},csp)
 	else ({t=Tapp ("range",[TA_nexp a2;TA_nexp a1])},csp)
+      (*| Nconst _, Nuvar _ | Nuvar _, Nconst _->
+	(t1, csp@[Eq(co,a1,a2)])*) (*TODO This is the correct constraint. However, without the proper support for In checks actually working, this will cause specs to not build*)	
       | _ -> let nu1,nu2 = new_n (),new_n () in 
 	     ({t=Tapp("range",[TA_nexp nu1;TA_nexp nu2])},
 	      csp@[LtEq(co,enforce,nu1,a1);LtEq(co,enforce,nu1,a2);LtEq(co,enforce,a1,nu2);LtEq(co,enforce,a2,nu2)]))
+  | Tapp("vector",[TA_nexp _; TA_nexp l1; ord; ty1]),Tapp("vector",[TA_nexp _; TA_nexp l2; ord2; ty2]) ->
+    (t2, Eq(co,l1,l2)::((type_arg_eq co d_env enforce widen ord ord2)@(type_arg_eq co d_env enforce widen ty1 ty2)))
   | Tapp(id1,args1), Tapp(id2,args2) ->
     (*let _ = Printf.eprintf "checking consistency of %s and %s\n" id1 id2 in*)
     let la1,la2 = List.length args1, List.length args2 in
@@ -2543,7 +2581,7 @@ let rec in_constraint_env = function
 let rec contains_var nu n =
   match n.nexp with
   | Nvar _ | Nuvar _ -> nexp_eq_check nu n
-  | Nconst _ | Npos_inf | Nneg_inf -> false
+  | Nconst _ | Npos_inf | Nneg_inf | Ninexact -> false
   | Nadd(n1,n2) | Nsub(n1,n2) | Nmult(n1,n2) -> contains_var nu n1 || contains_var nu n2
   | Nneg n | N2n(n,_) | Npow(n,_) -> contains_var nu n
 
@@ -2557,7 +2595,7 @@ let rec contains_in_vars in_env n =
 
 let rec subst_nuvars nu nc n =
   match n.nexp with
-  | Nconst _ | Nvar _ | Npos_inf | Nneg_inf -> n
+  | Nconst _ | Nvar _ | Npos_inf | Nneg_inf | Ninexact -> n
   | Nuvar _ -> if nexp_eq_check nu n then nc else n
   | Nmult(n1,n2) -> {nexp=Nmult(subst_nuvars nu nc n1,subst_nuvars nu nc n2)}
   | Nadd(n1,n2) -> {nexp=Nadd(subst_nuvars nu nc n1,subst_nuvars nu nc n2)}
@@ -2568,7 +2606,7 @@ let rec subst_nuvars nu nc n =
 
 let rec get_nuvars n =
   match n.nexp with
-    | Nconst _ | Nvar _ | Npos_inf | Nneg_inf -> []
+    | Nconst _ | Nvar _ | Npos_inf | Nneg_inf | Ninexact-> []
     | Nuvar _ -> [n]
     | Nmult(n1,n2) | Nadd(n1,n2) | Nsub(n1,n2) -> (get_nuvars n1)@(get_nuvars n2)
     | Nneg n | N2n(n,_) | Npow(n,_) -> get_nuvars n
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 7e786779..af2b99e0 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -97,6 +97,7 @@ type nexp_range =
   | GtEq of constraint_origin * range_enforcement * nexp * nexp
   | In of constraint_origin * string * int list
   | InS of constraint_origin * nexp * int list (* This holds the given value for string after a substitution *)
+  | Predicate of constraint_origin * nexp_range (* This will treat the inner constraint as holding in positive condcons positions : must be one of LtEq, Eq, or GtEq*)
   | CondCons of constraint_origin * nexp_range list * nexp_range list (* Constraints from one path from a conditional (pattern or if) and the constraints from that conditional *)
   | BranchCons of constraint_origin * nexp_range list (* CondCons constraints from all branches of a conditional; list should be all CondCons *)