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
    
    Scanner
    
    Loc
    
    Typ
    
    TypMap
  - Bitfield
  - Callgraph
    
    G
    
    Node
    
    NodeMap
    
    NodeSet
  - Chunk_ast
  - Constant_fold
    
    StringMap
  - Constant_propagation
  - Constant_propagation_mutrec
  - Constraint
  - Effects
    
    EffectSet
  - Elf_loader
  - Error_format
  - Format_sail
    
    CONFIG
    
    Make
    
    Config
  - Frontend
    
    FILE_HANDLER
  - Graph
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Infix_parser
    
    Incremental
    
    MenhirInterpreter
  - Initial_check
  - Interactive
    
    State
  - Interpreter
    
    Printer
  - Jib
  - Jib_compile
    
    CONFIG
    
    IdGraph
    
    Make
    
    C
  - Jib_optimize
  - Jib_ssa
    
    NameGraph
  - Jib_util
    
    CTListSet
    
    CTMap
    
    CTSet
    
    Name
    
    NameCTMap
    
    NameCTSet
    
    NameMap
    
    NameSet
  - Jib_visitor
    
    common_visitor
    
    empty_jib_visitor
    
    jib_visitor
  - Lexer
    
    M
  - Libsail_sites
    
    Sites
  - Mappings
  - Monad_params
  - Monomorphise
  - Nl_flow
  - Outcome_rewrites
  - Parse_ast
    
    Attribute_data
  - Parser
  - Parser_combinators
  - Pattern_completeness
    
    Config
    
    Make
    
    C
  - Preprocess
  - Pretty_print_common
  - Pretty_print_sail
    
    Default_print_config
    
    Document
    
    PRINT_CONFIG
    
    Printer
    
    Config
  - Profile
  - Project
    
    ModId
    
    ModSet
  - Project_lexer
    
    M
  - Project_parser
  - Property
    
    Event
  - Reporting
    
    Position
  - Rewriter
  - Rewrites
  - Sail2_instr_kinds
  - Sail2_operators
  - Sail2_operators_bitlists
  - Sail2_prompt
  - Sail2_prompt_monad
  - Sail2_values
  - Sail_file
    
    In_channel
  - Sail_lib
    
    BitType
    
    Mem
  - Scattered
  - Smt_exp
    
    COUNTEREXAMPLE_CONFIG
    
    Counterexample
    
    Config
  - 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
    
    Option_monad
    
    State_monad
    
    S
  - Value
    
    StringMap
  - Value2
  - Visitor

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Big_int = Nat_big_num

val opt_tc_debug : int Stdlib.ref

val depth : int Stdlib.ref

val indent : int -> string

val typ_debug : ?level:int -> string Stdlib.Lazy.t -> unit

val typ_print : string Stdlib.Lazy.t -> unit

val adding : string

type constraint_reason = (Ast.l * string) option

type type_variables = {

vars : (Ast.l * Ast.kind_aux) Ast_util.KBindings.t;
shadows : int Ast_util.KBindings.t;

}

type type_error =

| Err_no_overloading of Ast.id * (Ast.id * Parse_ast.l * type_error) list
| Err_unresolved_quants of Ast.id * Ast.quant_item list * (Ast_util.mut * Ast.typ) Ast_util.Bindings.t * type_variables * Ast.n_constraint list
| Err_failed_constraint of Ast.n_constraint * (Ast_util.mut * Ast.typ) Ast_util.Bindings.t * type_variables * Ast.n_constraint list
| Err_subtype of Ast.typ * Ast.typ * Ast.n_constraint option * (constraint_reason * Ast.n_constraint) list * type_variables
| Err_no_num_ident of Ast.id
| Err_other of string
| Err_inner of type_error * Parse_ast.l * string * type_error
| Err_not_in_scope of string option * Parse_ast.l option * string Project.spanned option * string Project.spanned option * bool
| Err_instantiation_info of int * type_error
| Err_function_arg of Parse_ast.l * Ast.typ * type_error
| Err_no_function_type of {
1. id : Ast.id;
2. functions : (Ast.typquant * Ast.typ) Ast_util.Bindings.t;
}
| Err_unbound_id of {
1. id : Ast.id;
2. locals : (Ast_util.mut * Ast.typ) Ast_util.Bindings.t;
3. have_function : bool;
}
| Err_hint of string
| Err_with_hint of string * type_error

val err_because : (type_error * Parse_ast.l * type_error) -> type_error

exception Type_error of Ast.l * type_error

val typ_error : Ast.l -> string -> 'a

val typ_raise : Ast.l -> type_error -> 'a

val string_of_bind : (Ast.typquant * Ast.typ) -> string

val unloc_id : Ast.id -> Ast.id

val unloc_kid : Ast.kid -> Ast.kid

val unloc_nexp_aux : Ast.nexp_aux -> Ast.nexp_aux

val unloc_nexp : Ast.nexp -> Ast.nexp

val unloc_n_constraint_aux : Ast.n_constraint_aux -> Ast.n_constraint_aux

val unloc_n_constraint : Ast.n_constraint -> Ast.n_constraint

val unloc_typ_arg : Ast.typ_arg -> Ast.typ_arg

val unloc_typ_arg_aux : Ast.typ_arg_aux -> Ast.typ_arg_aux

val unloc_typ_aux : Ast.typ_aux -> Ast.typ_aux

val unloc_typ : Ast.typ -> Ast.typ

val unloc_typq : Ast.typquant -> Ast.typquant

val unloc_typq_aux : Ast.typquant_aux -> Ast.typquant_aux

val unloc_quant_item : Ast.quant_item -> Ast.quant_item

val unloc_qi_aux : Ast.quant_item_aux -> Ast.quant_item_aux

val unloc_kinded_id : Ast.kinded_id -> Ast.kinded_id

val unloc_kinded_id_aux : Ast.kinded_id_aux -> Ast.kinded_id_aux

val unloc_kind : Ast.kind -> Ast.kind

val typ_nexps : Ast.typ -> Ast.nexp list

val typ_arg_nexps : Ast.typ_arg -> Ast.nexp list

val constraint_nexps : Ast.n_constraint -> Ast.nexp list

val nexp_power_variables : Ast.nexp -> Ast_util.KidSet.t

val constraint_power_variables : Ast.n_constraint -> Ast_util.KidSet.t

val ex_counter : int Stdlib.ref

val fresh_existential : Ast.l -> Ast.kind_aux -> Ast.kinded_id

val named_existential : Ast.l -> Ast.kind_aux -> string option -> Ast.kinded_id

val destruct_exist_plain : 
  ?name:string option ->
  Ast.typ ->
  (Ast.kinded_id list * Ast.n_constraint * Ast.typ) option

val destruct_numeric : 
  ?name:string option ->
  Ast.typ ->
  (Ast.kid list * Ast.n_constraint * Ast.nexp) option

Destructure and canonicalise a numeric type into a list of type variables, a constraint on those type variables, and an N-expression that represents that numeric type in the environment. For example:

'n, 'n <= 10. atom('n) => 'n, 'n <= 10, 'n
int => 'n, true, 'n (where 'n is fresh)
atom('n) => , true, 'n *

val destruct_boolean : 
  ?name:'a option ->
  Ast.typ ->
  (Ast.kid * Ast.n_constraint) option

val destruct_exist : 
  ?name:string option ->
  Ast.typ ->
  (Ast.kinded_id list * Ast.n_constraint * Ast.typ) option