diff options
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 226 |
1 files changed, 119 insertions, 107 deletions
@@ -1,179 +1,191 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) -(** Pretty-printers. *) - -type std_ppcmds - -(** {6 Formatting commands} *) - -val str : string -> std_ppcmds -val stras : int * string -> std_ppcmds -val brk : int * int -> std_ppcmds -val tbrk : int * int -> std_ppcmds -val tab : unit -> std_ppcmds -val fnl : unit -> std_ppcmds -val pifb : unit -> std_ppcmds -val ws : int -> std_ppcmds -val mt : unit -> std_ppcmds -val ismt : std_ppcmds -> bool - -val comment : string list -> std_ppcmds - -(** {6 Manipulation commands} *) +(** 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 againt 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")` *) +(* *) +(************************************************************************) -val app : std_ppcmds -> std_ppcmds -> std_ppcmds -(** Concatenation. *) +(* XXX: Improve and add attributes *) +type pp_tag = string -val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds -(** Infix alias for [app]. *) +(* Following discussion on #390, we play on the safe side and make the + internal representation opaque here. *) +type t -val eval_ppcmds : std_ppcmds -> std_ppcmds -(** Force computation. *) +type std_ppcmds = t +[@@ocaml.deprecated "alias of Pp.t"] -val is_empty : std_ppcmds -> bool -(** Test emptyness. *) +type block_type = + | Pp_hbox of int + | Pp_vbox of int + | Pp_hvbox of int + | Pp_hovbox of int -(** {6 Derived commands} *) +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 + (* Are those redundant? *) + | Ppcmd_print_break of int * int + | Ppcmd_force_newline + | Ppcmd_comment of string list -val spc : unit -> std_ppcmds -val cut : unit -> std_ppcmds -val align : unit -> std_ppcmds -val int : int -> std_ppcmds -val real : float -> std_ppcmds -val bool : bool -> std_ppcmds -val qstring : string -> std_ppcmds -val qs : string -> std_ppcmds -val quote : std_ppcmds -> std_ppcmds -val strbrk : string -> std_ppcmds +val repr : t -> doc_view +val unrepr : doc_view -> t -(** {6 Boxing commands} *) +(** {6 Formatting commands} *) -val h : int -> std_ppcmds -> std_ppcmds -val v : int -> std_ppcmds -> std_ppcmds -val hv : int -> std_ppcmds -> std_ppcmds -val hov : int -> std_ppcmds -> std_ppcmds -val t : std_ppcmds -> std_ppcmds +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 -(** {6 Opening and closing of boxes} *) +val comment : string list -> t -val hb : int -> std_ppcmds -val vb : int -> std_ppcmds -val hvb : int -> std_ppcmds -val hovb : int -> std_ppcmds -val tb : unit -> std_ppcmds -val close : unit -> std_ppcmds -val tclose : unit -> std_ppcmds +(** {6 Manipulation commands} *) -(** {6 Opening and closing of tags} *) +val app : t -> t -> t +(** Concatenation. *) -module Tag : -sig - type t - (** Type of tags. Tags are dynamic types comparable to {Dyn.t}. *) +val seq : t list -> t +(** Multi-Concatenation. *) - type 'a key - (** Keys used to inject tags *) +val (++) : t -> t -> t +(** Infix alias for [app]. *) - val create : string -> 'a key - (** Create a key with the given name. Two keys cannot share the same name, if - ever this is the case this function raises an assertion failure. *) +(** {6 Derived commands} *) - val inj : 'a -> 'a key -> t - (** Inject an object into a tag. *) +val spc : unit -> t +val cut : unit -> t +val align : unit -> t +val int : int -> 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 - val prj : t -> 'a key -> 'a option - (** Project an object from a tag. *) -end +(** {6 Boxing commands} *) -val tag : Tag.t -> std_ppcmds -> std_ppcmds -val open_tag : Tag.t -> std_ppcmds -val close_tag : unit -> std_ppcmds +val h : int -> t -> t +val v : int -> t -> t +val hv : int -> t -> t +val hov : int -> t -> t -(** {6 Utilities} *) +(** {6 Tagging} *) -val string_of_ppcmds : std_ppcmds -> string +val tag : pp_tag -> t -> t (** {6 Printing combinators} *) -val pr_comma : unit -> std_ppcmds +val pr_comma : unit -> t (** Well-spaced comma. *) -val pr_semicolon : unit -> std_ppcmds +val pr_semicolon : unit -> t (** Well-spaced semicolon. *) -val pr_bar : unit -> std_ppcmds +val pr_bar : unit -> t (** Well-spaced pipe bar. *) -val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds +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 -> std_ppcmds) -> 'a -> std_ppcmds +val pr_non_empty_arg : ('a -> t) -> 'a -> t (** Adds a space in front of its argument if non empty. *) -val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds +val pr_opt : ('a -> t) -> 'a option -> t (** Inner object preceded with a space if [Some], nothing otherwise. *) -val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds +val pr_opt_no_spc : ('a -> t) -> 'a option -> t (** Same as [pr_opt] but without the leading space. *) -val pr_nth : int -> std_ppcmds +val pr_nth : int -> t (** Ordinal number with the correct suffix (i.e. "st", "nd", "th", etc.). *) -val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +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 -> std_ppcmds) -> 'a list -> std_ppcmds +val prlist_strict : ('a -> t) -> 'a list -> t (** Same as [prlist], but strict. *) val prlist_with_sep : - (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a list -> std_ppcmds + (unit -> t) -> ('a -> t) -> 'a list -> t (** [prlist_with_sep sep pr [a ; ... ; c]] outputs - [pr a ++ sep() ++ ... ++ sep() ++ pr c]. *) + [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 -> std_ppcmds) -> 'a array -> std_ppcmds +val prvect : ('a -> t) -> 'a array -> t (** As [prlist], but on arrays. *) -val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds +val prvecti : (int -> 'a -> t) -> 'a array -> t (** Indexed version of [prvect]. *) val prvect_with_sep : - (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds + (unit -> t) -> ('a -> t) -> 'a array -> t (** As [prlist_with_sep], but on arrays. *) val prvecti_with_sep : - (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds + (unit -> t) -> (int -> 'a -> t) -> 'a array -> t (** Indexed version of [prvect_with_sep]. *) -val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val pr_enum : ('a -> t) -> 'a list -> t (** [pr_enum pr [a ; b ; ... ; c]] outputs [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c]. *) -val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val pr_sequence : ('a -> t) -> 'a list -> t (** Sequence of objects separated by space (unless an element is empty). *) -val surround : std_ppcmds -> std_ppcmds +val surround : t -> t (** Surround with parenthesis. *) -val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds - -val pr_loc : Loc.t -> std_ppcmds - -(** {6 Low-level pretty-printing functions with and without flush} *) +val pr_vertical_list : ('b -> t) -> 'b list -> t -(** FIXME: These ignore the logging settings and call [Format] directly *) -type tag_handler = Tag.t -> Format.tag +(** {6 Main renderers, to formatter and to string } *) -(** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and flush [fmt] *) -val msg_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit +(** [pp_with fmt pp] Print [pp] to [fmt] and don't flush [fmt] *) +val pp_with : Format.formatter -> t -> unit -(** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and don't flush [fmt] *) -val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit +val string_of_ppcmds : t -> string |