package libsail

You can search for identifiers within the package.

in-package search v0.2.0

libsail
- Libsail
  - Anf
  - Ast
  - Ast_defs
  - Ast_util
    
    Bindings
    
    Id
    
    IdSet
    
    KBindings
    
    KOpt
    
    KOptMap
    
    KOptSet
    
    Kid
    
    KidSet
    
    Kind
    
    NC
    
    NCMap
    
    Nexp
    
    NexpMap
    
    NexpSet
    
    Typ
    
    TypMap
  - Bitfield
  - Callgraph
    
    G
    
    Node
  - Chunk_ast
  - Constant_fold
    
    StringMap
  - Constant_propagation
  - Constant_propagation_mutrec
  - Constraint
  - Effects
    
    EffectSet
  - Elf_loader
  - Error_format
  - Format_sail
    
    CONFIG
    
    Make
    
    Config
  - Frontend
  - Graph
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Infix_parser
    
    Incremental
    
    MenhirInterpreter
  - Initial_check
  - Interactive
  - Interpreter
  - Jib
  - Jib_compile
    
    CONFIG
    
    IdGraph
    
    Make
    
    C
  - Jib_optimize
  - Jib_util
    
    CTListSet
    
    CTMap
    
    CTSet
    
    Name
    
    NameCTMap
    
    NameCTSet
    
    NameMap
    
    NameSet
  - Jib_visitor
    
    empty_jib_visitor
    
    jib_visitor
  - Lexer
    
    M
  - Libsail_sites
    
    Sites
  - Mappings
  - Monad_params
  - Monomorphise
  - Nl_flow
  - Outcome_rewrites
  - Parse_ast
  - Parser
  - Parser_combinators
  - Pattern_completeness
    
    Config
    
    Make
    
    C
  - Preprocess
  - Pretty_print_common
  - Pretty_print_sail
  - Profile
  - Property
    
    Event
  - Reporting
  - Rewriter
  - Rewrites
  - Sail2_instr_kinds
  - Sail2_operators
  - Sail2_operators_bitlists
  - Sail2_prompt
  - Sail2_prompt_monad
  - Sail2_values
  - Sail_lib
    
    BitType
    
    Mem
  - Scattered
    
    PC
    
    PC_config
  - Smt_exp
  - Smt_gen
    
    CONFIG
    
    Make
    
    Config
    
    Primop_gen
    
    PRIMOP_GEN
  - Spec_analysis
  - Specialize
  - Splice
  - State
  - Target
  - Type_check
    
    Env
  - Type_env
  - Type_error
  - Type_internal
  - Util
    
    Duplicate
  - Value
    
    StringMap
  - Value2
  - Visitor

Legend:
Library
Module
Module type
Parameter
Class
Class type

type 'a enumerationType_class = {

toNat_method : 'a -> int;

}

val instance_Basic_classes_Ord_var_dict : 
  'b ->
  'a Lem_pervasives_extra.ord_class

type read_kind =

| Read_plain
| Read_reserve
| Read_acquire
| Read_exclusive
| Read_exclusive_acquire
| Read_stream
| Read_RISCV_acquire
| Read_RISCV_strong_acquire
| Read_RISCV_reserved
| Read_RISCV_reserved_acquire
| Read_RISCV_reserved_strong_acquire
| Read_X86_locked
| Read_ifetch

val instance_Show_Show_Sail2_instr_kinds_read_kind_dict : 
  read_kind Lem_pervasives_extra.show_class

type write_kind =

| Write_plain
| Write_conditional
| Write_release
| Write_exclusive
| Write_exclusive_release
| Write_RISCV_release
| Write_RISCV_strong_release
| Write_RISCV_conditional
| Write_RISCV_conditional_release
| Write_RISCV_conditional_strong_release
| Write_X86_locked

val instance_Show_Show_Sail2_instr_kinds_write_kind_dict : 
  write_kind Lem_pervasives_extra.show_class

type a64_barrier_domain =

| A64_FullShare
| A64_InnerShare
| A64_OuterShare
| A64_NonShare

type a64_barrier_type =

| A64_barrier_all
| A64_barrier_LD
| A64_barrier_ST

type barrier_kind =

| Barrier_Sync of unit
| Barrier_LwSync of unit
| Barrier_Eieio of unit
| Barrier_Isync of unit
| Barrier_DMB of a64_barrier_domain * a64_barrier_type
| Barrier_DSB of a64_barrier_domain * a64_barrier_type
| Barrier_ISB of unit
| Barrier_TM_COMMIT of unit
| Barrier_MIPS_SYNC of unit
| Barrier_RISCV_rw_rw of unit
| Barrier_RISCV_r_rw of unit
| Barrier_RISCV_r_r of unit
| Barrier_RISCV_rw_w of unit
| Barrier_RISCV_w_w of unit
| Barrier_RISCV_w_rw of unit
| Barrier_RISCV_rw_r of unit
| Barrier_RISCV_r_w of unit
| Barrier_RISCV_w_r of unit
| Barrier_RISCV_tso of unit
| Barrier_RISCV_i of unit
| 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 =

| Transaction_start
| Transaction_commit
| Transaction_abort

val instance_Show_Show_Sail2_instr_kinds_trans_kind_dict : 
  trans_kind Lem_pervasives_extra.show_class

type cache_op_kind =

| Cache_op_D_IVAC
| Cache_op_D_ISW
| Cache_op_D_CSW
| Cache_op_D_CISW
| Cache_op_D_ZVA
| Cache_op_D_CVAC
| Cache_op_D_CVAU
| Cache_op_D_CIVAC
| Cache_op_I_IALLUIS
| Cache_op_I_IALLU
| 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 =

| IK_barrier of barrier_kind
| IK_mem_read of read_kind
| IK_mem_write of write_kind
| IK_mem_rmw of read_kind * write_kind
| IK_branch of unit
| IK_trans of trans_kind
| IK_simple of unit
| 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