More type checking, including coercing 0 and 1 into bits when appropriate (in limited circumstances at the moment due to which expressions are actually checked, so test files should not yet be changed)

5 files changed, 282 insertions, 110 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index 29635f91..25fbe49b 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -92,9 +92,9 @@ let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind
 
 
 let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) : Type_internal.tannot Ast.defs =
-  let d_env = { Type_check.k_env = k; Type_check.abbrevs = Envmap.empty; 
-		Type_check.namesch = Envmap.empty; Type_check.enum_env = Envmap.empty; 
-		Type_check.rec_env = []; } in
+  let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env; 
+		Type_internal.namesch = Envmap.empty; Type_internal.enum_env = Envmap.empty; 
+		Type_internal.rec_env = []; } in
   Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env)) defs 
 
 let open_output_with_check file_name =
diff --git a/src/type_check.ml b/src/type_check.ml
index 8c4f4a44..3a8a6389 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -5,14 +5,6 @@ type typ = Type_internal.t
 type 'a exp = 'a Ast.exp
 type 'a emap = 'a Envmap.t
 
-type rec_kind = Record | Register
-type def_envs = { 
-  k_env: kind emap; 
-  abbrevs: tannot emap; 
-  namesch : tannot emap; 
-  enum_env : (string list) emap; 
-  rec_env : (string * rec_kind * ((string * tannot) list)) list;
- }
 type envs = Env of def_envs * tannot emap
 type 'a envs_out = 'a * envs
 
@@ -175,7 +167,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
 	  | L_true  -> {t = Tid "bool"}
 	  | L_false -> {t = Tid "bool"}
 	  | L_num i -> {t = Tapp("enum",
-				 [TA_nexp{nexp = Nconst i};TA_nexp{nexp= Nconst 0};TA_ord{order = Oinc}])}
+				 [TA_nexp{nexp = Nconst i};TA_nexp{nexp= Nconst 0};])}
 	  | L_hex s -> {t = Tapp("vector",
 				 [TA_nexp{nexp = Nconst 0};TA_nexp{nexp = Nconst ((String.length s)*4)};
 				  TA_ord{order = Oinc};TA_typ{t = Tid "bit"}])}
@@ -195,7 +187,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
     | P_typ(typ,pat) -> 
       let t = typ_to_t typ in
       let (pat',env,constraints,u) = check_pattern envs pat in
-      let (t',constraint') = type_consistent l u t in
+      let (t',constraint') = type_consistent l d_env u t in
       (P_aux(P_typ(typ,pat'),(l,Some(([],t'),Emp,constraint'@constraints))),env,constraints@constraint',t)
     | P_id id -> 
       let t = new_t () in
@@ -206,7 +198,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
       (match Envmap.apply t_env i with
 	| None | Some None -> typ_error l ("Constructor " ^ i ^ " in pattern is undefined")
 	| Some(Some((params,t),Constructor,constraints)) -> 
-          let t = subst params t in
+          let t,constraints = subst params t constraints in
 	  (match t.t with
 	    | Tid id -> if pats = [] then 
 		(P_aux(p,(l,Some((params,t),Constructor,constraints))),Envmap.empty,constraints,t)
@@ -214,7 +206,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
 	    | Tfn(t1,t2,ef) -> 
 	      let ((P_aux(P_tup(pats'),_)),env,constraints,u) = 
 		check_pattern envs (P_aux(P_tup(pats),(l,annot))) in
-	      let (t',constraint') = type_consistent l u t1 in
+	      let (t',constraint') = type_consistent l d_env u t1 in
 	      (P_aux(P_app(id,pats'),(l,Some((params,t2),Constructor,constraints))),env,constraints,t2)
 	    | _ -> typ_error l ("Identifier " ^ i ^ " is not bound to a constructor"))
 	| Some(Some((params,t),tag,constraints)) -> typ_error l ("Identifier " ^ i ^ " used in pattern is not a constructor"))
@@ -226,7 +218,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
 	    List.map (fun (tan,id,l,pat) -> 
 	      let (pat,env,constraints,u) = check_pattern envs pat in
 	      let (Some((vs,t),tag,cs)) = tan in
-	      let (t',cs') = type_consistent l u t in 
+	      let (t',cs') = type_consistent l d_env u t in 
 	      let pat = FP_aux(FP_Fpat(id,pat),(l,Some((vs,t'),tag,cs@cs'@constraints))) in
 	      (pat,env,cs@cs'@constraints)) typ_pats in
 	  let pats' = List.map (fun (a,b,c) -> a) pat_checks in
@@ -243,7 +235,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
 	    ((pat'::pats),(t::ts),(t_env::t_envs),(cons@constraints)))
 	  pats ([],[],[],[]) in
       let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*Need to check for non-duplication of variables*)
-      let (u,cs) = List.fold_right (fun u (t,cs) -> let t',cs = type_consistent l u t in t',cs) ts ((new_t ()),[]) in
+      let (u,cs) = List.fold_right (fun u (t,cs) -> let t',cs = type_consistent l d_env u t in t',cs) ts ((new_t ()),[]) in
       let t = {t = Tapp("vector",[(TA_nexp {nexp= Nconst 0});(TA_nexp {nexp= Nconst (List.length ts)});(TA_ord{order=Oinc});(TA_typ u)])} in
       (P_aux(P_vector(pats'),(l,Some(([],t),Emp,cs@constraints))), env,cs@constraints,t)
     | P_vector_indexed(ipats) -> 
@@ -269,7 +261,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
 	    (((i,pat')::pats),(t::ts),(env::t_envs),(cons@constraints)))
 	  ipats ([],[],[],[]) in
       let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*Need to check for non-duplication of variables*)
-      let (u,cs) = List.fold_right (fun u (t,cs) -> type_consistent l u t) ts (new_t (),[]) in
+      let (u,cs) = List.fold_right (fun u (t,cs) -> type_consistent l d_env u t) ts (new_t (),[]) in
       let t = {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise);
 				  (TA_ord{order=(if inc_or_dec then Oinc else Odec)});(TA_typ u)])} in
       let cs = if inc_or_dec 
@@ -300,7 +292,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
       let or_init = new_o () in
       let ts = List.map 
 	(fun t->let ti= { t = Tapp("vector",[TA_nexp(new_n ());TA_nexp(new_n ());TA_ord(or_init);TA_typ t_init])} in
-	 type_consistent l t ti) ts in
+	 type_consistent l d_env t ti) ts in
       let ts,cs = List.split ts in
       let base,rise = new_n (),new_n () in
       let t = {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise);(TA_ord or_init);(TA_typ t_init)])} in
@@ -322,7 +314,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
 	    (pat'::pats,t::ts,env::t_envs,cons@constraints))
 	  pats ([],[],[],[]) in
       let env = List.fold_right (fun e env -> Envmap.union e env) envs Envmap.empty in (*Need to check for non-duplication of variables*)
-      let u,cs = List.fold_right (fun u (t,cs) -> let t',cs' = type_consistent l u t in t',cs@cs') ts (new_t (),[]) in
+      let u,cs = List.fold_right (fun u (t,cs) -> let t',cs' = type_consistent l d_env u t in t',cs@cs') ts (new_t (),[]) in
       let t = {t = Tapp("list",[TA_typ u])} in
       (P_aux(P_list(pats'),(l,Some(([],t),Emp,constraints@cs))), env,constraints@cs,t)
       
@@ -339,15 +331,15 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       | Some(Some((params,t),Constructor,cs)) ->
         (match t.t with
         | Tfn({t = Tid "unit"},t',ef) -> 
-          let t' = subst params t' in
-          let t',cs',e' = type_coerce l t' (rebuild (Some((params,{t=Tfn(unit_t,t',ef)}),Constructor,cs))) expect_t in
+          let t',cs = subst params t' cs in
+          let t',cs',e' = type_coerce l d_env t' (rebuild (Some((params,{t=Tfn(unit_t,t',ef)}),Constructor,cs))) expect_t in
           (e',t',t_env,cs@cs')
         | Tfn(t1,t',e) -> 
           typ_error l ("Constructor " ^ i ^ " expects arguments of type INSERT TYPE PRINTER HERE, found none")
         | _ -> raise (Reporting_basic.err_unreachable l "Constructor tannot does not have function type"))
       | Some(Some((params,t),Enum,cs)) ->
-        let t' = subst params t in
-        let t',cs',e' = type_coerce l t' (rebuild (Some((params,t'),Enum,cs))) expect_t in
+        let t',cs = subst params t cs in
+        let t',cs',e' = type_coerce l d_env t' (rebuild (Some((params,t'),Enum,cs))) expect_t in
         (e',t',t_env,cs@cs')
       | Some(Some(tp,Default,cs)) | Some(Some(tp,Spec,cs)) ->
         typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use")
@@ -356,45 +348,54 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
         | Tfn _,_ -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is bound to a function and cannot be used as a value")
         | Tapp("register",[TA_typ(t')]),Tapp("register",[TA_typ(expect_t')]) -> 
           let tannot = Some((params,t),External,cs) in
-          let t' = subst params t' in
-          let t',cs',e' = type_coerce l t' (rebuild tannot) expect_t' in
+          let t',cs = subst params t' cs in
+          let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t' in
           (e',t',t_env,cs@cs')
         | Tapp("register",[TA_typ(t')]),_ ->
           let tannot = Some((params,t),External,cs) in
-          let t' = subst params t' in
-          let t',cs',e' = type_coerce l t' (rebuild tannot) expect_t in
+          let t',cs = subst params t' cs in
+          let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t in
           (e',t',t_env,cs@cs')
         | Tapp("reg",[TA_typ(t)]),_ ->
           let tannot = Some((params,t),Emp,cs) in
-          let t',cs',e' = type_coerce l t (rebuild tannot) expect_t in
+          let t',cs',e' = type_coerce l d_env t (rebuild tannot) expect_t in
           (e',t',t_env,cs@cs')
         | _ -> 
-          let t',cs',e' = type_coerce l t (rebuild (Some((params,t),tag,cs))) expect_t in
+          let t',cs',e' = type_coerce l d_env t (rebuild (Some((params,t),tag,cs))) expect_t in
           (e',t',t_env,cs@cs')
         )
       | Some None | None -> (* Turned off until lexp is type checked. TURN ME BACK ON:: typ_error l ("Identifier " ^ (id_to_string id) ^ " is unbound")*) (rebuild None,expect_t,t_env,[]))
     | E_lit (L_aux(lit,l')) ->
-      let t = (match lit with
-        | L_unit  -> {t = Tid "unit"} 
-	| L_zero  -> {t = Tid "bit"}
-	| L_one   -> {t = Tid "bit"}
-	| L_true  -> {t = Tid "bool"}
-	| L_false -> {t = Tid "bool"}
-	| L_num i -> {t = Tapp("enum",
-			       [TA_nexp{nexp = Nconst i};TA_nexp{nexp= Nconst 0};TA_ord{order = Oinc}])}
+      let t,lit' = (match lit with
+        | L_unit  -> unit_t,lit
+	| L_zero  -> bit_t,lit
+	| L_one   -> bit_t,lit
+	| L_true  -> bool_t,lit
+	| L_false -> bool_t,lit
+	| L_num i -> 
+	  if expect_t = bit_t 
+	  then if i = 0 then bit_t,L_zero
+	    else 
+	      if i = 1 then bit_t,L_one
+	      else typ_error l "Expected bit,found number that cannot be used as a bit"
+	  else {t = Tapp("enum",
+			 [TA_nexp{nexp = Nconst i};TA_nexp{nexp= Nconst 0};])},lit	      
 	| L_hex s -> {t = Tapp("vector",
-			       [TA_nexp{nexp = Nconst 0};TA_nexp{nexp = Nconst ((String.length s)*4)};
-				TA_ord{order = Oinc};TA_typ{t = Tid "bit"}])}
+			       [TA_nexp{nexp = Nconst 0};
+				TA_nexp{nexp = Nconst ((String.length s)*4)};
+				TA_ord{order = Oinc};TA_typ{t = Tid "bit"}])},lit
 	| L_bin s -> {t = Tapp("vector",
-			       [TA_nexp{nexp = Nconst 0};TA_nexp{nexp = Nconst(String.length s)};
-				TA_ord{order = Oinc};TA_typ{t = Tid"bit"}])}
-	| L_string s -> {t = Tid "string"}
-	| L_undef -> new_t ()) in
-      let t',cs',e' = type_coerce l t (rebuild (Some (([],t),Emp,[]))) expect_t in
+			       [TA_nexp{nexp = Nconst 0};
+				TA_nexp{nexp = Nconst(String.length s)};
+				TA_ord{order = Oinc};TA_typ{t = Tid"bit"}])},lit
+	| L_string s -> {t = Tid "string"},lit
+	| L_undef -> new_t (),lit) in
+      let t',cs',e' = 
+	type_coerce l d_env t (E_aux(E_lit(L_aux(lit',l')),(l,(Some(([],t),Emp,[]))))) expect_t in
       (e',t',t_env,cs')
     | E_cast(typ,e) ->
       let t = typ_to_t typ in
-      let t',cs = type_consistent l t expect_t in
+      let t',cs = type_consistent l d_env t expect_t in
       let (e',u,t_env,cs') = check_exp envs t' e in
       (e',t',t_env,cs@cs')
     | E_app(id,parms) -> (E_aux(e,(l,annot)),expect_t,t_env,[]) (*TODO*)
@@ -581,12 +582,14 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
     List.split
       (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) ->
 	let (pat',t_env',constraints',t') = check_pattern (Env(d_env,t_env)) pat in
-	let u,cs = type_consistent l t' param_t in
+	let u,cs = type_consistent l d_env t' param_t in
 	let exp,_,_,constraints = check_exp (Env(d_env,Envmap.union t_env t_env')) ret_t exp in
 	(FCL_aux((FCL_Funcl(id,pat',exp)),(l,tannot)),constraints'@cs@constraints)) funcls) in
   match (in_env,tannot) with
     | Some(Some( (params,u),Spec,constraints)), Some( (p',t),Emp,c') ->
-      let t',cs = type_consistent l (subst p' t) (subst params u) in
+      let u,constraints = subst params u constraints in
+      let t,c' = subst p' t c' in
+      let t',cs = type_consistent l d_env t u in
       let t_env = if is_rec then t_env else Envmap.remove t_env id in
       let funcls,cs = check t_env in
       let cs' = resolve_constraints cs in
diff --git a/src/type_check.mli b/src/type_check.mli
index 9f8b6b33..a5056ee7 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -4,14 +4,6 @@ type kind = Type_internal.kind
 type typ = Type_internal.t
 type 'a emap = 'a Envmap.t
 
-type rec_kind = Record | Register
-type def_envs = { 
-  k_env: kind emap; 
-  abbrevs: tannot emap; 
-  namesch : tannot emap; 
-  enum_env : (string list) emap; 
-  rec_env : (string * rec_kind * ((string * tannot) list)) list;
- }
 type envs = Env of def_envs * tannot emap
 type 'a envs_out = 'a * envs
 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 4a3aaec0..96dba7e4 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -71,9 +71,20 @@ type nexp_range =
   | Eq of Parse_ast.l * nexp * nexp
   | GtEq of Parse_ast.l * nexp * nexp
   | In of Parse_ast.l * string * int list
+  | InS of Parse_ast.l * nexp * int list
 
 type t_params = (string * kind) list
 type tannot = ((t_params * t) * tag * nexp_range list) option
+type 'a emap = 'a Envmap.t
+
+type rec_kind = Record | Register
+type def_envs = { 
+  k_env: kind emap; 
+  abbrevs: tannot emap; 
+  namesch : tannot emap; 
+  enum_env : (string list) emap; 
+  rec_env : (string * rec_kind * ((string * tannot) list)) list;
+ }  
 
 type exp = tannot Ast.exp
 
@@ -111,8 +122,9 @@ let new_e _ =
   e_count := i + 1;
   { effect = Euvar { eindex = i; esubst = None }}
   
-let nat_t = {t = Tapp("enum",[TA_nexp{nexp= Nconst 0};TA_nexp{nexp = Nconst max_int};TA_ord{order=Oinc}])}
-let unit_t = { t = Tid "unit" } 
+let nat_t = {t = Tapp("enum",[TA_nexp{nexp= Nconst 0};TA_nexp{nexp = Nconst max_int};])}
+let unit_t = { t = Tid "unit" }
+let bit_t = {t = Tid "bit" }
 let bool_t = {t = Tid "bool" }
 
 let initial_kind_env = 
@@ -123,7 +135,7 @@ let initial_kind_env =
     ("bit", {k = K_Typ});
     ("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})});
     ("reg", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})});
-    ("enum", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}; {k=K_Ord} ], {k = K_Typ}) });
+    ("enum", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}], {k = K_Typ}) });
     ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } )
   ]
 
@@ -137,6 +149,11 @@ let initial_typ_env =
     
   ]
 
+let initial_abbrev_env =
+  Envmap.from_list [
+    ("nat",Some(([],nat_t),Emp,[]));
+  ]
+
 let rec t_subst s_env t =
   match t.t with
   | Tvar i -> (match Envmap.apply s_env i with
@@ -175,7 +192,16 @@ and e_subst s_env e =
                | _ -> e)
   | _ -> e
 
-let subst k_env t =
+let rec cs_subst t_env cs =
+  match cs with
+    | [] -> []
+    | Eq(l,n1,n2)::cs -> Eq(l,n_subst t_env n1,n_subst t_env n2)::(cs_subst t_env cs)
+    | GtEq(l,n1,n2)::cs -> GtEq(l,n_subst t_env n1, n_subst t_env n2)::(cs_subst t_env cs)
+    | LtEq(l,n1,n2)::cs -> LtEq(l,n_subst t_env n1, n_subst t_env n2)::(cs_subst t_env cs)
+    | In(l,s,ns)::cs -> InS(l,n_subst t_env {nexp=Nvar s},ns)::(cs_subst t_env cs)
+    | InS(l,n,ns)::cs -> InS(l,n_subst t_env n,ns)::(cs_subst t_env cs)
+
+let subst k_env t cs =
   let subst_env = Envmap.from_list
     (List.map (fun (id,k) -> (id, 
                               match k.k with
@@ -185,7 +211,44 @@ let subst k_env t =
                               | K_Efct -> TA_eft (new_e ())
                               | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "substitution given an environment with a non-base-kind kind"))) k_env) 
   in
-  t_subst subst_env t
+  t_subst subst_env t, cs_subst subst_env cs
+
+let rec t_to_string t = 
+  match t.t with
+    | Tid i -> i
+    | Tvar i -> "'" ^ i
+    | Tfn(t1,t2,e) -> (t_to_string t1) ^ " -> " ^ (t_to_string t2) ^ " effect " ^ e_to_string e
+    | Ttup(tups) -> "(" ^ (List.fold_right (fun t ts -> ts^ (t_to_string t) ^ " * ") tups "") ^ ")"
+    | Tapp(i,args) -> i ^ "<" ^ (List.fold_right (fun t ts -> ts^(targ_to_string t) ^ ", ") args "") ^ ">"
+    | Tuvar({index = i;subst = a}) -> string_of_int i ^ "()"
+and targ_to_string = function
+  | TA_typ t -> t_to_string t
+  | TA_nexp n -> n_to_string n
+  | TA_eft e -> e_to_string e
+  | TA_ord o -> o_to_string o
+and n_to_string n =
+  match n.nexp with
+    | Nvar i -> "'" ^ i
+    | Nconst i -> string_of_int i
+    | Nadd(n1,n2) -> (n_to_string n1) ^ " + " ^ (n_to_string n2)
+and e_to_string e = "effect"
+and o_to_string o = "order"
+
+let get_abbrev d_env t =
+  match t.t with
+    | Tid i ->
+      (match Envmap.apply d_env.abbrevs i with
+	| Some(Some((params,t),tag,cs)) ->
+	  Some(subst params t cs)
+	| _ -> None)
+    | Tapp(i,args) ->
+      (match Envmap.apply d_env.abbrevs i with
+	| Some(Some((params,t),tag,cs)) ->
+	  let env = Envmap.from_list2 (List.map fst params) args in
+	  Some(t_subst env t, cs_subst env cs)
+	| _ -> None)
+    | _ -> None
+
 
 let eq_error l msg = raise (Reporting_basic.err_typ l msg)
 
@@ -248,55 +311,74 @@ let rec nexp_eq n1 n2 =
   | _,_ -> false
 
 (*Is checking for structural equality amongst the types, building constraints for kind Nat. 
-  When considering two enum type applications, will check for consistency instead of equality
-  Note: needs an environment to handle type abbreviations, and to lookup in the case either is a Tid or Tapp*)
-let rec type_consistent l t1 t2 = 
+  When considering two enum type applications, will check for consistency instead of equality*)
+let rec type_consistent l d_env t1 t2 = 
   match t1.t,t2.t with
-  | Tvar v1,Tvar v2 -> if v1 = v2 then (t2,[]) else eq_error l ("Type variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified")
-  | Tid v1,Tid v2 -> if v1 = v2 then (t2,[]) else eq_error l ("Types " ^ v1 ^ " and " ^ v2 ^ " do not match") (*lookup for abbrev*)
+  | Tvar v1,Tvar v2 -> 
+    if v1 = v2 then (t2,[]) 
+    else eq_error l ("Type variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified")
+  | Tid v1,Tid v2 -> 
+    if v1 = v2 then (t2,[]) 
+    else (match get_abbrev d_env t1,get_abbrev d_env t2 with
+      | Some(t1,cs1),Some(t2,cs2) ->
+	let t',cs' = type_consistent l d_env t1 t2 in
+	t',cs1@cs2@cs'
+      | Some(t1,cs1),None ->
+	let t',cs' = type_consistent l d_env t1 t2 in
+	t',cs1@cs'
+      | None,Some(t2,cs2) ->
+	let t',cs' = type_consistent l d_env t1 t2 in
+	t',cs2@cs'
+      | None,None ->  eq_error l ("Types " ^ v1 ^ " and " ^ v2 ^ " do not match"))
+  | Tapp("enum",[TA_nexp b1;TA_nexp r1;]),Tapp("enum",[TA_nexp b2;TA_nexp r2;]) -> 
+    if (nexp_eq b1 b2)&&(nexp_eq r1 r2) then (t2,[])
+    else (t2, [GtEq(l,b1,b2);LtEq(l,r1,r2)])
+  | Tapp(id1,args1), Tapp(id2,args2) ->
+    let la1,la2 = List.length args1, List.length args2 in
+    if id1=id2 && la1 = la2 then (t2,(List.flatten (List.map2 (type_arg_eq l d_env) args1 args2)))
+    else
+      (match get_abbrev d_env t1,get_abbrev d_env t2 with
+	| Some(t1,cs1),Some(t2,cs2) ->
+	  let t',cs' = type_consistent l d_env t1 t2 in
+	  t',cs1@cs2@cs'
+	| Some(t1,cs1),None ->
+	  let t',cs' = type_consistent l d_env t1 t2 in
+	  t',cs1@cs'
+	| None,Some(t2,cs2) ->
+	  let t',cs' = type_consistent l d_env t1 t2 in
+	  t',cs2@cs'
+	| None,None -> eq_error l ("Type application of " ^ (t_to_string t1) ^ " and " ^ (t_to_string t2) ^ " must match"))
   | Tfn(tin1,tout1,effect1),Tfn(tin2,tout2,effect2) -> 
-    let (tin,cin) = type_consistent l tin1 tin2 in
-    let (tout,cout) = type_consistent l tout1 tout2 in
+    let (tin,cin) = type_consistent l d_env tin1 tin2 in
+    let (tout,cout) = type_consistent l d_env tout1 tout2 in
     let effect = effects_eq l effect1 effect2 in
     (t2,cin@cout)
   | Ttup t1s, Ttup t2s ->
-    (t2,(List.flatten (List.map snd (List.map2 (type_consistent l) t1s t2s))))
-  | Tapp(id1,args1), Tapp(id2,args2) ->
-    if id1=id2 && (List.length args2 = List.length args2) then
-      if id1="enum" then
-        (match args1,args2 with
-        | [TA_nexp b1;TA_nexp r1; TA_ord o1],[TA_nexp b2;TA_nexp r2;TA_ord o2] ->
-          (match (order_eq l o1 o2).order with
-          | Oinc -> 
-            if (nexp_eq b1 b2)&&(nexp_eq r1 r2)
-            then (t2,[])
-            else (t2, [GtEq(l,b1,b2);LtEq(l,r1,r2)])
-          | Odec ->
-            if (nexp_eq b1 b2)&&(nexp_eq r1 r2)
-            then (t2,[])
-            else (t2, [LtEq(l,b1,b2);GtEq(l,r1,r2)])
-          | _ ->
-            if (nexp_eq b1 b2)&&(nexp_eq r1 r2)
-            then (t2,[])
-            else (t2, [Eq(l,b1,b2);Eq(l,r1,r2)]))
-        | _ -> raise (Reporting_basic.err_unreachable l "enum application incorrectly kinded"))
-      else          
-      (t2,(List.flatten (List.map2 (type_arg_eq l) args1 args2)))
-    else eq_error l ("Type application of " ^ id1 ^ " and " ^ id2 ^ " must match")
+    (t2,(List.flatten (List.map snd (List.map2 (type_consistent l d_env) t1s t2s))))
   | Tuvar _, t -> t1.t <- t2.t; (t2,[])
   | t,Tuvar _ -> t2.t <- t1.t; (t2,[])
-  | _,_ -> eq_error l ("Type mismatch")
+  | _,_ ->
+    (match get_abbrev d_env t1,get_abbrev d_env t2 with
+      | Some(t1,cs1),Some(t2,cs2) ->
+	let t',cs' = type_consistent l d_env t1 t2 in
+	t',cs1@cs2@cs'
+      | Some(t1,cs1),None ->
+	let t',cs' = type_consistent l d_env t1 t2 in
+	t',cs1@cs'
+      | None,Some(t2,cs2) ->
+	let t',cs' = type_consistent l d_env t1 t2 in
+	t',cs2@cs'
+      | None,None -> eq_error l ("Type mismatch :" ^ (t_to_string t1) ^ " , " ^ (t_to_string t2)))
 
-and type_arg_eq l ta1 ta2 = 
+and type_arg_eq l d_env ta1 ta2 = 
   match ta1,ta2 with
-  | TA_typ t1,TA_typ t2 -> snd (type_consistent l t1 t2)
+  | TA_typ t1,TA_typ t2 -> snd (type_consistent l d_env t1 t2)
   | TA_nexp n1,TA_nexp n2 -> if nexp_eq n1 n2 then [] else [Eq(l,n1,n2)]
   | TA_eft e1,TA_eft e2 -> (ignore(effects_eq l e1 e2);[])
   | TA_ord o1,TA_ord o2 -> (ignore(order_eq l o1 o2);[])
   | _,_ -> eq_error l "Type arguments must be of the same kind" 
 
-
-let rec type_coerce l t1 e t2 = 
+let rec type_coerce l d_env t1 e t2 = 
   match t1.t,t2.t with
   | Ttup t1s, Ttup t2s ->
     let tl1,tl2 = List.length t1s,List.length t2s in
@@ -304,7 +386,7 @@ let rec type_coerce l t1 e t2 =
       let ids = List.map (fun _ -> Id_aux(Id (new_id ()),l)) t1s in
       let vars = List.map2 (fun i t -> E_aux(E_id(i),(l,Some(([],t),Emp,[])))) ids t1s in
       let (coerced_ts,cs,coerced_vars) = 
-        List.fold_right2 (fun v (t1,t2) (ts,cs,es) -> let (t',c',e') = type_coerce l t1 v t2 in
+        List.fold_right2 (fun v (t1,t2) (ts,cs,es) -> let (t',c',e') = type_coerce l d_env t1 v t2 in
                                                       ((t'::ts),c'@cs,(e'::es)))
           vars (List.combine t1s t2s) ([],[],[]) in
       if vars = coerced_vars then (t2,cs,e)
@@ -316,19 +398,101 @@ let rec type_coerce l t1 e t2 =
     else eq_error l ("A tuple of length " ^ (string_of_int tl1) ^ " cannot be used where a tuple of length " ^ (string_of_int tl2) ^ " is expected")
   | Tapp(id1,args1),Tapp(id2,args2) ->
     if id1=id2 
-    then let t',cs' = type_consistent l t1 t2 in (t',cs',e)
+    then let t',cs' = type_consistent l d_env t1 t2 in (t',cs',e)
     else (match id1,id2 with
     | "vector","enum" -> 
       (match args1,args2 with
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
-        [TA_nexp b2;TA_nexp r2;TA_ord {order = Oinc}] -> (t2,[],e) (*TODO*)
+        [TA_nexp b2;TA_nexp r2;] -> 
+	let cs = [Eq(l,b2,{nexp=Nconst 0});Eq(l,r2,{nexp=N2n({nexp=Nadd(b1,r1)})})] in
+	(t2,cs,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Some(([],t2),Emp,cs))))
+      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
+        [TA_nexp b2;TA_nexp r2;] -> 
+	let cs = [Eq(l,b2,{nexp=Nconst 0});Eq(l,r2,{nexp=N2n({nexp=Nadd({nexp=Nneg b1},r1)})})] in
+	(t2,cs,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Some(([],t2),Emp,cs))))
+      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
+	eq_error l "Cannot convert a vector to an enum without an order"
+      | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
+        eq_error l "Cannot convert non-bit vector into an enum"
+      | _,_ -> raise (Reporting_basic.err_unreachable l "vector or enum is not properly kinded"))
+    | "enum","vector" -> 
+      (match args2,args1 with
+      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
+        [TA_nexp b2;TA_nexp r2;] -> 
+	let cs = [Eq(l,b1,{nexp=Nconst 0});Eq(l,{nexp=Nadd(b2,r2)},{nexp=N2n r1})] in
+	(t2,cs,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),[e]),(l,Some(([],t2),Emp,cs))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
-        [TA_nexp b2;TA_nexp r2;TA_ord {order = Odec}] -> (t2,[],e) (*TODO*)
-      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> (t2,[],e) (*TODO*)
+        [TA_nexp b2;TA_nexp r2;] -> 
+	let cs = [Eq(l,b1,{nexp=N2n{nexp=Nadd(b2,{nexp=Nneg r2})}});
+		  Eq(l,r1,b1)] in
+	(t2,cs,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Some(([],t2),Emp,cs))))
+      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
+	eq_error l "Cannot convert an enum to a vector without an order"
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
-        eq_error l "Cannot convert non-bit vector into an enum")
-    | "enum","vector" -> (t2,[],e) (*TODO*)
-    | _,_ -> let t',cs' = type_consistent l t1 t2 in (t',cs',e))
-  | Tapp("enum",args1),Tid(i) -> (t2,[],e) (*Need env*)
-  | Tid(i),Tapp("enum",args1) -> (t2,[],e) (*Need env*)
-  | _,_ -> let t',cs = type_consistent l t1 t2 in (t',cs,e)
+        eq_error l "Cannot convert an enum into a non-bit vector"
+      | _,_ -> raise (Reporting_basic.err_unreachable l "vector or enum is not properly kinded"))
+    | _,_ -> 
+      (match get_abbrev d_env t1,get_abbrev d_env t2 with
+	| Some(t1,cs1),Some(t2,cs2) ->
+	  let t',cs',e' = type_coerce l d_env t1 e t2 in
+	  (t',cs1@cs2@cs',e')
+	| Some(t1,cs1),None ->
+	  let t',cs',e' = type_coerce l d_env t1 e t2 in
+	  (t',cs1@cs',e')
+	| None,Some(t2,cs2) ->
+	  let t',cs',e' = type_coerce l d_env t1 e t2 in
+	  (t',cs2@cs',e')
+	| None,None ->
+	  let t',cs' = type_consistent l d_env t1 t2 in (t',cs',e)))
+  | Tapp("enum",[TA_nexp b1;TA_nexp r1;]),Tid("bit") ->
+    let t',cs'= type_consistent l d_env t1 {t=Tapp("enum",[TA_nexp{nexp=Nconst 0};TA_nexp{nexp=Nconst 1}])} 
+    in (t2,cs',E_aux(E_if(E_aux(E_app(Id_aux(Id "is_zero",l),[e]),(l,Some(([],bool_t),Emp,[]))),
+			  E_aux(E_lit(L_aux(L_zero,l)),(l,Some(([],bit_t),Emp,[]))),
+			  E_aux(E_lit(L_aux(L_one,l)),(l,Some(([],bit_t),Emp,[])))),
+		     (l,Some(([],bit_t),Emp,cs'))))
+  | Tapp("enum",[TA_nexp b1;TA_nexp r1;]),Tid(i) -> 
+    (match get_abbrev d_env t2 with
+      | Some(t2,cs2) ->
+	let t',cs',e' = type_coerce l d_env t1 e t2 in
+	(t',cs2@cs',e')
+      | None -> 
+	(match Envmap.apply d_env.enum_env i with
+	  | Some(enums) -> 
+	    (t2,[Eq(l,b1,{nexp=Nconst 0});LtEq(l,r1,{nexp=Nconst (List.length enums)})],
+	     E_aux(E_case(e,
+			  List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_lit(L_aux((L_num i),l)),
+								      (l,Some(([],t1),Emp,[]))),
+								E_aux(E_id(Id_aux(Id a,l)),
+								      (l,Some(([],t2),Emp,[])))),
+							(l,Some(([],t2),Emp,[])))) enums),
+		   (l,Some(([],t2),Emp,[]))))
+	  | None -> eq_error l ("Type mismatch: " ^ (t_to_string t1) ^ " , " ^ (t_to_string t2))))
+  | Tid(i),Tapp("enum",[TA_nexp b1;TA_nexp r1;]) -> 
+    (match get_abbrev d_env t1 with
+      | Some(t1,cs1) ->
+	let t',cs',e' = type_coerce l d_env t1 e t2 in
+	(t',cs1@cs',e')
+      | None -> 
+	(match Envmap.apply d_env.enum_env i with
+	  | Some(enums) -> 
+	    (t2,[Eq(l,b1,{nexp=Nconst 0});GtEq(l,r1,{nexp=Nconst (List.length enums)})],
+	     E_aux(E_case(e,
+			  List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_id(Id_aux(Id a,l)),
+								      (l,Some(([],t1),Emp,[]))),
+								E_aux(E_lit(L_aux((L_num i),l)),
+								      (l,Some(([],t2),Emp,[])))),
+							(l,Some(([],t2),Emp,[])))) enums),
+		   (l,Some(([],t2),Emp,[]))))
+	  | None -> eq_error l ("Type mismatch: " ^ (t_to_string t1) ^ " , " ^ (t_to_string t2))))
+  | _,_ -> 
+    (match get_abbrev d_env t1,get_abbrev d_env t2 with
+      | Some(t1,cs1),Some(t2,cs2) -> 
+	let t',cs',e' = type_coerce l d_env t1 e t2 in
+	(t',cs'@cs1@cs2,e')
+      | Some(t1,cs1),None ->
+	let t',cs',e' = type_coerce l d_env t1 e t2 in
+	(t',cs'@cs1,e')
+      | None,Some(t2,cs2) ->
+	let t',cs',e' = type_coerce l d_env t1 e t2 in
+	(t',cs'@cs2,e')
+      | None,None -> let t',cs = type_consistent l d_env t1 t2 in (t',cs,e))
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 3a8c669d..458009f5 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -66,17 +66,30 @@ type nexp_range =
   | Eq of Parse_ast.l * nexp * nexp
   | GtEq of Parse_ast.l * nexp * nexp
   | In of Parse_ast.l * string * int list
+  | InS of Parse_ast.l * nexp * int list (* This holds the given value for string after a substitution *)
 
 type t_params = (string * kind) list
 type tannot = ((t_params * t) * tag * nexp_range list) option
+type 'a emap = 'a Envmap.t
+
+type rec_kind = Record | Register
+type def_envs = { 
+  k_env: kind emap; 
+  abbrevs: tannot emap; 
+  namesch : tannot emap; 
+  enum_env : (string list) emap; 
+  rec_env : (string * rec_kind * ((string * tannot) list)) list;
+ }
 
 type exp = tannot Ast.exp
 
 val initial_kind_env : kind Envmap.t
+val initial_abbrev_env : tannot Envmap.t
 val initial_typ_env : tannot Envmap.t
 val nat_t : t
 val unit_t : t
 val bool_t : t
+val bit_t : t
 
 val reset_fresh : unit -> unit
 val new_t : unit -> t
@@ -84,7 +97,7 @@ val new_n : unit -> nexp
 val new_o : unit -> order
 val new_e : unit -> effect
 
-val subst : (string * kind) list -> t -> t
+val subst : (string * kind) list -> t -> nexp_range list -> t * nexp_range list
 
 
 (* type_consistent is similar to a standard type equality, except in the case of [[consistent t1 t2]] where
@@ -92,7 +105,7 @@ val subst : (string * kind) list -> t -> t
    enum 2 5 inc is consistent with enum 0 10 inc, but not vice versa.
    type_consistent mutates uvars to perform unification and will raise an error if the [[t1]] and [[t2]] are inconsitent
 *)
-val type_consistent : Parse_ast.l -> t -> t -> t * nexp_range list
+val type_consistent : Parse_ast.l -> def_envs -> t -> t -> t * nexp_range list
 
 (* type_eq mutates to unify variables, and will raise an exception if the first type cannot be coerced into the second *)
-val type_coerce : Parse_ast.l -> t -> exp -> t -> t * nexp_range list * exp
+val type_coerce : Parse_ast.l -> def_envs -> t -> exp -> t -> t * nexp_range list * exp