Writing to concatenated aliases

8 files changed, 267 insertions, 237 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 60b566a9..a9bba453 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -29,24 +29,20 @@ type base_kind_aux =  (* base kind *)
  | BK_effect (* kind of effect sets *)
 
 
-type base_kind = 
- | BK_aux of base_kind_aux * l
-
-
 type kid_aux =  (* variables with kind, ticked to differntiate from program variables *)
  | Var of x
 
 
-type kind_aux =  (* kinds *)
- | K_kind of list base_kind
+type base_kind = 
+ | BK_aux of base_kind_aux * l
 
 
 type kid = 
  | Kid_aux of kid_aux * l
 
 
-type kind = 
- | K_aux of kind_aux * l
+type kind_aux =  (* kinds *)
+ | K_kind of list base_kind
 
 
 type nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
@@ -61,6 +57,10 @@ and nexp =
  | Nexp_aux of nexp_aux * l
 
 
+type kind = 
+ | K_aux of kind_aux * l
+
+
 type base_effect_aux =  (* effect *)
  | BE_rreg (* read register *)
  | BE_wreg (* write register *)
@@ -109,11 +109,6 @@ let effect_union e1 e2 =
   end
 
 
-type kinded_id_aux =  (* optionally kind-annotated identifier *)
- | KOpt_none of kid (* identifier *)
- | KOpt_kind of kind * kid (* kind-annotated variable *)
-
-
 type n_constraint_aux =  (* constraint over kind $Nat$ *)
  | NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
@@ -121,14 +116,19 @@ type n_constraint_aux =  (* constraint over kind $Nat$ *)
  | NC_nat_set_bounded of kid * list integer
 
 
-type kinded_id = 
- | KOpt_aux of kinded_id_aux * l
+type kinded_id_aux =  (* optionally kind-annotated identifier *)
+ | KOpt_none of kid (* identifier *)
+ | KOpt_kind of kind * kid (* kind-annotated variable *)
 
 
 type n_constraint = 
  | NC_aux of n_constraint_aux * l
 
 
+type kinded_id = 
+ | KOpt_aux of kinded_id_aux * l
+
+
 type quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
  | QI_id of kinded_id (* An optionally kinded identifier *)
  | QI_const of n_constraint (* A constraint for this type *)
@@ -143,6 +143,19 @@ type typquant_aux =  (* type quantifiers and constraints *)
  | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
+type lit_aux =  (* Literal constant *)
+ | L_unit (* $() : unit$ *)
+ | L_zero (* $bitzero : bit$ *)
+ | L_one (* $bitone : bit$ *)
+ | L_true (* $true : bool$ *)
+ | L_false (* $false : bool$ *)
+ | L_num of integer (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_undef (* constant representing undefined values *)
+ | L_string of string (* string constant *)
+
+
 type typquant = 
  | TypQ_aux of typquant_aux * l
 
@@ -168,29 +181,12 @@ and typ_arg =
  | Typ_arg_aux of typ_arg_aux * l
 
 
-type lit_aux =  (* Literal constant *)
- | L_unit (* $() : unit$ *)
- | L_zero (* $bitzero : bit$ *)
- | L_one (* $bitone : bit$ *)
- | L_true (* $true : bool$ *)
- | L_false (* $false : bool$ *)
- | L_num of integer (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_undef (* constant representing undefined values *)
- | L_string of string (* string constant *)
-
-
-type typschm_aux =  (* type scheme *)
- | TypSchm_ts of typquant * typ
-
-
 type lit = 
  | L_aux of lit_aux * l
 
 
-type typschm = 
- | TypSchm_aux of typschm_aux * l
+type typschm_aux =  (* type scheme *)
+ | TypSchm_ts of typquant * typ
 
 
 type pat_aux 'a =  (* Pattern *)
@@ -217,7 +213,22 @@ and fpat 'a =
  | FP_aux of (fpat_aux 'a) * annot 'a
 
 
-type exp_aux 'a =  (* Expression *)
+type typschm = 
+ | TypSchm_aux of typschm_aux * l
+
+
+type reg_id_aux 'a = 
+ | RI_id of id
+
+
+type letbind_aux 'a =  (* Let binding *)
+ | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *)
+ | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *)
+
+and letbind 'a = 
+ | LB_aux of (letbind_aux 'a) * annot 'a
+
+and exp_aux 'a =  (* Expression *)
  | E_block of list (exp 'a) (* block *)
  | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *)
  | E_id of id (* identifier *)
@@ -286,34 +297,29 @@ and pexp_aux 'a =  (* Pattern match *)
 and pexp 'a = 
  | Pat_aux of (pexp_aux 'a) * annot 'a
 
-and letbind_aux 'a =  (* Let binding *)
- | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *)
- | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *)
 
-and letbind 'a = 
- | LB_aux of (letbind_aux 'a) * annot 'a
+type reg_id 'a = 
+ | RI_aux of (reg_id_aux 'a) * annot 'a
 
 
 type alias_spec_aux 'a =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
- | AL_subreg of id * id (* id must refer to a register, id' to a declared subregister of id *)
- | AL_bit of id * (exp 'a)
- | AL_slice of id * (exp 'a) * (exp 'a)
- | AL_concat of id * id (* both id and id' must refer to a register *)
+ | AL_subreg of (reg_id 'a) * id
+ | AL_bit of (reg_id 'a) * (exp 'a)
+ | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a)
+ | AL_concat of (reg_id 'a) * (reg_id 'a)
 
 
-type type_union_aux =  (* Type union constructors *)
- | Tu_id of id
- | Tu_ty_id of typ * id
+type rec_opt_aux =  (* Optional recursive annotation for functions *)
+ | Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
 
 
-type name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
- | Name_sect_none
- | Name_sect_some of string
+type funcl_aux 'a =  (* Function clause *)
+ | FCL_Funcl of id * (pat 'a) * (exp 'a)
 
 
-type rec_opt_aux =  (* Optional recursive annotation for functions *)
- | Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+type tannot_opt_aux =  (* Optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
 
 
 type effect_opt_aux =  (* Optional effect annotation for functions *)
@@ -321,55 +327,51 @@ type effect_opt_aux =  (* Optional effect annotation for functions *)
  | Effect_opt_effect of effect
 
 
-type tannot_opt_aux =  (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
+type name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+ | Name_sect_none
+ | Name_sect_some of string
 
 
-type funcl_aux 'a =  (* Function clause *)
- | FCL_Funcl of id * (pat 'a) * (exp 'a)
+type type_union_aux =  (* Type union constructors *)
+ | Tu_id of id
+ | Tu_ty_id of typ * id
 
 
 type alias_spec 'a = 
  | AL_aux of (alias_spec_aux 'a) * annot 'a
 
 
-type type_union = 
- | Tu_aux of type_union_aux * l
-
-
-type name_scm_opt = 
- | Name_sect_aux of name_scm_opt_aux * l
-
+type rec_opt = 
+ | Rec_aux of rec_opt_aux * l
 
-type index_range_aux =  (* index specification, for bitfields in register types *)
- | BF_single of integer (* single index *)
- | BF_range of integer * integer (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
 
-and index_range = 
- | BF_aux of index_range_aux * l
+type funcl 'a = 
+ | FCL_aux of (funcl_aux 'a) * l
 
 
-type rec_opt = 
- | Rec_aux of rec_opt_aux * l
+type tannot_opt = 
+ | Typ_annot_opt_aux of tannot_opt_aux * l
 
 
 type effect_opt = 
  | Effect_opt_aux of effect_opt_aux * l
 
 
-type tannot_opt = 
- | Typ_annot_opt_aux of tannot_opt_aux * l
+type name_scm_opt = 
+ | Name_sect_aux of name_scm_opt_aux * l
 
 
-type funcl 'a = 
- | FCL_aux of (funcl_aux 'a) * l
+type type_union = 
+ | Tu_aux of type_union_aux * l
 
 
-type val_spec_aux 'a =  (* Value type specification *)
- | VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
+type index_range_aux =  (* index specification, for bitfields in register types *)
+ | BF_single of integer (* single index *)
+ | BF_range of integer * integer (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
+
+and index_range = 
+ | BF_aux of index_range_aux * l
 
 
 type dec_spec_aux 'a =  (* Register declarations *)
@@ -378,14 +380,6 @@ type dec_spec_aux 'a =  (* Register declarations *)
  | DEC_typ_alias of typ * id * (alias_spec 'a)
 
 
-type type_def_aux 'a =  (* Type definition body *)
- | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
- | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
- | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
- | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
-
-
 type fundef_aux 'a =  (* Function definition *)
  | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
 
@@ -399,23 +393,29 @@ type scattered_def_aux 'a =  (* Function and type union definitions that can be
  | SD_scattered_end of id (* scattered definition end *)
 
 
+type type_def_aux 'a =  (* Type definition body *)
+ | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
+ | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
+ | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
+ | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *)
+ | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
+
+
 type default_spec_aux 'a =  (* Default kinding or typing assumption *)
  | DT_kind of base_kind * kid
  | DT_typ of typschm * id
 
 
-type val_spec 'a = 
- | VS_aux of (val_spec_aux 'a) * annot 'a
+type val_spec_aux 'a =  (* Value type specification *)
+ | VS_val_spec of typschm * id
+ | VS_extern_no_rename of typschm * id
+ | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
 
 
 type dec_spec 'a = 
  | DEC_aux of (dec_spec_aux 'a) * annot 'a
 
 
-type type_def 'a = 
- | TD_aux of (type_def_aux 'a) * annot 'a
-
-
 type fundef 'a = 
  | FD_aux of (fundef_aux 'a) * annot 'a
 
@@ -424,10 +424,18 @@ type scattered_def 'a =
  | SD_aux of (scattered_def_aux 'a) * annot 'a
 
 
+type type_def 'a = 
+ | TD_aux of (type_def_aux 'a) * annot 'a
+
+
 type default_spec 'a = 
  | DT_aux of (default_spec_aux 'a) * l
 
 
+type val_spec 'a = 
+ | VS_aux of (val_spec_aux 'a) * annot 'a
+
+
 type def 'a =  (* Top-level definition *)
  | DEF_type of (type_def 'a) (* type definition *)
  | DEF_fundef of (fundef 'a) (* function definition *)
@@ -502,17 +510,6 @@ type tid =  (* A type identifier or type variable *)
  | Tid_var of kid
 
 
-type tag =  (* Data indicating where the identifier arises and thus information necessary in compilation *)
- | Tag_empty
- | Tag_global (* Globally let-bound or enumeration based value/variable *)
- | Tag_ctor (* Data constructor from a type union *)
- | Tag_extern of maybe string (* External function, specied only with a val statement *)
- | Tag_default (* Type has come from default declaration, identifier may not be bound locally *)
- | Tag_spec
- | Tag_enum
- | Tag_alias
-
-
 type t =  (* Internal types *)
  | T_id of x
  | T_var of x
@@ -531,6 +528,17 @@ and t_args =  (* Arguments to type constructors *)
  | T_args of list t_arg
 
 
+type tag =  (* Data indicating where the identifier arises and thus information necessary in compilation *)
+ | Tag_empty
+ | Tag_global (* Globally let-bound or enumeration based value/variable *)
+ | Tag_ctor (* Data constructor from a type union *)
+ | Tag_extern of maybe string (* External function, specied only with a val statement *)
+ | Tag_default (* Type has come from default declaration, identifier may not be bound locally *)
+ | Tag_spec
+ | Tag_enum
+ | Tag_alias
+
+
 type tinf =  (* Type variables, type, and constraints, bound to an identifier *)
  | Tinf_typ of t
  | Tinf_quant_typ of (map tid kinf) * list nec * tag * t
diff --git a/language/l2.ml b/language/l2.ml
index 60343397..a00e2f84 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -81,6 +81,12 @@ id_aux =  (* Identifier *)
 
 
 type 
+effect_aux =  (* effect set, of kind Effects *)
+   Effect_var of kid
+ | Effect_set of (base_effect) list (* effect set *)
+
+
+type 
 order_aux =  (* vector order specifications, of kind Order *)
    Ord_var of kid (* variable *)
  | Ord_inc (* increasing (little-endian) *)
@@ -88,24 +94,18 @@ order_aux =  (* vector order specifications, of kind Order *)
 
 
 type 
-effect_aux =  (* effect set, of kind Effects *)
-   Effect_var of kid
- | Effect_set of (base_effect) list (* effect set *)
-
-
-type 
 id = 
    Id_aux of id_aux * l
 
 
 type 
-order = 
-   Ord_aux of order_aux * l
+effect = 
+   Effect_aux of effect_aux * l
 
 
 type 
-effect = 
-   Effect_aux of effect_aux * l
+order = 
+   Ord_aux of order_aux * l
 
 
 type 
@@ -231,6 +231,11 @@ typschm =
 
 
 type 
+'a reg_id_aux = 
+   RI_id of id
+
+
+type 
 'a exp_aux =  (* Expression *)
    E_block of ('a exp) list (* block *)
  | E_nondet of ('a exp) list (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *)
@@ -309,11 +314,8 @@ and 'a letbind =
 
 
 type 
-'a alias_spec_aux =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
-   AL_subreg of id * id (* id must refer to a register, id' to a declared subregister of id *)
- | AL_bit of id * 'a exp
- | AL_slice of id * 'a exp * 'a exp
- | AL_concat of id * id (* both id and id' must refer to a register *)
+'a reg_id = 
+   RI_aux of 'a reg_id_aux * 'a annot
 
 
 type 
@@ -351,8 +353,11 @@ rec_opt_aux =  (* Optional recursive annotation for functions *)
 
 
 type 
-'a alias_spec = 
-   AL_aux of 'a alias_spec_aux * 'a annot
+'a alias_spec_aux =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
+   AL_subreg of 'a reg_id * id
+ | AL_bit of 'a reg_id * 'a exp
+ | AL_slice of 'a reg_id * 'a exp * 'a exp
+ | AL_concat of 'a reg_id * 'a reg_id
 
 
 type 
@@ -396,10 +401,8 @@ and index_range =
 
 
 type 
-'a dec_spec_aux =  (* Register declarations *)
-   DEC_reg of typ * id
- | DEC_alias of id * 'a alias_spec
- | DEC_typ_alias of typ * id * 'a alias_spec
+'a alias_spec = 
+   AL_aux of 'a alias_spec_aux * 'a annot
 
 
 type 
@@ -433,6 +436,13 @@ type
 
 
 type 
+'a dec_spec_aux =  (* Register declarations *)
+   DEC_reg of typ * id
+ | DEC_alias of id * 'a alias_spec
+ | DEC_typ_alias of typ * id * 'a alias_spec
+
+
+type 
 'a val_spec_aux =  (* Value type specification *)
    VS_val_spec of typschm * id
  | VS_extern_no_rename of typschm * id
@@ -440,11 +450,6 @@ type
 
 
 type 
-'a dec_spec = 
-   DEC_aux of 'a dec_spec_aux * 'a annot
-
-
-type 
 'a scattered_def = 
    SD_aux of 'a scattered_def_aux * 'a annot
 
@@ -465,6 +470,11 @@ type
 
 
 type 
+'a dec_spec = 
+   DEC_aux of 'a dec_spec_aux * 'a annot
+
+
+type 
 'a val_spec = 
    VS_aux of 'a val_spec_aux * 'a annot
 
diff --git a/language/l2.ott b/language/l2.ott
index 1a4d2038..7a50877b 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -828,15 +828,17 @@ scattered_def :: 'SD_' ::=
   | end id  :: :: scattered_end
 {{ com scattered definition end }}
 
+reg_id :: 'RI_' ::=
+  {{ aux _ annot }} {{ auxparam 'a }}
+  | id								:: :: id
+
 alias_spec :: 'AL_' ::=
   {{ com Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector }}
   {{ aux _ annot }} {{ auxparam 'a }}
-  | id . id'							:: :: subreg
-  {{ com id must refer to a register, id' to a declared subregister of id }}
-  | id [ exp ] 							:: :: bit
-  | id [ exp '..' exp' ]					:: :: slice
-  | id : id'  	    						:: :: concat
-  {{ com both id and id' must refer to a register }}
+  | reg_id . id							:: :: subreg
+  | reg_id [ exp ] 						:: :: bit
+  | reg_id [ exp '..' exp' ]					:: :: slice
+  | reg_id : reg_id'  	    					:: :: concat
 
 dec_spec :: 'DEC_' ::=
   {{ com Register declarations }}
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])) ->