why3 1.0.0 · OCaml Package

val black_list : string list

val fresh_printer : unit -> Ident.ident_printer

val iprinter : Ident.ident_printer

val forget_all : unit -> unit

val tv_set : Ident.Sid.t ref

val thprinter : Ident.ident_printer

val print_tv : Format.formatter -> Ty.tvsymbol -> unit

val print_tv_binder : Format.formatter -> Ty.tvsymbol -> unit

val print_params_list : Format.formatter -> Ty.tvsymbol list -> unit

val print_params : Format.formatter -> Ty.Stv.t -> unit

val forget_tvs : unit -> unit

val print_vs : Format.formatter -> Term.vsymbol -> unit

val forget_var : Term.vsymbol -> unit

val print_ts : Format.formatter -> Ty.tysymbol -> unit

val print_ls : Format.formatter -> Term.lsymbol -> unit

val print_pr : Format.formatter -> Decl.prsymbol -> unit

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

val get_th_name : Ident.ident -> string

type info = {

info_syn : Printer.syntax_map;
symbol_printers : (string * Theory.theory * Ident.ident_printer) Ident.Mid.t;
realization : bool;

}

val print_path : string list Pp.pp

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

val print_id_real : info -> Format.formatter -> Ident.Mid.key -> unit

val print_ls_real : info -> Format.formatter -> Term.lsymbol -> unit

val print_ts_real : info -> Format.formatter -> Ty.tysymbol -> unit

val print_pr_real : info -> Format.formatter -> Decl.prsymbol -> unit

val print_ty : info -> Ty.ty Pp.pp

val unambig_fs : Term.lsymbol -> bool

val lparen_l : Format.formatter -> unit -> unit

val lparen_r : Format.formatter -> unit -> unit

val print_paren_l : 'a Pp.pp -> Format.formatter -> 'a list -> unit

val print_paren_r : 'a Pp.pp -> Format.formatter -> 'a list -> unit

val arrow : Format.formatter -> unit -> unit

val print_arrow_list : 'a Pp.pp -> Format.formatter -> 'a list -> unit

val print_space_list : 'a Pp.pp -> Format.formatter -> 'a list -> unit

val print_comma_list : 'a Pp.pp -> Format.formatter -> 'a list -> unit

val print_or_list : 'a Pp.pp -> Format.formatter -> 'a list -> unit

val comma_newline : Format.formatter -> unit -> unit

val print_pat : info -> Term.pattern Pp.pp

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

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

val is_tuple0_ty : Ty.ty option -> bool

val is_tuple_ty : Ty.ty option -> bool

val print_binop : Format.formatter -> Term.binop -> unit

val print_attr : 'a -> ('b * 'c) -> unit

val protect_on : 
  bool ->
  ('a, 'b, 'c, 'd, 'e, 'f) format6 ->
  ('a, 'b, 'c, 'd, 'e, 'f) format6

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

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

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

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

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

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

val print_lrterm : 
  bool ->
  bool ->
  info ->
  Format.formatter ->
  Term.term ->
  unit

val print_lrfmla : 
  bool ->
  bool ->
  info ->
  Format.formatter ->
  Term.term ->
  unit

val print_tnode : bool -> bool -> info -> Format.formatter -> Term.term -> unit

val print_fnode : bool -> bool -> info -> Format.formatter -> Term.term -> unit

val print_tuple_pat : 
  info ->
  Term.term ->
  Format.formatter ->
  Term.pattern ->
  unit

val print_branch : 
  (info -> Format.formatter -> Term.term -> unit) ->
  info ->
  Format.formatter ->
  Term.term_branch ->
  unit

val print_branches : 
  ?first:bool ->
  (info -> Term.term Pp.pp) ->
  info ->
  Format.formatter ->
  Term.term_branch list ->
  unit

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

val print_constr : 
  info ->
  'a ->
  Format.formatter ->
  (Term.lsymbol * 'b) ->
  unit

val ls_ty_vars : Term.lsymbol -> Ty.Stv.t * Ty.Stv.t * Ty.Stv.t

val clean_line : string -> string

type contents = string list

type chunk =

| Edition of string * contents
| Other of contents

val re_blank : Str.regexp

val re_why3 : Str.regexp

val read_old_script : in_channel -> chunk list

val print_contents : Format.formatter -> string list -> unit

val output_till_statement : 
  Format.formatter ->
  chunk list ref ->
  string ->
  chunk option

val print_contents_in_comment : Format.formatter -> string list -> unit

val output_remaining : Format.formatter -> chunk list -> unit

val print_user_def : Format.formatter -> string list -> unit

val realization : Format.formatter -> info -> chunk option -> unit

val print_type_decl : 
  prev:chunk option ->
  info ->
  Format.formatter ->
  Ty.tysymbol ->
  unit

val print_data_decl : 
  info ->
  Format.formatter ->
  (Ty.tysymbol * (Term.lsymbol * 'a) list) ->
  unit

val print_ls_type : info -> Format.formatter -> Ty.ty option -> unit

val create_argument : Ty.ty -> Term.vsymbol

val print_arguments : info -> Format.formatter -> Term.vsymbol list -> unit

val re_macro : Str.regexp

val has_macro : string -> bool

val is_macro : info -> Format.formatter -> chunk option -> unit

val print_param_decl : 
  prev:chunk option ->
  info ->
  Format.formatter ->
  Term.lsymbol ->
  unit

val print_logic_decl : 
  prev:'a ->
  info ->
  Format.formatter ->
  (Term.lsymbol * Decl.ls_defn) ->
  unit

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

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

val print_ind_decl : 
  info ->
  Format.formatter ->
  (Term.lsymbol * ('a * Term.term) list) ->
  unit

val re_lemma : Str.regexp

val find_lemma : string list -> string

val axiom_or_lemma : chunk option -> string

val print_prop_decl : 
  prev:'a ->
  info ->
  Format.formatter ->
  (Decl.prop_kind * Decl.prsymbol * Term.term) ->
  unit

val print_decl : 
  old:chunk list ref ->
  info ->
  Format.formatter ->
  Decl.decl ->
  unit

val print_decls : 
  old:chunk list ref ->
  info ->
  Format.formatter ->
  Decl.decl list ->
  unit

val init_printer : Theory.theory -> Ident.ident_printer

val print_task : 
  Printer.printer_args ->
  bool ->
  ?old:in_channel ->
  Format.formatter ->
  Task.task ->
  unit

val print_task_full : 
  Printer.printer_args ->
  ?old:in_channel ->
  Format.formatter ->
  Task.task ->
  unit

val print_task_real : 
  Printer.printer_args ->
  ?old:in_channel ->
  Format.formatter ->
  Task.task ->
  unit

package why3