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 |
| |
Is_getter of |
| |
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 and priority | *) |
| |
Pp_ty of |
(* | ty * prio * q | *) |
| |
Pp_decl of |
(* |
| *) |
| |
Pp_ts of |
(* | Print tysymbol | *) |
| |
Pp_ls of |
(* | Print lsymbol | *) |
| |
Pp_id of |
(* | Print ident | *) |
| |
Pp_cs of |
(* | Print constructors | *) |
| |
Pp_vs of |
(* | Print vsymbol | *) |
| |
Pp_trigger of |
(* | Print triggers | *) |
| |
Pp_forget of |
(* | 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.