Module Pretty

module Pretty: sig .. end

Pretty-printing various objects from Why3's core logic


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 -> syntax
module type Printer = sig .. end
include Pretty.Printer
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:(any_pp Pp.pp -> any_pp Pp.pp) ->
Ident.ident_printer ->
Ident.ident_printer ->
Ident.ident_printer -> Ident.ident_printer -> bool -> (module Pretty.Printer)

`create spr apr tpr ppr forget` creates a new pretty-printing module from the printer `spr` for variables and functions, `apr` for type variables, `tpr` for type symbols and `ppr for proposition names`. When the Boolean `forget` is true then all recorded names are forgotten between printing of each tasks.