package why3

  1. Overview
  2. Docs
Package contains no libraries
type ty =
  1. | Tvar of Ty.tvsymbol
  2. | Tapp of Ident.ident * ty list
  3. | Ttuple of ty list
type is_ghost = bool
type var = Ident.ident * ty * is_ghost
type for_direction =
  1. | To
  2. | DownTo
type pat =
  1. | Pwild
  2. | Pvar of Term.vsymbol
  3. | Papp of Term.lsymbol * pat list
  4. | Ptuple of pat list
  5. | Por of pat * pat
  6. | Pas of pat * Term.vsymbol
type is_rec = bool
type binop =
  1. | Band
  2. | Bor
  3. | Beq
type ity =
  1. | I of Ity.ity
  2. | C of Ity.cty
type expr = {
  1. e_node : expr_node;
  2. e_ity : ity;
  3. e_effect : Ity.effect;
  4. e_attrs : Ident.Sattr.t;
}
and expr_node =
  1. | Econst of Constant.constant
  2. | Evar of Ity.pvsymbol
  3. | Eapp of Expr.rsymbol * expr list
  4. | Efun of var list * expr
  5. | Elet of let_def * expr
  6. | Eif of expr * expr * expr
  7. | Eassign of (Ity.pvsymbol * Expr.rsymbol * expr) list
  8. | Ematch of expr * reg_branch list * exn_branch list
  9. | Eblock of expr list
  10. | Ewhile of expr * expr
  11. | Efor of Ity.pvsymbol * Ity.pvsymbol * for_direction * Ity.pvsymbol * expr
  12. | Eraise of Ity.xsymbol * expr option
  13. | Eexn of Ity.xsymbol * ty option * expr
  14. | Eignore of expr
  15. | Eabsurd
and reg_branch = pat * expr
and exn_branch = Ity.xsymbol * Ity.pvsymbol list * expr
and let_def =
  1. | Lvar of Ity.pvsymbol * expr
  2. | Lsym of Expr.rsymbol * Ty.Stv.t * ty * var list * expr
  3. | Lany of Expr.rsymbol * Ty.Stv.t * ty * var list
  4. | Lrec of rdef list
and rdef = {
  1. rec_sym : Expr.rsymbol;
  2. rec_args : var list;
  3. rec_exp : expr;
  4. rec_res : ty;
  5. rec_svar : Ty.Stv.t;
}
type is_mutable = bool
type typedef =
  1. | Ddata of (Ident.ident * ty list) list
  2. | Drecord of (is_mutable * Ident.ident * ty) list
  3. | Dalias of ty
  4. | Drange of Number.int_range
  5. | Dfloat of Number.float_format
type its_defn = {
  1. its_name : Ident.ident;
  2. its_args : Ty.tvsymbol list;
  3. its_private : bool;
  4. its_def : typedef option;
}
type decl =
  1. | Dtype of its_defn list
  2. | Dlet of let_def
  3. | Dval of Ity.pvsymbol * ty
  4. | Dexn of Ity.xsymbol * ty option
  5. | Dmodule of string * decl list
type namespace = (Ident.ident * decl list) list
type from_module = {
  1. from_mod : Pmodule.pmodule option;
  2. from_km : Pdecl.known_map;
}
type known_map = decl Ident.Mid.t
type pmodule = {
  1. mod_from : from_module;
  2. mod_decl : decl list;
  3. 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 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 dummy_expr_attr : Ident.attribute
val e_dummy_unit : expr
val e_unit : expr
val var_defn : Ity.pvsymbol -> expr -> let_def
val sym_defn : Expr.rsymbol -> Ty.Stv.t -> 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_match : expr -> reg_branch list -> exn_branch list -> ity -> Ity.mask -> Ity.effect -> Ident.Sattr.t -> expr
val e_assign : (Ity.pvsymbol * Expr.rsymbol * expr) 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
val ld_map : (expr -> expr) -> let_def -> let_def
val e_map : (expr -> expr) -> expr -> expr
val ld_fold : ('a -> expr -> 'a) -> 'a -> let_def -> 'a
val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a
val ld_map_fold : ('a -> expr -> 'a * expr) -> 'a -> let_def -> 'a * let_def
val e_map_fold : ('a -> expr -> 'a * expr) -> 'a -> expr -> 'a * expr
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