Module Jasmin.Arm_decl

type __ = Obj.t
val arm_reg_size : Wsize.wsize
val arm_xreg_size : Wsize.wsize
type register =
  1. | R00
  2. | R01
  3. | R02
  4. | R03
  5. | R04
  6. | R05
  7. | R06
  8. | R07
  9. | R08
  10. | R09
  11. | R10
  12. | R11
  13. | R12
  14. | LR
  15. | SP
val register_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
val register_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
type is_register =
  1. | Coq_is_R00
  2. | Coq_is_R01
  3. | Coq_is_R02
  4. | Coq_is_R03
  5. | Coq_is_R04
  6. | Coq_is_R05
  7. | Coq_is_R06
  8. | Coq_is_R07
  9. | Coq_is_R08
  10. | Coq_is_R09
  11. | Coq_is_R10
  12. | Coq_is_R11
  13. | Coq_is_R12
  14. | Coq_is_LR
  15. | Coq_is_SP
val is_register_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> is_register -> 'a1
val is_register_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> is_register -> 'a1
val register_tag : register -> BinNums.positive
val is_register_inhab : register -> is_register
val is_register_functor : register -> is_register -> is_register
type box_register_R00 =
  1. | Box_register_R00
type register_fields_t = __
val register_fields : register -> register_fields_t
val register_construct : BinNums.positive -> register_fields_t -> register option
val register_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> is_register -> 'a1
val register_eqb_fields : (register -> register -> bool) -> BinNums.positive -> register_fields_t -> register_fields_t -> bool
val register_eqb : register -> register -> bool
val register_eqb_OK : register -> register -> Bool.reflect
val register_eqb_OK_sumbool : register -> register -> bool
val eqTC_register : register Utils0.eqTypeC
val arm_register_eqType : Eqtype.Equality.coq_type
val registers : register list
val finTC_register : register Utils0.finTypeC
val register_finType : Fintype.Finite.coq_type
val register_to_string : register -> string
type rflag =
  1. | NF
  2. | ZF
  3. | CF
  4. | VF
val rflag_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> 'a1
val rflag_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> 'a1
type is_rflag =
  1. | Coq_is_NF
  2. | Coq_is_ZF
  3. | Coq_is_CF
  4. | Coq_is_VF
val is_rflag_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> is_rflag -> 'a1
val is_rflag_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> is_rflag -> 'a1
val rflag_tag : rflag -> BinNums.positive
val is_rflag_inhab : rflag -> is_rflag
val is_rflag_functor : rflag -> is_rflag -> is_rflag
type box_rflag_NF =
  1. | Box_rflag_NF
type rflag_fields_t = __
val rflag_fields : rflag -> rflag_fields_t
val rflag_construct : BinNums.positive -> rflag_fields_t -> rflag option
val rflag_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> is_rflag -> 'a1
val rflag_eqb_fields : (rflag -> rflag -> bool) -> BinNums.positive -> rflag_fields_t -> rflag_fields_t -> bool
val rflag_eqb : rflag -> rflag -> bool
val rflag_eqb_OK : rflag -> rflag -> Bool.reflect
val rflag_eqb_OK_sumbool : rflag -> rflag -> bool
val eqTC_rflag : rflag Utils0.eqTypeC
val rflag_eqType : Eqtype.Equality.coq_type
val rflags : rflag list
val finTC_rflag : rflag Utils0.finTypeC
val rflag_finType : Fintype.Finite.coq_type
val flag_to_string : rflag -> string
type condt =
  1. | EQ_ct
  2. | NE_ct
  3. | CS_ct
  4. | CC_ct
  5. | MI_ct
  6. | PL_ct
  7. | VS_ct
  8. | VC_ct
  9. | HI_ct
  10. | LS_ct
  11. | GE_ct
  12. | LT_ct
  13. | GT_ct
  14. | LE_ct
val condt_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> 'a1
val condt_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> 'a1
type is_condt =
  1. | Coq_is_EQ_ct
  2. | Coq_is_NE_ct
  3. | Coq_is_CS_ct
  4. | Coq_is_CC_ct
  5. | Coq_is_MI_ct
  6. | Coq_is_PL_ct
  7. | Coq_is_VS_ct
  8. | Coq_is_VC_ct
  9. | Coq_is_HI_ct
  10. | Coq_is_LS_ct
  11. | Coq_is_GE_ct
  12. | Coq_is_LT_ct
  13. | Coq_is_GT_ct
  14. | Coq_is_LE_ct
val is_condt_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> is_condt -> 'a1
val is_condt_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> is_condt -> 'a1
val condt_tag : condt -> BinNums.positive
val is_condt_inhab : condt -> is_condt
val is_condt_functor : condt -> is_condt -> is_condt
type box_condt_EQ_ct =
  1. | Box_condt_EQ_ct
type condt_fields_t = __
val condt_fields : condt -> condt_fields_t
val condt_construct : BinNums.positive -> condt_fields_t -> condt option
val condt_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> is_condt -> 'a1
val condt_eqb_fields : (condt -> condt -> bool) -> BinNums.positive -> condt_fields_t -> condt_fields_t -> bool
val condt_eqb : condt -> condt -> bool
val condt_eqb_OK : condt -> condt -> Bool.reflect
val condt_eqb_OK_sumbool : condt -> condt -> bool
val eqTC_condt : condt Utils0.eqTypeC
val condt_eqType : Eqtype.Equality.coq_type
val condts : condt list
val finTC_condt : condt Utils0.finTypeC
val condt_finType : Fintype.Finite.coq_type
val string_of_condt : condt -> string
val shift_kind_eqType : Eqtype.Equality.coq_type
val shift_kinds : Shift_kind.shift_kind list
val string_of_shift_kind : Shift_kind.shift_kind -> string
val check_shift_amount : Shift_kind.shift_kind -> BinNums.coq_Z -> bool
val shift_of_sop2 : Wsize.wsize -> Expr.sop2 -> Shift_kind.shift_kind option
val is_expandable : BinNums.coq_Z -> bool
val is_expandable_or_shift : BinNums.coq_Z -> bool