why3 1.3.2 · OCaml Package

type dity

val dity_fresh : unit -> dity

val dity_of_ity : Ity.ity -> dity

val dity_int : dity

val dity_real : dity

val dity_str : dity

val dity_bool : dity

val dity_unit : dity

type dvty = dity list * dity

type dref = bool list * bool

type dpattern = private {

dp_pat : Expr.pre_pattern;
dp_dity : dity;
dp_vars : (dity * bool) Wstdlib.Mstr.t;
dp_loc : Loc.position option;

}

type dpattern_node =

| DPwild
| DPvar of Ident.preid * bool
| DPapp of Expr.rsymbol * dpattern list
| DPas of dpattern * Ident.preid * bool
| DPor of dpattern * dpattern
| DPcast of dpattern * dity

type ghost = bool

type dbinder = Ident.preid option * ghost * dity

val dummy_var_attr : Ident.attribute

exception UnboundLabel of string

val old_label : string

type register_old = string -> Ity.pvsymbol -> Ity.pvsymbol

type !'a later =
  Ity.pvsymbol Wstdlib.Mstr.t ->
  Ity.xsymbol Wstdlib.Mstr.t ->
  register_old ->
  'a

type dspec_final = {

ds_pre : Term.term list;
ds_post : (Ity.pvsymbol * Term.term) list;
ds_xpost : (Ity.pvsymbol * Term.term) list Ity.Mxs.t;
ds_reads : Ity.pvsymbol list;
ds_writes : Term.term list;
ds_diverge : bool;
ds_partial : bool;
ds_checkrw : bool;

}

type dspec = Ity.ity -> dspec_final

type dinvariant = Term.term list

type dxsymbol =

| DElexn of string * dity
| DEgexn of Ity.xsymbol

type dexpr = private {

de_node : dexpr_node;
de_dvty : dvty;
de_loc : Loc.position option;

}

and dexpr_node =

| DEvar of string * dvty * dref
| DEsym of Pmodule.prog_symbol
| DEconst of Constant.constant * dity
| DEapp of dexpr * dexpr
| DEfun of dbinder list * dity * Ity.mask * dspec later * dexpr
| DEany of dbinder list * dity * Ity.mask * dspec later
| DElet of dlet_defn * dexpr
| DErec of drec_defn * dexpr
| DEnot of dexpr
| DEand of dexpr * dexpr
| DEor of dexpr * dexpr
| DEif of dexpr * dexpr * dexpr
| DEmatch of dexpr * dreg_branch list * dexn_branch list
| DEassign of (dexpr * Expr.rsymbol * dexpr) list
| DEwhile of dexpr * dinvariant later * Expr.variant list later * dexpr
| DEfor of Ident.preid * dexpr * Expr.for_direction * dexpr * dinvariant later * dexpr
| DEraise of dxsymbol * dexpr
| DEghost of dexpr
| DEexn of Ident.preid * dity * Ity.mask * dexpr
| DEoptexn of Ident.preid * dity * Ity.mask * dexpr
| DEassert of Expr.assertion_kind * Term.term later
| DEpure of Term.term later * dity
| DEvar_pure of string * dvty * dref
| DEls_pure of Term.lsymbol * bool
| DEpv_pure of Ity.pvsymbol
| DEabsurd
| DEtrue
| DEfalse
| DElabel of Ident.preid * dexpr
| DEcast of dexpr * dity
| DEuloc of dexpr * Loc.position
| 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 {

fds : dfun_defn list;

}

and dfun_defn =
  Ident.preid
  * ghost
  * Expr.rs_kind
  * dbinder list
  * dity
  * Ity.mask
  * dspec later
  * Expr.variant list later
  * dexpr

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 undereference : dexpr -> dexpr

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

package why3