why3 1.0.0 · OCaml Package

type ty =

| Tvar of Ty.tvsymbol
| Tapp of Ident.ident * ty list
| Ttuple of ty list

type is_ghost = bool

type var = Ident.ident * ty * is_ghost

type for_direction =

| To
| DownTo

type pat =

| Pwild
| Pvar of Term.vsymbol
| Papp of Term.lsymbol * pat list
| Ptuple of pat list
| Por of pat * pat
| Pas of pat * Term.vsymbol

type is_rec = bool

type binop =

| Band
| Bor
| Beq

type ity =

| I of Ity.ity
| C of Ity.cty

type expr = {

e_node : expr_node;
e_ity : ity;
e_effect : Ity.effect;
e_attrs : Ident.Sattr.t;

}

and expr_node =

| Econst of Number.integer_constant
| Evar of Ity.pvsymbol
| Eapp of Expr.rsymbol * expr list
| Efun of var list * expr
| Elet of let_def * expr
| Eif of expr * expr * expr
| Eassign of (Ity.pvsymbol * Expr.rsymbol * Ity.pvsymbol) list
| Ematch of expr * reg_branch list * exn_branch list
| Eblock of expr list
| Ewhile of expr * expr
| Efor of Ity.pvsymbol * Ity.pvsymbol * for_direction * Ity.pvsymbol * expr
| Eraise of Ity.xsymbol * expr option
| Eexn of Ity.xsymbol * ty option * expr
| Eignore of expr
| Eany of ty
| Eabsurd
| Ehole

and reg_branch = pat * expr

and exn_branch = Ity.xsymbol * Ity.pvsymbol list * expr

and let_def =

| Lvar of Ity.pvsymbol * expr
| Lsym of Expr.rsymbol * ty * var list * expr
| Lany of Expr.rsymbol * ty * var list
| Lrec of rdef list

and rdef = {

rec_sym : Expr.rsymbol;
rec_rsym : Expr.rsymbol;
rec_args : var list;
rec_exp : expr;
rec_res : ty;
rec_svar : Ty.Stv.t;

}

type is_mutable = bool

type typedef =

| Ddata of (Ident.ident * ty list) list
| Drecord of (is_mutable * Ident.ident * ty) list
| Dalias of ty
| Drange of Number.int_range
| Dfloat of Number.float_format

type its_defn = {

its_name : Ident.ident;
its_args : Ty.tvsymbol list;
its_private : bool;
its_def : typedef option;

}

type decl =

| Dtype of its_defn list
| Dlet of let_def
| Dexn of Ity.xsymbol * ty option
| Dmodule of string * decl list

type namespace = (Ident.ident * decl list) list

type from_module = {

from_mod : Pmodule.pmodule option;
from_km : Pdecl.known_map;

}

type known_map = decl Ident.Mid.t

type pmodule = {

mod_from : from_module;
mod_decl : decl list;
mod_known : known_map;

}

val get_decl_name : decl -> Ident.ident list

val add_known_decl : 
  decl ->
  decl Ident.Mid.t ->
  Ident.Mid.key ->
  decl Ident.Mid.t

val iter_deps_ty : (Ident.ident -> 'a) -> ty -> unit

val iter_deps_typedef : (Ident.ident -> 'a) -> typedef -> unit

val iter_deps_its_defn : (Ident.ident -> 'a) -> its_defn -> unit

val iter_deps_args : (Ident.ident -> 'a) -> ('b * ty * 'c) list -> unit

val iter_deps_xbranch : (Ident.ident -> unit) -> exn_branch -> unit

val iter_deps_pat_list : (Ident.ident -> unit) -> pat list -> unit

val iter_deps_pat : (Ident.ident -> unit) -> pat -> unit

val iter_deps_expr : (Ident.ident -> unit) -> expr -> unit

val iter_deps : (Ident.ident -> unit) -> decl -> unit

val ity_unit : ity

val ity_of_mask : ity -> Ity.mask -> ity

val mk_expr : 
  expr_node ->
  ity ->
  Ity.mask ->
  Ity.effect ->
  Ident.Sattr.t ->
  expr

val tunit : ty

val is_unit : ity -> bool

val enope : expr_node

val e_any : ty -> Ity.cty -> expr

val mk_hole : expr

val mk_var : 'a -> 'b -> 'c -> 'a * 'b * 'c

val mk_var_unit : Ident.ident * ty * bool

val mk_its_defn : 
  Ident.ident ->
  Ty.tvsymbol list ->
  bool ->
  typedef option ->
  its_defn

val e_unit : expr

val var_defn : Ity.pvsymbol -> expr -> let_def

val sym_defn : Expr.rsymbol -> ty -> var list -> expr -> let_def

val e_let : 
  let_def ->
  expr ->
  ity ->
  Ity.mask ->
  Ity.effect ->
  Ident.Sattr.t ->
  expr

val e_app : 
  Expr.rsymbol ->
  expr list ->
  ity ->
  Ity.mask ->
  Ity.effect ->
  Ident.Sattr.t ->
  expr

val e_fun : 
  var list ->
  expr ->
  ity ->
  Ity.mask ->
  Ity.effect ->
  Ident.Sattr.t ->
  expr

val e_ignore : Ity.ity -> expr -> expr

val e_if : 
  expr ->
  expr ->
  expr ->
  Ity.mask ->
  Ity.effect ->
  Ident.Sattr.t ->
  expr

val e_while : expr -> expr -> Ity.mask -> Ity.effect -> Ident.Sattr.t -> expr

val e_for : 
  Ity.pvsymbol ->
  Ity.pvsymbol ->
  for_direction ->
  Ity.pvsymbol ->
  expr ->
  Ity.mask ->
  Ity.effect ->
  Ident.Sattr.t ->
  expr

val e_match : 
  expr ->
  reg_branch list ->
  exn_branch list ->
  ity ->
  Ity.mask ->
  Ity.effect ->
  Ident.Sattr.t ->
  expr

val e_assign : 
  (Ity.pvsymbol * Expr.rsymbol * Ity.pvsymbol) list ->
  ity ->
  Ity.mask ->
  Ity.effect ->
  Ident.Sattr.t ->
  expr

val e_absurd : ity -> Ity.mask -> Ity.effect -> Ident.Sattr.t -> expr

val e_seq : 
  expr ->
  expr ->
  ity ->
  Ity.mask ->
  Ity.effect ->
  Ident.Sattr.t ->
  expr

val var_list_of_pv_list : Ity.pvsymbol list -> expr list

package why3