added prompt.lem for connecting to concurrency model and {power,armv8}_extras.lem; fixes

7 files changed, 674 insertions, 142 deletions

diff --git a/src/gen_lib/armv8_extras.lem b/src/gen_lib/armv8_extras.lem
new file mode 100644
index 00000000..54304225
--- /dev/null
+++ b/src/gen_lib/armv8_extras.lem
@@ -0,0 +1,50 @@
+open import Pervasives
+open import State
+open import Sail_values
+import Set_extra
+
+(*
+let memory_parameter_transformer mode v =
+  let mode = <|mode with endian = E_big_endian|> in
+  match v with
+  | Interp.V_tuple [location;length] ->
+    match length with
+    | Interp.V_lit (L_aux (L_num len) _) ->
+      let (v,regs) = extern_mem_value mode location in
+      (v,(natFromInteger len),regs)
+    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+      let (v,loc_regs) = extern_mem_value mode location in
+      match loc_regs with
+      | Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
+      | Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
+      end
+    end
+  end
+ *)
+let rMem_NORMAL (addr,l) = read_memory (unsigned addr) l
+let rMem_STREAM (addr,l) = read_memory (unsigned addr) l
+let rMem_ORDERED (addr,l) = read_memory (unsigned addr) l
+let rMem_ATOMIC (addr,l) = read_memory (unsigned addr) l
+let rMem_ATOMIC_ORDERED (addr,l) = read_memory (unsigned addr) l
+
+let wMem_NORMAL (addr,l,v) = write_memory (unsigned addr) l v
+let wMem_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
+let wMem_ATOMIC (addr,l,v) = write_memory (unsigned addr) l v
+let wMem_ATOMIC_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
+
+let wMem_Addr_NORMAL (addr,l) = write_writeEA (unsigned addr) l
+let wMem_Addr_ORDERED (addr,l) = write_writeEA (unsigned addr) l
+let wMem_Addr_ATOMIC (addr,l) = write_writeEA (unsigned addr) l
+let wMem_Addr_ATOMIC_ORDERED (addr,l) = write_writeEA (unsigned addr) l
+
+let wMem_Val_NORMAL l v = read_writeEA () >>= fun (addr,_) -> write_memory addr l v
+let wMem_Val_ATOMIC l v = read_writeEA () >>= fun (addr,_) -> write_memory addr l v
+
+let DataMemoryBarrier_Reads = return ()
+let DataMemoryBarrier_Writes = return ()
+let DataMemoryBarrier_All = return ()
+let DataSynchronizationBarrier_Reads = return ()
+let DataSynchronizationBarrier_Writes = return ()
+let DataSynchronizationBarrier_All = return ()
+let InstructionSynchronizationBarrier = return ()
+
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem
new file mode 100644
index 00000000..f2941aff
--- /dev/null
+++ b/src/gen_lib/power_extras.lem
@@ -0,0 +1,35 @@
+open import Pervasives
+open import State
+open import Sail_values
+
+(*
+let rec countLeadingZeros_helper bits =  
+((match bits with
+    | (Interp.V_lit (L_aux( L_zero, _)))::bits -> 
+      let (Interp.V_lit (L_aux( (L_num n), loc))) = (countLeadingZeros_helper bits) in
+      Interp.V_lit (L_aux( (L_num (Nat_big_num.add n(Nat_big_num.of_int 1))), loc))
+    | _ -> Interp.V_lit (L_aux( (L_num(Nat_big_num.of_int 0)), Interp_ast.Unknown))
+))
+let rec countLeadingZeros (Interp.V_tuple v) = ((match v with
+  | [Interp.V_track( v, r);Interp.V_track( v2, r2)] -> 
+    Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) ( Pset.(union) r r2)
+  | [Interp.V_track( v, r);v2] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r
+  | [v;Interp.V_track( v2, r2)] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r2
+  | [Interp.V_unknown;_] -> Interp.V_unknown
+  | [_;Interp.V_unknown] -> Interp.V_unknown
+  | [Interp.V_vector( _, _, bits);Interp.V_lit (L_aux( (L_num n), _))] -> 
+    countLeadingZeros_helper (snd (Lem_list.split_at (abs (Nat_big_num.to_int n)) bits))
+))
+ *)
+
+let MEMr (addr,l) = read_memory (unsigned addr) l
+let MEMr_reserve (addr,l) = read_memory (unsigned addr) l
+
+let MEMw (addr,l,value) = write_memory (unsigned addr) l value
+let MEMw_conditional (addr,l,value) = write_memory (unsigned addr) l value >> return true
+
+let I_Sync () = return ()
+let H_Sync () = return ()
+let LW_Sync () = return ()
+let EIEIO_Sync () = return ()
+
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
new file mode 100644
index 00000000..0b616b7e
--- /dev/null
+++ b/src/gen_lib/prompt.lem
@@ -0,0 +1,299 @@
+open import Pervasives_extra
+open import Vector
+open import Arch
+
+let compose f g x = f (g x)
+
+type end_flag =
+  | E_big_endian
+  | E_little_endian
+
+type direction = 
+  | D_increasing
+  | D_decreasing
+
+type register_value = <| 
+    rv_bits: list bit (* MSB first, smallest index number *); 
+    rv_dir: direction; 
+    rv_start: nat ;
+    rv_start_internal: nat; 
+    (*when dir is increasing, rv_start = rv_start_internal. 
+      Otherwise, tells interpreter how to reconstruct a proper decreasing value*)
+    |>
+
+type byte = list bit (* of length 8 *)  (*MSB first everywhere*)
+
+type address = integer
+type address_lifted = address
+
+type memory_value = list byte
+(* the list is of length >=1 *)
+(* for both big-endian (Power) and little-endian (ARM), the head of the
+     list is the byte stored at the lowest address *)
+(* for big-endian Power the head of the list is the most-significant
+   byte, in both the interpreter and machineDef* code. *)
+(* For little-endian ARM, the head of the list is the
+   least-significant byte in machineDef* code and the
+   most-significant byte in interpreter code, with the switch over
+   (a list-reverse) being done just inside the interpreter interface*)
+(* In other words, in the machineDef* code the lowest-address byte is first,
+   and in the interpreter code the most-significant byte is first *)
+
+type opcode = Opcode of list byte (* of length 4 *)
+
+type read_kind =
+  (* common reads *)
+  | Read_plain
+  (* Power reads *)
+  | Read_reserve
+  (* AArch64 reads *)
+  | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
+
+type write_kind =
+  (* common writes *)
+  | Write_plain
+  (* Power writes *)
+  | Write_conditional
+  (* AArch64 writes *)
+  | Write_release | Write_exclusive | Write_exclusive_release
+
+type barrier_kind =
+  (* Power barriers *)
+  | Sync | LwSync | Eieio | Isync
+  (* AArch64 barriers *)
+  | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB 
+
+type slice = (nat * nat)
+
+type reg_name = 
+  (* Name of the register, accessing the entire register, the start and size of this register, 
+   * and its direction *)
+  | Reg of string * nat * nat * direction
+                                  
+  (* Name of the register, accessing from the bit indexed by the first
+   * to the bit indexed by the second integer of the slice, inclusive. For
+   * machineDef* the first is a smaller number or equal to the second.  *)
+  | Reg_slice of string * nat * direction * slice 
+                                              
+  (* Name of the register, start and direction, and name of the field of the register
+   * accessed. The slice specifies where this field is in the register*)
+  | Reg_field of string * nat * direction * string * slice 
+
+  (* The first four components are as in Reg_field; the final slice
+   * 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 =
+  (* 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 *)
+  (* address_lifted should go away: doesn't make sense to allow for undefined bits in addresses *)
+  | Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) *
+                  (memory_value -> outcome 'a)
+                    
+  (* Request to write memory, first value and dependent registers is location, second is the value 
+   * to write *)
+  | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value *
+                   maybe (list reg_name) * (bool -> outcome 'a)
+                                             
+  (* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *)
+  | Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * outcome 'a
+                                                                              
+  (* Request to write memory at last signaled address. Memory value should be 8* the size given in 
+   * ea signal *)
+  | Write_memv of memory_value * maybe (list reg_name) * (bool -> outcome 'a)
+                                                           
+  (* Request a memory barrier *)
+  (* outcome 'a used to be (unit -> outcome 'a), but since the code is purely functional we don't 
+   * need that *)
+  | Barrier of barrier_kind * outcome 'a
+                                
+  (* Tell the system to dynamically recalculate dependency footprint *)
+  | Footprint of outcome 'a
+                   
+  (* Request to read register *)
+  | Read_reg of reg_name * (register_value -> outcome 'a)
+                             
+  (* Request to write register *)
+  | Write_reg of reg_name * register_value * outcome 'a
+                                               
+  (* List of instruction states to be run in parrallel, any order permitted.
+     Expects concurrency model to choose an order: a permutation of the original list *)
+  | Nondet_choice of list (outcome unit) * (list (outcome unit) -> 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) *)
+
+  (* Stop for incremental stepping, function can be used to display function call data *)
+  | Done of 'a
+
+type M 'a = outcome 'a
+
+val return : forall 'a. 'a -> M 'a
+let return a = Done a
+
+val bind : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b
+let rec bind m f = match m with
+  | Done a -> f a
+  | Read_mem rk addr sz rs k ->        Read_mem rk addr sz rs        (fun v -> bind (k v) f)
+  | Write_mem wk addr sz rs v rs2 k -> Write_mem wk addr sz rs v rs2 (fun b -> bind (k b) f)
+  | Write_ea wk addr sz rs k ->        Write_ea wk addr sz rs        (bind k f)
+  | Write_memv v rs k ->               Write_memv v rs               (fun b -> bind (k b) f)
+  | Barrier bk k ->                    Barrier bk                    (bind k f)
+  | Footprint k ->                     Footprint                     (bind k f)
+  | Read_reg reg k ->                  Read_reg reg                  (fun v -> bind (k v) f)
+  | Write_reg reg v k ->               Write_reg reg v               (bind k f)
+  | Nondet_choice actions k ->         Nondet_choice actions         (fun c -> bind (k c) f)
+  | Escape -> Escape
+  end
+
+val exit : forall 'a 'e. 'e -> M 'a
+let exit _ = Escape
+
+let (>>=) = bind
+let (>>) m n = m >>= fun _ -> n
+
+val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
+let rec byte_chunks n list = match (n,list) with
+  | (0,_) -> []
+  | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest
+  | _ -> failwith "byte_chunks not given enough bits"
+end
+
+val bitvFromBytes : list byte -> vector bit
+let bitvFromBytes v = V (foldl (++) [] v) 0 defaultDir
+
+let dir is_inc = if is_inc then D_increasing else D_decreasing
+
+val bitvFromRegisterValue : register_value -> vector bit
+let bitvFromRegisterValue v =
+  V (v.rv_bits) (integerFromNat (v.rv_start)) (v.rv_dir = D_increasing)
+
+val registerValueFromBitv : vector bit -> register -> register_value
+let registerValueFromBitv (V bits start is_inc) reg = 
+  let start = natFromInteger start in
+  <| rv_bits = bits;
+     rv_dir = dir is_inc;
+     rv_start_internal = start;
+     rv_start = start+1 - (natFromInteger (length_reg reg)) |>
+
+val read_memory : read_kind -> integer -> integer -> M (vector bit)
+let read_memory rk addr sz =
+  let sz = natFromInteger sz in
+  Read_mem rk addr sz Nothing (compose Done bitvFromBytes)
+
+val write_memory : write_kind -> integer -> integer -> vector bit -> M bool
+let write_memory wk addr sz (V v _ _) =
+  let sz = natFromInteger sz in
+  Write_mem wk addr sz Nothing (byte_chunks sz v) Nothing Done
+
+val read_reg_range : register -> (integer * integer) -> M (vector bit)
+let read_reg_range reg (i,j) =
+  let (i,j) = (natFromInteger i,natFromInteger j) in
+  let start = natFromInteger (start_index_reg reg) in
+  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
+  Read_reg reg (compose Done bitvFromRegisterValue)
+
+val write_reg_range : register -> (integer * integer) -> vector bit -> M unit
+let write_reg_range reg (i,j) v =
+  let rv = registerValueFromBitv v reg in
+  let start = natFromInteger (start_index_reg reg) in
+  let (i,j) = (natFromInteger i,natFromInteger j) in
+  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
+  Write_reg reg rv (Done ())
+
+val read_reg_bit : register -> integer -> M bit
+let read_reg_bit reg i = 
+  let i = natFromInteger i in
+  let start = natFromInteger (start_index_reg reg) in
+  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,i) in
+  Read_reg reg (fun v -> Done (access (bitvFromRegisterValue v) 1))
+
+val write_reg_bit : register -> integer -> bit -> M unit
+let write_reg_bit reg i bit = write_reg_range reg (i,i) (V [bit] 0 true)
+
+val read_reg : register -> M (vector bit)
+let read_reg reg =
+  let start = natFromInteger (start_index_reg reg) in
+  let sz = natFromInteger (length_reg reg) in
+  let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
+  Read_reg reg (compose Done bitvFromRegisterValue)
+
+val write_reg : register -> vector bit -> M unit
+let write_reg reg v =
+  let rv = registerValueFromBitv v reg in
+  let start = natFromInteger (start_index_reg reg) in
+  let sz = natFromInteger (length_reg reg) in
+  let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
+  Write_reg reg rv (Done ())
+
+val read_reg_field : register -> register_field -> M (vector bit)
+let read_reg_field reg rfield = 
+  let (i,j) =
+    let (i,j) = field_indices rfield in
+    (natFromInteger i,natFromInteger j) in
+  let start = natFromInteger (start_index_reg reg) in
+  let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
+  Read_reg reg (compose Done bitvFromRegisterValue)
+
+val write_reg_field : register -> register_field -> vector bit -> M unit
+let write_reg_field reg rfield = write_reg_range reg (field_indices rfield)
+
+val read_reg_field_bit : register -> register_field_bit -> M bit
+let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit)
+
+val write_reg_field_bit : register -> register_field_bit -> bit -> M unit
+let write_reg_field_bit reg rbit = write_reg_bit reg (field_index_bit rbit)
+
+val foreach_inc :  forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
+                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
+let rec foreach_inc (i,stop,by) vars body = 
+  if i <= stop
+  then
+    let (_,vars) = body i vars in
+    foreach_inc (i + by,stop,by) vars body
+  else ((),vars)
+
+val foreach_dec : forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
+                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
+let rec foreach_dec (i,stop,by) vars body = 
+  if i >= stop
+  then
+    let (_,vars) = body i vars in
+    foreach_dec (i - by,stop,by) vars body
+  else ((),vars)
+
+
+val foreachM_inc : forall 'vars. (nat * nat * nat) -> 'vars ->
+                  (nat -> 'vars -> M (unit * 'vars)) -> M (unit * 'vars)
+let rec foreachM_inc (i,stop,by) vars body = 
+  if i <= stop
+  then
+    body i vars >>= fun (_,vars) ->
+    foreachM_inc (i + by,stop,by) vars body
+  else return ((),vars)
+
+
+val foreachM_dec : forall 'vars. (nat * nat * nat) -> 'vars ->
+                  (nat -> 'vars -> M (unit * 'vars)) -> M (unit * 'vars)
+let rec foreachM_dec (i,stop,by) vars body = 
+  if i >= stop
+  then
+    body i vars >>= fun (_,vars) ->
+    foreachM_dec (i - by,stop,by) vars body
+  else return ((),vars)
+
+
+let length l = integerFromNat (length l)
+
+let write_two_regs r1 r2 vec =
+  let size = length_reg r1 in
+  let start = get_start vec in
+  let vsize = length vec in
+  let r1_v = slice vec start ((if defaultDir then size - start else start - size) - 1) in
+  let r2_v =
+    (slice vec)
+      (if defaultDir then size - start else start - size)
+      (if defaultDir then vsize - start else start - vsize) in
+  write_reg r1 r1_v >> write_reg r2 r2_v
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index aa0578b2..b02e47cb 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -1,4 +1,4 @@
-open import Pervasives
+open import Pervasives_extra
 open import State
 open import Vector
 open import Arch
@@ -9,7 +9,10 @@ let length l = integerFromNat (length l)
 
 let has_undef (V bs _ _) = List.any (function Undef -> true | _ -> false end) bs
 
-let most_significant (V bs _ _) = let (b :: _) = bs in b
+let most_significant = function
+  | (V (b :: _) _ _) -> b
+  | _ -> failwith "most_significant applied to empty vector"
+  end
 
 let bitwise_not_bit = function
   | I -> O
@@ -57,16 +60,15 @@ let bitwise_or = bitwise_binop (||)
 let bitwise_xor = bitwise_binop xor
 
 let unsigned (V bs _ _ as v) : integer =
-  match has_undef v with
-  | true ->
-     fst (List.foldl
-            (fun (acc,exp) b -> (acc + (if b = I then integerPow 2 exp else 0),exp +1)) (0,0) bs)
-  end
+  if has_undef v then failwith "unsigned applied to vector with undefined bits" else
+    fst (List.foldl
+           (fun (acc,exp) b -> (acc + (if b = I then integerPow 2 exp else 0),exp +1)) (0,0) bs)
 
 let signed v : integer =
   match most_significant v with
   | I -> 0 - (1 + (unsigned (bitwise_not v)))
   | O -> unsigned v
+  | _ -> failwith "signed applied to vector with undefined bits"
   end
 
 let to_num sign = if sign then signed else unsigned
@@ -114,6 +116,7 @@ let rec add_one_bit bs co (i : integer) =
     | (O,true)  -> add_one_bit (replace bs (natFromInteger i,I)) true (i-1)
     | (I,false) -> add_one_bit (replace bs (natFromInteger i,O)) true (i-1)
     | (I,true)  -> add_one_bit bs true (i-1)
+    | _ -> failwith "add_one_bit applied to list with undefined bit"
    (*    | Vundef,_ -> assert false*) 
   end
 
@@ -215,7 +218,7 @@ let add_VII = arith_op_vec_range_range integerAdd false
 let addS_VII = arith_op_vec_range_range integerAdd true
 let minus_VII = arith_op_vec_range_range integerMinus false
 
-let arith_op_vec_vec_range op sign (V _ _ is_inc as l) r = 
+let arith_op_vec_vec_range op sign l r = 
   let (l',r') = (to_num sign l,to_num sign r) in
   op l' r'
 
@@ -276,6 +279,7 @@ let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (siz
   let (n,nu,changed) = match r_bit with
     | I -> (op l' 1, op l_u 1, true)
     | O -> (l',l_u,false)
+    | _ -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
     end in
 (*    | _ -> assert false *)
   let correct_size_num = to_vec is_inc (act_size,n) in
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index ac65a347..eeff4717 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,10 +1,26 @@
-open import Pervasives
+open import Pervasives_extra
 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 memstate = map integer (list bit)
+
+type state =
+  <| regstate : regstate;
+     memstate : memstate;
+     writeEA : integer * integer|>
+
+let compose f g x = f (g x)
+
+val ints_aux : list integer -> integer -> list integer
+let rec ints_aux acc x = 
+  if x = 0 then []
+  else ints_aux ((x - 1) :: acc) (x - 1)
+
+let ints = ints_aux []
+
 val return : forall 's 'e 'a. 'a -> M 's 'e 'a
 let return a s = (Left a,s)
 
@@ -20,6 +36,44 @@ let exit e s = (Right e,s)
 let (>>=) = bind
 let (>>) m n = m >>= fun _ -> n
 
+val read_writeEA : forall 'e. unit -> M state 'e (integer * integer)
+let read_writeEA () s = (Left s.writeEA,s)
+
+val write_writeEA : forall 'e. integer -> integer -> M 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)
+let rec byte_chunks n l =
+  if n = 0 then []
+  else
+    match l with
+    | a::b::c::d::e::f::g::h::rest -> [a;b;c;d;e;f;g;h] :: byte_chunks (n - 1) rest
+    | _ -> failwith "byte_chunks not given enough bits"
+    end
+
+val read_regstate : state -> register -> vector bit
+let read_regstate s = read_regstate_aux s.regstate
+
+val write_regstate : state -> register -> vector bit -> state
+let write_regstate s reg v = <| s with regstate = (write_regstate_aux s.regstate reg v) |>
+
+val read_memstate : memstate -> integer -> list bit
+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)
+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
+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)
 let read_reg_range reg (i,j) s =
   let v = slice (read_regstate s reg) i j in
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index 9efae768..ad0ba1db 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -1,17 +1,18 @@
-open import Pervasives
+open import Pervasives_extra
 
 type bit = O | I | Undef
 type vector 'a = V of list 'a * integer * bool
 
-let rec nth xs (n : integer) = match (n,xs) with
-  | (0,x :: xs) -> x
-  | (n + 1,x :: xs) -> nth xs n
-end
-
+let rec nth xs (n : integer) =
+  match xs with
+  | x :: xs -> if n = 0 then x else nth xs (n - 1)
+  | _ -> failwith "nth applied to empty list"
+  end
 
 let to_bool = function
   | O -> false
   | I  -> true
+  | Undef -> failwith "to_bool applied to Undef"
   end
 
 let get_start (V _ s _) = s
@@ -24,8 +25,10 @@ let rec replace bs ((n : nat),b') = match (n,bs) with
   end
 
 let make_indexed_vector_reg entries default start length =
-  let (Just v) = default in
-  V (List.foldl replace (replicate length v) entries) start
+  match default with
+  | Just v -> V (List.foldl replace (replicate length v) entries) start
+  | Nothing -> failwith "make_indexed_vector used without default value"
+  end
 
 let make_indexed_vector_bit entries default start length =
   let default = match default with Nothing -> Undef | Just v -> v end in
@@ -60,9 +63,6 @@ let update (V bs start is_inc) n m (V bs' _ _) =
   let start = integerFromNat start in
   V (prefix ++ (List.take length bs') ++ suffix) start is_inc
 
-let hd (x :: _) = x
-
-
 val access : forall 'a. vector 'a -> (*nat*) integer -> 'a
 let access (V bs start is_inc) n =
   if is_inc then nth bs (n - start) else nth bs (start - n)
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 0006f290..7e2e87b0 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1835,7 +1835,7 @@ let doc_id_lem_ctor aexp_needed (Id_aux(i,_)) =
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
      let epp = separate space [colon; string (String.capitalize x); empty] in
-     if aexp_needed then parens epp else epp
+     if aexp_needed then parens (align epp) else epp
 
 let doc_typ_lem, doc_atomic_typ_lem =
   (* following the structure of parser for precedence *)
@@ -1963,36 +1963,49 @@ let doc_exp_lem, doc_let_lem =
        (* can only be register writes *)
        let (_,(Base ((_,{t = t}),tag,_,_,_,_))) = tannot in
        let E_aux (_,(_,(Base ((_,{t = et}),_,_,_,_,_)))) = e in
-       let (f,args) = 
-         (match tag with
-          | External _ ->
-             (match le_act with
-              | LEXP_vector (le,e2) ->
-                 (string "write_reg_bit",[doc_lexp_deref_lem le;exp e2;exp e])
-              | LEXP_vector_range (le,e2,e3) ->
-                 (string "write_reg_range",[doc_lexp_deref_lem le;
-                                            parens (exp e2 ^^ comma ^^ exp e3);
-                                            exp e])
-              | LEXP_field (lexp,id) ->
-                 let typprefix = String.uncapitalize (getregtyp lexp) ^ "_" in
-                 (match et with
-                  | Tid "bit"
-                  | Tabbrev (_,{t=Tid "bit"}) ->
-                     (string "write_reg_field_bit"),
-                     [doc_lexp_deref_lem lexp;string typprefix ^^ doc_id_lem id;exp e]
-                  | Tapp ("vector",_)
-                  | Tabbrev (_,{t=Tapp ("vector",_)}) ->
-                     (string "write_reg_field",
-                      [doc_lexp_deref_lem lexp;string typprefix ^^ doc_id_lem id;exp e])
-                  | _ -> failwith (t_to_string {t = et})
-                 )
-              | (LEXP_id _ | LEXP_cast _) -> (string "write_reg",[doc_lexp_deref_lem le;exp e]))
-          | _ -> (string "write_reg",[doc_lexp_deref_lem le;exp e])
-         ) in
-       prefix 2 1 f (separate (break 1) args)
+       (match tag with
+        | External _ ->
+           (match le_act with
+            | LEXP_vector (le,e2) ->
+               (prefix 2 1)
+                 (string "write_reg_bit")
+                 (doc_lexp_deref_lem le ^^ space ^^
+                    exp e2 ^/^ exp e)
+            | LEXP_vector_range (le,e2,e3) ->
+               (prefix 2 1)
+                 (string "write_reg_range")
+                 (align (doc_lexp_deref_lem le ^^ space ^^
+                           (parens (group (align (exp e2 ^^ comma ^^ break 0 ^^ exp e3)))) ^/^
+                             exp e))
+            | LEXP_field (lexp,id) ->
+               let typprefix = String.uncapitalize (getregtyp lexp) ^ "_" in
+               (match et with
+                | Tid "bit"
+                | Tabbrev (_,{t=Tid "bit"}) ->
+                   (prefix 2 1)
+                     (string "write_reg_field_bit")
+                     (doc_lexp_deref_lem lexp ^^ space ^^ string typprefix ^^ doc_id_lem id ^/^
+                        exp e)
+                | Tapp ("vector",_)
+                | Tabbrev (_,{t=Tapp ("vector",_)}) ->
+                   (prefix 2 1)
+                     (string "write_reg_field")
+                     (doc_lexp_deref_lem lexp ^^ space ^^ string typprefix ^^ doc_id_lem id ^/^
+                        exp e)
+                | _ -> failwith (t_to_string {t = et})
+               )
+            | (LEXP_id _ | LEXP_cast _) ->
+               (prefix 2 1)
+                 (string "write_reg")
+                 (doc_lexp_deref_lem le ^/^ exp e))
+        | _ ->
+           (prefix 2 1)
+             (string "write_reg")
+             (doc_lexp_deref_lem le ^/^ exp e)
+       )
     | E_vector_append(l,r) ->
        let epp =
-         align (separate space [exp l;string "^^"] ^//^ exp r) in
+         align (separate space [exp l;string "^^"] ^/^ exp r) in
        if aexp_needed then parens epp else epp
     | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r)
     | E_if(c,t,e) ->
@@ -2000,12 +2013,12 @@ let doc_exp_lem, doc_let_lem =
        let epp = 
          (match cannot with
           | Base ((_,({t = Tid "bit"})),_,_,_,_,_) ->
-             separate space [string "if";string "to_bool";exp c]
+             separate space [string "if";group (align (string "to_bool" ^//^ group (exp c)))]
           | _ -> separate space [string "if";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
-       if aexp_needed then parens epp else epp
+       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
@@ -2024,7 +2037,7 @@ let doc_exp_lem, doc_let_lem =
                  | [v] -> v
                  | _ -> parens (separate comma vars) in
                (prefix 2 1)
-                 (parens ((separate space) [string loopf;exp indices;exp e5]))
+                 (parens ((separate space) [string loopf;group (exp indices);exp e5]))
                  (parens
                     ((prefix 1 1)
                        (separate space [string "fun";exp id;varspp;arrow])
@@ -2033,7 +2046,7 @@ let doc_exp_lem, doc_let_lem =
                  )
             | E_aux (E_lit (L_aux (L_unit,_)),_) ->
                (prefix 2 1)
-                 (parens ((separate space) [string loopf;exp indices;exp e5]))
+                 (parens ((separate space) [string loopf;group (exp indices);exp e5]))
                  (parens
                     ((prefix 1 1)
                        (separate space [string "fun";exp id;string "_";arrow])
@@ -2045,11 +2058,11 @@ let doc_exp_lem, doc_let_lem =
            (match annot with
             | Base (_,Constructor _,_,_,_,_) ->
                let epp = separate space [doc_id_lem f;separate_map space (top_exp true) args] in
-               if aexp_needed then parens epp else epp
+               if aexp_needed then parens (align epp) else epp
             | Base (_,External (Some "bitwise_not_bit"),_,_,_,_) ->
                let [a] = args in
                let epp = align (string "~" ^^ exp a) in
-               if aexp_needed then parens epp else epp
+               if aexp_needed then parens (align epp) else epp
             | _ -> 
                let call = match annot with
                  | Base(_,External (Some n),_,_,_,_) ->
@@ -2066,15 +2079,15 @@ let doc_exp_lem, doc_let_lem =
                       )
                    )
                in
-               if aexp_needed then parens epp else epp
+               if aexp_needed then parens (align epp) else epp
            )
        )
     | E_vector_access(v,e) ->
        let epp = separate space [string "access";exp v;exp e] in
-       if aexp_needed then parens epp else epp
+       if aexp_needed then parens (align epp) else epp
     | E_vector_subrange(v,e1,e2) ->
-       let epp = (string "slice") ^^ space ^^ (exp v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2) in
-       if aexp_needed then parens epp else epp
+       let epp = align (string "slice" ^^ space ^^ exp v ^//^ exp e1 ^//^ exp e2) in
+       if aexp_needed then parens (align epp) else epp
     | E_field((E_aux(_,(_,fannot)) as fexp),id) ->
        let (Base ((_,{t = t}),_,_,_,_,_)) = fannot in
       (match t with
@@ -2086,7 +2099,7 @@ let doc_exp_lem, doc_let_lem =
             | _ -> string "read_reg_field" in
           let epp = field_f ^^ space ^^ (exp fexp) ^^ space ^^
                       string (regtyp ^ "_") ^^ doc_id_lem id in
-         if aexp_needed then parens epp else epp
+         if aexp_needed then parens (align epp) else epp
       | _ -> exp fexp ^^ dot ^^ doc_id_lem id)
     | E_block [] -> string "()"
     | E_block exps -> failwith "Blocks should have been removed till now."
@@ -2113,10 +2126,10 @@ let doc_exp_lem, doc_let_lem =
                 separate space [string "access";string reg;doc_int start]
               else
                 separate space [string "slice"; string reg; doc_int start; doc_int stop] in
-            if aexp_needed then parens epp else epp
+            if aexp_needed then parens (align epp) else epp
          | Alias_pair(reg1,reg2) ->
             let epp = separate space [string "vector_concat";string reg1;string reg2] in
-            if aexp_needed then parens epp else epp
+            if aexp_needed then parens (align epp) else epp
          | Alias_extract(reg,start,stop) ->
             let epp = 
               if start = stop then
@@ -2127,12 +2140,12 @@ let doc_exp_lem, doc_let_lem =
                 (separate space)
                   [string "slice"; doc_int start; doc_int stop;
                    parens (string "read_reg" ^^ space ^^ string reg)] in
-            if aexp_needed then parens epp else epp
+            if aexp_needed then parens (align epp) else epp
          | Alias_pair(reg1,reg2) ->
             let epp = separate space [string "vector_concat";
                             parens (string "read_reg" ^^ space ^^ string reg1);
                             parens (string "read_reg" ^^ space ^^ string reg2)] in
-            if aexp_needed then parens epp else epp
+            if aexp_needed then parens (align epp) else epp
          )
       | _ -> doc_id_lem id)
     | E_lit lit -> doc_lit_lem false lit
@@ -2170,10 +2183,11 @@ let doc_exp_lem, doc_let_lem =
                     (fun (pp,count) e ->
                      (pp ^^ semi ^^ (if count = 20 then break 0 else empty) ^^ top_exp false e),
                      if count = 20 then 0 else count + 1)
-                    (top_exp false e,0) exps in
+                    (top_exp false e,0) es in
                 align (group expspp) in
-           let epp = group (separate space [string "V"; brackets expspp;string start;string dir_out]) in
-           if aexp_needed then parens epp else epp
+           let epp =
+             group (separate space [string "V"; brackets expspp;string start;string dir_out]) in
+           if aexp_needed then parens (align epp) else epp
       )
     | E_vector_indexed (iexps, (Def_val_aux (default,(dl,dannot)))) ->
       (match annot with
@@ -2195,37 +2209,48 @@ let doc_exp_lem, doc_let_lem =
               | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i))
             in
             let default_string = 
-              (match default with
-               | Def_val_empty -> string "Nothing" 
-               | Def_val_dec e ->
-                  if is_bit_vector t then
-                    parens (string "Just " ^^ (exp e))
-                  else
-                    let (Base ((_,{t = t}),_,_,_,_,_)) = dannot in
-                    let n =
-                      match t with
-                        Tapp ("register",
-                              [TA_typ ({t = Tapp ("vector",
-                                                  TA_nexp {nexp = Nconst i} ::
-                                                    TA_nexp {nexp = Nconst j} ::_)})]) ->
-                        abs_big_int (sub_big_int i j)
-                      | _ ->
-                         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 (separate_map comma (fun x -> x) [(doc_int i); top_exp false e]) in
+              match default with
+              | Def_val_empty -> string "Nothing" 
+              | Def_val_dec e ->
+                 if is_bit_vector t then
+                   parens (string "Just " ^^ (exp e))
+                 else
+                   let (Base ((_,{t = t}),_,_,_,_,_)) = dannot in
+                   let n =
+                     match t with
+                       Tapp ("register",
+                             [TA_typ ({t = Tapp ("vector",
+                                                 TA_nexp {nexp = Nconst i} ::
+                                                   TA_nexp {nexp = Nconst j} ::_)})]) ->
+                       abs_big_int (sub_big_int i j)
+                     | _ ->
+                        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 expspp =
+              match iexps with
+              | [] -> empty
+              | e :: es ->
+                 let (expspp,_) =
+                   List.fold_left
+                     (fun (pp,count) e ->
+                      (pp ^^ semi ^^ (if count = 5 then break 1 else empty) ^^ iexp e),
+                      if count = 5 then 0 else count + 1)
+                     (iexp e,0) es in
+                 align (expspp) in
             let epp =
-              (separate space)
-                [call;(brackets (separate_map semi iexp iexps));
-                 default_string;
-                 string start;
-                 string size] in
-            if aexp_needed then parens epp else epp)
+              align (group (call ^//^ brackets expspp ^/^
+                              separate space [default_string;string start;string size])) in
+            if aexp_needed then parens (align epp) else epp)
   | E_vector_update(v,e1,e2) ->
      let epp = separate space [string "update_pos";exp v;exp e1;exp e2] in
-     if aexp_needed then parens epp else epp
+     if aexp_needed then parens (align epp) else epp
   | E_vector_update_subrange(v,e1,e2,e3) ->
-     let epp = separate space [string "update";exp v;exp e1;exp e2;exp e3] in
-     if aexp_needed then parens epp else epp
+     let epp = align (string "update" ^//^
+                        group (group (exp v) ^/^ group (exp e1) ^/^ group (exp e2)) ^/^
+                          group (exp e3)) in
+     if aexp_needed then parens (align epp) else epp
   | E_list exps ->
       brackets (separate_map semi (top_exp false) exps)
   | E_case(e,pexps) ->
@@ -2234,15 +2259,15 @@ let doc_exp_lem, doc_let_lem =
          (separate space [string "match"; exp e; string "with"])
          (separate_map (break 1) doc_case pexps) ^^ (break 1) ^^
          (string "end" ^^ (break 1)) in
-     if aexp_needed then parens epp else epp
+     if aexp_needed then parens (align epp) else epp
   | E_exit e ->
     separate space [string "exit"; exp e;]
   | E_app_infix (e1,id,e2) ->
      (match annot with
       | Base((_,t),External(Some name),_,_,_,_) ->
          let epp =
-           let aux name = exp e1 ^//^ string name ^//^ exp e2 in
-           let aux2 name = string name ^//^ exp e1 ^//^ exp e2 in
+           let aux name = align (exp e1 ^^ space ^^ string name ^//^ exp e2) in
+           let aux2 name = align (string name ^//^ exp e1 ^/^ exp e2) in
            align
              (match name with
               | "bitwise_and_bit" -> aux "&."
@@ -2289,12 +2314,12 @@ let doc_exp_lem, doc_let_lem =
               | "minus_overflow_vec_bit_signed" -> aux2 "minusSO_VBV"
 
               | _ ->
-                 string name ^//^ parens (top_exp false e1 ^^ comma ^//^ top_exp false e2)) in
-         if aexp_needed then parens epp else epp
+                 string name ^//^ parens (top_exp false e1 ^^ comma ^/^ top_exp 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
-         if aexp_needed then parens epp else epp)
+           align (doc_id_lem id ^//^ parens (top_exp false e1 ^^ comma ^/^ top_exp 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"
 (*     (separate
@@ -2315,7 +2340,7 @@ let doc_exp_lem, doc_let_lem =
        | _ ->
           (separate space [top_exp b e1; string ">>= fun"; doc_pat_lem true pat;arrow]) ^/^
             top_exp false e2 in
-     if aexp_needed then parens epp else epp
+     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
@@ -2483,8 +2508,94 @@ let reg_decls (Defs defs) =
       (prefix 2 1)
         (separate space [string "type";string "register";equals])
         ((separate_map space (fun (reg,_) -> pipe ^^ space ^^ string reg) regs)
-         ^^ space ^^ pipe ^^ space ^^ string "UndefinedReg of integer" ^^
+         ^^ space ^^
+           pipe ^^ space ^^ string "UndefinedReg of integer" ^^
            pipe ^^ space ^^ string "RegisterPair of register * register") in
+
+  let reglength_pp =
+    if regs = [] then
+      string "length_reg _ = (0 : integer)"
+    else
+    (separate space [string "val";string "length_reg";colon;string "register";arrow;string "integer"])
+    ^/^
+    (prefix 2 1)
+      (separate space [string "let rec";string "length_reg";string "reg";equals;string "match reg with"])
+      (((separate_map (break 1))
+           (fun (name,typ) ->
+            let ((n1,n2,_,_),typname) =
+              match typ with
+              | Some typname -> (List.assoc typname regtypes,"register_" ^ typname)
+              | None -> (default,"register") in
+            separate space [pipe;string name;arrow;doc_nexp (if is_inc then n2 else n1);
+                            minus;doc_nexp (if is_inc then n1 else n2);plus;string "1"])
+           regs) ^/^
+         separate space [pipe;string "UndefinedReg _";arrow;
+                        string "failwith \"Trying to compute length of undefined register\""] ^/^
+         separate space [pipe;string "RegisterPair r1 r2";arrow;
+                         string "length_reg r1 + length_reg r2"] ^/^
+      string "end") in
+
+  let regstartindex_pp =
+    if regs = [] then
+      string "start_index_reg _ = (0 : integer)"
+    else
+    (separate space [string "val";string "start_index_reg";colon;string "register";arrow;string "integer"])
+    ^/^
+    (prefix 2 1)
+      (separate space [string "let rec";string "start_index_reg";string "reg";equals;string "match reg with"])
+      (((separate_map (break 1))
+           (fun (name,typ) ->
+            let ((n1,_,_,_),typname) =
+              match typ with
+              | Some typname -> (List.assoc typname regtypes,"register_" ^ typname)
+              | None -> (default,"register") in
+            separate space [pipe;string name;arrow;doc_nexp n1])
+           regs) ^/^
+         separate space [pipe;string "UndefinedReg _";arrow;
+                        string "failwith \"Trying to compute start index of undefined register\""] ^/^
+         separate space [pipe;string "RegisterPair r1 _";arrow;
+                         string "start_index_reg r1"] ^/^
+      string "end") in
+
+  let regtostring_pp =
+    if regs = [] then empty
+    else
+      (prefix 2 1)
+        (separate space [string "let";string "register_to_string";equals;string "function"])
+        (((separate_map (break 1))
+           (fun (reg,_) -> separate space [pipe;string reg;arrow;string ("\""^reg^"\"")])
+           regs) ^/^
+           separate space [pipe;string "UndefinedReg _";arrow;
+                           string "failwith";
+                           string_lit
+                             (string "register_to_string called for undefined register")] ^/^
+             separate space [pipe;string "RegisterPair _ _";arrow;
+                             string "failwith";
+                             string_lit (string "register_to_string called for register pair")] ^/^
+         string "end") in
+
+  let regfieldtostring_pp =
+    if rsranges = [] then empty
+    else
+      (prefix 2 1)
+        (separate space [string "let";string "register_field_to_string";equals;string "function"])
+        ((separate_map (break 1))
+           (fun (fname,tname,_,_) ->
+            separate space [pipe;string (tname ^ "_" ^ fname);arrow;
+                            string_lit (string (tname ^ "_" ^ fname))])
+           rsranges ^/^ string "end") in
+  
+  let regbittostring_pp =
+    if rsbits = [] then empty
+    else
+      (prefix 2 1)
+        (separate space [string "let";string "register_field_bit_to_string";
+                         equals;string "function"])
+        ((separate_map (break 1))
+           (fun (fname,tname,_) ->
+            separate space [pipe;string (tname ^ "_" ^ fname);arrow;
+                            string_lit (string (tname ^ "_" ^ fname))])
+           rsbits ^/^ string "end") in
   
   let regfields_pp =
     if rsranges = [] then
@@ -2511,42 +2622,18 @@ let reg_decls (Defs defs) =
        separate space [string "let";string name1;equals;string "RegisterPair";string name2;string name3])
       regaliases in
 
-  let state_pp =
+  let regstate_pp =
     if regs = [] then
-      string "type state = EMPTY_STATE"
+      string "type regstate = EMPTY_STATE"
     else
     (prefix 2 1)
-      (separate space [string "type";string "state";equals])
+      (separate space [string "type";string "regstate";equals])
       (anglebars
          ((separate_map (semi ^^ break 1))
             (fun (reg,_) -> separate space [string (String.lowercase reg);colon;string "vector bit"])
             regs
          )) in
 
-  let length_pp =
-    if regs = [] then
-      string "length_reg _ = (0 : integer)"
-    else
-    (separate space [string "val";string "length_reg";colon;string "register";arrow;string "integer"])
-    ^/^
-    (prefix 2 1)
-      (separate space [string "let rec";string "length_reg";string "reg";equals;string "match reg with"])
-      (((separate_map (break 1))
-           (fun (name,typ) ->
-            let ((n1,n2,_,_),typname) =
-              match typ with
-              | Some typname -> (List.assoc typname regtypes,"register_" ^ typname)
-              | None -> (default,"register") in
-            separate space [pipe;string name;arrow;doc_nexp (if is_inc then n2 else n1);
-                            minus;doc_nexp (if is_inc then n1 else n2);plus;string "1"])
-           regs) ^/^
-         separate space [pipe;string "UndefinedReg n";arrow;
-                        string "failwith \"Trying to compute length of undefined register\""] ^/^
-         separate space [pipe;string "RegisterPair r1 r2";arrow;
-                         string "length_reg r1 + length_reg r2"] ^/^
-      string "end") in
-
-
   let field_indices_pp =
     if rsranges = [] then
       string "let field_indices _ = ((0 : integer),(0 : integer))"
@@ -2558,7 +2645,7 @@ let reg_decls (Defs defs) =
       (
         ((separate_map (break 1))
            (fun (fname,tname,i,j) ->
-            separate space[pipe;string ((String.capitalize tname) ^ "_" ^ fname);arrow;
+            separate space[pipe;string (tname ^ "_" ^ fname);arrow;
                            parens (separate comma [string (string_of_int i);
                                                    string (string_of_int j)])]
            ) rsranges
@@ -2576,7 +2663,7 @@ let reg_decls (Defs defs) =
       (
         ((separate_map (break 1))
            (fun (fname,tname,i) ->
-            separate space[pipe;string ((String.capitalize tname) ^ "_" ^ fname);
+            separate space[pipe;string (tname ^ "_" ^ fname);
                            arrow;string (string_of_int i)]
            ) rsbits
         ) ^/^ string "end" ^^ hardline
@@ -2585,27 +2672,27 @@ let reg_decls (Defs defs) =
       
   let read_regstate_pp =
     if regs = [] then
-      string "let read_regstate _ _ -> Vector 0 0 true"
+      string "let read_regstate_aux _ _ -> Vector 0 0 true"
     else
     (prefix 2 1)
-      (separate space [string "let rec";string "read_regstate";string "s";equals;string "function"])
+      (separate space [string "let rec";string "read_regstate_aux";string "s";equals;string "function"])
       (
         ((separate_map (break 1))
            (fun (name,_) ->
             separate space [pipe;string name;arrow;string "s." ^^ (string (String.lowercase name))])
            regs) ^/^
-          separate space [pipe;string "UndefinedReg n";arrow;
+          separate space [pipe;string "UndefinedReg _";arrow;
                           string "failwith \"Trying to read from undefined register\""] ^/^
           separate space [pipe;string "RegisterPair r1 r2";arrow;
-                          string "read_regstate s r1 ^^ read_regstate s r2"] ^/^
+                          string "read_regstate_aux s r1 ^^ read_regstate_aux s r2"] ^/^
           string "end" ^^ hardline ) in
 
   let write_regstate_pp =
     if regs = [] then
-      string "let write_regstate _ _ _ -> EMPTY_STATE"
+      string "let write_regstate_aux _ _ _ -> EMPTY_STATE"
     else
     (prefix 2 1)
-      (separate space [string "let rec";string "write_regstate";string "s";string "reg";string "v";
+      (separate space [string "let rec";string "write_regstate_aux";string "s";string "reg";string "v";
                        equals;string "match reg with"])
       (
         ((separate_map (break 1))
@@ -2618,7 +2705,7 @@ let reg_decls (Defs defs) =
                     [string "s";string"with";string (String.lowercase name);equals;string "v"]
                  )]
            ) regs) ^/^
-          separate space [pipe;string "UndefinedReg n";arrow;
+          separate space [pipe;string "UndefinedReg _";arrow;
                           string "failwith \"Trying to write to undefined register\""]  ^/^
           ((prefix 3 1)
              (separate space [pipe;string "RegisterPair r1 r2";arrow])
@@ -2633,13 +2720,16 @@ let reg_decls (Defs defs) =
                   string ("let r2_v = slice v " ^
                          (if is_inc then "(size - start)" else "(start - size)") ^
                            (if is_inc then "(vsize - start) in" else ("start - vsize) in")));
-                  string "write_regstate (write_regstate s r1 r1_v) r2 r2_v"
+                  string "write_regstate_aux (write_regstate_aux s r1 r1_v) r2 r2_v"
                 ])) ^/^
           string "end" ^^ hardline ) in
 
   (separate (hardline ^^ hardline)
-            [dir_pp;regs_pp;regfields_pp;regfieldsbit_pp;field_index_bit_pp;field_indices_pp;
-             regalias_pp;state_pp;length_pp;read_regstate_pp;write_regstate_pp],defs)
+            [dir_pp;regs_pp;regfields_pp;regfieldsbit_pp;
+             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)
     
 let doc_defs_lem (Defs defs) =
   let (decls,defs) = reg_decls (Defs defs) in