package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
type rsymbol = private {
  1. rs_name : Ident.ident;
  2. rs_cty : Ity.cty;
  3. rs_logic : rs_logic;
  4. rs_field : Ity.pvsymbol option;
}
and rs_logic =
  1. | RLnone
  2. | RLpv of Ity.pvsymbol
  3. | RLls of Term.lsymbol
  4. | RLlemma
module Mrs : sig ... end
module Srs : sig ... end
module Hrs : sig ... end
module Wrs : sig ... end
val rs_compare : rsymbol -> rsymbol -> int
val rs_equal : rsymbol -> rsymbol -> bool
val rs_hash : rsymbol -> int
type rs_kind =
  1. | RKnone
  2. | RKlocal
  3. | RKfunc
  4. | RKpred
  5. | RKlemma
val rs_kind : rsymbol -> rs_kind
val create_rsymbol : Ident.preid -> ?ghost:bool -> ?kind:rs_kind -> Ity.cty -> rsymbol
val create_constructor : constr:int -> Ident.preid -> Ity.itysymbol -> Ity.pvsymbol list -> rsymbol
val create_projection : Ity.itysymbol -> Ity.pvsymbol -> rsymbol
val restore_rs : Term.lsymbol -> rsymbol
val rs_ghost : rsymbol -> bool
val ls_of_rs : rsymbol -> Term.lsymbol
val fd_of_rs : rsymbol -> Ity.pvsymbol
type pat_ghost =
  1. | PGfail
  2. | PGlast
  3. | PGnone
type prog_pattern = private {
  1. pp_pat : Term.pattern;
  2. pp_ity : Ity.ity;
  3. pp_mask : Ity.mask;
  4. pp_fail : pat_ghost;
}
type pre_pattern =
  1. | PPwild
  2. | PPvar of Ident.preid * bool
  3. | PPapp of rsymbol * pre_pattern list
  4. | PPas of pre_pattern * Ident.preid * bool
  5. | PPor of pre_pattern * pre_pattern
exception ConstructorExpected of rsymbol
type assertion_kind =
  1. | Assert
  2. | Assume
  3. | Check
type for_direction =
  1. | To
  2. | DownTo
type invariant = Term.term
type variant = Term.term * Term.lsymbol option
type expr = private {
  1. e_node : expr_node;
  2. e_ity : Ity.ity;
  3. e_mask : Ity.mask;
  4. e_effect : Ity.effect;
  5. e_attrs : Ident.Sattr.t;
  6. e_loc : Loc.position option;
}
and expr_node =
  1. | Evar of Ity.pvsymbol
  2. | Econst of Number.constant
  3. | Eexec of cexp * Ity.cty
  4. | Eassign of assign list
  5. | Elet of let_defn * expr
  6. | Eif of expr * expr * expr
  7. | Ematch of expr * reg_branch list * exn_branch Ity.Mxs.t
  8. | Ewhile of expr * invariant list * variant list * expr
  9. | Efor of Ity.pvsymbol * for_bounds * Ity.pvsymbol * invariant list * expr
  10. | Eraise of Ity.xsymbol * expr
  11. | Eexn of Ity.xsymbol * expr
  12. | Eassert of assertion_kind * Term.term
  13. | Eghost of expr
  14. | Epure of Term.term
  15. | Eabsurd
and reg_branch = prog_pattern * expr
and exn_branch = Ity.pvsymbol list * expr
and cexp = private {
  1. c_node : cexp_node;
  2. c_cty : Ity.cty;
}
and cexp_node =
  1. | Capp of rsymbol * Ity.pvsymbol list
  2. | Cpur of Term.lsymbol * Ity.pvsymbol list
  3. | Cfun of expr
  4. | Cany
and let_defn = private
  1. | LDvar of Ity.pvsymbol * expr
  2. | LDsym of rsymbol * cexp
  3. | LDrec of rec_defn list
and rec_defn = private {
  1. rec_sym : rsymbol;
  2. rec_rsym : rsymbol;
  3. rec_fun : cexp;
  4. rec_varl : variant list;
}
val e_attr_set : ?loc:Loc.position -> Ident.Sattr.t -> expr -> expr
val e_attr_push : ?loc:Loc.position -> Ident.Sattr.t -> expr -> expr
val e_attr_add : Ident.attribute -> expr -> expr
val e_attr_copy : expr -> expr -> expr
val let_var : Ident.preid -> ?ghost:bool -> expr -> let_defn * Ity.pvsymbol
val let_sym : Ident.preid -> ?ghost:bool -> ?kind:rs_kind -> cexp -> let_defn * rsymbol
val let_rec : (rsymbol * cexp * variant list * rs_kind) list -> let_defn * rec_defn list
val ls_decr_of_rec_defn : rec_defn -> Term.lsymbol option
val c_app : rsymbol -> Ity.pvsymbol list -> Ity.ity list -> Ity.ity -> cexp
val c_pur : Term.lsymbol -> Ity.pvsymbol list -> Ity.ity list -> Ity.ity -> cexp
val c_fun : ?mask:Ity.mask -> Ity.pvsymbol list -> Ity.pre list -> Ity.post list -> Ity.post list Ity.Mxs.t -> Ity.pvsymbol Ity.Mpv.t -> expr -> cexp
val c_any : Ity.cty -> cexp
val e_var : Ity.pvsymbol -> expr
val e_const : Number.constant -> Ity.ity -> expr
val e_nat_const : int -> expr
val e_exec : cexp -> expr
val e_app : rsymbol -> expr list -> Ity.ity list -> Ity.ity -> expr
val e_pur : Term.lsymbol -> expr list -> Ity.ity list -> Ity.ity -> expr
val e_let : let_defn -> expr -> expr
exception FieldExpected of rsymbol
val e_assign : (expr * rsymbol * expr) list -> expr
val e_if : expr -> expr -> expr -> expr
val e_and : expr -> expr -> expr
val e_or : expr -> expr -> expr
val e_not : expr -> expr
val e_true : expr
val e_false : expr
val is_e_true : expr -> bool
val is_e_false : expr -> bool
exception ExceptionLeak of Ity.xsymbol
val e_exn : Ity.xsymbol -> expr -> expr
val e_raise : Ity.xsymbol -> expr -> Ity.ity -> expr
val e_match : expr -> reg_branch list -> exn_branch Ity.Mxs.t -> expr
val e_while : expr -> invariant list -> variant list -> expr -> expr
val e_for : Ity.pvsymbol -> expr -> for_direction -> expr -> Ity.pvsymbol -> invariant list -> expr -> expr
val e_assert : assertion_kind -> Term.term -> expr
val e_ghostify : bool -> expr -> expr
val e_pure : Term.term -> expr
val e_absurd : Ity.ity -> expr
val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a
val e_locate_effect : (Ity.effect -> bool) -> expr -> Loc.position option
val proxy_attr : Ident.attribute
val e_rs_subst : rsymbol Mrs.t -> expr -> expr
val c_rs_subst : rsymbol Mrs.t -> cexp -> cexp
val term_of_post : prop:bool -> Term.vsymbol -> Term.term -> (Term.term * Term.term) option
val term_of_expr : prop:bool -> expr -> Term.term option
val post_of_expr : Term.term -> expr -> Term.term option
val e_ghost : expr -> bool
val c_ghost : cexp -> bool
val rs_true : rsymbol
val rs_false : rsymbol
val rs_tuple : int -> rsymbol
val e_tuple : expr list -> expr
val rs_void : rsymbol
val fs_void : Term.lsymbol
val e_void : expr
val t_void : Term.term
val is_e_void : expr -> bool
val is_rs_tuple : rsymbol -> bool
val rs_func_app : rsymbol
val ld_func_app : let_defn
val e_func_app : expr -> expr -> expr
val e_func_app_l : expr -> expr list -> expr
val forget_rs : rsymbol -> unit
val print_rs : Format.formatter -> rsymbol -> unit
val print_expr : Format.formatter -> expr -> unit
val print_let_defn : Format.formatter -> let_defn -> unit
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