package sail

  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Big_int = Nat_big_num
val opt_tc_debug : int Stdlib.ref
val opt_no_effects : bool Stdlib.ref
val opt_no_lexp_bounds_check : bool Stdlib.ref
val opt_expand_valspec : bool Stdlib.ref
val opt_smt_linearize : bool Stdlib.ref
val opt_smt_div : bool Stdlib.ref
val opt_new_bitfields : bool Stdlib.ref
type type_error =
  1. | Err_no_casts of unit Ast.exp * Ast.typ * Ast.typ * type_error * type_error list
  2. | Err_no_overloading of Ast.id * (Ast.id * type_error) list
  3. | Err_unresolved_quants of Ast.id * Ast.quant_item list * (Ast_util.mut * Ast.typ) Ast_util.Bindings.t * Ast.n_constraint list
  4. | Err_lexp_bounds of Ast.n_constraint * (Ast_util.mut * Ast.typ) Ast_util.Bindings.t * Ast.n_constraint list
  5. | Err_subtype of Ast.typ * Ast.typ * Ast.n_constraint list * Ast.l Ast_util.KBindings.t
  6. | Err_no_num_ident of Ast.id
  7. | Err_other of string
  8. | Err_because of type_error * Ast.l * type_error
type env
exception Type_error of env * Ast.l * type_error
val typ_debug : ?level:int -> string Stdlib.Lazy.t -> unit
val typ_print : string Stdlib.Lazy.t -> unit
module Env : sig ... end
val add_typquant : Ast.l -> Ast.typquant -> Env.t -> Env.t
val add_existential : Ast.l -> Ast.kinded_id list -> Ast.n_constraint -> Env.t -> Env.t
val orig_kid : Ast.kid -> Ast.kid
val dvector_typ : Env.t -> Ast.nexp -> Ast.typ -> Ast.typ
type tannot
val mk_tannot : Env.t -> Ast.typ -> Ast.effect -> tannot
val get_instantiations : tannot -> Ast.typ_arg Ast_util.KBindings.t option
val empty_tannot : tannot
val is_empty_tannot : tannot -> bool
val destruct_tannot : tannot -> (Env.t * Ast.typ * Ast.effect) option
val string_of_tannot : tannot -> string
val replace_typ : Ast.typ -> tannot -> tannot
val replace_env : Env.t -> tannot -> tannot
val strip_exp : 'a Ast.exp -> unit Ast.exp
val strip_pat : 'a Ast.pat -> unit Ast.pat
val strip_pexp : 'a Ast.pexp -> unit Ast.pexp
val strip_lexp : 'a Ast.lexp -> unit Ast.lexp
val strip_mpexp : 'a Ast.mpexp -> unit Ast.mpexp
val strip_mapcl : 'a Ast.mapcl -> unit Ast.mapcl
val strip_typ : Ast.typ -> Ast.typ
val strip_typq : Ast.typquant -> Ast.typquant
val strip_id : Ast.id -> Ast.id
val strip_kid : Ast.kid -> Ast.kid
val strip_base_effect : Ast.base_effect -> Ast.base_effect
val strip_effect : Ast.effect -> Ast.effect
val strip_nexp_aux : Ast.nexp_aux -> Ast.nexp_aux
val strip_nexp : Ast.nexp -> Ast.nexp
val strip_n_constraint_aux : Ast.n_constraint_aux -> Ast.n_constraint_aux
val strip_n_constraint : Ast.n_constraint -> Ast.n_constraint
val strip_typ_aux : Ast.typ_aux -> Ast.typ_aux
val check_exp : Env.t -> unit Ast.exp -> Ast.typ -> tannot Ast.exp
val infer_exp : Env.t -> unit Ast.exp -> tannot Ast.exp
val infer_pat : Env.t -> unit Ast.pat -> tannot Ast.pat * Env.t * unit Ast.exp list
val infer_lexp : Env.t -> unit Ast.lexp -> tannot Ast.lexp
val check_case : Env.t -> Ast.typ -> unit Ast.pexp -> Ast.typ -> tannot Ast.pexp
val check_funcl : Env.t -> 'a Ast.funcl -> Ast.typ -> tannot Ast.funcl
val check_fundef : Env.t -> 'a Ast.fundef -> tannot Ast.def list * Env.t
val check_val_spec : Env.t -> 'a Ast.val_spec -> tannot Ast.def list * Env.t
val assert_constraint : Env.t -> bool -> tannot Ast.exp -> Ast.n_constraint option
val prove : (string * int * int * int) -> Env.t -> Ast.n_constraint -> bool
val solve_unique : Env.t -> Ast.nexp -> Big_int.num option
val canonicalize : Env.t -> Ast.typ -> Ast.typ
val subtype_check : Env.t -> Ast.typ -> Ast.typ -> bool
val is_enum_member : Ast.id -> Env.t -> bool
val bind_pat : Env.t -> unit Ast.pat -> Ast.typ -> tannot Ast.pat * Env.t * unit Ast.exp list
val bind_pat_no_guard : Env.t -> unit Ast.pat -> Ast.typ -> tannot Ast.pat * Env.t
val typ_error : Env.t -> Ast.l -> string -> 'a
val env_of : tannot Ast.exp -> Env.t
val env_of_annot : (Ast.l * tannot) -> Env.t
val env_of_tannot : tannot -> Env.t
val typ_of : tannot Ast.exp -> Ast.typ
val typ_of_annot : (Ast.l * tannot) -> Ast.typ
val typ_of_tannot : tannot -> Ast.typ
val typ_of_pat : tannot Ast.pat -> Ast.typ
val env_of_pat : tannot Ast.pat -> Env.t
val typ_of_pexp : tannot Ast.pexp -> Ast.typ
val env_of_pexp : tannot Ast.pexp -> Env.t
val typ_of_mpat : tannot Ast.mpat -> Ast.typ
val env_of_mpat : tannot Ast.mpat -> Env.t
val typ_of_mpexp : tannot Ast.mpexp -> Ast.typ
val env_of_mpexp : tannot Ast.mpexp -> Env.t
val effect_of : tannot Ast.exp -> Ast.effect
val effect_of_pat : tannot Ast.pat -> Ast.effect
val effect_of_annot : tannot -> Ast.effect
val add_effect_annot : tannot -> Ast.effect -> tannot
val expected_typ_of : (Ast.l * tannot) -> Ast.typ option
val destruct_exist_plain : ?name:string option -> Ast.typ -> (Ast.kinded_id list * Ast.n_constraint * Ast.typ) option
val destruct_exist : ?name:string option -> Ast.typ -> (Ast.kinded_id list * Ast.n_constraint * Ast.typ) option
val destruct_atom_nexp : Env.t -> Ast.typ -> Ast.nexp option
val destruct_atom_bool : Env.t -> Ast.typ -> Ast.n_constraint option
val destruct_range : Env.t -> Ast.typ -> (Ast.kid list * Ast.n_constraint * Ast.nexp * Ast.nexp) option
val destruct_numeric : ?name:string option -> Ast.typ -> (Ast.kid list * Ast.n_constraint * Ast.nexp) option
val destruct_vector : Env.t -> Ast.typ -> (Ast.nexp * Ast.order * Ast.typ) option
val destruct_bitvector : Env.t -> Ast.typ -> (Ast.nexp * Ast.order) option
val exist_typ : (Ast.kid -> Ast.n_constraint) -> (Ast.kid -> Ast.typ) -> Ast.typ
val subst_unifiers : Ast.typ_arg Ast_util.KBindings.t -> Ast.typ -> Ast.typ
val alpha_equivalent : Env.t -> Ast.typ -> Ast.typ -> bool
val instantiation_of_without_type : tannot Ast.exp -> Ast.typ_arg Ast_util.KBindings.t
val instantiate_simple_equations : Ast.quant_item list -> Ast.typ_arg Ast_util.KBindings.t
val propagate_exp_effect : tannot Ast.exp -> tannot Ast.exp
val propagate_pexp_effect : tannot Ast.pexp -> tannot Ast.pexp * Ast.effect
val big_int_of_nexp : Ast.nexp -> Big_int.num option
val check : Env.t -> 'a Ast_defs.ast -> tannot Ast_defs.ast * Env.t
val check_defs : Env.t -> 'a Ast.def list -> tannot Ast.def list * Env.t
val check_with_envs : Env.t -> 'a Ast.def list -> (tannot Ast.def list * Env.t) list
val initial_env : Env.t
val prove_smt : Env.t -> Ast.n_constraint -> bool
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct