package sail

  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = env
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 update_val_spec : Ast.id -> (Ast.typquant * Ast.typ) -> t -> t
val get_register : Ast.id -> t -> Ast.effect * Ast.effect * Ast.typ
val get_registers : t -> (Ast.effect * Ast.effect * Ast.typ) Ast_util.Bindings.t
val get_enum : Ast.id -> t -> Ast.id list
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
val get_constraints : t -> Ast.n_constraint list
val add_constraint : Ast.n_constraint -> t -> t
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 get_typ_synonyms : t -> (Ast.typquant * Ast.typ_arg) Ast_util.Bindings.t
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
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 * Ast.effect
val get_ret_typ : t -> Ast.typ option
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 : ?raw:bool -> Ast.id -> t -> Ast.typ Ast_util.lvar
val get_toplevel_lets : t -> Ast_util.IdSet.t
val is_union_constructor : Ast.id -> t -> bool
val is_singleton_union_constructor : Ast.id -> t -> bool
val is_mapping : Ast.id -> t -> bool
val is_register : Ast.id -> t -> bool
val fresh_kid : ?kid:Ast.kid -> t -> Ast.kid
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
val no_casts : t -> t
val allow_casts : t -> bool
val empty : t
val pattern_completeness_ctx : t -> Pattern_completeness.ctx
val get_union_id : Ast.id -> t -> Ast.typquant * Ast.typ
val set_prover : (t -> Ast.n_constraint -> bool) option -> t -> t