Module Pretty

module Pretty: sig .. end

Pretty-printing various objects from Why3's core logic

val coercion_attr : Ident.attribute

Attribute to put on unary functions to make them considered as coercions, hence not printed by default.

val why3_keywords : string list

the list of all WhyML keywords.

val prio_binop : Term.binop -> int

priorities of each binary operators

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

add parentheses around when first arugment is true.

type syntax = 
| Is_array of string
| Is_getter of string
| Is_none

specific syntax

val get_element_syntax : attrs:Ident.Sattr.t -> syntax

Module type for printers

module type Printer = sig .. end

The default printer

include Pretty.Printer

Extended pretty-printers

type any_pp = 
| Pp_term of (Term.term * int) (*

Term and priority

*)
| Pp_ty of (Ty.ty * int * bool) (*

ty * prio * q

*)
| Pp_decl of (bool * Ty.tysymbol * (Term.lsymbol * Term.lsymbol option list) list) (*

Pp_decl (fst, ts, csl): Declaration of type ts with constructors csl as fst

*)
| Pp_ts of Ty.tysymbol (*

Print tysymbol

*)
| Pp_ls of Term.lsymbol (*

Print lsymbol

*)
| Pp_id of Ident.ident (*

Print ident

*)
| Pp_cs of Term.lsymbol (*

Print constructors

*)
| Pp_vs of Term.vsymbol (*

Print vsymbol

*)
| Pp_trigger of Term.trigger (*

Print triggers

*)
| Pp_forget of Term.vsymbol list (*

Forget all the vsymbols listed

*)
| Pp_forget_tvs (*

execute forget_tvs

*)
val create : ?print_ext_any:(any_pp Pp.pp -> 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)

create spr apr tpr ppr 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. If do_forget_all is true (default), then all recorded names are forgotten between printing of each tasks. If shorten_axioms is false (default), axioms are prefixed by the keyword. If show_uses_clones_metas is true (default), displays in comments the declarations of used and cloned theories, and metas.