Module `Pp`

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")

type pp_tag = string
type t
type block_type = | Pp_hbox | Pp_vbox of int | Pp_hvbox of int | Pp_hovbox of int
type 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

val repr : t -> doc_view
val unrepr : doc_view -> t

Formatting commands

val str : string -> t
val brk : (int * int) -> t
val fnl : unit -> t
val ws : int -> t
val mt : unit -> t
val ismt : t -> bool
val comment : string list -> t

Manipulation commands

val app : t -> t -> t: Concatenation.

val seq : t list -> t: Multi-Concatenation.

val (++) : t -> t -> t: Infix alias for app.

Derived commands

val spc : unit -> t
val cut : unit -> t
val align : unit -> t
val int : int -> t
val int64 : Stdlib.Int64.t -> t
val real : float -> t
val bool : bool -> t
val qstring : string -> t
val qs : string -> t
val quote : t -> t
val strbrk : string -> t

Boxing commands

val h : t -> t
val v : int -> t -> t
val hv : int -> t -> t
val hov : int -> t -> t

Tagging

val tag : pp_tag -> t -> t

Printing combinators

val pr_comma : unit -> t: Well-spaced comma.

val pr_semicolon : unit -> t: Well-spaced semicolon.

val pr_bar : unit -> t: Well-spaced pipe bar.

val pr_spcbar : unit -> t: Pipe bar with space before and after.

val pr_arg : ('a -> t) -> 'a -> t: Adds a space in front of its argument.

val pr_non_empty_arg : ('a -> t) -> 'a -> t: Adds a space in front of its argument if non empty.

val pr_opt : ('a -> t) -> 'a option -> t: Inner object preceded with a space if Some, nothing otherwise.

val pr_opt_no_spc : ('a -> t) -> 'a option -> t: Same as pr_opt but without the leading space.

val pr_opt_default : (unit -> t) -> ('a -> t) -> 'a option -> t: Prints pr v if ov is Some v, else prdf ().

val pr_opt_no_spc_default : (unit -> t) -> ('a -> t) -> 'a option -> t: Same as pr_opt_default but without the leading space.

val pr_nth : int -> t: Ordinal number with the correct suffix (i.e. "st", "nd", "th", etc.).

val 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.

val prlist_strict : ('a -> t) -> 'a list -> t: Same as prlist, but strict.

val 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.

val prvect : ('a -> t) -> 'a array -> t: As prlist, but on arrays.

val prvecti : (int -> 'a -> t) -> 'a array -> t: Indexed version of prvect.

val prvect_with_sep : (unit -> t) -> ('a -> t) -> 'a array -> t: As prlist_with_sep, but on arrays.

val prvecti_with_sep : (unit -> t) -> (int -> 'a -> t) -> 'a array -> t: Indexed version of prvect_with_sep.

val 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.

val 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.

val pr_sequence : ('a -> t) -> 'a list -> t: Sequence of objects separated by space (unless an element is empty).

val surround : t -> t: Surround with parenthesis.

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

Main renderers, to formatter and to string

val pp_with : Stdlib.Format.formatter -> t -> unit: pp_with fmt pp Print pp to fmt and don't flush fmt

val string_of_ppcmds : t -> string
val start_pfx : string: Tag prefix to start a multi-token diff span

val end_pfx : string: Tag prefix to end a multi-token diff span

val split_tag : string -> string * string: Split a tag into prefix and base tag

val db_print_pp : Stdlib.Format.formatter -> t -> unit: Print the Pp in tree form for debugging

val db_string_of_pp : t -> string: Print the Pp in tree form for debugging, return as a string

val flatten : t -> t: Combine nested Ppcmd_glues