Type check alias use in the left hand side of an assignment. Warning, interpreter still doesn't work with writes.

3 files changed, 18 insertions, 7 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index e952a457..b58ab263 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -367,7 +367,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       | Some(Base(tp,Default,cs,ef)) | Some(Base(tp,Spec,cs,ef)) ->
         typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use")
       | Some(Base((params,t),tag,cs,ef)) ->
-	let t,cs,ef = match tag with | Emp_global | External _ -> subst params t cs ef | _ -> t,cs,ef in
+	let t,cs,ef = match tag with | Emp_global | External _ -> subst params t cs ef | Alias -> t,cs, add_effect (BE_aux(BE_rreg, Parse_ast.Unknown)) ef | _ -> t,cs,ef in
         let t,cs' = get_abbrev d_env t in
         let cs = cs@cs' in
         let t_actual,expect_actual = match t.t,expect_t.t with
@@ -1053,6 +1053,15 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
       (match Envmap.apply t_env i with
 	| Some(Base((parms,t),Default,_,_)) ->
 	  typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists")
+        | Some(Base(([],t),Alias,_,_)) ->
+          (match Envmap.apply d_env.alias_env i with
+          | Some(OneReg(reg, (Base(([],t'),_,_,_)))) ->
+            let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
+            (LEXP_aux(lexp,(l,(Base(([],t'),Alias,[],ef)))), t, Envmap.empty, External (Some reg),[],ef)
+          | Some(TwoReg(reg1,reg2, (Base(([],t'),_,_,_)))) ->
+            let ef = {effect=Eset [BE_aux(BE_wreg,l)]} in
+            (LEXP_aux(lexp,(l,Base(([],t'),Alias,[],ef))), t, Envmap.empty, External None,[],ef)
+          | _ -> assert false)
 	| Some(Base((parms,t),tag,cs,_)) ->
 	  let t,cs,_ = match tag with | External _ | Emp_global -> subst parms t cs pure_e | _ -> t,cs,pure_e in
 	  let t,cs' = get_abbrev d_env t in
@@ -1462,7 +1471,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
                 | Overload _ ->  raise (Reporting_basic.err_unreachable l "Record given overload annot")
 		| Base(([],et),tag,cs,ef) ->
 		  let tannot = Base(([],et),Alias,[],pure_e) in
-		  let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (reg,tannot))} 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.printf "%s\n" (t_to_string reg_t) in assert false)
     | AL_bit(reg_a,bit) -> 
@@ -1475,7 +1484,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
 	      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) in
 		   let d_env = 
-		     {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (reg,tannot))} in
+		     {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)
@@ -1492,7 +1501,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
 					      TA_ord order; TA_typ item_t])} in 
 		   let tannot = Base(([],t),Alias,[],pure_e) in
 		   let d_env = 
-		     {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (reg,tannot))} in
+		     {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in
 		   (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")
@@ -1506,7 +1515,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
 	  let _ = type_consistent (Specc l) d_env item_t item_t2 in
 	  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) in
-	  let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (reg1,tannot))} 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))
 
 (*val check_def : envs -> tannot def -> (tannot def) envs_out*)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 880d317a..9834552e 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -103,13 +103,14 @@ type 'a emap = 'a Envmap.t
 
 type rec_kind = Record | Register
 type rec_env = (string * rec_kind * ((string * tannot) list))
+type alias_kind = OneReg of string * tannot | TwoReg of string * string * tannot | MultiReg of (string list) * tannot
 type def_envs = { 
   k_env: kind emap; 
   abbrevs: tannot emap; 
   namesch : tannot emap; 
   enum_env : (string list) emap; 
   rec_env : rec_env list;
-  alias_env : (string * tannot) emap;
+  alias_env : alias_kind emap;
  }  
 
 type exp = tannot Ast.exp
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 063ee088..fb4f1948 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -101,13 +101,14 @@ type 'a emap = 'a Envmap.t
 
 type rec_kind = Record | Register
 type rec_env = (string * rec_kind * ((string * tannot) list))
+type alias_kind = OneReg of string * tannot | TwoReg of string * string * tannot | MultiReg of (string list) * tannot
 type def_envs = { 
   k_env: kind emap; 
   abbrevs: tannot emap; 
   namesch : tannot emap; 
   enum_env : (string list) emap; 
   rec_env : rec_env list;
-  alias_env : (string * tannot) emap;
+  alias_env : alias_kind emap;
  }
 
 type exp = tannot Ast.exp