package jasmin

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

Module Jasmin.Expr

type __ = Obj.t
type cmp_kind =
  1. | Cmp_int
  2. | Cmp_w of Wsize.signedness * Wsize.wsize
type is_cmp_kind =
  1. | Coq_is_Cmp_int
  2. | Coq_is_Cmp_w of Wsize.signedness * Wsize.is_signedness * Wsize.wsize * Wsize.is_wsize
val cmp_kind_tag : cmp_kind -> BinNums.positive
val is_cmp_kind_inhab : cmp_kind -> is_cmp_kind
val is_cmp_kind_functor : cmp_kind -> is_cmp_kind -> is_cmp_kind
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;
}
val coq_Box_cmp_kind_Cmp_w_0 : box_cmp_kind_Cmp_w -> Wsize.signedness
val coq_Box_cmp_kind_Cmp_w_1 : box_cmp_kind_Cmp_w -> Wsize.wsize
type cmp_kind_fields_t = __
val cmp_kind_fields : cmp_kind -> cmp_kind_fields_t
val cmp_kind_construct : BinNums.positive -> cmp_kind_fields_t -> cmp_kind option
val cmp_kind_induction : 'a1 -> (Wsize.signedness -> Wsize.is_signedness -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> cmp_kind -> is_cmp_kind -> 'a1
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
val cmp_kind_eqb_OK : cmp_kind -> cmp_kind -> Bool.reflect
val cmp_kind_eqb_OK_sumbool : cmp_kind -> cmp_kind -> bool
type op_kind =
  1. | Op_int
  2. | Op_w of Wsize.wsize
type is_op_kind =
  1. | Coq_is_Op_int
  2. | Coq_is_Op_w of Wsize.wsize * Wsize.is_wsize
val op_kind_tag : op_kind -> BinNums.positive
val is_op_kind_inhab : op_kind -> is_op_kind
val is_op_kind_functor : op_kind -> is_op_kind -> is_op_kind
type box_op_kind_Op_int =
  1. | Box_op_kind_Op_int
type box_op_kind_Op_w = Wsize.wsize
val coq_Box_op_kind_Op_w_0 : box_op_kind_Op_w -> Wsize.wsize
type op_kind_fields_t = __
val op_kind_fields : op_kind -> op_kind_fields_t
val op_kind_construct : BinNums.positive -> op_kind_fields_t -> op_kind option
val op_kind_induction : 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> op_kind -> is_op_kind -> 'a1
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
val op_kind_eqb_OK_sumbool : op_kind -> op_kind -> bool
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
type is_wiop1 =
  1. | Coq_is_WIwint_of_int of Wsize.wsize * Wsize.is_wsize
  2. | Coq_is_WIint_of_wint of Wsize.wsize * Wsize.is_wsize
  3. | Coq_is_WIword_of_wint of Wsize.wsize * Wsize.is_wsize
  4. | Coq_is_WIwint_of_word of Wsize.wsize * Wsize.is_wsize
  5. | Coq_is_WIwint_ext of Wsize.wsize * Wsize.is_wsize * Wsize.wsize * Wsize.is_wsize
  6. | Coq_is_WIneg of Wsize.wsize * Wsize.is_wsize
val wiop1_tag : wiop1 -> BinNums.positive
val is_wiop1_inhab : wiop1 -> is_wiop1
val is_wiop1_functor : wiop1 -> is_wiop1 -> is_wiop1
type box_wiop1_WIwint_of_int = Wsize.wsize
val coq_Box_wiop1_WIwint_of_int_0 : box_wiop1_WIwint_of_int -> Wsize.wsize
type box_wiop1_WIwint_ext = {
  1. coq_Box_wiop1_WIwint_ext_0 : Wsize.wsize;
  2. coq_Box_wiop1_WIwint_ext_1 : Wsize.wsize;
}
val coq_Box_wiop1_WIwint_ext_0 : box_wiop1_WIwint_ext -> Wsize.wsize
val coq_Box_wiop1_WIwint_ext_1 : box_wiop1_WIwint_ext -> Wsize.wsize
type wiop1_fields_t = __
val wiop1_fields : wiop1 -> wiop1_fields_t
val wiop1_construct : BinNums.positive -> wiop1_fields_t -> wiop1 option
val wiop1_induction : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> wiop1 -> is_wiop1 -> 'a1
val wiop1_eqb_fields : (wiop1 -> wiop1 -> bool) -> BinNums.positive -> wiop1_fields_t -> wiop1_fields_t -> bool
val wiop1_eqb : wiop1 -> wiop1 -> bool
val wiop1_eqb_OK : wiop1 -> wiop1 -> Bool.reflect
val wiop1_eqb_OK_sumbool : 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
type is_sop1 =
  1. | Coq_is_Oword_of_int of Wsize.wsize * Wsize.is_wsize
  2. | Coq_is_Oint_of_word of Wsize.signedness * Wsize.is_signedness * Wsize.wsize * Wsize.is_wsize
  3. | Coq_is_Osignext of Wsize.wsize * Wsize.is_wsize * Wsize.wsize * Wsize.is_wsize
  4. | Coq_is_Ozeroext of Wsize.wsize * Wsize.is_wsize * Wsize.wsize * Wsize.is_wsize
  5. | Coq_is_Onot
  6. | Coq_is_Olnot of Wsize.wsize * Wsize.is_wsize
  7. | Coq_is_Oneg of op_kind * is_op_kind
  8. | Coq_is_Owi1 of Wsize.signedness * Wsize.is_signedness * wiop1 * is_wiop1
val sop1_tag : sop1 -> BinNums.positive
val is_sop1_inhab : sop1 -> is_sop1
val is_sop1_functor : sop1 -> is_sop1 -> is_sop1
type box_sop1_Oword_of_int = Wsize.wsize
val coq_Box_sop1_Oword_of_int_0 : box_sop1_Oword_of_int -> Wsize.wsize
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;
}
val coq_Box_sop1_Oint_of_word_0 : box_sop1_Oint_of_word -> Wsize.signedness
val coq_Box_sop1_Oint_of_word_1 : box_sop1_Oint_of_word -> Wsize.wsize
type box_sop1_Osignext = {
  1. coq_Box_sop1_Osignext_0 : Wsize.wsize;
  2. coq_Box_sop1_Osignext_1 : Wsize.wsize;
}
val coq_Box_sop1_Osignext_0 : box_sop1_Osignext -> Wsize.wsize
val coq_Box_sop1_Osignext_1 : box_sop1_Osignext -> Wsize.wsize
type box_sop1_Onot =
  1. | Box_sop1_Onot
type box_sop1_Oneg = op_kind
val coq_Box_sop1_Oneg_0 : box_sop1_Oneg -> op_kind
type box_sop1_Owi1 = {
  1. coq_Box_sop1_Owi1_0 : Wsize.signedness;
  2. coq_Box_sop1_Owi1_1 : wiop1;
}
val coq_Box_sop1_Owi1_0 : box_sop1_Owi1 -> Wsize.signedness
val coq_Box_sop1_Owi1_1 : box_sop1_Owi1 -> wiop1
type sop1_fields_t = __
val sop1_fields : sop1 -> sop1_fields_t
val sop1_construct : BinNums.positive -> sop1_fields_t -> sop1 option
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
val sop1_eqb_OK_sumbool : sop1 -> sop1 -> bool
val uint_of_word : Wsize.wsize -> sop1
val sint_of_word : Wsize.wsize -> sop1
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
type is_wiop2 =
  1. | Coq_is_WIadd
  2. | Coq_is_WImul
  3. | Coq_is_WIsub
  4. | Coq_is_WIdiv
  5. | Coq_is_WImod
  6. | Coq_is_WIshl
  7. | Coq_is_WIshr
  8. | Coq_is_WIeq
  9. | Coq_is_WIneq
  10. | Coq_is_WIlt
  11. | Coq_is_WIle
  12. | Coq_is_WIgt
  13. | Coq_is_WIge
val wiop2_tag : wiop2 -> BinNums.positive
val is_wiop2_inhab : wiop2 -> is_wiop2
val is_wiop2_functor : wiop2 -> is_wiop2 -> is_wiop2
type box_wiop2_WIadd =
  1. | Box_wiop2_WIadd
type wiop2_fields_t = __
val wiop2_fields : wiop2 -> wiop2_fields_t
val wiop2_construct : BinNums.positive -> wiop2_fields_t -> wiop2 option
val wiop2_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> wiop2 -> is_wiop2 -> 'a1
val wiop2_eqb_fields : (wiop2 -> wiop2 -> bool) -> BinNums.positive -> wiop2_fields_t -> wiop2_fields_t -> bool
val wiop2_eqb : wiop2 -> wiop2 -> bool
val wiop2_eqb_OK : wiop2 -> wiop2 -> Bool.reflect
val wiop2_eqb_OK_sumbool : 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
type is_sop2 =
  1. | Coq_is_Obeq
  2. | Coq_is_Oand
  3. | Coq_is_Oor
  4. | Coq_is_Oadd of op_kind * is_op_kind
  5. | Coq_is_Omul of op_kind * is_op_kind
  6. | Coq_is_Osub of op_kind * is_op_kind
  7. | Coq_is_Odiv of Wsize.signedness * Wsize.is_signedness * op_kind * is_op_kind
  8. | Coq_is_Omod of Wsize.signedness * Wsize.is_signedness * op_kind * is_op_kind
  9. | Coq_is_Oland of Wsize.wsize * Wsize.is_wsize
  10. | Coq_is_Olor of Wsize.wsize * Wsize.is_wsize
  11. | Coq_is_Olxor of Wsize.wsize * Wsize.is_wsize
  12. | Coq_is_Olsr of Wsize.wsize * Wsize.is_wsize
  13. | Coq_is_Olsl of op_kind * is_op_kind
  14. | Coq_is_Oasr of op_kind * is_op_kind
  15. | Coq_is_Oror of Wsize.wsize * Wsize.is_wsize
  16. | Coq_is_Orol of Wsize.wsize * Wsize.is_wsize
  17. | Coq_is_Oeq of op_kind * is_op_kind
  18. | Coq_is_Oneq of op_kind * is_op_kind
  19. | Coq_is_Olt of cmp_kind * is_cmp_kind
  20. | Coq_is_Ole of cmp_kind * is_cmp_kind
  21. | Coq_is_Ogt of cmp_kind * is_cmp_kind
  22. | Coq_is_Oge of cmp_kind * is_cmp_kind
  23. | Coq_is_Ovadd of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  24. | Coq_is_Ovsub of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  25. | Coq_is_Ovmul of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  26. | Coq_is_Ovlsr of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  27. | Coq_is_Ovlsl of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  28. | Coq_is_Ovasr of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  29. | Coq_is_Owi2 of Wsize.signedness * Wsize.is_signedness * Wsize.wsize * Wsize.is_wsize * wiop2 * is_wiop2
val sop2_tag : sop2 -> BinNums.positive
val is_sop2_inhab : sop2 -> is_sop2
val is_sop2_functor : sop2 -> is_sop2 -> is_sop2
type box_sop2_Obeq =
  1. | Box_sop2_Obeq
type box_sop2_Oadd = op_kind
val coq_Box_sop2_Oadd_0 : box_sop2_Oadd -> op_kind
type box_sop2_Odiv = {
  1. coq_Box_sop2_Odiv_0 : Wsize.signedness;
  2. coq_Box_sop2_Odiv_1 : op_kind;
}
val coq_Box_sop2_Odiv_0 : box_sop2_Odiv -> Wsize.signedness
val coq_Box_sop2_Odiv_1 : box_sop2_Odiv -> op_kind
type box_sop2_Oland = Wsize.wsize
val coq_Box_sop2_Oland_0 : box_sop2_Oland -> Wsize.wsize
type box_sop2_Olt = cmp_kind
val coq_Box_sop2_Olt_0 : box_sop2_Olt -> cmp_kind
type box_sop2_Ovadd = {
  1. coq_Box_sop2_Ovadd_0 : Wsize.velem;
  2. coq_Box_sop2_Ovadd_1 : Wsize.wsize;
}
val coq_Box_sop2_Ovadd_0 : box_sop2_Ovadd -> Wsize.velem
val coq_Box_sop2_Ovadd_1 : box_sop2_Ovadd -> 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;
}
val coq_Box_sop2_Owi2_0 : box_sop2_Owi2 -> Wsize.signedness
val coq_Box_sop2_Owi2_1 : box_sop2_Owi2 -> Wsize.wsize
val coq_Box_sop2_Owi2_2 : box_sop2_Owi2 -> wiop2
type sop2_fields_t = __
val sop2_fields : sop2 -> sop2_fields_t
val sop2_construct : BinNums.positive -> sop2_fields_t -> sop2 option
val sop2_induction : 'a1 -> 'a1 -> 'a1 -> (op_kind -> is_op_kind -> 'a1) -> (op_kind -> is_op_kind -> 'a1) -> (op_kind -> is_op_kind -> 'a1) -> (Wsize.signedness -> Wsize.is_signedness -> op_kind -> is_op_kind -> 'a1) -> (Wsize.signedness -> Wsize.is_signedness -> op_kind -> is_op_kind -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (op_kind -> is_op_kind -> 'a1) -> (op_kind -> is_op_kind -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (op_kind -> is_op_kind -> 'a1) -> (op_kind -> is_op_kind -> 'a1) -> (cmp_kind -> is_cmp_kind -> 'a1) -> (cmp_kind -> is_cmp_kind -> 'a1) -> (cmp_kind -> is_cmp_kind -> 'a1) -> (cmp_kind -> is_cmp_kind -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.signedness -> Wsize.is_signedness -> Wsize.wsize -> Wsize.is_wsize -> wiop2 -> is_wiop2 -> 'a1) -> sop2 -> is_sop2 -> 'a1
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
val sop2_eqb_OK_sumbool : sop2 -> sop2 -> bool
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
type is_combine_flags =
  1. | Coq_is_CF_LT of Wsize.signedness * Wsize.is_signedness
  2. | Coq_is_CF_LE of Wsize.signedness * Wsize.is_signedness
  3. | Coq_is_CF_EQ
  4. | Coq_is_CF_NEQ
  5. | Coq_is_CF_GE of Wsize.signedness * Wsize.is_signedness
  6. | Coq_is_CF_GT of Wsize.signedness * Wsize.is_signedness
val combine_flags_tag : combine_flags -> BinNums.positive
val is_combine_flags_inhab : combine_flags -> is_combine_flags
val is_combine_flags_functor : combine_flags -> is_combine_flags -> is_combine_flags
type box_combine_flags_CF_LT = Wsize.signedness
val coq_Box_combine_flags_CF_LT_0 : box_combine_flags_CF_LT -> Wsize.signedness
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_construct : BinNums.positive -> combine_flags_fields_t -> combine_flags option
val combine_flags_induction : (Wsize.signedness -> Wsize.is_signedness -> 'a1) -> (Wsize.signedness -> Wsize.is_signedness -> 'a1) -> 'a1 -> 'a1 -> (Wsize.signedness -> Wsize.is_signedness -> 'a1) -> (Wsize.signedness -> Wsize.is_signedness -> 'a1) -> combine_flags -> is_combine_flags -> 'a1
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
val combine_flags_eqb_OK : combine_flags -> combine_flags -> Bool.reflect
val combine_flags_eqb_OK_sumbool : combine_flags -> combine_flags -> bool
type opN =
  1. | Opack of Wsize.wsize * Wsize.pelem
  2. | Ocombine_flags of combine_flags
type is_opN =
  1. | Coq_is_Opack of Wsize.wsize * Wsize.is_wsize * Wsize.pelem * Wsize.is_pelem
  2. | Coq_is_Ocombine_flags of combine_flags * is_combine_flags
val opN_tag : opN -> BinNums.positive
val is_opN_inhab : opN -> is_opN
val is_opN_functor : opN -> is_opN -> is_opN
type box_opN_Opack = {
  1. coq_Box_opN_Opack_0 : Wsize.wsize;
  2. coq_Box_opN_Opack_1 : Wsize.pelem;
}
val coq_Box_opN_Opack_0 : box_opN_Opack -> Wsize.wsize
val coq_Box_opN_Opack_1 : box_opN_Opack -> Wsize.pelem
type box_opN_Ocombine_flags = combine_flags
val coq_Box_opN_Ocombine_flags_0 : box_opN_Ocombine_flags -> combine_flags
type opN_fields_t = __
val opN_fields : opN -> opN_fields_t
val opN_construct : BinNums.positive -> opN_fields_t -> opN option
val opN_induction : (Wsize.wsize -> Wsize.is_wsize -> Wsize.pelem -> Wsize.is_pelem -> 'a1) -> (combine_flags -> is_combine_flags -> 'a1) -> opN -> is_opN -> 'a1
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 opN_eqb_OK_sumbool : opN -> opN -> bool
val coq_HB_unnamed_factory_1 : op_kind Eqtype.Coq_hasDecEq.axioms_
val expr_op_kind__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_3 : sop1 Eqtype.Coq_hasDecEq.axioms_
val expr_sop1__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_5 : sop2 Eqtype.Coq_hasDecEq.axioms_
val expr_sop2__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_7 : opN Eqtype.Coq_hasDecEq.axioms_
val expr_opN__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val etype_of_wiop1 : Wsize.signedness -> wiop1 -> 'a1 Type.extended_type * 'a1 Type.extended_type
val type_of_wiop1 : wiop1 -> Type.stype * Type.stype
val type_of_opk : op_kind -> Type.stype
val etype_of_opk : op_kind -> 'a1 Type.extended_type
val etype_of_op1 : sop1 -> 'a1 Type.extended_type * 'a1 Type.extended_type
val type_of_op1 : sop1 -> Type.stype * Type.stype
val type_of_wiop2 : Wsize.wsize -> wiop2 -> (Type.stype * Type.stype) * Type.stype
val opk8 : op_kind -> op_kind
val opk_of_cmpk : cmp_kind -> op_kind
val etype_of_op2 : sop2 -> ('a1 Type.extended_type * 'a1 Type.extended_type) * 'a1 Type.extended_type
val type_of_op2 : sop2 -> (Type.stype * Type.stype) * Type.stype
val tin_combine_flags : Type.stype list
val type_of_opN : opN -> Type.stype list * Type.stype
module type TAG = sig ... end
module VarInfo : TAG
type var_info = Location.t
val dummy_var_info : var_info
type var_i = {
  1. v_var : Var0.Var.var;
  2. v_info : var_info;
}
val v_var : var_i -> Var0.Var.var
val v_info : var_i -> var_info
val mk_var_i : Var0.Var.var -> var_i
type v_scope =
  1. | Slocal
  2. | Sglob
type is_v_scope =
  1. | Coq_is_Slocal
  2. | Coq_is_Sglob
val v_scope_tag : v_scope -> BinNums.positive
val is_v_scope_inhab : v_scope -> is_v_scope
val is_v_scope_functor : v_scope -> is_v_scope -> is_v_scope
type box_v_scope_Slocal =
  1. | Box_v_scope_Slocal
type v_scope_fields_t = __
val v_scope_fields : v_scope -> v_scope_fields_t
val v_scope_construct : BinNums.positive -> v_scope_fields_t -> v_scope option
val v_scope_induction : 'a1 -> 'a1 -> v_scope -> is_v_scope -> 'a1
val v_scope_eqb_fields : (v_scope -> v_scope -> bool) -> BinNums.positive -> v_scope_fields_t -> v_scope_fields_t -> bool
val v_scope_eqb : v_scope -> v_scope -> bool
val v_scope_eqb_OK : v_scope -> v_scope -> Bool.reflect
val v_scope_eqb_OK_sumbool : v_scope -> v_scope -> bool
val coq_HB_unnamed_factory_9 : v_scope Eqtype.Coq_hasDecEq.axioms_
val expr_v_scope__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type gvar = {
  1. gv : var_i;
  2. gs : v_scope;
}
val gv : gvar -> var_i
val gs : gvar -> v_scope
val mk_gvar : var_i -> gvar
val mk_lvar : var_i -> gvar
val is_lvar : gvar -> bool
val is_glob : gvar -> bool
type pexpr =
  1. | Pconst of BinNums.coq_Z
  2. | Pbool of bool
  3. | Parr_init of BinNums.positive
  4. | Pvar of gvar
  5. | Pget of Memory_model.aligned * Warray_.arr_access * Wsize.wsize * gvar * pexpr
  6. | Psub of Warray_.arr_access * Wsize.wsize * BinNums.positive * gvar * pexpr
  7. | Pload of Memory_model.aligned * Wsize.wsize * pexpr
  8. | Papp1 of sop1 * pexpr
  9. | Papp2 of sop2 * pexpr * pexpr
  10. | PappN of opN * pexpr list
  11. | Pif of Type.stype * pexpr * pexpr * pexpr
val coq_Plvar : var_i -> pexpr
val enot : pexpr -> pexpr
val eor : pexpr -> pexpr -> pexpr
val eand : pexpr -> pexpr -> pexpr
val eeq : pexpr -> pexpr -> pexpr
val eneq : pexpr -> pexpr -> pexpr
val eaddw : Wsize.wsize -> pexpr -> pexpr -> pexpr
val cf_of_condition : sop2 -> (combine_flags * Wsize.wsize) option
val pexpr_of_cf : combine_flags -> var_info -> Var0.Var.var list -> pexpr
val get_pvar : pexpr -> Var0.Var.var Utils0.exec
val get_lvar : lval -> Var0.Var.var Utils0.exec
val coq_Lnone_b : var_info -> lval
val var_info_of_lval : lval -> var_info
type dir =
  1. | UpTo
  2. | DownTo
type is_dir =
  1. | Coq_is_UpTo
  2. | Coq_is_DownTo
val dir_tag : dir -> BinNums.positive
val is_dir_inhab : dir -> is_dir
val is_dir_functor : dir -> is_dir -> is_dir
type box_dir_UpTo =
  1. | Box_dir_UpTo
type dir_fields_t = __
val dir_fields : dir -> dir_fields_t
val dir_construct : BinNums.positive -> dir_fields_t -> dir option
val dir_induction : 'a1 -> 'a1 -> dir -> is_dir -> 'a1
val dir_eqb_fields : (dir -> dir -> bool) -> BinNums.positive -> dir_fields_t -> dir_fields_t -> bool
val dir_eqb : dir -> dir -> bool
val dir_eqb_OK : dir -> dir -> Bool.reflect
val dir_eqb_OK_sumbool : dir -> dir -> bool
val coq_HB_unnamed_factory_11 : dir Eqtype.Coq_hasDecEq.axioms_
val expr_dir__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type range = (dir * pexpr) * pexpr
val wrange : dir -> BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Z list
module type InstrInfoT = sig ... end
type instr_info = IInfo.t
val dummy_instr_info : instr_info
val ii_with_location : instr_info -> instr_info
val ii_is_inline : instr_info -> bool
val var_info_of_ii : instr_info -> var_info
type assgn_tag =
  1. | AT_none
  2. | AT_keep
  3. | AT_rename
  4. | AT_inline
  5. | AT_phinode
type is_assgn_tag =
  1. | Coq_is_AT_none
  2. | Coq_is_AT_keep
  3. | Coq_is_AT_rename
  4. | Coq_is_AT_inline
  5. | Coq_is_AT_phinode
val assgn_tag_tag : assgn_tag -> BinNums.positive
val is_assgn_tag_inhab : assgn_tag -> is_assgn_tag
val is_assgn_tag_functor : assgn_tag -> is_assgn_tag -> is_assgn_tag
type box_assgn_tag_AT_none =
  1. | Box_assgn_tag_AT_none
type assgn_tag_fields_t = __
val assgn_tag_fields : assgn_tag -> assgn_tag_fields_t
val assgn_tag_construct : BinNums.positive -> assgn_tag_fields_t -> assgn_tag option
val assgn_tag_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> assgn_tag -> is_assgn_tag -> 'a1
val assgn_tag_eqb_fields : (assgn_tag -> assgn_tag -> bool) -> BinNums.positive -> assgn_tag_fields_t -> assgn_tag_fields_t -> bool
val assgn_tag_eqb : assgn_tag -> assgn_tag -> bool
val assgn_tag_eqb_OK : assgn_tag -> assgn_tag -> Bool.reflect
val assgn_tag_eqb_OK_sumbool : assgn_tag -> assgn_tag -> bool
val coq_HB_unnamed_factory_13 : assgn_tag Eqtype.Coq_hasDecEq.axioms_
val expr_assgn_tag__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type align =
  1. | Align
  2. | NoAlign
type 'asm_op instr_r =
  1. | Cassgn of lval * assgn_tag * Type.stype * pexpr
  2. | Copn of lval list * assgn_tag * 'asm_op Sopn.sopn * pexpr list
  3. | Csyscall of lval list * BinNums.positive Syscall_t.syscall_t * pexpr list
  4. | Cif of pexpr * 'asm_op instr list * 'asm_op instr list
  5. | Cfor of var_i * range * 'asm_op instr list
  6. | Cwhile of align * 'asm_op instr list * pexpr * instr_info * 'asm_op instr list
  7. | Ccall of lval list * Var0.funname * pexpr list
and 'asm_op instr =
  1. | MkI of instr_info * 'asm_op instr_r
val cmd_rect_aux : 'a1 Sopn.asmOp -> 'a3 -> ('a1 instr -> 'a1 instr list -> 'a2 -> 'a3 -> 'a3) -> ('a1 instr -> 'a2) -> 'a1 instr list -> 'a3
val instr_Rect : 'a1 Sopn.asmOp -> ('a1 instr_r -> instr_info -> 'a2 -> 'a3) -> 'a4 -> ('a1 instr -> 'a1 instr list -> 'a3 -> 'a4 -> 'a4) -> (lval -> assgn_tag -> Type.stype -> pexpr -> 'a2) -> (lval list -> assgn_tag -> 'a1 Sopn.sopn -> pexpr list -> 'a2) -> (lval list -> BinNums.positive Syscall_t.syscall_t -> pexpr list -> 'a2) -> (pexpr -> 'a1 instr list -> 'a1 instr list -> 'a4 -> 'a4 -> 'a2) -> (var_i -> dir -> pexpr -> pexpr -> 'a1 instr list -> 'a4 -> 'a2) -> (align -> 'a1 instr list -> pexpr -> instr_info -> 'a1 instr list -> 'a4 -> 'a4 -> 'a2) -> (lval list -> Var0.funname -> pexpr list -> 'a2) -> 'a1 instr -> 'a3
val instr_r_Rect : 'a1 Sopn.asmOp -> ('a1 instr_r -> instr_info -> 'a2 -> 'a3) -> 'a4 -> ('a1 instr -> 'a1 instr list -> 'a3 -> 'a4 -> 'a4) -> (lval -> assgn_tag -> Type.stype -> pexpr -> 'a2) -> (lval list -> assgn_tag -> 'a1 Sopn.sopn -> pexpr list -> 'a2) -> (lval list -> BinNums.positive Syscall_t.syscall_t -> pexpr list -> 'a2) -> (pexpr -> 'a1 instr list -> 'a1 instr list -> 'a4 -> 'a4 -> 'a2) -> (var_i -> dir -> pexpr -> pexpr -> 'a1 instr list -> 'a4 -> 'a2) -> (align -> 'a1 instr list -> pexpr -> instr_info -> 'a1 instr list -> 'a4 -> 'a4 -> 'a2) -> (lval list -> Var0.funname -> pexpr list -> 'a2) -> 'a1 instr_r -> 'a2
val cmd_rect : 'a1 Sopn.asmOp -> ('a1 instr_r -> instr_info -> 'a2 -> 'a3) -> 'a4 -> ('a1 instr -> 'a1 instr list -> 'a3 -> 'a4 -> 'a4) -> (lval -> assgn_tag -> Type.stype -> pexpr -> 'a2) -> (lval list -> assgn_tag -> 'a1 Sopn.sopn -> pexpr list -> 'a2) -> (lval list -> BinNums.positive Syscall_t.syscall_t -> pexpr list -> 'a2) -> (pexpr -> 'a1 instr list -> 'a1 instr list -> 'a4 -> 'a4 -> 'a2) -> (var_i -> dir -> pexpr -> pexpr -> 'a1 instr list -> 'a4 -> 'a2) -> (align -> 'a1 instr list -> pexpr -> instr_info -> 'a1 instr list -> 'a4 -> 'a4 -> 'a2) -> (lval list -> Var0.funname -> pexpr list -> 'a2) -> 'a1 instr list -> 'a4
module type FunInfoT = sig ... end
module FunInfo : FunInfoT
type fun_info = FInfo.t
val entry_info_of_fun_info : fun_info -> instr_info
val ret_info_of_fun_info : fun_info -> instr_info
type progT =
  1. | Build_progT
type extra_fun_t = __
type extra_prog_t = __
type extra_val_t = __
type ('asm_op, 'extra_fun_t) _fundef = {
  1. f_info : fun_info;
  2. f_tyin : Type.stype list;
  3. f_params : var_i list;
  4. f_body : 'asm_op instr list;
  5. f_tyout : Type.stype list;
  6. f_res : var_i list;
  7. f_extra : 'extra_fun_t;
}
val f_info : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> fun_info
val f_tyin : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> Type.stype list
val f_params : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> var_i list
val f_body : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> 'a1 instr list
val f_tyout : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> Type.stype list
val f_res : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> var_i list
val f_extra : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> 'a2
type ('asm_op, 'extra_fun_t) _fun_decl = Var0.funname * ('asm_op, 'extra_fun_t) _fundef
type ('asm_op, 'extra_fun_t, 'extra_prog_t) _prog = {
  1. p_funcs : ('asm_op, 'extra_fun_t) _fun_decl list;
  2. p_globs : Global.glob_decl list;
  3. p_extra : 'extra_prog_t;
}
val p_funcs : 'a1 Sopn.asmOp -> ('a1, 'a2, 'a3) _prog -> ('a1, 'a2) _fun_decl list
val p_globs : 'a1 Sopn.asmOp -> ('a1, 'a2, 'a3) _prog -> Global.glob_decl list
val p_extra : 'a1 Sopn.asmOp -> ('a1, 'a2, 'a3) _prog -> 'a3
type 'asm_op fundef = ('asm_op, extra_fun_t) _fundef
type function_signature = Type.stype list * Type.stype list
val signature_of_fundef : 'a1 Sopn.asmOp -> progT -> 'a1 fundef -> function_signature
type 'asm_op fun_decl = Var0.funname * 'asm_op fundef
type 'asm_op prog = ('asm_op, extra_fun_t, extra_prog_t) _prog
val coq_Build_prog : 'a1 Sopn.asmOp -> progT -> ('a1, extra_fun_t) _fun_decl list -> Global.glob_decl list -> extra_prog_t -> 'a1 prog
val progUnit : progT
type 'asm_op ufundef = 'asm_op fundef
type 'asm_op ufun_decl = 'asm_op fun_decl
type 'asm_op ufun_decls = 'asm_op fun_decl list
type 'asm_op uprog = 'asm_op prog
type 'asm_op _ufundef = ('asm_op, unit) _fundef
type 'asm_op _ufun_decl = ('asm_op, unit) _fun_decl
type 'asm_op _ufun_decls = ('asm_op, unit) _fun_decl list
type 'asm_op _uprog = ('asm_op, unit, unit) _prog
val to_uprog : 'a1 Sopn.asmOp -> 'a1 _uprog -> 'a1 uprog
type saved_stack =
  1. | SavedStackNone
  2. | SavedStackReg of Var0.Var.var
  3. | SavedStackStk of BinNums.coq_Z
val saved_stack_beq : saved_stack -> saved_stack -> bool
val saved_stack_eq_axiom : saved_stack Eqtype.eq_axiom
val coq_HB_unnamed_factory_15 : saved_stack Eqtype.Coq_hasDecEq.axioms_
val expr_saved_stack__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type return_address_location =
  1. | RAnone
  2. | RAreg of Var0.Var.var * Var0.Var.var option
  3. | RAstack of Var0.Var.var option * Var0.Var.var option * BinNums.coq_Z * Var0.Var.var option
val is_RAnone : return_address_location -> bool
val is_RAstack : return_address_location -> bool
val return_address_location_beq : return_address_location -> return_address_location -> bool
val return_address_location_eq_axiom : return_address_location Eqtype.eq_axiom
val expr_return_address_location__canonical__eqtype_Equality : Eqtype.Equality.coq_type
type stk_fun_extra = {
  1. sf_align : Wsize.wsize;
  2. sf_stk_sz : BinNums.coq_Z;
  3. sf_stk_ioff : BinNums.coq_Z;
  4. sf_stk_extra_sz : BinNums.coq_Z;
  5. sf_stk_max : BinNums.coq_Z;
  6. sf_max_call_depth : BinNums.coq_Z;
  7. sf_to_save : (Var0.Var.var * BinNums.coq_Z) list;
  8. sf_save_stack : saved_stack;
  9. sf_return_address : return_address_location;
  10. sf_align_args : Wsize.wsize list;
}
val sf_align : stk_fun_extra -> Wsize.wsize
val sf_stk_sz : stk_fun_extra -> BinNums.coq_Z
val sf_stk_ioff : stk_fun_extra -> BinNums.coq_Z
val sf_stk_extra_sz : stk_fun_extra -> BinNums.coq_Z
val sf_stk_max : stk_fun_extra -> BinNums.coq_Z
val sf_max_call_depth : stk_fun_extra -> BinNums.coq_Z
val sf_to_save : stk_fun_extra -> (Var0.Var.var * BinNums.coq_Z) list
val sf_save_stack : stk_fun_extra -> saved_stack
val sf_return_address : stk_fun_extra -> return_address_location
val sf_align_args : stk_fun_extra -> Wsize.wsize list
type sprog_extra = {
  1. sp_rsp : Ident.Ident.ident;
  2. sp_rip : Ident.Ident.ident;
  3. sp_globs : Ssralg.GRing.ComRing.sort list;
  4. sp_glob_names : ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list;
}
val sp_globs : sprog_extra -> Ssralg.GRing.ComRing.sort list
val sp_glob_names : sprog_extra -> ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list
val progStack : Wsize.coq_PointerData -> progT
type 'asm_op sfundef = 'asm_op fundef
type 'asm_op sfun_decl = 'asm_op fun_decl
type 'asm_op sfun_decls = 'asm_op fun_decl list
type 'asm_op sprog = 'asm_op prog
type 'asm_op _sfundef = ('asm_op, stk_fun_extra) _fundef
type 'asm_op _sfun_decl = ('asm_op, stk_fun_extra) _fun_decl
type 'asm_op _sfun_decls = ('asm_op, stk_fun_extra) _fun_decl list
type 'asm_op _sprog = ('asm_op, stk_fun_extra, sprog_extra) _prog
val to_sprog : Wsize.coq_PointerData -> 'a1 Sopn.asmOp -> 'a1 _sprog -> 'a1 sprog
val with_body : 'a1 Sopn.asmOp -> ('a1, 'a2) _fundef -> 'a1 instr list -> ('a1, 'a2) _fundef
val is_const : pexpr -> BinNums.coq_Z option
val is_bool : pexpr -> bool option
val is_Papp2 : pexpr -> ((sop2 * pexpr) * pexpr) option
val is_Pload : pexpr -> bool
val is_load : pexpr -> bool
val is_array_init : pexpr -> bool
val cast_w : Wsize.wsize -> pexpr -> pexpr
val cast_ptr : Wsize.coq_PointerData -> pexpr -> pexpr
val eword_of_int : Wsize.wsize -> BinNums.coq_Z -> pexpr
val is_wconst : Wsize.wsize -> pexpr -> Ssralg.GRing.ComRing.sort option
val is_wconst_of_size : Eqtype.Equality.sort -> pexpr -> BinNums.coq_Z option
val vrvs_rec : Var0.SvExtra.Sv.t -> lval list -> Var0.SvExtra.Sv.t
val vrv : lval -> Var0.SvExtra.Sv.t
val vrvs : lval list -> Var0.SvExtra.Sv.t
val lv_write_mem : lval -> bool
val write_i_rec : 'a1 Sopn.asmOp -> Var0.SvExtra.Sv.t -> 'a1 instr_r -> Var0.SvExtra.Sv.t
val write_I_rec : 'a1 Sopn.asmOp -> Var0.SvExtra.Sv.t -> 'a1 instr -> Var0.SvExtra.Sv.t
val write_i : 'a1 Sopn.asmOp -> 'a1 instr_r -> Var0.SvExtra.Sv.t
val write_I : 'a1 Sopn.asmOp -> 'a1 instr -> Var0.SvExtra.Sv.t
val write_c_rec : 'a1 Sopn.asmOp -> Var0.SvExtra.Sv.t -> 'a1 instr list -> Var0.SvExtra.Sv.t
val write_c : 'a1 Sopn.asmOp -> 'a1 instr list -> Var0.SvExtra.Sv.t
val use_mem : pexpr -> bool
val read_gvar : gvar -> Var0.SvExtra.Sv.t
val read_e : pexpr -> Var0.SvExtra.Sv.t
val read_es_rec : Var0.SvExtra.Sv.t -> pexpr list -> Var0.SvExtra.Sv.t
val read_es : pexpr list -> Var0.SvExtra.Sv.t
val read_rv_rec : Var0.SvExtra.Sv.t -> lval -> Var0.SvExtra.Sv.t
val read_rv : lval -> Var0.SvExtra.Sv.t
val read_rvs_rec : Var0.SvExtra.Sv.t -> lval list -> Var0.SvExtra.Sv.t
val read_rvs : lval list -> Var0.SvExtra.Sv.t
val read_i_rec : 'a1 Sopn.asmOp -> Var0.SvExtra.Sv.t -> 'a1 instr_r -> Var0.SvExtra.Sv.t
val read_I_rec : 'a1 Sopn.asmOp -> Var0.SvExtra.Sv.t -> 'a1 instr -> Var0.SvExtra.Sv.t
val read_c_rec : 'a1 Sopn.asmOp -> Var0.SvExtra.Sv.t -> 'a1 instr list -> Var0.SvExtra.Sv.t
val read_i : 'a1 Sopn.asmOp -> 'a1 instr_r -> Var0.SvExtra.Sv.t
val read_I : 'a1 Sopn.asmOp -> 'a1 instr -> Var0.SvExtra.Sv.t
val read_c : 'a1 Sopn.asmOp -> 'a1 instr list -> Var0.SvExtra.Sv.t
val vars_I : 'a1 Sopn.asmOp -> 'a1 instr -> Var0.SvExtra.Sv.t
val vars_c : 'a1 Sopn.asmOp -> 'a1 instr list -> Var0.SvExtra.Sv.t
val vars_lval : lval -> Var0.SvExtra.Sv.t
val vars_lvals : lval list -> Var0.SvExtra.Sv.t
val vars_l : var_i list -> Var0.SvExtra.Sv.t
val vars_fd : 'a1 Sopn.asmOp -> progT -> 'a1 fundef -> Var0.SvExtra.Sv.t
val vars_p : 'a1 Sopn.asmOp -> progT -> 'a1 fun_decl list -> Var0.SvExtra.Sv.t
val eq_gvar : gvar -> gvar -> bool
val eq_expr : pexpr -> pexpr -> bool
val to_lvals : Var0.Var.var list -> lval list
val is_false : pexpr -> bool
val is_zero : Eqtype.Equality.sort -> pexpr -> bool
val instr_of_copn_args : 'a1 Sopn.asmOp -> assgn_tag -> ((lval list * 'a1 Sopn.sopn) * pexpr list) -> 'a1 instr_r