package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Libsail.Type_envSource

Sourceval opt_smt_linearize : bool ref

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

Sourceval opt_string_literal_type : bool ref

Val use a separate string literal type

Sourceval opt_strict_exponentials : bool ref
Sourcetype global_env
Sourcetype env
Sourcetype t = env
Sourceval 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!

Sourceval get_module_id_opt : t -> string -> Project.mod_id option
Sourceval get_module_id : at:Ast.l -> t -> string -> Project.mod_id
Sourceval 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.

Sourceval end_module : t -> t

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

Sourceval open_all_modules : t -> t

This effectively disables all module related access control

Sourceval with_private_visibility : ?restore:(t -> t) -> at:Ast.l -> t -> t * (t -> t)
Sourceval with_private_visibility_if : ?restore:(t -> t) -> at:Ast.l -> bool -> t -> t * (t -> t)
Sourceval get_current_visibility : t -> Ast.visibility
Sourcetype module_state
Sourceval 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.

Sourceval restore_scope : module_state -> t -> t
Sourceval fresh_kid : ?kid:Ast.kid -> env -> Ast.kid
Sourceval freshen_bind : t -> (Ast.typquant * Ast.typ) -> Ast.typquant * Ast.typ
Sourceval get_default_order : t -> Ast.order
Sourceval get_default_order_opt : t -> Ast.order option
Sourceval set_default_order : Ast.order -> t -> t
Sourceval add_val_spec : ?in_module:Project.mod_id -> ?already_bound:bool -> ?ignore_duplicate:bool -> Ast.id -> (Ast.typquant * Ast.typ) -> t -> t

Add a function type (val spec) to the global typing environment.

If already_bound = true, we can add a val_spec for something that is already bound as a global identifier in the typing environment. This is used for union constructors.

For legacy reasons, function declarations can be duplicated. This will typically produce a warning. If ignore_duplicate is true, this warning is supressed.

Sourceval update_val_spec : ?in_module:Project.mod_id -> Ast.id -> (Ast.typquant * Ast.typ) -> t -> t
Sourceval define_val_spec : Ast.id -> t -> t
Sourceval get_defined_val_specs : t -> Ast_util.IdSet.t
Sourceval get_val_spec_opt : Ast.id -> t -> ((Ast.typquant * Ast.typ) * Ast.l) option
Sourceval get_val_spec : Ast.id -> t -> Ast.typquant * Ast.typ
Sourceval get_val_specs : t -> (Ast.typquant * Ast.typ) Ast_util.Bindings.t
Sourceval get_val_spec_orig : Ast.id -> t -> Ast.typquant * Ast.typ
Sourceval is_outcome : Ast.id -> t -> bool
Sourceval add_outcome : Ast.id -> (Ast.typquant * Ast.typ * Ast.typquant * Ast.id list * t) -> t -> t
Sourceval get_outcome : Ast.l -> Ast.id -> t -> Ast.typquant * Ast.typ * Ast.typquant * Ast.id list * t
Sourceval get_outcome_instantiation : t -> (Ast.l * Ast.typ_arg) Ast_util.KBindings.t
Sourceval add_outcome_variable : Ast.l -> Ast.kid -> Ast.typ_arg -> t -> t
Sourceval set_outcome_typschm : outcome_loc:Ast.l -> (Ast.typquant * Ast.typ) -> t -> t
Sourceval get_outcome_typschm_opt : t -> (Ast.typquant * Ast.typ) option
Sourceval 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

Sourceval allow_user_undefined : Ast.id -> t -> t
Sourceval add_abstract_typ : Ast.id -> Ast.kind -> t -> t
Sourceval is_abstract_typ : Ast.id -> t -> bool
Sourceval get_abstract_typs : t -> Ast.kind Ast_util.Bindings.t
Sourceval remove_abstract_typ : Ast.id -> t -> t
Sourceval is_variant : Ast.id -> t -> bool
Sourceval add_variant : ?is_newtype:bool -> Ast.id -> (Ast.typquant * Ast.type_union list) -> t -> t
Sourceval add_scattered_variant : Ast.id -> Ast.typquant -> t -> t
Sourceval add_variant_clause : Ast.id -> Ast.type_union -> t -> t
Sourceval get_variant : Ast.id -> t -> Ast.typquant * Ast.type_union list
Sourceval get_scattered_variant_env : Ast.id -> t -> t
Sourceval set_scattered_variant_env : variant_env:t -> Ast.id -> t -> t
Sourceval union_constructor_info : Ast.id -> t -> (int * int * Ast.id * Ast.type_union) option
Sourceval is_union_constructor : Ast.id -> t -> bool
Sourceval is_singleton_union_constructor : Ast.id -> t -> bool
Sourceval add_union_id : ?in_module:Project.mod_id -> Ast.id -> (Ast.typquant * Ast.typ) -> t -> t
Sourceval get_union_id : Ast.id -> t -> Ast.typquant * Ast.typ
Sourceval is_newtype : Ast.id -> t -> bool
Sourceval is_mapping : Ast.id -> t -> bool
Sourceval add_record : Ast.id -> Ast.typquant -> (Ast.typ * Ast.id) list -> t -> t
Sourceval is_record : Ast.id -> t -> bool
Sourceval get_record : Ast.id -> t -> Ast.typquant * (Ast.typ * Ast.id) list
Sourceval get_records : t -> (Ast.typquant * (Ast.typ * Ast.id) list) Ast_util.Bindings.t
Sourceval get_accessor_fn : Ast.id -> Ast.id -> t -> Ast.typquant * Ast.typ
Sourceval get_accessor : Ast.id -> Ast.id -> t -> Ast.typquant * Ast.typ * Ast.typ
Sourceval add_local : Ast.id -> (Ast_util.mut * Ast.typ) -> t -> t
Sourceval is_mutable : Ast.id -> t -> bool
Sourceval add_toplevel_lets : Ast_util.IdSet.t -> t -> t
Sourceval get_toplevel_lets : t -> Ast_util.IdSet.t
Sourceval is_register : Ast.id -> t -> bool
Sourceval get_register : Ast.id -> t -> Ast.typ
Sourceval get_registers : t -> Ast.typ Ast_util.Bindings.t
Sourceval add_register : Ast.id -> Ast.typ -> t -> t
Sourceval get_constraints : t -> Ast.n_constraint list
Sourceval get_global_constraints : t -> Ast.n_constraint list
Sourceval get_constraint_reasons : t -> ((Ast.l * string) option * Ast.n_constraint) list
Sourceval add_constraint : ?global:bool -> ?reason:(Ast.l * string) -> Ast.n_constraint -> t -> t
Sourceval add_typquant : ?from_outcome:bool -> Ast.l -> Ast.typquant -> t -> t
Sourceval is_outcome_typ_var : Ast.kid -> t -> bool
Sourceval get_typ_var : Ast.kid -> t -> Ast.kind_aux
Sourceval get_typ_var_opt : Ast.kid -> t -> (Ast.l * Ast.kind_aux) option
Sourceval get_typ_var_loc_opt : Ast.kid -> t -> Ast.l option
Sourceval get_typ_var_locs : t -> Ast.l Ast_util.KBindings.t
Sourceval get_typ_vars_info : t -> type_variables
Sourceval lookup_typ_var : Ast.kid -> type_variables -> (Ast.l * Ast.kind_aux) option
Sourceval is_shadowed : Ast.kid -> type_variables -> bool
Sourceval shadows : Ast.kid -> t -> int
Sourceval add_typ_var_shadow : ?from_outcome:bool -> Ast.l -> Ast.kinded_id -> t -> t * Ast.kid option
Sourceval add_typ_var : ?from_outcome:bool -> Ast.l -> Ast.kinded_id -> t -> t
Sourceval get_ret_typ : t -> Ast.typ option
Sourceval add_ret_typ : Ast.typ -> t -> t
Sourceval add_typ_synonym : Ast.id -> Ast.typquant -> Ast.typ_arg -> t -> t
Sourceval get_typ_synonyms : t -> (Ast.typquant * Ast.typ_arg) Ast_util.Bindings.t
Sourceval bound_typ_id : t -> Ast.id -> bool
Sourceval is_overload : Ast.id -> t -> bool
Sourceval get_overload_locs : Ast.id -> t -> Ast.l list
Sourceval add_overloads : Ast.l -> Ast.id -> Ast.id list -> t -> t
Sourceval get_overloads : Ast.id -> t -> Ast.id list
Sourceval get_overloads_recursive : Ast.id -> t -> Ast.id list
Sourceval is_filtered_overload : Ast.id -> t -> bool
Sourceval get_filtered_overloads : at:Ast.l -> Ast.id -> t -> Ast.id * Ast.id list
Sourceval add_filtered_overload : Ast.id -> Ast.id list -> t -> Ast.id * t
Sourceval is_extern : Ast.id -> t -> string -> bool
Sourceval add_extern : Ast.id -> Ast.extern -> t -> t
Sourceval get_extern : Ast.id -> t -> string -> string
Sourceval add_enum : Ast.id -> Ast.id list -> t -> t
Sourceval add_scattered_enum : Ast.id -> (Ast.l * string * Ast.attribute_data option) list -> t -> t
Sourceval add_enum_clause : Ast.id -> Ast.id -> t -> t
Sourceval get_enum_opt : Ast.id -> t -> Ast.id list option
Sourceval get_enum : Ast.id -> t -> Ast.id list
Sourceval is_enum : Ast.id -> t -> bool
Sourceval lookup_id : Ast.id -> t -> Ast.typ Ast_util.lvar
Sourceval add_scattered_id : Ast.id -> (Ast.l * string * Ast.attribute_data option) list -> t -> t
Sourceval is_scattered_id : Ast.id -> t -> bool
Sourceval is_scattered_open : Ast.id -> t -> bool
Sourceval end_scattered_id : at:Ast.l -> Ast.id -> t -> t
Sourceval expand_synonyms : t -> Ast.typ -> Ast.typ
Sourceval expand_nexp_synonyms : t -> Ast.nexp -> Ast.nexp
Sourceval expand_constraint_synonyms : t -> Ast.n_constraint -> Ast.n_constraint
Sourceval simplify_constraints : t -> t
Sourceval base_typ_of : t -> Ast.typ -> Ast.typ
Sourceval allow_unknowns : t -> bool
Sourceval set_allow_unknowns : bool -> t -> t
Sourceval is_bitfield : Ast.id -> t -> bool
Sourceval no_bindings : t -> t
Sourceval is_toplevel : t -> Ast.l option
Sourceval wf_typ : at:Ast.l -> t -> Ast.typ -> unit
Sourceval wf_typ_arg : at:Ast.l -> t -> Ast.typ_arg -> unit
Sourceval wf_constraint : at:Ast.l -> t -> Ast.n_constraint -> unit
Sourceval 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.

Sourceval empty : t

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