package libsail

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val opt_smt_linearize : bool Stdlib.ref

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

val opt_string_literal_type : bool Stdlib.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 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 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.

OCaml

Innovation. Community. Security.