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 ref
val opt_no_effects : bool ref
val opt_no_lexp_bounds_check : bool ref
val opt_expand_valspec : bool ref
val opt_smt_linearize : bool ref
val opt_smt_div : bool ref
val opt_new_bitfields : bool 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 Lazy.t -> unit
val typ_print : string 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