package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module PpSource

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 =
  1. | Pp_hbox
  2. | Pp_vbox of int
  3. | Pp_hvbox of int
  4. | Pp_hovbox of int
Sourcetype doc_view =
  1. | Ppcmd_empty
  2. | Ppcmd_string of string
  3. | Ppcmd_glue of t list
  4. | Ppcmd_box of block_type * t
  5. | Ppcmd_tag of pp_tag * t
  6. | Ppcmd_print_break of int * int
  7. | Ppcmd_force_newline
  8. | 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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct