Change treatment of type abbreviations so that name and full type are available for field lookups of registers; this feature still not fully working.

7 files changed, 146 insertions, 177 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 32b6f1c7..2fd685f4 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -484,6 +484,7 @@ type t =  (* Internal types *)
  | T_fn of t * t * effect
  | T_tup of list t
  | T_app of id * t_args
+ | T_abbrev of t * t
 
 and t_arg =  (* Argument to type constructors *)
  | T_arg_typ of t
diff --git a/language/l2_typ.ott b/language/l2_typ.ott
index 43a3ea17..057ddfba 100644
--- a/language/l2_typ.ott
+++ b/language/l2_typ.ott
@@ -47,6 +47,7 @@ t , u :: 'T_' ::=
    | t1 -> t2 effect                        :: :: fn 
    | ( t1 * .... * tn )                          :: :: tup
    | id t_args                                  :: :: app 
+   | t |-> t1                                   :: :: abbrev
    | register t_args                         :: S :: reg_app {{ ichlo T_app "register" [[t_args]] }}
    | t [ t1 / id1 ... tn / idn ]            :: M :: subst {{ ichlo "todo" }}
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 7ee110d3..5d6e45e7 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -531,6 +531,7 @@ let rec pp_format_t t =
     | Tfn(t1,t2,e) -> "(T_fn " ^ (pp_format_t t1) ^ " " ^ (pp_format_t t2) ^ " " ^ pp_format_e e ^ ")"
     | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t tups) ^ "])"
     | Tapp(i,args) -> "(T_app (Id_aux (Id \"" ^ i ^ "\") Unknown) (T_args [" ^  list_format "; " pp_format_targ args ^ "]))"
+    | Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t ti) ^ " " ^ (pp_format_t ta) ^ ")"
     | Tuvar(_) -> "(T_var (Kid_aux (Var \"fresh_v\") Unknown))"
 and pp_format_targ = function
   | TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")"
diff --git a/src/test/regbits.sail b/src/test/regbits.sail
index e52d5ff9..5faf8d55 100644
--- a/src/test/regbits.sail
+++ b/src/test/regbits.sail
@@ -12,6 +12,6 @@ function bit main _ = {
   f := XER;
   (bit[7]) foo := XER[57..63];
   query := XER.SO;
-(*  XER.SO := query;*)
+  (*XER.SO := query;*)
   bitzero }
 
diff --git a/src/type_check.ml b/src/type_check.ml
index fad01f87..983340a1 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -151,12 +151,11 @@ let typschm_to_tannot envs ((TypSchm_aux(typschm,l)):typschm) (tag : tag) : tann
 let into_register d_env (t : tannot) : tannot =
   match t with
     | Some((ids,ty),tag,constraints,eft) -> 
-      let ty' =  match get_abbrev d_env ty with
-	| Some(t,cs,e) -> t
-	| None -> ty in
+      let ty',_,_ =  get_abbrev d_env ty in
       (match ty'.t with 
 	| Tapp("register",_)-> t
-	| _ -> Some((ids, {t= Tapp("register",[TA_typ ty])}),tag,constraints,eft))
+        | Tabbrev(ti,{t=Tapp("register",_)}) -> Some((ids,ty'),tag,constraints,eft)
+	| _ -> Some((ids, {t= Tapp("register",[TA_typ ty'])}),tag,constraints,eft))
     | None -> None
 
 let rec check_pattern envs expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap) * nexp_range list * t)  =
@@ -378,10 +377,14 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
         typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use")
       | Some(Some((params,t),tag,cs,ef)) ->
 	let t,cs,ef = subst params t cs ef in
-	let ta,cs,ef = match get_abbrev d_env t with
-	  | Some(t,cs1,ef1) -> t,cs@cs1,union_effects ef ef1
-	  | None -> t,cs,ef in
-        (match ta.t,expect_t.t with 
+        let t,cs',ef' = get_abbrev d_env t in
+        let cs,ef = cs@cs',union_effects ef ef' in
+        let t_actual,expect_actual = match t.t,expect_t.t with
+          | Tabbrev(_,t),Tabbrev(_,e) -> t,e
+          | Tabbrev(_,t),_ -> t,expect_t 
+          | _,Tabbrev(_,e) -> t,e
+          | _,_ -> t,expect_t in
+        (match t_actual.t,expect_actual.t with 
         | 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(([],t),Emp,cs,ef) in
@@ -389,13 +392,13 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
           (e',t,t_env,cs@cs',ef)
         | Tapp("register",[TA_typ(t')]),_ ->
 	  let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
-          let tannot = Some(([],ta),External (Some "register"),cs,ef') in
-          let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t in
+          let tannot = Some(([],t),External (Some i),cs,ef') in
+          let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_actual in
           (e',t,t_env,cs@cs',ef)
-        | Tapp("reg",[TA_typ(t)]),_ ->
+        | Tapp("reg",[TA_typ(t')]),_ ->
           let tannot = Some(([],t),Emp,cs,pure_e) in
-          let t',cs',e' = type_coerce l d_env t (rebuild tannot) expect_t in
-          (e',t,t_env,cs@cs',pure_e)
+          let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_actual in
+          (e',t',t_env,cs@cs',pure_e)
         | _ -> 
           let t',cs',e' = type_coerce l d_env t (rebuild (Some(([],t),tag,cs,pure_e))) expect_t in
           (e',t,t_env,cs@cs',pure_e)
@@ -694,10 +697,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let (t',cs',e') = type_coerce l d_env lt (E_aux(E_cons(ls',i'),(l,Some(([],lt),Emp,[],pure_e)))) expect_t in
       (e',t',t_env,cs@cs'@cs_i,(union_effects ef ef_i))
     | E_record(FES_aux(FES_Fexps(fexps,_),l')) -> 
-      let u = match (get_abbrev d_env expect_t) with
-	| Some(t,cs,ef) -> t
-	| None -> expect_t in
-      (match u.t with
+      let u,_,_ = get_abbrev d_env expect_t in
+      let u_actual = match u.t with | Tabbrev(_, u) -> u | _ -> u in
+      (match u_actual.t with
 	| Tid(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")
@@ -715,7 +717,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 			     let (e,t',_,c,ef) = check_exp envs et exp in
 			     (FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
 		       fexps ([],[],pure_e) in
-		   E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],expect_t),Emp,[],pure_e))),expect_t,t_env,cons,ef
+		   E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],u),Emp,[],pure_e))),expect_t,t_env,cons,ef
 	      else typ_error l ("Expected a struct of type " ^ n ^ ", which should have " ^ string_of_int (List.length fields) ^ " fields")
 	    | Some(i,Register,fields) -> typ_error l ("Expected a value with register type, found a struct"))
 	| Tuvar _ ->
@@ -741,7 +743,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
     | E_record_update(exp,FES_aux(FES_Fexps(fexps,_),l')) -> 
       let (e',t',_,c,ef) = check_exp envs expect_t exp in
       (match t'.t with
-	| Tid i ->
+	| Tid i | Tabbrev(_, {t=Tid 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,fields)) ->
@@ -786,7 +788,19 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
     | E_field(exp,id) ->
       let (e',t',_,c,ef) = check_exp envs (new_t()) exp in
       (match t'.t with
-	| Tid i ->
+      | Tabbrev({t=Tid i}, t2) ->
+	  (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,fields) as r)) ->
+	      let fi = id_to_string id in
+	      (match lookup_field_type fi r with
+		| None -> 
+		  typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
+		| Some((params,et),tag,cs,ef) ->
+		  let et,cs,ef = subst params et cs ef in
+		  let (et',c',acc) = type_coerce l d_env et (E_aux(E_field(e',id),(l,Some(([],et),tag,cs,ef)))) expect_t in
+		  (acc,et',t_env,cs@c',ef)))        
+      | Tid 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,fields) as r)) ->
@@ -867,23 +881,24 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
 	  typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists")
 	| Some(Some((parms,t),tag,cs,_)) ->
 	  let t,cs,_ = subst parms t cs pure_e in
-	  let t,cs = match get_abbrev d_env t with
-	    | None -> t,cs
-	    | Some(t,cs,e) -> t,cs in
-	  (match t.t,is_top with
+	  let t,cs',_ = get_abbrev d_env t in
+          let t_actual = match t.t with 
+            | Tabbrev(i,t) -> t
+            | _ -> t in
+	  (match t_actual.t,is_top with
 	    | Tapp("register",[TA_typ u]),_ ->
 	      let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
-	      (LEXP_aux(lexp,(l,(Some(([],t),External (Some "register"),cs,ef)))),u,Envmap.empty,External (Some "register"),[],ef)
+	      (LEXP_aux(lexp,(l,(Some(([],t),External (Some i),cs@cs',ef)))),u,Envmap.empty,External (Some i),[],ef)
 	    | Tapp("reg",[TA_typ u]),_ ->
-	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),u,Envmap.empty,Emp,[],pure_e)
+	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs@cs',pure_e)))),u,Envmap.empty,Emp,[],pure_e)
 	    | Tapp("vector",_),false ->
-	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),t,Envmap.empty,Emp,[],pure_e)
+	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs@cs',pure_e)))),t,Envmap.empty,Emp,[],pure_e)
 	    | _,_ -> 
 	      if is_top
 	      then typ_error l 
 		("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t)
 	      else 
-		(LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),t,Envmap.empty,Emp,[],pure_e) (* TODO, make sure this is a record *))
+		(LEXP_aux(lexp,(l,(Some(([],t),Emp,cs@cs',pure_e)))),t,Envmap.empty,Emp,[],pure_e) (* TODO, make sure this is a record *))
 	| _ -> 
 	  let u = new_t() in
 	  let t = {t=Tapp("reg",[TA_typ u])} in
@@ -895,23 +910,16 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
 	| Some(Some((parms,t),tag,cs,ef)) ->
 	  let is_external = match tag with | External any -> true | _ -> false in
 	  let t,cs,ef = subst parms t cs ef in
-	  let t,cs,ef = match get_abbrev d_env t with
-	    | None -> t,cs,ef
-	    | Some(t,cs,ef) -> t,cs,ef in
 	  (match t.t with
 	    | Tfn(apps,out,ef') ->
 	      (match ef'.effect with
 		| Eset effects ->
 		  if List.exists (fun (BE_aux(b,_)) -> match b with | BE_wmem -> true | _ -> false) effects 
 		  then
-		    let apps,cs' = match get_abbrev d_env apps with
-		      | None -> apps,[]
-		      | Some(t,cs,_) -> t,cs in
-		    let out,cs'' = match get_abbrev d_env out with
-		      | None -> out,[]
-		      | Some(t,cs,_) -> t,cs in 
-		    (match apps.t with
-		      | Ttup ts -> 
+                    let app,cs_a,_ = get_abbrev d_env apps in
+                    let out,cs_o,_ = get_abbrev d_env out in
+                    (match app.t with
+		      | Ttup ts | Tabbrev(_,{t=Ttup ts}) -> 
 			let (E_aux(E_tuple es,(l',tannot)),t',_,cs',ef_e) = check_exp envs apps (E_aux(E_tuple exps,(l,None))) in
 			let item_t = match out.t with
 			  | Tid "unit" -> {t = Tapp("vector",[TA_nexp (new_n());TA_nexp (new_n()); TA_ord (new_o());TA_typ bit_t])}
@@ -941,19 +949,18 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
 	  typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists")
 	| Some(Some((parms,t),tag,cs,_)) ->
 	  let t,cs,_ = subst parms t cs pure_e in
-	  let t,cs = match get_abbrev d_env t with
-	    | None -> t,cs
-	    | Some(t,cs,e) -> t,cs in
-	  (match t.t,is_top with
+	  let t,cs',_ = get_abbrev d_env t in
+          let t_actual = match t.t with | Tabbrev(_,t) -> t | _ -> t in
+	  (match t_actual.t,is_top with
 	    | Tapp("register",[TA_typ u]),_ ->
 	      let t',cs = type_consistent l d_env ty u in
 	      let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
-	      (LEXP_aux(lexp,(l,(Some(([],t),External (Some "register"),cs,ef)))),ty,Envmap.empty,External (Some "register"),[],ef)
+	      (LEXP_aux(lexp,(l,(Some(([],t),External (Some i),cs,ef)))),ty,Envmap.empty,External (Some i),[],ef)
 	    | Tapp("reg",[TA_typ u]),_ ->
 	      let t',cs = type_consistent l d_env ty u in
 	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),ty,Envmap.empty,Emp,[],pure_e)
 	    | Tapp("vector",_),false ->
-	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),t,Envmap.empty,Emp,[],pure_e)
+	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),ty,Envmap.empty,Emp,[],pure_e)
 	    | Tuvar _,_ ->
 	      let u' = {t=Tapp("reg",[TA_typ ty])} in
 	      t.t <- u'.t;
@@ -963,17 +970,16 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
 	      then typ_error l 
 		("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t)
 	      else 
-		(LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),t,Envmap.empty,Emp,[],pure_e)) (* TODO, make sure this is a record *)
+		(LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),ty,Envmap.empty,Emp,[],pure_e)) (* TODO, make sure this is a record *)
 	| _ -> 
 	  let t = {t=Tapp("reg",[TA_typ ty])} in
 	  let tannot = (Some(([],t),Emp,[],pure_e)) in
 	  (LEXP_aux(lexp,(l,tannot)),ty,Envmap.from_list [i,tannot],Emp,[],pure_e))
     | LEXP_vector(vec,acc) -> 
       let (vec',item_t,env,tag,csi,ef) = check_lexp envs false vec in
-      let item_t,cs = match get_abbrev d_env item_t with
-	| None -> item_t,csi
-	| Some(t,cs,ef) -> t,cs@csi in
-      (match item_t.t with
+      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
+      (match item_actual.t with
 	| Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ t]) ->
 	  let acc_t = match ord.order with
 	    | Oinc -> {t = Tapp("enum",[TA_nexp base;TA_nexp rise])} 
@@ -983,25 +989,23 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
 	  let (e,t',_,cs',ef_e) = check_exp envs acc_t acc in
 	  let t,add_reg_write = 
 	    match t.t with
-	      | Tapp("register",[TA_typ t]) -> t,true
+	      | Tapp("register",[TA_typ t]) | Tabbrev(_,{t=Tapp("register",[TA_typ t])}) -> t,true
 	      | _ -> t,false in
 	  let ef = if add_reg_write then add_effect (BE_aux(BE_wreg,l)) ef else ef in
-	  (LEXP_aux(LEXP_vector(vec',e),(l,Some(([],t),tag,cs,ef))),t,env,tag,cs@cs',union_effects ef ef_e)
+	  (LEXP_aux(LEXP_vector(vec',e),(l,Some(([],t),tag,csi,ef))),t,env,tag,csi@cs',union_effects ef ef_e)
 	| Tuvar _ -> typ_error l "Assignment to one position expected a vector with a known order, found a polymorphic value, try adding a cast"
 	| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string item_t))) 
     | LEXP_vector_range(vec,e1,e2)-> 
       let (vec',item_t,env,tag,csi,ef) = check_lexp envs false vec in
-      let item_t,cs = match get_abbrev d_env item_t with
-	| None -> item_t,csi
-	| Some(t,cs,ef) -> t,cs@csi in
-      let item_t,add_reg_write,cs = 
-	match item_t.t with
+      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,cs = 
+	match item_actual.t with
 	  | Tapp("register",[TA_typ t]) ->
 	    (match get_abbrev d_env t with
-	      | None -> t,true,cs
-	      | Some(t,cs',ef) -> t,true,cs@cs')
-	  | _ -> item_t,false,cs in
-      (match item_t.t with
+	      | {t=Tabbrev(_,t)},cs',_ | t,cs',_ -> t,true,cs@cs')
+	  | _ -> item_actual,false,cs in
+      (match item_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("enum",[TA_nexp base_e1;TA_nexp range_e1])} in
@@ -1029,7 +1033,7 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
     | LEXP_field(vec,id)-> 
       let (vec',item_t,env,tag,csi,ef) = check_lexp envs false vec in
       (match item_t.t with
-	| Tid i ->
+	| Tid i | Tabbrev({t=Tid i},_) ->
 	  (match lookup_record_typ i d_env.rec_env with
 	    | None -> typ_error l ("Expected a register for this update, instead found an expression with type " ^ i)
 	    | Some(((i,rec_kind,fields) as r)) ->
diff --git a/src/type_internal.ml b/src/type_internal.ml
index da60aa13..3d4d4689 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -26,6 +26,7 @@ and t_aux =
   | Tfn of t * t * effect
   | Ttup of t list
   | Tapp of string * t_arg list
+  | Tabbrev of t * t
   | Tuvar of t_uvar
 and t_uvar = { index : int; mutable subst : t option }
 and nexp = { mutable nexp : nexp_aux }
@@ -235,6 +236,7 @@ let rec t_subst s_env t =
   | Tfn(t1,t2,e) -> {t =Tfn((t_subst s_env t1),(t_subst s_env t2),(e_subst s_env e)) }
   | Ttup(ts) -> { t= Ttup(List.map (t_subst s_env) ts) }
   | Tapp(i,args) -> {t= Tapp(i,List.map (ta_subst s_env) args)}
+  | Tabbrev(ti,ta) -> {t = Tabbrev(t_subst s_env ti,t_subst s_env ta) }
 and ta_subst s_env ta =
   match ta with
   | TA_typ t -> TA_typ (t_subst s_env t)
@@ -300,6 +302,7 @@ let rec t_to_string t =
     | Tfn(t1,t2,e) -> (t_to_string t1) ^ " -> " ^ (t_to_string t2) ^ " effect " ^ e_to_string e
     | Ttup(tups) -> "(" ^ string_of_list " * " t_to_string tups ^ ")"
     | Tapp(i,args) -> i ^ "<" ^  string_of_list ", " targ_to_string args ^ ">"
+    | Tabbrev(ti,ta) -> (t_to_string ti) ^ " : " ^ (t_to_string ta)
     | Tuvar({index = i;subst = a}) -> string_of_int i ^ "()"
 and targ_to_string = function
   | TA_typ t -> t_to_string t
@@ -336,7 +339,6 @@ let tag_to_string = function
   | Enum -> "Enum"
   | Spec -> "Spec"
 
-
 let tannot_to_string = function
   | None -> "No tannot"
   | Some((vars,t),tag,ncs,ef) ->
@@ -379,21 +381,27 @@ and o_to_order o =
     | Odec -> Ord_dec), Parse_ast.Unknown)
 
 
-let get_abbrev d_env t =
+let rec 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,efct)) ->
-	  Some(subst params t cs efct)
-	| _ -> None)
+	| Some(Some((params,ta),tag,cs,efct)) ->
+          let ta,cs,efct = subst params ta cs efct in
+          let ta,cs',efct' = get_abbrev d_env ta in
+          (match ta.t with
+          | Tabbrev(t',ta) -> ({t=Tabbrev({t=Tabbrev(t,t')},ta)},cs@cs',union_effects efct efct')
+          | _ -> ({t = Tabbrev(t,ta)},cs,efct))
+	| _ -> t,[],pure_e)
     | Tapp(i,args) ->
       (match Envmap.apply d_env.abbrevs i with
-	| Some(Some((params,t),tag,cs,efct)) ->
+	| Some(Some((params,ta),tag,cs,efct)) ->
 	  let env = Envmap.from_list2 (List.map fst params) args in
-	  Some(t_subst env t, cs_subst env cs, e_subst env efct)
-	| _ -> None)
-    | _ -> None
-
+          let ta,cs',efct' = get_abbrev d_env (t_subst env ta) in
+          (match ta.t with
+          | Tabbrev(t',ta) -> ({t=Tabbrev({t=Tabbrev(t,t')},ta)},cs_subst env (cs@cs'),e_subst env (union_effects efct efct'))
+          | _ -> ({t = Tabbrev(t,ta)},cs_subst env cs,e_subst env efct))
+	| _ -> t,[],pure_e)
+    | _ -> t,[],pure_e
 
 let eq_error l msg = raise (Reporting_basic.err_typ l msg)
 
@@ -457,63 +465,37 @@ let rec nexp_eq n1 n2 =
 
 (*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*)
-let rec type_consistent l d_env t1 t2 = 
+let rec type_consistent_internal l d_env t1 cs1 t2 cs2 = 
+  let t1,cs1',_ = get_abbrev d_env t1 in
+  let t2,cs2',_ = get_abbrev d_env t2 in
+  let cs1,cs2 = cs1@cs1',cs2@cs2' in
   match t1.t,t2.t with
+  | Tabbrev(_,t1),Tabbrev(_,t2) -> type_consistent_internal l d_env t1 cs1 t2 cs2
+  | Tabbrev(_,t1),_ -> type_consistent_internal l d_env t1 cs1 t2 cs2
+  | _,Tabbrev(_,t2) -> type_consistent_internal l d_env t1 cs1 t2 cs2
   | 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,e1),Some(t2,cs2,e2) ->
-	let t',cs' = type_consistent l d_env t1 t2 in
-	t',cs1@cs2@cs'
-      | Some(t1,cs1,e1),None ->
-	let t',cs' = type_consistent l d_env t1 t2 in
-	t',cs1@cs'
-      | None,Some(t2,cs2,e2) ->
-	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"))
+    if v1 = v2 then (t2,cs1@cs2) 
+    else 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)])
+    else (t2, cs1@cs2@[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,e1),Some(t2,cs2,e2) ->
-	  let t',cs' = type_consistent l d_env t1 t2 in
-	  t',cs1@cs2@cs'
-	| Some(t1,cs1,e1),None ->
-	  let t',cs' = type_consistent l d_env t1 t2 in
-	  t',cs1@cs'
-	| None,Some(t2,cs2,e2) ->
-	  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"))
+    if id1=id2 && la1 = la2 then (t2,cs1@cs2@(List.flatten (List.map2 (type_arg_eq l d_env) args1 args2)))
+    else 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 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)
+    (t2,cs1@cs2@cin@cout)
   | Ttup t1s, Ttup t2s ->
-    (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,[])
-  | _,_ ->
-    (match get_abbrev d_env t1,get_abbrev d_env t2 with
-      | Some(t1,cs1,e1),Some(t2,cs2,e2) ->
-	let t',cs' = type_consistent l d_env t1 t2 in
-	t',cs1@cs2@cs'
-      | Some(t1,cs1,e1),None ->
-	let t',cs' = type_consistent l d_env t1 t2 in
-	t',cs1@cs'
-      | None,Some(t2,cs2,e2) ->
-	let t',cs' = type_consistent l d_env t1 t2 in
-	t',cs2@cs'
-      | None,None -> eq_error l ("Type mismatch found " ^ (t_to_string t1) ^ " but expected a " ^ (t_to_string t2)))
+    (t2,cs1@cs2@(List.flatten (List.map snd (List.map2 (type_consistent l d_env) t1s t2s))))
+  | Tuvar _, t -> t1.t <- t2.t; (t2,cs1@cs2)
+  | t,Tuvar _ -> t2.t <- t1.t; (t2,cs1@cs2)
+  | _,_ -> eq_error l ("Type mismatch found " ^ (t_to_string t1) ^ " but expected a " ^ (t_to_string t2))
 
 and type_arg_eq l d_env ta1 ta2 = 
   match ta1,ta2 with
@@ -523,8 +505,17 @@ and type_arg_eq l d_env ta1 ta2 =
   | 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 d_env t1 e t2 = 
+and type_consistent l d_env t1 t2 =
+  type_consistent_internal l d_env t1 [] t2 []
+
+let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 = 
+  let t1,cs1',_ = get_abbrev d_env t1 in
+  let t2,cs2',_ = get_abbrev d_env t2 in
+  let cs1,cs2 = cs1@cs1',cs2@cs2' in
   match t1.t,t2.t with
+  | Tabbrev(_,t1),Tabbrev(_,t2) -> type_coerce_internal l d_env t1 cs1 e t2 cs2
+  | Tabbrev(_,t1),_ -> type_coerce_internal l d_env t1 cs1 e t2 cs2
+  | _,Tabbrev(_,t2) -> type_coerce_internal l d_env t1 cs1 e t2 cs2
   | Ttup t1s, Ttup t2s ->
     let tl1,tl2 = List.length t1s,List.length t2s in
     if tl1=tl2 then 
@@ -583,18 +574,7 @@ let rec type_coerce l d_env t1 e t2 =
 	  (t',cs,E_aux(E_cast(t_to_typ t',e),(l,Some(([],t2),External None,cs,pure_e))))
 	| _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded"))			     
     | _,_ -> 
-      (match get_abbrev d_env t1,get_abbrev d_env t2 with
-	| Some(t1,cs1,ef1),Some(t2,cs2,ef2) ->
-	  let t',cs',e' = type_coerce l d_env t1 e t2 in
-	  (t',cs1@cs2@cs',e')
-	| Some(t1,cs1,ef1),None ->
-	  let t',cs',e' = type_coerce l d_env t1 e t2 in
-	  (t',cs1@cs',e')
-	| None,Some(t2,cs2,ef2) ->
-	  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)))
+      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,[],pure_e))),
@@ -602,51 +582,32 @@ let rec type_coerce l d_env t1 e t2 =
 			  E_aux(E_lit(L_aux(L_one,l)),(l,Some(([],bit_t),Emp,[],pure_e)))),
 		     (l,Some(([],bit_t),Emp,cs',pure_e))))
   | Tapp("enum",[TA_nexp b1;TA_nexp r1;]),Tid(i) -> 
-    (match get_abbrev d_env t2 with
-      | Some(t2,cs2,ef2) ->
-	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,[],pure_e))),
-								E_aux(E_id(Id_aux(Id a,l)),
-								      (l,Some(([],t2),Emp,[],pure_e)))),
-							(l,Some(([],t2),Emp,[],pure_e)))) enums),
-		   (l,Some(([],t2),Emp,[],pure_e))))
-	  | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2))))
+    (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,[],pure_e))),
+							  E_aux(E_id(Id_aux(Id a,l)),
+								(l,Some(([],t2),Emp,[],pure_e)))),
+						  (l,Some(([],t2),Emp,[],pure_e)))) enums),
+	     (l,Some(([],t2),Emp,[],pure_e))))
+    | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2)))
   | Tid("bit"),Tid("bool") ->
     let e' = E_aux(E_app((Id_aux(Id "is_one",l)),[e]),(l,Some(([],bool_t),External None,[],pure_e))) in
     (t2,[],e')
   | Tid(i),Tapp("enum",[TA_nexp b1;TA_nexp r1;]) -> 
-    (match get_abbrev d_env t1 with
-      | Some(t1,cs1,ef1) ->
-	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,[],pure_e))),
-								E_aux(E_lit(L_aux((L_num i),l)),
-								      (l,Some(([],t2),Emp,[],pure_e)))),
-							(l,Some(([],t2),Emp,[],pure_e)))) enums),
-		   (l,Some(([],t2),Emp,[],pure_e))))
-	  | 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,ef1),Some(t2,cs2,ef2) -> 
-	let t',cs',e' = type_coerce l d_env t1 e t2 in
-	(t',cs'@cs1@cs2,e')
-      | Some(t1,cs1,ef1),None ->
-	let t',cs',e' = type_coerce l d_env t1 e t2 in
-	(t',cs'@cs1,e')
-      | None,Some(t2,cs2,ef2) ->
-	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))
+    (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,[],pure_e))),
+							  E_aux(E_lit(L_aux((L_num i),l)),
+								(l,Some(([],t2),Emp,[],pure_e)))),
+						  (l,Some(([],t2),Emp,[],pure_e)))) enums),
+	     (l,Some(([],t2),Emp,[],pure_e))))
+    | None -> eq_error l ("Type mismatch: " ^ (t_to_string t1) ^ " , " ^ (t_to_string t2)))
+  | _,_ -> let t',cs = type_consistent l d_env t1 t2 in (t',cs,e)
+
+and type_coerce l d_env t1 e t2 = type_coerce_internal l d_env t1 [] e t2 []
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 63583d28..785f3c76 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -25,6 +25,7 @@ and t_aux =
   | Tfn of t * t * effect
   | Ttup of t list
   | Tapp of string * t_arg list
+  | Tabbrev of t * t (* first t is the specified type, which may itself be an abbrev; second is the ground type, never an abbrev *)
   | Tuvar of t_uvar
 and nexp = { mutable nexp : nexp_aux }
 and nexp_aux =
@@ -111,14 +112,14 @@ val new_o : unit -> order
 val new_e : unit -> effect
 
 val subst : (string * kind) list -> t -> nexp_range list -> effect -> t * nexp_range list * effect
-val get_abbrev : def_envs -> t -> (t * nexp_range list * effect) option
+val get_abbrev : def_envs -> t -> (t * nexp_range list * effect)
 
 (* type_consistent is similar to a standard type equality, except in the case of [[consistent t1 t2]] where
    t1 and t2 are both enum types and t1 is contained within the range of t2: i.e.
-   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
+   enum 2 5 is consistent with enum 0 10, but not vice versa.
+   type_consistent mutates uvars to perform unification and will raise an error if the [[t1]] and [[t2]] are inconsistent
 *)
 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 *)
+(* type_eq mutates to unify variables, and will raise an exception if the first type cannot be coerced into the second and is inconsistent *)
 val type_coerce : Parse_ast.l -> def_envs -> t -> exp -> t -> t * nexp_range list * exp