why3 1.0.0 · OCaml Package

type pattern =

| PatHole of int
| PatApp of Env.pathname * string * string list * pattern list

val incremental_pat_match : 
  Env.env ->
  Term.term option array ->
  pattern ->
  Term.term ->
  unit

val pat_match : Env.env -> int -> pattern -> Term.term -> Term.term array

type info = {

info_env : Env.env;
info_symbols : Ident.Sid.t;
info_ops_of_rel : (string * string * string) Term.Mls.t;
info_syn : Printer.syntax_map;

}

val int_minus : Term.lsymbol ref

val real_minus : Term.lsymbol ref

val arith_meta : Theory.meta

val find_th : Env.env -> string -> string -> string -> Term.lsymbol

val get_info : Env.env -> Task.task -> info

val ident_printer : Ident.ident_printer

val print_ident : Format.formatter -> Ident.ident -> unit

val print_const : Format.formatter -> Number.constant -> unit

val constant_value : Term.term -> string

val rel_error_pat : pattern

val print_term : info -> Term.term Pp.pp

val print_fmla : info -> Format.formatter -> Term.term -> unit

exception AlreadyDefined

val is_number : Ty.ty_node -> bool

val filter_logic : 
  info ->
  ('a * (Term.lsymbol * 'b) list * (Term.lsymbol * 'b) list * 'c) ->
  (Term.lsymbol * 'b) ->
  'a * (Term.lsymbol * 'b) list * (Term.lsymbol * 'b) list * 'c

val filter_hyp : 
  'a ->
  Term.lsymbol list ->
  unit Ident.Hid.t ->
  ('b * Term.term * Term.term) list ->
  ('b * Term.term) list ->
  'b ->
  Term.term ->
  Term.lsymbol list * ('b * Term.term * Term.term) list * ('b * Term.term) list

type filter_goal =

| Goal_good of Decl.prsymbol * Term.term
| Goal_bad of string
| Goal_none

val filter_goal : Decl.prsymbol -> Term.term -> filter_goal

val prepare : 
  info ->
  unit Ident.Hid.t ->
  (Term.lsymbol list
   * (Term.lsymbol * Decl.ls_defn) list
   * (Term.lsymbol * Decl.ls_defn) list
   * (Decl.prsymbol * Term.term * Term.term) list
   * (Decl.prsymbol * Term.term) list
   * filter_goal
   * 'a) ->
  Decl.decl ->
  Term.lsymbol list
  * (Term.lsymbol * Decl.ls_defn) list
  * (Term.lsymbol * Decl.ls_defn) list
  * (Decl.prsymbol * Term.term * Term.term) list
  * (Decl.prsymbol * Term.term) list
  * filter_goal
  * 'a

val print_equation : 
  info ->
  Format.formatter ->
  (Decl.prsymbol * Term.term * Term.term) ->
  unit

val print_logic_binder : 'a -> Format.formatter -> Term.vsymbol -> unit

val print_fun_def : 
  info ->
  Format.formatter ->
  (Term.lsymbol * Decl.ls_defn) ->
  unit

val print_pred_def : 
  info ->
  Format.formatter ->
  (Term.lsymbol * Decl.ls_defn) ->
  unit

val print_type_def : 'a -> Format.formatter -> (Ty.tysymbol * 'b list) -> unit

val print_hyp : info -> Format.formatter -> (Decl.prsymbol * Term.term) -> unit

val is_integer : Ty.ty_node -> bool

val print_dom : 'a -> Format.formatter -> Term.lsymbol -> unit

val print_param : 'a -> Format.formatter -> Term.lsymbol -> unit

val print_var : info -> Format.formatter -> Term.vsymbol -> unit

val print_goal : info -> Format.formatter -> filter_goal -> unit

val print_task : 
  Printer.printer_args ->
  ?old:'a ->
  Format.formatter ->
  Task.task ->
  unit

package why3