checking in in-progress translation of Shaked's handwritten sail1 ARM model to sail2

1 files changed, 702 insertions, 0 deletions

diff --git a/aarch64_small/armV8_toFromInterp.lem b/aarch64_small/armV8_toFromInterp.lem
new file mode 100644
index 00000000..0ce3f7f5
--- /dev/null
+++ b/aarch64_small/armV8_toFromInterp.lem
@@ -0,0 +1,702 @@
+(*Generated by Sail from armV8.sail.*)
+open import Pervasives_extra
+open import Sail_impl_base
+open import Sail_values
+open import ArmV8_embed_types
+open import ArmV8_extras_embed
+     import Interp
+     import Interp_ast
+open import Deep_shallow_convert
+let AccTypeToInterpValue = function
+  | AccType_NORMAL -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_NORMAL") Interp_ast.Unknown) (Interp_ast.T_id "AccType") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | AccType_VEC -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_VEC") Interp_ast.Unknown) (Interp_ast.T_id "AccType") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | AccType_STREAM -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_STREAM") Interp_ast.Unknown) (Interp_ast.T_id "AccType") (Interp_ast.C_Enum 2) (toInterpValue ())
+  | AccType_VECSTREAM -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_VECSTREAM") Interp_ast.Unknown) (Interp_ast.T_id "AccType") (Interp_ast.C_Enum 3) (toInterpValue ())
+  | AccType_ATOMIC -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_ATOMIC") Interp_ast.Unknown) (Interp_ast.T_id "AccType") (Interp_ast.C_Enum 4) (toInterpValue ())
+  | AccType_ORDERED -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_ORDERED") Interp_ast.Unknown) (Interp_ast.T_id "AccType") (Interp_ast.C_Enum 5) (toInterpValue ())
+  | AccType_UNPRIV -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_UNPRIV") Interp_ast.Unknown) (Interp_ast.T_id "AccType") (Interp_ast.C_Enum 6) (toInterpValue ())
+  | AccType_IFETCH -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_IFETCH") Interp_ast.Unknown) (Interp_ast.T_id "AccType") (Interp_ast.C_Enum 7) (toInterpValue ())
+  | AccType_PTW -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_PTW") Interp_ast.Unknown) (Interp_ast.T_id "AccType") (Interp_ast.C_Enum 8) (toInterpValue ())
+  | AccType_DC -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_DC") Interp_ast.Unknown) (Interp_ast.T_id "AccType") (Interp_ast.C_Enum 9) (toInterpValue ())
+  | AccType_IC -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_IC") Interp_ast.Unknown) (Interp_ast.T_id "AccType") (Interp_ast.C_Enum 10) (toInterpValue ())
+  | AccType_AT -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_AT") Interp_ast.Unknown) (Interp_ast.T_id "AccType") (Interp_ast.C_Enum 11) (toInterpValue ())
+  end
+
+let rec AccTypeFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_NORMAL") _) _ _ v -> AccType_NORMAL
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_VEC") _) _ _ v -> AccType_VEC
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_STREAM") _) _ _ v -> AccType_STREAM
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_VECSTREAM") _) _ _ v -> AccType_VECSTREAM
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_ATOMIC") _) _ _ v -> AccType_ATOMIC
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_ORDERED") _) _ _ v -> AccType_ORDERED
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_UNPRIV") _) _ _ v -> AccType_UNPRIV
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_IFETCH") _) _ _ v -> AccType_IFETCH
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_PTW") _) _ _ v -> AccType_PTW
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_DC") _) _ _ v -> AccType_DC
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_IC") _) _ _ v -> AccType_IC
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AccType_AT") _) _ _ v -> AccType_AT
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> AccType_NORMAL
+     | 1 -> AccType_VEC
+     | 2 -> AccType_STREAM
+     | 3 -> AccType_VECSTREAM
+     | 4 -> AccType_ATOMIC
+     | 5 -> AccType_ORDERED
+     | 6 -> AccType_UNPRIV
+     | 7 -> AccType_IFETCH
+     | 8 -> AccType_PTW
+     | 9 -> AccType_DC
+     | 10 -> AccType_IC
+     | 11 -> AccType_AT
+     end
+  | Interp_ast.V_tuple [v] -> AccTypeFromInterpValue v
+  | v -> failwith ("fromInterpValue AccType: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue AccType)
+  let toInterpValue = AccTypeToInterpValue
+  let fromInterpValue = AccTypeFromInterpValue
+end
+let MBReqDomainToInterpValue = function
+  | MBReqDomain_Nonshareable -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqDomain_Nonshareable") Interp_ast.Unknown) (Interp_ast.T_id "MBReqDomain") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | MBReqDomain_InnerShareable -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqDomain_InnerShareable") Interp_ast.Unknown) (Interp_ast.T_id "MBReqDomain") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | MBReqDomain_OuterShareable -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqDomain_OuterShareable") Interp_ast.Unknown) (Interp_ast.T_id "MBReqDomain") (Interp_ast.C_Enum 2) (toInterpValue ())
+  | MBReqDomain_FullSystem -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqDomain_FullSystem") Interp_ast.Unknown) (Interp_ast.T_id "MBReqDomain") (Interp_ast.C_Enum 3) (toInterpValue ())
+  end
+
+let rec MBReqDomainFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqDomain_Nonshareable") _) _ _ v -> MBReqDomain_Nonshareable
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqDomain_InnerShareable") _) _ _ v -> MBReqDomain_InnerShareable
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqDomain_OuterShareable") _) _ _ v -> MBReqDomain_OuterShareable
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqDomain_FullSystem") _) _ _ v -> MBReqDomain_FullSystem
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> MBReqDomain_Nonshareable
+     | 1 -> MBReqDomain_InnerShareable
+     | 2 -> MBReqDomain_OuterShareable
+     | 3 -> MBReqDomain_FullSystem
+     end
+  | Interp_ast.V_tuple [v] -> MBReqDomainFromInterpValue v
+  | v -> failwith ("fromInterpValue MBReqDomain: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue MBReqDomain)
+  let toInterpValue = MBReqDomainToInterpValue
+  let fromInterpValue = MBReqDomainFromInterpValue
+end
+let MBReqTypesToInterpValue = function
+  | MBReqTypes_Reads -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqTypes_Reads") Interp_ast.Unknown) (Interp_ast.T_id "MBReqTypes") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | MBReqTypes_Writes -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqTypes_Writes") Interp_ast.Unknown) (Interp_ast.T_id "MBReqTypes") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | MBReqTypes_All -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqTypes_All") Interp_ast.Unknown) (Interp_ast.T_id "MBReqTypes") (Interp_ast.C_Enum 2) (toInterpValue ())
+  end
+
+let rec MBReqTypesFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqTypes_Reads") _) _ _ v -> MBReqTypes_Reads
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqTypes_Writes") _) _ _ v -> MBReqTypes_Writes
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MBReqTypes_All") _) _ _ v -> MBReqTypes_All
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> MBReqTypes_Reads
+     | 1 -> MBReqTypes_Writes
+     | 2 -> MBReqTypes_All
+     end
+  | Interp_ast.V_tuple [v] -> MBReqTypesFromInterpValue v
+  | v -> failwith ("fromInterpValue MBReqTypes: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue MBReqTypes)
+  let toInterpValue = MBReqTypesToInterpValue
+  let fromInterpValue = MBReqTypesFromInterpValue
+end
+let BranchTypeToInterpValue = function
+  | BranchType_CALL -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_CALL") Interp_ast.Unknown) (Interp_ast.T_id "BranchType") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | BranchType_ERET -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_ERET") Interp_ast.Unknown) (Interp_ast.T_id "BranchType") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | BranchType_DBGEXIT -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_DBGEXIT") Interp_ast.Unknown) (Interp_ast.T_id "BranchType") (Interp_ast.C_Enum 2) (toInterpValue ())
+  | BranchType_RET -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_RET") Interp_ast.Unknown) (Interp_ast.T_id "BranchType") (Interp_ast.C_Enum 3) (toInterpValue ())
+  | BranchType_JMP -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_JMP") Interp_ast.Unknown) (Interp_ast.T_id "BranchType") (Interp_ast.C_Enum 4) (toInterpValue ())
+  | BranchType_EXCEPTION -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_EXCEPTION") Interp_ast.Unknown) (Interp_ast.T_id "BranchType") (Interp_ast.C_Enum 5) (toInterpValue ())
+  | BranchType_UNKNOWN -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_UNKNOWN") Interp_ast.Unknown) (Interp_ast.T_id "BranchType") (Interp_ast.C_Enum 6) (toInterpValue ())
+  end
+
+let rec BranchTypeFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_CALL") _) _ _ v -> BranchType_CALL
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_ERET") _) _ _ v -> BranchType_ERET
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_DBGEXIT") _) _ _ v -> BranchType_DBGEXIT
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_RET") _) _ _ v -> BranchType_RET
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_JMP") _) _ _ v -> BranchType_JMP
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_EXCEPTION") _) _ _ v -> BranchType_EXCEPTION
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchType_UNKNOWN") _) _ _ v -> BranchType_UNKNOWN
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> BranchType_CALL
+     | 1 -> BranchType_ERET
+     | 2 -> BranchType_DBGEXIT
+     | 3 -> BranchType_RET
+     | 4 -> BranchType_JMP
+     | 5 -> BranchType_EXCEPTION
+     | 6 -> BranchType_UNKNOWN
+     end
+  | Interp_ast.V_tuple [v] -> BranchTypeFromInterpValue v
+  | v -> failwith ("fromInterpValue BranchType: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue BranchType)
+  let toInterpValue = BranchTypeToInterpValue
+  let fromInterpValue = BranchTypeFromInterpValue
+end
+let MoveWideOpToInterpValue = function
+  | MoveWideOp_N -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MoveWideOp_N") Interp_ast.Unknown) (Interp_ast.T_id "MoveWideOp") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | MoveWideOp_Z -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MoveWideOp_Z") Interp_ast.Unknown) (Interp_ast.T_id "MoveWideOp") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | MoveWideOp_K -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MoveWideOp_K") Interp_ast.Unknown) (Interp_ast.T_id "MoveWideOp") (Interp_ast.C_Enum 2) (toInterpValue ())
+  end
+
+let rec MoveWideOpFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MoveWideOp_N") _) _ _ v -> MoveWideOp_N
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MoveWideOp_Z") _) _ _ v -> MoveWideOp_Z
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MoveWideOp_K") _) _ _ v -> MoveWideOp_K
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> MoveWideOp_N
+     | 1 -> MoveWideOp_Z
+     | 2 -> MoveWideOp_K
+     end
+  | Interp_ast.V_tuple [v] -> MoveWideOpFromInterpValue v
+  | v -> failwith ("fromInterpValue MoveWideOp: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue MoveWideOp)
+  let toInterpValue = MoveWideOpToInterpValue
+  let fromInterpValue = MoveWideOpFromInterpValue
+end
+let DeviceTypeToInterpValue = function
+  | DeviceType_GRE -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DeviceType_GRE") Interp_ast.Unknown) (Interp_ast.T_id "DeviceType") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | DeviceType_nGRE -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DeviceType_nGRE") Interp_ast.Unknown) (Interp_ast.T_id "DeviceType") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | DeviceType_nGnRE -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DeviceType_nGnRE") Interp_ast.Unknown) (Interp_ast.T_id "DeviceType") (Interp_ast.C_Enum 2) (toInterpValue ())
+  | DeviceType_nGnRnE -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DeviceType_nGnRnE") Interp_ast.Unknown) (Interp_ast.T_id "DeviceType") (Interp_ast.C_Enum 3) (toInterpValue ())
+  end
+
+let rec DeviceTypeFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DeviceType_GRE") _) _ _ v -> DeviceType_GRE
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DeviceType_nGRE") _) _ _ v -> DeviceType_nGRE
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DeviceType_nGnRE") _) _ _ v -> DeviceType_nGnRE
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DeviceType_nGnRnE") _) _ _ v -> DeviceType_nGnRnE
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> DeviceType_GRE
+     | 1 -> DeviceType_nGRE
+     | 2 -> DeviceType_nGnRE
+     | 3 -> DeviceType_nGnRnE
+     end
+  | Interp_ast.V_tuple [v] -> DeviceTypeFromInterpValue v
+  | v -> failwith ("fromInterpValue DeviceType: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue DeviceType)
+  let toInterpValue = DeviceTypeToInterpValue
+  let fromInterpValue = DeviceTypeFromInterpValue
+end
+let FaultToInterpValue = function
+  | Fault_None -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_None") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | Fault_AccessFlag -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_AccessFlag") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | Fault_Alignment -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Alignment") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 2) (toInterpValue ())
+  | Fault_Background -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Background") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 3) (toInterpValue ())
+  | Fault_Domain -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Domain") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 4) (toInterpValue ())
+  | Fault_Permission -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Permission") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 5) (toInterpValue ())
+  | Fault_Translation -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Translation") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 6) (toInterpValue ())
+  | Fault_AddressSize -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_AddressSize") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 7) (toInterpValue ())
+  | Fault_SyncExternal -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_SyncExternal") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 8) (toInterpValue ())
+  | Fault_SyncExternalOnWalk -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_SyncExternalOnWalk") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 9) (toInterpValue ())
+  | Fault_SyncParity -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_SyncParity") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 10) (toInterpValue ())
+  | Fault_SyncParityOnWalk -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_SyncParityOnWalk") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 11) (toInterpValue ())
+  | Fault_AsyncParity -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_AsyncParity") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 12) (toInterpValue ())
+  | Fault_AsyncExternal -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_AsyncExternal") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 13) (toInterpValue ())
+  | Fault_Debug -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Debug") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 14) (toInterpValue ())
+  | Fault_TLBConflict -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_TLBConflict") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 15) (toInterpValue ())
+  | Fault_Lockdown -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Lockdown") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 16) (toInterpValue ())
+  | Fault_Exclusive -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Exclusive") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 17) (toInterpValue ())
+  | Fault_ICacheMaint -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_ICacheMaint") Interp_ast.Unknown) (Interp_ast.T_id "Fault") (Interp_ast.C_Enum 18) (toInterpValue ())
+  end
+
+let rec FaultFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_None") _) _ _ v -> Fault_None
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_AccessFlag") _) _ _ v -> Fault_AccessFlag
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Alignment") _) _ _ v -> Fault_Alignment
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Background") _) _ _ v -> Fault_Background
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Domain") _) _ _ v -> Fault_Domain
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Permission") _) _ _ v -> Fault_Permission
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Translation") _) _ _ v -> Fault_Translation
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_AddressSize") _) _ _ v -> Fault_AddressSize
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_SyncExternal") _) _ _ v -> Fault_SyncExternal
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_SyncExternalOnWalk") _) _ _ v -> Fault_SyncExternalOnWalk
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_SyncParity") _) _ _ v -> Fault_SyncParity
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_SyncParityOnWalk") _) _ _ v -> Fault_SyncParityOnWalk
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_AsyncParity") _) _ _ v -> Fault_AsyncParity
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_AsyncExternal") _) _ _ v -> Fault_AsyncExternal
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Debug") _) _ _ v -> Fault_Debug
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_TLBConflict") _) _ _ v -> Fault_TLBConflict
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Lockdown") _) _ _ v -> Fault_Lockdown
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_Exclusive") _) _ _ v -> Fault_Exclusive
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Fault_ICacheMaint") _) _ _ v -> Fault_ICacheMaint
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> Fault_None
+     | 1 -> Fault_AccessFlag
+     | 2 -> Fault_Alignment
+     | 3 -> Fault_Background
+     | 4 -> Fault_Domain
+     | 5 -> Fault_Permission
+     | 6 -> Fault_Translation
+     | 7 -> Fault_AddressSize
+     | 8 -> Fault_SyncExternal
+     | 9 -> Fault_SyncExternalOnWalk
+     | 10 -> Fault_SyncParity
+     | 11 -> Fault_SyncParityOnWalk
+     | 12 -> Fault_AsyncParity
+     | 13 -> Fault_AsyncExternal
+     | 14 -> Fault_Debug
+     | 15 -> Fault_TLBConflict
+     | 16 -> Fault_Lockdown
+     | 17 -> Fault_Exclusive
+     | 18 -> Fault_ICacheMaint
+     end
+  | Interp_ast.V_tuple [v] -> FaultFromInterpValue v
+  | v -> failwith ("fromInterpValue Fault: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue Fault)
+  let toInterpValue = FaultToInterpValue
+  let fromInterpValue = FaultFromInterpValue
+end
+let MemTypeToInterpValue = function
+  | MemType_Normal -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemType_Normal") Interp_ast.Unknown) (Interp_ast.T_id "MemType") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | MemType_Device -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemType_Device") Interp_ast.Unknown) (Interp_ast.T_id "MemType") (Interp_ast.C_Enum 1) (toInterpValue ())
+  end
+
+let rec MemTypeFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemType_Normal") _) _ _ v -> MemType_Normal
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemType_Device") _) _ _ v -> MemType_Device
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> MemType_Normal
+     | 1 -> MemType_Device
+     end
+  | Interp_ast.V_tuple [v] -> MemTypeFromInterpValue v
+  | v -> failwith ("fromInterpValue MemType: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue MemType)
+  let toInterpValue = MemTypeToInterpValue
+  let fromInterpValue = MemTypeFromInterpValue
+end
+let PrefetchHintToInterpValue = function
+  | Prefetch_READ -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Prefetch_READ") Interp_ast.Unknown) (Interp_ast.T_id "PrefetchHint") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | Prefetch_WRITE -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Prefetch_WRITE") Interp_ast.Unknown) (Interp_ast.T_id "PrefetchHint") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | Prefetch_EXEC -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Prefetch_EXEC") Interp_ast.Unknown) (Interp_ast.T_id "PrefetchHint") (Interp_ast.C_Enum 2) (toInterpValue ())
+  end
+
+let rec PrefetchHintFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Prefetch_READ") _) _ _ v -> Prefetch_READ
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Prefetch_WRITE") _) _ _ v -> Prefetch_WRITE
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Prefetch_EXEC") _) _ _ v -> Prefetch_EXEC
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> Prefetch_READ
+     | 1 -> Prefetch_WRITE
+     | 2 -> Prefetch_EXEC
+     end
+  | Interp_ast.V_tuple [v] -> PrefetchHintFromInterpValue v
+  | v -> failwith ("fromInterpValue PrefetchHint: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue PrefetchHint)
+  let toInterpValue = PrefetchHintToInterpValue
+  let fromInterpValue = PrefetchHintFromInterpValue
+end
+let CountOpToInterpValue = function
+  | CountOp_CLZ -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "CountOp_CLZ") Interp_ast.Unknown) (Interp_ast.T_id "CountOp") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | CountOp_CLS -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "CountOp_CLS") Interp_ast.Unknown) (Interp_ast.T_id "CountOp") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | CountOp_CNT -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "CountOp_CNT") Interp_ast.Unknown) (Interp_ast.T_id "CountOp") (Interp_ast.C_Enum 2) (toInterpValue ())
+  end
+
+let rec CountOpFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "CountOp_CLZ") _) _ _ v -> CountOp_CLZ
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "CountOp_CLS") _) _ _ v -> CountOp_CLS
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "CountOp_CNT") _) _ _ v -> CountOp_CNT
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> CountOp_CLZ
+     | 1 -> CountOp_CLS
+     | 2 -> CountOp_CNT
+     end
+  | Interp_ast.V_tuple [v] -> CountOpFromInterpValue v
+  | v -> failwith ("fromInterpValue CountOp: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue CountOp)
+  let toInterpValue = CountOpToInterpValue
+  let fromInterpValue = CountOpFromInterpValue
+end
+let ExtendTypeToInterpValue = function
+  | ExtendType_SXTB -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_SXTB") Interp_ast.Unknown) (Interp_ast.T_id "ExtendType") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | ExtendType_SXTH -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_SXTH") Interp_ast.Unknown) (Interp_ast.T_id "ExtendType") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | ExtendType_SXTW -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_SXTW") Interp_ast.Unknown) (Interp_ast.T_id "ExtendType") (Interp_ast.C_Enum 2) (toInterpValue ())
+  | ExtendType_SXTX -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_SXTX") Interp_ast.Unknown) (Interp_ast.T_id "ExtendType") (Interp_ast.C_Enum 3) (toInterpValue ())
+  | ExtendType_UXTB -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_UXTB") Interp_ast.Unknown) (Interp_ast.T_id "ExtendType") (Interp_ast.C_Enum 4) (toInterpValue ())
+  | ExtendType_UXTH -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_UXTH") Interp_ast.Unknown) (Interp_ast.T_id "ExtendType") (Interp_ast.C_Enum 5) (toInterpValue ())
+  | ExtendType_UXTW -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_UXTW") Interp_ast.Unknown) (Interp_ast.T_id "ExtendType") (Interp_ast.C_Enum 6) (toInterpValue ())
+  | ExtendType_UXTX -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_UXTX") Interp_ast.Unknown) (Interp_ast.T_id "ExtendType") (Interp_ast.C_Enum 7) (toInterpValue ())
+  end
+
+let rec ExtendTypeFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_SXTB") _) _ _ v -> ExtendType_SXTB
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_SXTH") _) _ _ v -> ExtendType_SXTH
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_SXTW") _) _ _ v -> ExtendType_SXTW
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_SXTX") _) _ _ v -> ExtendType_SXTX
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_UXTB") _) _ _ v -> ExtendType_UXTB
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_UXTH") _) _ _ v -> ExtendType_UXTH
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_UXTW") _) _ _ v -> ExtendType_UXTW
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtendType_UXTX") _) _ _ v -> ExtendType_UXTX
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> ExtendType_SXTB
+     | 1 -> ExtendType_SXTH
+     | 2 -> ExtendType_SXTW
+     | 3 -> ExtendType_SXTX
+     | 4 -> ExtendType_UXTB
+     | 5 -> ExtendType_UXTH
+     | 6 -> ExtendType_UXTW
+     | 7 -> ExtendType_UXTX
+     end
+  | Interp_ast.V_tuple [v] -> ExtendTypeFromInterpValue v
+  | v -> failwith ("fromInterpValue ExtendType: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue ExtendType)
+  let toInterpValue = ExtendTypeToInterpValue
+  let fromInterpValue = ExtendTypeFromInterpValue
+end
+let RevOpToInterpValue = function
+  | RevOp_RBIT -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RevOp_RBIT") Interp_ast.Unknown) (Interp_ast.T_id "RevOp") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | RevOp_REV16 -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RevOp_REV16") Interp_ast.Unknown) (Interp_ast.T_id "RevOp") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | RevOp_REV32 -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RevOp_REV32") Interp_ast.Unknown) (Interp_ast.T_id "RevOp") (Interp_ast.C_Enum 2) (toInterpValue ())
+  | RevOp_REV64 -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RevOp_REV64") Interp_ast.Unknown) (Interp_ast.T_id "RevOp") (Interp_ast.C_Enum 3) (toInterpValue ())
+  end
+
+let rec RevOpFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RevOp_RBIT") _) _ _ v -> RevOp_RBIT
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RevOp_REV16") _) _ _ v -> RevOp_REV16
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RevOp_REV32") _) _ _ v -> RevOp_REV32
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RevOp_REV64") _) _ _ v -> RevOp_REV64
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> RevOp_RBIT
+     | 1 -> RevOp_REV16
+     | 2 -> RevOp_REV32
+     | 3 -> RevOp_REV64
+     end
+  | Interp_ast.V_tuple [v] -> RevOpFromInterpValue v
+  | v -> failwith ("fromInterpValue RevOp: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue RevOp)
+  let toInterpValue = RevOpToInterpValue
+  let fromInterpValue = RevOpFromInterpValue
+end
+let ShiftTypeToInterpValue = function
+  | ShiftType_LSL -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ShiftType_LSL") Interp_ast.Unknown) (Interp_ast.T_id "ShiftType") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | ShiftType_LSR -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ShiftType_LSR") Interp_ast.Unknown) (Interp_ast.T_id "ShiftType") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | ShiftType_ASR -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ShiftType_ASR") Interp_ast.Unknown) (Interp_ast.T_id "ShiftType") (Interp_ast.C_Enum 2) (toInterpValue ())
+  | ShiftType_ROR -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ShiftType_ROR") Interp_ast.Unknown) (Interp_ast.T_id "ShiftType") (Interp_ast.C_Enum 3) (toInterpValue ())
+  end
+
+let rec ShiftTypeFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ShiftType_LSL") _) _ _ v -> ShiftType_LSL
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ShiftType_LSR") _) _ _ v -> ShiftType_LSR
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ShiftType_ASR") _) _ _ v -> ShiftType_ASR
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ShiftType_ROR") _) _ _ v -> ShiftType_ROR
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> ShiftType_LSL
+     | 1 -> ShiftType_LSR
+     | 2 -> ShiftType_ASR
+     | 3 -> ShiftType_ROR
+     end
+  | Interp_ast.V_tuple [v] -> ShiftTypeFromInterpValue v
+  | v -> failwith ("fromInterpValue ShiftType: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue ShiftType)
+  let toInterpValue = ShiftTypeToInterpValue
+  let fromInterpValue = ShiftTypeFromInterpValue
+end
+let LogicalOpToInterpValue = function
+  | LogicalOp_AND -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LogicalOp_AND") Interp_ast.Unknown) (Interp_ast.T_id "LogicalOp") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | LogicalOp_EOR -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LogicalOp_EOR") Interp_ast.Unknown) (Interp_ast.T_id "LogicalOp") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | LogicalOp_ORR -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LogicalOp_ORR") Interp_ast.Unknown) (Interp_ast.T_id "LogicalOp") (Interp_ast.C_Enum 2) (toInterpValue ())
+  end
+
+let rec LogicalOpFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LogicalOp_AND") _) _ _ v -> LogicalOp_AND
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LogicalOp_EOR") _) _ _ v -> LogicalOp_EOR
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LogicalOp_ORR") _) _ _ v -> LogicalOp_ORR
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> LogicalOp_AND
+     | 1 -> LogicalOp_EOR
+     | 2 -> LogicalOp_ORR
+     end
+  | Interp_ast.V_tuple [v] -> LogicalOpFromInterpValue v
+  | v -> failwith ("fromInterpValue LogicalOp: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue LogicalOp)
+  let toInterpValue = LogicalOpToInterpValue
+  let fromInterpValue = LogicalOpFromInterpValue
+end
+let MemOpToInterpValue = function
+  | MemOp_LOAD -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemOp_LOAD") Interp_ast.Unknown) (Interp_ast.T_id "MemOp") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | MemOp_STORE -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemOp_STORE") Interp_ast.Unknown) (Interp_ast.T_id "MemOp") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | MemOp_PREFETCH -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemOp_PREFETCH") Interp_ast.Unknown) (Interp_ast.T_id "MemOp") (Interp_ast.C_Enum 2) (toInterpValue ())
+  end
+
+let rec MemOpFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemOp_LOAD") _) _ _ v -> MemOp_LOAD
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemOp_STORE") _) _ _ v -> MemOp_STORE
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemOp_PREFETCH") _) _ _ v -> MemOp_PREFETCH
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> MemOp_LOAD
+     | 1 -> MemOp_STORE
+     | 2 -> MemOp_PREFETCH
+     end
+  | Interp_ast.V_tuple [v] -> MemOpFromInterpValue v
+  | v -> failwith ("fromInterpValue MemOp: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue MemOp)
+  let toInterpValue = MemOpToInterpValue
+  let fromInterpValue = MemOpFromInterpValue
+end
+let MemBarrierOpToInterpValue = function
+  | MemBarrierOp_DSB -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemBarrierOp_DSB") Interp_ast.Unknown) (Interp_ast.T_id "MemBarrierOp") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | MemBarrierOp_DMB -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemBarrierOp_DMB") Interp_ast.Unknown) (Interp_ast.T_id "MemBarrierOp") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | MemBarrierOp_ISB -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemBarrierOp_ISB") Interp_ast.Unknown) (Interp_ast.T_id "MemBarrierOp") (Interp_ast.C_Enum 2) (toInterpValue ())
+  end
+
+let rec MemBarrierOpFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemBarrierOp_DSB") _) _ _ v -> MemBarrierOp_DSB
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemBarrierOp_DMB") _) _ _ v -> MemBarrierOp_DMB
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MemBarrierOp_ISB") _) _ _ v -> MemBarrierOp_ISB
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> MemBarrierOp_DSB
+     | 1 -> MemBarrierOp_DMB
+     | 2 -> MemBarrierOp_ISB
+     end
+  | Interp_ast.V_tuple [v] -> MemBarrierOpFromInterpValue v
+  | v -> failwith ("fromInterpValue MemBarrierOp: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue MemBarrierOp)
+  let toInterpValue = MemBarrierOpToInterpValue
+  let fromInterpValue = MemBarrierOpFromInterpValue
+end
+let SystemHintOpToInterpValue = function
+  | SystemHintOp_NOP -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "SystemHintOp_NOP") Interp_ast.Unknown) (Interp_ast.T_id "SystemHintOp") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | SystemHintOp_YIELD -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "SystemHintOp_YIELD") Interp_ast.Unknown) (Interp_ast.T_id "SystemHintOp") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | SystemHintOp_WFE -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "SystemHintOp_WFE") Interp_ast.Unknown) (Interp_ast.T_id "SystemHintOp") (Interp_ast.C_Enum 2) (toInterpValue ())
+  | SystemHintOp_WFI -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "SystemHintOp_WFI") Interp_ast.Unknown) (Interp_ast.T_id "SystemHintOp") (Interp_ast.C_Enum 3) (toInterpValue ())
+  | SystemHintOp_SEV -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "SystemHintOp_SEV") Interp_ast.Unknown) (Interp_ast.T_id "SystemHintOp") (Interp_ast.C_Enum 4) (toInterpValue ())
+  | SystemHintOp_SEVL -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "SystemHintOp_SEVL") Interp_ast.Unknown) (Interp_ast.T_id "SystemHintOp") (Interp_ast.C_Enum 5) (toInterpValue ())
+  end
+
+let rec SystemHintOpFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "SystemHintOp_NOP") _) _ _ v -> SystemHintOp_NOP
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "SystemHintOp_YIELD") _) _ _ v -> SystemHintOp_YIELD
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "SystemHintOp_WFE") _) _ _ v -> SystemHintOp_WFE
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "SystemHintOp_WFI") _) _ _ v -> SystemHintOp_WFI
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "SystemHintOp_SEV") _) _ _ v -> SystemHintOp_SEV
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "SystemHintOp_SEVL") _) _ _ v -> SystemHintOp_SEVL
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> SystemHintOp_NOP
+     | 1 -> SystemHintOp_YIELD
+     | 2 -> SystemHintOp_WFE
+     | 3 -> SystemHintOp_WFI
+     | 4 -> SystemHintOp_SEV
+     | 5 -> SystemHintOp_SEVL
+     end
+  | Interp_ast.V_tuple [v] -> SystemHintOpFromInterpValue v
+  | v -> failwith ("fromInterpValue SystemHintOp: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue SystemHintOp)
+  let toInterpValue = SystemHintOpToInterpValue
+  let fromInterpValue = SystemHintOpFromInterpValue
+end
+let PSTATEFieldToInterpValue = function
+  | PSTATEField_DAIFSet -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "PSTATEField_DAIFSet") Interp_ast.Unknown) (Interp_ast.T_id "PSTATEField") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | PSTATEField_DAIFClr -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "PSTATEField_DAIFClr") Interp_ast.Unknown) (Interp_ast.T_id "PSTATEField") (Interp_ast.C_Enum 1) (toInterpValue ())
+  | PSTATEField_SP -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "PSTATEField_SP") Interp_ast.Unknown) (Interp_ast.T_id "PSTATEField") (Interp_ast.C_Enum 2) (toInterpValue ())
+  end
+
+let rec PSTATEFieldFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "PSTATEField_DAIFSet") _) _ _ v -> PSTATEField_DAIFSet
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "PSTATEField_DAIFClr") _) _ _ v -> PSTATEField_DAIFClr
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "PSTATEField_SP") _) _ _ v -> PSTATEField_SP
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> PSTATEField_DAIFSet
+     | 1 -> PSTATEField_DAIFClr
+     | 2 -> PSTATEField_SP
+     end
+  | Interp_ast.V_tuple [v] -> PSTATEFieldFromInterpValue v
+  | v -> failwith ("fromInterpValue PSTATEField: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue PSTATEField)
+  let toInterpValue = PSTATEFieldToInterpValue
+  let fromInterpValue = PSTATEFieldFromInterpValue
+end
+let signalValueToInterpValue = function
+  | LOw -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LOw") Interp_ast.Unknown) (Interp_ast.T_id "signalValue") (Interp_ast.C_Enum 0) (toInterpValue ())
+  | HIGH -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "HIGH") Interp_ast.Unknown) (Interp_ast.T_id "signalValue") (Interp_ast.C_Enum 1) (toInterpValue ())
+  end
+
+let rec signalValueFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LOw") _) _ _ v -> LOw
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "HIGH") _) _ _ v -> HIGH
+  | Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _) ->
+     match (natFromInteger n) with
+     | 0 -> LOw
+     | 1 -> HIGH
+     end
+  | Interp_ast.V_tuple [v] -> signalValueFromInterpValue v
+  | v -> failwith ("fromInterpValue signalValue: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue signalValue)
+  let toInterpValue = signalValueToInterpValue
+  let fromInterpValue = signalValueFromInterpValue
+end
+let astToInterpValue = function
+  | Unallocated -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Unallocated") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue ())
+  | ImplementationDefinedTestBeginEnd v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ImplementationDefinedTestBeginEnd") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | ImplementationDefinedStopFetching -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ImplementationDefinedStopFetching") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue ())
+  | ImplementationDefinedThreadStart -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ImplementationDefinedThreadStart") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue ())
+  | TMStart v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "TMStart") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | TMCommit -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "TMCommit") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue ())
+  | TMAbort v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "TMAbort") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | TMTest -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "TMTest") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue ())
+  | CompareAndBranch v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "CompareAndBranch") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | BranchConditional v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchConditional") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | GenerateExceptionEL1 v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "GenerateExceptionEL1") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | GenerateExceptionEL2 v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "GenerateExceptionEL2") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | GenerateExceptionEL3 v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "GenerateExceptionEL3") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | DebugBreakpoint v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DebugBreakpoint") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | ExternalDebugBreakpoint -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExternalDebugBreakpoint") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue ())
+  | DebugSwitchToExceptionLevel v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DebugSwitchToExceptionLevel") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | MoveSystemImmediate v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MoveSystemImmediate") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | Hint v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Hint") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | ClearExclusiveMonitor v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ClearExclusiveMonitor") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | Barrier v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Barrier") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | System v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "System") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | MoveSystemRegister v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MoveSystemRegister") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | TestBitAndBranch v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "TestBitAndBranch") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | BranchImmediate v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchImmediate") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | BranchRegister v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchRegister") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | ExceptionReturn -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExceptionReturn") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue ())
+  | DebugRestorePState -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DebugRestorePState") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue ())
+  | LoadLiteral v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LoadLiteral") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | LoadStoreAcqExc v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LoadStoreAcqExc") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | LoadStorePairNonTemp v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LoadStorePairNonTemp") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | LoadImmediate v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LoadImmediate") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | LoadRegister v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LoadRegister") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | LoadStorePair v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LoadStorePair") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | AddSubImmediate v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AddSubImmediate") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | BitfieldMove v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BitfieldMove") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | ExtractRegister v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtractRegister") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | LogicalImmediate v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LogicalImmediate") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | MoveWide v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MoveWide") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | Address v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Address") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | AddSubExtendRegister v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AddSubExtendRegister") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | AddSubShiftedRegister v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AddSubShiftedRegister") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | AddSubCarry v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AddSubCarry") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | ConditionalCompareImmediate v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ConditionalCompareImmediate") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | ConditionalCompareRegister v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ConditionalCompareRegister") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | ConditionalSelect v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ConditionalSelect") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | Reverse v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Reverse") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | CountLeading v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "CountLeading") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | Division v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Division") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | Shift v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Shift") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | CRC v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "CRC") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | MultiplyAddSub v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MultiplyAddSub") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | MultiplyAddSubLong v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MultiplyAddSubLong") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | MultiplyHigh v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MultiplyHigh") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  | LogicalShiftedRegister v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LogicalShiftedRegister") Interp_ast.Unknown) (Interp_ast.T_id "ast") Interp_ast.C_Union (toInterpValue v)
+  end
+
+let rec astFromInterpValue v = match v with
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Unallocated") _) _ _ v -> Unallocated
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ImplementationDefinedTestBeginEnd") _) _ _ v -> ImplementationDefinedTestBeginEnd (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ImplementationDefinedStopFetching") _) _ _ v -> ImplementationDefinedStopFetching
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ImplementationDefinedThreadStart") _) _ _ v -> ImplementationDefinedThreadStart
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "TMStart") _) _ _ v -> TMStart (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "TMCommit") _) _ _ v -> TMCommit
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "TMAbort") _) _ _ v -> TMAbort (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "TMTest") _) _ _ v -> TMTest
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "CompareAndBranch") _) _ _ v -> CompareAndBranch (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchConditional") _) _ _ v -> BranchConditional (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "GenerateExceptionEL1") _) _ _ v -> GenerateExceptionEL1 (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "GenerateExceptionEL2") _) _ _ v -> GenerateExceptionEL2 (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "GenerateExceptionEL3") _) _ _ v -> GenerateExceptionEL3 (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DebugBreakpoint") _) _ _ v -> DebugBreakpoint (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExternalDebugBreakpoint") _) _ _ v -> ExternalDebugBreakpoint
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DebugSwitchToExceptionLevel") _) _ _ v -> DebugSwitchToExceptionLevel (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MoveSystemImmediate") _) _ _ v -> MoveSystemImmediate (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Hint") _) _ _ v -> Hint (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ClearExclusiveMonitor") _) _ _ v -> ClearExclusiveMonitor (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Barrier") _) _ _ v -> Barrier (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "System") _) _ _ v -> System (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MoveSystemRegister") _) _ _ v -> MoveSystemRegister (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "TestBitAndBranch") _) _ _ v -> TestBitAndBranch (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchImmediate") _) _ _ v -> BranchImmediate (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BranchRegister") _) _ _ v -> BranchRegister (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExceptionReturn") _) _ _ v -> ExceptionReturn
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "DebugRestorePState") _) _ _ v -> DebugRestorePState
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LoadLiteral") _) _ _ v -> LoadLiteral (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LoadStoreAcqExc") _) _ _ v -> LoadStoreAcqExc (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LoadStorePairNonTemp") _) _ _ v -> LoadStorePairNonTemp (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LoadImmediate") _) _ _ v -> LoadImmediate (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LoadRegister") _) _ _ v -> LoadRegister (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LoadStorePair") _) _ _ v -> LoadStorePair (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AddSubImmediate") _) _ _ v -> AddSubImmediate (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "BitfieldMove") _) _ _ v -> BitfieldMove (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ExtractRegister") _) _ _ v -> ExtractRegister (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LogicalImmediate") _) _ _ v -> LogicalImmediate (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MoveWide") _) _ _ v -> MoveWide (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Address") _) _ _ v -> Address (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AddSubExtendRegister") _) _ _ v -> AddSubExtendRegister (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AddSubShiftedRegister") _) _ _ v -> AddSubShiftedRegister (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "AddSubCarry") _) _ _ v -> AddSubCarry (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ConditionalCompareImmediate") _) _ _ v -> ConditionalCompareImmediate (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ConditionalCompareRegister") _) _ _ v -> ConditionalCompareRegister (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "ConditionalSelect") _) _ _ v -> ConditionalSelect (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Reverse") _) _ _ v -> Reverse (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "CountLeading") _) _ _ v -> CountLeading (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Division") _) _ _ v -> Division (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "Shift") _) _ _ v -> Shift (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "CRC") _) _ _ v -> CRC (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MultiplyAddSub") _) _ _ v -> MultiplyAddSub (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MultiplyAddSubLong") _) _ _ v -> MultiplyAddSubLong (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "MultiplyHigh") _) _ _ v -> MultiplyHigh (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "LogicalShiftedRegister") _) _ _ v -> LogicalShiftedRegister (fromInterpValue v)
+  | Interp_ast.V_tuple [v] -> astFromInterpValue v
+  | v -> failwith ("fromInterpValue ast: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue ast)
+  let toInterpValue = astToInterpValue
+  let fromInterpValue = astFromInterpValue
+end