package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a enumerationType_class = {
  1. toNat_method : 'a -> int;
}
val instance_Basic_classes_Ord_var_dict : 'b -> 'a Lem_pervasives_extra.ord_class
type read_kind =
  1. | Read_plain
  2. | Read_reserve
  3. | Read_acquire
  4. | Read_exclusive
  5. | Read_exclusive_acquire
  6. | Read_stream
  7. | Read_RISCV_acquire
  8. | Read_RISCV_strong_acquire
  9. | Read_RISCV_reserved
  10. | Read_RISCV_reserved_acquire
  11. | Read_RISCV_reserved_strong_acquire
  12. | Read_X86_locked
  13. | Read_ifetch
val instance_Show_Show_Sail2_instr_kinds_read_kind_dict : read_kind Lem_pervasives_extra.show_class
type write_kind =
  1. | Write_plain
  2. | Write_conditional
  3. | Write_release
  4. | Write_exclusive
  5. | Write_exclusive_release
  6. | Write_RISCV_release
  7. | Write_RISCV_strong_release
  8. | Write_RISCV_conditional
  9. | Write_RISCV_conditional_release
  10. | Write_RISCV_conditional_strong_release
  11. | Write_X86_locked
val instance_Show_Show_Sail2_instr_kinds_write_kind_dict : write_kind Lem_pervasives_extra.show_class
type a64_barrier_domain =
  1. | A64_FullShare
  2. | A64_InnerShare
  3. | A64_OuterShare
  4. | A64_NonShare
type a64_barrier_type =
  1. | A64_barrier_all
  2. | A64_barrier_LD
  3. | A64_barrier_ST
type barrier_kind =
  1. | Barrier_Sync of unit
  2. | Barrier_LwSync of unit
  3. | Barrier_Eieio of unit
  4. | Barrier_Isync of unit
  5. | Barrier_DMB of a64_barrier_domain * a64_barrier_type
  6. | Barrier_DSB of a64_barrier_domain * a64_barrier_type
  7. | Barrier_ISB of unit
  8. | Barrier_TM_COMMIT of unit
  9. | Barrier_MIPS_SYNC of unit
  10. | Barrier_RISCV_rw_rw of unit
  11. | Barrier_RISCV_r_rw of unit
  12. | Barrier_RISCV_r_r of unit
  13. | Barrier_RISCV_rw_w of unit
  14. | Barrier_RISCV_w_w of unit
  15. | Barrier_RISCV_w_rw of unit
  16. | Barrier_RISCV_rw_r of unit
  17. | Barrier_RISCV_r_w of unit
  18. | Barrier_RISCV_w_r of unit
  19. | Barrier_RISCV_tso of unit
  20. | Barrier_RISCV_i of unit
  21. | Barrier_x86_MFENCE of unit
val string_a64_barrier_domain : a64_barrier_domain -> string
val instance_Show_Show_Sail2_instr_kinds_a64_barrier_domain_dict : a64_barrier_domain Lem_pervasives_extra.show_class
val string_a64_barrier_type : a64_barrier_type -> string
val instance_Show_Show_Sail2_instr_kinds_a64_barrier_type_dict : a64_barrier_type Lem_pervasives_extra.show_class
val instance_Show_Show_Sail2_instr_kinds_barrier_kind_dict : barrier_kind Lem_pervasives_extra.show_class
type trans_kind =
  1. | Transaction_start
  2. | Transaction_commit
  3. | Transaction_abort
val instance_Show_Show_Sail2_instr_kinds_trans_kind_dict : trans_kind Lem_pervasives_extra.show_class
type cache_op_kind =
  1. | Cache_op_D_IVAC
  2. | Cache_op_D_ISW
  3. | Cache_op_D_CSW
  4. | Cache_op_D_CISW
  5. | Cache_op_D_ZVA
  6. | Cache_op_D_CVAC
  7. | Cache_op_D_CVAU
  8. | Cache_op_D_CIVAC
  9. | Cache_op_I_IALLUIS
  10. | Cache_op_I_IALLU
  11. | Cache_op_I_IVAU
val instance_Show_Show_Sail2_instr_kinds_cache_op_kind_dict : cache_op_kind Lem_pervasives_extra.show_class
type instruction_kind =
  1. | IK_barrier of barrier_kind
  2. | IK_mem_read of read_kind
  3. | IK_mem_write of write_kind
  4. | IK_mem_rmw of read_kind * write_kind
  5. | IK_branch of unit
  6. | IK_trans of trans_kind
  7. | IK_simple of unit
  8. | IK_cache_op of cache_op_kind
val instance_Show_Show_Sail2_instr_kinds_instruction_kind_dict : instruction_kind Lem_pervasives_extra.show_class
val read_is_exclusive : read_kind -> bool
val instance_Sail2_instr_kinds_EnumerationType_Sail2_instr_kinds_read_kind_dict : read_kind enumerationType_class
val instance_Sail2_instr_kinds_EnumerationType_Sail2_instr_kinds_write_kind_dict : write_kind enumerationType_class
val instance_Sail2_instr_kinds_EnumerationType_Sail2_instr_kinds_a64_barrier_domain_dict : a64_barrier_domain enumerationType_class
val instance_Sail2_instr_kinds_EnumerationType_Sail2_instr_kinds_a64_barrier_type_dict : a64_barrier_type enumerationType_class
val instance_Sail2_instr_kinds_EnumerationType_Sail2_instr_kinds_barrier_kind_dict : barrier_kind enumerationType_class