package libsail

  1. Overview
  2. Docs
package libsail
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.

type global_env
type env
type t = env
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 : ?ignore_duplicate:bool -> Ast.id -> (Ast.typquant * Ast.typ) -> t -> t
val update_val_spec : 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 : 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_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 : 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 : ?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 add_overloads : Ast.l -> Ast.id -> Ast.id list -> t -> t
val get_overloads : Ast.id -> t -> Ast.id list
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 : Ast.id -> t -> Ast.id list
val allow_polymorphic_undefineds : t -> t
val polymorphic_undefineds : t -> bool
val lookup_id : Ast.id -> t -> Ast.typ Ast_util.lvar
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 : t -> Ast.typ -> unit
val wf_constraint : ?exs:Ast_util.KidSet.t -> 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.