package why3

  1. Overview
  2. Docs
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.