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_smt_linearize : bool ref

Linearize cases involving power where we would otherwise require the SMT solver to use non-linear arithmetic.

type global_env

type env

type t = env

val freshen_bind : t -> (Ast.typquant * Ast.typ) -> Ast.typquant * Ast.typ

val get_default_order : t -> Ast.order

val get_default_order_opt : t -> Ast.order option

val set_default_order : Ast.order -> t -> t

val add_val_spec : 
  ?ignore_duplicate:bool ->
  Ast.id ->
  (Ast.typquant * Ast.typ) ->
  t ->
  t

val update_val_spec : Ast.id -> (Ast.typquant * Ast.typ) -> t -> t

val define_val_spec : Ast.id -> t -> t

val get_defined_val_specs : t -> Ast_util.IdSet.t

val get_val_spec : Ast.id -> t -> Ast.typquant * Ast.typ

val get_val_specs : t -> (Ast.typquant * Ast.typ) Ast_util.Bindings.t

val get_val_spec_orig : Ast.id -> t -> Ast.typquant * Ast.typ

val add_outcome : 
  Ast.id ->
  (Ast.typquant * Ast.typ * Ast.kinded_id list * Ast.id list * t) ->
  t ->
  t

val get_outcome : 
  Ast.l ->
  Ast.id ->
  t ->
  Ast.typquant * Ast.typ * Ast.kinded_id list * Ast.id list * t

val get_outcome_instantiation : t -> (Ast.l * Ast.typ) Ast_util.KBindings.t

val add_outcome_variable : Ast.l -> Ast.kid -> Ast.typ -> t -> t

val set_outcome_typschm : 
  outcome_loc:Ast.l ->
  (Ast.typquant * Ast.typ) ->
  t ->
  t

val get_outcome_typschm_opt : t -> (Ast.typquant * Ast.typ) option

val is_variant : Ast.id -> t -> bool

val add_variant : Ast.id -> (Ast.typquant * Ast.type_union list) -> t -> t

val add_scattered_variant : Ast.id -> Ast.typquant -> t -> t

val add_variant_clause : Ast.id -> Ast.type_union -> t -> t

val get_variant : Ast.id -> t -> Ast.typquant * Ast.type_union list

val get_variants : 
  t ->
  (Ast.typquant * Ast.type_union list) Ast_util.Bindings.t

val get_scattered_variant_env : Ast.id -> t -> t

val set_scattered_variant_env : variant_env:t -> Ast.id -> t -> t

val union_constructor_info : 
  Ast.id ->
  t ->
  (int * int * Ast.id * Ast.type_union) option

val is_union_constructor : Ast.id -> t -> bool

val is_singleton_union_constructor : Ast.id -> t -> bool

val add_union_id : Ast.id -> (Ast.typquant * Ast.typ) -> t -> t

val get_union_id : Ast.id -> t -> Ast.typquant * Ast.typ

val is_mapping : Ast.id -> t -> bool

val add_record : Ast.id -> Ast.typquant -> (Ast.typ * Ast.id) list -> t -> t

val is_record : Ast.id -> t -> bool

val get_record : Ast.id -> t -> Ast.typquant * (Ast.typ * Ast.id) list

val get_records : 
  t ->
  (Ast.typquant * (Ast.typ * Ast.id) list) Ast_util.Bindings.t

val get_accessor_fn : Ast.id -> Ast.id -> t -> Ast.typquant * Ast.typ

val get_accessor : Ast.id -> Ast.id -> t -> Ast.typquant * Ast.typ * Ast.typ

val add_local : Ast.id -> (Ast_util.mut * Ast.typ) -> t -> t

val get_locals : t -> (Ast_util.mut * Ast.typ) Ast_util.Bindings.t

val is_mutable : Ast.id -> t -> bool

val add_toplevel_lets : Ast_util.IdSet.t -> t -> t

val get_toplevel_lets : t -> Ast_util.IdSet.t

val is_register : Ast.id -> t -> bool

val get_register : Ast.id -> t -> Ast.typ

val get_registers : t -> Ast.typ Ast_util.Bindings.t

val add_register : Ast.id -> Ast.typ -> t -> t

val get_constraints : t -> Ast.n_constraint list

val get_constraint_reasons : 
  t ->
  ((Ast.l * string) option * Ast.n_constraint) list

val add_constraint : ?reason:(Ast.l * string) -> Ast.n_constraint -> t -> t

val add_typquant : Ast.l -> Ast.typquant -> t -> t

val get_typ_var : Ast.kid -> t -> Ast.kind_aux

val get_typ_var_loc_opt : Ast.kid -> t -> Ast.l option

val get_typ_vars : t -> Ast.kind_aux Ast_util.KBindings.t

val get_typ_var_locs : t -> Ast.l Ast_util.KBindings.t

type type_variables = Type_internal.type_variables

val get_typ_vars_info : t -> type_variables

val lookup_typ_var : Ast.kid -> type_variables -> (Ast.l * Ast.kind_aux) option

val is_shadowed : Ast.kid -> type_variables -> bool

val shadows : Ast.kid -> t -> int

val add_typ_var_shadow : Ast.l -> Ast.kinded_id -> t -> t * Ast.kid option

val add_typ_var : Ast.l -> Ast.kinded_id -> t -> t

val get_ret_typ : t -> Ast.typ option

val add_ret_typ : Ast.typ -> t -> t

val add_typ_synonym : Ast.id -> Ast.typquant -> Ast.typ_arg -> t -> t

val get_typ_synonyms : t -> (Ast.typquant * Ast.typ_arg) Ast_util.Bindings.t

val bound_typ_id : t -> Ast.id -> bool

val add_overloads : Ast.l -> Ast.id -> Ast.id list -> t -> t

val get_overloads : Ast.id -> t -> Ast.id list

val is_extern : Ast.id -> t -> string -> bool

val add_extern : Ast.id -> Ast.extern -> t -> t

val get_extern : Ast.id -> t -> string -> string

val add_enum : Ast.id -> Ast.id list -> t -> t

val add_scattered_enum : Ast.id -> t -> t

val add_enum_clause : Ast.id -> Ast.id -> t -> t

val get_enum : Ast.id -> t -> Ast.id list

val get_enums : t -> Ast_util.IdSet.t Ast_util.Bindings.t

val allow_polymorphic_undefineds : t -> t

val polymorphic_undefineds : t -> bool

val lookup_id : Ast.id -> t -> Ast.typ Ast_util.lvar

val expand_synonyms : t -> Ast.typ -> Ast.typ

val expand_nexp_synonyms : t -> Ast.nexp -> Ast.nexp

val expand_constraint_synonyms : t -> Ast.n_constraint -> Ast.n_constraint

val base_typ_of : t -> Ast.typ -> Ast.typ

val allow_unknowns : t -> bool

val set_allow_unknowns : bool -> t -> t

val is_bitfield : Ast.id -> t -> bool

val add_bitfield : 
  Ast.id ->
  Ast.typ ->
  Ast.index_range Ast_util.Bindings.t ->
  t ->
  t

val get_bitfield : Ast.id -> t -> Ast.typ * Ast.index_range Ast_util.Bindings.t

val no_bindings : t -> t

val is_toplevel : t -> Ast.l option

val wf_typ : t -> Ast.typ -> unit

val wf_constraint : ?exs:Ast_util.KidSet.t -> t -> Ast.n_constraint -> unit

val set_prover : (t -> Ast.n_constraint -> bool) option -> t -> t

Some of the code in the environment needs to use the smt solver, which is defined below. To break the circularity this would cause (as the prove code depends on the environment), we add a reference to the prover to the initial environment.

val empty : t

This should not be used outside the type checker, as initial_env sets up a correct initial environment.

val builtin_typs : Ast.typquant Ast_util.Bindings.t