sail-to-lem progress

8 files changed, 195 insertions, 149 deletions

diff --git a/src/gen_lib/armv8_extras.lem b/src/gen_lib/armv8_extras.lem
index 54304225..fd0fc17b 100644
--- a/src/gen_lib/armv8_extras.lem
+++ b/src/gen_lib/armv8_extras.lem
@@ -1,26 +1,7 @@
 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
@@ -37,14 +18,14 @@ 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 wMem_Val_NORMAL (l,v) = read_writeEA () >>= fun (addr,_) -> write_memory addr l v >> return ()
+let wMem_Val_ATOMIC (l,v) = read_writeEA () >>= fun (addr,_) -> write_memory addr l v >> return Vector.O
 
-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 ()
+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/prompt.lem b/src/gen_lib/prompt.lem
index 6fa406b8..1382fd1d 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 'e 'a =
+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 *)
@@ -123,7 +123,7 @@ type outcome 'e 'a =
                                                 
   (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally 
    * provide a handler. *)
-  | Escape 'e (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)
+  | Escape of (outcome unit) (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)
 
   (* Stop for incremental stepping, function can be used to display function call data *)
   | Done of 'a
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index c78a6cdf..0f6aa5ee 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -1,17 +1,18 @@
 open import Pervasives_extra
-open import State
 open import Vector
 open import Arch
 
 type i = integer
 type number = integer
 
+type n = natural
+
 let length l = integerFromNat (length l)
 
-let has_undef (V bs _ _) = List.any (function Undef -> true | _ -> false end) bs
+let has_undef (Vector bs _ _) = List.any (function Undef -> true | _ -> false end) bs
 
 let most_significant = function
-  | (V (b :: _) _ _) -> b
+  | (Vector (b :: _) _ _) -> b
   | _ -> failwith "most_significant applied to empty vector"
   end
 
@@ -22,9 +23,11 @@ let bitwise_not_bit = function
   end
 
 let (~) = bitwise_not_bit
+let pow m n = m ** (natFromInteger n)
+
 
-let bitwise_not (V bs start is_inc) =
-  V (List.map bitwise_not_bit bs) start is_inc
+let bitwise_not (Vector bs start is_inc) =
+  Vector (List.map bitwise_not_bit bs) start is_inc
 
 val is_one : integer -> bit
 let is_one i =
@@ -56,15 +59,15 @@ let (|.) x y = bitwise_or_bit (x,y)
 val (+.) : bit -> bit -> bit
 let (+.) x y = bitwise_xor_bit (x,y)
 
-let bitwise_binop op (V bsl start is_inc, V bsr _ _) =
+let bitwise_binop op (Vector bsl start is_inc, Vector bsr _ _) =
   let revbs = foldl (fun acc pair -> bitwise_binop_bit op pair :: acc) [] (zip bsl bsr) in
-  V (reverse revbs) start is_inc
+  Vector (reverse revbs) start is_inc
 
 let bitwise_and = bitwise_binop (&&)
 let bitwise_or = bitwise_binop (||)
 let bitwise_xor = bitwise_binop xor
 
-let unsigned (V bs _ _ as v) : integer =
+let unsigned (Vector bs _ _ as v) : integer =
   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)
@@ -133,13 +136,13 @@ let to_vec is_inc ((len : integer),(n : integer)) =
   let bs = List.replicate (natFromInteger len) O in
   let start = if is_inc then 0 else len-1 in
   if n = 0 then
-    V bs start is_inc
+    Vector bs start is_inc
   else if n > 0 then
-    V (divide_by_2 bs (len-1) n) start is_inc
+    Vector (divide_by_2 bs (len-1) n) start is_inc
   else
     let abs_bs = divide_by_2 bs (len-1) (abs n) in
-    let (V bs start is_inc) = bitwise_not (V abs_bs start is_inc) in
-    V (add_one_bit bs false (len-1)) start is_inc
+    let (Vector bs start is_inc) = bitwise_not (Vector abs_bs start is_inc) in
+    Vector (add_one_bit bs false (len-1)) start is_inc
 
 let to_vec_big = to_vec
       
@@ -147,12 +150,12 @@ let to_vec_inc = to_vec true
 let to_vec_dec = to_vec false
 
 let to_vec_undef is_inc (len : integer) =
-  V (replicate (natFromInteger len) Undef) (if is_inc then 0 else len-1) is_inc
+  Vector (replicate (natFromInteger len) Undef) (if is_inc then 0 else len-1) is_inc
 
 let to_vec_inc_undef = to_vec_undef true
 let to_vec_dec_undef = to_vec_undef false
 
-let get_dir (V _ _ ord) = ord
+let get_dir (Vector _ _ ord) = ord
                                     
 let exts (len, vec) = to_vec (get_dir vec) (len,signed vec)
 let extz (len, vec) = to_vec (get_dir vec) (len,unsigned vec)
@@ -168,7 +171,7 @@ let modulo = integerMod
 let quot = integerDiv
 let power = integerPow
 
-let arith_op_vec op sign (size : integer) (V _ _ is_inc as l) r =
+let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r =
   let (l',r') = (to_num sign l, to_num sign r) in
   let n = op  l' r' in
   to_vec is_inc (size * (length l),n)
@@ -186,7 +189,7 @@ let minus_VVV = arith_op_vec integerMinus false 1
 let mult_VVV = arith_op_vec integerMult false 2
 let multS_VVV = arith_op_vec integerMult true 2
 
-let arith_op_vec_range op sign size (V _ _ is_inc as l) r =
+let arith_op_vec_range op sign size (Vector _ _ is_inc as l) r =
   arith_op_vec op sign size l (to_vec is_inc (length l,r))
 
 (* add_vec_range
@@ -201,7 +204,7 @@ let minus_VIV = arith_op_vec_range integerMinus false 1
 let mult_VIV = arith_op_vec_range integerMult false 2
 let multS_VIV = arith_op_vec_range integerMult true 2
 
-let arith_op_range_vec op sign size l (V _ _ is_inc as r) =
+let arith_op_range_vec op sign size l (Vector _ _ is_inc as r) =
   arith_op_vec op sign size (to_vec is_inc (length r, l)) r
 
 (* add_range_vec
@@ -248,7 +251,7 @@ let arith_op_vec_vec_range op sign l r =
 let add_VVI = arith_op_vec_vec_range integerAdd false
 let addS_VVI = arith_op_vec_vec_range integerAdd true
 
-let arith_op_vec_bit op sign (size : integer) (V _ _ is_inc as l)r =
+let arith_op_vec_bit op sign (size : integer) (Vector _ _ is_inc as l)r =
   let l' = to_num sign l in
   let n = op l' (match r with | I -> (1 : integer) | _ -> 0 end) in
   to_vec is_inc (length l * size,n)
@@ -261,7 +264,7 @@ let add_VBV = arith_op_vec_bit integerAdd false 1
 let addS_VBV = arith_op_vec_bit integerAdd true 1
 let minus_VBV = arith_op_vec_bit integerMinus true 1
 
-let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (V _ _ is_inc as l) r =
+let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (Vector _ _ is_inc as l) r =
   let len = length l in
   let act_size = len * size in
   let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
@@ -292,7 +295,7 @@ let multO_VVV = arith_op_overflow_vec integerMult false 2
 let multSO_VVV = arith_op_overflow_vec integerMult true 2
 
 let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer)
-                                  (V _ _ is_inc as l) r_bit =
+                                  (Vector _ _ is_inc as l) r_bit =
   let act_size = length l * size in
   let l' = to_num sign l in
   let l_u = to_num false l in
@@ -320,35 +323,35 @@ let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1
 let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1
 let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1
     
-type shift = LL | RR | LLL
+type shift = LL_shift | RR_shift | LLL_shift
 
-let shift_op_vec op ((V bs start is_inc as l),(n : integer)) =
+let shift_op_vec op ((Vector bs start is_inc as l),(n : integer)) =
   let len = integerFromNat (List.length bs) in
     match op with
-     | LL (*"<<"*) ->
-       let right_vec = V (List.replicate (natFromInteger n) O) 0 true in
+     | LL_shift (*"<<"*) ->
+       let right_vec = Vector (List.replicate (natFromInteger n) O) 0 true in
        let left_vec = slice l n (if is_inc then len + start else start - len) in
        vector_concat left_vec right_vec
-     | RR (*">>"*) ->
+     | RR_shift (*">>"*) ->
        let right_vec = slice l start n in
-       let left_vec = V (List.replicate (natFromInteger n) O) 0 true in
+       let left_vec = Vector (List.replicate (natFromInteger n) O) 0 true in
        vector_concat left_vec right_vec 
-     | LLL (*"<<<"*) ->
+     | LLL_shift (*"<<<"*) ->
        let left_vec = slice l n (if is_inc then len + start else start - len) in
        let right_vec = slice l start n in
        vector_concat left_vec right_vec
      end
 
-let bitwise_leftshift = shift_op_vec LL (*"<<"*)
-let bitwise_rightshift = shift_op_vec RR (*">>"*)
-let bitwise_rotate = shift_op_vec LLL (*"<<<"*)
+let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*)
+let bitwise_rightshift = shift_op_vec RR_shift (*">>"*)
+let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*)
 
 let rec arith_op_no0 (op : integer -> integer -> integer) l r = 
   if r = 0
   then Nothing
   else Just (op l r)
 
-let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((V _ start is_inc) as l) r =
+let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector _ start is_inc) as l) r =
   let act_size = length l * size in
   let (l',r') = (to_num sign l,to_num sign r) in
   let n = arith_op_no0 op l' r' in
@@ -361,13 +364,13 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((V _ st
     end in
   if representable 
   then to_vec is_inc (act_size,n')
-  else V (List.replicate (natFromInteger act_size) Undef) start is_inc
+  else Vector (List.replicate (natFromInteger act_size) Undef) start is_inc
 
 let mod_VVV = arith_op_vec_no0 integerMod false 1
 let quot_VVV = arith_op_vec_no0 integerDiv false 1
 let quotS_VVV = arith_op_vec_no0 integerDiv true 1
 
-let arith_op_overflow_no0_vec op sign size ((V _ start is_inc) as l) r =
+let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
   let rep_size = length r * size in
   let act_size = length l * size in
   let (l',r') = (to_num sign l,to_num sign r) in
@@ -385,21 +388,31 @@ let arith_op_overflow_no0_vec op sign size ((V _ start is_inc) as l) r =
     if representable then
       (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
     else
-      (V (List.replicate (natFromInteger act_size) Undef) start is_inc,
-       V (List.replicate (natFromInteger (act_size + 1)) Undef) start is_inc) in
+      (Vector (List.replicate (natFromInteger act_size) Undef) start is_inc,
+       Vector (List.replicate (natFromInteger (act_size + 1)) Undef) start is_inc) in
   let overflow = if representable then O else I in
   (correct_size_num,overflow,most_significant one_more)
 
 let quotO_VVV = arith_op_overflow_no0_vec integerDiv false 1
 let quotSO_VVV = arith_op_overflow_no0_vec integerDiv true 1
 
-let arith_op_vec_range_no0 op sign size (V _ _ is_inc as l) r =
+let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r =
   arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r))
 
 let mod_VIV = arith_op_vec_range_no0 integerMod false 1
 
 let duplicate (bit,length) =
-  V (List.replicate (natFromInteger length) bit) 0 true
+  Vector (List.replicate (natFromInteger length) bit) 0 true
+
+val repeat : forall 'a. list 'a -> integer -> list 'a
+let rec repeat xs = function
+  | 0 -> []
+  | n -> xs ++ repeat xs (n-1)
+  end
+
+let duplicate_bits (Vector bits start direction,len) = 
+  let bits' = repeat bits len in
+  Vector bits' start direction
 
 let compare_op op (l,r) = bool_to_bit (op l r)
 
@@ -463,7 +476,7 @@ val make_indexed_vector_reg : list (integer * register) -> maybe register -> int
 let make_indexed_vector_reg entries default start length =
   let length = natFromInteger length in
   match default with
-  | Just v -> V (List.foldl replace (replicate length v) entries) start defaultDir
+  | Just v -> Vector (List.foldl replace (replicate length v) entries) start defaultDir
   | Nothing -> failwith "make_indexed_vector used without default value"
   end
 
@@ -471,15 +484,15 @@ val make_indexed_vector_bit : list (integer * bit) -> maybe bit -> integer -> in
 let make_indexed_vector_bit entries default start length =
   let length = natFromInteger length in
   let default = match default with Nothing -> Undef | Just v -> v end in
-  V (List.foldl replace (replicate length default) entries) start defaultDir
+  Vector (List.foldl replace (replicate length default) entries) start defaultDir
 
 val make_bit_vector_undef : integer -> vector bit
 let make_bitvector_undef length =
-  V (replicate (natFromInteger length) Undef) 0 true
+  Vector (replicate (natFromInteger length) Undef) 0 true
 
 
 let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n)
 
-let mask (n,V bits start dir) =
+let mask (n,Vector bits start dir) =
   let current_size = List.length bits in
-  V (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir
+  Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 610bcc7d..6db45002 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -38,6 +38,13 @@ let (>>=) = bind
 val (>>): forall 's 'e 'b. State 's 'e unit -> State 's 'e 'b -> State 's 'e 'b
 let (>>) m n = m >>= fun _ -> n
 
+let assert' b msg_opt =
+  let msg = match msg_opt with
+  | Just msg -> msg
+  | Nothing  -> "unspecified error"
+  end in
+  if to_bool b then failwith msg else ()
+
 val read_writeEA : forall 'e. unit -> State state 'e (integer * integer)
 let read_writeEA () s = (Left s.writeEA,s)
 
@@ -68,10 +75,10 @@ let write_memstate s (addr,bits) = Map.insert addr bits s
 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)
+  (Left (Vector (foldl (++) [] bytes) 0 defaultDir),s)
 
 val write_memory : forall 'e. integer -> integer -> vector bit -> State state 'e unit
-let write_memory addr l (V bits _ _) s =
+let write_memory addr l (Vector 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) |>)
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index 4044e23c..72c8b584 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -1,7 +1,7 @@
 open import Pervasives_extra
 
 type bit = O | I | Undef
-type vector 'a = V of list 'a * integer * bool
+type vector 'a = Vector of list 'a * integer * bool
 
 let rec nth xs (n : integer) =
   match xs with
@@ -15,8 +15,8 @@ let to_bool = function
   | Undef -> failwith "to_bool applied to Undef"
   end
 
-let get_start (V _ s _) = s
-let length (V bs _ _) = length bs
+let get_start (Vector _ s _) = s
+let length (Vector bs _ _) = length bs
 
 let rec replace bs ((n : integer),b') = match bs with
   | [] -> []
@@ -27,13 +27,13 @@ let rec replace bs ((n : integer),b') = match bs with
        b :: replace bs (n - 1,b')
   end
 
-let vector_concat (V bs start is_inc) (V bs' _ _) =
-  V (bs ++ bs') start is_inc
+let vector_concat (Vector bs start is_inc) (Vector bs' _ _) =
+  Vector (bs ++ bs') start is_inc
 
 let (^^) = vector_concat
 
 val slice : vector bit -> integer -> integer -> vector bit
-let slice (V bs start is_inc) n m =
+let slice (Vector bs start is_inc) n m =
   let n = natFromInteger n in
   let m = natFromInteger m in
   let start = natFromInteger start in
@@ -41,9 +41,9 @@ let slice (V bs start is_inc) n m =
   let (_,suffix) = List.splitAt offset bs in
   let (subvector,_) = List.splitAt length suffix in
   let n = integerFromNat n in
-  V subvector n is_inc
+  Vector subvector n is_inc
 
-let update (V bs start is_inc) n m (V bs' _ _) =
+let update (Vector bs start is_inc) n m (Vector bs' _ _) =
   let n = natFromInteger n in
   let m = natFromInteger m in
   let start = natFromInteger start in
@@ -51,12 +51,12 @@ let update (V bs start is_inc) n m (V bs' _ _) =
   let (prefix,_) = List.splitAt offset bs in
   let (_,suffix) = List.splitAt (offset + length) bs in
   let start = integerFromNat start in
-  V (prefix ++ (List.take length bs') ++ suffix) start is_inc
+  Vector (prefix ++ (List.take length bs') ++ suffix) start is_inc
 
 val access : forall 'a. vector 'a -> (*nat*) integer -> 'a
-let access (V bs start is_inc) n =
+let access (Vector bs start is_inc) n =
   if is_inc then nth bs (n - start) else nth bs (start - n)
 
 val update_pos : forall 'a. vector 'a -> (*nat*) integer -> 'a -> vector 'a
 let update_pos v n b =
-  update v n n (V [b] 0 true)
+  update v n n (Vector [b] 0 true)
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index a2859d6e..4503555a 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2071,6 +2071,7 @@ let doc_id_lem_type (Id_aux(i,_)) =
   | Id("bit") -> string "bit"
   | Id("int") -> string "integer"
   | Id("nat") -> string "integer"
+  | Id("option") -> string "maybe"
   | Id i -> string (fix_id i)
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
@@ -2090,13 +2091,31 @@ let doc_id_lem_ctor (Id_aux(i,_)) =
       * token in case of x ending with star. *)
      separate space [colon; string (String.capitalize x); empty]
 
+let effectful (Effect_aux (eff,_)) =
+  match eff with
+  | Effect_var _ -> failwith "effectful: Effect_var not supported"
+  | Effect_set effs ->
+     List.exists
+       (fun (BE_aux (eff,_)) ->
+         match eff with
+         | BE_rreg | BE_wreg | BE_rmem | BE_wmem | BE_eamem | BE_wmv
+         | BE_barr | BE_depend | BE_undef | BE_nondet | BE_escape -> true
+         | _ -> false)
+       effs
+
 let doc_typ_lem, doc_atomic_typ_lem =
   (* following the structure of parser for precedence *)
   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
+         let exc_typ = string "string" in
+         let ret_typ =
+           if effectful efct
+           then separate space [string "M";parens exc_typ;fn_typ true regtypes ret]
+           else separate space [fn_typ false regtypes ret] in
+         let tpp = separate space [tup_typ true regtypes arg; arrow;ret_typ] in
+         (* once we have proper excetions we need to know what the exceptions type is *)
          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
@@ -2115,15 +2134,15 @@ let doc_typ_lem, doc_atomic_typ_lem =
       | 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)
+         let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem regtypes) args) in
+         if atyp_needed then parens tpp else tpp
       | _ -> 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
+         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 _ ->
@@ -2150,7 +2169,7 @@ let doc_lit_lem in_pat (L_aux(lit,l)) a =
   | L_true  -> "I"
   | L_num i ->
      let ipp = string_of_int i in
-     (if i < 0 then "((0"^ipp^") : i)"
+     (if i < 0 then "((0"^ipp^") )"
       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*)*)
@@ -2194,12 +2213,12 @@ let rec doc_pat_lem apat_needed regtypes (P_aux (p,(l,annot)) as pa) = match p w
   | P_vector pats ->
      let ppp =
        (separate space)
-         [string "V";brackets (separate_map semi (doc_pat_lem true regtypes) pats);underscore;underscore] in
+         [string "Vector";brackets (separate_map semi (doc_pat_lem true regtypes) pats);underscore;underscore] in
      if apat_needed then parens ppp else ppp
   | P_vector_concat pats ->
      let ppp =
        (separate space)
-         [string "V";parens (separate_map (string "::") (doc_pat_lem true regtypes) pats);underscore;underscore] in
+         [string "Vector";parens (separate_map (string "::") (doc_pat_lem true regtypes) pats);underscore;underscore] in
      if apat_needed then parens ppp else ppp
   | P_tup pats  ->
      (match pats with
@@ -2220,8 +2239,11 @@ let rec getregtyp (LEXP_aux (le,(l,Base ((_,{t=t}),_,_,_,_,_)))) =
          | LEXP_field (le,_) ->
             getregtyp le
 
+let prefix_recordtype = true
+let report = Reporting_basic.err_unreachable
+
 let doc_exp_lem, doc_let_lem =
-  let rec top_exp (regs,(regtypes : string list)) (aexp_needed : bool) (E_aux (e, (_,annot))) =
+  let rec top_exp (regs,(regtypes : string list)) (aexp_needed : bool) (E_aux (e, (l,annot))) =
     let exp = top_exp (regs,regtypes) true in
     match e with
     | E_assign((LEXP_aux(le_act,tannot) as le),e) ->
@@ -2232,7 +2254,7 @@ let doc_exp_lem, doc_let_lem =
            (match le with
             | LEXP_aux (LEXP_field (le,id), (_,((Base ((_,{t = t}),_,_,_,_,_))))) ->
                if t = Tid "bit" then
-                 failwith "indexing a register's (single bit) bitfield not supported"
+                  raise (report l "indexing a register's (single bit) bitfield not supported")
                else
                  let typprefix = getregtyp le ^ "_" in
                  (prefix 2 1)
@@ -2248,7 +2270,7 @@ let doc_exp_lem, doc_let_lem =
            (match le with
             | LEXP_aux (LEXP_field (le,id), (_,((Base ((_,{t = t}),_,_,_,_,_))))) ->
                if t = Tid "bit" then
-                 failwith "indexing a register's (single bit) bitfield not supported"
+                 raise (report l "indexing a register's (single bit) bitfield not supported")
                else
                  let typprefix = getregtyp le ^ "_" in
                  (prefix 2 1)
@@ -2278,10 +2300,10 @@ let doc_exp_lem, doc_let_lem =
                  let f = match t with
                    | (Tid "bit" | Tabbrev (_,{t=Tid "bit"})) ->
                       string "write_reg_bitfield"
-                   | _ -> string "write_reg_bitfield" in
+                   | _ -> string "write_reg_field" in
                  let typ = match List.assoc reg regs with
                    | Some typ -> typ
-                   | None -> failwith "Register type information missing" in
+                   | None -> raise (report l "Register type information missing") in
                  (prefix 2 1)
                    f
                    (separate space [string reg;string (typ ^ "_" ^ field);exp e])
@@ -2306,7 +2328,7 @@ let doc_exp_lem, doc_let_lem =
              (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"
+       raise (report l "E_for should have been removed till now")
     | E_let(leb,e) ->
        let epp = let_exp (regs,regtypes) leb ^^ space ^^ string "in" ^/^
                    top_exp (regs,regtypes) false e in
@@ -2398,22 +2420,30 @@ let doc_exp_lem, doc_let_lem =
          else
            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) ->
+    | E_field((E_aux(_,(l,fannot)) as fexp),id) ->
        let (Base ((_,{t = t}),_,_,_,_,_)) = fannot in
        (match t with
         | Tabbrev({t = Tid regtyp},{t=Tapp("register",_)}) ->
            let field_f = match annot with
              | Base((_,{t = Tid "bit"}),_,_,_,_,_)
-               | Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) ->
+             | Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) ->
                 string "read_reg_bitfield"
              | _ -> 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 (align epp) else epp
-        | _ -> exp fexp ^^ dot ^^ doc_id_lem id)
+        | Tid recordtyp
+        | Tabbrev ({t = Tid recordtyp},_) ->
+           let fname =
+             if prefix_recordtype
+             then (string (recordtyp ^ "_")) ^^ doc_id_lem id
+             else doc_id_lem id in
+           exp fexp ^^ dot ^^ fname
+        | _ ->  
+           raise (report l "E_field expression with no register or record type"))
     | E_block [] -> string "()"
-    | E_block exps -> failwith "Blocks should have been removed till now."
-    | E_nondet exps -> failwith "Nondet blocks not supported."
+    | E_block exps -> raise (report l "Blocks should have been removed till now.")
+    | E_nondet exps -> raise (report l "Nondet blocks not supported.")
     | E_id id ->
        (match annot with
         | Base((_, ({t = Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})),
@@ -2428,7 +2458,7 @@ let doc_exp_lem, doc_let_lem =
             | Alias_field(reg,field) ->
                let typ = match List.assoc reg regs with
                  | Some typ -> typ
-                 | None -> failwith "Register type information missing" in
+                 | None -> raise (report l "Register type information missing") in
                let epp = match t.t with
                  | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> 
                     (separate space)
@@ -2469,10 +2499,20 @@ let doc_exp_lem, doc_let_lem =
         | [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,_),_)) ->
-       let epp = anglebars (separate_map semi_sp (doc_fexp (regs,regtypes)) fexps) in
+       let (Base ((_,{t = t}),_,_,_,_,_)) = annot in
+       let recordtyp = match t with
+         | Tid recordtyp
+         | Tabbrev ({t = Tid recordtyp},_) -> recordtyp
+         | _ ->  raise (report l "cannot get record type") in       
+       let epp = anglebars (separate_map semi_sp (doc_fexp recordtyp (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 (regs,regtypes)) fexps))
+       let (Base ((_,{t = t}),_,_,_,_,_)) = annot in
+       let recordtyp = match t with
+         | Tid recordtyp
+         | Tabbrev ({t = Tid recordtyp},_) -> recordtyp
+         | _ ->  raise (report l "cannot get record type") in       
+       anglebars (doc_op (string "with") (exp e) (separate_map semi_sp (doc_fexp recordtyp (regs,regtypes)) fexps))
     | E_vector exps ->
       (match annot with
        | Base((_,t),_,_,_,_,_) ->
@@ -2499,7 +2539,7 @@ let doc_exp_lem, doc_let_lem =
                     (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
+             group (separate space [string "Vector"; 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)))) ->
@@ -2531,13 +2571,15 @@ let doc_exp_lem, doc_let_lem =
                    let (Base ((_,{t = t}),_,_,_,_,_)) = dannot in
                    let n =
                      match t with
-                       Tapp ("register",
+                     | 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
+                        raise (Reporting_basic.err_unreachable dl
+                                 ("not the right type information available to construct "^
+                                 "undefined register")) in
                    parens (string "Just " ^^ parens (string ("UndefinedReg " ^
                                                                string_of_big_int n))) in 
             let iexp (i,e) = parens (doc_int i ^^ comma ^^ top_exp (regs,regtypes) false e) in
@@ -2573,8 +2615,9 @@ let doc_exp_lem, doc_let_lem =
          (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 ->
-    separate space [string "exit"; exp e;]
+  | E_exit e -> separate space [string "exit"; exp e;]
+  | E_assert (e1,e2) ->
+     separate space [string "assert'"; exp e1; exp e2]
   | E_app_infix (e1,id,e2) ->
      (match annot with
       | Base((_,t),External(Some name),_,_,_,_) ->
@@ -2583,7 +2626,7 @@ let doc_exp_lem, doc_let_lem =
            let aux2 name = align (string name ^//^ exp e1 ^/^ exp e2) in
            align
              (match name with
-              | "power" -> aux "**"
+              | "power" -> aux2 "pow"
 
               | "bitwise_and_bit" -> aux "&."
               | "bitwise_or_bit" -> aux "|."
@@ -2651,7 +2694,7 @@ let doc_exp_lem, doc_let_lem =
                                                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"
+     raise (report l "E_internal_lets should have been removed till now")
 (*     (separate
         space
         [string "let internal";
@@ -2681,8 +2724,12 @@ let doc_exp_lem, doc_let_lem =
         (separate space [string "let"; doc_pat_lem true regtypes pat; equals])
         (top_exp (regs,regtypes) 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_fexp recordtyp (regs,regtypes) (FE_aux(FE_Fexp(id,e),_)) =
+    let fname =
+      if prefix_recordtype
+      then (string (recordtyp ^ "_")) ^^ doc_id_lem id
+      else doc_id_lem id in
+    doc_op equals fname (top_exp (regs,regtypes) true 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])
@@ -2717,8 +2764,11 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
      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 regtypes typ; semi] in
+     let f_pp (typ,fid) =
+       let fname = if prefix_recordtype
+                   then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
+                   else doc_id_lem_type fid in
+       concat [fname;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;])
@@ -2779,35 +2829,17 @@ 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 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_spec_lem regtypes (VS_aux (valspec,annot)) =
+  match valspec with
+  | VS_extern_no_rename _
+  | VS_extern_spec _ -> empty (* ignore these at the moment *)
+  | VS_val_spec (typschm,id) ->
+     separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem regtypes typschm] ^/^ hardline
+     
+                        
 let doc_def_lem (regs,regtypes) def = match def with
   | DEF_default df -> empty
-  | DEF_spec v_spec -> empty (*doc_spec_lem regtypes v_spec ^/^ hardline *)
+  | DEF_spec v_spec -> doc_spec_lem regtypes v_spec
   | 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
@@ -3107,7 +3139,6 @@ let reg_decls (Defs defs) =
     
 let doc_defs_lem (Defs 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)
 
 
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 27098912..60e26c5e 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1565,7 +1565,7 @@ and n_exp (E_aux (exp_aux,annot) as exp : 'a exp) (k : 'a exp -> 'a exp) : 'a ex
   | E_record_update (exp1,fexps) -> 
      n_exp_name exp1 (fun exp1 ->
      n_fexps fexps (fun fexps ->
-     k (rewrap (E_record fexps))))
+     k (rewrap (E_record_update (exp1,fexps)))))
   | E_field (exp1,id) ->
      n_exp_name exp1 (fun exp1 ->
      k (rewrap (E_field (exp1,id))))
@@ -1585,12 +1585,20 @@ and n_exp (E_aux (exp_aux,annot) as exp : 'a exp) (k : 'a exp -> 'a exp) : 'a ex
          if effectful exp'
          then (rewrap (E_internal_plet (pat,exp',n_exp body k)))
          else (rewrap (E_let (lb,n_exp body k)))
-     ))
+          ))
+  | E_sizeof nexp ->
+     k (rewrap (E_sizeof nexp))
+  | E_sizeof_internal annot ->
+     k (rewrap (E_sizeof_internal annot))
   | E_assign (lexp,exp1) ->
      n_lexp lexp (fun lexp ->
      n_exp_name exp1 (fun exp1 ->
      k (rewrap (E_assign (lexp,exp1)))))
   | E_exit exp' -> k (E_aux (E_exit (n_exp_term (effectful exp') exp'),annot))
+  | E_assert (exp1,exp2) ->
+     n_exp exp1 (fun exp1 ->
+     n_exp exp2 (fun exp2 ->
+     k (rewrap (E_assert (exp1,exp2)))))
   | E_internal_cast (annot',exp') ->
      n_exp_name exp' (fun exp' ->
      k (rewrap (E_internal_cast (annot',exp'))))
@@ -1604,6 +1612,11 @@ and n_exp (E_aux (exp_aux,annot) as exp : 'a exp) (k : 'a exp -> 'a exp) : 'a ex
   | E_internal_return exp1 ->
      n_exp_name exp1 (fun exp1 ->
      k (rewrap (E_internal_return exp1)))
+  | E_comment str ->
+    k (rewrap (E_comment str))
+  | E_comment_struc exp' ->
+     n_exp exp' (fun exp' ->
+     k (rewrap (E_comment_struc exp')))
   | E_internal_plet _ -> failwith "E_internal_plet should not be here yet"
                                   
 
diff --git a/src/rewriter.mli b/src/rewriter.mli
index a9ba973e..d1d642ff 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -111,3 +111,4 @@ val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_a
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp
 
 val id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg
+