package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Jasmin.Operators

type __ = Obj.t
type cmp_kind =
  1. | Cmp_int
  2. | Cmp_w of Wsize.signedness * Wsize.wsize
val cmp_kind_tag : cmp_kind -> BinNums.positive
type box_cmp_kind_Cmp_int =
  1. | Box_cmp_kind_Cmp_int
type box_cmp_kind_Cmp_w = {
  1. coq_Box_cmp_kind_Cmp_w_0 : Wsize.signedness;
  2. coq_Box_cmp_kind_Cmp_w_1 : Wsize.wsize;
}
type cmp_kind_fields_t = __
val cmp_kind_fields : cmp_kind -> cmp_kind_fields_t
val cmp_kind_eqb_fields : (cmp_kind -> cmp_kind -> bool) -> BinNums.positive -> cmp_kind_fields_t -> cmp_kind_fields_t -> bool
val cmp_kind_eqb : cmp_kind -> cmp_kind -> bool
type op_kind =
  1. | Op_int
  2. | Op_w of Wsize.wsize
val op_kind_tag : op_kind -> BinNums.positive
type box_op_kind_Op_int =
  1. | Box_op_kind_Op_int
type op_kind_fields_t = __
val op_kind_fields : op_kind -> op_kind_fields_t
val op_kind_eqb_fields : (op_kind -> op_kind -> bool) -> BinNums.positive -> op_kind_fields_t -> op_kind_fields_t -> bool
val op_kind_eqb : op_kind -> op_kind -> bool
val op_kind_eqb_OK : op_kind -> op_kind -> Bool.reflect
type wiop1 =
  1. | WIwint_of_int of Wsize.wsize
  2. | WIint_of_wint of Wsize.wsize
  3. | WIword_of_wint of Wsize.wsize
  4. | WIwint_of_word of Wsize.wsize
  5. | WIwint_ext of Wsize.wsize * Wsize.wsize
  6. | WIneg of Wsize.wsize
val wiop1_tag : wiop1 -> BinNums.positive
type box_wiop1_WIwint_ext = {
  1. coq_Box_wiop1_WIwint_ext_0 : Wsize.wsize;
  2. coq_Box_wiop1_WIwint_ext_1 : Wsize.wsize;
}
type wiop1_fields_t = __
val wiop1_fields : wiop1 -> wiop1_fields_t
val wiop1_eqb_fields : (wiop1 -> wiop1 -> bool) -> BinNums.positive -> wiop1_fields_t -> wiop1_fields_t -> bool
val wiop1_eqb : wiop1 -> wiop1 -> bool
type sop1 =
  1. | Oword_of_int of Wsize.wsize
  2. | Oint_of_word of Wsize.signedness * Wsize.wsize
  3. | Osignext of Wsize.wsize * Wsize.wsize
  4. | Ozeroext of Wsize.wsize * Wsize.wsize
  5. | Onot
  6. | Olnot of Wsize.wsize
  7. | Oneg of op_kind
  8. | Owi1 of Wsize.signedness * wiop1
val sop1_tag : sop1 -> BinNums.positive
type box_sop1_Oint_of_word = {
  1. coq_Box_sop1_Oint_of_word_0 : Wsize.signedness;
  2. coq_Box_sop1_Oint_of_word_1 : Wsize.wsize;
}
type box_sop1_Osignext = {
  1. coq_Box_sop1_Osignext_0 : Wsize.wsize;
  2. coq_Box_sop1_Osignext_1 : Wsize.wsize;
}
type box_sop1_Onot =
  1. | Box_sop1_Onot
type box_sop1_Owi1 = {
  1. coq_Box_sop1_Owi1_0 : Wsize.signedness;
  2. coq_Box_sop1_Owi1_1 : wiop1;
}
type sop1_fields_t = __
val sop1_fields : sop1 -> sop1_fields_t
val sop1_eqb_fields : (sop1 -> sop1 -> bool) -> BinNums.positive -> sop1_fields_t -> sop1_fields_t -> bool
val sop1_eqb : sop1 -> sop1 -> bool
val sop1_eqb_OK : sop1 -> sop1 -> Bool.reflect
type wiop2 =
  1. | WIadd
  2. | WImul
  3. | WIsub
  4. | WIdiv
  5. | WImod
  6. | WIshl
  7. | WIshr
  8. | WIeq
  9. | WIneq
  10. | WIlt
  11. | WIle
  12. | WIgt
  13. | WIge
val wiop2_tag : wiop2 -> BinNums.positive
type box_wiop2_WIadd =
  1. | Box_wiop2_WIadd
type wiop2_fields_t = __
val wiop2_fields : wiop2 -> wiop2_fields_t
val wiop2_eqb_fields : (wiop2 -> wiop2 -> bool) -> BinNums.positive -> wiop2_fields_t -> wiop2_fields_t -> bool
val wiop2_eqb : wiop2 -> wiop2 -> bool
type sop2 =
  1. | Obeq
  2. | Oand
  3. | Oor
  4. | Oadd of op_kind
  5. | Omul of op_kind
  6. | Osub of op_kind
  7. | Odiv of Wsize.signedness * op_kind
  8. | Omod of Wsize.signedness * op_kind
  9. | Oland of Wsize.wsize
  10. | Olor of Wsize.wsize
  11. | Olxor of Wsize.wsize
  12. | Olsr of Wsize.wsize
  13. | Olsl of op_kind
  14. | Oasr of op_kind
  15. | Oror of Wsize.wsize
  16. | Orol of Wsize.wsize
  17. | Oeq of op_kind
  18. | Oneq of op_kind
  19. | Olt of cmp_kind
  20. | Ole of cmp_kind
  21. | Ogt of cmp_kind
  22. | Oge of cmp_kind
  23. | Ovadd of Wsize.velem * Wsize.wsize
  24. | Ovsub of Wsize.velem * Wsize.wsize
  25. | Ovmul of Wsize.velem * Wsize.wsize
  26. | Ovlsr of Wsize.velem * Wsize.wsize
  27. | Ovlsl of Wsize.velem * Wsize.wsize
  28. | Ovasr of Wsize.velem * Wsize.wsize
  29. | Owi2 of Wsize.signedness * Wsize.wsize * wiop2
val sop2_tag : sop2 -> BinNums.positive
type box_sop2_Obeq =
  1. | Box_sop2_Obeq
type box_sop2_Odiv = {
  1. coq_Box_sop2_Odiv_0 : Wsize.signedness;
  2. coq_Box_sop2_Odiv_1 : op_kind;
}
type box_sop2_Ovadd = {
  1. coq_Box_sop2_Ovadd_0 : Wsize.velem;
  2. coq_Box_sop2_Ovadd_1 : Wsize.wsize;
}
type box_sop2_Owi2 = {
  1. coq_Box_sop2_Owi2_0 : Wsize.signedness;
  2. coq_Box_sop2_Owi2_1 : Wsize.wsize;
  3. coq_Box_sop2_Owi2_2 : wiop2;
}
type sop2_fields_t = __
val sop2_fields : sop2 -> sop2_fields_t
val sop2_eqb_fields : (sop2 -> sop2 -> bool) -> BinNums.positive -> sop2_fields_t -> sop2_fields_t -> bool
val sop2_eqb : sop2 -> sop2 -> bool
val sop2_eqb_OK : sop2 -> sop2 -> Bool.reflect
type combine_flags =
  1. | CF_LT of Wsize.signedness
  2. | CF_LE of Wsize.signedness
  3. | CF_EQ
  4. | CF_NEQ
  5. | CF_GE of Wsize.signedness
  6. | CF_GT of Wsize.signedness
val combine_flags_tag : combine_flags -> BinNums.positive
type box_combine_flags_CF_EQ =
  1. | Box_combine_flags_CF_EQ
type combine_flags_fields_t = __
val combine_flags_fields : combine_flags -> combine_flags_fields_t
val combine_flags_eqb_fields : (combine_flags -> combine_flags -> bool) -> BinNums.positive -> combine_flags_fields_t -> combine_flags_fields_t -> bool
val combine_flags_eqb : combine_flags -> combine_flags -> bool
type opN =
  1. | Opack of Wsize.wsize * Wsize.pelem
  2. | Oarray of BinNums.positive
  3. | Ocombine_flags of combine_flags
val opN_tag : opN -> BinNums.positive
type box_opN_Opack = {
  1. coq_Box_opN_Opack_0 : Wsize.wsize;
  2. coq_Box_opN_Opack_1 : Wsize.pelem;
}
type opN_fields_t = __
val opN_fields : opN -> opN_fields_t
val opN_eqb_fields : (opN -> opN -> bool) -> BinNums.positive -> opN_fields_t -> opN_fields_t -> bool
val opN_eqb : opN -> opN -> bool
val opN_eqb_OK : opN -> opN -> Bool.reflect
val coq_HB_unnamed_factory_1 : op_kind Eqtype.Coq_hasDecEq.axioms_
val operators_op_kind__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_3 : sop1 Eqtype.Coq_hasDecEq.axioms_
val operators_sop1__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_5 : sop2 Eqtype.Coq_hasDecEq.axioms_
val operators_sop2__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_7 : opN Eqtype.Coq_hasDecEq.axioms_
val operators_opN__canonical__eqtype_Equality : Eqtype.Equality.coq_type