Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
(** Rocq document type. *)
(**{4 Pretty printing guidelines}
[Pp.t] is the main pretty printing document typein the Rocq system. Documents are composed laying out boxes, andusers can add arbitrary tag metadata that backends are freeto interpret.
The datatype has a public view to allow serialization or advanceduses, 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 createa 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")]*)
(* XXX: Improve and add attributes *)type pp_tag = string
(* Following discussion on #390, we play on the safe side and make the internal representation opaque here. *)type t
type block_type = | Pp_hbox | Pp_vbox of int | Pp_hvbox of int | Pp_hovbox of int(** [Pp_hovbox] produces boxes according to [Format.open_box] not [Format.open_hovbox] *)
type doc_view = | Ppcmd_empty | Ppcmd_string of string | Ppcmd_sized_string of int * string | Ppcmd_glue of t list | Ppcmd_box of block_type * t | Ppcmd_tag of pp_tag * t (* Are those redundant? *) | Ppcmd_print_break of int * int | Ppcmd_force_newline | Ppcmd_comment of string list
val repr : t -> doc_viewval unrepr : doc_view -> t
(** {6 Formatting commands} *)
val str : string -> tval brk : int * int -> tval fnl : unit -> tval ws : int -> tval mt : unit -> tval ismt : t -> bool
val comment : string list -> t
val fmt : ('a, unit, t) format -> 'a(** complex formatting *)
(** {6 Manipulation commands} *)
val app : t -> t -> t(** Concatenation. *)
val seq : t list -> t(** Multi-Concatenation. *)
val (++) : t -> t -> t(** Infix alias for [app]. *)
(** {6 Derived commands} *)
val spc : unit -> tval cut : unit -> tval align : unit -> tval int : int -> tval int64 : Int64.t -> tval real : float -> tval bool : bool -> tval qstring : string -> tval qs : string -> tval quote : t -> tval strbrk : string -> t
(** {6 Boxing commands} *)
val h : t -> tval v : int -> t -> tval hv : int -> t -> tval hov : int -> t -> t(** [hov] produces boxes according to [Format.open_box] not [Format.open_hovbox] *)
(** {6 Tagging} *)
val tag : pp_tag -> t -> t
(** {6 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
(** {6 Main renderers, to formatter and to string } *)
(** [pp_with fmt pp] Print [pp] to [fmt] and don't flush [fmt] *)val pp_with : Format.formatter -> t -> unit
val string_of_ppcmds : t -> string
(** Tag prefix to start a multi-token diff span *)val start_pfx : string
(** Tag prefix to end a multi-token diff span *)val end_pfx : string
(** Split a tag into prefix and base tag *)val split_tag : string -> string * string
(** Print the Pp in tree form for debugging *)val db_print_pp : Format.formatter -> t -> unit
(** Print the Pp in tree form for debugging, return as a string *)val db_string_of_pp : t -> string
(** Returns [fmt, args] such that [fmt] is a format string which applied to [args] produces the same result as [pp_with].
[with_tags] default false. *)val pp_as_format : ?with_tags:bool -> t -> string * string list
(** Combine nested Ppcmd_glues *)val flatten : t -> t