Module `Pp`Source

Coq document type.

Pretty printing guidelines

Pp.t is the main pretty printing document type in the Coq system. Documents are composed laying out boxes, and users can add arbitrary tag metadata that backends are free to interpret.

The datatype has a public view to allow serialization or advanced uses, however regular users are _strongly_ warned against its use, they should instead rely on the available functions below.

Box order and number is indeed an important factor. Try to create a proper amount of boxes. The ++ operator provides "efficient" concatenation, but using the list constructors is usually preferred.

That is to say, this:

hov [str "Term"; hov (pr_term t); str "is defined"]

is preferred to:

hov (str "Term" ++ hov (pr_term t) ++ str "is defined")

Sourcetype pp_tag = string

Sourcetype t

Sourcetype block_type =

| Pp_hbox
| Pp_vbox of int
| Pp_hvbox of int
| Pp_hovbox of int

Sourcetype doc_view =

| Ppcmd_empty
| Ppcmd_string of string
| Ppcmd_glue of t list
| Ppcmd_box of block_type * t
| Ppcmd_tag of pp_tag * t
| Ppcmd_print_break of int * int
| Ppcmd_force_newline
| Ppcmd_comment of string list

Sourceval repr : t -> doc_view

Sourceval unrepr : doc_view -> t

Formatting commands

Sourceval str : string -> t

Sourceval brk : (int * int) -> t

Sourceval fnl : unit -> t

Sourceval ws : int -> t

Sourceval mt : unit -> t

Sourceval ismt : t -> bool

Sourceval comment : string list -> t

Manipulation commands

Sourceval app : t -> t -> t

Concatenation.

Sourceval seq : t list -> t

Multi-Concatenation.

Sourceval (++) : t -> t -> t

Infix alias for app.

Derived commands

Sourceval spc : unit -> t

Sourceval cut : unit -> t

Sourceval align : unit -> t

Sourceval int : int -> t

Sourceval real : float -> t

Sourceval bool : bool -> t

Sourceval qstring : string -> t

Sourceval qs : string -> t

Sourceval quote : t -> t

Sourceval strbrk : string -> t

Boxing commands

Sourceval h : t -> t

Sourceval v : int -> t -> t

Sourceval hv : int -> t -> t

Sourceval hov : int -> t -> t

Tagging

Sourceval tag : pp_tag -> t -> t

Printing combinators

Sourceval pr_comma : unit -> t

Well-spaced comma.

Sourceval pr_semicolon : unit -> t

Well-spaced semicolon.

Sourceval pr_bar : unit -> t

Well-spaced pipe bar.

Sourceval pr_spcbar : unit -> t

Pipe bar with space before and after.

Sourceval pr_arg : ('a -> t) -> 'a -> t

Adds a space in front of its argument.

Sourceval pr_non_empty_arg : ('a -> t) -> 'a -> t

Adds a space in front of its argument if non empty.

Sourceval pr_opt : ('a -> t) -> 'a option -> t

Inner object preceded with a space if Some, nothing otherwise.

Sourceval pr_opt_no_spc : ('a -> t) -> 'a option -> t

Same as pr_opt but without the leading space.

Sourceval pr_opt_default : (unit -> t) -> ('a -> t) -> 'a option -> t

Prints pr v if ov is Some v, else prdf ().

Sourceval pr_opt_no_spc_default : (unit -> t) -> ('a -> t) -> 'a option -> t

Same as pr_opt_default but without the leading space.

Sourceval pr_nth : int -> t

Ordinal number with the correct suffix (i.e. "st", "nd", "th", etc.).

Sourceval prlist : ('a -> t) -> 'a list -> t

Concatenation of the list contents, without any separator.

Unlike all other functions below, prlist works lazily. If a strict behavior is needed, use prlist_strict instead.

Sourceval prlist_strict : ('a -> t) -> 'a list -> t

Same as prlist, but strict.

Sourceval prlist_with_sep : (unit -> t) -> ('a -> t) -> 'a list -> t

prlist_with_sep sep pr [a ; ... ; c] outputs pr a ++ sep () ++ ... ++ sep () ++ pr c. where the thunk sep is memoized, rather than being called each place its result is used.

Sourceval prvect : ('a -> t) -> 'a array -> t

As prlist, but on arrays.

Sourceval prvecti : (int -> 'a -> t) -> 'a array -> t

Indexed version of prvect.

Sourceval prvect_with_sep : (unit -> t) -> ('a -> t) -> 'a array -> t

As prlist_with_sep, but on arrays.

Sourceval prvecti_with_sep : (unit -> t) -> (int -> 'a -> t) -> 'a array -> t

Indexed version of prvect_with_sep.

Sourceval pr_enum : ('a -> t) -> 'a list -> t

pr_enum pr [a ; b ; ... ; c] outputs pr a ++ str "," ++ spc () ++ pr b ++ str "," ++ spc () ++ ... ++ str "and" ++ spc () ++ pr c.

Sourceval pr_choice : ('a -> t) -> 'a list -> t

pr_choice pr [a ; b ; ... ; c] outputs pr a ++ str "," ++ spc () ++ pr b ++ str "," ++ spc () ++ ... ++ str "or" ++ spc () ++ pr c.

Sourceval pr_sequence : ('a -> t) -> 'a list -> t

Sequence of objects separated by space (unless an element is empty).

Sourceval surround : t -> t

Surround with parenthesis.

Sourceval pr_vertical_list : ('b -> t) -> 'b list -> t

Main renderers, to formatter and to string

Sourceval pp_with : Format.formatter -> t -> unit

pp_with fmt pp Print pp to fmt and don't flush fmt

Sourceval string_of_ppcmds : t -> string

Sourceval start_pfx : string

Tag prefix to start a multi-token diff span

Sourceval end_pfx : string

Tag prefix to end a multi-token diff span

Sourceval split_tag : string -> string * string

Split a tag into prefix and base tag

Sourceval db_print_pp : Format.formatter -> t -> unit

Print the Pp in tree form for debugging

Sourceval db_string_of_pp : t -> string

Print the Pp in tree form for debugging, return as a string

Sourceval flatten : t -> t

Combine nested Ppcmd_glues

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.lib/Pp/index.html

Module `Pp`Source

Pretty printing guidelines

Formatting commands

Manipulation commands

Derived commands

Boxing commands

Tagging

Printing combinators

Main renderers, to formatter and to string

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.lib/Pp/index.html

Module PpSource

Pretty printing guidelines

Formatting commands

Manipulation commands

Derived commands

Boxing commands

Tagging

Printing combinators

Main renderers, to formatter and to string

Module `Pp`Source