Actually use new dependency information in generation of lem/etc.

Also stop rewriting code in the pretty printer, instead move it all into a new general rewriting pass

9 files changed, 238 insertions, 32 deletions

diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index cd754786..a622cd3a 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -416,7 +416,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
     | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_let" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_exit exp -> fprintf ppf "@[<0>(E_aux (E_exit %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
-    | E_internal_exp (l, Base((_,t),_,_,_,bindings)) ->
+    | E_internal_exp ((l, Base((_,t),_,_,_,bindings))) ->
       (*TODO use bindings where appropriate*)
       (match t.t with
 	| Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}])
@@ -975,7 +975,7 @@ let doc_exp, doc_let =
   | E_app_infix(l,op,r) ->
       failwith ("unexpected app_infix operator " ^ (pp_format_id op))
       (* doc_op (doc_id op) (exp l) (exp r) *)
-  | E_internal_exp (l, Base((_,t),_,_,_,bindings)) -> (*TODO use bindings*)
+  | E_internal_exp((l, Base((_,t),_,_,_,bindings))) -> (*TODO use bindings, and other params*)
     (match t.t with
       | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}])
       | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) ->
diff --git a/src/process_file.ml b/src/process_file.ml
index 7caf5172..21c6c542 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -100,6 +100,8 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.
 		                                     | (Ast.Ord_aux(Ast.Ord_dec,_)) -> Type_internal.Odec)};} in
   Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env,Type_internal.nob)) defs 
 
+let rewrite_ast (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs defs
+
 let open_output_with_check file_name =
   let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
   let o' = Format.formatter_of_out_channel o in
diff --git a/src/process_file.mli b/src/process_file.mli
index 29c6cb55..97b1ba46 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -47,6 +47,7 @@
 val parse_file : string -> Parse_ast.defs
 val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs * Type_internal.kind Type_internal.Envmap.t * Ast.order
 val check_ast: Type_internal.tannot Ast.defs -> Type_internal.kind Type_internal.Envmap.t -> Ast.order -> Type_internal.tannot Ast.defs
+val rewrite_ast: Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 
 type out_type =
   | Lem_ast_out
diff --git a/src/rewriter.ml b/src/rewriter.ml
new file mode 100644
index 00000000..6a78ba71
--- /dev/null
+++ b/src/rewriter.ml
@@ -0,0 +1,165 @@
+open Big_int
+open Ast
+open Type_internal
+type typ = Type_internal.t
+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
+  | [] -> None
+  | (v1,v2)::ls -> if v1 = v then Some v2 else partial_assoc 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 "mult"))))
+    | 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 ev -> E_aux (E_id (Id_aux (Id ev,l)), (l, simple_annot typ)))
+
+let rec match_to_program_vars vs bounds =
+  match vs with
+    | [] -> []
+    | v::vs -> match find_var_from_nvar v bounds with
+	| None -> match_to_program_vars vs bounds
+	| Some ev -> (v,ev)::(match_to_program_vars vs bounds)
+
+let rec rewrite_exp (E_aux (exp,(l,annot))) = 
+  let rewrap e = E_aux (e,(l,annot)) in
+  match exp with
+    | E_block exps -> rewrap (E_block (List.map rewrite_exp exps))
+    | E_nondet exps -> rewrap (E_nondet (List.map rewrite_exp exps))
+    | E_id _ | E_lit _  -> rewrap exp
+    | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite_exp exp))
+    | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite_exp exps))
+    | E_app_infix(el,id,er) -> rewrap (E_app_infix(rewrite_exp el,id,rewrite_exp er))
+    | E_tuple exps -> rewrap (E_tuple (List.map rewrite_exp exps))
+    | E_if (c,t,e) -> rewrap (E_if (rewrite_exp c,rewrite_exp t, rewrite_exp e))
+    | E_for (id, e1, e2, e3, o, body) ->
+      rewrap (E_for (id, rewrite_exp e1, rewrite_exp e2, rewrite_exp e3, o, rewrite_exp body))
+    | E_vector exps -> rewrap (E_vector (List.map rewrite_exp exps))
+    | E_vector_indexed (exps,(Def_val_aux(default,dannot))) ->
+      let def = match default with
+	| Def_val_empty -> default
+	| Def_val_dec e -> Def_val_dec (rewrite_exp e) in
+      rewrap (E_vector_indexed (List.map (fun (i,e) -> (i, rewrite_exp e)) exps, Def_val_aux(def,dannot)))
+    | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite_exp vec,rewrite_exp index))
+    | E_vector_subrange (vec,i1,i2) ->
+      rewrap (E_vector_subrange (rewrite_exp vec,rewrite_exp i1,rewrite_exp i2))
+    | E_vector_update (vec,index,new_v) -> 
+      rewrap (E_vector_update (rewrite_exp vec,rewrite_exp index,rewrite_exp new_v))
+    | E_vector_update_subrange (vec,i1,i2,new_v) ->
+      rewrap (E_vector_update_subrange (rewrite_exp vec,rewrite_exp i1,rewrite_exp i2,rewrite_exp new_v))
+    | E_vector_append (v1,v2) -> rewrap (E_vector_append (rewrite_exp v1,rewrite_exp v2))
+    | E_list exps -> rewrap (E_list (List.map rewrite_exp exps)) 
+    | E_cons(h,t) -> rewrap (E_cons (rewrite_exp h,rewrite_exp t))
+    | E_record (FES_aux (FES_Fexps(fexps, bool),fannot)) -> 
+      rewrap (E_record 
+		(FES_aux (FES_Fexps 
+			    (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> 
+			      FE_aux(FE_Fexp(id,rewrite_exp e),fannot)) fexps, bool), fannot)))
+    | E_record_update (re,(FES_aux (FES_Fexps(fexps, bool),fannot))) ->
+      rewrap (E_record_update ((rewrite_exp re),
+			       (FES_aux (FES_Fexps 
+					   (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> 
+					     FE_aux(FE_Fexp(id,rewrite_exp e),fannot)) fexps, bool), fannot))))
+    | E_field(exp,id) -> rewrap (E_field(rewrite_exp exp,id))
+    | E_case (exp ,pexps) -> 
+      rewrap (E_case (rewrite_exp exp,
+		      (List.map 
+			 (fun (Pat_aux (Pat_exp(p,e),pannot)) -> 
+			   Pat_aux (Pat_exp(p,rewrite_exp e),pannot)) pexps)))
+    | E_let (letbind,body) -> rewrap (E_let(rewrite_let letbind,rewrite_exp body))
+    | E_assign (lexp,exp) -> rewrap (E_assign(rewrite_lexp lexp,rewrite_exp exp))
+    | E_exit e -> rewrap (E_exit (rewrite_exp e))
+    | 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*)
+	    | Tapp("vector",[TA_nexp n1;_;_;_]),Tapp("vector",[TA_nexp n2;_;_;_]) ->
+	      if nexp_eq n1 n2 
+	      then new_exp
+	      else (match n1.nexp with
+		| Nconst i1 -> rewrap (E_cast (t_to_typ t,new_exp))
+		| _ -> new_exp)
+	    | _ -> new_exp))
+    | E_internal_exp (l,impl) ->
+      (match impl with
+	| Base((_,t),_,_,_,bounds) ->
+	  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;_;_]) ->
+	      (match r.nexp with
+		| Nconst bi -> rewrap (E_lit (L_aux (L_num (Big_int.int_of_big_int bi),l)))
+		| Nvar v -> rewrap (E_id (Id_aux (Id v,l))))
+	    | Tapp("implicit", [TA_nexp i]) ->
+	      let vars = get_all_nvar i in
+	      (match vars with
+		| [] -> rewrite_nexp_to_exp None l i
+		| vars -> rewrite_nexp_to_exp (Some (match_to_program_vars vars bounds)) l i))
+    | E_internal_exp_user (user_spec,impl) -> assert false
+
+and rewrite_let (LB_aux(letbind,(l,annot))) = match letbind with
+  | LB_val_explicit (typschm, pat,exp) ->
+    LB_aux(LB_val_explicit (typschm,pat, rewrite_exp exp),(l,annot))
+  | LB_val_implicit ( pat, exp) ->
+    LB_aux(LB_val_implicit (pat,rewrite_exp exp),(l,annot))
+
+and rewrite_lexp (LEXP_aux(lexp,(l,annot))) = 
+  let rewrap le = LEXP_aux(le,(l,annot)) in
+  match lexp with
+  | LEXP_id _ | LEXP_cast _ -> rewrap lexp
+  | LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map rewrite_exp exps))
+  | LEXP_vector (lexp,exp) -> rewrap (LEXP_vector (rewrite_lexp lexp,rewrite_exp exp))
+  | LEXP_vector_range (lexp,exp1,exp2) -> 
+    rewrap (LEXP_vector_range (rewrite_lexp lexp,rewrite_exp exp1,rewrite_exp exp2))
+  | LEXP_field (lexp,id) -> rewrap (LEXP_field (rewrite_lexp lexp,id))
+
+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))) = 
+    (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))
+
+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)
+
+let rewrite_defs (Defs defs) = 
+  let rec rewrite ds = match ds with
+    | [] -> []
+    | d::ds -> (rewrite_def d)::(rewrite ds) in
+  Defs (rewrite defs)
diff --git a/src/rewriter.mli b/src/rewriter.mli
new file mode 100644
index 00000000..3e81952d
--- /dev/null
+++ b/src/rewriter.mli
@@ -0,0 +1,10 @@
+open Big_int
+open Ast
+open Type_internal
+type typ = Type_internal.t
+type 'a exp = 'a Ast.exp
+type 'a emap = 'a Envmap.t
+type envs = Type_check.envs
+
+val rewrite_exp : tannot exp -> tannot exp
+val rewrite_defs : tannot defs -> tannot defs
diff --git a/src/sail.ml b/src/sail.ml
index 2e91d0b3..fbc339f0 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -395,18 +395,19 @@ let main() =
   if !(opt_print_version)
   then Printf.printf "L2 private release \n"
   else let parsed = (List.map (fun f -> (f,(parse_file f)))  !opt_file_arguments) in
-       let merged_asts = 
+       let ast = 
 	 List.fold_right (fun (_,(Parse_ast.Defs ast_nodes)) (Parse_ast.Defs later_nodes) 
 	 -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
-       let (ast,kenv,ord) = convert_ast merged_asts in
-       let chkedast = check_ast ast kenv ord in 
+       let (ast,kenv,ord) = convert_ast ast in
+       let ast = check_ast ast kenv ord in 
+       let ast = rewrite_ast ast in
        (*let _ = Printf.eprintf "Type checked, next to pretty print" in*)
        begin 
 	 (if !(opt_print_verbose)
-	  then ((Pretty_print.pp_defs stdout) chkedast)
+	  then ((Pretty_print.pp_defs stdout) ast)
 	  else ());
 	 (if !(opt_print_lem)
-	  then output "" Lem_ast_out [(fst (List.hd parsed)),chkedast]
+	  then output "" Lem_ast_out [(fst (List.hd parsed)),ast]
 	  else ());
        end
 
diff --git a/src/type_check.ml b/src/type_check.ml
index d4739543..6d652796 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -532,11 +532,13 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
             else typ_error l ("Expected bool or a bit, found " ^ string_of_int i)
           | Tapp ("vector",[TA_nexp base;TA_nexp rise;TA_ord o;(TA_typ {t=Tid "bit"})]) ->
             let n = {nexp = Nconst (big_int_of_int i) } in
-            let t = {t=Tapp("range", [TA_nexp n;TA_nexp {nexp = Nconst zero};])} in
+            let t = {t=Tapp("atom", [TA_nexp n;])} in
             let cs = [LtEq(Expr l,n,{nexp = N2n(rise,None)})] in
-            let f = match o.order with | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec" | _ -> "to_vec_inc" (*Change to follow a default?*) in
+            let f = match o.order with | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec" | _ -> "to_vec_inc" 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)),[(E_aux (E_internal_exp tannot, tannot));simp_exp e l t]),tannot),cs,pure_e
+            E_aux(E_app((Id_aux((Id f),l)),
+			[(E_aux (E_internal_exp(internal_tannot), tannot));simp_exp e l t]),tannot),cs,pure_e
           | _ -> simp_exp e l {t = Tapp("atom", [TA_nexp{nexp = Nconst (big_int_of_int i)}])},[],pure_e)
 	| L_hex s -> simp_exp e l {t = Tapp("vector",
 			                    [TA_nexp{nexp = Nconst zero};
@@ -555,7 +557,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 							  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
-              E_aux(E_app((Id_aux((Id f),l)),[(E_aux (E_internal_exp tannot, tannot));simp_exp e l bit_t]),tannot),[],ef
+              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 false true (get_e_typ e) e expect_t in
       (e',t',t_env,cs@cs',nob,effect)
@@ -590,35 +593,44 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	match (imp,imp_param) with
 	  | (IP_length n ,None) | (IP_user n,None) | (IP_start n,None) ->
 	    (*let _ = Printf.printf "implicit length or var required, no imp_param\n!" in*)
-	    (*let internal_exp = 
-	      let internal_typ = {t= Toptions(expect_t,Some ret)} in
-	      let annot = Base(([],internal_typ),Emp_local,[],pure_e,b_env) in
-	      E_aux(E_internal_exp(l,annot),(l,simple_annot nat_t)) in*)
-	    let internal_exp =  match expect_t.t,ret.t with 
+	    let internal_exp = 
+	      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
+	    (*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
+              | _ -> 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(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.printf "implicit length or var required with imp_param\n" in*)
-	    let internal_exp = (match expect_t.t,ret.t with
+	    (*let internal_exp = (match expect_t.t,ret.t with
 	      | Tapp("vector",[_;TA_nexp len;_;_]),_ ->
 		if nexp_eq ne len 
 		(*TODO This shouldn't be nat_t but should be a range bounded by the length of the vector *)
-		then E_aux (E_internal_exp (l, simple_annot expect_t), (l, simple_annot nat_t)) 
-		else E_aux (E_internal_exp (l, simple_annot {t= Tapp("implicit",[TA_nexp ne])}), (l, simple_annot nat_t))
+		then E_aux (E_internal_exp((l, simple_annot expect_t),(l,NoTyp),(l,NoTyp)), (l, simple_annot nat_t)) 
+		else E_aux (E_internal_exp((l, simple_annot {t= Tapp("implicit",[TA_nexp ne])}),(l,NoTyp),(l,NoTyp)), (l, simple_annot nat_t))
 	      | _,Tapp("vector",[_;TA_nexp len;_;_]) -> 
 		if nexp_eq ne len 
 		then E_aux (E_internal_exp (l, simple_annot ret), (l, simple_annot nat_t)) 
 		else E_aux (E_internal_exp (l, simple_annot {t= Tapp("implicit",[TA_nexp ne])}),(l, simple_annot nat_t))
-	      | _ -> E_aux (E_internal_exp (l, simple_annot {t= Tapp("implicit",[TA_nexp ne])}),(l, simple_annot nat_t))) in
-	    type_coerce (Expr l) d_env false false ret (E_aux (E_app(id,internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t
+	      | _ -> E_aux (E_internal_exp (l, simple_annot {t= Tapp("implicit",[TA_nexp ne])}),(l, simple_annot nat_t)))*) 
+	    let internal_exp = 
+	      let implicit_user = {t = Tapp("implicit",[TA_nexp ne])} in
+	      let implicit = {t= Tapp("implicit",[TA_nexp n])} in
+	      let annot_iu = Base(([],implicit_user),Emp_local,[],pure_e,b_env)in
+	      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 false false 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 false false ret (E_aux (E_app(id, parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t 
+            type_coerce (Expr l) d_env false false ret 
+	      (E_aux (E_app(id, parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t
       in
       (match Envmap.apply t_env i with
       | Some(Base(tp,Enum,_,_,_)) ->
@@ -678,14 +690,14 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
         | _ -> raise (Reporting_basic.err_unreachable l "check exp given tuple and tuple type and returned non-tuple") in
       let check_result ret imp tag cs ef lft rht =
         match imp with
-	  | IP_length _ ->  
+	  (*| 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
+            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 false false ret (E_aux (E_app_infix(lft,op,rht),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t 
       in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index d93f8f99..15ed1dc4 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -350,7 +350,7 @@ let rec get_var n =
 
 let rec get_all_nvar n = 
   match n.nexp with
-    | Nvar _ | Nuvar _ -> [n]
+    | Nvar v -> [v]
     | Nneg n | N2n(n,_) | Npow(n,_) -> get_all_nvar n
     | Nmult(n1,n2) | Nadd(n1,n2) -> (get_all_nvar n1)@(get_all_nvar n2)
     | _ -> []
@@ -1785,7 +1785,8 @@ let build_variable_range d_env v typ =
     | Tuvar _ -> Some(VR_recheck(v,t_actual))
     | _ -> None
 
-let get_vr_var = function | VR_eq (v,_) | VR_range(v,_) -> v | VR_vec_eq(v,_) -> v | VR_vec_r(v,_) -> v | VR_recheck(v,_) -> v
+let get_vr_var = 
+  function | VR_eq (v,_) | VR_range(v,_) | VR_vec_eq(v,_) | VR_vec_r(v,_) | VR_recheck(v,_) -> v
 
 let compare_variable_range v1 v2 = compare (get_vr_var v1) (get_vr_var v2)
 
@@ -1802,6 +1803,19 @@ 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) | VR_vec_eq (ev,n)->
+	    (match n.nexp with 
+	      | Nvar nv -> if nv = v then Some ev else find_rec bs
+	      | _ -> find_rec bs)
+	  | _ -> find_rec bs) in
+    find_rec bs
+
 let merge_bounds b1 b2 =
   match b1,b2 with
     | No_bounds,b | b,No_bounds -> b
@@ -2069,13 +2083,13 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 =
 	let cs = [LtEq(co,r2,{nexp=N2n(r1,None)})] in
 	let tannot = (l,Base(([],t2),External None, cs,pure_e,nob)) 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))
+				  [(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 = [LtEq(co,r2,{nexp=N2n(r1,None)})] in
 	let tannot = (l,Base(([],t2),External None,cs,pure_e,nob)) 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))
+				  [(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"}],_ -> 
 	eq_error l "Cannot convert a range to a vector without an order"
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
@@ -2088,13 +2102,13 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 =
 	let cs = [LtEq(co,b2,{nexp=N2n(r1,None)})] in
 	let tannot = (l,Base(([],t2),External None, cs,pure_e,nob)) 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))
+				  [(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,b2,{nexp=N2n(r1,None)})] in
 	let tannot = (l,Base(([],t2),External None,cs,pure_e,nob)) 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))
+				  [(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"}],_ -> 
 	eq_error l "Cannot convert a range to a vector without an order"
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
diff --git a/src/type_internal.mli b/src/type_internal.mli
index aa2453ec..d6cecdf5 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -183,10 +183,11 @@ 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
 
 val normalize_nexp : nexp -> nexp
 val get_index : nexp -> int (*TEMPORARILY expose nindex through this for debugging purposes*)
-val get_all_nvar : nexp -> nexp list (*Pull out all of the contained nvar and nuvars in nexp*)
+val get_all_nvar : nexp -> string list (*Pull out all of the contained nvar and nuvars in nexp*)
 
 val select_overload_variant : def_envs -> bool -> bool -> tannot list -> t -> tannot list