sail changes for making lem embedding Isabelle-friendlier

9 files changed, 215 insertions, 219 deletions

diff --git a/mips/hgen/herdtools_types_to_shallow_types.hgen b/mips/hgen/herdtools_types_to_shallow_types.hgen
index 115de27c..5a0e3bfc 100644
--- a/mips/hgen/herdtools_types_to_shallow_types.hgen
+++ b/mips/hgen/herdtools_types_to_shallow_types.hgen
@@ -100,21 +100,21 @@ let translate_imm16 name value =
 let translate_imm5 name value = 
     Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int value)
 let translate_bool name = function
-  | true -> Sail_values.I
-  | false -> Sail_values.O
+  | true -> Sail_values.B1
+  | false -> Sail_values.B0
 
 let translate_wordsize _ = function
- | MIPSByte -> Mips_embed_types.B0
+ | MIPSByte -> Mips_embed_types.B2
  | MIPSHalf -> Mips_embed_types.H
  | MIPSWord -> Mips_embed_types.W
  | MIPSDouble -> Mips_embed_types.D
 
 let translate_cmp _ = function
-  | MIPS_EQ  -> EQ_
+  | MIPS_EQ  -> EQ'
   | MIPS_NE  -> NE
   | MIPS_GE  -> GE
   | MIPS_GEU -> GEU
-  | MIPS_GT  -> GT_
+  | MIPS_GT  -> GT'
   | MIPS_LE  -> LE
-  | MIPS_LT  -> LT_
+  | MIPS_LT  -> LT'
   | MIPS_LTU -> LTU
diff --git a/mips/hgen/shallow_types_to_herdtools_types.hgen b/mips/hgen/shallow_types_to_herdtools_types.hgen
index 88743ac0..a02d83b7 100644
--- a/mips/hgen/shallow_types_to_herdtools_types.hgen
+++ b/mips/hgen/shallow_types_to_herdtools_types.hgen
@@ -17,23 +17,23 @@ let translate_out_simm16 imm = translate_out_signed_int imm 16
 let translate_out_imm5 imm = translate_out_int imm
 
 let translate_out_bool = function
-  | Sail_values.I  -> true
-  | Sail_values.O -> false
+  | Sail_values.B1  -> true
+  | Sail_values.B0 -> false
   | _ -> failwith "translate_out_bool Undef"
 
 
 let translate_out_wordWidth = function
-    | Mips_embed_types.B0 -> MIPSByte
+    | Mips_embed_types.B2 -> MIPSByte
     | Mips_embed_types.H -> MIPSHalf
     | Mips_embed_types.W -> MIPSWord
     | Mips_embed_types.D -> MIPSDouble
 
 let translate_out_cmp = function
-    | Mips_embed_types.EQ_ -> MIPS_EQ  (* equal *)
+    | Mips_embed_types.EQ' -> MIPS_EQ  (* equal *)
     | Mips_embed_types.NE -> MIPS_NE  (* not equal *)
     | Mips_embed_types.GE -> MIPS_GE  (* signed greater than or equal *)
     | Mips_embed_types.GEU -> MIPS_GEU (* unsigned greater than or equal *) 
-    | Mips_embed_types.GT_ -> MIPS_GT  (* signed strictly greater than *) 
+    | Mips_embed_types.GT' -> MIPS_GT  (* signed strictly greater than *) 
     | Mips_embed_types.LE -> MIPS_LE  (* signed less than or equal *) 
-    | Mips_embed_types.LT_ -> MIPS_LT  (* signed strictly less than *) 
+    | Mips_embed_types.LT' -> MIPS_LT  (* signed strictly less than *) 
     | Mips_embed_types.LTU -> MIPS_LTU (* unsigned less than or qual *) 
diff --git a/mips/mips_extras_embed.lem b/mips/mips_extras_embed.lem
index d59213b8..41a6726f 100644
--- a/mips/mips_extras_embed.lem
+++ b/mips/mips_extras_embed.lem
@@ -33,9 +33,9 @@ val MEMval_tag             : (vector bitU * integer * vector bitU) -> M unit
 val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bitU
 
 let MEMval (_,_,v)                 = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v)     = write_mem_val endian v >>= fun b -> return (if b then I else O)
+let MEMval_conditional (_,_,v)     = write_mem_val endian v >>= fun b -> return (if b then B1 else B0)
 let MEMval_tag (_,_,v)             = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then I else O)
+let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then B1 else B0)
 
 
 val MEM_sync  : unit -> M unit
diff --git a/mips/mips_extras_embed_sequential.lem b/mips/mips_extras_embed_sequential.lem
index 6070df09..502fe102 100644
--- a/mips/mips_extras_embed_sequential.lem
+++ b/mips/mips_extras_embed_sequential.lem
@@ -33,9 +33,9 @@ val MEMval_tag             : (vector bitU * integer * vector bitU) -> M unit
 val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bitU
 
 let MEMval (_,_,v)                 = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v)     = write_mem_val endian v >>= fun b -> return (if b then I else O)
+let MEMval_conditional (_,_,v)     = write_mem_val endian v >>= fun b -> return (if b then B1 else B0)
 let MEMval_tag (_,_,v)             = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then I else O)
+let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then B1 else B0)
 
 
 val MEM_sync  : unit -> M unit
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index f770042c..72effa2f 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -15,7 +15,7 @@ let rec bind m f = match m with
   | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (bind o f,opt))
   | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (bind o f,opt))
   | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (bind o f,opt))
-  | Escape descr mo  ->    Escape descr mo
+  | Escape descr ->        Escape descr
   | Fail descr ->          Fail descr
   | Error descr ->         Error descr
   | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (bind o f ,opt))
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 0d47a5e8..4771bcd7 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -17,12 +17,12 @@ let rec replace bs ((n : integer),b') = match bs with
 
 
 (*** Bits *)
-type bitU = O | I | Undef
+type bitU = B0 | B1 | BU
 
 let showBitU = function
-  | O -> "O"
-  | I -> "I"
-  | Undef -> "Undef"
+  | B0 -> "O"
+  | B1 -> "I"
+  | BU -> "U"
 end
 
 instance (Show bitU)
@@ -31,52 +31,52 @@ end
 
 
 let bitU_to_bool = function
-  | O -> false
-  | I  -> true
-  | Undef -> failwith "to_bool applied to Undef"
+  | B0 -> false
+  | B1  -> true
+  | BU -> failwith "to_bool applied to BU"
   end
 
 let bit_lifted_of_bitU = function
-  | O -> Bitl_zero
-  | I -> Bitl_one
-  | Undef -> Bitl_undef
+  | B0 -> Bitl_zero
+  | B1 -> Bitl_one
+  | BU -> Bitl_undef
   end
 
 let bitU_of_bit = function
-  | Bitc_zero -> O
-  | Bitc_one  -> I
+  | Bitc_zero -> B0
+  | Bitc_one  -> B1
   end
 
 let bit_of_bitU = function
-  | O -> Bitc_zero
-  | I -> Bitc_one
-  | Undef -> failwith "bit_of_bitU: Undef"
+  | B0 -> Bitc_zero
+  | B1 -> Bitc_one
+  | BU -> failwith "bit_of_bitU: BU"
   end
 
 let bitU_of_bit_lifted = function
-  | Bitl_zero -> O
-  | Bitl_one  -> I
-  | Bitl_undef -> Undef
+  | Bitl_zero -> B0
+  | Bitl_one  -> B1
+  | Bitl_undef -> BU
   | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown"
   end
 
 let bitwise_not_bit = function
-  | I -> O
-  | O -> I
-  | Undef -> Undef
+  | 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 I else O
+  if i = 1 then B1 else B0
 
-let bool_to_bitU b = if b then I else O
+let bool_to_bitU b = if b then B1 else B0
 
 let bitwise_binop_bit op = function
-  | (Undef,_) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
-  | (_,Undef) -> Undef (*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?*)
+  | (_,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
 
@@ -234,9 +234,9 @@ let unsigned (Vector bs _ _) : integer =
     List.foldr
       (fun b (acc,exp) ->
         match b with
-        | I -> (acc + integerPow 2 exp,exp + 1)
-        | O -> (acc, exp + 1)
-        | Undef -> failwith "unsigned: vector has undefined bits"
+        | B1 -> (acc + integerPow 2 exp,exp + 1)
+        | B0 -> (acc, exp + 1)
+        | BU -> failwith "unsigned: vector has undefined bits"
         end)
       (0,0) bs in
   sum
@@ -245,9 +245,9 @@ let unsigned_big = unsigned
 
 let signed v : integer =
   match most_significant v with
-  | I -> 0 - (1 + (unsigned (bitwise_not v)))
-  | O -> unsigned v
-  | Undef -> failwith "signed applied to vector with undefined bits"
+  | 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 = 
@@ -301,19 +301,19 @@ let get_min_representable_in _ (n : integer) : integer =
 val to_bin_aux : natural -> list bitU
 let rec to_bin_aux x =
   if x = 0 then []
-  else (if x mod 2 = 1 then I else O) :: to_bin_aux (x / 2)
+  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 (O :: bits) (n -1)
+  if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
 
 
 let rec add_one_bit_ignore_overflow_aux bits = match bits with
   | [] -> []
-  | O :: bits -> I :: bits
-  | I :: bits -> O :: add_one_bit_ignore_overflow_aux bits
-  | Undef :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
+  | 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 =
@@ -339,7 +339,7 @@ let to_vec_inc = to_vec true
 let to_vec_dec = to_vec false
 
 let to_vec_undef is_inc (len : integer) =
-  Vector (replicate (natFromInteger len) Undef) (if is_inc then 0 else len-1) is_inc
+  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
@@ -440,7 +440,7 @@ 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 | I -> (1 : integer) | _ -> 0 end) 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
@@ -463,7 +463,7 @@ let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (Ve
   let overflow =
     if n <= get_max_representable_in sign len &&
          n >= get_min_representable_in sign len
-    then O else I in
+    then B0 else B1 in
   let c_out = most_significant one_more_size_u in
   (correct_size_num,overflow,c_out)
 
@@ -487,9 +487,9 @@ let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (siz
   let l' = to_num sign l in
   let l_u = to_num false l in
   let (n,nu,changed) = match r_bit with
-    | I -> (op l' 1, op l_u 1, true)
-    | O -> (l',l_u,false)
-    | _ -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
+    | 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
@@ -498,8 +498,8 @@ let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (siz
     if changed
     then
       if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
-      then O else I
-    else O in
+      then B0 else B1
+    else B0 in
   (correct_size_num,overflow,most_significant one_larger)
 
 (* add_overflow_vec_bit_signed
@@ -516,9 +516,9 @@ 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 O) start is_inc
+     Vector (sublist bs (n,List.length bs -1) ++ List.replicate n B0) start is_inc
   | RR_shift (*">>"*) ->
-     Vector (List.replicate n O ++ sublist bs (0,n-1)) start is_inc
+     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
@@ -545,7 +545,7 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector
     end in
   if representable
   then to_vec is_inc (act_size,n')
-  else Vector (List.replicate (natFromInteger act_size) Undef) start is_inc
+  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
@@ -569,9 +569,9 @@ let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
     if representable then
       (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
     else
-      (Vector (List.replicate (natFromInteger act_size) Undef) start is_inc,
-       Vector (List.replicate (natFromInteger (act_size + 1)) Undef) start is_inc) in
-  let overflow = if representable then O else I in
+      (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
@@ -658,7 +658,7 @@ let make_indexed_vector entries default start length dir =
 (*
 val make_bit_vector_undef : integer -> vector bitU
 let make_bitvector_undef length =
-  Vector (replicate (natFromInteger length) Undef) 0 true
+  Vector (replicate (natFromInteger length) BU) 0 true
  *)
 
 (* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
@@ -887,10 +887,11 @@ let assert' b msg_opt =
 (* convert numbers unsafely to naturals *)
 
 class (ToNatural 'a) val toNatural : 'a -> natural end
-instance (ToNatural integer) let toNatural = naturalFromInteger end
-instance (ToNatural int)     let toNatural = naturalFromInt     end
-instance (ToNatural nat)     let toNatural = naturalFromNat     end
-instance (ToNatural natural) let toNatural = id                 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,
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 6149bdea..dbc8e0e6 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -862,8 +862,8 @@ let rec outcome_to_outcome pp_instruction_state mode =
      Sail_impl_base.Write_reg (r,rv) (state_to_outcome_s mode state)
   | Interp_interface.Nondet_choice _ _ ->
      failwith "Nondet_choice not supported yet"
-  | Interp_interface.Escape maybestate _ ->
-     Sail_impl_base.Escape Nothing (Maybe.map (state_to_outcome_s mode) maybestate)
+  | Interp_interface.Escape _ _ ->
+     Sail_impl_base.Escape Nothing
   | Interp_interface.Fail maybestring ->
      Sail_impl_base.Fail maybestring
   | Interp_interface.Internal maybestring maybeprint state ->
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 88e197d5..9679b658 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -103,13 +103,16 @@ end
 let ~{ocaml} bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) =
   match (bl1,bl2) with
   | (Bitl_zero, Bitl_zero) -> EQ
+  | (Bitl_zero,_) -> LT
+  | (Bitl_one, Bitl_zero) -> GT
   | (Bitl_one, Bitl_one) -> EQ
+  | (Bitl_one, _) -> LT
+  | (Bitl_undef,Bitl_zero) -> GT
+  | (Bitl_undef,Bitl_one) -> GT
   | (Bitl_undef,Bitl_undef) -> EQ
+  | (Bitl_undef,_) -> LT
   | (Bitl_unknown,Bitl_unknown) -> EQ
-  | (Bitl_zero,_) -> LT
-  | (Bitl_one, _) -> LT
-  | (Bitl_undef, _) -> LT
-  | (_,_) -> GT
+  | (Bitl_unknown,_) -> GT
   end
 let inline {ocaml} bit_liftedCompare = defaultCompare
 
@@ -416,30 +419,32 @@ they just have particular nias (and will be IK_simple *)
   | IK_simple
 
 (* the address_lifted types should go away here and be replaced by address *)
+type with_pp 'o = 'o * maybe (unit -> (string * string))
 type outcome 'a =
   (* 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 -> outcome_s 'a)
+  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_pp (outcome 'a))
   (* Tell the system a write is imminent, at address lifted, of size nat *)
-  | Write_ea of (write_kind * address_lifted * nat) * outcome_s 'a
+  | Write_ea of (write_kind * address_lifted * nat) * (with_pp (outcome 'a))
   (* 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 -> outcome_s 'a)
+  | Write_memv of memory_value * (bool -> with_pp (outcome 'a))
   (* Request a memory barrier *)
-  | Barrier of barrier_kind * outcome_s 'a
+  | Barrier of barrier_kind * with_pp (outcome 'a)
   (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint of outcome_s 'a
+  | Footprint of with_pp (outcome 'a)
   (* Request to read register, will track dependency when mode.track_values *)
-  | Read_reg of reg_name * (register_value -> outcome_s 'a)
+  | Read_reg of reg_name * (register_value -> with_pp (outcome 'a))
   (* Request to write register *)
-  | Write_reg of (reg_name * register_value) * (outcome_s 'a)
-  | Escape of maybe string * maybe (outcome_s unit)
+  | Write_reg of (reg_name * register_value) * with_pp (outcome 'a)
+  | 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)) * outcome_s 'a
+  | Internal of (maybe string * maybe (unit -> string)) * with_pp (outcome 'a)
   | Done of 'a
   | Error of string
- and outcome_s 'a = outcome 'a * maybe (unit -> (string * string))
+
+type outcome_s 'a = with_pp (outcome 'a)
 (* first string : output of instruction_stack_to_string
    second string: output of local_variables_to_string *)
 
@@ -618,56 +623,22 @@ end
 let ~{ocaml} barrier_kindCompare bk1 bk2 =
   match (bk1, bk2) with
   | (Barrier_Sync, Barrier_Sync)   -> EQ
-  | (Barrier_Sync, Barrier_LwSync) -> LT
-  | (Barrier_Sync, Barrier_Eieio)  -> LT
-  | (Barrier_Sync, Barrier_Isync)  -> LT
-  | (Barrier_Sync, Barrier_DMB)    -> LT
-  | (Barrier_Sync, Barrier_DMB_ST) -> LT
-  | (Barrier_Sync, Barrier_DMB_LD) -> LT
-  | (Barrier_Sync, Barrier_DSB)    -> LT
-  | (Barrier_Sync, Barrier_DSB_ST) -> LT
-  | (Barrier_Sync, Barrier_DSB_LD) -> LT
-  | (Barrier_Sync, Barrier_ISB)    -> LT
-  | (Barrier_Sync, Barrier_MIPS_SYNC) -> LT
+  | (Barrier_Sync, _) -> LT
 
   | (Barrier_LwSync, Barrier_Sync)   -> GT
   | (Barrier_LwSync, Barrier_LwSync) -> EQ
-  | (Barrier_LwSync, Barrier_Eieio)  -> LT
-  | (Barrier_LwSync, Barrier_Isync)  -> LT
-  | (Barrier_LwSync, Barrier_DMB)    -> LT
-  | (Barrier_LwSync, Barrier_DMB_ST) -> LT
-  | (Barrier_LwSync, Barrier_DMB_LD) -> LT
-  | (Barrier_LwSync, Barrier_DSB)    -> LT
-  | (Barrier_LwSync, Barrier_DSB_ST) -> LT
-  | (Barrier_LwSync, Barrier_DSB_LD) -> LT
-  | (Barrier_LwSync, Barrier_ISB)    -> LT
-  | (Barrier_LwSync, Barrier_MIPS_SYNC) -> LT
+  | (Barrier_LwSync, _)  -> LT
 
   | (Barrier_Eieio, Barrier_Sync)   -> GT
   | (Barrier_Eieio, Barrier_LwSync) -> GT
   | (Barrier_Eieio, Barrier_Eieio)  -> EQ
-  | (Barrier_Eieio, Barrier_Isync)  -> LT
-  | (Barrier_Eieio, Barrier_DMB)    -> LT
-  | (Barrier_Eieio, Barrier_DMB_ST) -> LT
-  | (Barrier_Eieio, Barrier_DMB_LD) -> LT
-  | (Barrier_Eieio, Barrier_DSB)    -> LT
-  | (Barrier_Eieio, Barrier_DSB_ST) -> LT
-  | (Barrier_Eieio, Barrier_DSB_LD) -> LT
-  | (Barrier_Eieio, Barrier_ISB)    -> LT
-  | (Barrier_Eieio, Barrier_MIPS_SYNC) -> LT
+  | (Barrier_Eieio, _)  -> LT
 
   | (Barrier_Isync, Barrier_Sync)   -> GT
   | (Barrier_Isync, Barrier_LwSync) -> GT
   | (Barrier_Isync, Barrier_Eieio)  -> GT
   | (Barrier_Isync, Barrier_Isync)  -> EQ
-  | (Barrier_Isync, Barrier_DMB)    -> LT
-  | (Barrier_Isync, Barrier_DMB_ST) -> LT
-  | (Barrier_Isync, Barrier_DMB_LD) -> LT
-  | (Barrier_Isync, Barrier_DSB)    -> LT
-  | (Barrier_Isync, Barrier_DSB_ST) -> LT
-  | (Barrier_Isync, Barrier_DSB_LD) -> LT
-  | (Barrier_Isync, Barrier_ISB)    -> LT
-  | (Barrier_Isync, Barrier_MIPS_SYNC) -> LT
+  | (Barrier_Isync, _)    -> LT
 
   | (Barrier_DMB, Barrier_Sync)   -> GT
   | (Barrier_DMB, Barrier_LwSync) -> GT
@@ -675,12 +646,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
   | (Barrier_DMB, Barrier_Isync)  -> GT
   | (Barrier_DMB, Barrier_DMB)    -> EQ
   | (Barrier_DMB, Barrier_DMB_ST) -> LT
-  | (Barrier_DMB, Barrier_DMB_LD) -> LT
-  | (Barrier_DMB, Barrier_DSB)    -> LT
-  | (Barrier_DMB, Barrier_DSB_ST) -> LT
-  | (Barrier_DMB, Barrier_DSB_LD) -> LT
-  | (Barrier_DMB, Barrier_ISB)    -> LT
-  | (Barrier_DMB, Barrier_MIPS_SYNC) -> LT
+  | (Barrier_DMB, _) -> LT
 
   | (Barrier_DMB_ST, Barrier_Sync)   -> GT
   | (Barrier_DMB_ST, Barrier_LwSync) -> GT
@@ -688,12 +654,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
   | (Barrier_DMB_ST, Barrier_Isync)  -> GT
   | (Barrier_DMB_ST, Barrier_DMB)    -> GT
   | (Barrier_DMB_ST, Barrier_DMB_ST) -> EQ
-  | (Barrier_DMB_ST, Barrier_DMB_LD) -> LT
-  | (Barrier_DMB_ST, Barrier_DSB)    -> LT
-  | (Barrier_DMB_ST, Barrier_DSB_ST) -> LT
-  | (Barrier_DMB_ST, Barrier_DSB_LD) -> LT
-  | (Barrier_DMB_ST, Barrier_ISB)    -> LT
-  | (Barrier_DMB_ST, Barrier_MIPS_SYNC) -> LT
+  | (Barrier_DMB_ST, _) -> LT
 
   | (Barrier_DMB_LD, Barrier_Sync)   -> GT
   | (Barrier_DMB_LD, Barrier_LwSync) -> GT
@@ -702,11 +663,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
   | (Barrier_DMB_LD, Barrier_DMB)    -> GT
   | (Barrier_DMB_LD, Barrier_DMB_ST) -> GT
   | (Barrier_DMB_LD, Barrier_DMB_LD) -> EQ
-  | (Barrier_DMB_LD, Barrier_DSB)    -> LT
-  | (Barrier_DMB_LD, Barrier_DSB_ST) -> LT
-  | (Barrier_DMB_LD, Barrier_DSB_LD) -> LT
-  | (Barrier_DMB_LD, Barrier_ISB)    -> LT
-  | (Barrier_DMB_LD, Barrier_MIPS_SYNC) -> LT
+  | (Barrier_DMB_LD, _)    -> LT
 
   | (Barrier_DSB, Barrier_Sync)   -> GT
   | (Barrier_DSB, Barrier_LwSync) -> GT
@@ -716,10 +673,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
   | (Barrier_DSB, Barrier_DMB_ST) -> GT
   | (Barrier_DSB, Barrier_DMB_LD) -> GT
   | (Barrier_DSB, Barrier_DSB)    -> EQ
-  | (Barrier_DSB, Barrier_DSB_ST) -> LT
-  | (Barrier_DSB, Barrier_DSB_LD) -> LT
-  | (Barrier_DSB, Barrier_ISB)    -> LT
-  | (Barrier_DSB, Barrier_MIPS_SYNC) -> LT
+  | (Barrier_DSB, _) -> LT
 
   | (Barrier_DSB_ST, Barrier_Sync)   -> GT
   | (Barrier_DSB_ST, Barrier_LwSync) -> GT
@@ -730,9 +684,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
   | (Barrier_DSB_ST, Barrier_DMB_LD) -> GT
   | (Barrier_DSB_ST, Barrier_DSB)    -> GT
   | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ
-  | (Barrier_DSB_ST, Barrier_DSB_LD) -> LT
-  | (Barrier_DSB_ST, Barrier_ISB)    -> LT
-  | (Barrier_DSB_ST, Barrier_MIPS_SYNC) -> LT
+  | (Barrier_DSB_ST, _) -> LT
 
   | (Barrier_DSB_LD, Barrier_Sync)   -> GT
   | (Barrier_DSB_LD, Barrier_LwSync) -> GT
@@ -744,8 +696,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
   | (Barrier_DSB_LD, Barrier_DSB)    -> GT
   | (Barrier_DSB_LD, Barrier_DSB_ST) -> GT
   | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ
-  | (Barrier_DSB_LD, Barrier_ISB)    -> LT
-  | (Barrier_DSB_LD, Barrier_MIPS_SYNC) -> LT
+  | (Barrier_DSB_LD, _)    -> LT
                           
   | (Barrier_ISB, Barrier_Sync)   -> GT
   | (Barrier_ISB, Barrier_LwSync) -> GT
@@ -760,18 +711,18 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
   | (Barrier_ISB, Barrier_ISB)    -> EQ
   | (Barrier_ISB, Barrier_MIPS_SYNC) -> LT
 
-  | (Barrier_ISB, Barrier_Sync)   -> GT
-  | (Barrier_ISB, Barrier_LwSync) -> GT
-  | (Barrier_ISB, Barrier_Eieio)  -> GT
-  | (Barrier_ISB, Barrier_Isync)  -> GT
-  | (Barrier_ISB, Barrier_DMB)    -> GT
-  | (Barrier_ISB, Barrier_DMB_ST) -> GT
-  | (Barrier_ISB, Barrier_DMB_LD) -> GT
-  | (Barrier_ISB, Barrier_DSB)    -> GT
-  | (Barrier_ISB, Barrier_DSB_ST) -> GT
-  | (Barrier_ISB, Barrier_DSB_LD) -> GT
-  | (Barrier_ISB, Barrier_ISB)    -> GT
-  | (Barrier_ISB, Barrier_MIPS_SYNC) -> EQ
+  | (Barrier_MIPS_SYNC, Barrier_Sync)   -> GT
+  | (Barrier_MIPS_SYNC, Barrier_LwSync) -> GT
+  | (Barrier_MIPS_SYNC, Barrier_Eieio)  -> GT
+  | (Barrier_MIPS_SYNC, Barrier_Isync)  -> GT
+  | (Barrier_MIPS_SYNC, Barrier_DMB)    -> GT
+  | (Barrier_MIPS_SYNC, Barrier_DMB_ST) -> GT
+  | (Barrier_MIPS_SYNC, Barrier_DMB_LD) -> GT
+  | (Barrier_MIPS_SYNC, Barrier_DSB)    -> GT
+  | (Barrier_MIPS_SYNC, Barrier_DSB_ST) -> GT
+  | (Barrier_MIPS_SYNC, Barrier_DSB_LD) -> GT
+  | (Barrier_MIPS_SYNC, Barrier_ISB)    -> GT
+  | (Barrier_MIPS_SYNC, Barrier_MIPS_SYNC) -> EQ
   end
 let inline {ocaml} barrier_kindCompare = defaultCompare
 
@@ -1260,17 +1211,25 @@ type nia =
                                 instructions *)
 
 let niaCompare n1 n2 = match (n1,n2) with
-  | (NIA_successor,NIA_successor) -> EQ
+  | (NIA_successor, NIA_successor) -> EQ
+  | (NIA_successor, _) -> LT
+  | (NIA_concrete_address _, NIA_successor) -> GT
   | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2
-  | (NIA_LR,NIA_LR) -> EQ
-  | (NIA_CTR,NIA_CTR) -> EQ
-  | (NIA_register r1,NIA_register r2) -> compare r1 r2
-
-  | (NIA_successor,_) -> LT
-  | (NIA_concrete_address _,_) -> LT
-  | (NIA_LR,_) -> LT
-  | (NIA_CTR,_) -> LT
-  | (_,_) -> GT
+  | (NIA_concrete_address _, _) -> LT
+  | (NIA_LR, NIA_successor) -> GT
+  | (NIA_LR, NIA_concrete_address _) -> GT
+  | (NIA_LR, NIA_LR) -> EQ
+  | (NIA_LR, _) -> LT
+  | (NIA_CTR, NIA_successor) -> GT
+  | (NIA_CTR, NIA_concrete_address _) -> GT
+  | (NIA_CTR, NIA_LR) -> GT
+  | (NIA_CTR, NIA_CTR) -> EQ
+  | (NIA_CTR, NIA_register _) -> LT
+  | (NIA_register _, NIA_successor) -> GT
+  | (NIA_register _, NIA_concrete_address _) -> GT
+  | (NIA_register _, NIA_LR) -> GT
+  | (NIA_register _, NIA_CTR) -> GT
+  | (NIA_register r1, NIA_register r2) -> compare r1 r2
   end
 
 instance (Ord nia)
@@ -1300,11 +1259,12 @@ type dia =
 
 let diaCompare d1 d2 = match (d1, d2) with
   | (DIA_none, DIA_none) -> EQ
+  | (DIA_none, _) -> LT
+  | (DIA_concrete_address a1, DIA_none) -> GT
   | (DIA_concrete_address a1, DIA_concrete_address a2) -> compare a1 a2
+  | (DIA_concrete_address a1, _) -> LT
   | (DIA_register r1, DIA_register r2) -> compare r1 r2
-  | (DIA_none, _) -> LT
-  | (DIA_concrete_address _, _) -> LT
-  | (DIA_register _, _) -> LT
+  | (DIA_register _, _) -> GT
 end
 
 instance (Ord dia)
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 6ecf2be1..f5680cb8 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2036,37 +2036,36 @@ let langlebar = string "<|"
 let ranglebar = string "|>"
 let anglebars = enclose langlebar ranglebar
 
-module M = Map.Make(String)
-
-let keywords =
-  (List.fold_left (fun m x -> M.add x (x ^ "_") m) (M.empty))
-    [
-      "assert";
-      "lsl";
-      "lsr";
-      "asr";
-      "type";
-      "fun";
-      "function";
-      "raise";
-      "try";
-      "match";
-      "with";
-      "field";
-      "LT";
-      "GT";
-      "EQ";
-      "integer";
-    ]
-
-let fix_id i = if M.mem i keywords then M.find i keywords else i
+
+let fix_id name = match name with
+  | "assert"
+  | "lsl"
+  | "lsr"
+  | "asr"
+  | "type"
+  | "fun"
+  | "function"
+  | "raise"
+  | "try"
+  | "match"
+  | "with"
+  | "field"
+  | "LT"
+  | "GT"
+  | "EQ"
+  | "integer"
+    -> name ^ "'"
+  | _ -> name
+
 
 let doc_id_lem (Id_aux(i,_)) =
   match i with
   | Id i ->
      (* this not the right place to do this, just a workaround *)
-     if i.[0] = '\'' || is_number(i.[0]) then
-       string ("_" ^ i)
+     if i.[0] = '\'' then
+       string ((String.sub i 1 (String.length i - 1)) ^ "'")
+     else if is_number(i.[0]) then
+       string ("v" ^ i ^ "'")
      else
        string (fix_id i)
   | DeIid x ->
@@ -2076,8 +2075,8 @@ let doc_id_lem (Id_aux(i,_)) =
 
 let doc_id_lem_type (Id_aux(i,_)) =
   match i with
-  | Id("int") -> string "SV.ii"
-  | Id("nat") -> string "SV.ii"
+  | Id("int") -> string "ii"
+  | Id("nat") -> string "ii"
   | Id("option") -> string "maybe"
   | Id i -> string (fix_id i)
   | DeIid x ->
@@ -2180,10 +2179,10 @@ let doc_typ_lem, doc_atomic_typ_lem =
 let doc_lit_lem in_pat (L_aux(lit,l)) a =
   utf8string (match lit with
   | L_unit  -> "()"
-  | L_zero  -> "O"
-  | L_one   -> "I"
-  | L_false -> "O"
-  | L_true  -> "I"
+  | L_zero  -> "B0"
+  | L_one   -> "B1"
+  | L_false -> "B0"
+  | L_true  -> "B1"
   | L_num i ->
      let ipp = string_of_int i in
      if in_pat then "("^ipp^":nn)"
@@ -2195,7 +2194,7 @@ let doc_lit_lem in_pat (L_aux(lit,l)) a =
      let (Base ((_,{t = t}),_,_,_,_,_)) = a in
      (match t with
       | Tid "bit"
-      | Tabbrev ({t = Tid "bit"},_) -> "Undef"
+      | Tabbrev ({t = Tid "bit"},_) -> "BU"
       | Tapp ("register",_)
       | Tabbrev ({t = Tapp ("register",_)},_) -> "UndefinedRegister 0"
       | Tid "string"
@@ -2568,7 +2567,7 @@ let doc_exp_lem, doc_let_lem =
        let default_string =
          match default with
          | Def_val_empty ->
-            if is_bit_vector t then string "Undef"
+            if is_bit_vector t then string "BU"
             else failwith "E_vector_indexed of non-bitvector type without default argument"
          | Def_val_dec e ->
             let (Base ((_,{t = t}),_,_,_,_,_)) = dannot in
@@ -3007,7 +3006,9 @@ let get_id = function
   | [] -> failwith "FD_function with empty list"
   | (FCL_aux (FCL_Funcl (id,_,_),_))::_ -> id
 
-let doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),_)) =
+module StringSet = Set.Make(String)
+
+let rec doc_fundef_lem regtypes (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),_)] ->
@@ -3020,12 +3021,47 @@ let doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),_)) =
   | _ ->
     let id = get_id fcls in
     (*    let sep = hardline ^^ pipe ^^ space in *)
-    let clauses =
-      (separate_map (break 1))
-        (fun fcl -> separate space [pipe;doc_funcl_lem regtypes fcl]) fcls in
-    (prefix 2 1)
-      ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"])
-      (clauses ^/^ string "end")
+    match id with
+    | Id_aux (Id fname,idl)
+      when fname = "execute" || fname = "initial_analysis" ->
+      let (_,auxiliary_functions,clauses) = 
+        List.fold_left 
+          (fun (already_used_fnames,auxiliary_functions,clauses) funcl ->
+            match funcl with
+            | FCL_aux (FCL_Funcl (Id_aux (Id _,l),pat,exp),annot) ->
+               let (P_aux (P_app (Id_aux (Id ctor,l),argspat),pannot)) = pat in
+               let rec pick_name_not_clashing_with already_used candidate =
+                 if StringSet.mem candidate already_used then
+                   pick_name_not_clashing_with already_used (candidate ^ "'")
+                 else candidate in
+               let aux_fname = pick_name_not_clashing_with already_used_fnames (fname ^ "_" ^ ctor) in
+               let already_used_fnames = StringSet.add aux_fname already_used_fnames in
+               let fcl = FCL_aux (FCL_Funcl (Id_aux (Id aux_fname,l),
+                                             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
+               let clauses =
+                 clauses ^^ (break 1) ^^
+                   (separate space
+                      [pipe;doc_pat_lem regtypes false pat;arrow;
+                       string aux_fname;
+                       doc_pat_lem regtypes true (P_aux (P_tup argspat, pannot))]) in
+               (already_used_fnames,auxiliary_functions,clauses)
+          ) (StringSet.empty,empty,empty) fcls in
+
+      auxiliary_functions ^^ hardline ^^ hardline ^^
+      (prefix 2 1)
+        ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"])
+        (clauses ^/^ string "end")
+    | _ ->
+      let clauses =
+        (separate_map (break 1))
+          (fun fcl -> separate space [pipe;doc_funcl_lem regtypes fcl]) fcls in
+      (prefix 2 1)
+        ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"])
+        (clauses ^/^ string "end")
+      
 
 
 let doc_dec_lem (DEC_aux (reg,(l,annot))) =
@@ -3116,7 +3152,6 @@ let pp_defs_lem (types_file,types_modules) (prompt_file,prompt_modules) (state_f
              string "module SIA = Interp_ast"; hardline;
              hardline]
         else empty;
-        string "module SV = Sail_values"; hardline;
         typdefs]);
   (print prompt_file)
     (concat