package jasmin

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

Module Jasmin.Riscv_instr_decl

type __ = Obj.t
module E : sig ... end
type riscv_op =
  1. | ADD
  2. | ADDI
  3. | SUB
  4. | SLT
  5. | SLTI
  6. | SLTU
  7. | SLTIU
  8. | AND
  9. | ANDI
  10. | OR
  11. | ORI
  12. | XOR
  13. | XORI
  14. | SLL
  15. | SLLI
  16. | SRL
  17. | SRLI
  18. | SRA
  19. | SRAI
  20. | MV
  21. | LA
  22. | LI
  23. | NOT
  24. | NEG
  25. | LOAD of Wsize.signedness * Wsize.wsize
  26. | STORE of Wsize.wsize
  27. | MUL
  28. | MULH
  29. | MULHU
  30. | MULHSU
  31. | DIV
  32. | DIVU
  33. | REM
  34. | REMU
val riscv_op_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 -> (Wsize.signedness -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> riscv_op -> 'a1
val riscv_op_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 -> (Wsize.signedness -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> riscv_op -> 'a1
type is_riscv_op =
  1. | Coq_is_ADD
  2. | Coq_is_ADDI
  3. | Coq_is_SUB
  4. | Coq_is_SLT
  5. | Coq_is_SLTI
  6. | Coq_is_SLTU
  7. | Coq_is_SLTIU
  8. | Coq_is_AND
  9. | Coq_is_ANDI
  10. | Coq_is_OR
  11. | Coq_is_ORI
  12. | Coq_is_XOR
  13. | Coq_is_XORI
  14. | Coq_is_SLL
  15. | Coq_is_SLLI
  16. | Coq_is_SRL
  17. | Coq_is_SRLI
  18. | Coq_is_SRA
  19. | Coq_is_SRAI
  20. | Coq_is_MV
  21. | Coq_is_LA
  22. | Coq_is_LI
  23. | Coq_is_NOT
  24. | Coq_is_NEG
  25. | Coq_is_LOAD of Wsize.signedness * Wsize.is_signedness * Wsize.wsize * Wsize.is_wsize
  26. | Coq_is_STORE of Wsize.wsize * Wsize.is_wsize
  27. | Coq_is_MUL
  28. | Coq_is_MULH
  29. | Coq_is_MULHU
  30. | Coq_is_MULHSU
  31. | Coq_is_DIV
  32. | Coq_is_DIVU
  33. | Coq_is_REM
  34. | Coq_is_REMU
val is_riscv_op_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 -> (Wsize.signedness -> Wsize.is_signedness -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> riscv_op -> is_riscv_op -> 'a1
val is_riscv_op_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 -> (Wsize.signedness -> Wsize.is_signedness -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> riscv_op -> is_riscv_op -> 'a1
val riscv_op_tag : riscv_op -> BinNums.positive
val is_riscv_op_inhab : riscv_op -> is_riscv_op
val is_riscv_op_functor : riscv_op -> is_riscv_op -> is_riscv_op
type box_riscv_op_ADD =
  1. | Box_riscv_op_ADD
type box_riscv_op_LOAD = {
  1. coq_Box_riscv_op_LOAD_0 : Wsize.signedness;
  2. coq_Box_riscv_op_LOAD_1 : Wsize.wsize;
}
val coq_Box_riscv_op_LOAD_0 : box_riscv_op_LOAD -> Wsize.signedness
val coq_Box_riscv_op_LOAD_1 : box_riscv_op_LOAD -> Wsize.wsize
type box_riscv_op_STORE = Wsize.wsize
val coq_Box_riscv_op_STORE_0 : box_riscv_op_STORE -> Wsize.wsize
type riscv_op_fields_t = __
val riscv_op_fields : riscv_op -> riscv_op_fields_t
val riscv_op_construct : BinNums.positive -> riscv_op_fields_t -> riscv_op option
val riscv_op_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 -> (Wsize.signedness -> Wsize.is_signedness -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> riscv_op -> is_riscv_op -> 'a1
val riscv_op_eqb_fields : (riscv_op -> riscv_op -> bool) -> BinNums.positive -> riscv_op_fields_t -> riscv_op_fields_t -> bool
val riscv_op_eqb : riscv_op -> riscv_op -> bool
val riscv_op_eqb_OK : riscv_op -> riscv_op -> Bool.reflect
val riscv_op_eqb_OK_sumbool : riscv_op -> riscv_op -> bool
val eqTC_riscv_op : riscv_op Utils0.eqTypeC
val riscv_op_eqType : Eqtype.Equality.coq_type
val prim_ADD : string * riscv_op Sopn.prim_constructor
val prim_ADDI : string * riscv_op Sopn.prim_constructor
val prim_SUB : string * riscv_op Sopn.prim_constructor
val prim_SLT : string * riscv_op Sopn.prim_constructor
val prim_SLTI : string * riscv_op Sopn.prim_constructor
val prim_SLTU : string * riscv_op Sopn.prim_constructor
val prim_SLTIU : string * riscv_op Sopn.prim_constructor
val prim_AND : string * riscv_op Sopn.prim_constructor
val prim_ANDI : string * riscv_op Sopn.prim_constructor
val prim_OR : string * riscv_op Sopn.prim_constructor
val prim_ORI : string * riscv_op Sopn.prim_constructor
val prim_XOR : string * riscv_op Sopn.prim_constructor
val prim_XORI : string * riscv_op Sopn.prim_constructor
val prim_SLL : string * riscv_op Sopn.prim_constructor
val prim_SLLI : string * riscv_op Sopn.prim_constructor
val prim_SRL : string * riscv_op Sopn.prim_constructor
val prim_SRLI : string * riscv_op Sopn.prim_constructor
val prim_SRA : string * riscv_op Sopn.prim_constructor
val prim_SRAI : string * riscv_op Sopn.prim_constructor
val riscv_MV_semi : Sem_type.sem_tuple -> Sem_type.sem_tuple
val prim_MV : string * riscv_op Sopn.prim_constructor
val riscv_LA_semi : Sem_type.sem_tuple -> Sem_type.sem_tuple
val prim_LA : string * riscv_op Sopn.prim_constructor
val riscv_LI_semi : Sem_type.sem_tuple -> Sem_type.sem_tuple
val prim_LI : string * riscv_op Sopn.prim_constructor
val riscv_NOT_semi : Sem_type.sem_tuple -> Sem_type.sem_tuple
val prim_NOT : string * riscv_op Sopn.prim_constructor
val riscv_NEG_semi : Sem_type.sem_tuple -> Sem_type.sem_tuple
val prim_NEG : string * riscv_op Sopn.prim_constructor
val string_of_sign : Wsize.signedness -> string
val string_of_size : Wsize.wsize -> string
val pp_sign_sz : string -> Wsize.signedness -> Wsize.wsize -> unit -> string
val prim_LOAD : string * riscv_op Sopn.prim_constructor
val prim_STORE : string * riscv_op Sopn.prim_constructor
val prim_MUL : string * riscv_op Sopn.prim_constructor
val prim_MULH : string * riscv_op Sopn.prim_constructor
val prim_MULHU : string * riscv_op Sopn.prim_constructor
val prim_MULHSU : string * riscv_op Sopn.prim_constructor
val prim_DIV : string * riscv_op Sopn.prim_constructor
val prim_DIVU : string * riscv_op Sopn.prim_constructor
val prim_REM : string * riscv_op Sopn.prim_constructor
val prim_REMU : string * riscv_op Sopn.prim_constructor
val riscv_prim_string : (string * riscv_op Sopn.prim_constructor) list