fixes, pp progress

8 files changed, 308 insertions, 222 deletions

diff --git a/mips/mips.sail b/mips/mips.sail
index 4f468354..b18f3cda 100644
--- a/mips/mips.sail
+++ b/mips/mips.sail
@@ -547,7 +547,7 @@ function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5])
   DSLL32(rt, rd, sa)
 function clause execute (DSLL32 (rt, rd, sa)) =
   {
-    wGPR(rd) := (rGPR(rt) << (1 : sa)) (* make tuareg mode less blue >> *)
+    wGPR(rd) := (rGPR(rt) << (0b1 : sa)) (* make tuareg mode less blue >> *)
   }
 
 (* DSLLV reg, reg, reg *)
@@ -557,7 +557,7 @@ function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b0000
   DSLLV(rs, rt, rd)
 function clause execute (DSLLV (rs, rt, rd)) =
   {
-    wGPR(rd) := (rGPR(rs) << ((rGPR(rt))[5:0])) (* make tuareg mode less blue >> *)
+    wGPR(rd) := (rGPR(rs) << ((rGPR(rt))[5 .. 0])) (* make tuareg mode less blue >> *)
   }
 
 (* DSRA arithmetic shift duplicating sign bit - reg, reg, imm5 *)
@@ -1482,7 +1482,7 @@ union ast member unit HCF
 function clause decode (0b010000 : 0b00100 : (regno) rt : 0b10111 : 0b00000000000) =
   HCF() (* simulator halt instruction "MTC0 rt, $23" (cheri specific behaviour) *)
 
-function clause decode _ = exit no_matching_pattern
+function clause decode _ = {exit no_matching_pattern; HCF()}
 
 end decode
 end execute
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 8e1e1f67..3efdd163 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -83,7 +83,7 @@ type reg_name =
    * specifies a part of the field, indexed w.r.t. the register as a whole *)
   | Reg_f_slice of string * nat * direction * string * slice * slice 
 
-type outcome 'a =
+type outcome 'e 'a =
   (* Request to read memory, value is location to read followed by registers that location depended 
    * on when mode.track_values, integer is size to read, followed by registers that were used in 
    * computing that size *)
@@ -123,14 +123,14 @@ type outcome 'a =
                                                 
   (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally 
    * provide a handler. *)
-  | Escape (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)
+  | Escape 'e (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)
 
   (* Stop for incremental stepping, function can be used to display function call data *)
   | Done of 'a
 
-type M 'a = outcome 'a
+type M 'e 'a = outcome 'e 'a
 
-val return : forall 'a. 'a -> M 'a
+val return : forall 'e 'a. 'a -> M 'e 'a
 let return a = Done a
 
 val (>>=) : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index d2364397..ace65b3b 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -4,6 +4,7 @@ open import Vector
 open import Arch
 
 type i = integer
+type number = integer
 
 let length l = integerFromNat (length l)
 
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index f79f8eff..b5b0c37f 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -3,7 +3,7 @@ open import Vector
 open import Arch
 
 (* 'a is result type, 'e is error type *)
-type M 's 'e 'a = 's -> (either 'a 'e * 's)
+type State 's 'e 'a = 's -> (either 'a 'e * 's)
 
 type memstate = map integer (list bit)
 
@@ -21,25 +21,27 @@ let rec ints_aux acc x =
 
 let ints = ints_aux []
 
-val return : forall 's 'e 'a. 'a -> M 's 'e 'a
+val return : forall 's 'e 'a. 'a -> State 's 'e 'a
 let return a s = (Left a,s)
 
-val bind : forall 's 'e 'a 'b. M 's 'e 'a -> ('a -> M 's 'e 'b) -> M 's 'e 'b
+val bind : forall 's 'e 'a 'b. State 's 'e 'a -> ('a -> State 's 'e 'b) -> State 's 'e 'b
 let bind m f s = match m s with
   | (Left a,s') -> f a s'
   | (Right error,s') -> (Right error,s')
   end
 
-val exit : forall 's 'e 'a. 'e -> M 's 'e 'a
+val exit : forall 's 'e. 'e -> State 's 'e unit
 let exit e s = (Right e,s)
 
 let (>>=) = bind
+
+val (>>): forall 's 'e 'a 'b. State 's 'e 'a -> State 's 'e 'b -> State 's 'e 'b
 let (>>) m n = m >>= fun _ -> n
 
-val read_writeEA : forall 'e. unit -> M state 'e (integer * integer)
+val read_writeEA : forall 'e. unit -> State state 'e (integer * integer)
 let read_writeEA () s = (Left s.writeEA,s)
 
-val write_writeEA : forall 'e. integer -> integer -> M state 'e unit
+val write_writeEA : forall 'e. integer -> integer -> State state 'e unit
 let write_writeEA addr l s = (Left (), <| s with writeEA = (addr,l) |>)
 
 val byte_chunks : forall 'a. integer -> list 'a -> list (list 'a)
@@ -63,46 +65,46 @@ let read_memstate s addr = findWithDefault addr (replicate 8 Undef) s
 val write_memstate : memstate -> (integer * list bit) -> memstate
 let write_memstate s (addr,bits) = Map.insert addr bits s
 
-val read_memory : forall 'e. integer -> integer -> M state 'e (vector bit)
+val read_memory : forall 'e. integer -> integer -> State state 'e (vector bit)
 let read_memory addr l s =
   let bytes = List.map (compose (read_memstate s.memstate) ((+) addr)) (ints l) in
   (Left (V (foldl (++) [] bytes) 0 defaultDir),s)
 
-val write_memory : forall 'e. integer -> integer -> vector bit -> M state 'e unit
+val write_memory : forall 'e. integer -> integer -> vector bit -> State state 'e unit
 let write_memory addr l (V bits _ _) s =
   let addrs = List.map ((+) addr) (ints l) in
   let bytes = byte_chunks l bits in
   (Left (), <| s with memstate = foldl write_memstate s.memstate (zip addrs bytes) |>)
 
-val read_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> M state 'e (vector bit)
+val read_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> State state 'e (vector bit)
 let read_reg_range reg i j s =
   let v = slice (read_regstate s reg) i j in
   (Left v,s)
 
-val read_reg_bit : forall 'e. register -> integer (*nat*) -> M state 'e bit
+val read_reg_bit : forall 'e. register -> integer (*nat*) -> State state 'e bit
 let read_reg_bit reg i s =
   let v = access (read_regstate s reg) i in
   (Left v,s)
 
-val write_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> vector bit -> M state 'e unit
+val write_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> vector bit -> State state 'e unit
 let write_reg_range reg i j v s =
   let v' = update (read_regstate s reg) i j v in
   let s' = write_regstate s reg v' in
   (Left (),s')
 
-val write_reg_bit : forall 'e. register -> integer (*nat*) -> bit -> M state 'e unit
+val write_reg_bit : forall 'e. register -> integer (*nat*) -> bit -> State state 'e unit
 let write_reg_bit reg i bit s =
   let v = read_regstate s reg in
   let v' = update_pos v i bit in
   let s' = write_regstate s reg v' in
   (Left (),s')
 
-val read_reg : forall 'e. register -> M state 'e (vector bit)
+val read_reg : forall 'e. register -> State state 'e (vector bit)
 let read_reg reg s =
   let v = read_regstate s reg in
   (Left v,s)
 
-val write_reg : forall 'e. register -> vector bit -> M state 'e unit
+val write_reg : forall 'e. register -> vector bit -> State state 'e unit
 let write_reg reg v s =
   let s' = write_regstate s reg v in
   (Left (),s')
@@ -128,45 +130,45 @@ let rec foreach_dec (i,stop,by) vars body =
   else ((),vars)
 
 
-val foreachM_inc : forall 's 'e 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars)
-let rec foreachM_inc (i,stop,by) vars body = 
+val foreachState_inc : forall 's 'e 'vars. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> State 's 'e (unit * 'vars)) -> State 's 'e (unit * 'vars)
+let rec foreachState_inc (i,stop,by) vars body = 
   if i <= stop
   then
     body i vars >>= fun (_,vars) ->
-    foreachM_inc (i + by,stop,by) vars body
+    foreachState_inc (i + by,stop,by) vars body
   else return ((),vars)
 
 
-val foreachM_dec : forall 's 'e 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars)
-let rec foreachM_dec (i,stop,by) vars body = 
+val foreachState_dec : forall 's 'e 'vars. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> State 's 'e (unit * 'vars)) -> State 's 'e (unit * 'vars)
+let rec foreachState_dec (i,stop,by) vars body = 
   if i >= stop
   then
     body i vars >>= fun (_,vars) ->
-    foreachM_dec (i - by,stop,by) vars body
+    foreachState_dec (i - by,stop,by) vars body
   else return ((),vars)
 
-val read_reg_field : forall 'e. register -> register_field -> M state 'e (vector bit)
+val read_reg_field : forall 'e. register -> register_field -> State state 'e (vector bit)
 let read_reg_field reg rfield = uncurry (read_reg_range reg) (field_indices rfield)
 
-val write_reg_field : forall 'e. register -> register_field -> vector bit -> M state 'e unit
+val write_reg_field : forall 'e. register -> register_field -> vector bit -> State state 'e unit
 let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield)
 
-val read_reg_bitfield : forall 'e. register -> register_bitfield -> M state 'e bit
+val read_reg_bitfield : forall 'e. register -> register_bitfield -> State state 'e bit
 let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit)
 
-val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> M state 'e unit
+val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> State state 'e unit
 let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit)
 
 val write_reg_field_range : forall 'e. register -> register_field -> integer -> integer ->
-                            vector bit -> M state 'e unit
+                            vector bit -> State state 'e unit
 let write_reg_field_range reg rfield i j v =
   let (i',j') = field_indices rfield in
   write_reg_range reg i' j' v
 
 val write_reg_field_bit : forall 'e. register -> register_field -> integer ->
-                            bit -> M state 'e unit
+                            bit -> State state 'e unit
 let write_reg_field_bit reg rfield i v =
   let (i',_) = field_indices rfield in
   write_reg_bit reg (i + i') v
@@ -190,3 +192,5 @@ let read_two_regs r1 r2 =
   read_reg r1 >>= fun v1 ->
   read_reg r2 >>= fun v2 ->
   return (v1 ^^ v2)
+
+type M 'e 'a = State state 'e 'a
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 546fc770..f0005d02 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1808,11 +1808,35 @@ let langlebar = string "<|"
 let ranglebar = string "|>"
 let anglebars = enclose langlebar ranglebar
 
+module M = Map.Make(String)
+
+let keywords =
+  (List.fold_left (fun m (x,y) -> M.add x y m) (M.empty))
+    [
+      ("assert","assert'");
+      ("lsl","lsl'");
+      ("lsr","lsr'");
+      ("asr","asr'");
+      ("type","type'");
+      ("fun","fun'");
+      ("function","function'");
+      ("raise","raise'");
+      ("try","try'");
+      ("match","match'");
+      ("with","with'");
+      ("field","fields'");
+    ] 
+
+let fix_id i = if M.mem i keywords then M.find i keywords else i
+
 let doc_id_lem (Id_aux(i,_)) =
   match i with
-  | Id("bit") -> string "bit" 
-  | Id i -> string (if i.[0] = '\'' || is_number(i.[0])
-                    then "_" ^ i else i)
+  | Id i ->
+     (* this not the right place to do this, just a workaround *)
+     if i.[0] = '\'' || is_number(i.[0]) then
+       string ("_" ^ i)
+     else
+       string (fix_id i)
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
@@ -1820,8 +1844,10 @@ let doc_id_lem (Id_aux(i,_)) =
 
 let doc_id_lem_type (Id_aux(i,_)) =
   match i with
-  | Id("bit") -> string "bit" 
-  | Id i -> string i
+  | Id("bit") -> string "bit"
+  | Id("int") -> string "integer"
+  | Id("nat") -> string "integer"
+  | Id i -> string (fix_id i)
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
@@ -1830,7 +1856,9 @@ let doc_id_lem_type (Id_aux(i,_)) =
 let doc_id_lem_ctor aexp_needed (Id_aux(i,_)) =
   match i with
   | Id("bit") -> string "bit" 
-  | Id i -> string (String.capitalize i)
+  | Id("int") -> string "integer"
+  | Id("nat") -> string "integer"
+  | Id i -> string (fix_id (String.capitalize i))
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
@@ -1839,47 +1867,56 @@ let doc_id_lem_ctor aexp_needed (Id_aux(i,_)) =
 
 let doc_typ_lem, doc_atomic_typ_lem =
   (* following the structure of parser for precedence *)
-  let rec typ ty = fn_typ ty
-  and fn_typ ((Typ_aux (t, _)) as ty) = match t with
-  | Typ_fn(arg,ret,efct) ->
-      separate space [tup_typ arg; arrow; fn_typ ret]
-  | _ -> tup_typ ty
-  and tup_typ ((Typ_aux (t, _)) as ty) = match t with
-  | Typ_tup typs -> separate_map star app_typ typs
-  | _ -> app_typ ty
-  and app_typ ((Typ_aux (t, _)) as ty) = match t with
-  | Typ_app(Id_aux (Id "vector", _), [
-      Typ_arg_aux(Typ_arg_nexp n, _);
-      Typ_arg_aux(Typ_arg_nexp m, _);
-      Typ_arg_aux (Typ_arg_order ord, _);
-      Typ_arg_aux (Typ_arg_typ typa, _)]) ->
-    string "vector" ^^ space ^^ parens (typ typa)
-  | Typ_app(Id_aux (Id "range", _), [
-    Typ_arg_aux(Typ_arg_nexp n, _);
-    Typ_arg_aux(Typ_arg_nexp m, _);]) ->
-    (string "number")
-  | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
-    (string "number")
-  | Typ_app(id,args) ->
-      (doc_id_lem_type id) ^^ space ^^ (separate_map space doc_typ_arg_lem args)
-  | _ -> atomic_typ ty 
-  and atomic_typ ((Typ_aux (t, _)) as ty) = match t with
-    | Typ_id (Id_aux ((Id "bool"),_)) -> string "bit"
-    | Typ_id id  -> doc_id_lem_type id
-    | Typ_var v  -> doc_var v
-    | Typ_wild -> underscore
-    | Typ_app _ | Typ_tup _ | Typ_fn _ ->
-       (* exhaustiveness matters here to avoid infinite loops
-        * if we add a new Typ constructor *)
-       group (parens (typ ty))
-  and doc_typ_arg_lem (Typ_arg_aux(t,_)) = match t with
-    | Typ_arg_typ t -> app_typ t
-    | Typ_arg_nexp n -> empty
-    | Typ_arg_order o -> empty
-    | Typ_arg_effect e -> empty
-  in typ, atomic_typ
-
-let doc_lit_lem in_pat (L_aux(l,_)) =
+  let rec typ regtypes ty = fn_typ true regtypes ty
+    and typ' regtypes ty = fn_typ false regtypes ty
+    and fn_typ atyp_needed regtypes ((Typ_aux (t, _)) as ty) = match t with
+      | Typ_fn(arg,ret,efct) ->
+         let tpp = separate space [tup_typ true regtypes arg; arrow;fn_typ false regtypes ret] in
+         if atyp_needed then parens tpp else tpp
+      | _ -> tup_typ atyp_needed regtypes ty
+    and tup_typ atyp_needed regtypes ((Typ_aux (t, _)) as ty) = match t with
+      | Typ_tup typs ->
+         let tpp = separate_map (space ^^ star ^^ space) (app_typ false regtypes) typs in
+         if atyp_needed then parens tpp else tpp
+      | _ -> app_typ atyp_needed regtypes ty
+    and app_typ atyp_needed regtypes ((Typ_aux (t, _)) as ty) = match t with
+      | Typ_app(Id_aux (Id "vector", _),[_;_;_;Typ_arg_aux (Typ_arg_typ typa, _)]) ->
+         let tpp = string "vector" ^^ space ^^ typ regtypes typa in
+         if atyp_needed then parens tpp else tpp
+      | Typ_app(Id_aux (Id "range", _),_) ->
+         (string "number")
+      | Typ_app(Id_aux (Id "implicit", _),_) ->
+         (string "integer")
+      | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
+         (string "number")
+      | Typ_app(id,args) ->
+         (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem regtypes) args)
+      | _ -> atomic_typ atyp_needed regtypes ty 
+    and atomic_typ atyp_needed regtypes ((Typ_aux (t, _)) as ty) = match t with
+      | Typ_id (Id_aux (Id "bool",_)) -> string "bit"
+      | Typ_id ((Id_aux (Id name,_)) as id) ->
+         if List.exists ((=) name) regtypes then
+           string "register"
+         else
+           doc_id_lem_type id
+      | Typ_var v -> doc_var v
+      | Typ_wild -> underscore
+      | Typ_app _ | Typ_tup _ | Typ_fn _ ->
+         (* exhaustiveness matters here to avoid infinite loops
+          * if we add a new Typ constructor *)
+         let tpp = typ regtypes ty in
+         if atyp_needed then parens tpp else tpp
+    and doc_typ_arg_lem regtypes (Typ_arg_aux(t,_)) = match t with
+      | Typ_arg_typ t -> app_typ false regtypes t
+      | Typ_arg_nexp n -> empty
+      | Typ_arg_order o -> empty
+      | Typ_arg_effect e -> empty
+  in typ', atomic_typ
+
+(* doc_lit_lem gets as an additional parameter the type information from the
+ * expression around it: that's a hack, but how else can we distinguish between
+ * undefined values of different types ? *)
+let doc_lit_lem in_pat (L_aux(l,_)) a =
   utf8string (match l with
   | L_unit  -> "()"
   | L_zero  -> "O"
@@ -1892,45 +1929,52 @@ let doc_lit_lem in_pat (L_aux(l,_)) =
       else "("^ipp^" : i)")
   | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*)
-  | L_undef -> "Undef"
+  | L_undef ->
+     let (Base ((_,{t = t}),_,_,_,_,_)) = a in
+     (match t with
+      | Tid "bit"
+      | Tabbrev ({t = Tid "bit"},_) -> "Undef"
+      | Tapp ("register",_)
+      | Tabbrev ({t = Tapp ("register",_)},_) -> "UndefinedReg 0")
   | L_string s -> "\"" ^ s ^ "\"")
 
 (* typ_doc is the doc for the type being quantified *)
+
 let doc_typquant_lem (TypQ_aux(tq,_)) typ_doc = typ_doc
 
-let doc_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),_)) =
-  (doc_typquant tq (doc_typ_lem t))
+let doc_typschm_lem regtypes (TypSchm_aux(TypSchm_ts(tq,t),_)) =
+  (doc_typquant_lem tq (doc_typ_lem regtypes t))
 
 (*Note: vector concatenation, literal vectors, indexed vectors, and record should 
   be removed prior to pp. The latter two have never yet been seen
 *)
-let rec doc_pat_lem apat_needed (P_aux (p,(l,annot)) as pa) = match p with
+let rec doc_pat_lem apat_needed regtypes (P_aux (p,(l,annot)) as pa) = match p with
   | P_app(id, ((_ :: _) as pats)) ->
      (match annot with
       | Base(_,(Constructor _ | Enum _),_,_,_,_) ->
          let ppp = doc_unop (doc_id_lem_ctor true id)
-                            (parens (separate_map comma (doc_pat_lem true) pats)) in
+                            (parens (separate_map comma (doc_pat_lem true regtypes) pats)) in
          if apat_needed then parens ppp else ppp
       | _ -> empty)
   | P_app(id,[]) ->
     (match annot with
      | Base(_,(Constructor _| Enum _),_,_,_,_) -> doc_id_lem_ctor apat_needed id
      | _ -> empty)
-  | P_lit lit  -> doc_lit_lem true lit
+  | P_lit lit  -> doc_lit_lem true lit annot
   | P_wild -> underscore
   | P_id id -> doc_id_lem id
-  | P_as(p,id) -> parens (separate space [doc_pat_lem true p; string "as"; doc_id_lem id])
-  | P_typ(typ,p) -> doc_op colon (doc_pat_lem true p) (doc_typ_lem typ) 
+  | P_as(p,id) -> parens (separate space [doc_pat_lem true regtypes p; string "as"; doc_id_lem id])
+  | P_typ(typ,p) -> doc_op colon (doc_pat_lem true regtypes p) (doc_typ_lem regtypes typ) 
   | P_vector pats ->
      let ppp =
        (separate space)
-         [string "V";brackets (separate_map semi (doc_pat_lem true) pats);underscore;underscore] in
+         [string "V";brackets (separate_map semi (doc_pat_lem true regtypes) pats);underscore;underscore] in
      if apat_needed then parens ppp else ppp
   | P_tup pats  ->
      (match pats with
-      | [p] -> doc_pat_lem apat_needed p
-      | _ -> parens (separate_map comma_sp (doc_pat_lem false) pats))
-     | P_list pats -> brackets (separate_map semi (doc_pat_lem false) pats) (*Never seen but easy in lem*)
+      | [p] -> doc_pat_lem apat_needed regtypes p
+      | _ -> parens (separate_map comma_sp (doc_pat_lem false regtypes) pats))
+     | P_list pats -> brackets (separate_map semi (doc_pat_lem false regtypes) pats) (*Never seen but easy in lem*)
 
 let rec getregtyp_annot (Base ((_,t),_,_,_,_,_)) = 
   match t with
@@ -1946,8 +1990,8 @@ let rec getregtyp (LEXP_aux (le,(_,annot))) = match le with
      getregtyp le
 
 let doc_exp_lem, doc_let_lem =
-  let rec top_exp (aexp_needed : bool) (E_aux (e, (_,annot))) =
-    let exp = top_exp true in
+  let rec top_exp (regs,(regtypes : string list)) (aexp_needed : bool) (E_aux (e, (_,annot))) =
+    let exp = top_exp (regs,regtypes) true in
     match e with
     | E_assign((LEXP_aux(le_act,tannot) as le),e) ->
        (* can only be register writes *)
@@ -1962,12 +2006,12 @@ let doc_exp_lem, doc_let_lem =
                  let typprefix = getregtyp le ^ "_" in
                  (prefix 2 1)
                    (string "write_reg_field_range")
-                   (align (doc_lexp_deref_lem le ^^ space ^^ string typprefix ^^
+                   (align (doc_lexp_deref_lem (regs,regtypes) le ^^ space ^^ string typprefix ^^
                              doc_id_lem id ^/^ exp e2 ^/^ exp e3 ^/^ exp e))
             | _ ->
                (prefix 2 1)
                  (string "write_reg_range")
-                 (align (doc_lexp_deref_lem le ^^ space ^^ exp e2 ^/^ exp e3 ^/^ exp e))
+                 (align (doc_lexp_deref_lem (regs,regtypes) le ^^ space ^^ exp e2 ^/^ exp e3 ^/^ exp e))
            )
         | LEXP_vector (le,e2), (Tid "bit" | Tabbrev (_,{t=Tid "bit"})),_ ->
            (match le with
@@ -1978,24 +2022,24 @@ let doc_exp_lem, doc_let_lem =
                  let typprefix = getregtyp le ^ "_" in
                  (prefix 2 1)
                    (string "write_reg_field_bit")
-                   (align (doc_lexp_deref_lem le ^^ space ^^ string typprefix ^^
+                   (align (doc_lexp_deref_lem (regs,regtypes) le ^^ space ^^ string typprefix ^^
                              doc_id_lem id ^/^ exp e2 ^/^ exp e))
             | _ ->
                (prefix 2 1)
                  (string "write_reg_bit")
-                 (doc_lexp_deref_lem le ^^ space ^^ exp e2 ^/^ exp e)
+                 (doc_lexp_deref_lem (regs,regtypes) le ^^ space ^^ exp e2 ^/^ exp e)
            )
           | LEXP_field (le,id), (Tid "bit"| Tabbrev (_,{t=Tid "bit"})), _ ->
              let typprefix = getregtyp le ^ "_" in
              (prefix 2 1)
                (string "write_reg_bitfield")
-               (doc_lexp_deref_lem le ^^ space ^^ string typprefix ^^
+               (doc_lexp_deref_lem (regs,regtypes) le ^^ space ^^ string typprefix ^^
                   doc_id_lem id ^/^ exp e)
           | LEXP_field (le,id), _, _ ->
              let typprefix = getregtyp le ^ "_" in
              (prefix 2 1)
                (string "write_reg_field")
-               (doc_lexp_deref_lem le ^^ space ^^ string typprefix ^^
+               (doc_lexp_deref_lem (regs,regtypes) le ^^ space ^^ string typprefix ^^
                   doc_id_lem id ^/^ exp e)
           | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info ->
              (match alias_info with
@@ -2004,17 +2048,19 @@ let doc_exp_lem, doc_let_lem =
                    | (Tid "bit" | Tabbrev (_,{t=Tid "bit"})) ->
                       string "write_reg_bitfield"
                    | _ -> string "write_reg_bitfield" in
+                 let typ = match List.assoc reg regs with
+                   | Some typ -> typ
+                   | None -> failwith "Register type information missing" in
                  (prefix 2 1)
                    f
-                   (separate space [string reg;string (reg ^ "_" ^ field);exp e])
-                    (* the type should go instead of the lowercase reg *)
+                   (separate space [string reg;string (typ ^ "_" ^ field);exp e])
               | Alias_pair(reg1,reg2) ->
                  string "write_two_regs" ^^ space ^^ string reg1 ^^ space ^^
                    string reg2 ^^ space ^^ exp e)
           | _ ->
              (prefix 2 1)
                (string "write_reg")
-               (doc_lexp_deref_lem le ^/^ exp e))
+               (doc_lexp_deref_lem (regs,regtypes) le ^/^ exp e))
     | E_vector_append(l,r) ->
        let epp =
          align (separate space [exp l;string "^^"] ^/^ exp r) in
@@ -2023,17 +2069,15 @@ let doc_exp_lem, doc_let_lem =
     | E_if(c,t,e) ->
        let (E_aux (_,(_,cannot))) = c in
        let epp = 
-         (match cannot with
-          | Base ((_,({t = Tid "bit"})),_,_,_,_,_) ->
-             separate space [string "if";group (align (string "to_bool" ^//^ group (exp c)))]
-          | _ -> separate space [string "if";exp c])
+         separate space [string "if";group (align (string "to_bool" ^//^ group (exp c)))]
          ^^ break 1 ^^ 
-           (prefix 2 1 (string "then") (top_exp false t)) ^^ (break 1) ^^
-             (prefix 2 1 (string "else") (top_exp false e)) in
+           (prefix 2 1 (string "then") (top_exp (regs,regtypes) false t)) ^^ (break 1) ^^
+             (prefix 2 1 (string "else") (top_exp (regs,regtypes) false e)) in
        if aexp_needed then parens (align epp) else epp
     | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
        failwith "E_for should have been removed till now"
-    | E_let(leb,e) -> let_exp leb ^^ space ^^ string "in" ^/^ top_exp false e
+    | E_let(leb,e) -> let_exp (regs,regtypes) leb ^^ space ^^ string "in" ^/^
+                        top_exp (regs,regtypes) false e
     | E_app(f,args) ->
        (match f with
         (* temporary hack to make the loop body a function of the temporary variables *)
@@ -2054,7 +2098,7 @@ let doc_exp_lem, doc_let_lem =
                      (parens
                         ((prefix 1 1)
                            (separate space [string "fun";exp id;varspp;arrow])
-                           (top_exp false body)
+                           (top_exp (regs,regtypes) false body)
                         )
                      )
                  )
@@ -2065,7 +2109,7 @@ let doc_exp_lem, doc_let_lem =
                      (parens
                         ((prefix 1 1)
                            (separate space [string "fun";exp id;string "_";arrow])
-                           (top_exp false body)
+                           (top_exp (regs,regtypes) false body)
                         )
                      )
                  )
@@ -2073,7 +2117,8 @@ let doc_exp_lem, doc_let_lem =
         | _ ->
            (match annot with
             | Base (_,Constructor _,_,_,_,_) ->
-               let epp = doc_id_lem f ^^ space ^^ parens (separate_map comma (top_exp true) args) in
+               let epp = doc_id_lem f ^^ space ^^ 
+                           parens (separate_map comma (top_exp (regs,regtypes) true) args) in
                if aexp_needed then parens (align epp) else epp
             | Base (_,External (Some "bitwise_not_bit"),_,_,_,_) ->
                let [a] = args in
@@ -2139,17 +2184,18 @@ let doc_exp_lem, doc_let_lem =
         | Base((_,t),Alias alias_info,_,_,_,_) ->
            (match alias_info with
             | Alias_field(reg,field) ->
+               let typ = match List.assoc reg regs with
+                 | Some typ -> typ
+                 | None -> failwith "Register type information missing" in
                let epp = match t.t with
                  | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> 
                     (separate space)
                       [string "read_reg_bitfield"; string reg;
-                       string (reg ^ "_" ^ field)]
-                 (* the type should go instead of the lowercase reg *)
+                       string (typ ^ "_" ^ field)]
                  | _ -> 
                     (separate space)
                       [string "read_reg_field"; string reg;
-                       string (reg ^ "_" ^ field)] in
-                 (* the type should go instead of the lowercase reg *)
+                       string (typ ^ "_" ^ field)] in
                if aexp_needed then parens (align epp) else epp
             | Alias_pair(reg1,reg2) ->
                let epp = separate space [string "read_two_regs";string reg1;string reg2] in
@@ -2167,19 +2213,20 @@ let doc_exp_lem, doc_let_lem =
                if aexp_needed then parens (align epp) else epp
            )
         | _ -> doc_id_lem id)
-    | E_lit lit -> doc_lit_lem false lit
+    | E_lit lit -> doc_lit_lem false lit annot
     | E_cast(typ,e) ->
       (match annot with
       | Base(_,External _,_,_,_,_) -> string "read_reg" ^^ space ^^ exp e
-      | _ -> top_exp aexp_needed e) (*(parens (doc_op colon (group (exp e)) (doc_typ_lem typ)))) *)
+      | _ -> top_exp (regs,regtypes) aexp_needed e) (*(parens (doc_op colon (group (exp e)) (doc_typ_lem typ)))) *)
     | E_tuple exps ->
        (match exps with
-        | [e] -> top_exp aexp_needed e
-        | _ -> parens (separate_map comma (top_exp false) exps))
+        | [e] -> top_exp (regs,regtypes) aexp_needed e
+        | _ -> parens (separate_map comma (top_exp (regs,regtypes) false) exps))
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
-      anglebars (separate_map semi_sp doc_fexp fexps)
+       let epp = anglebars (separate_map semi_sp (doc_fexp (regs,regtypes)) fexps) in
+       if aexp_needed then parens epp else epp
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
-       anglebars (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps))
+       anglebars (doc_op (string "with") (exp e) (separate_map semi_sp (doc_fexp (regs,regtypes)) fexps))
     | E_vector exps ->
       (match annot with
        | Base((_,t),_,_,_,_,_) ->
@@ -2200,9 +2247,10 @@ let doc_exp_lem, doc_let_lem =
                 let (expspp,_) =
                   List.fold_left
                     (fun (pp,count) e ->
-                     (pp ^^ semi ^^ (if count = 20 then break 0 else empty) ^^ top_exp false e),
+                      (pp ^^ semi ^^ (if count = 20 then break 0 else empty) ^^
+                         top_exp (regs,regtypes) false e),
                      if count = 20 then 0 else count + 1)
-                    (top_exp false e,0) es in
+                    (top_exp (regs,regtypes) false e,0) es in
                 align (group expspp) in
            let epp =
              group (separate space [string "V"; brackets expspp;string start;string dir_out]) in
@@ -2246,7 +2294,7 @@ let doc_exp_lem, doc_let_lem =
                         raise (Reporting_basic.err_unreachable dl "nono") in
                    parens (string "Just " ^^ parens (string ("UndefinedReg " ^
                                                                string_of_big_int n))) in 
-            let iexp (i,e) = parens (doc_int i ^^ comma ^^ top_exp false e) in
+            let iexp (i,e) = parens (doc_int i ^^ comma ^^ top_exp (regs,regtypes) false e) in
             let expspp =
               match iexps with
               | [] -> empty
@@ -2271,12 +2319,12 @@ let doc_exp_lem, doc_let_lem =
                           group (exp e3)) in
      if aexp_needed then parens (align epp) else epp
   | E_list exps ->
-      brackets (separate_map semi (top_exp false) exps)
+      brackets (separate_map semi (top_exp (regs,regtypes) false) exps)
   | E_case(e,pexps) ->
      let epp = 
        (prefix 0 1)
          (separate space [string "match"; exp e; string "with"])
-         (separate_map (break 1) doc_case pexps) ^^ (break 1) ^^
+         (separate_map (break 1) (doc_case (regs,regtypes)) pexps) ^^ (break 1) ^^
          (string "end" ^^ (break 1)) in
      if aexp_needed then parens (align epp) else epp
   | E_exit e ->
@@ -2289,6 +2337,8 @@ let doc_exp_lem, doc_let_lem =
            let aux2 name = align (string name ^//^ exp e1 ^/^ exp e2) in
            align
              (match name with
+              | "power" -> aux "**"
+
               | "bitwise_and_bit" -> aux "&."
               | "bitwise_or_bit" -> aux "|."
               | "bitwise_xor_bit" -> aux "+."
@@ -2300,49 +2350,59 @@ let doc_exp_lem, doc_let_lem =
 
               | "add_vec" -> aux2 "add_VVV"
               | "add_vec_signed" -> aux2 "addS_VVV"
+              | "add_overflow_vec" -> aux2 "addO_VVV"
+              | "add_overflow_vec_signed" -> aux2 "addSO_VVV"
               | "minus_vec" -> aux2 "minus_VVV"
+              | "minus_overflow_vec" -> aux2 "minusO_VVV"
+              | "minus_overflow_vec_signed" -> aux2 "minusSO_VVV"
               | "multiply_vec" -> aux2 "mult_VVV"
               | "multiply_vec_signed" -> aux2 "multS_VVV"
+              | "mult_overflow_vec" -> aux2 "multO_VVV"
+              | "mult_overflow_vec_signed" -> aux2 "multSO_VVV"
+              | "quot_vec" -> aux2 "quot_VVV"
+              | "quot_vec_signed" -> aux2 "quotS_VVV"
+              | "quot_overflow_vec" -> aux2 "quotO_VVV"
+              | "quot_overflow_vec_signed" -> aux2 "quotSO_VVV"
+              | "mod_vec" -> aux2 "mod_VVV"
+
               | "add_vec_range" -> aux2 "add_VIV"
               | "add_vec_range_signed" -> aux2 "addS_VIV"
               | "minus_vec_range" -> aux2 "minus_VIV"
               | "mult_vec_range" -> aux2 "mult_VIV"
               | "mult_vec_range_signed" -> aux2 "multS_VIV"
               | "mod_vec_range" -> aux2 "minus_VIV"
+
               | "add_range_vec" -> aux2 "add_IVV"
               | "add_range_vec_signed" -> aux2 "addS_IVV"
               | "minus_range_vec" -> aux2 "minus_IVV"
               | "mult_range_vec" -> aux2 "mult_IVV"
               | "mult_range_vec_signed" -> aux2 "multS_IVV"
+
               | "add_range_vec_range" -> aux2 "add_IVI"
               | "add_range_vec_range_signed" -> aux2 "addS_IVI"
               | "minus_range_vec_range" -> aux2 "minus_IVI"
+
               | "add_vec_range_range" -> aux2 "add_VII"
               | "add_vec_range_range_signed" -> aux2 "addS_VII"
               | "minus_vec_range_range" -> aux2 "minus_VII"
               | "add_vec_vec_range" -> aux2 "add_VVI"
               | "add_vec_vec_range_signed" -> aux2 "addS_VVI"
+
               | "add_vec_bit" -> aux2 "add_VBV"
               | "add_vec_bit_signed" -> aux2 "addS_VBV"
-              | "minus_vec_bit_signed" -> aux2 "minus_VBV"
-              | "add_overflow_vec" -> aux2 "addO_VVV"
-              | "add_overflow_vec_signed" -> aux2 "addSO_VVV"
-              | "minus_overflow_vec" -> aux2 "minusO_VVV"
-              | "minus_overflow_vec_signed" -> aux2 "minusSO_VVV"
-              | "mult_overflow_vec" -> aux2 "multO_VVV"
-              | "mult_overflow_vec_signed" -> aux2 "multSO_VVV"
-              | "quot_overflow_vec" -> aux2 "quotO_VVV"
-              | "quot_overflow_vec_signed" -> aux2 "quotSO_VVV"
               | "add_overflow_vec_bit_signed" -> aux2 "addSO_VBV"
+              | "minus_vec_bit_signed" -> aux2 "minus_VBV"
               | "minus_overflow_vec_bit" -> aux2 "minusO_VBV"
               | "minus_overflow_vec_bit_signed" -> aux2 "minusSO_VBV"
 
               | _ ->
-                 string name ^//^ parens (top_exp false e1 ^^ comma ^/^ top_exp false e2)) in
+                 string name ^//^ parens (top_exp (regs,regtypes) false e1 ^^ comma ^/^
+                                            top_exp (regs,regtypes) false e2)) in
          if aexp_needed then parens (align epp) else epp
       | _ -> 
          let epp =
-           align (doc_id_lem id ^//^ parens (top_exp false e1 ^^ comma ^/^ top_exp false e2)) in
+           align (doc_id_lem id ^//^ parens (top_exp (regs,regtypes) false e1 ^^ comma ^/^
+                                               top_exp (regs,regtypes) false e2)) in
          if aexp_needed then parens (align epp) else epp)
   | E_internal_let(lexp, eq_exp, in_exp) ->
      failwith "E_internal_lets should have been removed till now"
@@ -2359,31 +2419,35 @@ let doc_exp_lem, doc_let_lem =
        let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
        match pat with
        | P_aux (P_wild,_) ->
-          (separate space [top_exp b e1; string ">>"]) ^/^
-            top_exp false e2
+          (separate space [top_exp (regs,regtypes) b e1; string ">>"]) ^/^
+            top_exp (regs,regtypes) false e2
        | _ ->
-          (separate space [top_exp b e1; string ">>= fun"; doc_pat_lem true pat;arrow]) ^/^
-            top_exp false e2 in
+          (separate space [top_exp (regs,regtypes) b e1; string ">>= fun";
+                           doc_pat_lem true regtypes pat;arrow]) ^/^
+            top_exp (regs,regtypes) false e2 in
      if aexp_needed then parens (align epp) else epp
   | E_internal_return (e1) ->
      separate space [string "return"; exp e1;]
-  and let_exp (LB_aux(lb,_)) = match lb with
+  and let_exp (regs,regtypes) (LB_aux(lb,_)) = match lb with
   | LB_val_explicit(_,pat,e)
   | LB_val_implicit(pat,e) ->
       prefix 2 1
-        (separate space [string "let"; doc_pat_lem true pat; equals])
-        (top_exp false e)
+        (separate space [string "let"; doc_pat_lem true regtypes pat; equals])
+        (top_exp (regs,regtypes) false e)
 
-  and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id_lem id) (top_exp false e)
+  and doc_fexp (regs,regtypes) (FE_aux(FE_Fexp(id,e),_)) =
+    doc_op equals (doc_id_lem id) (top_exp (regs,regtypes) true e)
 
-  and doc_case (Pat_aux(Pat_exp(pat,e),_)) =
-    group (prefix 3 1 (separate space [pipe; doc_pat_lem false pat;arrow]) (group (top_exp false e)))
+  and doc_case (regs,regtypes) (Pat_aux(Pat_exp(pat,e),_)) =
+    group (prefix 3 1 (separate space [pipe; doc_pat_lem false regtypes pat;arrow])
+                  (group (top_exp (regs,regtypes) false e)))
 
-  and doc_lexp_deref_lem ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
+  and doc_lexp_deref_lem (regs,regtypes) ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
     | LEXP_field (le,id) ->
-       parens (separate empty [doc_lexp_deref_lem le;dot;doc_id_lem id])
+       parens (separate empty [doc_lexp_deref_lem (regs,regtypes) le;dot;doc_id_lem id])
     | LEXP_vector(le,e) ->
-       parens ((separate space) [string "access";doc_lexp_deref_lem le;top_exp true e])
+       parens ((separate space) [string "access";doc_lexp_deref_lem (regs,regtypes) le;
+                                 top_exp (regs,regtypes) true e])
     | LEXP_id id -> doc_id_lem id
     | LEXP_cast (typ,id) -> doc_id_lem id
     | _ -> 
@@ -2392,8 +2456,9 @@ let doc_exp_lem, doc_let_lem =
   in top_exp, let_exp
 
 (*TODO Upcase and downcase type and constructors as needed*)
-let doc_type_union_lem (Tu_aux(typ_u,_)) = match typ_u with
-  | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor false id; string "of"; parens (doc_typ_lem typ)]
+let doc_type_union_lem regtypes (Tu_aux(typ_u,_)) = match typ_u with
+  | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor false id; string "of";
+                                        parens (doc_typ_lem regtypes typ)]
   | Tu_id id -> separate space [pipe; doc_id_lem_ctor false id]
 
 let rec doc_range_lem (BF_aux(r,_)) = match r with
@@ -2401,17 +2466,19 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with
   | BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2))
   | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
 
-let doc_typdef_lem (TD_aux(td,_)) = match td with
+let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
   | TD_abbrev(id,nm,typschm) ->
-      doc_op equals (concat [string "type"; space; doc_id_lem_type id;]) (doc_typscm_lem typschm)
+     doc_op equals (concat [string "type"; space; doc_id_lem_type id])
+            (doc_typschm_lem regtypes typschm)
   | TD_record(id,nm,typq,fs,_) ->
-      let f_pp (typ,id) = concat [doc_id_lem_type id; space; colon; doc_typ_lem typ; semi] in
+     let f_pp (typ,id) = concat [doc_id_lem_type id; space; colon;
+                                 doc_typ_lem regtypes typ; semi] in
       let fs_doc = group (separate_map (break 1) f_pp fs) in
       doc_op equals
              (concat [string "type"; space; doc_id_lem_type id;])
              (doc_typquant_lem typq (anglebars fs_doc))
   | TD_variant(id,nm,typq,ar,_) ->
-    let ar_doc = group (separate_map (break 1) doc_type_union_lem ar) in
+    let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in
     doc_op equals
       (concat [string "type"; space; doc_id_lem_type id;])
       (doc_typquant_lem typq ar_doc)
@@ -2426,32 +2493,33 @@ let doc_rec_lem (Rec_aux(r,_)) = match r with
   | Rec_nonrec -> space
   | Rec_rec -> space ^^ string "rec" ^^ space
 
-let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with
-  | Typ_annot_opt_some(tq,typ) -> doc_typquant_lem tq (doc_typ_lem typ)
+let doc_tannot_opt_lem regtypes (Typ_annot_opt_aux(t,_)) = match t with
+  | Typ_annot_opt_some(tq,typ) -> doc_typquant_lem tq (doc_typ_lem regtypes typ)
 
-let doc_funcl_lem (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
-  group (prefix 3 1 ((doc_pat_lem false pat) ^^ space ^^ arrow) (doc_exp_lem false exp))
+let doc_funcl_lem (regs,regtypes) (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
+  group (prefix 3 1 ((doc_pat_lem false regtypes pat) ^^ space ^^ arrow)
+                (doc_exp_lem (regs,regtypes) false exp))
 
 let get_id = function
   | [] -> failwith "FD_function with empty list"
   | (FCL_aux (FCL_Funcl (id,_,_),_))::_ -> id
 
-let doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),_)) =
+let doc_fundef_lem (regs,regtypes) (FD_aux(FD_function(r, typa, efa, fcls),_)) =
   match fcls with
   | [] -> failwith "FD_function with empty function list"
   | [FCL_aux (FCL_Funcl(id,pat,exp),_)] ->
      (prefix 2 1)
        ((separate space)
           [(string "let") ^^ (doc_rec_lem r) ^^ (doc_id_lem id);
-           (doc_pat_lem true pat);
+           (doc_pat_lem true regtypes pat);
            equals])
-       (doc_exp_lem false exp)
+       (doc_exp_lem (regs,regtypes) false exp)
   | _ ->
     let id = get_id fcls in
     (*    let sep = hardline ^^ pipe ^^ space in *)
     let clauses =
       (separate_map (break 1))
-        (fun fcl -> separate space [pipe;doc_funcl_lem fcl]) fcls in
+        (fun fcl -> separate space [pipe;doc_funcl_lem (regs,regtypes) fcl]) fcls in
     (prefix 2 1)
       ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"])
       (clauses ^/^ string "end")
@@ -2465,14 +2533,40 @@ let doc_dec_lem (DEC_aux (reg,(l,annot))) =
   | DEC_typ_alias(typ,id,alspec) -> empty (*
         doc_op equals (string "register alias" ^^ space ^^ doc_atomic_typ typ) (doc_alias alspec) *)
 
-let doc_def_lem def = match def with
+let rec rearrange_defs defs =
+
+  let name (Id_aux ((Id n | DeIid n),_)) = n in
+  
+  let rec find_def n (left,right) =
+    match right with
+    | [] -> failwith ("rearrange_defs definition for " ^ n ^ "not found")
+    | current :: right ->
+       match current with
+       | DEF_fundef (FD_aux (FD_function (_,_,_,(FCL_aux (FCL_Funcl (id,_,_),_)) :: _),_))
+       | DEF_val (LB_aux (LB_val_explicit (_,P_aux (P_id id,_),_),_))
+       | DEF_val (LB_aux (LB_val_implicit (P_aux (P_id id,_),_),_))
+            when n = name id ->
+          (current, left @ right)
+       | _ -> find_def n (left @ [current],right) in
+
+  match defs with
+  | [] -> []
+  | DEF_spec (VS_aux ((VS_val_spec (_,id)),_)) :: defs ->
+     let (d',defs') = find_def (name id) ([],defs) in
+     d' :: rearrange_defs defs'
+  | d :: defs -> d :: rearrange_defs defs
+
+
+
+
+let doc_def_lem (regs,regtypes) def = match def with
   | DEF_default df -> empty
-  | DEF_spec v_spec -> empty (*unless we want to have a separate pass to create mli files*)
-  | DEF_type t_def -> group (doc_typdef_lem t_def) ^/^ hardline
-  | DEF_fundef f_def -> group (doc_fundef_lem f_def) ^/^ hardline
-  | DEF_val lbind -> group (doc_let_lem lbind) ^/^ hardline
+  | DEF_spec v_spec -> empty (*doc_spec_lem regtypes v_spec ^/^ hardline *)
+  | DEF_type t_def -> group (doc_typdef_lem regtypes t_def) ^/^ hardline
+  | DEF_fundef f_def -> group (doc_fundef_lem (regs,regtypes) f_def) ^/^ hardline
+  | DEF_val lbind -> group (doc_let_lem (regs,regtypes) lbind) ^/^ hardline
   | DEF_reg_dec dec -> empty (*group (doc_dec_lem dec) ^/^ hardline *)
-  | DEF_scattered sdef -> empty (*shoulnd't still be here*)
+  | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point"
 
 let reg_decls (Defs defs) = 
 
@@ -2756,11 +2850,15 @@ let reg_decls (Defs defs) =
              regtostring_pp;regfieldtostring_pp;regbittostring_pp;
              field_index_bit_pp;field_indices_pp;
              regalias_pp;regstate_pp;reglength_pp;regstartindex_pp;
-             read_regstate_pp;write_regstate_pp],defs)
+             read_regstate_pp;write_regstate_pp],
+   regs,
+   List.map fst regtypes,
+   defs)
     
 let doc_defs_lem (Defs defs) =
-  let (decls,defs) = reg_decls (Defs defs) in
-  (decls,separate_map empty doc_def_lem defs)
+  let (decls,regs,regtypes,defs) = reg_decls (Defs defs) in
+  let defs = rearrange_defs defs in
+  (decls,separate_map empty (doc_def_lem (regs,regtypes)) defs)
 
 
 let pp_defs_lem f_arch f d top_line opens =
@@ -2768,7 +2866,8 @@ let pp_defs_lem f_arch f d top_line opens =
   print f
         (string "(*" ^^ (string top_line) ^^ string "*)" ^/^
            ((separate_map hardline)
-              (fun lib -> separate space [string "open import";string lib]) opens) ^/^ hardline ^^ defs);
+              (fun lib -> separate space [string "open import";string lib]) opens) ^/^
+             hardline ^^ defs);
   print f_arch
         (string "(*" ^^ (string top_line) ^^ string "*)" ^/^
            ((separate_map hardline)
diff --git a/src/process_file.ml b/src/process_file.ml
index 8dd6fd46..b3990ba4 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -178,7 +178,7 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
          let ((o2,_, _) as ext_o2) =
            open_output_with_check_unformatted (f' ^ "embed.lem") in
          (Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename))
-           ["Pervasives";"Vector";"State";"Arch";"Sail_values";"Power_extras"];
+           ["Pervasives";"Vector";"State";"Arch";"Sail_values"];
          close_output_with_check ext_o1;
          close_output_with_check ext_o2
       | Lem_out (Some lib) ->
@@ -187,7 +187,7 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
          let ((o2,_, _) as ext_o2) =
            open_output_with_check_unformatted (f' ^ "embed.lem") in
 	 (Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename))
-           ["Pervasives";"Vector";"State";"Arch";"Sail_values";"Power_extras"; lib];
+           ["Pervasives";"Vector";"State";"Arch";"Sail_values"; lib];
          close_output_with_check ext_o1;
          close_output_with_check ext_o2
       | Ocaml_out None ->
diff --git a/src/rewriter.ml b/src/rewriter.ml
index f920128a..9cda79f7 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -16,7 +16,6 @@ type 'a rewriters = { rewrite_exp  : 'a rewriters -> (nexp_map * 'a namemap) opt
                       rewrite_def  : 'a rewriters -> 'a def -> 'a def;
                       rewrite_defs : 'a rewriters -> 'a defs -> 'a defs;
                     }
-                    
 
 let fresh_name_counter = ref 0
 
@@ -796,6 +795,7 @@ let remove_vector_concat_pat pat =
         | P_vector _ -> P_aux (P_as (pat,fresh_name l),a)
         | P_id id -> P_aux (P_id id,a)
         | P_as (p,id) -> P_aux (P_as (p,id),a)
+        | P_wild -> P_aux (P_wild,a)
         | _ ->
            raise
              (Reporting_basic.err_unreachable
@@ -849,6 +849,11 @@ let remove_vector_concat_pat pat =
                 (* normal vector patterns are fine *)
                 | _ -> (pos + length, pat_acc @ [P_aux (p,cannot)],decl_acc) )
             (* non-vector patterns aren't *)
+            | (l,Base((_,{t = Tapp ("vector",[_;_;_;_])}),_,_,_,_,_))
+            | (l,Base((_,{t = Tabbrev (_,{t = Tapp ("vector",[_;_;_;_])})}),_,_,_,_,_)) ->
+               raise
+                 (Reporting_basic.err_unreachable
+                    l ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern"))
             | (l,Base((_,t),_,_,_,_,_)) ->
                raise
                  (Reporting_basic.err_unreachable
diff --git a/src/test/power.sail b/src/test/power.sail
index 7a66cb20..3c9a13e3 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -163,8 +163,7 @@ let (vector <0, 32, inc, (register<(bit[64])>) >) GPR =
   GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31
   ]
 
-(* adapted to make type checker accept SPR definition *)
-register (bit[(* 32 *) 0:63]) VRSAVE
+register (bit[32:63]) VRSAVE
 
 register (bit[64]) SPRG3
 register (bit[64]) SPRG4
@@ -173,7 +172,7 @@ register (bit[64]) SPRG6
 register (bit[64]) SPRG7
 
 let (vector <0, 1024, inc, (register<(bit[64])>) >) SPR =
-  [ 1=XER, 8=LR, 9=CTR, 256=VRSAVE, 259=SPRG3, 260=SPRG4, 261=SPRG5, 262=SPRG6, 263=SPRG7
+  [ 1=XER, 8=LR, 9=CTR(*, 256=VRSAVE (*32 bit, so not 64, caught by type checker at last*)*), 259=SPRG3, 260=SPRG4, 261=SPRG5, 262=SPRG6, 263=SPRG7
   ]
 
 (* XXX DCR is implementation-dependent; also, some DCR are only 32 bits
@@ -299,7 +298,7 @@ function  bit[64] DOUBLE word = {
   } else if word[1..8] == 0 & word[9..31] != 0 
   then {
     sign := word[0];
-    exp := 0 - 126;
+    exp := -126;
     (bit[53]) frac := 0b0 : word[9..31] : 0b00000000000000000000000000000;
     foreach (i from 0 to 52) {
       if frac[0] == 0 
@@ -308,7 +307,7 @@ function  bit[64] DOUBLE word = {
       else ()
      };
      temp[0] := sign;
-     temp[1..11] := (bit[10]) exp + 1023;
+     temp[1..11] := (bit[11]) exp + 1023;
      temp[12..63] := frac[1..52];
    } else {
      temp[0..1] := word[0..1];
@@ -328,7 +327,7 @@ function bit[32] SINGLE ((bit[64]) frs) = {
   else if (874 <= frs[1..11]) & (frs[1..11] <= 896)
   then { 
    sign := frs[0];
-   (bit[10]) exp := frs[1..11] - 1023;
+   (bit[11]) exp := frs[1..11] - 1023;
    (bit[53]) frac := 0b1 : frs[12..63];
    foreach (i from 0 to 53) {
      if exp < (0 - 126) 
@@ -1422,7 +1421,6 @@ function clause execute (Stdux (RS, RA, RB)) =
     MEMw(EA,8) := GPR[RS]
   }
 
-(*
 union ast member (bit[5], bit[5], bit[12], bit[4]) Lq
 
 function clause decode (0b111000 :
@@ -1450,9 +1448,7 @@ function clause execute (Lq (RTp, RA, DQ, PT)) =
       GPR[RTp + 1] := bytereverse[64 .. 127]
     }
   }
-*)
 
-(*
 union ast member (bit[5], bit[5], bit[14]) Stq
 
 function clause decode (0b111110 :
@@ -1462,7 +1458,6 @@ function clause decode (0b111110 :
 0b10 as instr) =
   Stq (RSp,RA,DS)
 
-
 function clause execute (Stq (RSp, RA, DS)) =
   {
     (bit[64]) b := 0;
@@ -1481,7 +1476,6 @@ function clause execute (Stq (RSp, RA, DS)) =
     EA := b + EXTS (DS : 0b00);
     MEMw(EA,8) := RSp
   }
-*)
 
 union ast member (bit[5], bit[5], bit[5]) Lhbrx
 
@@ -2229,7 +2223,6 @@ function clause execute (Mullw (RT, RA, RB, OE, Rc)) =
       if OE then set_SO_OV (overflow) else ()
     }
 
-(*
 union ast member (bit[5], bit[5], bit[5], bit) Mulhw
 
 function clause decode (0b011111 :
@@ -2251,7 +2244,7 @@ function clause execute (Mulhw (RT, RA, RB, Rc)) =
         overflow := o
       };
     (GPR[RT])[32..63] := prod[0 .. 31];
-    (GPR[RT])[0..31] := undefined;
+    (GPR[RT])[0..31] := (bit[32]) undefined;
     if Rc
     then {
       xer_so := XER.SO;
@@ -2261,9 +2254,7 @@ function clause execute (Mulhw (RT, RA, RB, Rc)) =
     }
     else ()
   }
-*)
 
-(*
 union ast member (bit[5], bit[5], bit[5], bit) Mulhwu
 
 function clause decode (0b011111 :
@@ -2279,7 +2270,7 @@ function clause execute (Mulhwu (RT, RA, RB, Rc)) =
   {
     (bit[64]) prod := (GPR[RA])[32 .. 63] * (GPR[RB])[32 .. 63];
     (GPR[RT])[32..63] := prod[0 .. 31];
-    (GPR[RT])[0..31] := undefined;
+    (GPR[RT])[0..31] := (bit[32]) undefined;
     if Rc
     then {
       xer_so := XER.SO;
@@ -2289,9 +2280,7 @@ function clause execute (Mulhwu (RT, RA, RB, Rc)) =
     }
     else ()
   }
-*)
 
-(*
 union ast member (bit[5], bit[5], bit[5], bit, bit) Divw
 
 function clause decode (0b011111 :
@@ -2316,7 +2305,7 @@ function clause execute (Divw (RT, RA, RB, OE, Rc)) =
         overflow := o
       };
     (GPR[RT])[32..63] := divided[32 .. 63];
-    (GPR[RT])[0..31] := undefined;
+    (GPR[RT])[0..31] := (bit[32]) undefined;
     if Rc
     then {
       xer_so := XER.SO;
@@ -2329,7 +2318,6 @@ function clause execute (Divw (RT, RA, RB, OE, Rc)) =
     if OE then set_SO_OV (overflow) else ()
   }
 
-
 union ast member (bit[5], bit[5], bit[5], bit, bit) Divwu
 
 function clause decode (0b011111 :
@@ -2354,7 +2342,7 @@ function clause execute (Divwu (RT, RA, RB, OE, Rc)) =
         overflow := o
       };
     (GPR[RT])[32..63] := divided[32 .. 63];
-    (GPR[RT])[0..31] := undefined;
+    (GPR[RT])[0..31] := (bit[32]) undefined;
     if Rc
     then {
       xer_so := XER.SO;
@@ -2392,7 +2380,7 @@ function clause execute (Divwe (RT, RA, RB, OE, Rc)) =
         overflow := o
       };
     (GPR[RT])[32..63] := divided[32 .. 63];
-    (GPR[RT])[0..31] := undefined;
+    (GPR[RT])[0..31] := (bit[32]) undefined;
     if Rc
     then {
       xer_so := XER.SO;
@@ -2430,7 +2418,7 @@ function clause execute (Divweu (RT, RA, RB, OE, Rc)) =
         overflow := o
       };
     (GPR[RT])[32..63] := divided[32 .. 63];
-    (GPR[RT])[0..31] := undefined;
+    (GPR[RT])[0..31] := (bit[32]) undefined;
     if Rc
     then {
       xer_so := XER.SO;
@@ -2442,7 +2430,6 @@ function clause execute (Divweu (RT, RA, RB, OE, Rc)) =
     else ();
     if OE then set_SO_OV (overflow) else ()
   }
-*)
 
 union ast member (bit[5], bit[5], bit[5], bit, bit) Mulld
 
@@ -2745,7 +2732,6 @@ function clause execute (Cmpl (BF, L, RA, RB)) =
     CR[4 * BF + 32..4 * BF + 35] := c : [XER.SO]
   }
 
-(*
 union ast member (bit[5], bit[5], bit[16]) Twi
 
 function clause decode (0b000011 :
@@ -2784,7 +2770,6 @@ function clause execute (Tw (TO, RA, RB)) =
     if a <_u b & TO[3] then trap () else ();
     if a >_u b & TO[4] then trap () else ()
   }
-*)
 
 union ast member (bit[5], bit[5], bit[16]) Tdi
 
@@ -3413,7 +3398,7 @@ function clause execute (Rldic (RS, RA, sh, mb, Rc)) =
     n := [sh[5]] : sh[0 .. 4];
     r := ROTL (GPR[RS],n);
     b := [mb[5]] : mb[0 .. 4];
-    m := MASK (b,(bit[5]) (~ (n)));
+    m := MASK (b,(bit[6]) (~ (n)));
     (bit[64]) temp := (r & m);
     GPR[RA] := temp;
     if Rc then set_overflow_cr0 (temp,XER.SO) else ()
@@ -3480,7 +3465,7 @@ function clause execute (Rldimi (RS, RA, sh, mb, Rc)) =
     n := [sh[5]] : sh[0 .. 4];
     r := ROTL (GPR[RS],n);
     b := [mb[5]] : mb[0 .. 4];
-    m := MASK (b,(bit[5]) (~ (n)));
+    m := MASK (b,(bit[6]) (~ (n)));
     (bit[64]) temp := (r & m | GPR[RA] & ~ (m));
     GPR[RA] := temp;
     if Rc then set_overflow_cr0 (temp,XER.SO) else ()
@@ -3640,7 +3625,7 @@ function clause execute (Sradi (RS, RA, sh, Rc)) =
     (bit[64]) temp := (r & m | s ^^ 64 & ~ (m));
     GPR[RA] := temp;
     if Rc then set_overflow_cr0 (temp,XER.SO) else ();
-    XER.CA := if n >_u (bit[5]) 0 then s & ~ ((r & ~ (m)) == 0) else 0
+    XER.CA := if n >_u (bit[6]) 0 then s & ~ ((r & ~ (m)) == 0) else 0
   }
 
 union ast member (bit[5], bit[5], bit[5], bit) Srad
@@ -3664,7 +3649,7 @@ function clause execute (Srad (RS, RA, RB, Rc)) =
     (bit[64]) temp := (r & m | s ^^ 64 & ~ (m));
     GPR[RA] := temp;
     if Rc then set_overflow_cr0 (temp,XER.SO) else ();
-    XER.CA := if n >_u (bit[5]) 0 then s & ~ ((r & ~ (m)) == 0) else 0
+    XER.CA := if n >_u (bit[6]) 0 then s & ~ ((r & ~ (m)) == 0) else 0
   }
 
 union ast member (bit[5], bit[5]) Cdtbcd
@@ -3769,7 +3754,7 @@ function clause execute (Mtspr (RS, spr)) =
     }
     else if length (SPR[n]) == 64
     then SPR[n] := GPR[RS]
-    else SPR[n] := (GPR[RS])[32 .. 63]
+    else SPR[n] := ((bit[32]) 0):(GPR[RS])[32 .. 63]
   }
 
 union ast member (bit[5], bit[10]) Mfspr
@@ -5920,7 +5905,6 @@ function clause decode (0b011111 :
 
 function clause execute (Lvsr (VRT, RA, RB)) = ()
 
-(*
 union ast member (bit[5], bit[5], bit[5]) Vpkpx
 
 function clause decode (0b000100 :
@@ -5943,7 +5927,6 @@ function clause execute (Vpkpx (VRT, VRA, VRB)) =
     (VR[VRT])[i + 75..i + 79] := (VR[VRB])[i * 2 + 24 .. i * 2 + 28]
   }
 
-
 union ast member (bit[5], bit[5], bit[5]) Vpkshss
 
 function clause decode (0b000100 :
@@ -6022,7 +6005,6 @@ function clause execute (Vpkswus (VRT, VRA, VRB)) =
         31]
   }
 
-
 union ast member (bit[5], bit[5], bit[5]) Vpkuhum
 
 function clause decode (0b000100 :
@@ -6039,7 +6021,6 @@ function clause execute (Vpkuhum (VRT, VRA, VRB)) =
     (VR[VRT])[i + 64..i + 71] := (VR[VRB])[i * 2 + 8 .. i * 2 + 15]
   }
 
-
 union ast member (bit[5], bit[5], bit[5]) Vpkuhus
 
 function clause decode (0b000100 :
@@ -6058,7 +6039,6 @@ function clause execute (Vpkuhus (VRT, VRA, VRB)) =
       (Clamp (EXTZ ((VR[VRB])[i * 2 .. i * 2 + 15]),0,255))[24 .. 31]
   }
 
-
 union ast member (bit[5], bit[5], bit[5]) Vpkuwum
 
 function clause decode (0b000100 :
@@ -6075,7 +6055,6 @@ function clause execute (Vpkuwum (VRT, VRA, VRB)) =
     (VR[VRT])[i + 64..i + 79] := (VR[VRB])[i * 2 + 16 .. i * 2 + 31]
   }
 
-
 union ast member (bit[5], bit[5], bit[5]) Vpkuwus
 
 function clause decode (0b000100 :
@@ -10376,8 +10355,6 @@ function clause decode (0b011111 :
   Dcbf (L,RA,RB)
 
 function clause execute (Dcbf (L, RA, RB)) = ()
-*)
-
 
 union ast member Isync
 
@@ -10640,8 +10617,8 @@ function bit illegal_instructions_pred ((ast) instr) = {
         case (Stfdp(FRSp,RA,DS)) -> (FRSp mod 2 == 1)
         case (Lfdpx(FRTp,RA,RB)) -> (FRTp mod 2 == 1)
         case (Stfdpx(FRSp,RA,RB)) -> (FRSp mod 2 == 1)
-                                       (*case (Lq(RTp,RA,DQ,Pt)) -> ((RTp mod 2 ==1) | RTp == RA)
-        case (Stq(RSp,RA,RS)) -> (RSp mod 2 == 1) *)
+        case (Lq(RTp,RA,DQ,Pt)) -> ((RTp mod 2 ==1) | RTp == RA)
+        case (Stq(RSp,RA,RS)) -> (RSp mod 2 == 1)
         case (Mtspr(RS, spr)) ->
           ~ ((spr == 1) | (spr == 8) | (spr == 9) | (spr == 256) |
             (spr == 512) | (spr == 896) | (spr == 898))