aarch64_small: sort out types and names in hgen files

4 files changed, 156 insertions, 156 deletions

diff --git a/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen b/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen
index b8fe851c..2d0ac5e2 100644
--- a/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen
+++ b/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen
@@ -1,20 +1,20 @@
-| `AArch64Unallocated -> Unallocated
+| `AArch64Unallocated -> Unallocated ()
 | `AArch64TMStart t -> TMStart (translate_reg "t" t)
 
-| `AArch64TMCommit -> TMCommit
+| `AArch64TMCommit -> TMCommit ()
 
 | `AArch64TMAbort (retry,reason) ->
     TMAbort
-      (translate_boolean "retry" retry,
+      (translate_bool "retry" retry,
         translate_bit5 "reason" reason)
 
-| `AArch64TMTest -> TMTest
+| `AArch64TMTest -> TMTest ()
 
 | `AArch64ImplementationDefinedStopFetching ->
-    ImplementationDefinedStopFetching
+    ImplementationDefinedStopFetching ()
 
 | `AArch64ImplementationDefinedThreadStart ->
-    ImplementationDefinedThreadStart
+    ImplementationDefinedThreadStart ()
 
 | `AArch64ImplementationDefinedTestBeginEnd(isEnd) ->
     ImplementationDefinedTestBeginEnd
diff --git a/aarch64_small/gen/herdtools_types_to_shallow_types.hgen b/aarch64_small/gen/herdtools_types_to_shallow_types.hgen
index e14a37e3..6ca50f83 100644
--- a/aarch64_small/gen/herdtools_types_to_shallow_types.hgen
+++ b/aarch64_small/gen/herdtools_types_to_shallow_types.hgen
@@ -1,4 +1,4 @@
-open Sail_values
+open Sail2_values
 
 let is_inc = false
 
@@ -6,16 +6,16 @@ let translate_big_int bits (name : string) value =
   (name, Range0 (Some bits), IInt.bit_list_of_integer bits value)
 
 let translate_big_bit bits (name:string) value =
-  Sail_values.to_vec0 is_inc (Nat_big_num.of_int bits,value)
+  Sail2_values.bits_of_int (Nat_big_num.of_int bits) value
 
 let translate_int (size : int) (name:string) value = (Nat_big_num.of_int value)
 
 let translate_bits bits (name:string) value =
-  Sail_values.to_vec0 is_inc (Nat_big_num.of_int bits,Nat_big_num.of_int value)
+  Sail2_values.bits_of_int (Nat_big_num.of_int bits) (Nat_big_num.of_int value)
 
 let translate_bool _ = function
-  | true -> B1
-  | false -> B0
+  | true -> B10
+  | false -> B00
 
 let translate_reg_size name value =
   match value with
@@ -59,95 +59,95 @@ let translate_range8_64 = translate_int 7
 let translate_uinteger = translate_int 63
 
 let translate_extendType _ = function
-  | ExtendType_UXTB -> ArmV8_embed_types.ExtendType_UXTB
-  | ExtendType_UXTH -> ArmV8_embed_types.ExtendType_UXTH
-  | ExtendType_UXTW -> ArmV8_embed_types.ExtendType_UXTW
-  | ExtendType_UXTX -> ArmV8_embed_types.ExtendType_UXTX
-  | ExtendType_SXTB -> ArmV8_embed_types.ExtendType_SXTB
-  | ExtendType_SXTH -> ArmV8_embed_types.ExtendType_SXTH
-  | ExtendType_SXTW -> ArmV8_embed_types.ExtendType_SXTW
-  | ExtendType_SXTX -> ArmV8_embed_types.ExtendType_SXTX
+  | ExtendType_UXTB -> ArmV8_types.ExtendType_UXTB
+  | ExtendType_UXTH -> ArmV8_types.ExtendType_UXTH
+  | ExtendType_UXTW -> ArmV8_types.ExtendType_UXTW
+  | ExtendType_UXTX -> ArmV8_types.ExtendType_UXTX
+  | ExtendType_SXTB -> ArmV8_types.ExtendType_SXTB
+  | ExtendType_SXTH -> ArmV8_types.ExtendType_SXTH
+  | ExtendType_SXTW -> ArmV8_types.ExtendType_SXTW
+  | ExtendType_SXTX -> ArmV8_types.ExtendType_SXTX
 
 let translate_shiftType _ = function
-  | ShiftType_LSL -> ArmV8_embed_types.ShiftType_LSL
-  | ShiftType_LSR -> ArmV8_embed_types.ShiftType_LSR
-  | ShiftType_ASR -> ArmV8_embed_types.ShiftType_ASR
-  | ShiftType_ROR -> ArmV8_embed_types.ShiftType_ROR
+  | ShiftType_LSL -> ArmV8_types.ShiftType_LSL
+  | ShiftType_LSR -> ArmV8_types.ShiftType_LSR
+  | ShiftType_ASR -> ArmV8_types.ShiftType_ASR
+  | ShiftType_ROR -> ArmV8_types.ShiftType_ROR
 
 let translate_logicalOp _ = function
-  | LogicalOp_AND -> ArmV8_embed_types.LogicalOp_AND
-  | LogicalOp_EOR -> ArmV8_embed_types.LogicalOp_EOR
-  | LogicalOp_ORR -> ArmV8_embed_types.LogicalOp_ORR
+  | LogicalOp_AND -> ArmV8_types.LogicalOp_AND
+  | LogicalOp_EOR -> ArmV8_types.LogicalOp_EOR
+  | LogicalOp_ORR -> ArmV8_types.LogicalOp_ORR
 
 let translate_branchType _ = function
-  | BranchType_CALL -> ArmV8_embed_types.BranchType_CALL
-  | BranchType_ERET -> ArmV8_embed_types.BranchType_ERET
-  | BranchType_DBGEXIT -> ArmV8_embed_types.BranchType_DBGEXIT
-  | BranchType_RET -> ArmV8_embed_types.BranchType_RET
-  | BranchType_JMP -> ArmV8_embed_types.BranchType_JMP
-  | BranchType_EXCEPTION -> ArmV8_embed_types.BranchType_EXCEPTION
-  | BranchType_UNKNOWN -> ArmV8_embed_types.BranchType_UNKNOWN
+  | BranchType_CALL -> ArmV8_types.BranchType_CALL
+  | BranchType_ERET -> ArmV8_types.BranchType_ERET
+  | BranchType_DBGEXIT -> ArmV8_types.BranchType_DBGEXIT
+  | BranchType_RET -> ArmV8_types.BranchType_RET
+  | BranchType_JMP -> ArmV8_types.BranchType_JMP
+  | BranchType_EXCEPTION -> ArmV8_types.BranchType_EXCEPTION
+  | BranchType_UNKNOWN -> ArmV8_types.BranchType_UNKNOWN
 
 let translate_countOp _ = function
-  | CountOp_CLZ -> ArmV8_embed_types.CountOp_CLZ
-  | CountOp_CLS -> ArmV8_embed_types.CountOp_CLS
-  | CountOp_CNT -> ArmV8_embed_types.CountOp_CNT
+  | CountOp_CLZ -> ArmV8_types.CountOp_CLZ
+  | CountOp_CLS -> ArmV8_types.CountOp_CLS
+  | CountOp_CNT -> ArmV8_types.CountOp_CNT
 
 let translate_memBarrierOp _ = function
-  | MemBarrierOp_DSB -> ArmV8_embed_types.MemBarrierOp_DSB
-  | MemBarrierOp_DMB -> ArmV8_embed_types.MemBarrierOp_DMB
-  | MemBarrierOp_ISB -> ArmV8_embed_types.MemBarrierOp_ISB
+  | MemBarrierOp_DSB -> ArmV8_types.MemBarrierOp_DSB
+  | MemBarrierOp_DMB -> ArmV8_types.MemBarrierOp_DMB
+  | MemBarrierOp_ISB -> ArmV8_types.MemBarrierOp_ISB
 
 let translate_mBReqDomain _ = function
-  | MBReqDomain_Nonshareable -> ArmV8_embed_types.MBReqDomain_Nonshareable
-  | MBReqDomain_InnerShareable -> ArmV8_embed_types.MBReqDomain_InnerShareable
-  | MBReqDomain_OuterShareable -> ArmV8_embed_types.MBReqDomain_OuterShareable
-  | MBReqDomain_FullSystem -> ArmV8_embed_types.MBReqDomain_FullSystem
+  | MBReqDomain_Nonshareable -> ArmV8_types.MBReqDomain_Nonshareable
+  | MBReqDomain_InnerShareable -> ArmV8_types.MBReqDomain_InnerShareable
+  | MBReqDomain_OuterShareable -> ArmV8_types.MBReqDomain_OuterShareable
+  | MBReqDomain_FullSystem -> ArmV8_types.MBReqDomain_FullSystem
 
 let translate_mBReqTypes _ = function
-  | MBReqTypes_Reads -> ArmV8_embed_types.MBReqTypes_Reads
-  | MBReqTypes_Writes -> ArmV8_embed_types.MBReqTypes_Writes
-  | MBReqTypes_All -> ArmV8_embed_types.MBReqTypes_All
+  | MBReqTypes_Reads -> ArmV8_types.MBReqTypes_Reads
+  | MBReqTypes_Writes -> ArmV8_types.MBReqTypes_Writes
+  | MBReqTypes_All -> ArmV8_types.MBReqTypes_All
 
 let translate_systemHintOp _ = function
-  | SystemHintOp_NOP -> ArmV8_embed_types.SystemHintOp_NOP
-  | SystemHintOp_YIELD -> ArmV8_embed_types.SystemHintOp_YIELD
-  | SystemHintOp_WFE -> ArmV8_embed_types.SystemHintOp_WFE
-  | SystemHintOp_WFI -> ArmV8_embed_types.SystemHintOp_WFI
-  | SystemHintOp_SEV -> ArmV8_embed_types.SystemHintOp_SEV
-  | SystemHintOp_SEVL -> ArmV8_embed_types.SystemHintOp_SEVL
+  | SystemHintOp_NOP -> ArmV8_types.SystemHintOp_NOP
+  | SystemHintOp_YIELD -> ArmV8_types.SystemHintOp_YIELD
+  | SystemHintOp_WFE -> ArmV8_types.SystemHintOp_WFE
+  | SystemHintOp_WFI -> ArmV8_types.SystemHintOp_WFI
+  | SystemHintOp_SEV -> ArmV8_types.SystemHintOp_SEV
+  | SystemHintOp_SEVL -> ArmV8_types.SystemHintOp_SEVL
 
 let translate_accType _ = function
-  | AccType_NORMAL -> ArmV8_embed_types.AccType_NORMAL
-  | AccType_VEC -> ArmV8_embed_types.AccType_VEC
-  | AccType_STREAM -> ArmV8_embed_types.AccType_STREAM
-  | AccType_VECSTREAM -> ArmV8_embed_types.AccType_VECSTREAM
-  | AccType_ATOMIC -> ArmV8_embed_types.AccType_ATOMIC
-  | AccType_ORDERED -> ArmV8_embed_types.AccType_ORDERED
-  | AccType_UNPRIV -> ArmV8_embed_types.AccType_UNPRIV
-  | AccType_IFETCH -> ArmV8_embed_types.AccType_IFETCH
-  | AccType_PTW -> ArmV8_embed_types.AccType_PTW
-  | AccType_DC -> ArmV8_embed_types.AccType_DC
-  | AccType_IC -> ArmV8_embed_types.AccType_IC
-  | AccType_AT -> ArmV8_embed_types.AccType_AT
+  | AccType_NORMAL -> ArmV8_types.AccType_NORMAL
+  | AccType_VEC -> ArmV8_types.AccType_VEC
+  | AccType_STREAM -> ArmV8_types.AccType_STREAM
+  | AccType_VECSTREAM -> ArmV8_types.AccType_VECSTREAM
+  | AccType_ATOMIC -> ArmV8_types.AccType_ATOMIC
+  | AccType_ORDERED -> ArmV8_types.AccType_ORDERED
+  | AccType_UNPRIV -> ArmV8_types.AccType_UNPRIV
+  | AccType_IFETCH -> ArmV8_types.AccType_IFETCH
+  | AccType_PTW -> ArmV8_types.AccType_PTW
+  | AccType_DC -> ArmV8_types.AccType_DC
+  | AccType_IC -> ArmV8_types.AccType_IC
+  | AccType_AT -> ArmV8_types.AccType_AT
 
 let translate_memOp _ = function
-  | MemOp_LOAD -> ArmV8_embed_types.MemOp_LOAD
-  | MemOp_STORE -> ArmV8_embed_types.MemOp_STORE
-  | MemOp_PREFETCH -> ArmV8_embed_types.MemOp_PREFETCH
+  | MemOp_LOAD -> ArmV8_types.MemOp_LOAD
+  | MemOp_STORE -> ArmV8_types.MemOp_STORE
+  | MemOp_PREFETCH -> ArmV8_types.MemOp_PREFETCH
 
 let translate_moveWideOp _ = function
-  | MoveWideOp_N -> ArmV8_embed_types.MoveWideOp_N
-  | MoveWideOp_Z -> ArmV8_embed_types.MoveWideOp_Z
-  | MoveWideOp_K -> ArmV8_embed_types.MoveWideOp_K
+  | MoveWideOp_N -> ArmV8_types.MoveWideOp_N
+  | MoveWideOp_Z -> ArmV8_types.MoveWideOp_Z
+  | MoveWideOp_K -> ArmV8_types.MoveWideOp_K
 
 let translate_revOp _ = function
-  | RevOp_RBIT -> ArmV8_embed_types.RevOp_RBIT
-  | RevOp_REV16 -> ArmV8_embed_types.RevOp_REV16
-  | RevOp_REV32 -> ArmV8_embed_types.RevOp_REV32
-  | RevOp_REV64 -> ArmV8_embed_types.RevOp_REV64
+  | RevOp_RBIT -> ArmV8_types.RevOp_RBIT
+  | RevOp_REV16 -> ArmV8_types.RevOp_REV16
+  | RevOp_REV32 -> ArmV8_types.RevOp_REV32
+  | RevOp_REV64 -> ArmV8_types.RevOp_REV64
 
 let translate_pSTATEField _ = function
-  | PSTATEField_DAIFSet -> ArmV8_embed_types.PSTATEField_DAIFSet
-  | PSTATEField_DAIFClr -> ArmV8_embed_types.PSTATEField_DAIFClr
-  | PSTATEField_SP -> ArmV8_embed_types.PSTATEField_SP
+  | PSTATEField_DAIFSet -> ArmV8_types.PSTATEField_DAIFSet
+  | PSTATEField_DAIFClr -> ArmV8_types.PSTATEField_DAIFClr
+  | PSTATEField_SP -> ArmV8_types.PSTATEField_SP
diff --git a/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen b/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen
index 55179a97..96b74b4f 100644
--- a/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen
+++ b/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen
@@ -1,20 +1,20 @@
-| Unallocated -> `AArch64Unallocated
+| Unallocated () -> `AArch64Unallocated
 
 | TMStart t ->
   `AArch64TMStart (translate_out_regzr Set64 t)
 
-| TMCommit -> `AArch64TMCommit
+| TMCommit () -> `AArch64TMCommit
 
 | TMAbort (retry, reason) ->
   `AArch64TMAbort ( translate_out_bool retry,
                     translate_out_bits reason)
 
-| TMTest -> `AArch64TMTest
+| TMTest () -> `AArch64TMTest
 
-| ImplementationDefinedStopFetching ->
+| ImplementationDefinedStopFetching () ->
   `AArch64ImplementationDefinedStopFetching
 
-| ImplementationDefinedThreadStart ->
+| ImplementationDefinedThreadStart () ->
   `AArch64ImplementationDefinedThreadStart
 
 | ImplementationDefinedTestBeginEnd (isEnd) ->
diff --git a/aarch64_small/gen/shallow_types_to_herdtools_types.hgen b/aarch64_small/gen/shallow_types_to_herdtools_types.hgen
index 771f52ac..a26879b4 100644
--- a/aarch64_small/gen/shallow_types_to_herdtools_types.hgen
+++ b/aarch64_small/gen/shallow_types_to_herdtools_types.hgen
@@ -1,17 +1,17 @@
-let translate_out_big_int_bits x = Sail_values.unsigned x
+let translate_out_big_int_bits bits = (match Sail2_values.unsigned_of_bits bits with Some x -> x | None -> failwith "unsigned_of_bits returned None")
 
-let translate_out_big_bit = Sail_values.unsigned
+let translate_out_big_bit bits = (match Sail2_values.unsigned_of_bits bits with Some x -> x | None -> failwith "unsigned_of_bits returned None")
 
-let translate_out_signed_big_bit = Sail_values.signed
+let translate_out_signed_big_bit bits = (match Sail2_values.signed_of_bits bits with Some x -> x | None -> failwith "signed_of_bits returned None")
 
 let translate_out_int inst = (Nat_big_num.to_int inst)
 
-let translate_out_bits bits = Nat_big_num.to_int (Sail_values.unsigned bits)
+let translate_out_bits bits = Nat_big_num.to_int (match Sail2_values.unsigned_of_bits bits with Some x -> x | None -> failwith "unsigned_of_bits returned None")
 
 let translate_out_bool = function
-  | Sail_values.B1 -> true
-  | Sail_values.B0 -> false
-  | Sail_values.BU -> failwith "translate_out_bool Undef"
+  | Sail2_values.B10 -> true
+  | Sail2_values.B00 -> false
+  | Sail2_values.BU0 -> failwith "translate_out_bool Undef"
 
 let translate_out_enum (name,_,bits) =
     Nat_big_num.to_int (IInt.integer_of_bit_list bits)
@@ -44,7 +44,7 @@ let translate_out_regzrbyext regsize extend_type reg =  begin match extend_type
   end
 
 let translate_out_reg_size_bits bits =
-  match Nat_big_num.to_int (Sail_values.length bits) with
+  match (List.length bits) with
     | 32 -> R32Bits (translate_out_bits bits)
     | 64 -> R64Bits (translate_out_big_bit bits)
     | _ -> assert false
@@ -58,97 +58,97 @@ let translate_out_data_size inst =
     | _ -> assert false
 
 let translate_out_extendType = function
-    | ArmV8_embed_types.ExtendType_UXTB -> ExtendType_UXTB
-    | ArmV8_embed_types.ExtendType_UXTH -> ExtendType_UXTH
-    | ArmV8_embed_types.ExtendType_UXTW -> ExtendType_UXTW
-    | ArmV8_embed_types.ExtendType_UXTX -> ExtendType_UXTX
-    | ArmV8_embed_types.ExtendType_SXTB -> ExtendType_SXTB
-    | ArmV8_embed_types.ExtendType_SXTH -> ExtendType_SXTH
-    | ArmV8_embed_types.ExtendType_SXTW -> ExtendType_SXTW
-    | ArmV8_embed_types.ExtendType_SXTX -> ExtendType_SXTX
+    | ArmV8_types.ExtendType_UXTB -> ExtendType_UXTB
+    | ArmV8_types.ExtendType_UXTH -> ExtendType_UXTH
+    | ArmV8_types.ExtendType_UXTW -> ExtendType_UXTW
+    | ArmV8_types.ExtendType_UXTX -> ExtendType_UXTX
+    | ArmV8_types.ExtendType_SXTB -> ExtendType_SXTB
+    | ArmV8_types.ExtendType_SXTH -> ExtendType_SXTH
+    | ArmV8_types.ExtendType_SXTW -> ExtendType_SXTW
+    | ArmV8_types.ExtendType_SXTX -> ExtendType_SXTX
 
 let translate_out_shiftType = function
-    | ArmV8_embed_types.ShiftType_LSL -> ShiftType_LSL
-    | ArmV8_embed_types.ShiftType_LSR -> ShiftType_LSR
-    | ArmV8_embed_types.ShiftType_ASR -> ShiftType_ASR
-    | ArmV8_embed_types.ShiftType_ROR -> ShiftType_ROR
+    | ArmV8_types.ShiftType_LSL -> ShiftType_LSL
+    | ArmV8_types.ShiftType_LSR -> ShiftType_LSR
+    | ArmV8_types.ShiftType_ASR -> ShiftType_ASR
+    | ArmV8_types.ShiftType_ROR -> ShiftType_ROR
 
 let translate_out_logicalOp = function
-    | ArmV8_embed_types.LogicalOp_AND -> LogicalOp_AND
-    | ArmV8_embed_types.LogicalOp_EOR -> LogicalOp_EOR
-    | ArmV8_embed_types.LogicalOp_ORR -> LogicalOp_ORR
+    | ArmV8_types.LogicalOp_AND -> LogicalOp_AND
+    | ArmV8_types.LogicalOp_EOR -> LogicalOp_EOR
+    | ArmV8_types.LogicalOp_ORR -> LogicalOp_ORR
 
 let translate_out_branchType = function
-      | ArmV8_embed_types.BranchType_CALL -> BranchType_CALL
-      | ArmV8_embed_types.BranchType_ERET -> BranchType_ERET
-      | ArmV8_embed_types.BranchType_DBGEXIT -> BranchType_DBGEXIT
-      | ArmV8_embed_types.BranchType_RET -> BranchType_RET
-      | ArmV8_embed_types.BranchType_JMP -> BranchType_JMP
-      | ArmV8_embed_types.BranchType_EXCEPTION -> BranchType_EXCEPTION
-      | ArmV8_embed_types.BranchType_UNKNOWN -> BranchType_UNKNOWN
+      | ArmV8_types.BranchType_CALL -> BranchType_CALL
+      | ArmV8_types.BranchType_ERET -> BranchType_ERET
+      | ArmV8_types.BranchType_DBGEXIT -> BranchType_DBGEXIT
+      | ArmV8_types.BranchType_RET -> BranchType_RET
+      | ArmV8_types.BranchType_JMP -> BranchType_JMP
+      | ArmV8_types.BranchType_EXCEPTION -> BranchType_EXCEPTION
+      | ArmV8_types.BranchType_UNKNOWN -> BranchType_UNKNOWN
 
 let translate_out_countOp = function
-    | ArmV8_embed_types.CountOp_CLZ -> CountOp_CLZ
-    | ArmV8_embed_types.CountOp_CLS -> CountOp_CLS
-    | ArmV8_embed_types.CountOp_CNT -> CountOp_CNT
+    | ArmV8_types.CountOp_CLZ -> CountOp_CLZ
+    | ArmV8_types.CountOp_CLS -> CountOp_CLS
+    | ArmV8_types.CountOp_CNT -> CountOp_CNT
 
 let translate_out_memBarrierOp = function
-    | ArmV8_embed_types.MemBarrierOp_DSB -> MemBarrierOp_DSB
-    | ArmV8_embed_types.MemBarrierOp_DMB -> MemBarrierOp_DMB
-    | ArmV8_embed_types.MemBarrierOp_ISB -> MemBarrierOp_ISB
+    | ArmV8_types.MemBarrierOp_DSB -> MemBarrierOp_DSB
+    | ArmV8_types.MemBarrierOp_DMB -> MemBarrierOp_DMB
+    | ArmV8_types.MemBarrierOp_ISB -> MemBarrierOp_ISB
 
 let translate_out_mBReqDomain = function
-    | ArmV8_embed_types.MBReqDomain_Nonshareable -> MBReqDomain_Nonshareable
-    | ArmV8_embed_types.MBReqDomain_InnerShareable -> MBReqDomain_InnerShareable
-    | ArmV8_embed_types.MBReqDomain_OuterShareable -> MBReqDomain_OuterShareable
-    | ArmV8_embed_types.MBReqDomain_FullSystem -> MBReqDomain_FullSystem
+    | ArmV8_types.MBReqDomain_Nonshareable -> MBReqDomain_Nonshareable
+    | ArmV8_types.MBReqDomain_InnerShareable -> MBReqDomain_InnerShareable
+    | ArmV8_types.MBReqDomain_OuterShareable -> MBReqDomain_OuterShareable
+    | ArmV8_types.MBReqDomain_FullSystem -> MBReqDomain_FullSystem
 
 let translate_out_mBReqTypes = function
-    | ArmV8_embed_types.MBReqTypes_Reads -> MBReqTypes_Reads
-    | ArmV8_embed_types.MBReqTypes_Writes -> MBReqTypes_Writes
-    | ArmV8_embed_types.MBReqTypes_All -> MBReqTypes_All
+    | ArmV8_types.MBReqTypes_Reads -> MBReqTypes_Reads
+    | ArmV8_types.MBReqTypes_Writes -> MBReqTypes_Writes
+    | ArmV8_types.MBReqTypes_All -> MBReqTypes_All
 
 let translate_out_systemHintOp = function
-    | ArmV8_embed_types.SystemHintOp_NOP -> SystemHintOp_NOP
-    | ArmV8_embed_types.SystemHintOp_YIELD -> SystemHintOp_YIELD
-    | ArmV8_embed_types.SystemHintOp_WFE -> SystemHintOp_WFE
-    | ArmV8_embed_types.SystemHintOp_WFI -> SystemHintOp_WFI
-    | ArmV8_embed_types.SystemHintOp_SEV -> SystemHintOp_SEV
-    | ArmV8_embed_types.SystemHintOp_SEVL -> SystemHintOp_SEVL
+    | ArmV8_types.SystemHintOp_NOP -> SystemHintOp_NOP
+    | ArmV8_types.SystemHintOp_YIELD -> SystemHintOp_YIELD
+    | ArmV8_types.SystemHintOp_WFE -> SystemHintOp_WFE
+    | ArmV8_types.SystemHintOp_WFI -> SystemHintOp_WFI
+    | ArmV8_types.SystemHintOp_SEV -> SystemHintOp_SEV
+    | ArmV8_types.SystemHintOp_SEVL -> SystemHintOp_SEVL
 
 let translate_out_accType = function
-    | ArmV8_embed_types.AccType_NORMAL  -> AccType_NORMAL
-    | ArmV8_embed_types.AccType_VEC  -> AccType_VEC
-    | ArmV8_embed_types.AccType_STREAM  -> AccType_STREAM
-    | ArmV8_embed_types.AccType_VECSTREAM  -> AccType_VECSTREAM
-    | ArmV8_embed_types.AccType_ATOMIC  -> AccType_ATOMIC
-    | ArmV8_embed_types.AccType_ORDERED  -> AccType_ORDERED
-    | ArmV8_embed_types.AccType_UNPRIV  -> AccType_UNPRIV
-    | ArmV8_embed_types.AccType_IFETCH  -> AccType_IFETCH
-    | ArmV8_embed_types.AccType_PTW  -> AccType_PTW
-    | ArmV8_embed_types.AccType_DC  -> AccType_DC
-    | ArmV8_embed_types.AccType_IC -> AccType_IC
-    | ArmV8_embed_types.AccType_AT -> AccType_AT
+    | ArmV8_types.AccType_NORMAL  -> AccType_NORMAL
+    | ArmV8_types.AccType_VEC  -> AccType_VEC
+    | ArmV8_types.AccType_STREAM  -> AccType_STREAM
+    | ArmV8_types.AccType_VECSTREAM  -> AccType_VECSTREAM
+    | ArmV8_types.AccType_ATOMIC  -> AccType_ATOMIC
+    | ArmV8_types.AccType_ORDERED  -> AccType_ORDERED
+    | ArmV8_types.AccType_UNPRIV  -> AccType_UNPRIV
+    | ArmV8_types.AccType_IFETCH  -> AccType_IFETCH
+    | ArmV8_types.AccType_PTW  -> AccType_PTW
+    | ArmV8_types.AccType_DC  -> AccType_DC
+    | ArmV8_types.AccType_IC -> AccType_IC
+    | ArmV8_types.AccType_AT -> AccType_AT
 
 let translate_out_memOp = function
-    | ArmV8_embed_types.MemOp_LOAD -> MemOp_LOAD
-    | ArmV8_embed_types.MemOp_STORE -> MemOp_STORE
-    | ArmV8_embed_types.MemOp_PREFETCH -> MemOp_PREFETCH
+    | ArmV8_types.MemOp_LOAD -> MemOp_LOAD
+    | ArmV8_types.MemOp_STORE -> MemOp_STORE
+    | ArmV8_types.MemOp_PREFETCH -> MemOp_PREFETCH
 
 
 let translate_out_moveWideOp = function
-    | ArmV8_embed_types.MoveWideOp_N -> MoveWideOp_N
-    | ArmV8_embed_types.MoveWideOp_Z -> MoveWideOp_Z
-    | ArmV8_embed_types.MoveWideOp_K -> MoveWideOp_K
+    | ArmV8_types.MoveWideOp_N -> MoveWideOp_N
+    | ArmV8_types.MoveWideOp_Z -> MoveWideOp_Z
+    | ArmV8_types.MoveWideOp_K -> MoveWideOp_K
 
 let translate_out_revOp = function
-    | ArmV8_embed_types.RevOp_RBIT -> RevOp_RBIT
-    | ArmV8_embed_types.RevOp_REV16 -> RevOp_REV16
-    | ArmV8_embed_types.RevOp_REV32 -> RevOp_REV32
-    | ArmV8_embed_types.RevOp_REV64 -> RevOp_REV64
+    | ArmV8_types.RevOp_RBIT -> RevOp_RBIT
+    | ArmV8_types.RevOp_REV16 -> RevOp_REV16
+    | ArmV8_types.RevOp_REV32 -> RevOp_REV32
+    | ArmV8_types.RevOp_REV64 -> RevOp_REV64
 
 let translate_out_pSTATEField = function
-    | ArmV8_embed_types.PSTATEField_DAIFSet -> PSTATEField_DAIFSet
-    | ArmV8_embed_types.PSTATEField_DAIFClr -> PSTATEField_DAIFClr
-    | ArmV8_embed_types.PSTATEField_SP -> PSTATEField_SP
+    | ArmV8_types.PSTATEField_DAIFSet -> PSTATEField_DAIFSet
+    | ArmV8_types.PSTATEField_DAIFClr -> PSTATEField_DAIFClr
+    | ArmV8_types.PSTATEField_SP -> PSTATEField_SP