Treat registers as values when not being actively read or written to, so that we can have a vector of registers for example.

Also, register types can be explicitly referenced.

6 files changed, 248 insertions, 192 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 75e6443e..ad22aa36 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -55,6 +55,10 @@ let map2 f l l' = List.map (Tuple.uncurry f) (List.zip l l')
 
 let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end
 
+type reg_form =
+ | Reg of id * tannot
+ | SubReg of id * reg_form * index_range
+
 type value =
  | V_boxref of nat * t  
  | V_lit of lit
@@ -63,6 +67,7 @@ type value =
  | V_vector of natural * bool * list value (* The nat stores the first index, the bool whether that's most or least significant *)
  | V_record of t * list (id * value)
  | V_ctor of id * t * value
+ | V_register of reg_form (* Value to store register access, when not actively reading or writing *)
 
  (* seems useless currently:
 let rec id_value_eq (i, v) (i', v') = i = i' && value_eq v v'
@@ -91,10 +96,6 @@ type env = list (id * value)
 
 let emem = Mem 1 Map.empty
 
-type reg_form =
- | Reg of id * t
- | SubReg of id * reg_form * index_range
-
 (* These may need to be refined or expanded based on memory requirement *)
 type action = 
  | Read_reg of reg_form * maybe (natural * natural)
@@ -110,41 +111,23 @@ type stack =
 
 (* Either a case must be added for parallel options or action must be tied to a list *)
 type outcome =
- | Value of value
+ | Value of value * tag (* If tag is external and value is register, then register value should be read *)
  | Action of action * stack
  | Error of l * string 
 
 (* interprets the exp sequentially in the presence of a set of top level definitions and returns a value or a memory request *)
 val interp : defs tannot -> exp tannot -> outcome
 
-val to_registers : defs tannot -> list (id * reg_form)
-let rec to_registers (Defs defs) = []
-(*  match defs with
+val to_registers : defs tannot -> env
+let rec to_registers (Defs defs) = 
+  match defs with
   | [ ] -> [ ]
-  | (DEF_aux def _)::defs -> 
+  | (DEF_aux def (l,tannot))::defs -> 
     match def with 
-    | DEF_spec valsp -> 
-      match valsp with
-      | (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts tq ((Typ_aux (Typ_app (Id_aux (Id "reg") _) _) _) as t)) _) id) _) -> 
-	(id, Reg id t):: (to_registers (Defs defs))
-      | _ -> to_registers (Defs defs)
-      end
-    | DEF_reg_dec typ id -> (id, Reg id typ) :: (to_registers (Defs defs))
-    | DEF_type tdef ->
-      match tdef with 
-      | (TD_aux (TD_register id n1 n2 ranges) _) -> 
-	(id,Reg id (Typ_aux (Typ_app (Id_aux (Id "vector") Unknown) []) Unknown))::
-	((to_reg_ranges id (Reg id (Typ_aux (Typ_app (Id_aux (Id "vector") Unknown) []) Unknown)) ranges) ++ (to_registers (Defs defs)))
-      | _ -> to_registers (Defs defs)
-      end
+    | DEF_reg_dec typ id -> (id, V_register(Reg id tannot)) :: (to_registers (Defs defs))
     | _ -> to_registers (Defs defs)
     end 
   end
-and to_reg_ranges base_id base_reg ranges =
-  match ranges with
-  | [ ] -> [ ]
-  | (irange,id)::ranges -> (id,(SubReg base_id base_reg irange))::(to_reg_ranges base_id base_reg ranges)
-  end*)
 
 val has_memory_effect : list base_effect -> bool
 let rec has_memory_effect efcts =
@@ -165,45 +148,6 @@ let get_effects (Typ_aux t _) =
     | _ -> []
   end
 
-(*Look for externs as well*)
-val to_memory_ops : defs tannot -> list (id * typ)
-let rec to_memory_ops (Defs defs) = []
-(*  match defs with
-  | [] -> []
-  | (DEF_aux def _) ::defs ->
-    match def with
-    | DEF_spec (VS_aux valsp _) ->
-      match valsp with
-      | VS_val_spec ts id ->
-	let t = get_typ ts in
-	let eff = get_effects t in
-        if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
-      | VS_extern_spec ts id _ ->
-	let t = get_typ ts in
-	let eff = get_effects t in
-        if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
-      | VS_extern_no_rename ts id ->
-	let t = get_typ ts in
-	let eff = get_effects t in
-        if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
-      | _ -> to_memory_ops (Defs defs) end
-    | _ -> to_memory_ops (Defs defs) end
-  end*)
-
-val to_externs : defs tannot -> list (id * string)
-let rec to_externs (Defs defs) = []
-(*  match defs with
-  | [] -> []
-  | (DEF_aux def _) ::defs ->
-    match def with
-    | DEF_spec (VS_aux valsp _) ->
-      match valsp with
-      | VS_extern_spec (TypSchm_aux (TypSchm_ts tq (Typ_aux (Typ_fn a r e) _)) _) id s ->
-        (id,s)::(to_externs (Defs defs))
-      | _ -> to_externs (Defs defs) end
-    | _ -> to_externs (Defs defs) end
-  end*)
-
 val to_data_constructors : defs tannot -> list (id * typ)
 let rec to_data_constructors (Defs defs) =
   match defs with
@@ -347,15 +291,13 @@ val fupdate_vector_slice : value -> value -> natural -> natural -> value
 let fupdate_vector_slice vec replace start stop =
   match (vec,replace) with
   | (V_vector m inc vals,V_vector _ inc' reps) ->
-    V_vector m inc (replace_is vals (if inc=inc' then reps else (List.reverse reps)) 0 (if inc then (start-m) else (m-start)) (if inc then (stop-m) else (m-stop)))
+    V_vector m inc 
+      (replace_is vals 
+	 (if inc=inc' then reps 
+	  else (List.reverse reps)) 
+	 0 (if inc then (start-m) else (m-start)) (if inc then (stop-m) else (m-stop)))
   end
 
-val in_reg : list (id * reg_form) -> id -> maybe reg_form
-let rec in_reg regs id =
-  match regs with
-  | [] -> Nothing
-  | (eid,regf)::regs -> if (get_id eid) = (get_id id) then Just regf else in_reg regs id
-end
 val in_ctors : list (id * typ) -> id -> maybe typ
 let rec in_ctors ctors id =
   match ctors with
@@ -405,6 +347,11 @@ let rec combine_typs ts =
      end 
    end
 
+let reg_to_t r =
+  match r with
+    | Reg id (Just (t,_,_,_)) -> t
+    | _ -> T_var (Kid_aux (Var "fresh") Unknown)
+ end
 
 let rec val_typ v =
   match v with
@@ -433,6 +380,7 @@ let rec val_typ v =
       let t = combine_typs ts in
       T_app (id_of_string "list") (T_args [T_arg_typ t])
     | V_ctor id t vals -> t
+    | V_register reg -> reg_to_t reg
   end
 
 let rec to_exp v =
@@ -454,6 +402,7 @@ let rec to_exp v =
 		   (Unknown,Nothing))
       | V_list(vals) -> E_list (List.map to_exp vals)
       | V_ctor id t vals -> E_app id [to_exp vals]
+      | V_register (Reg id tan) -> E_id id
      end)
     (Unknown,(val_annot (val_typ v)))
 
@@ -474,12 +423,6 @@ let rec find_function (Defs defs) id =
     | _ -> find_function (Defs defs) id
     end end
 
-val find_memory : list ( id * typ ) -> id -> maybe typ
-let find_memory mems id = List.lookup id mems
-
-val find_extern : list ( id * string ) -> id -> maybe string
-let find_extern externs id = List.lookup id externs
-
 val match_pattern : pat tannot -> value -> bool * list (id * value)
 let rec match_pattern (P_aux p _) value =
   match p with 
@@ -631,8 +574,8 @@ let rec find_case pexps value =
   end
 
 (*top_level is a tuple of 
-  (all definitions, external functions, letbound values, declared registers, memory functions (typ expected to be num -> num -> a), and Typedef union constructors) *)
-type top_level = Env of (defs tannot) * list (id * string) * env * list (id*reg_form) * list (id * typ) * list (id * typ)
+  (all definitions, letbound and enum values, register values, and Typedef union constructors) *)
+type top_level = Env of (defs tannot) * env * env * list (id * typ)
 
 val interp_main : top_level -> env -> mem -> (exp tannot) -> (outcome * mem * env)
 val exp_list : top_level -> (list (exp tannot) -> (exp tannot)) -> (list value -> value) -> env -> mem -> list value -> list (exp tannot) -> (outcome * mem * env)
@@ -640,9 +583,15 @@ val interp_lbind : top_level -> env -> mem -> (letbind tannot) -> ((outcome * me
 
 let resolve_outcome to_match value_thunk action_thunk =
   match to_match with
-  | (Value v,lm,le) -> value_thunk v lm le
-  | (Action action stack,lm,le) -> (action_thunk (Action action stack), lm,le)
-  | (Error l s,lm,le) -> (Error l s,lm,le)
+    | (Value v tag,lm,le) -> 
+      match (tag,v) with 
+	| (Tag_extern _, V_register regform) ->
+	  (Action (Read_reg regform Nothing) 
+	          (Frame (id_of_string "0")
+		         (E_aux (E_id (id_of_string "0")) (Unknown, (val_annot (reg_to_t regform)))) le lm Top), lm,le)
+	| _ -> value_thunk v lm le end
+    | (Action action stack,lm,le) -> (action_thunk (Action action stack), lm,le)
+    | (Error l s,lm,le) -> (Error l s,lm,le)
   end
 
 let update_stack (Action act stack) fn = Action act (fn stack)  
@@ -650,7 +599,7 @@ let update_stack (Action act stack) fn = Action act (fn stack)
 (*Interpret a list of expressions, tracking local state but evaluating in the same scope (i.e. not tracking env) *)
 let rec exp_list t_level build_e build_v l_env l_mem vals exps =
   match exps with
-  | [ ] -> (Value (build_v vals), l_mem, l_env)
+  | [ ] -> (Value (build_v vals) Tag_empty, l_mem, l_env)
   | e::exps -> 
     resolve_outcome (interp_main t_level l_env l_mem e)
                     (fun value lm le -> exp_list t_level build_e build_v l_env lm (vals++[value]) exps)
@@ -658,35 +607,48 @@ let rec exp_list t_level build_e build_v l_env l_mem vals exps =
   end
 
 and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
-  let (Env defs externs lets regs mems ctors) = t_level in 
+  let (Env defs lets regs ctors) = t_level in 
   let (typ,tag,ncs,effect) = match annot with 
     | Nothing -> (T_var (Kid_aux (Var "fresh_v") Unknown),
 		  Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
   match exp with
     | E_lit lit -> 
-      if is_lit_vector lit then (Value (litV_to_vec lit),l_mem,l_env) else (Value (V_lit lit), l_mem,l_env)
-    | E_cast typ exp -> interp_main t_level l_env l_mem exp (* Potentially introduce coercions ie vectors and numbers *)
+      if is_lit_vector lit then (Value (litV_to_vec lit) Tag_empty,l_mem,l_env) 
+      else (Value (V_lit lit) Tag_empty, l_mem,l_env)
+    | E_cast typ exp -> 
+      resolve_outcome (interp_main t_level l_env l_mem exp)
+	              (fun v lm le -> (Value v tag,lm,le))
+	              (fun a -> a )
+ (* TODO introduce coercions to change offset of vectors *)
     | E_id id -> 
       let name = get_id id in
       match tag with
 	| Tag_empty -> 
 	  match in_env l_env id with
 	    | Just(value) -> match value with
-		             | V_boxref n t -> (Value (in_mem l_mem n),l_mem,l_env)
-			     | _ -> (Value value,l_mem,l_env) end
+		             | V_boxref n t -> (Value (in_mem l_mem n) Tag_empty,l_mem,l_env)
+			     | _ -> (Value value Tag_empty,l_mem,l_env) end
             | Nothing -> 
               match in_env lets id with
-              | Just(value) -> (Value value,l_mem,l_env) 
-              | Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_none " name), l_mem,l_env)
-          end end
+              | Just(value) -> (Value value Tag_empty,l_mem,l_env) 
+	      | Nothing -> 
+		match in_env regs id with
+		  | Just(value) -> (Value value Tag_empty, l_mem,l_env)
+		  | Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_none " name), l_mem,l_env)
+          end end end
         | Tag_enum ->
           match in_env lets id with
-            | Just(value) -> (Value value,l_mem,l_env)
+            | Just(value) -> (Value value Tag_empty,l_mem,l_env)
 	    | Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_enum " name), l_mem,l_env)
 	    end 
-        | Tag_extern _ -> (* Need to change from "register" to which register where different from id *)
-	  let regf = Reg id typ in
+        | Tag_extern _ -> (* update with id here when it's never just "register" *)
+	  let regf = match in_env l_env id with
+	    | Just(V_register regform) -> regform
+	    | _ -> 
+	      match in_env regs id with
+		| Just(V_register regform) -> regform
+		| _ -> Reg id annot end end in
 	  (Action (Read_reg regf Nothing)
 	          (Frame (Id_aux (Id "0") Unknown)
 		         (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),
@@ -695,10 +657,10 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
         end
     | E_if cond thn els ->
       resolve_outcome (interp_main t_level l_env l_mem cond)
-                      (fun value lm le -> 
-                        match value with
-                        | V_lit(L_aux L_true _) -> interp_main t_level l_env lm thn
-                        | V_lit(L_aux L_false _) -> interp_main t_level l_env lm els end)
+	              (fun value lm le -> 
+			match value with
+                          | V_lit(L_aux L_true _) -> interp_main t_level l_env lm thn
+                          | _ -> interp_main t_level l_env lm els end)
                       (fun a -> update_stack a (add_to_top_frame (fun c -> (E_aux (E_if c thn els) (l,annot)))))
     | E_for id from to_ by ((Ord_aux o _) as order) exp ->
       let is_inc = match o with
@@ -718,7 +680,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
                                                   match by_val with 
                                                   | (V_lit (L_aux (L_num by_num) bl) as bval) ->
                                                     if (from_num = to_num) 
-                                                    then (Value(V_lit (L_aux L_unit l)),lm,le)
+                                                    then (Value(V_lit (L_aux L_unit l)) Tag_empty,lm,le)
                                                     else
                                                       let (ftyp,ttyp,btyp) = (val_typ fval,val_typ tval,val_typ bval) in
                                                       interp_main t_level le lm 
@@ -757,7 +719,8 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
                       (fun v lm le ->
                         match find_case pats v with
                         | Nothing -> (Error l "No matching patterns in case",lm,le)
-                        | Just (env,exp) -> interp_main t_level (env++l_env) lm exp end)
+                        | Just (env,exp) -> interp_main t_level (env++l_env) lm exp
+		        end)
                       (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_case e pats) (l,annot)))))
     | E_record(FES_aux (FES_Fexps fexps _) fes_annot) -> 
       let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
@@ -782,7 +745,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
 						      (l,annot)))					     
                                              (fun vs -> (V_record t (List.zip fields vs))) l_env l_mem [] exps)
                                           (fun vs lm le ->
-                                            (Value (fupdate_record rv vs), lm, le))
+                                            (Value (fupdate_record rv vs) Tag_empty, lm, le))
                                           (fun a -> a)
                         | _ -> (Error l "record upate requires record",lm,le) end)
                       (fun a -> update_stack a (add_to_top_frame 
@@ -794,7 +757,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
                       (fun hdv lm le -> resolve_outcome
                                         (interp_main t_level l_env lm tl)
                                         (fun tlv lm le -> match tlv with 
-                                                   | V_list t -> (Value(V_list (hdv::t)),lm,le)
+                                                   | V_list t -> (Value(V_list (hdv::t)) Tag_empty,lm,le)
                                                    | _ -> (Error l ":: of non-list value",lm,le) end)
                                         (fun a -> update_stack a (add_to_top_frame (fun t ->E_aux (E_cons (to_exp hdv) t) (l,annot)))))
                       (fun a -> update_stack a (add_to_top_frame (fun h -> E_aux (E_cons h tl) (l,annot))))
@@ -803,12 +766,13 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
                       (fun value lm le -> 
                         match value with 
                         | V_record t fexps -> match in_env fexps id with
-                                            | Just v -> (Value v,lm,l_env)
+                                            | Just v -> (Value v Tag_empty,lm,l_env)
                                             | Nothing -> (Error l "Field not found in record",lm,le) end
-                        | _ -> (Error l "Field access requires a record",lm,le)
+                        | _ -> (Error l "Field access of vectors not implemented",lm,le)
                         end )
                       (fun a -> update_stack a (add_to_top_frame (fun e -> E_aux(E_field e id) (l,annot))))
     | E_vector_access vec i ->
+      (*Need to update to read one position of a register*)
       resolve_outcome (interp_main t_level l_env l_mem i)
                       (fun iv lm le -> 
                         match iv with
@@ -816,13 +780,14 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
                           resolve_outcome (interp_main t_level l_env lm vec)
                                           (fun vvec lm le ->
                                             match vvec with
-                                            | V_vector base inc vals -> (Value (access_vector vvec n),lm,le)
+                                            | V_vector base inc vals -> (Value (access_vector vvec n) Tag_empty,lm,le)
                                             | _ -> (Error l "Vector access of non-vector",lm,le)end)
                                           (fun a -> update_stack a 
 					    (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)))))
                         | _ -> (Error l "Vector access not given a number for index",lm,l_env) end)
                       (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_access vec i) (l,annot))))
     | E_vector_subrange vec i1 i2 ->
+      (*Need to update to read a slice of a register*)
       resolve_outcome (interp_main t_level l_env l_mem i1)
                       (fun i1v lm le ->
                         match i1v with
@@ -834,7 +799,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
                                               resolve_outcome (interp_main t_level l_env lm vec)
                                                               (fun vvec lm le ->
                                                                 match vvec with
-                                                                | V_vector base inc vals -> (Value (slice_vector vvec n1 n2),lm,le)
+                                                                | V_vector base inc vals -> (Value (slice_vector vvec n1 n2) Tag_empty,lm,le)
                                                                 | _ -> (Error l "Vector slice of non-vector",lm,le)end)
                                                               (fun a -> update_stack a 
                                                                 (add_to_top_frame 
@@ -860,7 +825,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
                                             resolve_outcome (interp_main t_level le lm vec)
                                                             (fun vec lm le ->
                                                               match vec with
-                                                              | V_vector base inc vals -> (Value (fupdate_vec vec n1 vup), lm,le)
+                                                              | V_vector base inc vals -> (Value (fupdate_vec vec n1 vup) Tag_empty, lm,le)
                                                               | _ -> (Error l "Update of vector given non-vector",lm,le) end)
                                                             (fun a -> update_stack a 
 							      (add_to_top_frame 
@@ -889,7 +854,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
                                        (interp_main t_level l_env lm vec)
                                        (fun vvec lm le ->
                                          match vvec with
-                                         | V_vector m inc vals -> (Value (fupdate_vector_slice vvec v_rep n1 n2),lm,le)
+                                         | V_vector m inc vals -> (Value (fupdate_vector_slice vvec v_rep n1 n2) Tag_empty,lm,le)
                                          | _ -> (Error l "Vector update requires vector",lm,le) end)
                                        (fun a -> update_stack a 
                                          (add_to_top_frame 
@@ -921,7 +886,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
       (match (exp_list t_level (fun es -> E_aux (E_app f es) (l,annot)) 
 		               (fun vs -> match vs with | [] -> V_lit (L_aux L_unit l) | [v] -> v | vs -> V_tuple vs end) 
 			       l_env l_mem [] args) with
-      | (Value v,lm,le) -> 
+      | (Value v tag_e,lm,le) -> 
         let name = get_id f in 
         (match tag with
         | Tag_empty -> 
@@ -932,7 +897,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
               (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
 	    | Just(env,exp) -> 
               resolve_outcome (interp_main t_level env l_mem exp)
-	                      (fun ret lm le -> (Value ret, lm,l_env))
+	                      (fun ret lm le -> (Value ret Tag_empty, lm,l_env))
                               (fun a -> update_stack a 
 				(fun stack -> (Frame (id_of_string "0") (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack)))
              end)
@@ -945,14 +910,14 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
               (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
 	    | Just(env,exp) -> 
               resolve_outcome (interp_main t_level env l_mem exp)
-	                      (fun ret lm le -> (Value ret, lm,l_env))
+	                      (fun ret lm le -> (Value ret Tag_empty, lm,l_env))
                               (fun a -> update_stack a 
 				(fun stack -> (Frame (id_of_string "0") (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack)))
              end)
           | Nothing -> (Error l (String.stringAppend "Specified function must be defined before executing " name),lm,le) end)
         | Tag_ctor ->
           (match in_ctors ctors f with
-          | Just(_) -> (Value (V_ctor f typ v), lm, le)
+          | Just(_) -> (Value (V_ctor f typ v) Tag_empty, lm, le)
           | Nothing -> (Error l (String.stringAppend "Internal error: function with ctor tag unfound " name),lm,le)
            end)
         | Tag_extern opt_name ->
@@ -985,7 +950,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
 				               | Nothing -> (Error l (String.stringAppend "No matching pattern for function " name),lm,l_env)
 				               | Just(env,exp) ->
 				                 resolve_outcome (interp_main t_level env emem exp)
-				                   (fun ret lm le -> (Value ret,l_mem,l_env))
+				                   (fun ret lm le -> (Value ret Tag_empty,l_mem,l_env))
                                                    (fun a -> update_stack a 
 						     (fun stack -> (Frame (Id_aux (Id "0") l)
 								          (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack)))
@@ -998,7 +963,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
 				               | Nothing -> (Error l (String.stringAppend "No matching pattern for function " name),lm,l_env)
 				               | Just(env,exp) ->
 				                 resolve_outcome (interp_main t_level env emem exp)
-				                   (fun ret lm le -> (Value ret,l_mem,l_env))
+				                   (fun ret lm le -> (Value ret Tag_empty,l_mem,l_env))
                                                    (fun a -> update_stack a 
 						     (fun stack -> (Frame (Id_aux (Id "0") l)
 								          (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack)))
@@ -1012,7 +977,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
                        (fun a -> update_stack a (add_to_top_frame (fun lft -> (E_aux (E_app_infix lft op r) (l,annot)))))
   | E_let (lbind : letbind tannot) exp -> 
     match (interp_letbind t_level l_env l_mem lbind) with
-    | ((Value v,lm,le),_) -> interp_main t_level le lm exp
+    | ((Value v tag_l,lm,le),_) -> interp_main t_level le lm exp                                             
     | (((Action a s as o),lm,le),Just lbuild) ->  
       ((update_stack o (add_to_top_frame (fun e -> (E_aux (E_let (lbuild e) exp) (l,annot))))),lm,le)
     | (e,_) -> e end
@@ -1023,7 +988,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
                       | (outcome,Nothing) -> outcome
                       | (outcome,Just lexp_builder) ->
                         resolve_outcome outcome
-                                        (fun v lm le -> (Value v,lm,le))
+                                        (fun v lm le -> (Value v Tag_empty,lm,le))
                                         (fun a -> 
 					  (match a with
 					    | (Action (Write_reg regf range value) stack) -> 
@@ -1038,7 +1003,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
 
  and interp_block t_level init_env local_env local_mem exps =
    match exps with
-    | [ ] -> (Value (V_lit (L_aux (L_unit) Unknown)), local_mem, init_env)
+    | [ ] -> (Value (V_lit (L_aux (L_unit) Unknown)) Tag_empty, local_mem, init_env)
     | [ exp ] -> interp_main t_level local_env local_mem exp
     | exp:: exps ->
       resolve_outcome (interp_main t_level local_env local_mem exp)
@@ -1047,7 +1012,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
     end
 
 and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) =
-   let (Env defs externs lets regs mems ctors) = t_level in
+   let (Env defs lets regs ctors) = t_level in
   let (typ,tag,ncs,ef) = match annot with 
     | Nothing -> (T_var (Kid_aux (Var "fresh_v") Unknown), Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -1058,22 +1023,26 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
 	  match in_env l_env id with
 	    | Just (V_boxref n t) -> 
 	      if is_top_level 
-	      then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
-	      else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_id id) (l,annot)))
+	      then ((Value (V_lit (L_aux L_unit l)) Tag_empty, update_mem l_mem n value, l_env),Nothing)
+	      else ((Value (in_mem l_mem n) Tag_empty, l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_id id) (l,annot)))
 	    | Just v -> 
 	      if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) 
-	      else ((Value v,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_id id) (l,annot)))
-	    | Nothing -> 	  
-	      if is_top_level 
-              then begin
-		let (Mem c m) = l_mem in
-		let l_mem = (Mem (c+1) m) in
-		((Value (V_lit (L_aux L_unit l)), update_mem l_mem c value, (id,(V_boxref c typ))::l_env),Nothing)
-              end
-              else ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing)
+	      else ((Value v Tag_empty,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_id id) (l,annot)))
+	    | Nothing -> 
+	      (match in_env lets id with
+		| Just v -> 
+		  if is_top_level then ((Error l "Writes must be to reg or registers",l_mem,l_env),Nothing)
+		  else ((Value v Tag_empty,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_id id) (l,annot)))
+		| Nothing ->
+		  if is_top_level then begin
+		    let (Mem c m) = l_mem in
+		    let l_mem = (Mem (c+1) m) in
+		    ((Value (V_lit (L_aux L_unit l)) Tag_empty, update_mem l_mem c value, (id,(V_boxref c typ))::l_env),Nothing)
+		  end
+		  else ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing) end)
           end 
         | Tag_extern _ ->
-	  let regf = Reg id typ in
+	  let regf = Reg id annot in
 	  let request = (Action (Write_reg regf Nothing value) 
 			        (Frame (Id_aux (Id "0") l) 
 				       (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),l_mem,l_env) in
@@ -1084,7 +1053,7 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
       match (exp_list t_level (fun exps -> E_aux (E_tuple exps) (Unknown,Nothing)) 
 	              (fun vs -> match vs with | [] -> V_lit (L_aux L_unit Unknown) | [v] -> v | vs -> V_tuple vs end)
 		      l_env l_mem [] exps) with
-      | (Value v,lm,le) ->
+      | (Value v tag',lm,le) ->
         (match tag with
         | Tag_extern ->
           let request = (Action (Write_mem id v Nothing value) 
@@ -1101,22 +1070,22 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
 	  match in_env l_env id with
 	    | Just (V_boxref n t) -> 
 	      if is_top_level 
-	      then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
-	      else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_cast typc id) (l,annot)))
+	      then ((Value (V_lit (L_aux L_unit l)) Tag_empty, update_mem l_mem n value, l_env),Nothing)
+	      else ((Value (in_mem l_mem n) Tag_empty, l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_cast typc id) (l,annot)))
 	    | Just v -> 
 	      if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) 
-	      else ((Value v,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_cast typc id) (l,annot)))
+	      else ((Value v Tag_empty,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_cast typc id) (l,annot)))
 	    | Nothing -> 	  
 	      if is_top_level 
               then begin
 		let (Mem c m) = l_mem in
 		let l_mem = (Mem (c+1) m) in
-		((Value (V_lit (L_aux L_unit l)), update_mem l_mem c value, (id,(V_boxref c typ))::l_env),Nothing)
+		((Value (V_lit (L_aux L_unit l)) Tag_empty, update_mem l_mem c value, (id,(V_boxref c typ))::l_env),Nothing)
               end
               else ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing)
           end 
         | Tag_extern _ ->
-	  let regf = Reg id typ in
+	  let regf = Reg id annot in
 	  let request = (Action (Write_reg regf Nothing value) 
 			        (Frame (Id_aux (Id "0") l) 
 				       (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),l_mem,l_env) in
@@ -1125,21 +1094,30 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
       end 
     | LEXP_vector lexp exp -> 
       match (interp_main t_level l_env l_mem exp) with
-      | (Value i,lm,le) ->
+      | (Value i tag',lm,le) ->
         (match i with 
         | V_lit (L_aux (L_num n) ln) -> 
           let next_builder le_builder = (fun e -> 
 	                                  LEXP_aux (LEXP_vector (le_builder e) (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)) in
           (match (create_write_message_or_update t_level value l_env lm false lexp) with
-          | ((Value v,lm,le),maybe_builder) ->
+          | ((Value v tag3,lm,le),maybe_builder) ->
             (match v with 
             | V_vector inc m vs -> 
               let nth = access_vector v n in
               (match (nth,is_top_level,maybe_builder) with
-              | (V_boxref n t,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
-              | (v,true,_) -> ((Error l "Vector does not contain reg values",lm,l_env),Nothing)
-              | ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
-              | (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end)
+	      | (V_register regform,true,_) ->
+		((Action (Write_reg regform Nothing value)
+		         (Frame (Id_aux (Id "0") l)
+			        (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),l_mem,l_env),Nothing)
+	      | (V_register regform,false,Just lexp_builder) ->
+		((Action (Write_reg regform Nothing value)
+		         (Frame (Id_aux (Id "0") l)
+			        (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),l_mem,l_env),
+                 Just (next_builder lexp_builder))
+              | (V_boxref n t,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)) Tag_empty, update_mem lm n value, l_env),Nothing)
+              | (v,true,_) -> ((Error l "Vector does not contain reg or register values",lm,l_env),Nothing)
+              | ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n) Tag_empty,lm, l_env),Just (next_builder lexp_builder))
+              | (v,false, Just lexp_builder) -> ((Value v Tag_empty,lm,le), Just (next_builder lexp_builder)) end)
             | _ -> ((Error l "Vector access of non-vector",lm,l_env),Nothing) end)
          | ((Action a s,lm,le),Just lexp_builder) ->
            (match (a,is_top_level) with
@@ -1156,11 +1134,11 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
       | e -> (e,Nothing) end
     | LEXP_vector_range lexp exp1 exp2  ->
       match (interp_main t_level l_env l_mem exp1) with
-      | (Value i1, lm, le) ->
+      | (Value i1 tag_e, lm, le) ->
         (match i1 with
         | V_lit (L_aux (L_num n1) ln1) ->
           (match (interp_main t_level l_env l_mem exp2) with
-          | (Value i2,lm,le) ->
+          | (Value i2 tag_e2,lm,le) ->
             (match i2 with
             | V_lit (L_aux (L_num n2) ln2) ->
               let next_builder le_builder = 
@@ -1168,12 +1146,12 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
 				                      (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
 						      (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing))) (l,annot)) in
               (match (create_write_message_or_update t_level value l_env lm false lexp) with
-              | ((Value v,lm,le), Just lexp_builder) ->
+              | ((Value v tag_le,lm,le), Just lexp_builder) ->
                 (match (v,is_top_level) with
                 | (V_vector m inc vs,true) -> 
-                  ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice (slice_vector v n1 n2) value lm, l_env), Nothing)
+                  ((Value (V_lit (L_aux L_unit Unknown)) Tag_empty, update_vector_slice (slice_vector v n1 n2) value lm, l_env), Nothing)
                 | (V_vector m inc vs,false) ->
-                  ((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder))
+                  ((Value (slice_vector v n1 n2) Tag_empty,lm,l_env), Just (next_builder lexp_builder))
                 | _ -> ((Error l "Vector required",lm,le),Nothing) end)
               | ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) ->
                 ((Action (Write_reg regf (Just (n1,n2)) value) s,lm,le), Just (next_builder lexp_builder))
@@ -1194,13 +1172,13 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
       | e -> (e,Nothing) end
    | LEXP_field lexp id ->
      (match (create_write_message_or_update t_level value l_env l_mem false lexp) with
-     | ((Value (V_record t fexps),lm,le),Just lexp_builder) ->
+     | ((Value (V_record t fexps) tag_le,lm,le),Just lexp_builder) ->
        match (in_env fexps id,is_top_level) with
-       | (Just (V_boxref n t),true) -> ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
+       | (Just (V_boxref n t),true) -> ((Value (V_lit (L_aux L_unit l)) Tag_empty, update_mem lm n value, l_env),Nothing)
        | (Just (V_boxref n t),false) -> 
-	 ((Value (in_mem lm n),lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+	 ((Value (in_mem lm n) Tag_empty,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
        | (Just v, true) -> ((Error l "Field access requires record",lm,le),Nothing)
-       | (Just v,false) -> ((Value v,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+       | (Just v,false) -> ((Value v Tag_empty,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
        | (Nothing,_) -> ((Error l "Field not found in specified record",lm,le),Nothing) end
      | ((Action a s,lm,le), Just lexp_builder) ->  
        match a with
@@ -1216,32 +1194,34 @@ and interp_letbind t_level l_env l_mem (LB_aux lbind (l,annot)) =
   match lbind with
   | LB_val_explicit t pat exp ->
     match (interp_main t_level l_env l_mem exp) with
-    | (Value v,lm,le) ->
+    | (Value v Tag_empty,lm,le) ->
       (match match_pattern pat v with
-      | (true,env) -> ((Value (V_lit (L_aux L_unit l)), lm, env++l_env),Nothing)
+      | (true,env) -> ((Value (V_lit (L_aux L_unit l)) Tag_empty, lm, env++l_env),Nothing)
       | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
     | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e ->(LB_aux (LB_val_explicit t pat e) (l,annot)))))
     | e -> (e,Nothing) end
   | LB_val_implicit pat exp ->
     match (interp_main t_level l_env l_mem exp) with
-    | (Value v,lm,le) ->
+    | (Value v Tag_empty,lm,le) ->
       (match match_pattern pat v with
-      | (true,env) -> ((Value (V_lit (L_aux L_unit l)), lm, env++l_env),Nothing)
+      | (true,env) -> ((Value (V_lit (L_aux L_unit l)) Tag_empty, lm, env++l_env),Nothing)
       | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
     | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_implicit pat e) (l,annot)))))
     | e -> (e,Nothing) end
 end	
 
+(*Beef up to pick up enums as well*)
 let rec to_global_letbinds (Defs defs) t_level =
-  let  (Env defs' externs lets regs mems ctors) = t_level in
+  let  (Env defs' lets regs ctors) = t_level in
   match defs with
-  | [] -> ((Value (V_lit (L_aux L_unit Unknown)), emem, []),t_level)
+  | [] -> ((Value (V_lit (L_aux L_unit Unknown)) Tag_empty, emem, []),t_level)
   | (DEF_aux def (l,_))::defs ->
     match def with
     | DEF_val lbind ->
       match interp_letbind t_level [] emem lbind with
-      | ((Value v,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' externs (lets++le) regs mems ctors)
-      | ((Action a s,lm,le),_) -> ((Error l "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
+      | ((Value v tag,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors)
+      | ((Action a s,lm,le),_) -> 
+	((Error l "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
       | (e,_) -> (e,t_level) end
     | _ -> to_global_letbinds (Defs defs) t_level
     end
@@ -1249,10 +1229,10 @@ let rec to_global_letbinds (Defs defs) t_level =
 
 
 let interp defs exp =
-  let t_level = Env defs (to_externs defs) [] (to_registers defs) (to_memory_ops defs) (to_data_constructors defs) in 
+  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) in 
   let (o,t_level) = to_global_letbinds defs t_level in
   match o with
-  | (Value _,_,_) -> 
+  | (Value _ _,_,_) -> 
      match interp_main t_level [] emem exp with
      | (o,_,_) -> o
      end 
@@ -1266,7 +1246,7 @@ let rec resume_main t_level stack value =
     match interp_main t_level ((id,value)::env) mem exp with | (o,_,_) -> o end 
   | Frame id exp env mem stack ->
     match resume_main t_level stack value with
-    | Value v -> 
+    | Value v tag -> 
       match interp_main t_level ((id,v)::env) mem exp with | (o,_,_) -> o end 
     | Action action stack -> Action action (Frame id exp env mem stack)
     | Error l s -> Error l s
@@ -1274,10 +1254,10 @@ let rec resume_main t_level stack value =
   end
 
 let resume defs stack value =
-  let t_level = Env defs (to_externs defs) [] (to_registers defs) (to_memory_ops defs) (to_data_constructors defs) in 
+  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) in 
   let (o,t_level) = to_global_letbinds defs t_level in
   match o with
-  | (Value _,_,_) -> 
+  | (Value _ _,_,_) -> 
      resume_main t_level stack value
   | (o,_,_) -> o 
   end
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 19daeeb9..b519a2cb 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -57,6 +57,8 @@ let rec val_to_string = function
      sprintf "record {%s}" repr
  | V_ctor (id,_, value) ->
      sprintf "constructor %s %s" (id_to_string id) (val_to_string value)
+ | V_register (Reg (id,_)) ->
+     sprintf "register %s as value" (id_to_string id)
 ;;
 
 let rec env_to_string = function
@@ -185,7 +187,7 @@ let run
   ?(mem=Mem.empty)
   (name, test) =
   let rec loop env = function
-  | Value v -> eprintf "%s: returned %s\n" name (val_to_string v); true
+  | Value (v, _) -> eprintf "%s: returned %s\n" name (val_to_string v); true
   | Action (a, s) ->
       eprintf "%s: suspended on action %s\n" name (act_to_string a);
       (*eprintf "%s: suspended on action %s, with stack %s\n" name (act_to_string a) (stack_to_string s);*)
diff --git a/src/parser.mly b/src/parser.mly
index 8106df7c..8672704f 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -351,6 +351,8 @@ app_typ:
     { $1 }
   | tid Lt app_typs Gt
     { tloc (ATyp_app($1,$3)) }
+  | Register Lt app_typs Gt
+    { tloc (ATyp_app(Id_aux(Id "register", locn 1 1),$3)) }
 
 star_typ_list:
   | app_typ
diff --git a/src/test/vectors.sail b/src/test/vectors.sail
index f7872be8..353444e5 100644
--- a/src/test/vectors.sail
+++ b/src/test/vectors.sail
@@ -7,6 +7,8 @@ register (bit[10]) slice_check
 
 register nat match_success
 
+let (vector<0,3,inc,(register<(bit[10])>)>) gpr_small = [slice_check,slice_check,slice_check]
+
 function unit decode ([bitzero, bitzero, bitone, bitzero]) = match_success := 1
 and decode x = match_success := x
 
@@ -16,6 +18,9 @@ function bit main _ = {
   slice_check := v3[1..10];
   slice_check := v3[5..10];
 
+  gpr_small[1] := v3;
+  slice_check := gpr_small[1];
+ 
   i := [bitzero, bitzero, bitone, bitzero];
 
   (* literal match *)
diff --git a/src/type_check.ml b/src/type_check.ml
index fda5c97c..58bbffee 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -384,7 +384,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
         (match t.t,expect_t.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),External (Some "register"),cs,ef) in
+          let tannot = Some(([],t),Emp,cs,ef) in
           let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t' in
           (e',t',t_env,cs@cs',ef)
         | Tapp("register",[TA_typ(t')]),_ ->
@@ -572,7 +572,8 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
     | E_vector_access(vec,i) ->
       let base,rise,ord = new_n(),new_n(),new_o() in
       let min,m_rise = new_n(),new_n() in
-      let vt = {t= Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord; TA_typ expect_t])} in
+      let item_t = new_t () in
+      let vt = {t= Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord; TA_typ item_t])} in
       let (vec',t',_,cs,ef) = check_exp envs vt vec in
       let it = {t= Tapp("enum",[TA_nexp min;TA_nexp m_rise])} in
       let (i',ti',_,cs_i,ef_i) = check_exp envs it i in
@@ -583,9 +584,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 	  | Odec -> 
 	    [GtEq(l,base,min); LtEq(l,{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,{nexp=Nneg rise})})]
 	  | _ -> typ_error l "A vector must be either increasing or decreasing to access a single element"
-      in
-      (E_aux(E_vector_access(vec',i'),(l, Some(([],expect_t),Emp,cs_loc,pure_e))),
-       t',t_env,cs_loc@cs_i@cs,union_effects ef ef_i)
+      in 
+      let t',cs',e' = type_coerce l d_env item_t (E_aux(E_vector_access(vec',i'),(l,Some(([],item_t),Emp,[],pure_e)))) expect_t in
+      (e',t',t_env,cs_loc@cs_i@cs@cs',union_effects ef ef_i)
     | E_vector_subrange(vec,i1,i2) ->
       let base,rise,ord = new_n(),new_n(),new_o() in
       let min1,m_rise1 = new_n(),new_n() in
@@ -823,7 +824,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let (e,t,_,cs',ef') = check_exp (Env(d_env,Envmap.union t_env t_env')) expect_t body in
       (E_aux(E_let(lb',e),(l,Some(([],t),Emp,[],pure_e))),t,t_env,cs@cs',union_effects ef ef')
     | E_assign(lexp,exp) ->
-      let (lexp',t',t_env',tag,cs,ef) = check_lexp envs lexp in
+      let (lexp',t',t_env',tag,cs,ef) = check_lexp envs true lexp in
       let (exp',t'',_,cs',ef') = check_exp envs t' exp in
       let (t',c') = type_consistent l d_env unit_t expect_t in
       (E_aux(E_assign(lexp',exp'),(l,(Some(([],unit_t),tag,[],ef)))),unit_t,t_env',cs@cs'@c',union_effects ef ef')
@@ -856,7 +857,7 @@ and check_cases envs check_t expect_t pexps : ((tannot pexp) list * typ * nexp_r
        t'',
        csl@cs_p@cs_p'@cs2,union_effects efl ef2)
 
-and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot emap * tag *nexp_range list *effect ) =
+and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot emap * tag *nexp_range list *effect ) =
   let (Env(d_env,t_env)) = envs in
   match lexp with
     | LEXP_id id -> 
@@ -869,15 +870,20 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
 	  let t,cs = match get_abbrev d_env t with
 	    | None -> t,cs
 	    | Some(t,cs,e) -> t,cs in
-	  (match t.t with
-	    | Tapp("register",[TA_typ u]) ->
+	  (match t.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)
-	    | Tapp("reg",[TA_typ u]) ->
+	    | Tapp("reg",[TA_typ u]),_ ->
 	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),u,Envmap.empty,Emp,[],pure_e)
-	    | _ -> 
-	      typ_error l 
-		("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t))
+	    | Tapp("vector",_),false ->
+	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,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 *))
 	| _ -> 
 	  let u = new_t() in
 	  let t = {t=Tapp("reg",[TA_typ u])} in
@@ -938,27 +944,32 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
 	  let t,cs = match get_abbrev d_env t with
 	    | None -> t,cs
 	    | Some(t,cs,e) -> t,cs in
-	  (match t.t with
-	    | Tapp("register",[TA_typ u]) ->
+	  (match t.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)
-	    | Tapp("reg",[TA_typ u]) ->
+	    | 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)
-	    | Tuvar _ ->
+	    | Tapp("vector",_),false ->
+	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),t,Envmap.empty,Emp,[],pure_e)
+	    | Tuvar _,_ ->
 	      let u' = {t=Tapp("reg",[TA_typ ty])} in
 	      t.t <- u'.t;
 	      (LEXP_aux(lexp,(l,(Some((([],u'),Emp,cs,pure_e))))),ty,Envmap.empty,Emp,[],pure_e)
-	    | _ -> 
-	      typ_error l 
-		("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t))
+	    | _,_ -> 
+	      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 *)
 	| _ -> 
 	  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 vec in
+      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
@@ -970,14 +981,26 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
 	    | _ -> typ_error l ("Assignment to one vector element requires either inc or dec order")
 	  in
 	  let (e,t',_,cs',ef_e) = check_exp envs acc_t acc in
-	  (LEXP_aux(LEXP_vector(vec',e),(l,Some(([],t),tag,cs@cs',union_effects ef ef_e))),t,env,tag,cs@cs',union_effects ef ef_e)
+	  let t,add_reg_write = 
+	    match t.t with
+	      | 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)
 	| 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 vec in
+      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
+	  | 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
 	| 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
@@ -1004,7 +1027,7 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
 	| Tuvar _ -> typ_error l "Assignement to a range of elements requires a vector with a known order, found a polymorphic value, try addinga  cast"
 	| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string item_t))) 
     | LEXP_field(vec,id)-> 
-      let (vec',item_t,env,tag,csi,ef) = check_lexp envs vec in
+      let (vec',item_t,env,tag,csi,ef) = check_lexp envs false vec in
       (match item_t.t with
 	| Tid i ->
 	  (match lookup_record_typ i d_env.rec_env with
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 52a12365..e395b09b 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -190,6 +190,7 @@ let initial_kind_env =
     ("bit", {k = K_Typ});
     ("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})});
     ("reg", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})});
+    ("register", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})});
     ("enum", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}], {k = K_Typ}) });
     ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } )
   ]
@@ -340,6 +341,43 @@ let tannot_to_string = function
   | Some((vars,t),tag,ncs,ef) ->
     "Tannot: type = " ^ (t_to_string t) ^ " tag = " ^ tag_to_string tag ^ " constraints = not printing effect = " ^ e_to_string ef
 
+let rec t_to_typ t =
+  Typ_aux (
+   (match t.t with
+    | Tid i -> Typ_id (Id_aux((Id i), Parse_ast.Unknown))
+    | Tvar i -> Typ_var (Kid_aux((Var i),Parse_ast.Unknown)) 
+    | Tfn(t1,t2,e) -> Typ_fn (t_to_typ t1, t_to_typ t2, e_to_ef e)
+    | Ttup ts -> Typ_tup(List.map t_to_typ ts)
+    | Tapp(i,args) -> Typ_app(Id_aux((Id i), Parse_ast.Unknown),List.map targ_to_typ_arg args)), Parse_ast.Unknown)
+and targ_to_typ_arg targ = 
+ Typ_arg_aux( 
+  (match targ with
+    | TA_nexp n -> Typ_arg_nexp (n_to_nexp n) 
+    | TA_typ t -> Typ_arg_typ (t_to_typ t)
+    | TA_ord o -> Typ_arg_order (o_to_order o)
+    | TA_eft e -> Typ_arg_effect (e_to_ef e)), Parse_ast.Unknown)
+and n_to_nexp n =
+  Nexp_aux(
+  (match n.nexp with
+    | Nvar i -> Nexp_var (Kid_aux((Var i),Parse_ast.Unknown)) 
+    | Nconst i -> Nexp_constant i 
+    | Nmult(n1,n2) -> Nexp_times(n_to_nexp n1,n_to_nexp n2) 
+    | Nadd(n1,n2) -> Nexp_sum(n_to_nexp n1,n_to_nexp n2) 
+    | N2n n -> Nexp_exp (n_to_nexp n) 
+    | Nneg n -> Nexp_neg (n_to_nexp n)), Parse_ast.Unknown)
+and e_to_ef ef =
+ Effect_aux( 
+  (match ef.effect with
+    | Evar i -> Effect_var (Kid_aux((Var i),Parse_ast.Unknown)) 
+    | Eset effects -> Effect_set effects), Parse_ast.Unknown)
+and o_to_order o =
+ Ord_aux( 
+  (match o.order with
+    | Ovar i -> Ord_var (Kid_aux((Var i),Parse_ast.Unknown)) 
+    | Oinc -> Ord_inc 
+    | Odec -> Ord_dec), Parse_ast.Unknown)
+
+
 let get_abbrev d_env t =
   match t.t with
     | Tid i ->
@@ -537,6 +575,12 @@ let rec type_coerce l d_env t1 e t2 =
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
         eq_error l "Cannot convert an enum into a non-bit vector"
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or enum is not properly kinded"))
+    | "register",_ ->
+      (match args1 with
+	| [TA_typ t] -> 
+	  let t',cs = type_consistent l d_env t t2 in
+	  (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) ->