sig
val coercion_attr : Ident.attribute
val why3_keywords : string list
val prio_binop : Term.binop -> int
val protect_on :
bool ->
('a, 'b, 'c, 'd, 'e, 'f) Stdlib.format6 ->
('a, 'b, 'c, 'd, 'e, 'f) Stdlib.format6
type syntax = Is_array of string | Is_getter of string | Is_none
val get_element_syntax : attrs:Ident.Sattr.t -> Pretty.syntax
module type Printer =
sig
val tprinter : Ident.ident_printer
val aprinter : Ident.ident_printer
val sprinter : Ident.ident_printer
val pprinter : Ident.ident_printer
val forget_all : unit -> unit
val forget_tvs : unit -> unit
val forget_var : Term.vsymbol -> unit
val print_id_attrs : Ident.ident Pp.pp
val print_tv : Ty.tvsymbol Pp.pp
val print_vs : Term.vsymbol Pp.pp
val print_ts : Ty.tysymbol Pp.pp
val print_ls : Term.lsymbol Pp.pp
val print_cs : Term.lsymbol Pp.pp
val print_pr : Decl.prsymbol Pp.pp
val print_th : Theory.theory Pp.pp
val print_ty : Ty.ty Pp.pp
val print_vsty : Term.vsymbol Pp.pp
val print_ts_qualified : Ty.tysymbol Pp.pp
val print_ls_qualified : Term.lsymbol Pp.pp
val print_cs_qualified : Term.lsymbol Pp.pp
val print_pr_qualified : Decl.prsymbol Pp.pp
val print_th_qualified : Theory.theory Pp.pp
val print_ty_qualified : Ty.ty Pp.pp
val print_vs_qualified : Term.vsymbol Pp.pp
val print_tv_qualified : Ty.tvsymbol Pp.pp
val print_quant : Term.quant Pp.pp
val print_binop : asym:bool -> Term.binop Pp.pp
val print_pat : Term.pattern Pp.pp
val print_term : Term.term Pp.pp
val print_attr : Ident.attribute Pp.pp
val print_attrs : Ident.Sattr.t Pp.pp
val print_loc_as_attribute : Loc.position Pp.pp
val print_pkind : Decl.prop_kind Pp.pp
val print_meta_arg : Theory.meta_arg Pp.pp
val print_meta_arg_type : Theory.meta_arg_type Pp.pp
val print_ty_decl : Ty.tysymbol Pp.pp
val print_data_decl : Decl.data_decl Pp.pp
val print_param_decl : Term.lsymbol Pp.pp
val print_logic_decl : Decl.logic_decl Pp.pp
val print_ind_decl : Decl.ind_sign -> Decl.ind_decl Pp.pp
val print_next_data_decl : Decl.data_decl Pp.pp
val print_next_logic_decl : Decl.logic_decl Pp.pp
val print_next_ind_decl : Decl.ind_decl Pp.pp
val print_prop_decl : Decl.prop_decl Pp.pp
val print_decl : Decl.decl Pp.pp
val print_tdecl : Theory.tdecl Pp.pp
val print_task : Task.task Pp.pp
val print_sequent : Task.task Pp.pp
val print_theory : Theory.theory Pp.pp
val print_namespace : string -> Theory.theory Pp.pp
end
val tprinter : Ident.ident_printer
val aprinter : Ident.ident_printer
val sprinter : Ident.ident_printer
val pprinter : Ident.ident_printer
val forget_all : unit -> unit
val forget_tvs : unit -> unit
val forget_var : Term.vsymbol -> unit
val print_id_attrs : Ident.ident Pp.pp
val print_tv : Ty.tvsymbol Pp.pp
val print_vs : Term.vsymbol Pp.pp
val print_ts : Ty.tysymbol Pp.pp
val print_ls : Term.lsymbol Pp.pp
val print_cs : Term.lsymbol Pp.pp
val print_pr : Decl.prsymbol Pp.pp
val print_th : Theory.theory Pp.pp
val print_ty : Ty.ty Pp.pp
val print_vsty : Term.vsymbol Pp.pp
val print_ts_qualified : Ty.tysymbol Pp.pp
val print_ls_qualified : Term.lsymbol Pp.pp
val print_cs_qualified : Term.lsymbol Pp.pp
val print_pr_qualified : Decl.prsymbol Pp.pp
val print_th_qualified : Theory.theory Pp.pp
val print_ty_qualified : Ty.ty Pp.pp
val print_vs_qualified : Term.vsymbol Pp.pp
val print_tv_qualified : Ty.tvsymbol Pp.pp
val print_quant : Term.quant Pp.pp
val print_binop : asym:bool -> Term.binop Pp.pp
val print_pat : Term.pattern Pp.pp
val print_term : Term.term Pp.pp
val print_attr : Ident.attribute Pp.pp
val print_attrs : Ident.Sattr.t Pp.pp
val print_loc_as_attribute : Loc.position Pp.pp
val print_pkind : Decl.prop_kind Pp.pp
val print_meta_arg : Theory.meta_arg Pp.pp
val print_meta_arg_type : Theory.meta_arg_type Pp.pp
val print_ty_decl : Ty.tysymbol Pp.pp
val print_data_decl : Decl.data_decl Pp.pp
val print_param_decl : Term.lsymbol Pp.pp
val print_logic_decl : Decl.logic_decl Pp.pp
val print_ind_decl : Decl.ind_sign -> Decl.ind_decl Pp.pp
val print_next_data_decl : Decl.data_decl Pp.pp
val print_next_logic_decl : Decl.logic_decl Pp.pp
val print_next_ind_decl : Decl.ind_decl Pp.pp
val print_prop_decl : Decl.prop_decl Pp.pp
val print_decl : Decl.decl Pp.pp
val print_tdecl : Theory.tdecl Pp.pp
val print_task : Task.task Pp.pp
val print_sequent : Task.task Pp.pp
val print_theory : Theory.theory Pp.pp
val print_namespace : string -> Theory.theory Pp.pp
type any_pp =
Pp_term of (Term.term * int)
| Pp_ty of (Ty.ty * int * bool)
| Pp_decl of
(bool * Ty.tysymbol * (Term.lsymbol * Term.lsymbol option list) list)
| Pp_ts of Ty.tysymbol
| Pp_ls of Term.lsymbol
| Pp_id of Ident.ident
| Pp_cs of Term.lsymbol
| Pp_vs of Term.vsymbol
| Pp_trigger of Term.trigger
| Pp_forget of Term.vsymbol list
| Pp_forget_tvs
val create :
?print_ext_any:(Pretty.any_pp Pp.pp -> Pretty.any_pp Pp.pp) ->
?do_forget_all:bool ->
?shorten_axioms:bool ->
?show_uses_clones_metas:bool ->
Ident.ident_printer ->
Ident.ident_printer ->
Ident.ident_printer -> Ident.ident_printer -> (module Pretty.Printer)
end