(*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