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
  - 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
    
    S
    
    IntIntSet
    
    IntSet
  - Value
    
    StringMap
  - Value2
  - Visitor

Legend:
Library
Module
Module type
Parameter
Class
Class type

val opt_mono_rewrites : bool ref

val opt_mono_complex_nexps : bool ref

val opt_mono_split : ((string * int) * string) list ref

val opt_dmono_analysis : int ref

val opt_auto_mono : bool ref

val opt_dall_split_errors : bool ref

val opt_dmono_continue : bool ref

val opt_coq_warn_nonexhaustive : bool ref

Warn about matches where we add a default case for Coq because they're not exhaustive

val opt_ddump_rewrite_ast : (string * int) option ref

Output each rewrite step (as produced by the rewrite function) to a file for debugging

val fresh_id : string -> Ast.l -> Ast.id

Generate a fresh id with the given prefix

val move_loop_measures : 'a Ast_defs.ast -> 'a Ast_defs.ast

Move loop termination measures into loop AST nodes

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

Re-write undefined to functions created by -undefined_gen flag

type rewriter =

| Base_rewriter of Effects.side_effect_info -> Type_check.Env.t -> Type_check.tannot Ast_defs.ast -> Type_check.tannot Ast_defs.ast * Effects.side_effect_info * Type_check.Env.t
| Bool_rewriter of bool -> rewriter
| String_rewriter of string -> rewriter
| Literal_rewriter of (Ast.lit -> bool) -> rewriter

val describe_rewriter : rewriter -> string list

val all_rewriters : (string * rewriter) list

type rewrite_sequence =
  (string
   * (Effects.side_effect_info ->
   Type_check.Env.t ->
   Type_check.tannot Ast_defs.ast ->
   Type_check.tannot Ast_defs.ast * Effects.side_effect_info * Type_check.Env.t))
    list

val rewrite_lit_ocaml : Ast.lit -> bool

val rewrite_lit_lem : Ast.lit -> bool

type rewriter_arg =

| If_mono_arg
| If_mwords_arg
| If_flag of bool ref
| Bool_arg of bool
| Flag_arg of bool ref
| String_arg of string
| Literal_arg of string

val instantiate_rewrites : 
  (string * rewriter_arg list) list ->
  rewrite_sequence

Get the list of instantiated rewrites for a list of rewrites

val rewrite : 
  Effects.side_effect_info ->
  Type_check.Env.t ->
  rewrite_sequence ->
  Type_check.tannot Ast_defs.ast ->
  Type_check.tannot Ast_defs.ast * Effects.side_effect_info * Type_check.Env.t

Apply a sequence of rewrites to an AST

val rewrites_interpreter : (string * rewriter_arg list) list

val simple_typ : Ast.typ -> Ast.typ