Module Jasmin.Arm_expand_imm

type __ = Obj.t
type expand_immediate_kind =
  1. | EI_none
  2. | EI_byte
  3. | EI_pattern
  4. | EI_shift
val is_ei_pattern : BinNums.coq_Z -> bool
val is_ei_shift : BinNums.coq_Z -> bool
type wencoding =
  1. | WE_allowed of bool
  2. | W12_encoding
  3. | W16_encoding
type is_wencoding =
  1. | Coq_is_WE_allowed of bool * Param1.Coq_exports.is_bool
  2. | Coq_is_W12_encoding
  3. | Coq_is_W16_encoding
val wencoding_tag : wencoding -> BinNums.positive
val is_wencoding_inhab : wencoding -> is_wencoding
type box_wencoding_W12_encoding =
  1. | Box_wencoding_W12_encoding
type wencoding_fields_t = __
val wencoding_fields : wencoding -> wencoding_fields_t
val wencoding_eqb_fields : (wencoding -> wencoding -> bool) -> BinNums.positive -> wencoding_fields_t -> wencoding_fields_t -> bool
val wencoding_eqb : wencoding -> wencoding -> bool
type expected_wencoding = {
  1. on_shift : wencoding;
  2. on_none : wencoding;
}
type is_expected_wencoding =
  1. | Coq_is_Build_expected_wencoding of wencoding * is_wencoding * wencoding * is_wencoding
val expected_wencoding_tag : expected_wencoding -> BinNums.positive
val is_expected_wencoding_inhab : expected_wencoding -> is_expected_wencoding
type box_expected_wencoding_Build_expected_wencoding = {
  1. coq_Box_expected_wencoding_Build_expected_wencoding_0 : wencoding;
  2. coq_Box_expected_wencoding_Build_expected_wencoding_1 : wencoding;
}
type expected_wencoding_fields_t = box_expected_wencoding_Build_expected_wencoding
val expected_wencoding_fields : expected_wencoding -> expected_wencoding_fields_t
val expected_wencoding_eqb : expected_wencoding -> expected_wencoding -> bool
val is_w12_encoding : BinNums.coq_Z -> bool
val is_w16_encoding : BinNums.coq_Z -> bool
val check_wencoding : wencoding -> BinNums.coq_Z -> bool
val check_ei_kind : expected_wencoding -> Wsize.wsize -> Ssralg.GRing.ComRing.sort -> bool
val string_of_ew : wencoding -> string