Writing to concatenated aliases

5 files changed, 110 insertions, 100 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index d14fdc59..3c1ab601 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -614,14 +614,15 @@ let to_ast_alias_spec k_env (Parse_ast.E_aux(e,le)) =
   AL_aux(
     (match e with
       | Parse_ast.E_field(Parse_ast.E_aux(Parse_ast.E_id id,li), field) -> 
-	AL_subreg(to_ast_id id,to_ast_id field)
+	AL_subreg(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_id field)
       | Parse_ast.E_vector_access(Parse_ast.E_aux(Parse_ast.E_id id,li),range) ->
-	AL_bit(to_ast_id id,to_ast_exp k_env range)
+	AL_bit(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_exp k_env range)
       | Parse_ast.E_vector_subrange(Parse_ast.E_aux(Parse_ast.E_id id,li),base,stop) ->
-	AL_slice(to_ast_id id,to_ast_exp k_env base,to_ast_exp k_env stop)
+	AL_slice(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_exp k_env base,to_ast_exp k_env stop)
       | Parse_ast.E_vector_append(Parse_ast.E_aux(Parse_ast.E_id first,lf),
 				  Parse_ast.E_aux(Parse_ast.E_id second,ls)) ->
-	AL_concat(to_ast_id first,to_ast_id second)
+	AL_concat(RI_aux(RI_id (to_ast_id first),(lf,NoTyp)),
+		  RI_aux(RI_id (to_ast_id second),(ls,NoTyp)))
     ), (le,NoTyp))      
 
 let to_ast_dec (names,k_env,t_env) (Parse_ast.DEC_aux(regdec,l)) =
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index cf2ca43d..e2d6b781 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1560,53 +1560,62 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	    (match in_env aliases id with
 	      | Just (AL_aux aspec (l,_)) -> 
 		(match aspec with
-		  | AL_subreg reg subreg ->
-		    (match in_env regs reg with
-		      | Just (V_register (Reg _ (Just((T_id id),_,_,_)))) ->
-			(match in_env subregs (Id_aux (Id id) Unknown) with
-			  | Just indexes -> 
-			    (match in_env indexes subreg with
-			      | Just ir -> 
-				(Action (Write_reg (SubReg subreg (Reg reg annot) ir) Nothing value) 
-				   (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
-				      t_level l_env l_mem Top), l_mem, l_env)
-			      | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
-			    | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " id), l_mem, l_env) end)
-			| Just (V_register ((Reg _ (Just((T_abbrev (T_id id) _),_,_,_))) as rf)) ->
-			  (match in_env subregs (Id_aux (Id id) Unknown) with
-			    | Just indexes -> 
-			      (match in_env indexes subreg with
-				| Just ir -> 
-				  (Action (Write_reg (SubReg subreg (Reg reg annot) ir) Nothing value) 
-				     (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
-					t_level l_env l_mem Top), l_mem, l_env)
-				| _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
-			    | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " id), l_mem, l_env) end)
-			| _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register " (get_id reg)),l_mem,l_env) end)
-		    | AL_bit reg e ->
-		      resolve_outcome (interp_main mode t_level l_env l_mem e) 
-			(fun v le lm -> match v with 
-			  | V_lit (L_aux (L_num i) _) -> 
-			    (Action (Write_reg (Reg reg annot) (Just (i,i)) value) 
+		  | AL_subreg (RI_aux (RI_id reg)  (li, ((Just((T_id id),_,_,_)) as annot'))) subreg ->
+		    (match in_env subregs (Id_aux (Id id) Unknown) with
+		      | Just indexes -> 
+			(match in_env indexes subreg with
+			  | Just ir -> 
+			    (Action (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing value) 
 			       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
-				  t_level l_env l_mem Top), l_mem, l_env) end)
-			(fun a -> a)
-		    | AL_slice reg start stop -> 
-		      resolve_outcome (interp_main mode t_level l_env l_mem start)
-			(fun v lm le -> 
-			  match v with 
-			    | V_lit (L_aux (L_num start) _) ->
-			      (resolve_outcome (interp_main mode t_level l_env lm stop)
-			         (fun v le lm ->
-				   (match v with
-				     | V_lit (L_aux (L_num stop) _) ->
-				       (Action (Write_reg (Reg reg annot) (Just (start,stop)) value) 
-					  (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
-					     t_level l_env l_mem Top),
-					l_mem, l_env) end))
-				 (fun a -> a)) end)
-			(fun a -> a)
-		    | AL_concat reg1 reg2 -> (Error l "Unimplemented yet, alias spec concat", l_mem, l_env) end)
+				  t_level l_env l_mem Top), l_mem, l_env)
+			  | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
+		      | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " id), l_mem, l_env) end)
+		  | AL_subreg (RI_aux (RI_id reg) (li, ((Just((T_abbrev (T_id id) _),_,_,_)) as annot'))) subreg ->
+		    (match in_env subregs (Id_aux (Id id) Unknown) with
+		      | Just indexes -> 
+			(match in_env indexes subreg with
+			  | Just ir -> 
+			    (Action (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing value) 
+			       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+				  t_level l_env l_mem Top), l_mem, l_env)
+			  | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
+		      | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " id), l_mem, l_env) end)
+		  | AL_bit (RI_aux (RI_id reg) (_,annot')) e ->
+		    resolve_outcome (interp_main mode t_level l_env l_mem e) 
+		      (fun v le lm -> match v with 
+			| V_lit (L_aux (L_num i) _) -> 
+			  (Action (Write_reg (Reg reg annot') (Just (i,i)) value) 
+			     (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+				t_level l_env l_mem Top), l_mem, l_env) end)
+		      (fun a -> a)
+		  | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop -> 
+		    resolve_outcome (interp_main mode t_level l_env l_mem start)
+		      (fun v lm le -> 
+			match v with 
+			  | V_lit (L_aux (L_num start) _) ->
+			    (resolve_outcome (interp_main mode t_level l_env lm stop)
+			       (fun v le lm ->
+				 (match v with
+				   | V_lit (L_aux (L_num stop) _) ->
+				     (Action (Write_reg (Reg reg annot') (Just (start,stop)) value) 
+					(Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+					   t_level l_env l_mem Top),
+				      l_mem, l_env) end))
+			       (fun a -> a)) end)
+		      (fun a -> a)
+		  | AL_concat (RI_aux (RI_id reg1) (l1,annot1)) (RI_aux (RI_id reg2) annot2) -> 
+		    let val_typ t = match t with
+			  | T_app "register" (T_args [T_arg_typ t]) -> t
+			  | T_abbrev _ (T_app "register" (T_args [T_arg_typ t])) -> t end in
+		    let (t1,t2) = match (annot1,annot2) with
+		      | (Just (t1,_,_,_), (_,(Just (t2,_,_,_)))) -> (val_typ t1,val_typ t2) end in
+                   (match (t1,t2) with
+		      | (T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); _;_]),
+			 T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); _;_])) ->
+			(Action (Write_reg (Reg reg1 annot1) Nothing (slice_vector value b1 r1))
+			        (Thunk_frame (E_aux (E_assign (LEXP_aux (LEXP_id reg2) annot2)
+						              (to_exp (slice_vector value (r1+1) r2))) annot2)
+				              t_level l_env l_mem Top), l_mem,l_env) end) end)
 	    | _ -> (Error l (String.stringAppend "Internal error: alias not found for id " (get_id id)),l_mem,l_env) end) in
 	  (request,Nothing)
         | _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than extern, empty, or alias " (get_id id)),l_mem,l_env),Nothing)
@@ -1814,43 +1823,38 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
       | T_abbrev (T_id i) _ -> i
     end in
   match alspec with
-    | AL_subreg reg subreg ->
-      (match in_env regs reg with
-	| Just (V_register (Reg _ (Just (t,_,_,_)))) ->
-	  let reg_ti = get_reg_typ_name t in
-	  (match in_env subregs (Id_aux (Id reg_ti) Unknown) with
-	    | Just indexes -> 
-	      (match in_env indexes subreg with
-		| Just ir -> (Action (Read_reg (SubReg subreg (Reg reg annot) ir) Nothing) stack, l_mem, l_env)
-		| _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
-	    | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " reg_ti), l_mem, l_env) end)
-	| _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register " (get_id reg)),l_mem,l_env) end)
-    | AL_bit reg e ->
+    | AL_subreg (RI_aux (RI_id reg) (li,((Just (t,_,_,_)) as annot'))) subreg ->
+      let reg_ti = get_reg_typ_name t in
+      (match in_env subregs (Id_aux (Id reg_ti) Unknown) with
+	| Just indexes -> 
+	  (match in_env indexes subreg with
+	    | Just ir -> (Action (Read_reg (SubReg subreg (Reg reg annot') ir) Nothing) stack, l_mem, l_env)
+	    | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
+	| _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " reg_ti), l_mem, l_env) end)
+    | AL_bit (RI_aux (RI_id reg) (_,annot')) e ->
       resolve_outcome (interp_main mode t_level l_env l_mem e) 
-                      (fun v le lm -> match v with 
-			| V_lit (L_aux (L_num i) _) -> 
-			  (Action (Read_reg (Reg reg annot) (Just (i,i))) stack, l_mem, l_env) end)
-                      (fun a -> a) (*Should not currently happen as type system enforces constants*)
-    | AL_slice reg start stop -> 
+        (fun v le lm -> match v with 
+	  | V_lit (L_aux (L_num i) _) -> 
+	    (Action (Read_reg (Reg reg annot') (Just (i,i))) stack, l_mem, l_env) end)
+        (fun a -> a) (*Should not currently happen as type system enforces constants*)
+    | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop -> 
       resolve_outcome (interp_main mode t_level l_env l_mem start)
-                      (fun v lm le -> 
-			match v with 
-			  | V_lit (L_aux (L_num start) _) ->
-			    (resolve_outcome 
-			       (interp_main mode t_level l_env lm stop)
-			       (fun v le lm ->
-				 (match v with
-				   | V_lit (L_aux (L_num stop) _) ->
-				     (Action (Read_reg (Reg reg annot) (Just (start,stop))) stack, l_mem, l_env) end))
-			       (fun a -> a)) end)
-                      (fun a -> a) (*Neither action function should occur, due to above*)
-    | AL_concat reg1 reg2 -> 
-      (Action (Read_reg (Reg reg1 annot) Nothing)
+        (fun v lm le -> 
+	  match v with 
+	    | V_lit (L_aux (L_num start) _) ->
+	      (resolve_outcome 
+		 (interp_main mode t_level l_env lm stop)
+		 (fun v le lm ->
+		   (match v with
+		     | V_lit (L_aux (L_num stop) _) ->
+		       (Action (Read_reg (Reg reg annot') (Just (start,stop))) stack, l_mem, l_env) end))
+		 (fun a -> a)) end)
+        (fun a -> a) (*Neither action function should occur, due to above*)
+    | AL_concat (RI_aux (RI_id reg1) (l1, annot1)) (RI_aux (RI_id reg2) annot2) -> 
+      (Action (Read_reg (Reg reg1 annot1) Nothing)
 	      (Hole_frame (Id_aux (Id "0") Unknown)
-		          (E_aux (E_vector_append (E_aux (E_id (Id_aux (Id "0") l)) (l, (intern_annot annot)))
-				                  (E_aux (E_id reg2) 
-						         (l, (Just ((T_app "register" (T_args [T_arg_typ (T_var "fresh")])),
-								   (Tag_extern (Just (get_id reg2))), [], pure)))))
+		          (E_aux (E_vector_append (E_aux (E_id (Id_aux (Id "0") l1)) (l1, (intern_annot annot1)))
+    				                  (E_aux (E_id reg2) annot2)) 
 			        (l,(intern_annot annot))) t_level l_env l_mem Top), l_mem,l_env) end
 
 let rec to_global_letbinds (Defs defs) t_level =
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index ea6a893b..f4729814 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -496,15 +496,17 @@ let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) =
     pp_lem_l l pp_annot annot
 
 let pp_lem_aspec ppf (AL_aux(aspec,(l,annot))) =
+  let pp_reg_id ppf (RI_aux((RI_id ri),(l,annot))) =
+    fprintf ppf "@[<0>(RI_aux (RI_id %a) (%a,%a))@]" pp_lem_id ri pp_lem_l l pp_annot annot in
   match aspec with
     | AL_subreg(reg,subreg) -> 
-      fprintf ppf "@[<0>(AL_aux (AL_subreg %a %a) (%a,%a))@]" pp_lem_id reg pp_lem_id subreg pp_lem_l l pp_annot annot
+      fprintf ppf "@[<0>(AL_aux (AL_subreg %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_id subreg pp_lem_l l pp_annot annot
     | AL_bit(reg,ac) ->
-      fprintf ppf "@[<0>(AL_aux (AL_bit %a %a) (%a,%a))@]" pp_lem_id reg pp_lem_exp ac pp_lem_l l pp_annot annot
+      fprintf ppf "@[<0>(AL_aux (AL_bit %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_exp ac pp_lem_l l pp_annot annot
     | AL_slice(reg,b,e) ->
-      fprintf ppf "@[<0>(AL_aux (AL_slice %a %a %a) (%a,%a))@]" pp_lem_id reg pp_lem_exp b pp_lem_exp e pp_lem_l l pp_annot annot
+      fprintf ppf "@[<0>(AL_aux (AL_slice %a %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_exp b pp_lem_exp e pp_lem_l l pp_annot annot
     | AL_concat(f,s) ->
-      fprintf ppf "@[<0>(AL_aux (AL_concat %a %a) (%a,%a))@]" pp_lem_id f pp_lem_id s pp_lem_l l pp_annot annot
+      fprintf ppf "@[<0>(AL_aux (AL_concat %a %a) (%a,%a))@]" pp_reg_id f pp_reg_id s pp_lem_l l pp_annot annot
 
 let pp_lem_dec ppf (DEC_aux(reg,(l,annot))) =
   match reg with 
@@ -1033,10 +1035,10 @@ let doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),_)) =
 
 let doc_alias (AL_aux (alspec,_)) =
   match alspec with
-    | AL_subreg(id,subid) -> doc_id id ^^ dot ^^ doc_id subid
-    | AL_bit(id,ac) -> doc_id id ^^ brackets (doc_exp ac)
-    | AL_slice(id,b,e) -> doc_id id ^^ brackets (doc_op dotdot (doc_exp b) (doc_exp e))
-    | AL_concat(f,s) -> doc_op colon (doc_id f) (doc_id s)
+    | AL_subreg((RI_aux (RI_id id,_)),subid) -> doc_id id ^^ dot ^^ doc_id subid
+    | AL_bit((RI_aux (RI_id id,_)),ac) -> doc_id id ^^ brackets (doc_exp ac)
+    | AL_slice((RI_aux (RI_id id,_)),b,e) -> doc_id id ^^ brackets (doc_op dotdot (doc_exp b) (doc_exp e))
+    | AL_concat((RI_aux (RI_id f,_)),(RI_aux (RI_id s,_))) -> doc_op colon (doc_id f) (doc_id s)
 
 let doc_dec (DEC_aux (reg,_)) =
   match reg with
diff --git a/src/test/regbits.sail b/src/test/regbits.sail
index 53f03da8..469f0f79 100644
--- a/src/test/regbits.sail
+++ b/src/test/regbits.sail
@@ -25,5 +25,6 @@ function (bit[64]) main _ = {
   XER.FOOBAR := 0b11;
   XER.FOOBAR := foobar;
   query := doub[13];
+  doub := XER:XER;
   XER }
 
diff --git a/src/type_check.ml b/src/type_check.ml
index d0274d72..40a5f04c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1062,7 +1062,9 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
             (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)
+	    let u = match t.t with
+	      | Tapp("register", [TA_typ u]) -> u in
+            (LEXP_aux(lexp,(l,Base(([],t'),Alias,[],ef))), u, 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
@@ -1444,7 +1446,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
 (*TODO Only works for inc vectors, need to add support for dec*)
 let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
   let (Env(d_env,t_env)) = envs in
-  let check_reg (Id_aux(_,l) as id) : (string * typ * typ) =
+  let check_reg (RI_aux ((RI_id (Id_aux(_,l) as id)), _)) : (string * tannot reg_id * typ * typ) =
     let i = id_to_string id in
     (match Envmap.apply t_env i with
       | Some(Base(([],t), External (Some j), [], _)) ->
@@ -1454,14 +1456,14 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
           | _ -> t,t in
 	(match t_actual.t with 
 	  | Tapp("register",[TA_typ t']) -> 
-	    if i = j then (i,t_id,t')
+	    if i = j then (i,(RI_aux (RI_id id, (l,Base(([],t),External (Some j), [], pure_e)))),t_id,t')
 	    else assert false
 	  | _ -> typ_error l 
 	    ("register alias " ^ alias ^ " to " ^ i ^ " expected a register, found " ^ (t_to_string t)))
       | _ -> typ_error l ("register alias " ^ alias ^ " to " ^ i ^ " exepcted a register.")) in
   match al with
     | AL_subreg(reg_a,subreg) -> 
-      let (reg,reg_t,t) = check_reg reg_a in 
+      let (reg,reg_a,reg_t,t) = check_reg reg_a in 
       (match reg_t.t with
 	| Tid i ->
 	  (match lookup_record_typ i d_env.rec_env with
@@ -1477,7 +1479,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
 		  (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) -> 
-      let (reg,reg_t,t) = check_reg reg_a in
+      let (reg,reg_a,reg_t,t) = check_reg reg_a in
       let (E_aux(bit,(le,eannot)),_,_,_,_) = check_exp envs (new_t ()) bit in
       (match t.t with
 	| Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) ->
@@ -1491,7 +1493,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
 	      else typ_error ll ("Alias bit lookup must be in the range of the vector in the register")
 	    | _ -> assert false)
     | AL_slice(reg_a,sl1,sl2) -> 
-      let (reg,reg_t,t) = check_reg reg_a in 
+      let (reg,reg_a,reg_t,t) = check_reg reg_a in 
       let (E_aux(sl1,(le1,eannot1)),_,_,_,_) = check_exp envs (new_t ()) sl1 in
       let (E_aux(sl2,(le2,eannot2)),_,_,_,_) = check_exp envs (new_t ()) sl2 in
       (match t.t with
@@ -1509,8 +1511,8 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
 	      else typ_error ll ("Alias slices must be in the range of the vector in the register")
 	    | _ -> assert false)
     | AL_concat(reg1_a,reg2_a) -> 
-      let (reg1,reg_t,t1) = check_reg reg1_a in
-      let (reg2,reg_t,t2) = check_reg reg2_a in
+      let (reg1,reg1_a,reg_t,t1) = check_reg reg1_a in
+      let (reg2,reg2_a,reg_t,t2) = check_reg reg2_a in
       (match (t1.t,t2.t) with
 	| (Tapp("vector",[TA_nexp b1;TA_nexp r; TA_ord {order = Oinc}; TA_typ item_t]),
 	   Tapp("vector",[TA_nexp _ ;TA_nexp r2; TA_ord {order = Oinc}; TA_typ item_t2])) ->