package libsail

  1. Overview
  2. Docs

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.

Sourcetype global_env
Sourcetype env
Sourcetype t = env
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 : ?ignore_duplicate:bool -> Ast.id -> (Ast.typquant * Ast.typ) -> t -> t
Sourceval update_val_spec : 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 : 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 add_outcome : Ast.id -> (Ast.typquant * Ast.typ * Ast.kinded_id list * Ast.id list * t) -> t -> t
Sourceval get_outcome : Ast.l -> Ast.id -> t -> Ast.typquant * Ast.typ * Ast.kinded_id list * Ast.id list * t
Sourceval get_outcome_instantiation : t -> (Ast.l * Ast.typ) Ast_util.KBindings.t
Sourceval add_outcome_variable : Ast.l -> Ast.kid -> Ast.typ -> 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_variant : Ast.id -> t -> bool
Sourceval add_variant : 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 : Ast.id -> (Ast.typquant * Ast.typ) -> t -> t
Sourceval get_union_id : Ast.id -> t -> Ast.typquant * Ast.typ
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_constraint_reasons : t -> ((Ast.l * string) option * Ast.n_constraint) list
Sourceval add_constraint : ?reason:(Ast.l * string) -> Ast.n_constraint -> t -> t
Sourceval add_typquant : Ast.l -> Ast.typquant -> t -> t
Sourceval get_typ_var : Ast.kid -> t -> Ast.kind_aux
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 : Ast.l -> Ast.kinded_id -> t -> t * Ast.kid option
Sourceval add_typ_var : 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 add_overloads : Ast.l -> Ast.id -> Ast.id list -> t -> t
Sourceval get_overloads : Ast.id -> t -> Ast.id list
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 -> t -> t
Sourceval add_enum_clause : Ast.id -> Ast.id -> t -> t
Sourceval get_enum : Ast.id -> t -> Ast.id list
Sourceval allow_polymorphic_undefineds : t -> t
Sourceval polymorphic_undefineds : t -> bool
Sourceval lookup_id : Ast.id -> t -> Ast.typ Ast_util.lvar
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 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 : t -> Ast.typ -> unit
Sourceval wf_constraint : ?exs:Ast_util.KidSet.t -> 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.