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
    
    S
    
    IntIntSet
    
    IntMap
    
    IntSet
    
    Option_monad
    
    State_monad
    
    S
    
    StringMap
  - 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.

val opt_string_literal_type : bool ref

Val use a separate string literal type

type global_env

type env

type t = env

val set_modules : Project.project_structure -> t -> t

Set the modules in the environment. Note that calling this twice on an environment with different arguments will invalidate all module identifiers!

val get_module_id_opt : t -> string -> Project.mod_id option

val get_module_id : at:Ast.l -> t -> string -> Project.mod_id

val start_module : at:Ast.l -> Project.mod_id -> t -> t

Start typechecking within a module context. The module id must be a valid module created via the set_modules call, otherwise we will fail with an internal error.

val end_module : t -> t

End the current module context, returning us to type-checking in the global scope.

val open_all_modules : t -> t

This effectively disables all module related access control

val with_private_visibility : 
  ?restore:(t -> t) ->
  at:Ast.l ->
  t ->
  t * (t -> t)

val with_private_visibility_if : 
  ?restore:(t -> t) ->
  at:Ast.l ->
  bool ->
  t ->
  t * (t -> t)

val get_current_visibility : t -> Ast.visibility

type module_state

val with_global_scope : t -> t * module_state

This is the same as end_module and open_all_modules, except it returns the module state so it can be restored with restore_scope.

val restore_scope : module_state -> t -> t

val fresh_kid : ?kid:Ast.kid -> env -> Ast.kid

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 : 
  ?in_module:Project.mod_id ->
  ?ignore_duplicate:bool ->
  Ast.id ->
  (Ast.typquant * Ast.typ) ->
  t ->
  t

val update_val_spec : 
  ?in_module:Project.mod_id ->
  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_opt : Ast.id -> t -> ((Ast.typquant * Ast.typ) * Ast.l) option

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_user_undefined : Ast.id -> t -> bool

For a user-defined type identifier we can control whether it is allowed to be created with the undefined literal in Sail

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

val add_abstract_typ : Ast.id -> Ast.kind -> t -> t

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

val get_abstract_typs : t -> Ast.kind Ast_util.Bindings.t

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 : 
  ?in_module:Project.mod_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 : 
  ?global:bool ->
  ?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 is_overload : Ast.id -> t -> bool

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

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

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

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

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

val get_filtered_overloads : at:Ast.l -> Ast.id -> t -> Ast.id * Ast.id list

val add_filtered_overload : Ast.id -> Ast.id list -> t -> Ast.id * t

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_opt : Ast.id -> t -> Ast.id list option

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

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

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

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

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

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 : at:Ast.l -> t -> Ast.typ -> unit

val wf_constraint : at:Ast.l -> 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