package libsail

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

Module Type_check.EnvSource

The env module defines the internal type checking environment, and contains functions that operate on that state.

Sourcetype t = env

Env.t is the type of environments

Sourceval open_all_modules : t -> t

This effectively disables all module related access control

Note: Most get_ functions assume the identifiers exist, and throw type errors if they don't.

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

Get the quantifier and type for a function identifier, freshening type variables.

Sourceval get_val_specs : t -> (Ast.typquant * Ast.typ) Ast_util.Bindings.t
Sourceval get_defined_val_specs : t -> Ast_util.IdSet.t
Sourceval get_val_spec_orig : Ast.id -> t -> Ast.typquant * Ast.typ

Like get_val_spec, except that the original type variables are used. Useful when processing the body of the function.

Sourceval update_val_spec : ?in_module:Project.mod_id -> Ast.id -> (Ast.typquant * Ast.typ) -> t -> t
Sourceval get_register : Ast.id -> t -> Ast.typ
Sourceval get_registers : t -> Ast.typ Ast_util.Bindings.t
Sourceval get_enum : Ast.id -> t -> Ast.id list

Return all the identifiers in an enumeration. Throws a type error if the enumeration doesn't exist.

Sourceval add_local : Ast.id -> (Ast_util.mut * Ast.typ) -> t -> t
Sourceval get_default_order : t -> Ast.order
Sourceval get_default_order_opt : t -> Ast.order option
Sourceval add_scattered_variant : Ast.id -> Ast.typquant -> t -> t
Sourceval is_mutable : Ast.id -> t -> bool

Check if a local variable is mutable. Throws Type_error if it isn't a local variable. Probably best to use Env.lookup_id instead

Sourceval get_constraints : t -> Ast.n_constraint list

Get the current set of constraints.

Sourceval add_constraint : ?global:bool -> ?reason:(Ast.l * string) -> Ast.n_constraint -> t -> t
Sourceval add_typquant : Ast.l -> Ast.typquant -> t -> t

Push all the type variables and constraints from a typquant into an environment

Sourceval get_typ_var : Ast.kid -> t -> Ast.kind_aux
Sourceval get_typ_var_locs : t -> Ast.l Ast_util.KBindings.t
Sourceval shadows : Ast.kid -> t -> int

Returns the shadowing depth for the given type variable

Sourceval get_typ_synonyms : t -> (Ast.typquant * Ast.typ_arg) Ast_util.Bindings.t
Sourceval bound_typ_id : t -> Ast.id -> bool

Check whether the identifier is a type name

Sourceval add_typ_var : Ast.l -> Ast.kinded_id -> t -> t
Sourceval is_record : Ast.id -> t -> bool
Sourceval get_record : Ast.id -> t -> Ast.typquant * (Ast.typ * Ast.id) list

Returns record quantifiers and fields

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

Return type is: quantifier, argument type, return type

Sourceval get_ret_typ : t -> Ast.typ option

If the environment is checking a function, then this will get the expected return type of the function. It's useful for checking or inserting early returns. Returns an option type and won't throw any exceptions.

Sourceval get_overloads : Ast.id -> t -> Ast.id list
Sourceval is_extern : Ast.id -> t -> string -> bool
Sourceval get_extern : Ast.id -> t -> string -> string
Sourceval lookup_id : Ast.id -> t -> Ast.typ Ast_util.lvar

Lookup id searchs for a specified id in the environment, and returns its type and what kind of identifier it is, using the lvar type. Returns Unbound if the identifier is unbound, and won't throw any exceptions.

Sourceval get_toplevel_lets : t -> Ast_util.IdSet.t
Sourceval get_outcome_instantiation : t -> (Ast.l * Ast.typ) Ast_util.KBindings.t
Sourceval union_constructor_info : Ast.id -> t -> (int * int * Ast.id * Ast.type_union) option

Check if id is a constructor, then if it is return a (n, m, id, type_union) triple where the values represent its position (n) in the list of (m) constructors, the union name, and the type_union entry itself

Sourceval is_union_constructor : Ast.id -> t -> bool
Sourceval is_singleton_union_constructor : Ast.id -> t -> bool

Check if the id is both a constructor, and the only constructor of that type.

Sourceval is_mapping : Ast.id -> t -> bool
Sourceval is_register : Ast.id -> t -> bool
Sourceval is_bitfield : Ast.id -> t -> bool

Check if the type with the given id is a bitfield type

Sourceval expand_constraint_synonyms : t -> Ast.n_constraint -> Ast.n_constraint
Sourceval expand_nexp_synonyms : t -> Ast.nexp -> Ast.nexp
Sourceval expand_synonyms : t -> Ast.typ -> Ast.typ
Sourceval base_typ_of : t -> Ast.typ -> Ast.typ

Expand type synonyms and remove register annotations (i.e. register<t> -> t))

Sourceval empty : t

Note: Likely want use Type_check.initial_env instead. The empty environment is lacking even basic builtins.

Sourceval get_union_id : Ast.id -> t -> Ast.typquant * Ast.typ
Sourceval set_prover : (t -> Ast.n_constraint -> bool) option -> t -> t