Initial support for aliases and exit through the type system and the interpreter.

An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter.

10 files changed, 254 insertions, 25 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index b95bf279..d14fdc59 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -384,6 +384,7 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
     | Parse_ast.E_case(exp,pexps) -> E_case(to_ast_exp k_env exp, List.map (to_ast_case k_env) pexps)
     | Parse_ast.E_let(leb,exp) -> E_let(to_ast_letbind k_env leb, to_ast_exp k_env exp)
     | Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env lexp, to_ast_exp k_env exp)
+    | Parse_ast.E_exit exp -> E_exit(to_ast_exp k_env exp)
     ), (l,NoTyp))
 
 and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot lexp = 
@@ -609,10 +610,30 @@ let rec def_in_progress (id : id) (partial_defs : (id * partial_def) list) : par
     | Id_aux(Id(n),_), Id_aux(Id(i),_) -> if (n = i) then Some(pd) else def_in_progress id defs
     | _,_ -> def_in_progress id defs)
 
-let to_ast_dec (names,k_env,t_env) (Parse_ast.DEC_aux(Parse_ast.DEC_reg(typ,id),l)) =
-  let t = to_ast_typ k_env typ in
-  let id = to_ast_id id in
-  (DEC_aux(DEC_reg(t,id),(l,NoTyp)))
+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)
+      | 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)
+      | 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)
+      | 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)
+    ), (le,NoTyp))      
+
+let to_ast_dec (names,k_env,t_env) (Parse_ast.DEC_aux(regdec,l)) =
+  DEC_aux(
+    (match regdec with
+      | Parse_ast.DEC_reg(typ,id) ->
+	DEC_reg(to_ast_typ k_env typ,to_ast_id id)
+      | Parse_ast.DEC_alias(id,e) ->
+	DEC_alias(to_ast_id id,to_ast_alias_spec k_env e)
+      | Parse_ast.DEC_typ_alias(typ,id,e) ->
+	DEC_typ_alias(to_ast_typ k_env typ,to_ast_id id,to_ast_alias_spec k_env e)
+    ),(l,NoTyp))
       
 let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * (id * partial_def) list = 
   let envs = (names,k_env,t_env) in
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index d4fcafb7..4a429423 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -116,7 +116,7 @@ type barrier_kind = | Barrier_plain  (* ?? *)
 
 (*top_level is a tuple of 
   (all definitions, letbound and enum values, register values, Typedef union constructors, and sub register mappings) *)
-type top_level = Env of (defs tannot) * env * env * list (id * typ) * list (id * list (id * index_range))
+type top_level = Env of (defs tannot) * env * env * list (id * typ) * list (id * list (id * index_range)) * list (id * (alias_spec tannot))
 
 type action = 
  | Read_reg of reg_form * maybe (integer * integer)
@@ -126,6 +126,7 @@ type action =
  | Barrier of id * value
  | Write_next_IA of value (* Perhaps not needed? *)
  | Nondet of list (exp tannot)
+ | Exit of (exp tannot)
  | Debug of l
  | Call_extern of string * value
 
@@ -173,7 +174,19 @@ let rec to_registers (Defs defs) =
     | DEF_reg_dec (DEC_aux (DEC_reg typ id) (l,tannot)) -> (id, V_register(Reg id tannot)) :: (to_registers (Defs defs))
     | _ -> to_registers (Defs defs)
     end 
-  end
+  end 
+
+val to_aliases : defs tannot -> list (id * (alias_spec tannot))
+let rec to_aliases (Defs defs) =
+  match defs with
+    | [] -> []
+    | def::defs ->
+      match def with
+	| DEF_reg_dec (DEC_aux (DEC_alias id aspec) _) -> (id, aspec) :: (to_aliases (Defs defs))
+	| DEF_reg_dec (DEC_aux (DEC_typ_alias typ id aspec) _) -> (id, aspec) :: (to_aliases (Defs defs))
+	| _ -> to_aliases (Defs defs)
+      end 
+    end
 
 val has_rmem_effect : list base_effect -> bool
 val has_barr_effect : list base_effect -> bool
@@ -874,6 +887,7 @@ let rec find_case pexps value =
 val interp_main : interp_mode -> top_level -> env -> lmem -> (exp tannot) -> (outcome * lmem * env)
 val exp_list : interp_mode -> top_level -> (list (exp tannot) -> (exp tannot)) -> (list value -> value) -> env -> lmem -> list value -> list (exp tannot) -> (outcome * lmem * env)
 val interp_lbind : interp_mode -> top_level -> env -> lmem -> (letbind tannot) -> ((outcome * lmem * env) * (maybe ((exp tannot) -> (letbind tannot))))
+val interp_alias_read : interp_mode -> top_level -> env -> lmem -> (alias_spec tannot) -> (outcome * lmem * env)
 
 let resolve_outcome to_match value_thunk action_thunk =
   match to_match with
@@ -897,7 +911,7 @@ let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
   end
 
 and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
-  let (Env defs lets regs ctors subregs) = t_level in 
+  let (Env defs lets regs ctors subregs aliases) = t_level in 
   let (typ,tag,ncs,effect) = match annot with 
     | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -962,6 +976,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	          (Hole_frame (Id_aux (Id "0") Unknown)
 		         (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level l_env l_mem Top),
            l_mem,l_env)
+        | Tag_alias -> 
+	  match in_env aliases id with
+	    | Just aspec -> interp_alias_read mode t_level l_env l_mem aspec
+	    | _ -> (Error l ("Internal error: alias not found"), l_mem,l_env) end
         | _ -> (Error l (String.stringAppend "Internal error: tag other than empty,enum,or extern " name),l_mem,l_env)
         end
     | E_if cond thn els ->
@@ -1500,7 +1518,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     end
 
 and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) =
-   let (Env defs lets regs ctors subregs) = t_level in
+   let (Env defs lets regs ctors subregs aliases) = t_level in
   let (typ,tag,ncs,ef) = match annot with 
     | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -1729,15 +1747,60 @@ and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
     | e -> (e,Nothing) end
 end	
 
+and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
+  let (Env defs lets regs ctors subregs aliases) = t_level in 
+  let stack = Hole_frame (Id_aux (Id "0") Unknown)
+		          (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
+			  t_level l_env l_mem Top in
+  match alspec 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 (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 " 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 (Read_reg (SubReg subreg rf 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 " 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 (Read_reg (Reg reg annot) (Just (i,i))) stack, 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 (Read_reg (Reg reg annot) (Just (start,stop))) stack,
+						 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
+
 let rec to_global_letbinds (Defs defs) t_level =
-  let  (Env defs' lets regs ctors subregs) = t_level in
+  let  (Env defs' lets regs ctors subregs aliases) = t_level in
   match defs with
   | [] -> ((Value (V_lit (L_aux L_unit Unknown)) Tag_empty, emem, []),t_level)
   | def::defs ->
     match def with
     | DEF_val lbind ->
       match interp_letbind <|eager_eval=true|> t_level [] emem lbind with
-      | ((Value v tag,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors subregs)
+      | ((Value v tag,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors subregs aliases)
       | ((Action a s,lm,le),_) -> 
 	((Error Unknown "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
       | (e,_) -> (e,t_level) end
@@ -1745,14 +1808,14 @@ let rec to_global_letbinds (Defs defs) t_level =
       match tdef with
       | TD_enum id ns ids _ -> 
         let enum_vals = map (fun eid -> (eid,V_ctor eid (T_id (get_id id)) unitv)) ids in
-        to_global_letbinds (Defs defs) (Env defs' (lets++enum_vals) regs ctors subregs)
+        to_global_letbinds (Defs defs) (Env defs' (lets++enum_vals) regs ctors subregs aliases)
       | _ -> to_global_letbinds (Defs defs) t_level end
     | _ -> to_global_letbinds (Defs defs) t_level
     end
   end
 
 let to_top_env defs = 
-  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) (to_register_fields defs) in
+  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
   let (o,t_level) = to_global_letbinds defs t_level in
   match o with
     | (Value _ _,_,_) -> (Nothing,t_level)
diff --git a/src/lexer.mll b/src/lexer.mll
index b53577c5..f7cd1272 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -59,6 +59,7 @@ let kw_table =
     M.empty
     [
      ("and",                     (fun _ -> And));
+     ("alias",                   (fun _ -> Alias));
      ("as",                      (fun _ -> As));
      ("bitzero",                 (fun _ -> Bitzero));
      ("bitone",                  (fun _ -> Bitone));
@@ -75,6 +76,7 @@ let kw_table =
      ("end",                     (fun _ -> End));
      ("enumerate",		 (fun _ -> Enumerate));
      ("else",                    (fun _ -> Else));
+     ("exit",                    (fun _ -> Exit));
      ("extern",                  (fun _ -> Extern));
      ("false",                   (fun _ -> False));
      ("forall",                  (fun _ -> Forall));
diff --git a/src/parser.mly b/src/parser.mly
index aa6c853d..b36085a5 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -122,10 +122,12 @@ let make_vector_sugar typ typ1 =
 
 /*Terminals with no content*/
 
-%token And As Bitzero Bitone Bits By Case Clause Const Dec Default Deinfix Effect EFFECT End Enumerate Else Extern
-%token False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order Pure Rec Register
+%token And Alias As Bitzero Bitone Bits By Case Clause Const Dec Default Deinfix Effect EFFECT End 
+%token Enumerate Else Exit Extern False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order 
+%token Pure Rec Register Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef 
+%token Undefined Union With Val
 %token Barr Rreg Wreg Rmem Wmem Undef Unspec Nondet
-%token Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef Undefined Union With Val
+
 
 /* Avoid shift/reduce conflict - see right_atomic_exp rule */
 %nonassoc Then
@@ -541,9 +543,6 @@ atomic_exp:
     { eloc (E_cast($2,$4)) }
   | Lparen comma_exps Rparen
     { eloc (E_tuple($2)) }
-  /* XXX creates many conflicts
-  | Lcurly semi_exps Rcurly
-    { eloc (E_record($2)) }  */
   | Lcurly exp With semi_exps Rcurly
     { eloc (E_record_update($2,$4)) } 
   | Lsquare Rsquare
@@ -562,6 +561,8 @@ atomic_exp:
     { eloc (E_list($2)) }
   | Switch exp Lcurly case_exps Rcurly
     { eloc (E_case($2,$4)) }
+  | Exit atomic_exp
+    { eloc (E_exit $2) }
 
 field_exp:
   | atomic_exp
@@ -1171,6 +1172,10 @@ def:
     { dloc (DEF_default($1)) }
   | Register atomic_typ id
     { dloc (DEF_reg_dec(DEC_aux(DEC_reg($2,$3),loc ()))) }
+  | Register Alias id Eq exp
+    { dloc (DEF_reg_dec(DEC_aux(DEC_alias($3,$5),loc ()))) }
+  | Register Alias atomic_typ id Eq exp
+    { dloc (DEF_reg_dec(DEC_aux(DEC_typ_alias($3,$4,$6), loc ()))) }
   | Scattered scattered_def
     { dloc (DEF_scattered $2) }
   | Function_ Clause funcl
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 2a24dc3e..a537ff46 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -253,6 +253,7 @@ let pp_format_tag = function
   | Default -> "Tag_default"
   | Constructor -> "Tag_ctor"
   | Enum -> "Tag_enum"
+  | Alias -> "Tag_alias"
   | Spec -> "Tag_spec"
 
 let rec pp_format_nes nes = 
@@ -374,6 +375,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
       fprintf ppf "@[<0>(E_aux (%a %a [%a]) (%a, %a))@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot
     | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_let" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot
+    | E_exit exp -> fprintf ppf "@[<0>(E_aux (E_exit %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_internal_exp (l, Base((_,t),_,_,_)) ->
       (match t.t with
 	| Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) ->
@@ -493,8 +495,25 @@ let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) =
     kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls
     pp_lem_l l pp_annot annot
 
-let pp_lem_dec ppf (DEC_aux(DEC_reg(typ,id),(l,annot))) =
-  fprintf ppf "@[<0>(DEC_aux (DEC_reg %a %a) (%a,%a))@]" pp_lem_typ typ pp_lem_id id pp_lem_l l pp_annot annot
+let pp_lem_aspec ppf (AL_aux(aspec,(l,annot))) =
+  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
+    | 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
+    | 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
+    | 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
+
+let pp_lem_dec ppf (DEC_aux(reg,(l,annot))) =
+  match reg with 
+    | DEC_reg(typ,id) ->
+      fprintf ppf "@[<0>(DEC_aux (DEC_reg %a %a) (%a,%a))@]" pp_lem_typ typ pp_lem_id id pp_lem_l l pp_annot annot
+    | DEC_alias(id,alias_spec) ->
+      fprintf ppf "@[<0>(DEC_aux (DEC_alias %a %a) (%a, %a))@]" pp_lem_id id pp_lem_aspec alias_spec pp_lem_l l pp_annot annot
+    | DEC_typ_alias(typ,id,alias_spec) ->
+      fprintf ppf "@[<0>(DEC_aux (DEC_typ_alias %a %a %a) (%a, %a))@]" pp_lem_typ typ pp_lem_id id pp_lem_aspec alias_spec pp_lem_l l pp_annot annot
 
 let pp_lem_def ppf d =
   match d with
@@ -827,7 +846,7 @@ let doc_exp, doc_let =
       parens (separate_map comma exp exps)
   | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
       (* XXX E_record is not handled by parser currently
-         AAA I don't think the parser can handle E_record due to ambiguity with blocks; initial_check looks for blocks that are all field assignments and converts *)
+         AAA The parser can't handle E_record due to ambiguity with blocks; initial_check looks for blocks that are all field assignments and converts *)
       braces (separate_map semi_sp doc_fexp fexps)
   | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
       braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps))
@@ -849,6 +868,8 @@ let doc_exp, doc_let =
       let opening = separate space [string "switch"; exp e; lbrace] in
       let cases = separate_map (break 1) doc_case pexps in
       surround 2 1 opening cases rbrace
+  | E_exit e ->
+    separate space [string "exit"; exp e;]
   (* adding parens and loop for lower precedence *)
   | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _)
   | E_cons (_, _)|E_field (_, _)|E_assign (_, _)
@@ -1010,8 +1031,19 @@ let doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),_)) =
         string "effect"; doc_effects_opt efa;
         clauses]
 
-let doc_dec (DEC_aux(DEC_reg(typ,id),_)) =
-  separate space [string "register"; doc_atomic_typ typ; doc_id id]
+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)
+
+let doc_dec (DEC_aux (reg,_)) =
+  match reg with
+    | DEC_reg(typ,id) -> separate space [string "register"; doc_atomic_typ typ; doc_id id]
+    | DEC_alias(id,alspec) -> separate space [string "register"; string "alias"; doc_id id; equals; doc_alias alspec]
+    | DEC_typ_alias(typ,id,alspec) -> 
+      separate space [string "register"; string "alias"; doc_atomic_typ typ; doc_id id; equals; doc_alias alspec]
 
 let doc_scattered (SD_aux (sdef, _)) = match sdef with
  | SD_scattered_function (r, typa, efa, id) ->
diff --git a/src/process_file.ml b/src/process_file.ml
index 6d1729a5..98dd4db9 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -93,7 +93,7 @@ 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_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_internal.rec_env = []; Type_internal.alias_env = Envmap.empty} 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/test/regbits.sail b/src/test/regbits.sail
index ed2a95e0..46343d67 100644
--- a/src/test/regbits.sail
+++ b/src/test/regbits.sail
@@ -8,12 +8,19 @@
 register (xer) XER
 register (bit) query
 
+register alias CA = XER.CA
+register alias Fo = XER[35]
+register alias foobar = XER[35..36]
+
 function (bit[64]) main _ = {
   XER := 0b0101010101010101010101010101010101010101010101010101010101010010;
   f := XER;
   (bit[7]) foo := XER[57..63];
   query := XER.SO;
   XER.SO := 0;
+  query := CA;
+  query := Fo;
   XER.FOOBAR := 0b11;
+  XER.FOOBAR := foobar;
   XER }
 
diff --git a/src/type_check.ml b/src/type_check.ml
index f8ec0642..e68337ab 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -28,6 +28,7 @@ let rec field_equivs fields fmaps =
       if (List.mem_assoc (id_to_string id) fmaps)
       then match (field_equivs fields fmaps) with
 	| None -> None
+	| Some [] -> None
 	| Some fs -> Some(((List.assoc (id_to_string id) fmaps),id,l,pat)::fs)
       else None
 
@@ -1010,6 +1011,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let (exp',t'',_,cs',ef') = check_exp envs t' exp in
       let (t',c') = type_consistent (Expr l) d_env unit_t expect_t in
       (E_aux(E_assign(lexp',exp'),(l,(Base(([],unit_t),tag,[],ef)))),unit_t,t_env',cs@cs'@c',union_effects ef ef')
+    | E_exit e ->
+      let (e',t',_,_,_) = check_exp envs (new_t ()) e in
+      (E_aux (E_exit e',(l,(Base(([],expect_t),Emp_local,[],pure_e)))),expect_t,t_env,[],pure_e)
     | E_internal_cast _ | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
 		    
 and check_block orig_envs envs expect_t exps : ((tannot exp) list * tannot * tannot emap * nexp_range list * t * effect) =
@@ -1426,6 +1430,84 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))),
       Env(d_env,(if is_rec then t_env else Envmap.insert t_env (id,tannot)))
 
+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 i = id_to_string id in
+    (match Envmap.apply t_env i with
+      | Some(Base(([],t), External (Some j), [], _)) ->
+	let t,_ = get_abbrev d_env t in
+        let t_actual,t_id = match t.t with 
+          | Tabbrev(i,t) -> t,i
+          | _ -> t,t in
+	(match t_actual.t with 
+	  | Tapp("register",[TA_typ t']) -> 
+	    if i = j then (i,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 
+      (match reg_t.t with
+	| Tid i ->
+	  (match lookup_record_typ i d_env.rec_env with
+	    | None -> typ_error l ("Expected a register with bit fields, given " ^ i)
+	    | Some(((i,rec_kind,fields) as r)) ->
+	      let fi = id_to_string subreg in
+	      (match lookup_field_type fi r with
+		| NoTyp -> typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
+                | 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
+		  (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 (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]) ->
+	  match (base.nexp,len.nexp,order.order, bit) with
+	    | (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll))) ->
+	      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
+		   (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)
+    | AL_slice(reg_a,sl1,sl2) -> 
+      let (reg,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
+	| Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) ->
+	  match (base.nexp,len.nexp,order.order, sl1,sl2) with
+	    | (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll)),E_lit (L_aux((L_num k2), ll2))) ->
+	      if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k2 && k < k2 
+	      then let t = {t = Tapp("vector",[TA_nexp (int_to_nexp k);TA_nexp (int_to_nexp ((k2-k) +1));
+					      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
+		   (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")
+	    | _ -> 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
+      (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])) ->
+	  let _ = type_consistent (Specc l) d_env item_t item_t2 in
+	  let t = {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
+	  (AL_aux (AL_concat(reg1_a,reg2_a), (l,tannot)), tannot, d_env))
+
 (*val check_def : envs -> tannot def -> (tannot def) envs_out*)
 let check_def envs def = 
   let (Env(d_env,t_env)) = envs in
@@ -1445,6 +1527,15 @@ let check_def envs def =
     let i = id_to_string id in
     let tannot = into_register d_env (Base(([],t),External (Some i),[],pure_e)) in
     (DEF_reg_dec(DEC_aux(DEC_reg(typ,id),(l,tannot))),(Env(d_env,Envmap.insert t_env (i,tannot))))
+  | DEF_reg_dec(DEC_aux(DEC_alias(id,aspec), (l,annot))) -> 
+    let i = id_to_string id in
+    let (aspec,tannot,d_env) = check_alias_spec envs i aspec None in
+    (DEF_reg_dec(DEC_aux(DEC_alias(id,aspec),(l,tannot))),(Env(d_env, Envmap.insert t_env (i,tannot))))
+  | DEF_reg_dec(DEC_aux(DEC_typ_alias(typ,id,aspec),(l,tannot))) ->
+    let i = id_to_string id in
+    let t = typ_to_t typ in
+    let (aspec,tannot,d_env) = check_alias_spec envs i aspec (Some t) in
+    (DEF_reg_dec(DEC_aux(DEC_typ_alias(typ,id,aspec),(l,tannot))),(Env(d_env,Envmap.insert t_env (i,tannot))))
   | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker")
 
 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 08eddc3f..880d317a 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -74,6 +74,7 @@ type tag =
   | Default
   | Constructor
   | Enum
+  | Alias
   | Spec
 
 type constraint_origin =
@@ -98,7 +99,6 @@ type tannot =
   | Base of (t_params * t) * tag * nexp_range list * effect
   | Overload of tannot * bool * tannot list (* First tannot is the most polymorphic version; the boolean indicates whether the overloaded functions can use the return type; the list includes all variants. All t to be Tfn *)
 
-(*type tannot = ((t_params * t) * tag * nexp_range list * effect) option*)
 type 'a emap = 'a Envmap.t
 
 type rec_kind = Record | Register
@@ -109,6 +109,7 @@ type def_envs = {
   namesch : tannot emap; 
   enum_env : (string list) emap; 
   rec_env : rec_env list;
+  alias_env : (string * tannot) emap;
  }  
 
 type exp = tannot Ast.exp
@@ -193,6 +194,7 @@ let tag_to_string = function
   | Default -> "Default"
   | Constructor -> "Constructor"
   | Enum -> "Enum"
+  | Alias -> "Alias"
   | Spec -> "Spec"
 
 let rec tannot_to_string = function
@@ -496,6 +498,8 @@ let rec normalize_nexp n =
     | Nneg _,_ | _,Nneg _ -> let _ = Printf.printf "neg case still around %s\n" (n_to_string n) in assert false (* If things are normal, neg should be gone. *)
     )
     
+let int_to_nexp i = {nexp = Nconst (big_int_of_int i)}
+
 let v_count = ref 0
 let t_count = ref 0
 let tuvars = ref []
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 7ddb082f..063ee088 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -70,6 +70,7 @@ type tag =
   | Default
   | Constructor
   | Enum
+  | Alias
   | Spec
 
 type constraint_origin =
@@ -106,6 +107,7 @@ type def_envs = {
   namesch : tannot emap; 
   enum_env : (string list) emap; 
   rec_env : rec_env list;
+  alias_env : (string * tannot) emap;
  }
 
 type exp = tannot Ast.exp
@@ -131,6 +133,8 @@ val t_to_string : t -> string
 val tannot_to_string : tannot -> string
 val t_to_typ : t -> Ast.typ
 
+val int_to_nexp : int -> nexp
+
 val reset_fresh : unit -> unit
 val new_t : unit -> t
 val new_n : unit -> nexp