package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type vsymbol = private {
  1. vs_name : Ident.ident;
  2. vs_ty : Ty.ty;
}
module Mvs : sig ... end
module Svs : sig ... end
module Hvs : sig ... end
module Wvs : sig ... end
val vs_compare : vsymbol -> vsymbol -> int
val vs_equal : vsymbol -> vsymbol -> bool
val vs_hash : vsymbol -> int
val create_vsymbol : Ident.preid -> Ty.ty -> vsymbol
type lsymbol = private {
  1. ls_name : Ident.ident;
  2. ls_args : Ty.ty list;
  3. ls_value : Ty.ty option;
  4. ls_constr : int;
}
module Mls : sig ... end
module Sls : sig ... end
module Hls : sig ... end
module Wls : sig ... end
val ls_compare : lsymbol -> lsymbol -> int
val ls_equal : lsymbol -> lsymbol -> bool
val ls_hash : lsymbol -> int
val create_lsymbol : ?constr:int -> Ident.preid -> Ty.ty list -> Ty.ty option -> lsymbol
val create_fsymbol : ?constr:int -> Ident.preid -> Ty.ty list -> Ty.ty -> lsymbol
val create_psymbol : Ident.preid -> Ty.ty list -> lsymbol
val ls_ty_freevars : lsymbol -> Ty.Stv.t
exception EmptyCase
exception DuplicateVar of vsymbol
exception UncoveredVar of vsymbol
exception BadArity of lsymbol * int
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
exception ConstructorExpected of lsymbol
exception InvalidIntegerLiteralType of Ty.ty
exception InvalidRealLiteralType of Ty.ty
exception InvalidStringLiteralType of Ty.ty
type pattern = private {
  1. pat_node : pattern_node;
  2. pat_vars : Svs.t;
  3. pat_ty : Ty.ty;
}
and pattern_node =
  1. | Pwild
  2. | Pvar of vsymbol
  3. | Papp of lsymbol * pattern list
  4. | Por of pattern * pattern
  5. | Pas of pattern * vsymbol
val pat_wild : Ty.ty -> pattern
val pat_var : vsymbol -> pattern
val pat_app : lsymbol -> pattern list -> Ty.ty -> pattern
val pat_or : pattern -> pattern -> pattern
val pat_as : pattern -> vsymbol -> pattern
val pat_map : (pattern -> pattern) -> pattern -> pattern
val pat_fold : ('a -> pattern -> 'a) -> 'a -> pattern -> 'a
val pat_all : (pattern -> bool) -> pattern -> bool
val pat_any : (pattern -> bool) -> pattern -> bool
type quant =
  1. | Tforall
  2. | Texists
type binop =
  1. | Tand
  2. | Tor
  3. | Timplies
  4. | Tiff
type term = private {
  1. t_node : term_node;
  2. t_ty : Ty.ty option;
  3. t_attrs : Ident.Sattr.t;
  4. t_loc : Loc.position option;
}
and term_node =
  1. | Tvar of vsymbol
  2. | Tconst of Constant.constant
  3. | Tapp of lsymbol * term list
  4. | Tif of term * term * term
  5. | Tlet of term * term_bound
  6. | Tcase of term * term_branch list
  7. | Teps of term_bound
  8. | Tquant of quant * term_quant
  9. | Tbinop of binop * term * term
  10. | Tnot of term
  11. | Ttrue
  12. | Tfalse
and term_bound
and term_branch
and term_quant
and trigger = term list list
val t_equal_strict : term -> term -> bool
val t_compare_strict : term -> term -> int
val t_hash_strict : term -> int
module Mterm_strict : sig ... end
module Sterm_strict : sig ... end
module Hterm_strict : sig ... end
val t_equal : term -> term -> bool
val t_compare : term -> term -> int
val t_hash : term -> int
module Mterm : sig ... end
module Sterm : sig ... end
module Hterm : sig ... end
val t_close_bound : vsymbol -> term -> term_bound
val t_close_branch : pattern -> term -> term_branch
val t_close_quant : vsymbol list -> trigger -> term -> term_quant
val t_open_bound : term_bound -> vsymbol * term
val t_open_branch : term_branch -> pattern * term
val t_open_quant : term_quant -> vsymbol list * trigger * term
val t_open_bound_with : term -> term_bound -> term
val t_clone_bound_id : term_bound -> Ident.preid
val t_open_bound_cb : term_bound -> vsymbol * term * (vsymbol -> term -> term_bound)
val t_open_branch_cb : term_branch -> pattern * term * (pattern -> term -> term_branch)
val t_open_quant_cb : term_quant -> vsymbol list * trigger * term * (vsymbol list -> trigger -> term -> term_quant)
val t_peek_bound : term_bound -> Ident.ident
val t_peek_branch : term_branch -> Ident.Sid.t
val t_peek_quant : term_quant -> Ident.ident list
exception TermExpected of term
exception FmlaExpected of term
val t_type : term -> Ty.ty
val t_prop : term -> term
val t_ty_check : term -> Ty.ty option -> unit
val t_app : lsymbol -> term list -> Ty.ty option -> term
val fs_app : lsymbol -> term list -> Ty.ty -> term
val ps_app : lsymbol -> term list -> term
val t_app_infer : lsymbol -> term list -> term
val ls_arg_inst : lsymbol -> term list -> Ty.ty Ty.Mtv.t
val ls_app_inst : lsymbol -> term list -> Ty.ty option -> Ty.ty Ty.Mtv.t
val check_literal : Constant.constant -> Ty.ty -> unit
val t_var : vsymbol -> term
val t_const : Constant.constant -> Ty.ty -> term
val t_if : term -> term -> term -> term
val t_let : term -> term_bound -> term
val t_case : term -> term_branch list -> term
val t_eps : term_bound -> term
val t_quant : quant -> term_quant -> term
val t_forall : term_quant -> term
val t_exists : term_quant -> term
val t_binary : binop -> term -> term -> term
val t_and : term -> term -> term
val t_or : term -> term -> term
val t_implies : term -> term -> term
val t_iff : term -> term -> term
val t_not : term -> term
val t_true : term
val t_false : term
val t_nat_const : int -> term
val t_int_const : BigInt.t -> term
val t_real_const : ?pow2:BigInt.t -> ?pow5:BigInt.t -> BigInt.t -> term
val t_string_const : string -> term
val stop_split : Ident.attribute
val asym_split : Ident.attribute
val t_and_l : term list -> term
val t_or_l : term list -> term
val t_and_asym : term -> term -> term
val t_or_asym : term -> term -> term
val t_and_asym_l : term list -> term
val t_or_asym_l : term list -> term
val t_let_close : vsymbol -> term -> term -> term
val t_eps_close : vsymbol -> term -> term
val t_case_close : term -> (pattern * term) list -> term
val t_quant_close : quant -> vsymbol list -> trigger -> term -> term
val t_forall_close : vsymbol list -> trigger -> term -> term
val t_exists_close : vsymbol list -> trigger -> term -> term
val t_attr_set : ?loc:Loc.position -> Ident.Sattr.t -> term -> term
val t_attr_add : Ident.attribute -> term -> term
val t_attr_remove : Ident.attribute -> term -> term
val t_attr_copy : term -> term -> term
val t_if_simp : term -> term -> term -> term
val t_let_simp : term -> term_bound -> term
val t_case_simp : term -> term_branch list -> term
val t_quant_simp : quant -> term_quant -> term
val t_forall_simp : term_quant -> term
val t_exists_simp : term_quant -> term
val t_binary_simp : binop -> term -> term -> term
val t_and_simp : term -> term -> term
val t_and_simp_l : term list -> term
val t_or_simp : term -> term -> term
val t_or_simp_l : term list -> term
val t_implies_simp : term -> term -> term
val t_iff_simp : term -> term -> term
val t_not_simp : term -> term
val t_and_asym_simp : term -> term -> term
val t_and_asym_simp_l : term list -> term
val t_or_asym_simp : term -> term -> term
val t_or_asym_simp_l : term list -> term
val t_let_close_simp : vsymbol -> term -> term -> term
val t_case_close_simp : term -> (pattern * term) list -> term
val t_quant_close_simp : quant -> vsymbol list -> trigger -> term -> term
val t_forall_close_simp : vsymbol list -> trigger -> term -> term
val t_exists_close_simp : vsymbol list -> trigger -> term -> term
val t_forall_close_merge : vsymbol list -> term -> term
val t_exists_close_merge : vsymbol list -> term -> term
val ps_equ : lsymbol
val t_equ : term -> term -> term
val t_neq : term -> term -> term
val t_equ_simp : term -> term -> term
val t_neq_simp : term -> term -> term
val fs_bool_true : lsymbol
val fs_bool_false : lsymbol
val t_bool_true : term
val t_bool_false : term
val fs_tuple : int -> lsymbol
val t_tuple : term list -> term
val is_fs_tuple : lsymbol -> bool
val is_fs_tuple_id : Ident.ident -> int option
val fs_func_app : lsymbol
val t_func_app : term -> term -> term
val t_pred_app : term -> term -> term
val t_func_app_l : term -> term list -> term
val t_pred_app_l : term -> term list -> term
val t_lambda : vsymbol list -> trigger -> term -> term
val t_open_lambda : term -> vsymbol list * trigger * term
val t_open_lambda_cb : term -> vsymbol list * trigger * term * (vsymbol list -> trigger -> term -> term)
val t_is_lambda : term -> bool
val t_closure : lsymbol -> Ty.ty list -> Ty.ty option -> term
val t_app_partial : lsymbol -> term list -> Ty.ty list -> Ty.ty option -> term
val t_func_app_beta : term -> term -> term
val t_pred_app_beta : term -> term -> term
val t_func_app_beta_l : term -> term list -> term
val t_pred_app_beta_l : term -> term list -> term
val t_map : (term -> term) -> term -> term
val t_fold : ('a -> term -> 'a) -> 'a -> term -> 'a
val t_iter : (term -> unit) -> term -> unit
val t_map_fold : ('a -> term -> 'a * term) -> 'a -> term -> 'a * term
val t_all : (term -> bool) -> term -> bool
val t_any : (term -> bool) -> term -> bool
val t_map_simp : (term -> term) -> term -> term
val t_map_sign : (bool -> term -> term) -> bool -> term -> term
val t_map_cont : ((term -> 'a) -> term -> 'a) -> (term -> 'a) -> term -> 'a
val list_map_cont : (('a -> 'b) -> 'c -> 'b) -> ('a list -> 'b) -> 'c list -> 'b
val tr_equal : trigger -> trigger -> bool
val tr_map : (term -> term) -> trigger -> trigger
val tr_fold : ('a -> term -> 'a) -> 'a -> trigger -> 'a
val tr_map_fold : ('a -> term -> 'a * term) -> 'a -> trigger -> 'a * trigger
module TermTF : sig ... end
val t_v_map : (vsymbol -> term) -> term -> term
val t_v_fold : ('a -> vsymbol -> 'a) -> 'a -> term -> 'a
val t_v_all : (vsymbol -> bool) -> term -> bool
val t_v_any : (vsymbol -> bool) -> term -> bool
val t_v_count : ('a -> vsymbol -> int -> 'a) -> 'a -> term -> 'a
val t_v_occurs : vsymbol -> term -> int
val t_subst_single : vsymbol -> term -> term -> term
val t_subst : term Mvs.t -> term -> term
val t_ty_subst : Ty.ty Ty.Mtv.t -> term Mvs.t -> term -> term
val t_subst_types : Ty.ty Ty.Mtv.t -> term Mvs.t -> term -> term Mvs.t * term
val t_closed : term -> bool
val t_vars : term -> int Mvs.t
val t_freevars : int Mvs.t -> term -> int Mvs.t
val t_ty_freevars : Ty.Stv.t -> term -> Ty.Stv.t
val t_gen_map : (Ty.ty -> Ty.ty) -> (lsymbol -> lsymbol) -> vsymbol Mvs.t -> term -> term
val t_s_map : (Ty.ty -> Ty.ty) -> (lsymbol -> lsymbol) -> term -> term
val t_s_fold : ('a -> Ty.ty -> 'a) -> ('a -> lsymbol -> 'a) -> 'a -> term -> 'a
val t_s_all : (Ty.ty -> bool) -> (lsymbol -> bool) -> term -> bool
val t_s_any : (Ty.ty -> bool) -> (lsymbol -> bool) -> term -> bool
val t_ty_map : (Ty.ty -> Ty.ty) -> term -> term
val t_ty_fold : ('a -> Ty.ty -> 'a) -> 'a -> term -> 'a
val t_app_map : (lsymbol -> Ty.ty list -> Ty.ty option -> lsymbol) -> term -> term
val t_app_fold : ('a -> lsymbol -> Ty.ty list -> Ty.ty option -> 'a) -> 'a -> term -> 'a
val t_occurs : term -> term -> bool
val t_replace : term -> term -> term -> term
OCaml

Innovation. Community. Security.