sail 0.13 · OCaml Package

type t = env

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

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_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 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 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_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 builtin_typs : Ast.typquant Ast_util.Bindings.t

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

val set_prover : (t -> Ast.n_constraint -> bool) option -> t -> t

package sail