Begin refactoring Sail library

- Add back support for bit list representation of bit vectors, for backwards
  compatibility in order to ease integration with the interpreter.  For this
purpose, split out a file sail_operators.lem from sail_values.lem, and add a
variant sail_operators_mwords.lem for the machine word representation of
bitvectors.  Currently, Sail is hardcoded to use machine words for the
sequential state monad, and bit lists for the free monad, but this could be
turned into a command line flag.

- Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem
  library.  The wrappers make use of sizeof expressions to extract type
information from bitvectors (length, start index) in order to pass it to the
Lem functions.

- Add early return support to the free monad, using a new constructor "Return
  of 'r".  As with the sequential monad, functions with early return are
wrapped into "catch_early_return", which extracts the return value at the end
of the function execution.

11 files changed, 1445 insertions, 1843 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 0944f42b..5c539354 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -2,10 +2,13 @@ open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
 
-val return : forall 'a. 'a -> outcome 'a
+type MR 'a 'r = outcome_r 'a 'r
+type M 'a = outcome 'a
+
+val return : forall 'a 'r. 'a -> MR 'a 'r
 let return a = Done a
 
-val bind : forall 'a 'b. outcome 'a -> ('a -> outcome 'b) -> outcome 'b
+val bind : forall 'a 'b 'r. MR 'a 'r -> ('a -> MR 'b 'r) -> MR 'b 'r
 let rec bind m f = match m with
   | Done a ->              f a
   | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
@@ -19,19 +22,57 @@ let rec bind m f = match m with
   | Escape descr ->        Escape descr
   | Fail descr ->          Fail descr
   | Error descr ->         Error descr
+  | Return a ->            Return a
   | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (bind o f ,opt))
 end
 
 
-type M 'a = outcome 'a
-
 let inline (>>=) = bind
-val (>>) : forall 'b. M unit -> M 'b -> M 'b
+val (>>) : forall 'b 'r. MR unit 'r -> MR 'b 'r -> MR 'b 'r
 let inline (>>) m n = m >>= fun _ -> n
 
 val exit : forall 'a 'b. 'b -> M 'a
 let exit s = Fail Nothing
 
+val early_return : forall 'r. 'r -> MR unit 'r
+let early_return r = Return r
+
+val liftR : forall 'a 'r. M 'a -> MR 'a 'r
+let rec liftR m = match m with
+  | Done a ->              Done a
+  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (liftR o,opt))
+  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (liftR o,opt))
+  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (liftR o,opt))
+  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (liftR o,opt))
+  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (liftR o,opt))
+  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (liftR o,opt))
+  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (liftR o,opt))
+  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (liftR o,opt))
+  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (liftR o,opt))
+  | Escape descr ->        Escape descr
+  | Fail descr ->          Fail descr
+  | Error descr ->         Error descr
+  | Return _ ->            Error "uncaught early return"
+end
+
+val catch_early_return : forall 'a 'r. MR 'a 'a -> M 'a
+let rec catch_early_return m = match m with
+  | Done a ->              Done a
+  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
+  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
+  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
+  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (catch_early_return o,opt))
+  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (catch_early_return o,opt))
+  | Escape descr ->        Escape descr
+  | Fail descr ->          Fail descr
+  | Error descr ->         Error descr
+  | Return a ->            Done a
+end
+
 val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
 let read_mem dir rk addr sz =
   let addr = address_lifted_of_bitv addr in
@@ -73,9 +114,9 @@ let read_reg_bit reg i =
   read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
   return (extract_only_element v)
 let read_reg_field reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield)
+  read_reg_aux (external_reg_field_whole reg regfield.field_name)
 let read_reg_bitfield reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
+  read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v ->
   return (extract_only_element v)
 
 let reg_deref = read_reg
@@ -93,12 +134,12 @@ let write_reg_bit reg i bit =
   let iN = natFromInteger i in
   write_reg_aux (external_reg_slice reg (iN,iN)) (Vector [bit] i (is_inc_of_reg reg))
 let write_reg_field reg regfield v =
-  write_reg_aux (external_reg_field_whole reg regfield) v
+  write_reg_aux (external_reg_field_whole reg regfield.field_name) v
 let write_reg_bitfield reg regfield bit =
-  write_reg_aux (external_reg_field_whole reg regfield)
+  write_reg_aux (external_reg_field_whole reg regfield.field_name)
                 (Vector [bit] 0 (is_inc_of_reg reg))
 let write_reg_field_range reg regfield i j v =
-  write_reg_aux (external_reg_field_slice reg regfield (natFromInteger i,natFromInteger j)) v
+  write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v
 
 
 
@@ -110,8 +151,8 @@ val footprint : M unit
 let footprint = Footprint (Done (),Nothing)
 
 
-val foreachM_inc : forall 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'vars) -> M 'vars
+val foreachM_inc : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
 let rec foreachM_inc (i,stop,by) vars body =
   if i <= stop
   then
@@ -120,8 +161,8 @@ let rec foreachM_inc (i,stop,by) vars body =
   else return vars
 
 
-val foreachM_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'vars) -> M 'vars
+val foreachM_dec : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
 let rec foreachM_dec (i,stop,by) vars body =
   if i >= stop
   then
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
new file mode 100644
index 00000000..3919d540
--- /dev/null
+++ b/src/gen_lib/sail_operators.lem
@@ -0,0 +1,531 @@
+open import Pervasives_extra
+open import Machine_word
+open import Sail_impl_base
+open import Sail_values
+
+(*** Bit vector operations *)
+
+let bvlength = length
+
+let set_bitvector_start = set_vector_start
+let reset_bitvector_start = reset_vector_start
+
+let set_bitvector_start_to_length = set_vector_start_to_length
+
+let bitvector_concat = vector_concat
+let inline (^^^) = bitvector_concat
+
+let bitvector_subrange_inc = vector_subrange_inc
+let bitvector_subrange_dec = vector_subrange_dec
+
+let vector_subrange_bl (v, i, j) =
+  let v' = slice v i j in
+  get_elems v'
+
+let bitvector_access_inc = vector_access_inc
+let bitvector_access_dec = vector_access_dec
+let bitvector_update_pos_dec = update_pos
+let bitvector_update_dec = vector_update_dec
+
+let extract_only_bit = extract_only_element
+
+let norm_dec = reset_vector_start
+let adjust_start_index (start, v) = set_vector_start (start, v)
+
+let cast_vec_bool v = bitU_to_bool (extract_only_element v)
+let cast_bit_vec (start, len, b) = Vector (repeat [b] len) start false
+
+let pp_bitu_vector (Vector elems start inc) =
+  let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
+  "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc
+
+
+let most_significant = function
+  | (Vector (b :: _) _ _) -> b
+  | _ -> failwith "most_significant applied to empty vector"
+  end
+
+let bitwise_not_bitlist = List.map bitwise_not_bit
+
+let bitwise_not (Vector bs start is_inc) =
+  Vector (bitwise_not_bitlist bs) start is_inc
+
+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
+  Vector (reverse revbs) start is_inc
+
+let bitwise_and = bitwise_binop (&&)
+let bitwise_or = bitwise_binop (||)
+let bitwise_xor = bitwise_binop xor
+
+let unsigned (Vector bs _ _) : integer =
+  let (sum,_) =
+    List.foldr
+      (fun b (acc,exp) ->
+        match b with
+        | B1 -> (acc + integerPow 2 exp,exp + 1)
+        | B0 -> (acc, exp + 1)
+        | BU -> failwith "unsigned: vector has undefined bits"
+        end)
+      (0,0) bs in
+  sum
+
+let unsigned_big = unsigned
+
+let signed v : integer =
+  match most_significant v with
+  | B1 -> 0 - (1 + (unsigned (bitwise_not v)))
+  | B0 -> unsigned v
+  | BU -> failwith "signed applied to vector with undefined bits"
+  end
+
+let hardware_mod (a: integer) (b:integer) : integer = 
+ if a < 0 && b < 0
+ then (abs a) mod (abs b)
+ else if (a < 0 && b >= 0) 
+ then (a mod b) - b
+ else a mod b
+
+(* There are different possible answers for integer divide regarding
+rounding behaviour on negative operands. Positive operands always
+round down so derive the one we want (trucation towards zero) from
+that *)
+let hardware_quot (a:integer) (b:integer) : integer = 
+  let q = (abs a) / (abs b) in
+  if ((a<0) = (b<0)) then
+    q  (* same sign -- result positive *)
+  else
+    ~q (* different sign -- result negative *)
+
+let quot_signed = hardware_quot
+
+
+let signed_big = signed
+
+let to_num sign = if sign then signed else unsigned
+
+let max_64u = (integerPow 2 64) - 1
+let max_64  = (integerPow 2 63) - 1
+let min_64  = 0 - (integerPow 2 63)
+let max_32u = (4294967295 : integer)
+let max_32  = (2147483647 : integer)
+let min_32  = (0 - 2147483648 : integer)
+let max_8   = (127 : integer)
+let min_8   = (0 - 128 : integer)
+let max_5   = (31 : integer)
+let min_5   = (0 - 32 : integer)
+
+let get_max_representable_in sign (n : integer) : integer =
+  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
+  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
+  else if (n=8) then max_8
+  else if (n=5) then max_5
+  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
+                       | false -> integerPow 2 (natFromInteger n)
+       end
+
+let get_min_representable_in _ (n : integer) : integer =
+  if n = 64 then min_64
+  else if n = 32 then min_32
+  else if n = 8 then min_8
+  else if n = 5 then min_5
+  else 0 - (integerPow 2 (natFromInteger n))
+
+val to_bin_aux : natural -> list bitU
+let rec to_bin_aux x =
+  if x = 0 then []
+  else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
+let to_bin n = List.reverse (to_bin_aux n)
+
+val pad_zero : list bitU -> integer -> list bitU
+let rec pad_zero bits n =
+  if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
+
+
+let rec add_one_bit_ignore_overflow_aux bits = match bits with
+  | [] -> []
+  | B0 :: bits -> B1 :: bits
+  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
+  | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
+end
+
+let add_one_bit_ignore_overflow bits =
+  List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
+  
+
+let to_vec is_inc ((len : integer),(n : integer)) =
+  let start = if is_inc then 0 else len - 1 in
+  let bits = to_bin (naturalFromInteger (abs n)) in
+  let len_bits = integerFromNat (List.length bits) in
+  let longer = len - len_bits in
+  let bits' =
+    if longer < 0 then drop (natFromInteger (abs (longer))) bits
+    else pad_zero bits longer in
+  if n > (0 : integer)
+  then Vector bits' start is_inc
+  else Vector (add_one_bit_ignore_overflow (bitwise_not_bitlist bits'))
+              start is_inc
+
+let to_vec_big = to_vec
+
+let to_vec_inc (start, len, n) = set_vector_start (start, to_vec true (len, n))
+let to_vec_norm_inc (len, n) = to_vec true (len, n)
+let to_vec_dec (start, len, n) = set_vector_start (start, to_vec false (len, n))
+let to_vec_norm_dec (len, n) = to_vec false (len, n)
+
+let cast_0_vec = to_vec_dec
+let cast_1_vec = to_vec_dec
+let cast_01_vec = to_vec_dec
+
+let to_vec_undef is_inc (len : integer) =
+  Vector (replicate (natFromInteger len) BU) (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 exts (start, len, vec) = set_vector_start (start, to_vec (get_dir vec) (len,signed vec))
+let extz (start, len, vec) = set_vector_start (start, to_vec (get_dir vec) (len,unsigned vec))
+
+let exts_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, signed_big vec))
+let extz_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, unsigned_big vec))
+
+(* TODO *)
+let extz_bl (start, len, bits) = Vector bits start false
+let exts_bl (start, len, bits) = Vector bits start false
+
+
+let add (l,r) = integerAdd l r
+let add_signed (l,r) = integerAdd l r
+let sub (l,r) = integerMinus l r
+let mult (l,r) = integerMult l r
+let quotient (l,r) = integerDiv l r
+let modulo (l,r) = hardware_mod l r
+let quot = hardware_quot
+let power (l,r) = integerPow l r
+
+let sub_int = sub
+let mult_int = mult
+
+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)
+
+
+(* add_vec
+ * add_vec_signed
+ * minus_vec
+ * multiply_vec
+ * multiply_vec_signed
+ *)
+let add_VVV = arith_op_vec integerAdd false 1
+let addS_VVV = arith_op_vec integerAdd true 1
+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 mult_vec (l, r) = mult_VVV l r
+let mult_svec (l, r) = multS_VVV l r
+
+let add_vec (l, r) = add_VVV l r
+let sub_vec (l, r) = minus_VVV 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
+ * add_vec_range_signed
+ * minus_vec_range
+ * mult_vec_range
+ * mult_vec_range_signed
+ *)
+let add_VIV = arith_op_vec_range integerAdd false 1
+let addS_VIV = arith_op_vec_range integerAdd true 1
+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 add_vec_int (l, r) = add_VIV l r
+let sub_vec_int (l, r) = minus_VIV l 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
+ * add_range_vec_signed
+ * minus_range_vec
+ * mult_range_vec
+ * mult_range_vec_signed
+ *)
+let add_IVV = arith_op_range_vec integerAdd false 1
+let addS_IVV = arith_op_range_vec integerAdd true 1
+let minus_IVV = arith_op_range_vec integerMinus false 1
+let mult_IVV = arith_op_range_vec integerMult false 2
+let multS_IVV = arith_op_range_vec integerMult true 2
+
+let arith_op_range_vec_range op sign l r = op l (to_num sign r)
+
+(* add_range_vec_range
+ * add_range_vec_range_signed
+ * minus_range_vec_range
+ *)
+let add_IVI = arith_op_range_vec_range integerAdd false
+let addS_IVI = arith_op_range_vec_range integerAdd true
+let minus_IVI = arith_op_range_vec_range integerMinus false
+
+let arith_op_vec_range_range op sign l r = op (to_num sign l) r
+
+(* add_vec_range_range
+ * add_vec_range_range_signed
+ * minus_vec_range_range
+ *)
+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 l r =
+  let (l',r') = (to_num sign l,to_num sign r) in
+  op l' r'
+
+(* add_vec_vec_range
+ * add_vec_vec_range_signed
+ *)
+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) (Vector _ _ is_inc as l)r =
+  let l' = to_num sign l in
+  let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
+  to_vec is_inc (length l * size,n)
+
+(* add_vec_bit
+ * add_vec_bit_signed
+ * minus_vec_bit_signed
+ *)
+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 (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
+  let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
+  let n = op l_sign r_sign in
+  let n_unsign = op l_unsign r_unsign in
+  let correct_size_num = to_vec is_inc (act_size,n) in
+  let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in
+  let overflow =
+    if n <= get_max_representable_in sign len &&
+         n >= get_min_representable_in sign len
+    then B0 else B1 in
+  let c_out = most_significant one_more_size_u in
+  (correct_size_num,overflow,c_out)
+
+(* add_overflow_vec
+ * add_overflow_vec_signed
+ * minus_overflow_vec
+ * minus_overflow_vec_signed
+ * mult_overflow_vec
+ * mult_overflow_vec_signed
+ *)
+let addO_VVV = arith_op_overflow_vec integerAdd false 1
+let addSO_VVV = arith_op_overflow_vec integerAdd true 1
+let minusO_VVV = arith_op_overflow_vec integerMinus false 1
+let minusSO_VVV = arith_op_overflow_vec integerMinus true 1
+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)
+                                  (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
+  let (n,nu,changed) = match r_bit with
+    | B1 -> (op l' 1, op l_u 1, true)
+    | B0 -> (l',l_u,false)
+    | BU -> 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
+  let one_larger = to_vec is_inc (act_size + 1,nu) in
+  let overflow =
+    if changed
+    then
+      if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
+      then B0 else B1
+    else B0 in
+  (correct_size_num,overflow,most_significant one_larger)
+
+(* add_overflow_vec_bit_signed
+ * minus_overflow_vec_bit
+ * minus_overflow_vec_bit_signed
+ *)
+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_shift | RR_shift | LLL_shift
+
+let shift_op_vec op (Vector bs start is_inc,(n : integer)) =
+  let n = natFromInteger n in
+  match op with
+  | LL_shift (*"<<"*) ->
+     Vector (sublist bs (n,List.length bs -1) ++ List.replicate n B0) start is_inc
+  | RR_shift (*">>"*) ->
+     Vector (List.replicate n B0 ++ sublist bs (0,n-1)) start is_inc
+  | LLL_shift (*"<<<"*) ->
+     Vector (sublist bs (n,List.length bs - 1) ++ sublist bs (0,n-1)) start is_inc
+  end
+
+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 shiftl = bitwise_leftshift
+
+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 ((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
+  let (representable,n') =
+    match n with
+    | Just n' ->
+      (n' <= get_max_representable_in sign act_size &&
+         n' >= get_min_representable_in sign act_size, n')
+    | _ -> (false,0)
+    end in
+  if representable
+  then to_vec is_inc (act_size,n')
+  else Vector (List.replicate (natFromInteger act_size) BU) start is_inc
+
+let mod_VVV = arith_op_vec_no0 hardware_mod false 1
+let quot_VVV = arith_op_vec_no0 hardware_quot false 1
+let quotS_VVV = arith_op_vec_no0 hardware_quot true 1
+
+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
+  let (l_u,r_u) = (to_num false l,to_num false r) in
+  let n = arith_op_no0 op l' r' in
+  let n_u = arith_op_no0 op l_u r_u in
+  let (representable,n',n_u') =
+    match (n, n_u) with
+    | (Just n',Just n_u') ->
+       ((n' <= get_max_representable_in sign rep_size &&
+           n' >= (get_min_representable_in sign rep_size)), n', n_u')
+    | _ -> (true,0,0)
+    end in
+  let (correct_size_num,one_more) =
+    if representable then
+      (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
+    else
+      (Vector (List.replicate (natFromInteger act_size) BU) start is_inc,
+       Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in
+  let overflow = if representable then B0 else B1 in
+  (correct_size_num,overflow,most_significant one_more)
+
+let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1
+let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1
+
+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 hardware_mod false 1
+
+val repeat : forall 'a. list 'a -> integer -> list 'a
+let rec repeat xs n =
+  if n = 0 then []
+  else xs ++ repeat xs (n-1)
+
+(* Assumes decreasing bit vectors *)
+let duplicate (bit, length) =
+  Vector (repeat [bit] length) (length - 1) false
+
+let compare_op op (l,r) = (op l r)
+
+let lt = compare_op (<)
+let gt = compare_op (>)
+let lteq = compare_op (<=)
+let gteq = compare_op (>=)
+
+
+let compare_op_vec op sign (l,r) =
+  let (l',r') = (to_num sign l, to_num sign r) in
+  compare_op op (l',r')
+
+let lt_vec = compare_op_vec (<) true
+let gt_vec = compare_op_vec (>) true
+let lteq_vec = compare_op_vec (<=) true
+let gteq_vec = compare_op_vec (>=) true
+
+let lt_vec_signed = compare_op_vec (<) true
+let gt_vec_signed = compare_op_vec (>) true
+let lteq_vec_signed = compare_op_vec (<=) true
+let gteq_vec_signed = compare_op_vec (>=) true
+let lt_vec_unsigned = compare_op_vec (<) false
+let gt_vec_unsigned = compare_op_vec (>) false
+let lteq_vec_unsigned = compare_op_vec (<=) false
+let gteq_vec_unsigned = compare_op_vec (>=) false
+
+let lt_svec = lt_vec_signed
+
+let compare_op_vec_range op sign (l,r) =
+  compare_op op ((to_num sign l),r)
+
+let lt_vec_range = compare_op_vec_range (<) true
+let gt_vec_range = compare_op_vec_range (>) true
+let lteq_vec_range = compare_op_vec_range (<=) true
+let gteq_vec_range = compare_op_vec_range (>=) true
+
+let compare_op_range_vec op sign (l,r) =
+  compare_op op (l, (to_num sign r))
+
+let lt_range_vec = compare_op_range_vec (<) true
+let gt_range_vec = compare_op_range_vec (>) true
+let lteq_range_vec = compare_op_range_vec (<=) true
+let gteq_range_vec = compare_op_range_vec (>=) true
+
+val eq : forall 'a. Eq 'a => 'a * 'a -> bool
+let eq (l,r) = (l = r)
+let eq_range (l,r) = (l = r)
+
+val eq_vec : forall 'a. vector 'a * vector 'a -> bool
+let eq_vec (l,r) = (l = r)
+let eq_bit (l,r) = (l = r)
+let eq_vec_range (l,r) = eq (to_num false l,r)
+let eq_range_vec (l,r) = eq (l, to_num false r)
+let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
+
+let neq (l,r) = not (eq (l,r))
+let neq_bit (l,r) = not (eq_bit (l,r))
+let neq_range (l,r) = not (eq_range (l,r))
+let neq_vec (l,r) = not (eq_vec_vec (l,r))
+let neq_vec_range (l,r) = not (eq_vec_range (l,r))
+let neq_range_vec (l,r) = not (eq_range_vec (l,r))
+
+
+val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
+let make_indexed_vector entries default start length dir =
+  let length = natFromInteger length in
+  Vector (List.foldl replace (replicate length default) entries) start dir
+
+(*
+val make_bit_vector_undef : integer -> vector bitU
+let make_bitvector_undef length =
+  Vector (replicate (natFromInteger length) BU) 0 true
+ *)
+
+(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
+
+let mask' (start, n, Vector bits _ dir) =
+  let current_size = List.length bits in
+  Vector (drop (current_size - (natFromInteger n)) bits) start dir
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
new file mode 100644
index 00000000..87d805f6
--- /dev/null
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -0,0 +1,571 @@
+open import Pervasives_extra
+open import Machine_word
+open import Sail_impl_base
+open import Sail_values
+
+(*** Bit vector operations *)
+
+let bvlength (Bitvector bs _ _) = integerFromNat (word_length bs)
+
+val set_bitvector_start : forall 'a. (integer * bitvector 'a) -> bitvector 'a
+let set_bitvector_start (new_start, Bitvector bs _ is_inc) =
+  Bitvector bs new_start is_inc
+
+let reset_bitvector_start v =
+  set_bitvector_start (if (bvget_dir v) then 0 else (bvlength v - 1), v)
+
+let set_bitvector_start_to_length v =
+  set_bitvector_start (bvlength v - 1, v)
+
+let bitvector_concat (Bitvector bs start is_inc, Bitvector bs' _ _) =
+  Bitvector (word_concat bs bs') start is_inc
+
+let inline (^^^) = bitvector_concat
+
+val bvslice : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b
+let bvslice (Bitvector bs start is_inc) i j =
+  let iN = natFromInteger i in
+  let jN = natFromInteger j in
+  let startN = natFromInteger start in
+  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
+  let subvector_bits = word_extract lo hi bs in
+  Bitvector subvector_bits i is_inc
+
+let bitvector_subrange_inc (v, i, j) = bvslice v i j
+let bitvector_subrange_dec (v, i, j) = bvslice v i j
+
+let vector_subrange_bl (v, i, j) =
+  let v' = slice (bvec_to_vec v) i j in
+  get_elems v'
+
+(* this is for the vector slicing introduced in vector-concat patterns: i and j
+index into the "raw data", the list of bits. Therefore getting the bit list is
+easy, but the start index has to be transformed to match the old vector start
+and the direction. *)
+val bvslice_raw : forall 'a 'b. Size 'b => bitvector 'a -> integer -> integer -> bitvector 'b
+let bvslice_raw (Bitvector bs start is_inc) i j =
+  let iN = natFromInteger i in
+  let jN = natFromInteger j in
+  let bits = word_extract iN jN bs in
+  let len = integerFromNat (word_length bits) in
+  Bitvector bits (if is_inc then 0 else len - 1) is_inc
+
+val bvupdate_aux : forall 'a 'b. bitvector 'a -> integer -> integer -> mword 'b -> bitvector 'a
+let bvupdate_aux (Bitvector bs start is_inc) i j bs' =
+  let iN = natFromInteger i in
+  let jN = natFromInteger j in
+  let startN = natFromInteger start in
+  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
+  let bits = word_update bs lo hi bs' in
+  Bitvector bits start is_inc
+
+val bvupdate : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a
+let bvupdate v i j (Bitvector bs' _ _) =
+  bvupdate_aux v i j bs'
+
+val bvaccess : forall 'a. bitvector 'a -> integer -> bitU
+let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU (
+  if is_inc then getBit bs (natFromInteger (n - start))
+  else getBit bs (natFromInteger (start - n)))
+
+val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bitU -> bitvector 'a
+let bvupdate_pos v n b =
+  bvupdate_aux v n n ((wordFromNatural (if bitU_to_bool b then 1 else 0)) : mword ty1)
+
+let bitvector_access_inc (v, i) = bvaccess v i
+let bitvector_access_dec (v, i) = bvaccess v i
+let bitvector_update_pos_dec (v, i, b) = bvupdate_pos v i b
+let bitvector_update_dec (v, i, j, v') = bvupdate v i j v'
+
+val extract_only_bit : bitvector ty1 -> bitU
+let extract_only_bit (Bitvector elems _ _) =
+  (*let l = word_length elems in
+  if l = 1 then*)
+    bool_to_bitU (msb elems)
+  (*else if l = 0 then
+    failwith "extract_single_bit called for empty vector"
+  else
+    failwith "extract_single_bit called for vector with more bits"*)
+
+
+let norm_dec = reset_bitvector_start
+let adjust_start_index (start, v) = set_bitvector_start (start, v)
+
+let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
+let cast_bit_vec (start, len, b) = vec_to_bvec (Vector [b] start false)
+
+let pp_bitu_vector (Vector elems start inc) =
+  let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
+  "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc
+
+
+let most_significant (Bitvector v _ _) =
+  if word_length v = 0 then
+    failwith "most_significant applied to empty vector"
+  else
+    bool_to_bitU (msb v)
+
+let bitwise_not_bitlist = List.map bitwise_not_bit
+
+let bitwise_not (Bitvector bs start is_inc) =
+  Bitvector (lNot bs) start is_inc
+
+let bitwise_binop op (Bitvector bsl start is_inc, Bitvector bsr _ _) =
+  Bitvector (op bsl bsr) start is_inc
+
+let bitwise_and = bitwise_binop lAnd
+let bitwise_or = bitwise_binop lOr
+let bitwise_xor = bitwise_binop lXor
+
+let unsigned (Bitvector bs _ _) : integer = unsignedIntegerFromWord bs
+let unsigned_big = unsigned
+
+let signed (Bitvector v _ _) : integer = signedIntegerFromWord v
+
+let hardware_mod (a: integer) (b:integer) : integer = 
+ if a < 0 && b < 0
+ then (abs a) mod (abs b)
+ else if (a < 0 && b >= 0) 
+ then (a mod b) - b
+ else a mod b
+
+(* There are different possible answers for integer divide regarding
+rounding behaviour on negative operands. Positive operands always
+round down so derive the one we want (trucation towards zero) from
+that *)
+let hardware_quot (a:integer) (b:integer) : integer = 
+  let q = (abs a) / (abs b) in
+  if ((a<0) = (b<0)) then
+    q  (* same sign -- result positive *)
+  else
+    ~q (* different sign -- result negative *)
+
+let quot_signed = hardware_quot
+
+
+let signed_big = signed
+
+let to_num sign = if sign then signed else unsigned
+
+let max_64u = (integerPow 2 64) - 1
+let max_64  = (integerPow 2 63) - 1
+let min_64  = 0 - (integerPow 2 63)
+let max_32u = (4294967295 : integer)
+let max_32  = (2147483647 : integer)
+let min_32  = (0 - 2147483648 : integer)
+let max_8   = (127 : integer)
+let min_8   = (0 - 128 : integer)
+let max_5   = (31 : integer)
+let min_5   = (0 - 32 : integer)
+
+let get_max_representable_in sign (n : integer) : integer =
+  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
+  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
+  else if (n=8) then max_8
+  else if (n=5) then max_5
+  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
+                       | false -> integerPow 2 (natFromInteger n)
+       end
+
+let get_min_representable_in _ (n : integer) : integer =
+  if n = 64 then min_64
+  else if n = 32 then min_32
+  else if n = 8 then min_8
+  else if n = 5 then min_5
+  else 0 - (integerPow 2 (natFromInteger n))
+
+val to_bin_aux : natural -> list bitU
+let rec to_bin_aux x =
+  if x = 0 then []
+  else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
+let to_bin n = List.reverse (to_bin_aux n)
+
+val pad_zero : list bitU -> integer -> list bitU
+let rec pad_zero bits n =
+  if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
+
+
+let rec add_one_bit_ignore_overflow_aux bits = match bits with
+  | [] -> []
+  | B0 :: bits -> B1 :: bits
+  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
+  | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
+end
+
+let add_one_bit_ignore_overflow bits =
+  List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
+  
+val to_vec_ord : forall 'a. Size 'a => bool -> (integer * integer) -> bitvector 'a
+let to_vec_ord is_inc ((len : integer), (n : integer)) =
+  (* Bitvector length is determined by return type *)
+  let bits = wordFromInteger n in
+  let len = integerFromNat (word_length bits) in
+  let start = if is_inc then 0 else len - 1 in
+  (*if integerFromNat (word_length bits) = len then*)
+    Bitvector bits start is_inc
+  (*else
+    failwith "Vector length mismatch in to_vec"*)
+
+let to_vec_big = to_vec_ord
+
+let to_vec_inc (start, len, n) = set_bitvector_start (start, to_vec_ord true (len, n))
+let to_vec_norm_inc (len, n) = to_vec_ord true (len, n)
+let to_vec_dec (start, len, n) = set_bitvector_start (start, to_vec_ord false (len, n))
+let to_vec_norm_dec (len, n) = to_vec_ord false (len, n)
+
+(* TODO: Think about undefined bit(vector)s *)
+let to_vec_undef is_inc (len : integer) =
+  Bitvector (failwith "undefined bitvector") (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 exts (start, len, vec) = set_bitvector_start (start, to_vec_ord (bvget_dir vec) (len, signed vec))
+val extz : forall 'a 'b. Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b
+let extz (start, len, vec) = set_bitvector_start (start, to_vec_ord (bvget_dir vec) (len, unsigned vec))
+
+let exts_big (start, len, vec) = set_bitvector_start (start, to_vec_big (bvget_dir vec) (len, signed_big vec))
+let extz_big (start, len, vec) = set_bitvector_start (start, to_vec_big (bvget_dir vec) (len, unsigned_big vec))
+
+(* TODO *)
+let extz_bl (start, len, bits) = set_bitvector_start (start, vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false))
+let exts_bl (start, len, bits) = set_bitvector_start (start, vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false))
+
+let add (l,r) = integerAdd l r
+let add_signed (l,r) = integerAdd l r
+let sub (l,r) = integerMinus l r
+let mult (l,r) = integerMult l r
+let quotient (l,r) = integerDiv l r
+let modulo (l,r) = hardware_mod l r
+let quot = hardware_quot
+let power (l,r) = integerPow l r
+
+let sub_int = sub
+let mult_int = mult
+
+(* TODO: this, and the definitions that use it, currently require Size for
+   to_vec, which I'd rather avoid in favour of library versions; the
+   double-size results for multiplication may be a problem *)
+let arith_op_vec op sign (size : integer) (Bitvector _ _ 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_ord is_inc (size, n)
+
+
+(* add_vec
+ * add_vec_signed
+ * minus_vec
+ * multiply_vec
+ * multiply_vec_signed
+ *)
+let add_VVV = arith_op_vec integerAdd false 1
+let addS_VVV = arith_op_vec integerAdd true 1
+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 mult_vec (l, r) = mult_VVV l r
+let mult_svec (l, r) = multS_VVV l r
+
+let add_vec (l, r) = add_VVV l r
+let sub_vec (l, r) = minus_VVV l r
+
+val arith_op_vec_range : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'b
+let arith_op_vec_range op sign size (Bitvector _ _ is_inc as l) r =
+  arith_op_vec op sign size l ((to_vec_ord is_inc (size, r)) : bitvector 'a)
+
+(* add_vec_range
+ * add_vec_range_signed
+ * minus_vec_range
+ * mult_vec_range
+ * mult_vec_range_signed
+ *)
+let add_VIV = arith_op_vec_range integerAdd false 1
+let addS_VIV = arith_op_vec_range integerAdd true 1
+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 add_vec_int (l, r) = add_VIV l r
+let sub_vec_int (l, r) = minus_VIV l r
+
+val arith_op_range_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'b
+let arith_op_range_vec op sign size l (Bitvector _ _ is_inc as r) =
+  arith_op_vec op sign size ((to_vec_ord is_inc (size, l)) : bitvector 'a) r
+
+(* add_range_vec
+ * add_range_vec_signed
+ * minus_range_vec
+ * mult_range_vec
+ * mult_range_vec_signed
+ *)
+let add_IVV = arith_op_range_vec integerAdd false 1
+let addS_IVV = arith_op_range_vec integerAdd true 1
+let minus_IVV = arith_op_range_vec integerMinus false 1
+let mult_IVV = arith_op_range_vec integerMult false 2
+let multS_IVV = arith_op_range_vec integerMult true 2
+
+let arith_op_range_vec_range op sign l r = op l (to_num sign r)
+
+(* add_range_vec_range
+ * add_range_vec_range_signed
+ * minus_range_vec_range
+ *)
+let add_IVI = arith_op_range_vec_range integerAdd false
+let addS_IVI = arith_op_range_vec_range integerAdd true
+let minus_IVI = arith_op_range_vec_range integerMinus false
+
+let arith_op_vec_range_range op sign l r = op (to_num sign l) r
+
+(* add_vec_range_range
+ * add_vec_range_range_signed
+ * minus_vec_range_range
+ *)
+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 l r =
+  let (l',r') = (to_num sign l,to_num sign r) in
+  op l' r'
+
+(* add_vec_vec_range
+ * add_vec_vec_range_signed
+ *)
+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) (Bitvector _ _ is_inc as l) r =
+  let l' = to_num sign l in
+  let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
+  to_vec_ord is_inc (size, n)
+
+(* add_vec_bit
+ * add_vec_bit_signed
+ * minus_vec_bit_signed
+ *)
+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
+
+(* TODO: these can't be done directly in Lem because of the one_more size calculation
+val arith_op_overflow_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b * bitU * bool
+let rec arith_op_overflow_vec op sign size (Bitvector _ _ is_inc as l) r =
+  let len = bvlength l in
+  let act_size = len * size in
+  let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
+  let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
+  let n = op l_sign r_sign in
+  let n_unsign = op l_unsign r_unsign in
+  let correct_size_num = to_vec_ord is_inc (act_size,n) in
+  let one_more_size_u = to_vec_ord is_inc (act_size + 1,n_unsign) in
+  let overflow =
+    if n <= get_max_representable_in sign len &&
+         n >= get_min_representable_in sign len
+    then B0 else B1 in
+  let c_out = most_significant one_more_size_u in
+  (correct_size_num,overflow,c_out)
+
+(* add_overflow_vec
+ * add_overflow_vec_signed
+ * minus_overflow_vec
+ * minus_overflow_vec_signed
+ * mult_overflow_vec
+ * mult_overflow_vec_signed
+ *)
+let addO_VVV = arith_op_overflow_vec integerAdd false 1
+let addSO_VVV = arith_op_overflow_vec integerAdd true 1
+let minusO_VVV = arith_op_overflow_vec integerMinus false 1
+let minusSO_VVV = arith_op_overflow_vec integerMinus true 1
+let multO_VVV = arith_op_overflow_vec integerMult false 2
+let multSO_VVV = arith_op_overflow_vec integerMult true 2
+
+val arith_op_overflow_vec_bit : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer ->
+                                bitvector 'a -> bitU -> bitvector 'b * bitU * bool
+let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer)
+                                  (Bitvector _ _ is_inc as l) r_bit =
+  let act_size = bvlength l * size in
+  let l' = to_num sign l in
+  let l_u = to_num false l in
+  let (n,nu,changed) = match r_bit with
+    | B1 -> (op l' 1, op l_u 1, true)
+    | B0 -> (l',l_u,false)
+    | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
+    end in
+(*    | _ -> assert false *)
+  let correct_size_num = to_vec_ord is_inc (act_size,n) in
+  let one_larger = to_vec_ord is_inc (act_size + 1,nu) in
+  let overflow =
+    if changed
+    then
+      if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
+      then B0 else B1
+    else B0 in
+  (correct_size_num,overflow,most_significant one_larger)
+
+(* add_overflow_vec_bit_signed
+ * minus_overflow_vec_bit
+ * minus_overflow_vec_bit_signed
+ *)
+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_shift | RR_shift | LLL_shift
+
+let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) =
+  let n = natFromInteger n in
+  match op with
+  | LL_shift (*"<<"*) ->
+     Bitvector (shiftLeft bs n) start is_inc
+  | RR_shift (*">>"*) ->
+     Bitvector (shiftRight bs n) start is_inc
+  | LLL_shift (*"<<<"*) ->
+     Bitvector (rotateLeft n bs) start is_inc
+  end
+
+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 shiftl = bitwise_leftshift
+
+let rec arith_op_no0 (op : integer -> integer -> integer) l r =
+  if r = 0
+  then Nothing
+  else Just (op l r)
+(* TODO
+let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Bitvector _ start is_inc) as l) r =
+  let act_size = bvlength l * size in
+  let (l',r') = (to_num sign l,to_num sign r) in
+  let n = arith_op_no0 op l' r' in
+  let (representable,n') =
+    match n with
+    | Just n' ->
+      (n' <= get_max_representable_in sign act_size &&
+         n' >= get_min_representable_in sign act_size, n')
+    | _ -> (false,0)
+    end in
+  if representable
+  then to_vec_ord is_inc (act_size,n')
+  else Vector (List.replicate (natFromInteger act_size) BU) start is_inc
+
+let mod_VVV = arith_op_vec_no0 hardware_mod false 1
+let quot_VVV = arith_op_vec_no0 hardware_quot false 1
+let quotS_VVV = arith_op_vec_no0 hardware_quot true 1
+
+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
+  let (l_u,r_u) = (to_num false l,to_num false r) in
+  let n = arith_op_no0 op l' r' in
+  let n_u = arith_op_no0 op l_u r_u in
+  let (representable,n',n_u') =
+    match (n, n_u) with
+    | (Just n',Just n_u') ->
+       ((n' <= get_max_representable_in sign rep_size &&
+           n' >= (get_min_representable_in sign rep_size)), n', n_u')
+    | _ -> (true,0,0)
+    end in
+  let (correct_size_num,one_more) =
+    if representable then
+      (to_vec_ord is_inc (act_size,n'),to_vec_ord is_inc (act_size + 1,n_u'))
+    else
+      (Vector (List.replicate (natFromInteger act_size) BU) start is_inc,
+       Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in
+  let overflow = if representable then B0 else B1 in
+  (correct_size_num,overflow,most_significant one_more)
+
+let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1
+let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1
+
+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_ord is_inc (length l,r))
+
+let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1
+*)
+
+let duplicate (bit, length) =
+  vec_to_bvec (Vector (repeat [bit] length) (length - 1) false)
+
+let compare_op op (l,r) = (op l r)
+
+let lt = compare_op (<)
+let gt = compare_op (>)
+let lteq = compare_op (<=)
+let gteq = compare_op (>=)
+
+let compare_op_vec op sign (l,r) =
+  let (l',r') = (to_num sign l, to_num sign r) in
+  compare_op op (l',r')
+
+let lt_vec = compare_op_vec (<) true
+let gt_vec = compare_op_vec (>) true
+let lteq_vec = compare_op_vec (<=) true
+let gteq_vec = compare_op_vec (>=) true
+
+let lt_vec_signed = compare_op_vec (<) true
+let gt_vec_signed = compare_op_vec (>) true
+let lteq_vec_signed = compare_op_vec (<=) true
+let gteq_vec_signed = compare_op_vec (>=) true
+let lt_vec_unsigned = compare_op_vec (<) false
+let gt_vec_unsigned = compare_op_vec (>) false
+let lteq_vec_unsigned = compare_op_vec (<=) false
+let gteq_vec_unsigned = compare_op_vec (>=) false
+
+let lt_svec = lt_vec_signed
+
+let compare_op_vec_range op sign (l,r) =
+  compare_op op ((to_num sign l),r)
+
+let lt_vec_range = compare_op_vec_range (<) true
+let gt_vec_range = compare_op_vec_range (>) true
+let lteq_vec_range = compare_op_vec_range (<=) true
+let gteq_vec_range = compare_op_vec_range (>=) true
+
+let compare_op_range_vec op sign (l,r) =
+  compare_op op (l, (to_num sign r))
+
+let lt_range_vec = compare_op_range_vec (<) true
+let gt_range_vec = compare_op_range_vec (>) true
+let lteq_range_vec = compare_op_range_vec (<=) true
+let gteq_range_vec = compare_op_range_vec (>=) true
+
+val eq : forall 'a. Eq 'a => 'a * 'a -> bool
+let eq (l,r) = (l = r)
+let eq_range (l,r) = (l = r)
+
+val eq_vec : forall 'a. bitvector 'a * bitvector 'a -> bool
+let eq_vec (l,r) = (l = r)
+let eq_bit (l,r) = (l = r)
+let eq_vec_range (l,r) = eq (to_num false l,r)
+let eq_range_vec (l,r) = eq (l, to_num false r)
+let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
+
+let neq (l,r) = not (eq (l,r))
+let neq_bit (l,r) = not (eq_bit (l,r))
+let neq_range (l,r) = not (eq_range (l,r))
+let neq_vec (l,r) = not (eq_vec_vec (l,r))
+let neq_vec_range (l,r) = not (eq_vec_range (l,r))
+let neq_range_vec (l,r) = not (eq_range_vec (l,r))
+
+
+val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
+let make_indexed_vector entries default start length dir =
+  let length = natFromInteger length in
+  Vector (List.foldl replace (replicate length default) entries) start dir
+
+(*
+val make_bit_vector_undef : integer -> vector bitU
+let make_bitvector_undef length =
+  Vector (replicate (natFromInteger length) BU) 0 true
+ *)
+
+(* let bitwise_not_range_bit n = bitwise_not (to_vec_ord defaultDir n) *)
+
+(* TODO *)
+val mask : forall 'a 'b. Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b
+let mask (start, _, Bitvector w _ dir) = (Bitvector (zeroExtend w) start dir)
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index eb5cdef5..eeec7440 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -17,6 +17,13 @@ let bool_xor (l, r) = xor l r
 
 let list_append (l, r) = l ++ r
 
+val repeat : forall 'a. list 'a -> integer -> list 'a
+let rec repeat xs n =
+  if n = 0 then []
+  else xs ++ repeat xs (n-1)
+
+let duplicate_to_list (bit, length) = repeat [bit] length
+
 let rec replace bs ((n : integer),b') = match bs with
   | [] -> []
   | b :: bs ->
@@ -137,17 +144,17 @@ let bool_of_dir = function
 
 (*** Vector operations *)
 
-val set_vector_start : forall 'a. integer -> vector 'a -> vector 'a
-let set_vector_start new_start (Vector bs _ is_inc) =
+val set_vector_start : forall 'a. (integer * vector 'a) -> vector 'a
+let set_vector_start (new_start, Vector bs _ is_inc) =
   Vector bs new_start is_inc
 
 let reset_vector_start v =
-  set_vector_start (if (get_dir v) then 0 else (length v - 1)) v
+  set_vector_start (if (get_dir v) then 0 else (length v - 1), v)
 
 let set_vector_start_to_length v =
-  set_vector_start (length v - 1) v
+  set_vector_start (length v - 1, v)
 
-let vector_concat (Vector bs start is_inc) (Vector bs' _ _) =
+let vector_concat (Vector bs start is_inc, Vector bs' _ _) =
   Vector (bs ++ bs') start is_inc
 
 let inline (^^) = vector_concat
@@ -173,6 +180,9 @@ let slice (Vector bs start is_inc) i j =
     sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) in
   Vector subvector_bits i is_inc
 
+let vector_subrange_inc (v, i, j) = slice v i j
+let vector_subrange_dec (v, i, j) = slice v i j
+
 (* this is for the vector slicing introduced in vector-concat patterns: i and j
 index into the "raw data", the list of bits. Therefore getting the bit list is
 easy, but the start index has to be transformed to match the old vector start
@@ -200,6 +210,9 @@ val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector '
 let update v i j (Vector bs' _ _) =
   update_aux v i j bs'
 
+let vector_update_inc (v, i, j, v') = update v i j v'
+let vector_update_dec (v, i, j, v') = update v i j v'
+
 val access : forall 'a. vector 'a -> integer -> 'a
 let access (Vector bs start is_inc) n =
   if is_inc then List_extra.nth bs (natFromInteger (n - start))
@@ -212,6 +225,12 @@ val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a
 let update_pos v n b =
   update_aux v n n [b]
 
+let extract_only_element (Vector elems _ _) = match elems with
+  | [] -> failwith "extract_only_element called for empty vector"
+  | [e] -> e
+  | _ -> failwith "extract_only_element called for vector with more elements"
+end
+
 (*** Bitvectors *)
 
 (* element list * start * has increasing direction *)
@@ -224,7 +243,6 @@ let showBitvector (Bitvector elems start inc) =
 let bvget_dir (Bitvector _ _ ord) = ord
 let bvget_start (Bitvector _ s _) = s
 let bvget_elems (Bitvector elems _ _) = elems
-let bvlength (Bitvector bs _ _) = integerFromNat (word_length bs)
 
 instance forall 'a. (Show (bitvector 'a))
   let show = showBitvector
@@ -240,581 +258,8 @@ let vec_to_bvec (Vector elems start is_inc) =
 
 (*** Vector operations *)
 
-val set_bitvector_start : forall 'a. integer -> bitvector 'a -> bitvector 'a
-let set_bitvector_start new_start (Bitvector bs _ is_inc) =
-  Bitvector bs new_start is_inc
-
-let reset_bitvector_start v =
-  set_bitvector_start (if (bvget_dir v) then 0 else (bvlength v - 1)) v
-
-let set_bitvector_start_to_length v =
-  set_bitvector_start (bvlength v - 1) v
-
-let bitvector_concat (Bitvector bs start is_inc, Bitvector bs' _ _) =
-  Bitvector (word_concat bs bs') start is_inc
-
-let norm_dec = reset_bitvector_start
-let adjust_dec = reset_bitvector_start
-
-let inline (^^^) = bitvector_concat
-
-val bvslice : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice (Bitvector bs start is_inc) i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
-  let subvector_bits = word_extract lo hi bs in
-  Bitvector subvector_bits i is_inc
-
-let bitvector_subrange_inc (v, i, j) = bvslice v i j
-let bitvector_subrange_dec (v, i, j) = bvslice v i j
-
-let vector_subrange_bl (v, i, j) =
-  let v' = slice (bvec_to_vec v) i j in
-  get_elems v'
-
-(* this is for the vector slicing introduced in vector-concat patterns: i and j
-index into the "raw data", the list of bits. Therefore getting the bit list is
-easy, but the start index has to be transformed to match the old vector start
-and the direction. *)
-val bvslice_raw : forall 'a 'b. Size 'b => bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice_raw (Bitvector bs start is_inc) i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let bits = word_extract iN jN bs in
-  let len = integerFromNat (word_length bits) in
-  Bitvector bits (if is_inc then 0 else len - 1) is_inc
-
-val bvupdate_aux : forall 'a 'b. bitvector 'a -> integer -> integer -> mword 'b -> bitvector 'a
-let bvupdate_aux (Bitvector bs start is_inc) i j bs' =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
-  let bits = word_update bs lo hi bs' in
-  Bitvector bits start is_inc
-
-val bvupdate : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a
-let bvupdate v i j (Bitvector bs' _ _) =
-  bvupdate_aux v i j bs'
-
-val bvaccess : forall 'a. bitvector 'a -> integer -> bitU
-let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU (
-  if is_inc then getBit bs (natFromInteger (n - start))
-  else getBit bs (natFromInteger (start - n)))
-
-val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bitU -> bitvector 'a
-let bvupdate_pos v n b =
-  bvupdate_aux v n n ((wordFromNatural (if bitU_to_bool b then 1 else 0)) : mword ty1)
-
-let bitvector_access_inc (v, i) = bvaccess v i
-let bitvector_access_dec (v, i) = bvaccess v i
-let bitvector_update_pos_dec (v, i, b) = bvupdate_pos v i b
-let bitvector_update_dec (v, i, j, v') = bvupdate v i j v'
-
-(*** Bit vector operations *)
-
-let extract_only_element (Vector elems _ _) = match elems with
-  | [] -> failwith "extract_only_element called for empty vector"
-  | [e] -> e
-  | _ -> failwith "extract_only_element called for vector with more elements"
-end
-
-val extract_only_bit : bitvector ty1 -> bitU
-let extract_only_bit (Bitvector elems _ _) =
-  (*let l = word_length elems in
-  if l = 1 then*)
-    bool_to_bitU (msb elems)
-  (*else if l = 0 then
-    failwith "extract_single_bit called for empty vector"
-  else
-    failwith "extract_single_bit called for vector with more bits"*)
-
-let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
-let cast_bit_vec b = vec_to_bvec (Vector [b] 0 false)
-
-let pp_bitu_vector (Vector elems start inc) =
-  let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
-  "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc
-
-
-let most_significant (Bitvector v _ _) =
-  if word_length v = 0 then
-    failwith "most_significant applied to empty vector"
-  else
-    bool_to_bitU (msb v)
-
-let bitwise_not_bitlist = List.map bitwise_not_bit
-
-let bitwise_not (Bitvector bs start is_inc) =
-  Bitvector (lNot bs) start is_inc
-
-let bitwise_binop op (Bitvector bsl start is_inc, Bitvector bsr _ _) =
-  Bitvector (op bsl bsr) start is_inc
-
-let bitwise_and = bitwise_binop lAnd
-let bitwise_or = bitwise_binop lOr
-let bitwise_xor = bitwise_binop lXor
-
-let unsigned (Bitvector bs _ _) : integer = unsignedIntegerFromWord bs
-let unsigned_big = unsigned
-
-let signed (Bitvector v _ _) : integer = signedIntegerFromWord v
-
-let hardware_mod (a: integer) (b:integer) : integer = 
- if a < 0 && b < 0
- then (abs a) mod (abs b)
- else if (a < 0 && b >= 0) 
- then (a mod b) - b
- else a mod b
-
-(* There are different possible answers for integer divide regarding
-rounding behaviour on negative operands. Positive operands always
-round down so derive the one we want (trucation towards zero) from
-that *)
-let hardware_quot (a:integer) (b:integer) : integer = 
-  let q = (abs a) / (abs b) in
-  if ((a<0) = (b<0)) then
-    q  (* same sign -- result positive *)
-  else
-    integerNegate q (* different sign -- result negative *)
-
-let quot_signed = hardware_quot
-
-
-let signed_big = signed
-
-let to_num sign = if sign then signed else unsigned
-
-let max_64u = (integerPow 2 64) - 1
-let max_64  = (integerPow 2 63) - 1
-let min_64  = 0 - (integerPow 2 63)
-let max_32u = (4294967295 : integer)
-let max_32  = (2147483647 : integer)
-let min_32  = (0 - 2147483648 : integer)
-let max_8   = (127 : integer)
-let min_8   = (0 - 128 : integer)
-let max_5   = (31 : integer)
-let min_5   = (0 - 32 : integer)
-
-let get_max_representable_in sign (n : integer) : integer =
-  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
-  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
-  else if (n=8) then max_8
-  else if (n=5) then max_5
-  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
-                       | false -> integerPow 2 (natFromInteger n)
-       end
-
-let get_min_representable_in _ (n : integer) : integer =
-  if n = 64 then min_64
-  else if n = 32 then min_32
-  else if n = 8 then min_8
-  else if n = 5 then min_5
-  else 0 - (integerPow 2 (natFromInteger n))
-
-val to_bin_aux : natural -> list bitU
-let rec to_bin_aux x =
-  if x = 0 then []
-  else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
-let to_bin n = List.reverse (to_bin_aux n)
-
-val pad_zero : list bitU -> integer -> list bitU
-let rec pad_zero bits n =
-  if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
-
-
-let rec add_one_bit_ignore_overflow_aux bits = match bits with
-  | [] -> []
-  | B0 :: bits -> B1 :: bits
-  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
-  | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
-end
-
-let add_one_bit_ignore_overflow bits =
-  List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
-  
-let to_vec is_inc ((n : integer)) =
-  (* Bitvector length is determined by return type *)
-  let bits = wordFromInteger n in
-  let len = integerFromNat (word_length bits) in
-  let start = if is_inc then 0 else len - 1 in
-  (*if integerFromNat (word_length bits) = len then*)
-    Bitvector bits start is_inc
-  (*else
-    failwith "Vector length mismatch in to_vec"*)
-
-let to_vec_big = to_vec
-
-let to_vec_inc = to_vec true
-let to_vec_dec = to_vec false
-
-let cast_0_vec = to_vec_dec
-let cast_1_vec = to_vec_dec
-let cast_01_vec = to_vec_dec
-
-(* TODO: Think about undefined bit(vector)s *)
-let to_vec_undef is_inc (len : integer) =
-  Bitvector (failwith "undefined bitvector") (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 exts (vec) = to_vec (bvget_dir vec) (signed vec)
-let extz (vec) = to_vec (bvget_dir vec) (unsigned vec)
-
-let exts_big (vec) = to_vec_big (bvget_dir vec) (signed_big vec)
-let extz_big (vec) = to_vec_big (bvget_dir vec) (unsigned_big vec)
-
-let extz_bl (bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
-
-let add (l,r) = integerAdd l r
-let add_signed (l,r) = integerAdd l r
-let sub (l,r) = integerMinus l r
-let multiply (l,r) = integerMult l r
-let quotient (l,r) = integerDiv l r
-let modulo (l,r) = hardware_mod l r
-let quot = hardware_quot
-let power (l,r) = integerPow l r
-
-let sub_int = sub
-let mul_int = multiply
-
-(* TODO: this, and the definitions that use it, currently require Size for
-   to_vec, which I'd rather avoid in favour of library versions; the
-   double-size results for multiplication may be a problem *)
-let arith_op_vec op sign (size : integer) (Bitvector _ _ 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 (n)
-
-
-(* add_vec
- * add_vec_signed
- * minus_vec
- * multiply_vec
- * multiply_vec_signed
- *)
-let add_VVV = arith_op_vec integerAdd false 1
-let addS_VVV = arith_op_vec integerAdd true 1
-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 mul_vec (l, r) = mult_VVV l r
-let mul_svec (l, r) = multS_VVV l r
-
-let add_vec (l, r) = add_VVV l r
-let sub_vec (l, r) = minus_VVV l r
-
-val arith_op_vec_range : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'b
-let arith_op_vec_range op sign size (Bitvector _ _ is_inc as l) r =
-  arith_op_vec op sign size l ((to_vec is_inc (r)) : bitvector 'a)
-
-(* add_vec_range
- * add_vec_range_signed
- * minus_vec_range
- * mult_vec_range
- * mult_vec_range_signed
- *)
-let add_VIV = arith_op_vec_range integerAdd false 1
-let addS_VIV = arith_op_vec_range integerAdd true 1
-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 add_vec_int (l, r) = add_VIV l r
-let sub_vec_int (l, r) = minus_VIV l r
-
-val arith_op_range_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'b
-let arith_op_range_vec op sign size l (Bitvector _ _ is_inc as r) =
-  arith_op_vec op sign size ((to_vec is_inc (l)) : bitvector 'a) r
-
-(* add_range_vec
- * add_range_vec_signed
- * minus_range_vec
- * mult_range_vec
- * mult_range_vec_signed
- *)
-let add_IVV = arith_op_range_vec integerAdd false 1
-let addS_IVV = arith_op_range_vec integerAdd true 1
-let minus_IVV = arith_op_range_vec integerMinus false 1
-let mult_IVV = arith_op_range_vec integerMult false 2
-let multS_IVV = arith_op_range_vec integerMult true 2
-
-let arith_op_range_vec_range op sign l r = op l (to_num sign r)
-
-(* add_range_vec_range
- * add_range_vec_range_signed
- * minus_range_vec_range
- *)
-let add_IVI = arith_op_range_vec_range integerAdd false
-let addS_IVI = arith_op_range_vec_range integerAdd true
-let minus_IVI = arith_op_range_vec_range integerMinus false
-
-let arith_op_vec_range_range op sign l r = op (to_num sign l) r
-
-(* add_vec_range_range
- * add_vec_range_range_signed
- * minus_vec_range_range
- *)
-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 l r =
-  let (l',r') = (to_num sign l,to_num sign r) in
-  op l' r'
-
-(* add_vec_vec_range
- * add_vec_vec_range_signed
- *)
-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) (Bitvector _ _ is_inc as l) r =
-  let l' = to_num sign l in
-  let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
-  to_vec is_inc (n)
-
-(* add_vec_bit
- * add_vec_bit_signed
- * minus_vec_bit_signed
- *)
-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
-
-(* TODO: these can't be done directly in Lem because of the one_more size calculation
-val arith_op_overflow_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b * bitU * bool
-let rec arith_op_overflow_vec op sign size (Bitvector _ _ is_inc as l) r =
-  let len = bvlength l in
-  let act_size = len * size in
-  let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
-  let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
-  let n = op l_sign r_sign in
-  let n_unsign = op l_unsign r_unsign in
-  let correct_size_num = to_vec is_inc (act_size,n) in
-  let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in
-  let overflow =
-    if n <= get_max_representable_in sign len &&
-         n >= get_min_representable_in sign len
-    then B0 else B1 in
-  let c_out = most_significant one_more_size_u in
-  (correct_size_num,overflow,c_out)
-
-(* add_overflow_vec
- * add_overflow_vec_signed
- * minus_overflow_vec
- * minus_overflow_vec_signed
- * mult_overflow_vec
- * mult_overflow_vec_signed
- *)
-let addO_VVV = arith_op_overflow_vec integerAdd false 1
-let addSO_VVV = arith_op_overflow_vec integerAdd true 1
-let minusO_VVV = arith_op_overflow_vec integerMinus false 1
-let minusSO_VVV = arith_op_overflow_vec integerMinus true 1
-let multO_VVV = arith_op_overflow_vec integerMult false 2
-let multSO_VVV = arith_op_overflow_vec integerMult true 2
-
-val arith_op_overflow_vec_bit : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer ->
-                                bitvector 'a -> bitU -> bitvector 'b * bitU * bool
-let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer)
-                                  (Bitvector _ _ is_inc as l) r_bit =
-  let act_size = bvlength l * size in
-  let l' = to_num sign l in
-  let l_u = to_num false l in
-  let (n,nu,changed) = match r_bit with
-    | B1 -> (op l' 1, op l_u 1, true)
-    | B0 -> (l',l_u,false)
-    | BU -> 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
-  let one_larger = to_vec is_inc (act_size + 1,nu) in
-  let overflow =
-    if changed
-    then
-      if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
-      then B0 else B1
-    else B0 in
-  (correct_size_num,overflow,most_significant one_larger)
-
-(* add_overflow_vec_bit_signed
- * minus_overflow_vec_bit
- * minus_overflow_vec_bit_signed
- *)
-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_shift | RR_shift | LLL_shift
-
-let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) =
-  let n = natFromInteger n in
-  match op with
-  | LL_shift (*"<<"*) ->
-     Bitvector (shiftLeft bs n) start is_inc
-  | RR_shift (*">>"*) ->
-     Bitvector (shiftRight bs n) start is_inc
-  | LLL_shift (*"<<<"*) ->
-     Bitvector (rotateLeft n bs) start is_inc
-  end
-
-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 shiftl = bitwise_leftshift
-
-let rec arith_op_no0 (op : integer -> integer -> integer) l r =
-  if r = 0
-  then Nothing
-  else Just (op l r)
-(* TODO
-let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Bitvector _ start is_inc) as l) r =
-  let act_size = bvlength l * size in
-  let (l',r') = (to_num sign l,to_num sign r) in
-  let n = arith_op_no0 op l' r' in
-  let (representable,n') =
-    match n with
-    | Just n' ->
-      (n' <= get_max_representable_in sign act_size &&
-         n' >= get_min_representable_in sign act_size, n')
-    | _ -> (false,0)
-    end in
-  if representable
-  then to_vec is_inc (act_size,n')
-  else Vector (List.replicate (natFromInteger act_size) BU) start is_inc
-
-let mod_VVV = arith_op_vec_no0 hardware_mod false 1
-let quot_VVV = arith_op_vec_no0 hardware_quot false 1
-let quotS_VVV = arith_op_vec_no0 hardware_quot true 1
-
-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
-  let (l_u,r_u) = (to_num false l,to_num false r) in
-  let n = arith_op_no0 op l' r' in
-  let n_u = arith_op_no0 op l_u r_u in
-  let (representable,n',n_u') =
-    match (n, n_u) with
-    | (Just n',Just n_u') ->
-       ((n' <= get_max_representable_in sign rep_size &&
-           n' >= (get_min_representable_in sign rep_size)), n', n_u')
-    | _ -> (true,0,0)
-    end in
-  let (correct_size_num,one_more) =
-    if representable then
-      (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
-    else
-      (Vector (List.replicate (natFromInteger act_size) BU) start is_inc,
-       Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in
-  let overflow = if representable then B0 else B1 in
-  (correct_size_num,overflow,most_significant one_more)
-
-let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1
-let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1
-
-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 hardware_mod false 1
-*)
-val repeat : forall 'a. list 'a -> integer -> list 'a
-let rec repeat xs n =
-  if n = 0 then []
-  else xs ++ repeat xs (n-1)
-
-
-let duplicate (bit, length) =
-  vec_to_bvec (Vector (repeat [bit] length) (length - 1) false)
-
-let duplicate_to_list (bit, length) = repeat [bit] length
-
-let compare_op op (l,r) = (op l r)
-
-let lt = compare_op (<)
-let gt = compare_op (>)
-let lteq = compare_op (<=)
-let gteq = compare_op (>=)
-
-let compare_op_vec op sign (l,r) =
-  let (l',r') = (to_num sign l, to_num sign r) in
-  compare_op op (l',r')
-
-let lt_vec = compare_op_vec (<) true
-let gt_vec = compare_op_vec (>) true
-let lteq_vec = compare_op_vec (<=) true
-let gteq_vec = compare_op_vec (>=) true
-
-let lt_vec_signed = compare_op_vec (<) true
-let gt_vec_signed = compare_op_vec (>) true
-let lteq_vec_signed = compare_op_vec (<=) true
-let gteq_vec_signed = compare_op_vec (>=) true
-let lt_vec_unsigned = compare_op_vec (<) false
-let gt_vec_unsigned = compare_op_vec (>) false
-let lteq_vec_unsigned = compare_op_vec (<=) false
-let gteq_vec_unsigned = compare_op_vec (>=) false
-
-let lt_svec = lt_vec_signed
-
-let compare_op_vec_range op sign (l,r) =
-  compare_op op ((to_num sign l),r)
-
-let lt_vec_range = compare_op_vec_range (<) true
-let gt_vec_range = compare_op_vec_range (>) true
-let lteq_vec_range = compare_op_vec_range (<=) true
-let gteq_vec_range = compare_op_vec_range (>=) true
-
-let compare_op_range_vec op sign (l,r) =
-  compare_op op (l, (to_num sign r))
-
-let lt_range_vec = compare_op_range_vec (<) true
-let gt_range_vec = compare_op_range_vec (>) true
-let lteq_range_vec = compare_op_range_vec (<=) true
-let gteq_range_vec = compare_op_range_vec (>=) true
-
-val eq : forall 'a. Eq 'a => 'a * 'a -> bool
-let eq (l,r) = (l = r)
-let eq_range (l,r) = (l = r)
-
-val eq_vec : forall 'a. bitvector 'a * bitvector 'a -> bool
-let eq_vec (l,r) = (l = r)
-let eq_bit (l,r) = (l = r)
-let eq_vec_range (l,r) = eq (to_num false l,r)
-let eq_range_vec (l,r) = eq (l, to_num false r)
-let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
-
-let neq (l,r) = not (eq (l,r))
-let neq_bit (l,r) = not (eq_bit (l,r))
-let neq_range (l,r) = not (eq_range (l,r))
-let neq_vec (l,r) = not (eq_vec_vec (l,r))
-let neq_vec_range (l,r) = not (eq_vec_range (l,r))
-let neq_range_vec (l,r) = not (eq_range_vec (l,r))
-
-
-val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
-let make_indexed_vector entries default start length dir =
-  let length = natFromInteger length in
-  Vector (List.foldl replace (replicate length default) entries) start dir
-
-(*
-val make_bit_vector_undef : integer -> vector bitU
-let make_bitvector_undef length =
-  Vector (replicate (natFromInteger length) BU) 0 true
- *)
-
-(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
-
-(* TODO *)
-val mask : forall 'a 'b. Size 'b => bitvector 'a -> bitvector 'b
-let mask (Bitvector w i dir) = (Bitvector (zeroExtend w) i dir)
 
+(* Bytes and addresses *)
 
 val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
 let rec byte_chunks n list = match (n,list) with
@@ -885,11 +330,13 @@ type register =
   | RegisterPair of register * register
 
 type register_ref 'regstate 'a =
-  <| read_from : 'regstate -> 'a;
+  <| reg_name : string;
+     read_from : 'regstate -> 'a;
      write_to : 'regstate -> 'a -> 'regstate |>
 
 type field_ref 'regtype 'a =
-  <| get_field : 'regtype -> 'a;
+  <| field_name : string;
+     get_field : 'regtype -> 'a;
      set_field : 'regtype -> 'a -> 'regtype |>
 
 let name_of_reg = function
diff --git a/src/gen_lib/sail_values_word.lem b/src/gen_lib/sail_values_word.lem
deleted file mode 100644
index 048bf30a..00000000
--- a/src/gen_lib/sail_values_word.lem
+++ /dev/null
@@ -1,1030 +0,0 @@
-(* Version of sail_values.lem that uses Lem's machine words library *)
-
-open import Pervasives_extra
-open import Machine_word
-open import Sail_impl_base
-
-
-type ii = integer
-type nn = natural
-
-val pow : integer -> integer -> integer
-let pow m n = m ** (natFromInteger n)
-
-let rec replace bs ((n : integer),b') = match bs with
-  | [] -> []
-  | b :: bs ->
-     if n = 0 then b' :: bs
-              else b :: replace bs (n - 1,b')
-  end
-
-
-(*** Bits *)
-type bitU = B0 | B1 | BU
-
-let showBitU = function
-  | B0 -> "O"
-  | B1 -> "I"
-  | BU -> "U"
-end
-
-instance (Show bitU)
-  let show = showBitU
-end
-
-
-let bitU_to_bool = function
-  | B0 -> false
-  | B1  -> true
-  | BU -> failwith "to_bool applied to BU"
-  end
-
-let bit_lifted_of_bitU = function
-  | B0 -> Bitl_zero
-  | B1 -> Bitl_one
-  | BU -> Bitl_undef
-  end
-
-let bitU_of_bit = function
-  | Bitc_zero -> B0
-  | Bitc_one  -> B1
-  end
-
-let bit_of_bitU = function
-  | B0 -> Bitc_zero
-  | B1 -> Bitc_one
-  | BU -> failwith "bit_of_bitU: BU"
-  end
-
-let bitU_of_bit_lifted = function
-  | Bitl_zero -> B0
-  | Bitl_one  -> B1
-  | Bitl_undef -> BU
-  | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown"
-  end
-
-let bitwise_not_bit = function
-  | B1 -> B0
-  | B0 -> B1
-  | BU -> BU
-  end
-
-let inline (~) = bitwise_not_bit
-
-val is_one : integer -> bitU
-let is_one i =
-  if i = 1 then B1 else B0
-
-let bool_to_bitU b = if b then B1 else B0
-
-let bitwise_binop_bit op = function
-  | (BU,_) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
-  | (_,BU) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
-  | (x,y) -> bool_to_bitU (op (bitU_to_bool x) (bitU_to_bool y))
-  end
-
-val bitwise_and_bit : bitU * bitU -> bitU
-let bitwise_and_bit = bitwise_binop_bit (&&)
-
-val bitwise_or_bit : bitU * bitU -> bitU
-let bitwise_or_bit = bitwise_binop_bit (||)
-
-val bitwise_xor_bit : bitU * bitU -> bitU
-let bitwise_xor_bit = bitwise_binop_bit xor
-
-val (&.) : bitU -> bitU -> bitU
-let inline (&.) x y = bitwise_and_bit (x,y)
-
-val (|.) : bitU -> bitU -> bitU
-let inline (|.) x y = bitwise_or_bit (x,y)
-
-val (+.) : bitU -> bitU -> bitU
-let inline (+.) x y = bitwise_xor_bit (x,y)
-
-
-
-(*** Vectors *)
-
-(* element list * start * has increasing direction *)
-type vector 'a = Vector of list 'a * integer * bool
-
-let showVector (Vector elems start inc) =
-  "Vector " ^ show elems ^ " " ^ show start ^ " " ^ show inc
-
-let get_dir (Vector _ _ ord) = ord
-let get_start (Vector _ s _) = s
-let get_elems (Vector elems _ _) = elems
-let length (Vector bs _ _) = integerFromNat (length bs)
-
-instance forall 'a. Show 'a => (Show (vector 'a))
-  let show = showVector
-end
-
-let dir is_inc = if is_inc then D_increasing else D_decreasing
-let bool_of_dir = function
-  | D_increasing -> true
-  | D_decreasing -> false
-  end
-
-(*** Vector operations *)
-
-val set_vector_start : forall 'a. integer -> vector 'a -> vector 'a
-let set_vector_start new_start (Vector bs _ is_inc) =
-  Vector bs new_start is_inc
-
-let reset_vector_start v =
-  set_vector_start (if (get_dir v) then 0 else (length v - 1)) v
-
-let set_vector_start_to_length v =
-  set_vector_start (length v - 1) v
-
-let vector_concat (Vector bs start is_inc) (Vector bs' _ _) =
-  Vector (bs ++ bs') start is_inc
-
-let inline (^^) = vector_concat
-
-val sublist : forall 'a. list 'a -> (nat * nat) -> list 'a
-let sublist xs (i,j) =
-  let (toJ,_suffix) = List.splitAt (j+1) xs in
-  let (_prefix,fromItoJ) = List.splitAt i toJ in
-  fromItoJ
-
-val update_sublist : forall 'a. list 'a -> (nat * nat) -> list 'a -> list 'a
-let update_sublist xs (i,j) xs' =
-  let (toJ,suffix) = List.splitAt (j+1) xs in
-  let (prefix,_fromItoJ) = List.splitAt i toJ in
-  prefix ++ xs' ++ suffix
-
-val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a
-let slice (Vector bs start is_inc) i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let subvector_bits =
-    sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) in
-  Vector subvector_bits i is_inc
-
-(* this is for the vector slicing introduced in vector-concat patterns: i and j
-index into the "raw data", the list of bits. Therefore getting the bit list is
-easy, but the start index has to be transformed to match the old vector start
-and the direction. *)
-val slice_raw : forall 'a. vector 'a -> integer -> integer -> vector 'a
-let slice_raw (Vector bs start is_inc) i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let bits = sublist bs (iN,jN) in
-  let len = integerFromNat (List.length bits) in
-  Vector bits (if is_inc then 0 else len - 1) is_inc
-
-
-val update_aux : forall 'a. vector 'a -> integer -> integer -> list 'a -> vector 'a
-let update_aux (Vector bs start is_inc) i j bs' =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let bits =
-    (update_sublist bs)
-      (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) bs' in
-  Vector bits start is_inc
-
-val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector 'a
-let update v i j (Vector bs' _ _) =
-  update_aux v i j bs'
-
-val access : forall 'a. vector 'a -> integer -> 'a
-let access (Vector bs start is_inc) n =
-  if is_inc then List_extra.nth bs (natFromInteger (n - start))
-  else List_extra.nth bs (natFromInteger (start - n))
-
-val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a
-let update_pos v n b =
-  update_aux v n n [b]
-
-(*** Bitvectors *)
-
-(* element list * start * has increasing direction *)
-type bitvector 'a = Bitvector of mword 'a * integer * bool
-
-let showBitvector (Bitvector elems start inc) =
-  "Bitvector " ^ show elems ^ " " ^ show start ^ " " ^ show inc
-
-let bvget_dir (Bitvector _ _ ord) = ord
-let bvget_start (Bitvector _ s _) = s
-let bvget_elems (Bitvector elems _ _) = elems
-let bvlength (Bitvector bs _ _) = integerFromNat (word_length bs)
-
-instance forall 'a. Show 'a => (Show (bitvector 'a))
-  let show = showBitvector
-end
-
-(*** Vector operations *)
-
-val set_bitvector_start : forall 'a. integer -> bitvector 'a -> bitvector 'a
-let set_bitvector_start new_start (Bitvector bs _ is_inc) =
-  Bitvector bs new_start is_inc
-
-let reset_bitvector_start v =
-  set_bitvector_start (if (bvget_dir v) then 0 else (bvlength v - 1)) v
-
-let set_bitvector_start_to_length v =
-  set_bitvector_start (bvlength v - 1) v
-
-let bitvector_concat (Bitvector bs start is_inc) (Bitvector bs' _ _) =
-  Bitvector (word_concat bs bs') start is_inc
-
-let inline (^^^) = bitvector_concat
-
-val bvslice : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice (Bitvector bs start is_inc) i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
-  let subvector_bits = word_extract lo hi bs in
-  Bitvector subvector_bits i is_inc
-
-(* this is for the vector slicing introduced in vector-concat patterns: i and j
-index into the "raw data", the list of bits. Therefore getting the bit list is
-easy, but the start index has to be transformed to match the old vector start
-and the direction. *)
-val bvslice_raw : forall 'a 'b. Size 'b => bitvector 'a -> integer -> integer -> bitvector 'b
-let bvslice_raw (Bitvector bs start is_inc) i j =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let bits = word_extract iN jN bs in
-  let len = integerFromNat (word_length bits) in
-  Bitvector bits (if is_inc then 0 else len - 1) is_inc
-
-val bvupdate_aux : forall 'a 'b. bitvector 'a -> integer -> integer -> mword 'b -> bitvector 'a
-let bvupdate_aux (Bitvector bs start is_inc) i j bs' =
-  let iN = natFromInteger i in
-  let jN = natFromInteger j in
-  let startN = natFromInteger start in
-  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
-  let bits = word_update bs lo hi bs' in
-  Bitvector bits start is_inc
-
-val bvupdate : forall 'a. bitvector 'a -> integer -> integer -> bitvector 'a -> bitvector 'a
-let bvupdate v i j (Bitvector bs' _ _) =
-  bvupdate_aux v i j bs'
-
-(* TODO: decide between nat/natural, change either here or in machine_word *)
-val getBit' : forall 'a. mword 'a -> nat -> bool
-let getBit' w n = getBit w (naturalFromNat n)
-
-val bvaccess : forall 'a. bitvector 'a -> integer -> bool
-let bvaccess (Bitvector bs start is_inc) n =
-  if is_inc then getBit' bs (natFromInteger (n - start))
-  else getBit' bs (natFromInteger (start - n))
-
-val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bool -> bitvector 'a
-let bvupdate_pos v n b =
-  bvupdate_aux v n n (wordFromNatural (if b then 1 else 0))
-
-(*** Bit vector operations *)
-
-let extract_only_bit (Bitvector elems _ _) =
-  let l = word_length elems in
-  if l = 1 then
-    msb elems
-  else if l = 0 then
-    failwith "extract_single_bit called for empty vector"
-  else
-    failwith "extract_single_bit called for vector with more bits"
-
-let pp_bitu_vector (Vector elems start inc) =
-  let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
-  "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc
-
-
-let most_significant (Bitvector v _ _) =
-  if word_length v = 0 then
-    failwith "most_significant applied to empty vector"
-  else
-    msb v
-
-let bitwise_not_bitlist = List.map bitwise_not_bit
-
-let bitwise_not (Bitvector bs start is_inc) =
-  Bitvector (lNot bs) start is_inc
-
-let bitwise_binop op (Bitvector bsl start is_inc, Bitvector bsr _ _) =
-  Bitvector (op bsl bsr) start is_inc
-
-let bitwise_and = bitwise_binop lAnd
-let bitwise_or = bitwise_binop lOr
-let bitwise_xor = bitwise_binop lXor
-
-let unsigned (Bitvector bs _ _) : integer = unsignedIntegerFromWord bs
-let unsigned_big = unsigned
-
-let signed (Bitvector v _ _) : integer = signedIntegerFromWord v
-
-let hardware_mod (a: integer) (b:integer) : integer = 
- if a < 0 && b < 0
- then (abs a) mod (abs b)
- else if (a < 0 && b >= 0) 
- then (a mod b) - b
- else a mod b
-
-(* There are different possible answers for integer divide regarding
-rounding behaviour on negative operands. Positive operands always
-round down so derive the one we want (trucation towards zero) from
-that *)
-let hardware_quot (a:integer) (b:integer) : integer = 
-  let q = (abs a) / (abs b) in
-  if ((a<0) = (b<0)) then
-    q  (* same sign -- result positive *)
-  else
-    ~q (* different sign -- result negative *)
-
-let quot_signed = hardware_quot
-
-
-let signed_big = signed
-
-let to_num sign = if sign then signed else unsigned
-
-let max_64u = (integerPow 2 64) - 1
-let max_64  = (integerPow 2 63) - 1
-let min_64  = 0 - (integerPow 2 63)
-let max_32u = (4294967295 : integer)
-let max_32  = (2147483647 : integer)
-let min_32  = (0 - 2147483648 : integer)
-let max_8   = (127 : integer)
-let min_8   = (0 - 128 : integer)
-let max_5   = (31 : integer)
-let min_5   = (0 - 32 : integer)
-
-let get_max_representable_in sign (n : integer) : integer =
-  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
-  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
-  else if (n=8) then max_8
-  else if (n=5) then max_5
-  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
-                       | false -> integerPow 2 (natFromInteger n)
-       end
-
-let get_min_representable_in _ (n : integer) : integer =
-  if n = 64 then min_64
-  else if n = 32 then min_32
-  else if n = 8 then min_8
-  else if n = 5 then min_5
-  else 0 - (integerPow 2 (natFromInteger n))
-
-val to_bin_aux : natural -> list bitU
-let rec to_bin_aux x =
-  if x = 0 then []
-  else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
-let to_bin n = List.reverse (to_bin_aux n)
-
-val pad_zero : list bitU -> integer -> list bitU
-let rec pad_zero bits n =
-  if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
-
-
-let rec add_one_bit_ignore_overflow_aux bits = match bits with
-  | [] -> []
-  | B0 :: bits -> B1 :: bits
-  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
-  | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
-end
-
-let add_one_bit_ignore_overflow bits =
-  List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
-  
-let to_vec is_inc ((len : integer),(n : integer)) =
-  let start = if is_inc then 0 else len - 1 in
-  let bits = wordFromInteger n in
-  if integerFromNat (word_length bits) = len then
-    Bitvector bits start is_inc
-  else
-    failwith "Vector length mismatch in to_vec"
-
-let to_vec_big = to_vec
-
-let to_vec_inc = to_vec true
-let to_vec_dec = to_vec false
-(* TODO??
-let to_vec_undef is_inc (len : integer) =
-  Vector (replicate (natFromInteger len) BU) (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 exts (len, vec) = to_vec (bvget_dir vec) (len,signed vec)
-let extz (len, vec) = to_vec (bvget_dir vec) (len,unsigned vec)
-
-let exts_big (len, vec) = to_vec_big (bvget_dir vec) (len, signed_big vec)
-let extz_big (len, vec) = to_vec_big (bvget_dir vec) (len, unsigned_big vec)
-
-let add = integerAdd
-let add_signed = integerAdd
-let minus = integerMinus
-let multiply = integerMult
-let modulo = hardware_mod
-let quot = hardware_quot
-let power = integerPow
-
-(* TODO: this, and the definitions that use it, currently requires Size for
-   to_vec, which I'd rather avoid *)
-let arith_op_vec op sign (size : integer) (Bitvector _ _ 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 * (bvlength l),n)
-
-
-(* add_vec
- * add_vec_signed
- * minus_vec
- * multiply_vec
- * multiply_vec_signed
- *)
-let add_VVV = arith_op_vec integerAdd false 1
-let addS_VVV = arith_op_vec integerAdd true 1
-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
-
-val arith_op_vec_range : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'a
-let arith_op_vec_range op sign size (Bitvector _ _ is_inc as l) r =
-  arith_op_vec op sign size l (to_vec is_inc (bvlength l,r))
-
-(* add_vec_range
- * add_vec_range_signed
- * minus_vec_range
- * mult_vec_range
- * mult_vec_range_signed
- *)
-let add_VIV = arith_op_vec_range integerAdd false 1
-let addS_VIV = arith_op_vec_range integerAdd true 1
-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
-
-val arith_op_range_vec : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'a
-let arith_op_range_vec op sign size l (Bitvector _ _ is_inc as r) =
-  arith_op_vec op sign size (to_vec is_inc (bvlength r, l)) r
-
-(* add_range_vec
- * add_range_vec_signed
- * minus_range_vec
- * mult_range_vec
- * mult_range_vec_signed
- *)
-let add_IVV = arith_op_range_vec integerAdd false 1
-let addS_IVV = arith_op_range_vec integerAdd true 1
-let minus_IVV = arith_op_range_vec integerMinus false 1
-let mult_IVV = arith_op_range_vec integerMult false 2
-let multS_IVV = arith_op_range_vec integerMult true 2
-
-let arith_op_range_vec_range op sign l r = op l (to_num sign r)
-
-(* add_range_vec_range
- * add_range_vec_range_signed
- * minus_range_vec_range
- *)
-let add_IVI = arith_op_range_vec_range integerAdd false
-let addS_IVI = arith_op_range_vec_range integerAdd true
-let minus_IVI = arith_op_range_vec_range integerMinus false
-
-let arith_op_vec_range_range op sign l r = op (to_num sign l) r
-
-(* add_vec_range_range
- * add_vec_range_range_signed
- * minus_vec_range_range
- *)
-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 l r =
-  let (l',r') = (to_num sign l,to_num sign r) in
-  op l' r'
-
-(* add_vec_vec_range
- * add_vec_vec_range_signed
- *)
-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) (Bitvector _ _ is_inc as l)r =
-  let l' = to_num sign l in
-  let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
-  to_vec is_inc (bvlength l * size,n)
-
-(* add_vec_bit
- * add_vec_bit_signed
- * minus_vec_bit_signed
- *)
-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
-
-val arith_op_overflow_vec : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'a * bitU * bool
-let rec arith_op_overflow_vec op sign size (Bitvector _ _ is_inc as l) r =
-  let len = bvlength l in
-  let act_size = len * size in
-  let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
-  let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
-  let n = op l_sign r_sign in
-  let n_unsign = op l_unsign r_unsign in
-  let correct_size_num = to_vec is_inc (act_size,n) in
-  let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in
-  let overflow =
-    if n <= get_max_representable_in sign len &&
-         n >= get_min_representable_in sign len
-    then B0 else B1 in
-  let c_out = most_significant one_more_size_u in
-  (correct_size_num,overflow,c_out)
-
-(* add_overflow_vec
- * add_overflow_vec_signed
- * minus_overflow_vec
- * minus_overflow_vec_signed
- * mult_overflow_vec
- * mult_overflow_vec_signed
- *)
-let addO_VVV = arith_op_overflow_vec integerAdd false 1
-let addSO_VVV = arith_op_overflow_vec integerAdd true 1
-let minusO_VVV = arith_op_overflow_vec integerMinus false 1
-let minusSO_VVV = arith_op_overflow_vec integerMinus true 1
-let multO_VVV = arith_op_overflow_vec integerMult false 2
-let multSO_VVV = arith_op_overflow_vec integerMult true 2
-
-val arith_op_overflow_vec_bit : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer ->
-                                bitvector 'a -> bitU -> bitvector 'a * bitU * bool
-let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer)
-                                  (Bitvector _ _ is_inc as l) r_bit =
-  let act_size = bvlength l * size in
-  let l' = to_num sign l in
-  let l_u = to_num false l in
-  let (n,nu,changed) = match r_bit with
-    | B1 -> (op l' 1, op l_u 1, true)
-    | B0 -> (l',l_u,false)
-    | BU -> 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
-  let one_larger = to_vec is_inc (act_size + 1,nu) in
-  let overflow =
-    if changed
-    then
-      if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
-      then B0 else B1
-    else B0 in
-  (correct_size_num,overflow,most_significant one_larger)
-
-(* add_overflow_vec_bit_signed
- * minus_overflow_vec_bit
- * minus_overflow_vec_bit_signed
- *)
-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_shift | RR_shift | LLL_shift
-
-let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) =
-  let n = natFromInteger n in
-  match op with
-  | LL_shift (*"<<"*) ->
-     Bitvector (shiftLeft bs (naturalFromNat n)) start is_inc
-  | RR_shift (*">>"*) ->
-     Bitvector (shiftRight bs (naturalFromNat n)) start is_inc
-  | LLL_shift (*"<<<"*) ->
-     Bitvector (rotateLeft (naturalFromNat n) bs) start is_inc
-  end
-
-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)
-(* TODO
-let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Bitvector _ start is_inc) as l) r =
-  let act_size = bvlength l * size in
-  let (l',r') = (to_num sign l,to_num sign r) in
-  let n = arith_op_no0 op l' r' in
-  let (representable,n') =
-    match n with
-    | Just n' ->
-      (n' <= get_max_representable_in sign act_size &&
-         n' >= get_min_representable_in sign act_size, n')
-    | _ -> (false,0)
-    end in
-  if representable
-  then to_vec is_inc (act_size,n')
-  else Vector (List.replicate (natFromInteger act_size) BU) start is_inc
-
-let mod_VVV = arith_op_vec_no0 hardware_mod false 1
-let quot_VVV = arith_op_vec_no0 hardware_quot false 1
-let quotS_VVV = arith_op_vec_no0 hardware_quot true 1
-
-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
-  let (l_u,r_u) = (to_num false l,to_num false r) in
-  let n = arith_op_no0 op l' r' in
-  let n_u = arith_op_no0 op l_u r_u in
-  let (representable,n',n_u') =
-    match (n, n_u) with
-    | (Just n',Just n_u') ->
-       ((n' <= get_max_representable_in sign rep_size &&
-           n' >= (get_min_representable_in sign rep_size)), n', n_u')
-    | _ -> (true,0,0)
-    end in
-  let (correct_size_num,one_more) =
-    if representable then
-      (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
-    else
-      (Vector (List.replicate (natFromInteger act_size) BU) start is_inc,
-       Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in
-  let overflow = if representable then B0 else B1 in
-  (correct_size_num,overflow,most_significant one_more)
-
-let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1
-let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1
-
-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 hardware_mod false 1
-*)
-val repeat : forall 'a. list 'a -> integer -> list 'a
-let rec repeat xs n =
-  if n = 0 then []
-  else xs ++ repeat xs (n-1)
-
-(*
-let duplicate bit length =
-  Vector (repeat [bit] length) (if dir then 0 else length - 1) dir
- *)
-
-let compare_op op (l,r) = bool_to_bitU (op l r)
-
-let lt = compare_op (<)
-let gt = compare_op (>)
-let lteq = compare_op (<=)
-let gteq = compare_op (>=)
-
-
-let compare_op_vec op sign (l,r) =
-  let (l',r') = (to_num sign l, to_num sign r) in
-  compare_op op (l',r')
-
-let lt_vec = compare_op_vec (<) true
-let gt_vec = compare_op_vec (>) true
-let lteq_vec = compare_op_vec (<=) true
-let gteq_vec = compare_op_vec (>=) true
-
-let lt_vec_signed = compare_op_vec (<) true
-let gt_vec_signed = compare_op_vec (>) true
-let lteq_vec_signed = compare_op_vec (<=) true
-let gteq_vec_signed = compare_op_vec (>=) true
-let lt_vec_unsigned = compare_op_vec (<) false
-let gt_vec_unsigned = compare_op_vec (>) false
-let lteq_vec_unsigned = compare_op_vec (<=) false
-let gteq_vec_unsigned = compare_op_vec (>=) false
-
-let compare_op_vec_range op sign (l,r) =
-  compare_op op ((to_num sign l),r)
-
-let lt_vec_range = compare_op_vec_range (<) true
-let gt_vec_range = compare_op_vec_range (>) true
-let lteq_vec_range = compare_op_vec_range (<=) true
-let gteq_vec_range = compare_op_vec_range (>=) true
-
-let compare_op_range_vec op sign (l,r) =
-  compare_op op (l, (to_num sign r))
-
-let lt_range_vec = compare_op_range_vec (<) true
-let gt_range_vec = compare_op_range_vec (>) true
-let lteq_range_vec = compare_op_range_vec (<=) true
-let gteq_range_vec = compare_op_range_vec (>=) true
-
-let eq (l,r) = bool_to_bitU (l = r)
-let eq_range (l,r) = bool_to_bitU (l = r)
-let eq_vec (l,r) = bool_to_bitU (l = r)
-let eq_bit (l,r) = bool_to_bitU (l = r)
-let eq_vec_range (l,r) = eq (to_num false l,r)
-let eq_range_vec (l,r) = eq (l, to_num false r)
-let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
-
-let neq (l,r) = bitwise_not_bit (eq (l,r))
-let neq_bit (l,r) = bitwise_not_bit (eq_bit (l,r))
-let neq_range (l,r) = bitwise_not_bit (eq_range (l,r))
-let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r))
-let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r))
-let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r))
-
-
-val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
-let make_indexed_vector entries default start length dir =
-  let length = natFromInteger length in
-  Vector (List.foldl replace (replicate length default) entries) start dir
-
-(*
-val make_bit_vector_undef : integer -> vector bitU
-let make_bitvector_undef length =
-  Vector (replicate (natFromInteger length) BU) 0 true
- *)
-
-(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
-
-let mask (n,Vector bits start dir) =
-  let current_size = List.length bits in
-  Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir
-
-
-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 bitv_of_byte_lifteds : bool -> list Sail_impl_base.byte_lifted -> vector bitU
-let bitv_of_byte_lifteds dir v =
-  let bits = foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v in
-  let len = integerFromNat (List.length bits) in
-  Vector bits (if dir then 0 else len - 1) dir
-
-val bitv_of_bytes : bool -> list Sail_impl_base.byte -> vector bitU
-let bitv_of_bytes dir v =
-  let bits = foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v in
-  let len = integerFromNat (List.length bits) in
-  Vector bits (if dir then 0 else len - 1) dir
-
-
-val byte_lifteds_of_bitv : vector bitU -> list byte_lifted
-let byte_lifteds_of_bitv (Vector bits length is_inc) =
-  let bits = List.map bit_lifted_of_bitU bits in
-  byte_lifteds_of_bit_lifteds bits
-
-val bytes_of_bitv : vector bitU -> list byte
-let bytes_of_bitv (Vector bits length is_inc) =
-  let bits = List.map bit_of_bitU bits in
-  bytes_of_bits bits
-
-val bit_lifteds_of_bitUs : list bitU -> list bit_lifted
-let bit_lifteds_of_bitUs bits = List.map bit_lifted_of_bitU bits
-
-val bit_lifteds_of_bitv : vector bitU -> list bit_lifted
-let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs (get_elems v)
-
-
-val address_lifted_of_bitv : vector bitU -> address_lifted
-let address_lifted_of_bitv v =
-  let byte_lifteds = byte_lifteds_of_bitv v in
-  let maybe_address_integer =
-    match (maybe_all (List.map byte_of_byte_lifted byte_lifteds)) with
-    | Just bs -> Just (integer_of_byte_list bs)
-    | _ -> Nothing
-    end in
-  Address_lifted byte_lifteds maybe_address_integer
-
-val address_of_bitv : vector bitU -> address
-let address_of_bitv v =
-  let bytes = bytes_of_bitv v in
-  address_of_byte_list bytes
-
-
-
-(*** Registers *)
-
-type register_field = string
-type register_field_index = string * (integer * integer) (* name, start and end *)
-
-type register =
-  | Register of string * (* name *)
-                integer * (* length *)
-                integer * (* start index *)
-                bool * (* is increasing *)
-                  list register_field_index
-  | UndefinedRegister of integer (* length *)
-  | RegisterPair of register * register
-
-let name_of_reg = function
-  | Register name _ _ _ _ -> name
-  | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister"
-  | RegisterPair _ _ -> failwith "name_of_reg RegisterPair"
-end
-
-let size_of_reg = function
-  | Register _ size _ _ _ -> size
-  | UndefinedRegister size -> size
-  | RegisterPair _ _ -> failwith "size_of_reg RegisterPair"
-end
-                              
-let start_of_reg = function
-  | Register _ _ start _ _ -> start
-  | UndefinedRegister _ -> failwith "start_of_reg UndefinedRegister"
-  | RegisterPair _ _ -> failwith "start_of_reg RegisterPair"
-end
-
-let is_inc_of_reg = function
-  | Register _ _ _ is_inc _ -> is_inc
-  | UndefinedRegister _ -> failwith "is_inc_of_reg UndefinedRegister"
-  | RegisterPair _ _ -> failwith "in_inc_of_reg RegisterPair"
-end
-
-let dir_of_reg = function
-  | Register _ _ _ is_inc _ -> dir is_inc
-  | UndefinedRegister _ -> failwith "dir_of_reg UndefinedRegister"
-  | RegisterPair _ _ -> failwith "dir_of_reg RegisterPair"
-end
-
-let size_of_reg_nat reg = natFromInteger (size_of_reg reg)
-let start_of_reg_nat reg = natFromInteger (start_of_reg reg)
-
-val register_field_indices_aux : register -> register_field -> maybe (integer * integer)
-let rec register_field_indices_aux register rfield =
-  match register with
-  | Register _ _ _ _ rfields -> List.lookup rfield rfields
-  | RegisterPair r1 r2 ->
-      let m_indices = register_field_indices_aux r1 rfield in
-      if isJust m_indices then m_indices else register_field_indices_aux r2 rfield
-  | UndefinedRegister _ -> Nothing
-  end
-
-val register_field_indices : register -> register_field -> integer * integer
-let register_field_indices register rfield =
-  match register_field_indices_aux register rfield with
-  | Just indices -> indices
-  | Nothing -> failwith "Invalid register/register-field combination"
-  end
-
-let register_field_indices_nat reg regfield=
-  let (i,j) = register_field_indices reg regfield in
-  (natFromInteger i,natFromInteger j)
-
-let rec external_reg_value reg_name v = 
-  let (internal_start, external_start, direction) =
-    match reg_name with 
-     | Reg _ start size dir ->
-        (start, (if dir = D_increasing then start else (start - (size +1))), dir)
-     | Reg_slice _ reg_start dir (slice_start, slice_end) ->
-        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
-         slice_start, dir)
-     | Reg_field _ reg_start dir _ (slice_start, slice_end) ->
-        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
-         slice_start, dir)
-     | Reg_f_slice _ reg_start dir _ _ (slice_start, slice_end) ->
-        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
-         slice_start, dir) 
-     end in
-  let bits = bit_lifteds_of_bitv v in
-  <| rv_bits           = bits; 
-     rv_dir            = direction;
-     rv_start          = external_start;
-     rv_start_internal = internal_start |>
-
-val internal_reg_value : register_value -> vector bitU
-let internal_reg_value v =
-  Vector (List.map bitU_of_bit_lifted v.rv_bits)
-         (integerFromNat v.rv_start_internal)
-         (v.rv_dir = D_increasing)
-
-
-let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
-  match d with
-  (*This is the case the thread/concurrecny model expects, so no change needed*)
-  | D_increasing -> (i,j)
-  | D_decreasing -> let slice_i = start - i in 
-                    let slice_j = (i - j) + slice_i in
-                    (slice_i,slice_j)
-  end 
-
-let external_reg_whole reg =
-  Reg (name_of_reg reg) (start_of_reg_nat reg) (size_of_reg_nat reg) (dir_of_reg reg)
-      
-let external_reg_slice reg (i,j) =
-  let start = start_of_reg_nat reg in
-  let dir = dir_of_reg reg in
-  Reg_slice (name_of_reg reg) start dir (external_slice dir start (i,j))
-
-let external_reg_field_whole reg rfield = 
-  let (m,n) = register_field_indices_nat reg rfield in
-  let start = start_of_reg_nat reg in
-  let dir = dir_of_reg reg in
-  Reg_field (name_of_reg reg) start dir rfield (external_slice dir start (m,n))
-            
-let external_reg_field_slice reg rfield (i,j) = 
-  let (m,n) = register_field_indices_nat reg rfield in
-  let start = start_of_reg_nat reg in
-  let dir = dir_of_reg reg in
-  Reg_f_slice (name_of_reg reg) start dir rfield
-              (external_slice dir start (m,n))
-              (external_slice dir start (i,j))
-
-let external_mem_value v =
-  byte_lifteds_of_bitv v $> List.reverse
-
-let internal_mem_value direction bytes =
-  List.reverse bytes $> bitv_of_byte_lifteds direction
-
-
-
-                       
-
-val foreach_inc :  forall 'vars. (integer * integer * integer) -> 'vars ->
-                   (integer -> 'vars -> 'vars) -> '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) -> 'vars ->
-                  (integer -> 'vars -> 'vars) -> '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
-
-let assert' b msg_opt =
-  let msg = match msg_opt with
-  | Just msg -> msg
-  | Nothing  -> "unspecified error"
-  end in
-  if bitU_to_bool b then () else failwith msg
-
-(* convert numbers unsafely to naturals *)
-
-class (ToNatural 'a) val toNatural : 'a -> natural end
-(* eta-expanded for Isabelle output, otherwise it breaks *)
-instance (ToNatural integer) let toNatural = (fun n -> naturalFromInteger n) end
-instance (ToNatural int)     let toNatural = (fun n -> naturalFromInt n)     end
-instance (ToNatural nat)     let toNatural = (fun n -> naturalFromNat n)     end
-instance (ToNatural natural) let toNatural = (fun n -> n)                    end
-
-let toNaturalFiveTup (n1,n2,n3,n4,n5) =
-  (toNatural n1,
-   toNatural n2,
-   toNatural n3,
-   toNatural n4,
-   toNatural n5)
-
-
-type regfp =
-  | RFull of (string)
-  | RSlice of (string * integer * integer)
-  | RSliceBit of (string * integer)
-  | RField of (string * string)
-
-type niafp = 
-  | NIAFP_successor
-  | NIAFP_concrete_address of vector bitU
-  | NIAFP_LR
-  | NIAFP_CTR
-  | NIAFP_register of regfp
-
-(* only for MIPS *)
-type diafp = 
-  | DIAFP_none
-  | DIAFP_concrete of vector bitU
-  | DIAFP_reg of regfp
-
-let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function
-  | RFull name -> 
-     let (start,length,direction,_) = reg_info name Nothing in
-     Reg name start length direction
-  | RSlice (name,i,j) ->
-     let i = natFromInteger i in
-     let j = natFromInteger j in
-     let (start,length,direction,_) = reg_info name Nothing in
-     let slice = external_slice direction start (i,j) in
-     Reg_slice name start direction slice
-  | RSliceBit (name,i) ->
-     let i = natFromInteger i in
-     let (start,length,direction,_) = reg_info name Nothing in
-     let slice = external_slice direction start (i,i) in
-     Reg_slice name start direction slice
-  | RField (name,field_name) ->
-     let (start,length,direction,span) = reg_info name (Just field_name) in
-     let slice = external_slice direction start span in
-     Reg_field name start direction field_name slice
-end
-
-let niafp_to_nia reginfo = function
-  | NIAFP_successor -> NIA_successor
-  | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v)
-  | NIAFP_LR -> NIA_LR
-  | NIAFP_CTR -> NIA_CTR
-  | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r)
-end
-
-let diafp_to_dia reginfo = function
-  | DIAFP_none -> DIA_none
-  | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v)
-  | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r)
-end
-
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 3cbcd4c8..4543bbcf 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,6 +1,7 @@
 open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
+open import Sail_operators_mwords
 
 (* 'a is result type *)
 
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 0cdeb414..167e7de9 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -779,32 +779,35 @@ end
 
 (* the address_lifted types should go away here and be replaced by address *)
 type with_aux 'o = 'o * maybe ((unit -> (string * string)) * ((list (reg_name * register_value)) -> list event))
-type outcome 'a =
+type outcome_r 'a 'r =
   (* Request to read memory, value is location to read, integer is size to read,
      followed by registers that were used in computing that size *)
-  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome 'a))
+  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome_r 'a 'r))
   (* Tell the system a write is imminent, at address lifted, of size nat *)
-  | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome 'a))
+  | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome_r 'a 'r))
   (* Request the result of store-exclusive *)
-  | Excl_res of (bool -> with_aux (outcome 'a))
+  | Excl_res of (bool -> with_aux (outcome_r 'a 'r))
   (* Request to write memory at last signalled address. Memory value should be 8
      times the size given in ea signal *)
-  | Write_memv of memory_value * (bool -> with_aux (outcome 'a))
+  | Write_memv of memory_value * (bool -> with_aux (outcome_r 'a 'r))
   (* Request a memory barrier *)
-  | Barrier of barrier_kind * with_aux (outcome 'a)
+  | Barrier of barrier_kind * with_aux (outcome_r 'a 'r)
   (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint of with_aux (outcome 'a)
+  | Footprint of with_aux (outcome_r 'a 'r)
   (* Request to read register, will track dependency when mode.track_values *)
-  | Read_reg of reg_name * (register_value -> with_aux (outcome 'a))
+  | Read_reg of reg_name * (register_value -> with_aux (outcome_r 'a 'r))
   (* Request to write register *)
-  | Write_reg of (reg_name * register_value) * with_aux (outcome 'a)
+  | Write_reg of (reg_name * register_value) * with_aux (outcome_r 'a 'r)
   | Escape of maybe string
   (*Result of a failed assert with possible error message to report*)
   | Fail of maybe string
-  | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome 'a)
+  (* Early return with value of type 'r *)
+  | Return of 'r
+  | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome_r 'a 'r)
   | Done of 'a
   | Error of string
 
+type outcome 'a = outcome_r 'a unit
 type outcome_s 'a = with_aux (outcome 'a)
 (* first string : output of instruction_stack_to_string
    second string: output of local_variables_to_string *)
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index 37de5241..835d4648 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -52,4 +52,4 @@ val pat_to_string : 'a pat -> string
 val pp_lem_defs : Format.formatter -> tannot defs -> unit
 
 val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit
-val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit
+val pp_defs_lem : bool -> bool -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 2971081e..7671c26b 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -148,44 +148,47 @@ let doc_nexp_lem (Nexp_aux (nexp, l) as full_nexp) = match nexp with
 
 let doc_typ_lem, doc_atomic_typ_lem =
   (* following the structure of parser for precedence *)
-  let rec typ regtypes ty = fn_typ regtypes true ty
-    and typ' regtypes ty = fn_typ regtypes false ty
-    and fn_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+  let rec typ sequential mwords ty = fn_typ sequential mwords true ty
+    and typ' sequential mwords ty = fn_typ sequential mwords false ty
+    and fn_typ (sequential : bool) (mwords : bool) atyp_needed ((Typ_aux (t, _)) as ty) = match t with
       | Typ_fn(arg,ret,efct) ->
          (*let exc_typ = string "string" in*)
          let ret_typ =
            if effectful efct
-           then separate space [string "M";(*parens exc_typ;*) fn_typ regtypes true ret]
-           else separate space [fn_typ regtypes false ret] in
-         let tpp = separate space [tup_typ regtypes true arg; arrow;ret_typ] in
+           then separate space [string "M";(*parens exc_typ;*) fn_typ sequential mwords true ret]
+           else separate space [fn_typ sequential mwords false ret] in
+         let tpp = separate space [tup_typ sequential mwords true 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 regtypes atyp_needed ty
-    and tup_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+      | _ -> tup_typ sequential mwords atyp_needed ty
+    and tup_typ sequential mwords atyp_needed ((Typ_aux (t, _)) as ty) = match t with
       | Typ_tup typs ->
-         let tpp = separate_map (space ^^ star ^^ space) (app_typ regtypes false) typs in
+         let tpp = separate_map (space ^^ star ^^ space) (app_typ sequential mwords false) typs in
          if atyp_needed then parens tpp else tpp
-      | _ -> app_typ regtypes atyp_needed ty
-    and app_typ regtypes atyp_needed ((Typ_aux (t, l)) as ty) = match t with
+      | _ -> app_typ sequential mwords atyp_needed ty
+    and app_typ sequential mwords atyp_needed ((Typ_aux (t, l)) 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 elem_typ, _)]) ->
          let tpp = match elem_typ with
-           | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) ->
+           | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) when mwords ->
              string "bitvector " ^^ doc_nexp_lem (simplify_nexp m)
              (* (match simplify_nexp m with
                | (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i
                | (Nexp_aux(Nexp_var _, _)) -> separate space [string "bitvector"; doc_nexp m]
                | _ -> raise (Reporting_basic.err_unreachable l
                  "cannot pretty-print bitvector type with non-constant length")) *)
-           | _ -> string "vector" ^^ space ^^ typ regtypes elem_typ in
+           | _ -> string "vector" ^^ space ^^ typ sequential mwords elem_typ in
          if atyp_needed then parens tpp else tpp
       | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
          (* TODO: Better distinguish register names and contents? *)
          (* fn_typ regtypes atyp_needed etyp *)
-         let tpp = (string "register_ref regstate " ^^ typ regtypes etyp) in
+         let tpp =
+           if sequential
+           then string "register_ref regstate " ^^ typ sequential mwords etyp
+           else string "register" in
          if atyp_needed then parens tpp else tpp
       | Typ_app(Id_aux (Id "range", _),_) ->
          (string "integer")
@@ -194,10 +197,10 @@ let doc_typ_lem, doc_atomic_typ_lem =
       | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
          (string "integer")
       | Typ_app(id,args) ->
-         let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem regtypes) args) in
+         let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem sequential mwords) args) in
          if atyp_needed then parens tpp else tpp
-      | _ -> atomic_typ regtypes atyp_needed ty
-    and atomic_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+      | _ -> atomic_typ sequential mwords atyp_needed ty
+    and atomic_typ sequential mwords atyp_needed ((Typ_aux (t, _)) as ty) = match t with
       | Typ_id (Id_aux (Id "bool",_)) -> string "bool"
       | Typ_id (Id_aux (Id "boolean",_)) -> string "bool"
       | Typ_id (Id_aux (Id "bit",_)) -> string "bitU"
@@ -210,10 +213,10 @@ let doc_typ_lem, doc_atomic_typ_lem =
       | 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
+         let tpp = typ sequential mwords 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 regtypes true t
+    and doc_typ_arg_lem sequential mwords (Typ_arg_aux(t,_)) = match t with
+      | Typ_arg_typ t -> app_typ sequential mwords true t
       | Typ_arg_nexp n -> doc_nexp_lem (simplify_nexp n)
       | Typ_arg_order o -> empty
   in typ', atomic_typ
@@ -240,17 +243,17 @@ and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with
   | Typ_arg_nexp nexp -> not (is_nexp_constant (simplify_nexp nexp))
   | _ -> false
 
-let doc_tannot_lem regtypes eff typ =
+let doc_tannot_lem sequential mwords eff typ =
   (* if contains_t_pp_var typ then empty
   else *)
-    let ta = doc_typ_lem regtypes typ in
+    let ta = doc_typ_lem sequential mwords typ in
     if eff then string " : _M " ^^ parens ta
     else string " : " ^^ ta
 
 (* 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 regtypes in_pat (L_aux(lit,l)) a =
+let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a =
   match lit with
   | L_unit  -> utf8string "()"
   | L_zero  -> utf8string "B0"
@@ -275,7 +278,7 @@ let doc_lit_lem regtypes in_pat (L_aux(lit,l)) a =
           | _ ->
             parens
               ((utf8string "(failwith \"undefined value of unsupported type\")") ^^
-              (doc_tannot_lem regtypes false typ)))
+              (doc_tannot_lem sequential mwords false typ)))
        | _ -> utf8string "(failwith \"undefined value of unsupported type\")")
   | L_string s -> utf8string ("\"" ^ s ^ "\"")
   | L_real s -> utf8string s (* TODO What's the Lem syntax for reals? *)
@@ -295,9 +298,9 @@ let doc_typquant_lem (TypQ_aux(tq,_)) typ = match tq with
   string "forall " ^^ separate_map space doc_quant_item qs ^^ string ". " ^^ typ
 | _ -> empty
 
-let doc_typschm_lem regtypes quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
-  if quants then (doc_typquant_lem tq (doc_typ_lem regtypes t))
-  else doc_typ_lem regtypes t
+let doc_typschm_lem sequential mwords quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
+  if quants then (doc_typquant_lem tq (doc_typ_lem sequential mwords t))
+  else doc_typ_lem sequential mwords t
 
 let is_ctor env id = match Env.lookup_id id env with
 | Enum _ | Union _ -> true
@@ -306,37 +309,37 @@ let is_ctor env id = match Env.lookup_id id env with
 (*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 regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p with
+let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) = match p with
   | P_app(id, ((_ :: _) as pats)) ->
     let ppp = doc_unop (doc_id_lem_ctor id)
-                       (parens (separate_map comma (doc_pat_lem regtypes true) pats)) in
+                       (parens (separate_map comma (doc_pat_lem sequential mwords true) pats)) in
     if apat_needed then parens ppp else ppp
   | P_app(id,[]) -> doc_id_lem_ctor id
-  | P_lit lit  -> doc_lit_lem regtypes true lit annot
+  | P_lit lit  -> doc_lit_lem sequential mwords true lit annot
   | P_wild -> underscore
   | P_id id ->
      begin match id with
      | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
      | _ -> doc_id_lem id end
-  | P_as(p,id) -> parens (separate space [doc_pat_lem regtypes true p; string "as"; doc_id_lem id])
+  | P_as(p,id) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_id_lem id])
   | P_typ(typ,p) ->
-    let doc_p = doc_pat_lem regtypes true p in
+    let doc_p = doc_pat_lem sequential mwords true p in
     if contains_t_pp_var typ then doc_p
-    else parens (doc_op colon doc_p (doc_typ_lem regtypes typ))
+    else parens (doc_op colon doc_p (doc_typ_lem sequential mwords typ))
   | P_vector pats ->
      let ppp =
        (separate space)
-         [string "Vector";brackets (separate_map semi (doc_pat_lem regtypes true) pats);underscore;underscore] in
+         [string "Vector";brackets (separate_map semi (doc_pat_lem sequential mwords true) pats);underscore;underscore] in
      if apat_needed then parens ppp else ppp
   | P_vector_concat pats ->
      raise (Reporting_basic.err_unreachable l
        "vector concatenation patterns should have been removed before pretty-printing")
   | P_tup pats  ->
      (match pats with
-      | [p] -> doc_pat_lem regtypes apat_needed p
-      | _ -> parens (separate_map comma_sp (doc_pat_lem regtypes false) pats))
-  | P_list pats -> brackets (separate_map semi (doc_pat_lem regtypes false) pats) (*Never seen but easy in lem*)
-  | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem regtypes true p) (doc_pat_lem regtypes true p')
+      | [p] -> doc_pat_lem sequential mwords apat_needed p
+      | _ -> parens (separate_map comma_sp (doc_pat_lem sequential mwords false) pats))
+  | P_list pats -> brackets (separate_map semi (doc_pat_lem sequential mwords false) pats) (*Never seen but easy in lem*)
+  | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem sequential mwords true p) (doc_pat_lem sequential mwords true p')
   | P_record (_,_) | P_vector_indexed _ -> empty (* TODO *)
 
 let rec contains_bitvector_typ (Typ_aux (t,_) as typ) = match t with
@@ -363,11 +366,11 @@ let typ_id_of (Typ_aux (typ, l)) = match typ with
 let prefix_recordtype = true
 let report = Reporting_basic.err_unreachable
 let doc_exp_lem, doc_let_lem =
-  let rec top_exp regtypes (early_ret : bool) (aexp_needed : bool)
+  let rec top_exp sequential mwords (early_ret : bool) (aexp_needed : bool)
     (E_aux (e, (l,annot)) as full_exp) =
-    let expY = top_exp regtypes early_ret true in
-    let expN = top_exp regtypes early_ret false in
-    let expV = top_exp regtypes early_ret in
+    let expY = top_exp sequential mwords early_ret true in
+    let expN = top_exp sequential mwords early_ret false in
+    let expV = top_exp sequential mwords early_ret in
     let liftR doc =
       if early_ret && effectful (effect_of full_exp)
       then separate space [string "liftR"; parens (doc)]
@@ -389,12 +392,12 @@ let doc_exp_lem, doc_let_lem =
                    doc_id_lem id in
                  liftR ((prefix 2 1)
                    (string "write_reg_field_range")
-                   (align (doc_lexp_deref_lem regtypes early_ret le ^^ space^^
+                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space^^
                              field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
             | _ ->
                liftR ((prefix 2 1)
                  (string "write_reg_range")
-                 (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e)))
+                 (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e)))
            )
         | LEXP_vector (le,e2) when is_bit_typ t ->
            (match le with
@@ -408,16 +411,16 @@ let doc_exp_lem, doc_let_lem =
                    doc_id_lem id in
                  liftR ((prefix 2 1)
                    (string "write_reg_field_bit")
-                   (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ field_ref ^/^ expY e2 ^/^ expY e)))
+                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ field_ref ^/^ expY e2 ^/^ expY e)))
             | _ ->
                liftR ((prefix 2 1)
                  (string "write_reg_bit")
-                 (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ expY e2 ^/^ expY e))
+                 (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e))
            )
         (* | LEXP_field (le,id) when is_bit_typ t ->
            liftR ((prefix 2 1)
              (string "write_reg_bitfield")
-             (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)) *)
+             (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)) *)
         | LEXP_field ((LEXP_aux (_, lannot) as le),id) ->
           let field_ref =
             doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^
@@ -425,7 +428,7 @@ let doc_exp_lem, doc_let_lem =
             doc_id_lem id in
            liftR ((prefix 2 1)
              (string "write_reg_field")
-             (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^
+             (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
                 field_ref ^/^ expY e))
         (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info ->
            (match alias_info with
@@ -441,15 +444,15 @@ let doc_exp_lem, doc_let_lem =
                string "write_two_regs" ^^ space ^^ string reg1 ^^ space ^^
                  string reg2 ^^ space ^^ expY e) *)
         | _ ->
-           liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem regtypes early_ret le ^/^ expY e)))
+           liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem sequential mwords early_ret le ^/^ expY e)))
     | E_vector_append(le,re) ->
       raise (Reporting_basic.err_unreachable l
-        "E_vector_access should have been rewritten before pretty-printing")
+        "E_vector_append should have been rewritten before pretty-printing")
        (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let (call,ta,aexp_needed) =
          if is_bitvector_typ t then
            if not (contains_t_pp_var t)
-           then ("bitvector_concat", doc_tannot_lem regtypes false t, true)
+           then ("bitvector_concat", doc_tannot_lem sequential mwords false t, true)
            else ("bitvector_concat", empty, aexp_needed)
          else ("vector_concat",empty,aexp_needed) in
        let epp =
@@ -467,7 +470,7 @@ let doc_exp_lem, doc_let_lem =
     | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
        raise (report l "E_for should have been removed till now")
     | E_let(leb,e) ->
-       let epp = let_exp regtypes early_ret leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
+       let epp = let_exp sequential mwords early_ret leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
        if aexp_needed then parens epp else epp
     | E_app(f,args) ->
        begin match f with
@@ -506,7 +509,7 @@ let doc_exp_lem, doc_let_lem =
             let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
             let eff = effect_of full_exp in
             if contains_bitvector_typ t && not (contains_t_pp_var t)
-            then (align epp ^^ (doc_tannot_lem regtypes (effectful eff) t), true)
+            then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
             else (epp, aexp_needed) in
           if aexp_needed then parens (align taepp) else taepp
        | Id_aux (Id "length",_) ->
@@ -544,7 +547,7 @@ let doc_exp_lem, doc_let_lem =
                let eff = effect_of full_exp in
                if contains_bitvector_typ (Env.base_typ_of (env_of full_exp) t) &&
                   not (contains_t_pp_var t)
-               then (align epp ^^ (doc_tannot_lem regtypes (effectful eff) t), true)
+               then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
                else (epp, aexp_needed) in
              liftR (if aexp_needed then parens (align taepp) else taepp)
           end
@@ -563,20 +566,20 @@ let doc_exp_lem, doc_let_lem =
        if aexp_needed then parens (align epp) else epp*)
     | E_vector_subrange (v,e1,e2) ->
       raise (Reporting_basic.err_unreachable l
-        "E_vector_access should have been rewritten before pretty-printing")
+        "E_vector_subrange should have been rewritten before pretty-printing")
        (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let eff = effect_of full_exp in
        let (epp,aexp_needed) =
          if has_effect eff BE_rreg then
            let epp = align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in
            if contains_bitvector_typ t && not (contains_t_pp_var t)
-           then (epp ^^ doc_tannot_lem regtypes true t, true)
+           then (epp ^^ doc_tannot_lem sequential mwords true t, true)
            else (epp, aexp_needed)
          else
            if is_bitvector_typ t then
              let bepp = string "bvslice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2 in
              if not (contains_t_pp_var t)
-             then (bepp ^^ doc_tannot_lem regtypes false t, true)
+             then (bepp ^^ doc_tannot_lem sequential mwords false t, true)
              else (bepp, aexp_needed)
            else (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2, aexp_needed) in
        if aexp_needed then parens (align epp) else epp *)
@@ -591,7 +594,7 @@ let doc_exp_lem, doc_let_lem =
            let field_f = doc_id_lem tid ^^ underscore ^^ doc_id_lem id ^^ dot ^^ string "get_field" in
            let (ta,aexp_needed) =
              if contains_bitvector_typ t && not (contains_t_pp_var t)
-             then (doc_tannot_lem regtypes (effectful eff) t, true)
+             then (doc_tannot_lem sequential mwords (effectful eff) t, true)
              else (empty, aexp_needed) in
            let epp = field_f ^^ space ^^ (expY fexp) in
            if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta)
@@ -614,7 +617,7 @@ let doc_exp_lem, doc_let_lem =
        if has_effect eff BE_rreg then
          let epp = separate space [string "read_reg";doc_id_lem id] in
          if is_bitvector_typ base_typ && not (contains_t_pp_var base_typ)
-         then liftR (parens (epp ^^ doc_tannot_lem regtypes true base_typ))
+         then liftR (parens (epp ^^ doc_tannot_lem sequential mwords true base_typ))
          else liftR epp
        else if is_ctor env id then doc_id_lem_ctor id
        else doc_id_lem id
@@ -626,7 +629,7 @@ let doc_exp_lem, doc_let_lem =
                   | _ -> "read_reg_field" in
                 let ta =
                   if contains_bitvector_typ t && not (contains_t_pp_var t)
-                  then doc_tannot_lem regtypes true t else empty in
+                  then doc_tannot_lem sequential mwords true t else empty in
                 let epp = separate space [string call;string reg;string_lit(string field)] ^^ ta in
                 if aexp_needed then parens (align epp) else epp
             | Alias_pair(reg1,reg2) ->
@@ -634,7 +637,7 @@ let doc_exp_lem, doc_let_lem =
                   if has_effect eff BE_rreg then
                     let ta =
                       if contains_bitvector_typ t && not (contains_t_pp_var t)
-                      then doc_tannot_lem regtypes true t else empty in
+                      then doc_tannot_lem sequential mwords true t else empty in
                     ("read_two_regs", ta)
                   else
                     ("RegisterPair", empty) in
@@ -647,11 +650,11 @@ let doc_exp_lem, doc_let_lem =
                   else
                     let ta =
                       if contains_bitvector_typ t && not (contains_t_pp_var t)
-                      then doc_tannot_lem regtypes true t else empty in
+                      then doc_tannot_lem sequential mwords true t else empty in
                     separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in
                 if aexp_needed then parens (align epp) else epp
            )*)
-    | E_lit lit -> doc_lit_lem regtypes false lit annot
+    | E_lit lit -> doc_lit_lem sequential mwords false lit annot
     | E_cast(typ,e) ->
        expV aexp_needed e (*
        (match annot with
@@ -659,7 +662,7 @@ let doc_exp_lem, doc_let_lem =
            (* TODO: Does this case still exist with the new type checker? *)
            let epp = string "read_reg" ^^ space ^^ expY e in
            if contains_bitvector_typ t && not (contains_t_pp_var t)
-           then parens (epp ^^ doc_tannot_lem regtypes true t) else epp
+           then parens (epp ^^ doc_tannot_lem sequential mwords true t) else epp
         | Base((_,t),_,_,_,_,_) ->
            (match typ with
             | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) ->
@@ -692,7 +695,7 @@ let doc_exp_lem, doc_let_lem =
          | _ ->  raise (report l "cannot get record type") in
        let epp = anglebars (space ^^ (align (separate_map
                                           (semi_sp ^^ break 1)
-                                          (doc_fexp regtypes early_ret recordtyp) fexps)) ^^ space) in
+                                          (doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in
        if aexp_needed then parens epp else epp
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
        let (E_aux (_, (_, eannot))) = e in
@@ -700,7 +703,7 @@ let doc_exp_lem, doc_let_lem =
          | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
            tid
          | _ ->  raise (report l "cannot get record type") in
-       anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp regtypes early_ret recordtyp) fexps))
+       anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps))
     | E_vector exps ->
        let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let (start, len, order, etyp) =
@@ -731,11 +734,11 @@ let doc_exp_lem, doc_let_lem =
               let epp =
                 group (separate space [string "Vector"; brackets expspp;string start;string dir_out]) in
               let (epp,aexp_needed) =
-                if is_bit_typ etyp then
+                if is_bit_typ etyp && mwords then
                   let bepp = string "vec_to_bvec" ^^ space ^^ parens (align epp) in
                   if contains_t_pp_var t
                   then (bepp, aexp_needed)
-                  else (bepp ^^ doc_tannot_lem regtypes false t, true)
+                  else (bepp ^^ doc_tannot_lem sequential mwords false t, true)
                 else (epp,aexp_needed) in
               if aexp_needed then parens (align epp) else epp
        (* *)
@@ -792,18 +795,24 @@ let doc_exp_lem, doc_let_lem =
          align (group (call ^//^ brackets expspp ^/^
                          separate space [default_string;string start;string size;string dir_out])) in
        let (bepp, aexp_needed) =
-         if is_bitvector_typ t
-         then (string "vec_to_bvec" ^^ space ^^ parens (epp) ^^ doc_tannot_lem regtypes false t, true)
+         if is_bitvector_typ t && mwords
+         then (string "vec_to_bvec" ^^ space ^^ parens (epp) ^^ doc_tannot_lem sequential mwords false t, true)
          else (epp, aexp_needed) in
        if aexp_needed then parens (align bepp) else bepp
     | E_vector_update(v,e1,e2) ->
        let t = typ_of full_exp in
-       let call = if is_bitvector_typ t then "bvupdate_pos" else "update_pos" in
+       let call =
+         if is_bitvector_typ t (*&& mwords*)
+         then "bitvector_update_pos"
+         else "update_pos" in
        let epp = separate space [string call;expY v;expY e1;expY e2] in
        if aexp_needed then parens (align epp) else epp
     | E_vector_update_subrange(v,e1,e2,e3) ->
        let t = typ_of full_exp in
-       let call = if is_bitvector_typ t then "bvupdate" else "update" in
+       let call =
+         if is_bitvector_typ t (*&& mwords*)
+         then "bitvector_update"
+         else "update" in
        let epp = align (string call ^//^
                           group (group (expY v) ^/^ group (expY e1) ^/^ group (expY e2)) ^/^
                             group (expY e3)) in
@@ -829,7 +838,7 @@ let doc_exp_lem, doc_let_lem =
         pattern-matching on integers *)
        let epp =
          group ((separate space [string "match"; only_integers e; string "with"]) ^/^
-                  (separate_map (break 1) (doc_case regtypes early_ret) pexps) ^/^
+                  (separate_map (break 1) (doc_case sequential mwords early_ret) pexps) ^/^
                     (string "end")) in
        if aexp_needed then parens (align epp) else align epp
     | E_exit e -> liftR (separate space [string "exit"; expY e;])
@@ -919,7 +928,7 @@ let doc_exp_lem, doc_let_lem =
                    string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in
            let (epp,aexp_needed) =
              if contains_bitvector_typ t && not (contains_t_pp_var t)
-             then (parens epp ^^ doc_tannot_lem regtypes false t, true)
+             then (parens epp ^^ doc_tannot_lem sequential mwords false t, true)
              else (epp, aexp_needed) in
            if aexp_needed then parens (align epp) else epp
         | _ ->
@@ -944,13 +953,13 @@ let doc_exp_lem, doc_let_lem =
             (separate space [expV b e1; string ">>"]) ^^ hardline ^^ expN e2
          | _ ->
             (separate space [expV b e1; string ">>= fun";
-                             doc_pat_lem regtypes true pat;arrow]) ^^ hardline ^^ expN e2 in
+                             doc_pat_lem sequential mwords true pat;arrow]) ^^ hardline ^^ expN e2 in
        if aexp_needed then parens (align epp) else epp
     | E_internal_return (e1) ->
        separate space [string "return"; expY e1;]
     | E_sizeof nexp ->
       (match simplify_nexp nexp with
-        | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem regtypes false (L_aux (L_num i, l)) annot
+        | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem sequential mwords false (L_aux (L_num i, l)) annot
         | _ ->
           raise (Reporting_basic.err_unreachable l
             "pretty-printing non-constant sizeof expressions to Lem not supported"))
@@ -960,34 +969,34 @@ let doc_exp_lem, doc_let_lem =
     | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ | E_internal_exp_user _ ->
       raise (Reporting_basic.err_unreachable l
         "unsupported internal expression encountered while pretty-printing")
-  and let_exp regtypes early_ret (LB_aux(lb,_)) = match lb with
+  and let_exp sequential mwords early_ret (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 regtypes true pat; equals])
-              (top_exp regtypes early_ret false e)
+              (separate space [string "let"; doc_pat_lem sequential mwords true pat; equals])
+              (top_exp sequential mwords early_ret false e)
 
-  and doc_fexp regtypes early_ret recordtyp (FE_aux(FE_Fexp(id,e),_)) =
+  and doc_fexp sequential mwords early_ret recordtyp (FE_aux(FE_Fexp(id,e),_)) =
     let fname =
       if prefix_recordtype
       then (string (string_of_id recordtyp ^ "_")) ^^ doc_id_lem id
       else doc_id_lem id in
-    group (doc_op equals fname (top_exp regtypes early_ret true e))
+    group (doc_op equals fname (top_exp sequential mwords early_ret true e))
 
-  and doc_case regtypes early_ret = function
+  and doc_case sequential mwords early_ret = function
   | Pat_aux(Pat_exp(pat,e),_) ->
-    group (prefix 3 1 (separate space [pipe; doc_pat_lem regtypes false pat;arrow])
-                  (group (top_exp regtypes early_ret false e)))
+    group (prefix 3 1 (separate space [pipe; doc_pat_lem sequential mwords false pat;arrow])
+                  (group (top_exp sequential mwords early_ret false e)))
   | Pat_aux(Pat_when(_,_,_),(l,_)) ->
     raise (Reporting_basic.err_unreachable l
       "guarded pattern expression should have been rewritten before pretty-printing")
 
-  and doc_lexp_deref_lem regtypes early_ret ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
+  and doc_lexp_deref_lem sequential mwords early_ret ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
     | LEXP_field (le,id) ->
-       parens (separate empty [doc_lexp_deref_lem regtypes early_ret le;dot;doc_id_lem id])
+       parens (separate empty [doc_lexp_deref_lem sequential mwords early_ret le;dot;doc_id_lem id])
     | LEXP_vector(le,e) ->
-       parens ((separate space) [string "access";doc_lexp_deref_lem regtypes early_ret le;
-                                 top_exp regtypes early_ret true e])
+       parens ((separate space) [string "access";doc_lexp_deref_lem sequential mwords early_ret le;
+                                 top_exp sequential mwords early_ret true e])
     | LEXP_id id -> doc_id_lem id
     | LEXP_cast (typ,id) -> doc_id_lem id
     | _ ->
@@ -996,9 +1005,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 regtypes (Tu_aux(typ_u,_)) = match typ_u with
+let doc_type_union_lem sequential mwords (Tu_aux(typ_u,_)) = match typ_u with
   | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor id; string "of";
-                                        parens (doc_typ_lem regtypes typ)]
+                                        parens (doc_typ_lem sequential mwords typ)]
   | Tu_id id -> separate space [pipe; doc_id_lem_ctor id]
 
 let rec doc_range_lem (BF_aux(r,_)) = match r with
@@ -1006,16 +1015,16 @@ 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 regtypes (TD_aux(td, (l, _))) = match td with
+let doc_typdef_lem sequential mwords (TD_aux(td, (l, _))) = match td with
   | TD_abbrev(id,nm,typschm) ->
      doc_op equals (concat [string "type"; space; doc_id_lem_type id])
-            (doc_typschm_lem regtypes false typschm)
+            (doc_typschm_lem sequential mwords false typschm)
   | TD_record(id,nm,typq,fs,_) ->
     let fname fid = if prefix_recordtype
                     then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
                     else doc_id_lem_type fid in
     let f_pp (typ,fid) =
-      concat [fname fid;space;colon;space;doc_typ_lem regtypes typ; semi] in
+      concat [fname fid;space;colon;space;doc_typ_lem sequential mwords typ; semi] in
     let rectyp = match typq with
       | TypQ_aux (TypQ_tq qs, _) ->
         let quant_item = function
@@ -1032,7 +1041,7 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
         mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown),
           [mk_typ_arg (Typ_arg_typ rectyp);
            mk_typ_arg (Typ_arg_typ ftyp)])) in
-      let rfannot = doc_tannot_lem regtypes false reftyp in
+      let rfannot = doc_tannot_lem sequential mwords false reftyp in
       let get, set =
         string "rec_val" ^^ dot ^^ fname fid,
         anglebars (space ^^ string "rec_val with " ^^
@@ -1040,12 +1049,14 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
       doc_op equals
         (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])])
         (anglebars (concat [space;
+          doc_op equals (string "field_name") (string_lit (doc_id_lem fid)); semi_sp;
           doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp;
           doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in
     doc_op equals
            (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem typq])
            ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline ^^
-    separate_map hardline doc_field fs
+    if sequential && string_of_id id = "regstate" then empty
+    else separate_map hardline doc_field fs
   | TD_variant(id,nm,typq,ar,_) ->
      (match id with
       | Id_aux ((Id "read_kind"),_) -> empty
@@ -1058,7 +1069,7 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
       | Id_aux ((Id "diafp"),_) -> empty
       | Id_aux ((Id "option"),_) -> empty
       | _ ->
-         let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in
+         let ar_doc = group (separate_map (break 1) (doc_type_union_lem sequential mwords) ar) in
          let typ_pp =
 
            (doc_op equals)
@@ -1230,20 +1241,16 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
   | TD_register(id,n1,n2,rs) ->
     match n1, n2 with
     | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
-       let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id);
-                                                       doc_range_lem r;]) in
-       let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in
-       (*let doc_rfield (_,id) =
-         (doc_op equals)
-           (string "let" ^^ space ^^ doc_id_lem id)
-           (string "Register_field" ^^ space ^^ string_lit(doc_id_lem id)) in*)
        let dir_b = i1 < i2 in
        let dir = string (if dir_b then "true" else "false") in
        let dir_suffix = (if dir_b then "_inc" else "_dec") in
        let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in
        let size = if dir_b then i2-i1 +1 else i1-i2 + 1 in
        let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in
-       let tannot = doc_tannot_lem regtypes false vtyp in
+       let tannot = doc_tannot_lem sequential mwords false vtyp in
+       let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id);
+                                                       doc_range_lem r;]) in
+       let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in
        let doc_field (fr, fid) =
          let i, j = match fr with
          | BF_aux (BF_single i, _) -> (i, i)
@@ -1255,32 +1262,21 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
            mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown),
              [mk_typ_arg (Typ_arg_typ (mk_id_typ id));
               mk_typ_arg (Typ_arg_typ ftyp)])) in
-         let rfannot = doc_tannot_lem regtypes false reftyp in
+         let rfannot = doc_tannot_lem sequential mwords false reftyp in
          let get, set =
            "bitvector_subrange" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ")",
            "bitvector_update" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ", v)" in
          doc_op equals
            (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])])
            (concat [
-             space; langlebar; string (" get_field = (fun reg -> " ^ get ^ ");"); hardline;
+             space; langlebar; string " field_name = \"" ^^ doc_id_lem fid ^^ string "\";"; hardline;
+             space; space; space; string (" get_field = (fun reg -> " ^ get ^ ");"); hardline;
              space; space; space; string (" set_field = (fun reg v -> " ^ set ^ ") "); ranglebar])
-             (* string " = <|" (*; parens (string "reg" ^^ tannot) *)]) ^^ hardline ^^
-         string ("  get_field = (fun reg -> " ^ get ^ ");") ^^ hardline ^^
-         string ("  set_field = (fun reg v -> " ^ set ^") |>") *)
-         (* doc_op equals
-           (concat [string "let set_"; doc_id_lem id; underscore; doc_id_lem fid;
-             space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set) *)
        in
        doc_op equals
          (concat [string "type";space;doc_id_lem id])
-         (doc_typ_lem regtypes vtyp)
+         (doc_typ_lem sequential mwords vtyp)
        ^^ hardline ^^
-       (* doc_op equals
-         (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
-         (string "Register" ^^ space ^^
-            align (separate space [string "regname"; doc_int size; doc_int i1; dir;
-                                   break 0 ^^ brackets (align doc_rids)]))
-       ^^ hardline ^^ *)
        doc_op equals
          (concat [string "let";space;string "cast_";doc_id_lem id;space;string "reg"])
          (string "reg")
@@ -1289,25 +1285,54 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
          (concat [string "let";space;string "cast_to_";doc_id_lem id;space;string "reg"])
          (string "reg")
        ^^ hardline ^^
-         separate_map hardline doc_field rs
+       (* if sequential then *)
+               (* string " = <|" (*; parens (string "reg" ^^ tannot) *)]) ^^ hardline ^^
+           string ("  get_field = (fun reg -> " ^ get ^ ");") ^^ hardline ^^
+           string ("  set_field = (fun reg v -> " ^ set ^") |>") *)
+           (* doc_op equals
+             (concat [string "let set_"; doc_id_lem id; underscore; doc_id_lem fid;
+               space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set) *)
+         (* in *)
+         (* doc_op equals
+           (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
+           (string "Register" ^^ space ^^
+              align (separate space [string "regname"; doc_int size; doc_int i1; dir;
+                                     break 0 ^^ brackets (align doc_rids)]))
+         ^^ hardline ^^ *)
+           separate_map hardline doc_field rs
+       ^^ hardline ^^
+       (* else *)
+         (*let doc_rfield (_,id) =
+           (doc_op equals)
+             (string "let" ^^ space ^^ doc_id_lem id)
+             (string "Register_field" ^^ space ^^ string_lit(doc_id_lem id)) in*)
+         doc_op equals
+           (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
+           (string "Register" ^^ space ^^
+              align (separate space [string "regname"; doc_int size; doc_int i1; dir;
+                                     break 0 ^^ brackets (align doc_rids)]))
+         (*^^ hardline ^^
+           separate_map hardline doc_field rs*)
+    | _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices")
+
 
 let doc_rec_lem (Rec_aux(r,_)) = match r with
   | Rec_nonrec -> space
   | Rec_rec -> space ^^ string "rec" ^^ space
 
-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_tannot_opt_lem sequential mwords (Typ_annot_opt_aux(t,_)) = match t with
+  | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem sequential mwords typ)
 
-let doc_fun_body_lem regtypes exp =
+let doc_fun_body_lem sequential mwords exp =
   let early_ret = contains_early_return exp in
-  let doc_exp = doc_exp_lem regtypes early_ret false exp in
+  let doc_exp = doc_exp_lem sequential mwords early_ret false exp in
   if early_ret
   then align (string "catch_early_return" ^//^ parens (doc_exp))
   else doc_exp
 
-let doc_funcl_lem regtypes (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
-  group (prefix 3 1 ((doc_pat_lem regtypes false pat) ^^ space ^^ arrow)
-    (doc_fun_body_lem regtypes exp))
+let doc_funcl_lem sequential mwords (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
+  group (prefix 3 1 ((doc_pat_lem sequential mwords false pat) ^^ space ^^ arrow)
+    (doc_fun_body_lem sequential mwords exp))
 
 let get_id = function
   | [] -> failwith "FD_function with empty list"
@@ -1315,20 +1340,21 @@ let get_id = function
 
 module StringSet = Set.Make(String)
 
-let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot)) =
+let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls),fannot)) =
   match fcls with
   | [] -> failwith "FD_function with empty function list"
-  | [FCL_aux (FCL_Funcl(id,pat,exp),_)] ->
+  | [FCL_aux (FCL_Funcl(id,pat,exp),_)]
+    when not (Env.is_extern id (env_of exp)) ->
      (prefix 2 1)
        ((separate space)
           [(string "let") ^^ (doc_rec_lem r) ^^ (doc_id_lem id);
-           (doc_pat_lem regtypes true pat);
+           (doc_pat_lem sequential mwords true pat);
            equals])
-       (doc_fun_body_lem regtypes exp)
-  | _ ->
-    let id = get_id fcls in
+       (doc_fun_body_lem sequential mwords exp)
+  | FCL_aux (FCL_Funcl(id,_,exp),_) :: _
+    when not (Env.is_extern id (env_of exp)) ->
     (*    let sep = hardline ^^ pipe ^^ space in *)
-    match id with
+    (match id with
     | Id_aux (Id fname,idl)
       when fname = "execute" || fname = "initial_analysis" ->
       let (_,auxiliary_functions,clauses) = 
@@ -1354,7 +1380,7 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot))
                                              P_aux (P_tup argspat,pannot),exp),annot) in
                let auxiliary_functions = 
                   auxiliary_functions ^^ hardline ^^ hardline ^^
-                    doc_fundef_lem regtypes (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in
+                    doc_fundef_lem sequential mwords (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in
                (* Bind complex patterns to names so that we can pass them to the
                   auxiliary function *)
                let name_pat idx (P_aux (p,a)) = match p with
@@ -1366,13 +1392,13 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot))
                let named_pat = P_aux (P_app (Id_aux (Id ctor,l),named_argspat),pannot) in
                let doc_arg idx (P_aux (p,(l,a))) = match p with
                  | P_as (pat,id) -> doc_id_lem id
-                 | P_lit lit -> doc_lit_lem regtypes false lit a
+                 | P_lit lit -> doc_lit_lem sequential mwords false lit a
                  | P_id id -> doc_id_lem id
                  | _ -> string ("arg" ^ string_of_int idx) in
                let clauses =
                  clauses ^^ (break 1) ^^
                    (separate space
-                      [pipe;doc_pat_lem regtypes false named_pat;arrow;
+                      [pipe;doc_pat_lem sequential mwords false named_pat;arrow;
                        string aux_fname;
                        parens (separate comma (List.mapi doc_arg named_argspat))]) in
                (already_used_fnames,auxiliary_functions,clauses)
@@ -1385,73 +1411,75 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot))
     | _ ->
       let clauses =
         (separate_map (break 1))
-          (fun fcl -> separate space [pipe;doc_funcl_lem regtypes fcl]) fcls in
+          (fun fcl -> separate space [pipe;doc_funcl_lem sequential mwords fcl]) fcls in
       (prefix 2 1)
         ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"])
-        (clauses ^/^ string "end")
-      
+        (clauses ^/^ string "end"))
+  | _ -> empty
 
 
-let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
+
+let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) =
   match reg with
   | DEC_reg(typ,id) ->
-     empty
-     (* let env = env_of_annot annot in
-     (match typ with
-      | Typ_aux (Typ_id idt, _) when Env.is_regtyp idt env ->
-        separate space [string "let";doc_id_lem id;equals;
-                        string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline
-      | _ ->
-        let rt = Env.base_typ_of env typ in
-        if is_vector_typ rt then
-          let (start, size, order, etyp) = vector_typ_args_of rt in
-          if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then
-            let o = if is_order_inc order then "true" else "false" in
-            (doc_op equals)
-            (string "let" ^^ space ^^ doc_id_lem id)
-            (string "Register" ^^ space ^^
-               align (separate space [string_lit(doc_id_lem id);
-                                      doc_nexp (size);
-                                      doc_nexp (start);
-                                      string o;
-                                      string "[]"]))
-               ^/^ hardline
+     if sequential then empty
+     else
+       let env = env_of_annot annot in
+       (match typ with
+        | Typ_aux (Typ_id idt, _) when Env.is_regtyp idt env ->
+          separate space [string "let";doc_id_lem id;equals;
+                          string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline
+        | _ ->
+          let rt = Env.base_typ_of env typ in
+          if is_vector_typ rt then
+            let (start, size, order, etyp) = vector_typ_args_of rt in
+            if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then
+              let o = if is_order_inc order then "true" else "false" in
+              (doc_op equals)
+              (string "let" ^^ space ^^ doc_id_lem id)
+              (string "Register" ^^ space ^^
+                 align (separate space [string_lit(doc_id_lem id);
+                                        doc_nexp (size);
+                                        doc_nexp (start);
+                                        string o;
+                                        string "[]"]))
+                 ^/^ hardline
+            else raise (Reporting_basic.err_unreachable l
+              ("can't deal with register type " ^ string_of_typ typ))
           else raise (Reporting_basic.err_unreachable l
-            ("can't deal with register type " ^ string_of_typ typ))
-        else raise (Reporting_basic.err_unreachable l
-          ("can't deal with register type " ^ string_of_typ typ))) *)
+            ("can't deal with register type " ^ string_of_typ typ)))
   | DEC_alias(id,alspec) -> empty
   | DEC_typ_alias(typ,id,alspec) -> empty
 
-let doc_spec_lem regtypes (VS_aux (valspec,annot)) =
+let doc_spec_lem mwords (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) | VS_cast_spec (typschm,id) -> empty
-(* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem regtypes typschm] ^/^ hardline *)
+(* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem mwords typschm] ^/^ hardline *)
 
 
-let rec doc_def_lem regtypes def = match def with
-  | DEF_spec v_spec -> (doc_spec_lem regtypes v_spec,empty)
+let rec doc_def_lem sequential mwords def = match def with
+  | DEF_spec v_spec -> (doc_spec_lem mwords v_spec,empty)
   | DEF_overload _ -> (empty,empty)
-  | DEF_type t_def -> (group (doc_typdef_lem regtypes t_def) ^/^ hardline,empty)
-  | DEF_reg_dec dec -> (group (doc_dec_lem dec),empty)
+  | DEF_type t_def -> (group (doc_typdef_lem sequential mwords t_def) ^/^ hardline,empty)
+  | DEF_reg_dec dec -> (group (doc_dec_lem sequential dec),empty)
 
   | DEF_default df -> (empty,empty)
-  | DEF_fundef f_def -> (empty,group (doc_fundef_lem regtypes f_def) ^/^ hardline)
-  | DEF_val lbind -> (empty,group (doc_let_lem regtypes false lbind) ^/^ hardline)
+  | DEF_fundef f_def -> (empty,group (doc_fundef_lem sequential mwords f_def) ^/^ hardline)
+  | DEF_val lbind -> (empty,group (doc_let_lem sequential mwords false lbind) ^/^ hardline)
   | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point"
 
   | DEF_kind _ -> (empty,empty)
 
   | DEF_comm (DC_comm s) -> (empty,comment (string s))
   | DEF_comm (DC_comm_struct d) ->
-     let (typdefs,vdefs) = doc_def_lem regtypes d in
+     let (typdefs,vdefs) = doc_def_lem sequential mwords d in
      (empty,comment (typdefs ^^ hardline ^^ vdefs))
 
 
-let doc_defs_lem regtypes (Defs defs) =
-  let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in
+let doc_defs_lem sequential mwords (Defs defs) =
+  let (typdefs,valdefs) = List.split (List.map (doc_def_lem sequential mwords) defs) in
   (separate empty typdefs,separate empty valdefs)
 
 let find_regtypes (Defs defs) =
@@ -1470,7 +1498,7 @@ let find_registers (Defs defs) =
       | _ -> acc
     ) [] defs
 
-let doc_regstate_lem regtypes registers =
+let doc_regstate_lem mwords registers =
   let l = Parse_ast.Unknown in
   let annot = (l, None) in
   let regstate = match registers with
@@ -1487,25 +1515,26 @@ let doc_regstate_lem regtypes registers =
         registers,
         false) in
   concat [
-    doc_typdef_lem regtypes (TD_aux (regstate, annot)); hardline;
+    doc_typdef_lem true mwords (TD_aux (regstate, annot)); hardline;
     hardline;
     string "type _M 'a = M regstate 'a"
   ]
 
-let doc_register_refs_lem regtypes registers =
+let doc_register_refs_lem registers =
   let doc_register_ref (typ, id) =
     let idd = doc_id_lem id in
     let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in
     concat [string "let "; idd; string " = <|"; hardline;
+      string "  reg_name = \""; idd; string "\";"; hardline;
       string "  read_from = (fun s -> s."; field; string ");"; hardline;
       string "  write_to = (fun s v -> (<| s with "; field; string " = v |>)) |>"] in
   separate_map hardline doc_register_ref registers
 
-let pp_defs_lem (types_file,types_modules) (types_seq_file,types_seq_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line =
-  let regtypes = find_regtypes d in
-  let (typdefs,valdefs) = doc_defs_lem regtypes d in
-  let regstate_def = doc_regstate_lem regtypes (find_registers d) in
-  let register_refs = doc_register_refs_lem regtypes (find_registers d) in
+let pp_defs_lem sequential mwords (types_file,types_modules) (defs_file,defs_modules) d top_line =
+  (* let regtypes = find_regtypes d in *)
+  let (typdefs,valdefs) = doc_defs_lem sequential mwords d in
+  let regstate_def = doc_regstate_lem mwords (find_registers d) in
+  let register_refs = doc_register_refs_lem (find_registers d) in
   (print types_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
@@ -1523,8 +1552,16 @@ let pp_defs_lem (types_file,types_modules) (types_seq_file,types_seq_modules) (p
              string "module SIA = Interp_ast"; hardline;
              hardline]
         else empty;
-        typdefs]);
-  (print types_seq_file)
+        typdefs; hardline;
+        hardline;
+        if sequential then
+          concat [regstate_def; hardline;
+          hardline;
+          register_refs]
+        else
+          concat [string "type _M 'a = M 'a"; hardline]
+        ]);
+  (* (print types_seq_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
         (separate_map hardline)
@@ -1541,24 +1578,22 @@ let pp_defs_lem (types_file,types_modules) (types_seq_file,types_seq_modules) (p
              string "module SIA = Interp_ast"; hardline;
              hardline]
         else empty;
-        typdefs;
-        hardline;
+        typdefs_seq; hardline;
         hardline;
-        regstate_def;
+        regstate_def; hardline;
         hardline;
-        hardline;
-        register_refs]);
-  (print prompt_file)
+        register_refs]); *)
+  (print defs_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
         (separate_map hardline)
-          (fun lib -> separate space [string "open import";string lib]) prompt_modules;hardline;
+          (fun lib -> separate space [string "open import";string lib]) defs_modules;hardline;
         hardline;
         valdefs]);
-  (print state_file)
+  (* (print state_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
         (separate_map hardline)
           (fun lib -> separate space [string "open import";string lib]) state_modules;hardline;
         hardline;
-        valdefs]);
+        valdefs_seq]); *)
diff --git a/src/process_file.ml b/src/process_file.ml
index 6a3fc24c..46b6538e 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -134,10 +134,11 @@ let close_output_with_check (o, temp_file_name, file_name) =
 let generated_line f =
   Printf.sprintf "Generated by Sail from %s." f
 
-let output_lem filename libs libs_seq defs =
+let output_lem filename libs defs =
   let generated_line = generated_line filename in
   let types_module = (filename ^ "_embed_types") in
-  let types_module_sequential = (filename ^ "_embed_types_sequential") in
+  let types_module_seq = (filename ^ "_embed_types_sequential") in
+  let libs_seq = List.map (fun lib -> lib ^ "_sequential") libs in
   let ((ot,_, _) as ext_ot) =
     open_output_with_check_unformatted (filename ^ "_embed_types.lem") in
   let ((ots,_, _) as ext_ots) =
@@ -146,13 +147,15 @@ let output_lem filename libs libs_seq defs =
     open_output_with_check_unformatted (filename ^ "_embed.lem") in
   let ((os,_, _) as ext_os) =
     open_output_with_check_unformatted (filename ^ "_embed_sequential.lem") in
-  (Pretty_print.pp_defs_lem
-     (ot,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Prompt"])
-     (ots,["Pervasives_extra";"Sail_impl_base";"Sail_values";"State"])
-     (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Prompt";
+  (Pretty_print.pp_defs_lem false false
+     (ot,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt"])
+     (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt";
        String.capitalize types_module] @ libs)
-     (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"State";
-       String.capitalize types_module_sequential] @ libs_seq)
+     defs generated_line);
+  (Pretty_print.pp_defs_lem true true
+     (ots,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State"])
+     (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State";
+       String.capitalize types_module_seq] @ libs_seq)
      defs generated_line);
   close_output_with_check ext_ot;
   close_output_with_check ext_ots;
@@ -205,9 +208,9 @@ let output1 libpath out_arg filename defs  =
 	  close_output_with_check ext_o
 	end
       | Lem_out None ->
-        output_lem f' [] [] defs
+        output_lem f' [] defs
       | Lem_out (Some lib) ->
-        output_lem f' [lib] [lib ^ "_sequential"] defs
+        output_lem f' [lib] defs
       | Ocaml_out None ->
         let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in
 	begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"];
diff --git a/src/type_check.ml b/src/type_check.ml
index 9e7a1ab3..fcabbb1c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2566,7 +2566,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      let else_branch' = crule check_exp (add_constraints (List.map nc_negate constrs) (add_flows false flows env)) else_branch (typ_of then_branch') in
      annot_exp (E_if (cond', then_branch', else_branch')) (typ_of then_branch')
   | E_vector_access (v, n) -> infer_exp env (E_aux (E_app (mk_id "vector_access", [v; n]), (l, ())))
-  | E_vector_append (v1, v2) -> infer_exp env (E_aux (E_app (mk_id "vector_append", [v1; v2]), (l, ())))
+  | E_vector_append (v1, v2) -> infer_exp env (E_aux (E_app (mk_id "append", [v1; v2]), (l, ())))
   | E_vector_subrange (v, n, m) -> infer_exp env (E_aux (E_app (mk_id "vector_subrange", [v; n; m]), (l, ())))
   | E_vector [] -> typ_error l "Cannot infer type of empty vector"
   | E_vector ((item :: items) as vec) ->