1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** Coq document type. *)
(** Pretty printing guidelines ******************************************)
(* *)
(* `Pp.t` or `Pp.std_ppcmds` 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")` *)
(* *)
(************************************************************************)
(* 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 std_ppcmds = t
type block_type =
| Pp_hbox of int
| 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
(* Are those redundant? *)
| Ppcmd_print_break of int * int
| Ppcmd_force_newline
| Ppcmd_comment of string list
val repr : std_ppcmds -> doc_view
val unrepr : doc_view -> std_ppcmds
(** {6 Formatting commands} *)
val str : string -> std_ppcmds
val brk : int * int -> std_ppcmds
val fnl : 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} *)
val app : std_ppcmds -> std_ppcmds -> std_ppcmds
(** Concatenation. *)
val seq : std_ppcmds list -> std_ppcmds
(** Multi-Concatenation. *)
val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
(** Infix alias for [app]. *)
(** {6 Derived commands} *)
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
(** {6 Boxing 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
(** {6 Tagging} *)
val tag : pp_tag -> std_ppcmds -> std_ppcmds
(** {6 Printing combinators} *)
val pr_comma : unit -> std_ppcmds
(** Well-spaced comma. *)
val pr_semicolon : unit -> std_ppcmds
(** Well-spaced semicolon. *)
val pr_bar : unit -> std_ppcmds
(** Well-spaced pipe bar. *)
val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
(** Adds a space in front of its argument. *)
val pr_non_empty_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
(** Adds a space in front of its argument if non empty. *)
val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
(** Inner object preceded with a space if [Some], nothing otherwise. *)
val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
(** Same as [pr_opt] but without the leading space. *)
val pr_nth : int -> std_ppcmds
(** Ordinal number with the correct suffix (i.e. "st", "nd", "th", etc.). *)
val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
(** 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
(** Same as [prlist], but strict. *)
val prlist_with_sep :
(unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a list -> std_ppcmds
(** [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 -> std_ppcmds) -> 'a array -> std_ppcmds
(** As [prlist], but on arrays. *)
val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
(** Indexed version of [prvect]. *)
val prvect_with_sep :
(unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds
(** As [prlist_with_sep], but on arrays. *)
val prvecti_with_sep :
(unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
(** Indexed version of [prvect_with_sep]. *)
val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
(** [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
(** Sequence of objects separated by space (unless an element is empty). *)
val surround : std_ppcmds -> std_ppcmds
(** Surround with parenthesis. *)
val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
(** {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 -> std_ppcmds -> unit
val string_of_ppcmds : std_ppcmds -> string
|
