package jasmin

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

Module Jasmin.Riscv_decl

type __ = Obj.t
val riscv_reg_size : Wsize.wsize
val riscv_xreg_size : Wsize.wsize
type register =
  1. | RA
  2. | SP
  3. | X5
  4. | X6
  5. | X7
  6. | X8
  7. | X9
  8. | X10
  9. | X11
  10. | X12
  11. | X13
  12. | X14
  13. | X15
  14. | X16
  15. | X17
  16. | X18
  17. | X19
  18. | X20
  19. | X21
  20. | X22
  21. | X23
  22. | X24
  23. | X25
  24. | X26
  25. | X27
  26. | X28
  27. | X29
  28. | X30
  29. | X31
val register_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> '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 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
type is_register =
  1. | Coq_is_RA
  2. | Coq_is_SP
  3. | Coq_is_X5
  4. | Coq_is_X6
  5. | Coq_is_X7
  6. | Coq_is_X8
  7. | Coq_is_X9
  8. | Coq_is_X10
  9. | Coq_is_X11
  10. | Coq_is_X12
  11. | Coq_is_X13
  12. | Coq_is_X14
  13. | Coq_is_X15
  14. | Coq_is_X16
  15. | Coq_is_X17
  16. | Coq_is_X18
  17. | Coq_is_X19
  18. | Coq_is_X20
  19. | Coq_is_X21
  20. | Coq_is_X22
  21. | Coq_is_X23
  22. | Coq_is_X24
  23. | Coq_is_X25
  24. | Coq_is_X26
  25. | Coq_is_X27
  26. | Coq_is_X28
  27. | Coq_is_X29
  28. | Coq_is_X30
  29. | Coq_is_X31
val is_register_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> '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 -> '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_RA =
  1. | Box_register_RA
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 -> '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 riscv_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 condition_kind =
  1. | EQ
  2. | NE
  3. | LT of Wsize.signedness
  4. | GE of Wsize.signedness
val condition_kind_rect : 'a1 -> 'a1 -> (Wsize.signedness -> 'a1) -> (Wsize.signedness -> 'a1) -> condition_kind -> 'a1
val condition_kind_rec : 'a1 -> 'a1 -> (Wsize.signedness -> 'a1) -> (Wsize.signedness -> 'a1) -> condition_kind -> 'a1
type is_condition_kind =
  1. | Coq_is_EQ
  2. | Coq_is_NE
  3. | Coq_is_LT of Wsize.signedness * Wsize.is_signedness
  4. | Coq_is_GE of Wsize.signedness * Wsize.is_signedness
val is_condition_kind_rect : 'a1 -> 'a1 -> (Wsize.signedness -> Wsize.is_signedness -> 'a1) -> (Wsize.signedness -> Wsize.is_signedness -> 'a1) -> condition_kind -> is_condition_kind -> 'a1
val is_condition_kind_rec : 'a1 -> 'a1 -> (Wsize.signedness -> Wsize.is_signedness -> 'a1) -> (Wsize.signedness -> Wsize.is_signedness -> 'a1) -> condition_kind -> is_condition_kind -> 'a1
val condition_kind_tag : condition_kind -> BinNums.positive
val is_condition_kind_inhab : condition_kind -> is_condition_kind
val is_condition_kind_functor : condition_kind -> is_condition_kind -> is_condition_kind
type box_condition_kind_EQ =
  1. | Box_condition_kind_EQ
type box_condition_kind_LT = Wsize.signedness
val coq_Box_condition_kind_LT_0 : box_condition_kind_LT -> Wsize.signedness
type condition_kind_fields_t = __
val condition_kind_fields : condition_kind -> condition_kind_fields_t
val condition_kind_construct : BinNums.positive -> condition_kind_fields_t -> condition_kind option
val condition_kind_induction : 'a1 -> 'a1 -> (Wsize.signedness -> Wsize.is_signedness -> 'a1) -> (Wsize.signedness -> Wsize.is_signedness -> 'a1) -> condition_kind -> is_condition_kind -> 'a1
val condition_kind_eqb_fields : (condition_kind -> condition_kind -> bool) -> BinNums.positive -> condition_kind_fields_t -> condition_kind_fields_t -> bool
val condition_kind_eqb : condition_kind -> condition_kind -> bool
val condition_kind_eqb_OK : condition_kind -> condition_kind -> Bool.reflect
val condition_kind_eqb_OK_sumbool : condition_kind -> condition_kind -> bool
type condt = {
  1. cond_kind : condition_kind;
  2. cond_fst : register option;
  3. cond_snd : register option;
}
val cond_kind : condt -> condition_kind
val cond_fst : condt -> register option
val cond_snd : condt -> register option
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_Build_condt = {
  1. coq_Box_condt_Build_condt_0 : condition_kind;
  2. coq_Box_condt_Build_condt_1 : register option;
  3. coq_Box_condt_Build_condt_2 : register option;
}
val coq_Box_condt_Build_condt_0 : box_condt_Build_condt -> condition_kind
val coq_Box_condt_Build_condt_1 : box_condt_Build_condt -> register option
val coq_Box_condt_Build_condt_2 : box_condt_Build_condt -> register option
type condt_fields_t = box_condt_Build_condt
val condt_fields : condt -> condt_fields_t
val condt_construct : BinNums.positive -> box_condt_Build_condt -> condt option
val condt_eqb_fields : (condt -> condt -> bool) -> BinNums.positive -> box_condt_Build_condt -> box_condt_Build_condt -> 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