package libsail

You can search for identifiers within the package.

in-package search v0.2.0

package libsail

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
  - Constant_fold
    
    StringMap
  - Constant_propagation
  - Constant_propagation_mutrec
  - Constraint
  - Effects
    
    EffectSet
  - Elf_loader
  - Error_format
  - Frontend
  - Graph
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Initial_check
  - Interactive
  - Interpreter
  - Jib
  - Jib_compile
    
    Config
    
    Make
    
    C
  - Jib_optimize
  - Jib_util
    
    CT
    
    CTList
    
    CTListSet
    
    CTMap
    
    CTSet
    
    Name
    
    NameCT
    
    NameCTMap
    
    NameCTSet
    
    NameMap
    
    NameSet
    
    UBindings
    
    UId
  - Lexer
    
    M
  - Libsail_sites
    
    Sites
  - Monomorphise
  - Nl_flow
  - Optimize
  - 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
  - Spec_analysis
  - Specialize
  - Splice
  - State
  - Target
  - Type_check
    
    Env
  - Type_error
  - Util
    
    Duplicate
  - Value
    
    StringMap
  - Value2

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Big_int = Nat_big_num

val opt_type_grouped_regstate : bool Stdlib.ref

val is_defined : 'a Ast.def list -> string -> bool

val has_default_order : 'a Ast.def list -> bool

val find_registers : Type_check.tannot Ast.def list -> (Ast.typ * Ast.id) list

val generate_register_id_enum : ('a * Ast.id) list -> string list

val id_of_regtyp : Ast_util.IdSet.t -> bool -> Ast.typ -> Ast.id

val regstate_field : Ast.typ -> Ast.id

val generate_regstate : (Ast.typ * Ast.id) list -> unit Ast.def list

val generate_initial_regstate : 
  Type_check.tannot Ast.def list ->
  unit Ast.def list list

val regval_constr_id : bool -> Ast.typ -> Ast.id

val register_base_types : bool -> Ast.typ list -> Ast.typ Ast_util.Bindings.t

val generate_regval_typ : Ast.typ Ast_util.Bindings.t -> unit Ast.def list list

val regval_class_typs_lem : (string * string) list

val regval_instance_lem : PPrint.document

val add_regval_conv : 
  Ast.id ->
  Ast.typ ->
  unit Ast.def list ->
  unit Ast.def list

val regval_convs : bool -> (string -> string) -> Ast.typ -> string * string

val regval_convs_lem : bool -> Ast.typ -> string * string

val regval_convs_isa : bool -> Ast.typ -> string * string

val register_refs_lem : 
  bool ->
  (Ast.typ -> PPrint.document) ->
  (Ast.typ * Ast.id) list ->
  PPrint.document

val generate_isa_lemmas : 
  bool ->
  Type_check.tannot Ast.def list ->
  PPrint.document

val regval_convs_coq : Ast.typ -> string * string

val register_refs_coq : 
  ('a -> PPrint.document) ->
  (Ast.typ * 'a) list ->
  PPrint.document

val generate_regstate_defs : 
  bool ->
  Type_check.tannot Ast.def list ->
  unit Ast.def list

val add_regstate_defs : 
  bool ->
  Type_check.Env.t ->
  Type_check.tannot Ast_defs.ast ->
  Type_check.Env.t * Type_check.tannot Ast_defs.ast