why3 1.3.0 · OCaml Package

type its_defn = private {

itd_its : Ity.itysymbol;
itd_fields : Expr.rsymbol list;
itd_constructors : Expr.rsymbol list;
itd_invariant : Term.term list;
itd_witness : Expr.expr list;

}

val create_plain_record_decl : 
  priv:bool ->
  mut:bool ->
  Ident.preid ->
  Ty.tvsymbol list ->
  (bool * Ity.pvsymbol) list ->
  Term.term list ->
  Expr.expr list ->
  its_defn

val create_rec_record_decl : Ity.itysymbol -> Ity.pvsymbol list -> its_defn

val create_plain_variant_decl : 
  Ident.preid ->
  Ty.tvsymbol list ->
  (Ident.preid * (bool * Ity.pvsymbol) list) list ->
  its_defn

val create_rec_variant_decl : 
  Ity.itysymbol ->
  (Ident.preid * (bool * Ity.pvsymbol) list) list ->
  its_defn

val create_alias_decl : Ident.preid -> Ty.tvsymbol list -> Ity.ity -> its_defn

val create_range_decl : Ident.preid -> Number.int_range -> its_defn

val create_float_decl : Ident.preid -> Number.float_format -> its_defn

type pdecl = private {

pd_node : pdecl_node;
pd_pure : Decl.decl list;
pd_meta : meta_decl list;
pd_syms : Ident.Sid.t;
pd_news : Ident.Sid.t;
pd_tag : int;

}

and pdecl_node = private

| PDtype of its_defn list
| PDlet of Expr.let_defn
| PDexn of Ity.xsymbol
| PDpure

and meta_decl = Theory.meta * Theory.meta_arg list

val axiom_of_invariant : its_defn -> Term.term

val create_type_decl : its_defn list -> pdecl list

val create_let_decl : Expr.let_defn -> pdecl

val create_exn_decl : Ity.xsymbol -> pdecl

val create_pure_decl : Decl.decl -> pdecl

val pd_int : pdecl

val pd_real : pdecl

val pd_equ : pdecl

val pd_bool : pdecl

val pd_str : pdecl

val pd_tuple : int -> pdecl

val pd_func : pdecl

val pd_func_app : pdecl

type known_map = pdecl Ident.Mid.t

val known_id : known_map -> Ident.ident -> unit

val known_add_decl : known_map -> pdecl -> known_map

val merge_known : known_map -> known_map -> known_map

val find_its_defn : known_map -> Ity.itysymbol -> its_defn

val print_pdecl : Format.formatter -> pdecl -> unit

package why3