package libsail

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

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

type t = env

Env.t is the type of environments

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

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

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

val get_val_specs : t -> (Ast.typquant * Ast.typ) Ast_util.Bindings.t
val get_defined_val_specs : t -> Ast_util.IdSet.t
val 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.

val update_val_spec : Ast.id -> (Ast.typquant * Ast.typ) -> t -> t
val get_register : Ast.id -> t -> Ast.typ
val get_registers : t -> Ast.typ Ast_util.Bindings.t
val 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.

val get_locals : t -> (Ast_util.mut * Ast.typ) Ast_util.Bindings.t
val add_local : Ast.id -> (Ast_util.mut * Ast.typ) -> t -> t
val get_default_order_option : t -> Ast.order option
val add_scattered_variant : Ast.id -> Ast.typquant -> t -> t
val 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

val get_constraints : t -> Ast.n_constraint list

Get the current set of constraints.

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

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

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

Returns the shadowing depth for the given type variable

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

Check whether the identifier is a type name

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

Returns record quantifiers and fields

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

Return type is: quantifier, argument type, return type, effect

val 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.

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

Lookup id searchs for a specified id in the environment, and returns it's 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.

val get_toplevel_lets : t -> Ast_util.IdSet.t
val get_outcome_instantiation : t -> (Ast.l * Ast.typ) Ast_util.KBindings.t
val 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 it's position (n) in the list of (m) constructors, the union name, and the type_union entry itself

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

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

val is_mapping : Ast.id -> t -> bool
val is_register : Ast.id -> t -> bool
val expand_constraint_synonyms : t -> Ast.n_constraint -> Ast.n_constraint
val expand_nexp_synonyms : t -> Ast.nexp -> Ast.nexp
val expand_synonyms : t -> Ast.typ -> Ast.typ
val base_typ_of : t -> Ast.typ -> Ast.typ

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

val no_casts : t -> t

no_casts removes all the implicit type casts/coercions from the environment, so checking a term with such an environment will guarantee not to insert any casts. Not that this is only about the implicit casting and has nothing to do with the E_cast AST node.

val allow_casts : t -> bool

Is casting allowed by the environment?

val empty : t

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

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