package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type dity
val dity_fresh : unit -> dity
val dity_of_ity : Ity.ity -> dity
val dity_int : dity
val dity_real : dity
val dity_bool : dity
val dity_unit : dity
type dvty = dity list * dity
type dpattern = private {
  1. dp_pat : Expr.pre_pattern;
  2. dp_dity : dity;
  3. dp_vars : dity Wstdlib.Mstr.t;
  4. dp_loc : Loc.position option;
}
type dpattern_node =
  1. | DPwild
  2. | DPvar of Ident.preid * bool
  3. | DPapp of Expr.rsymbol * dpattern list
  4. | DPas of dpattern * Ident.preid * bool
  5. | DPor of dpattern * dpattern
  6. | DPcast of dpattern * dity
type ghost = bool
type dbinder = Ident.preid option * ghost * dity
exception UnboundLabel of string
val old_label : string
type register_old = string -> Ity.pvsymbol -> Ity.pvsymbol
type dspec_final = {
  1. ds_pre : Term.term list;
  2. ds_post : (Ity.pvsymbol * Term.term) list;
  3. ds_xpost : (Ity.pvsymbol * Term.term) list Ity.Mxs.t;
  4. ds_reads : Ity.pvsymbol list;
  5. ds_writes : Term.term list;
  6. ds_diverge : bool;
  7. ds_partial : bool;
  8. ds_checkrw : bool;
}
type dspec = Ity.ity -> dspec_final
type dinvariant = Term.term list
type dxsymbol =
  1. | DElexn of string * dity
  2. | DEgexn of Ity.xsymbol
type dexpr = private {
  1. de_node : dexpr_node;
  2. de_dvty : dvty;
  3. de_loc : Loc.position option;
}
and dexpr_node =
  1. | DEvar of string * dvty
  2. | DEsym of Pmodule.prog_symbol
  3. | DEconst of Number.constant * dity
  4. | DEapp of dexpr * dexpr
  5. | DEfun of dbinder list * dity * Ity.mask * dspec later * dexpr
  6. | DEany of dbinder list * dity * Ity.mask * dspec later
  7. | DElet of dlet_defn * dexpr
  8. | DErec of drec_defn * dexpr
  9. | DEnot of dexpr
  10. | DEand of dexpr * dexpr
  11. | DEor of dexpr * dexpr
  12. | DEif of dexpr * dexpr * dexpr
  13. | DEmatch of dexpr * dreg_branch list * dexn_branch list
  14. | DEassign of (dexpr * Expr.rsymbol * dexpr) list
  15. | DEwhile of dexpr * dinvariant later * Expr.variant list later * dexpr
  16. | DEfor of Ident.preid * dexpr * Expr.for_direction * dexpr * dinvariant later * dexpr
  17. | DEraise of dxsymbol * dexpr
  18. | DEghost of dexpr
  19. | DEexn of Ident.preid * dity * Ity.mask * dexpr
  20. | DEoptexn of Ident.preid * dity * Ity.mask * dexpr
  21. | DEassert of Expr.assertion_kind * Term.term later
  22. | DEpure of Term.term later * dity
  23. | DEvar_pure of string * dvty
  24. | DEls_pure of Term.lsymbol * bool
  25. | DEpv_pure of Ity.pvsymbol
  26. | DEabsurd
  27. | DEtrue
  28. | DEfalse
  29. | DElabel of Ident.preid * dexpr
  30. | DEcast of dexpr * dity
  31. | DEuloc of dexpr * Loc.position
  32. | DEattr of dexpr * Ident.Sattr.t
and dreg_branch = dpattern * dexpr
and dexn_branch = dxsymbol * dpattern * dexpr
and dlet_defn = Ident.preid * ghost * Expr.rs_kind * dexpr
and drec_defn = private {
  1. fds : dfun_defn list;
}
type denv
val denv_empty : denv
val denv_add_var : denv -> Ident.preid -> dity -> denv
val denv_add_let : denv -> dlet_defn -> denv
val denv_add_args : denv -> dbinder list -> denv
val denv_add_pat : denv -> dpattern -> dity -> denv
val denv_add_expr_pat : denv -> dpattern -> dexpr -> denv
val denv_add_exn_pat : denv -> dpattern -> dxsymbol -> denv
val denv_add_for_index : denv -> Ident.preid -> dvty -> denv
val denv_add_exn : denv -> Ident.preid -> dity -> denv
val denv_get : denv -> string -> dexpr_node
val denv_get_opt : denv -> string -> dexpr_node option
val denv_get_pure : denv -> string -> dexpr_node
val denv_get_pure_opt : denv -> string -> dexpr_node option
val denv_get_exn : denv -> string -> dxsymbol
val denv_get_exn_opt : denv -> string -> dxsymbol option
val denv_names : denv -> Wstdlib.Sstr.t
val denv_pure : denv -> (Dterm.denv -> Dterm.dty) -> dity
val dpattern : ?loc:Loc.position -> dpattern_node -> dpattern
val dexpr : ?loc:Loc.position -> dexpr_node -> dexpr
type pre_fun_defn = Ident.preid * ghost * Expr.rs_kind * dbinder list * dity * Ity.mask * (denv -> dspec later * Expr.variant list later * dexpr)
val drec_defn : denv -> pre_fun_defn list -> denv * drec_defn
val expr : ?keep_loc:bool -> ?ughost:bool -> dexpr -> Expr.expr
val let_defn : ?keep_loc:bool -> dlet_defn -> Expr.let_defn
val rec_defn : ?keep_loc:bool -> drec_defn -> Expr.let_defn
OCaml

Innovation. Community. Security.