0 | module Text.PrettyPrint.Bernardy.Combinators
  1 |
  2 | import Data.String
  3 | import Text.PrettyPrint.Bernardy.Core
  4 |
  5 | %default total
  6 |
  7 | --------------------------------------------------------------------------------
  8 | --          Symbols
  9 | --------------------------------------------------------------------------------
 10 |
 11 | ||| Creates a single-line document from the given character.
 12 | |||
 13 | ||| @c A printable non-control character.
 14 | export %inline
 15 | symbol : (c : Char) -> Doc opts
 16 | symbol = line . singleton
 17 |
 18 | ||| A single space character.
 19 | export
 20 | space : Doc opts
 21 | space = symbol ' '
 22 |
 23 | export
 24 | squote : Doc opts
 25 | squote = symbol '\''
 26 |
 27 | export
 28 | dquote : Doc opts
 29 | dquote = symbol '"'
 30 |
 31 | export
 32 | lparen : Doc opts
 33 | lparen = symbol '('
 34 |
 35 | export
 36 | rparen : Doc opts
 37 | rparen = symbol ')'
 38 |
 39 | export
 40 | langle : Doc opts
 41 | langle = symbol '<'
 42 |
 43 | export
 44 | rangle : Doc opts
 45 | rangle = symbol '>'
 46 |
 47 | export
 48 | lbracket : Doc opts
 49 | lbracket = symbol '['
 50 |
 51 | export
 52 | rbracket : Doc opts
 53 | rbracket = symbol ']'
 54 |
 55 | export
 56 | lbrace : Doc opts
 57 | lbrace = symbol '{'
 58 |
 59 | export
 60 | rbrace : Doc opts
 61 | rbrace = symbol '}'
 62 |
 63 | export
 64 | semi : Doc opts
 65 | semi = symbol ';'
 66 |
 67 | export
 68 | colon : Doc opts
 69 | colon = symbol ':'
 70 |
 71 | export
 72 | comma : Doc opts
 73 | comma = symbol ','
 74 |
 75 | export
 76 | dot : Doc opts
 77 | dot = symbol '.'
 78 |
 79 | export
 80 | slash : Doc opts
 81 | slash = symbol '/'
 82 |
 83 | export
 84 | backslash : Doc opts
 85 | backslash = symbol '\\'
 86 |
 87 | export
 88 | equals : Doc opts
 89 | equals = symbol '='
 90 |
 91 | export
 92 | pipe : Doc opts
 93 | pipe = symbol '|'
 94 |
 95 | --------------------------------------------------------------------------------
 96 | --          Enclosing Documents
 97 | --------------------------------------------------------------------------------
 98 |
 99 | ||| Encloses the document between two other documents using `(<+>)`.
100 | export
101 | enclose : {opts : _} -> Doc opts -> Doc opts -> Doc opts -> Doc opts
102 | enclose l r x = l <+> x <+> r
103 |
104 | ||| Encolses a document in single quotes.
105 | export
106 | squotes : {opts : _} -> Doc opts -> Doc opts
107 | squotes = enclose squote squote
108 |
109 | ||| Encolses a document in double quotes.
110 | export
111 | dquotes : {opts : _} -> Doc opts -> Doc opts
112 | dquotes = enclose dquote dquote
113 |
114 | ||| Encolses a document in parentheses.
115 | export
116 | parens : {opts : _} -> Doc opts -> Doc opts
117 | parens = enclose lparen rparen
118 |
119 | ||| Encolses a document in parentheses if `b` equals `True`.
120 | export
121 | parenthesise : {opts : _} -> (b : Bool) -> Doc opts -> Doc opts
122 | parenthesise b = if b then parens else id
123 |
124 | ||| Encolses a document in angles (`<` and `>`).
125 | export
126 | angles : {opts : _} -> Doc opts -> Doc opts
127 | angles = enclose langle rangle
128 |
129 | ||| Encolses a document in curly braces.
130 | export
131 | braces : {opts : _} -> Doc opts -> Doc opts
132 | braces = enclose lbrace rbrace
133 |
134 | ||| Encolses a document in brackets.
135 | export
136 | brackets : {opts : _} -> Doc opts -> Doc opts
137 | brackets = enclose lbracket rbracket
138 |
139 | --------------------------------------------------------------------------------
140 | --          Combining Documents
141 | --------------------------------------------------------------------------------
142 |
143 | ||| Tries to layout the first document on a single line, replacing
144 | ||| it with the alternative if a) it does not fit the page with or b)
145 | ||| it inherently is placed on several lines.
146 | |||
147 | ||| This combinator is very useful for pretty printing Idris values
148 | ||| (data constructors, lists, records), because we typically try to
149 | ||| place them on a single line if and only if they fit the page width
150 | ||| and none of their arguments is placed on several lines.
151 | export
152 | ifMultiline : {opts : _} -> (doc, alt : Doc opts) -> Doc opts
153 | ifMultiline doc alt = do
154 |   l <- doc
155 |   if isMultiline l then alt else pure l <|> alt
156 |
157 | export infixl 8 <++>
158 |
159 | ||| Concatenates two documents horizontally with a single space between them.
160 | export %inline
161 | (<++>) : {opts : _} -> Doc opts -> Doc opts -> Doc opts
162 | x <++> y = x <+> space <+> y
163 |
164 | export infixl 8 <+?+>
165 |
166 | ||| Concatenates two documents horizontally with a space between them, if both
167 | ||| documents are not empty.
168 | export %inline
169 | (<+?+>) : {opts : _} -> Doc opts -> Doc opts -> Doc opts
170 | x <+?+> y = do
171 |   l <- x
172 |   if isEmpty l then y else do
173 |     r <- y
174 |     if isEmpty r then pure l else
175 |       pure l <+> space <+> pure r
176 |
177 | export
178 | vappend : {opts : _} -> Doc opts -> Doc opts -> Doc opts
179 | vappend x y = flush x <+> y
180 |
181 | ||| Concatenate a sequence of documents horizontally using `(<+>)`.
182 | export
183 | hcat : {opts : _} -> List (Doc opts) -> Doc opts
184 | hcat []       = empty
185 | hcat (h :: t) = foldl (<+>) h t
186 |
187 | ||| Concatenate a sequence of documents horizontally using `(<++>)`.
188 | export
189 | hsep : {opts : _} -> List (Doc opts) -> Doc opts
190 | hsep []       = empty
191 | hsep (h :: t) = foldl (<++>) h t
192 |
193 | ||| Concatenate a list of documents vertically.
194 | export
195 | vsep : {opts : _} -> List (Doc opts) -> Doc opts
196 | vsep []       = empty
197 | vsep (h :: t) = foldl vappend h t
198 |
199 | ||| Tries to layout the two documents horizontally, but appends
200 | ||| the second indented by the given number of spaces below the
201 | ||| first if the horizontal version exceeds the width limit.
202 | export
203 | hang : {opts : _} -> Nat -> Doc opts -> Doc opts -> Doc opts
204 | hang k x y = (x <+> y) <|> vappend x (indent k y)
205 |
206 | ||| Like `hang` but separates the two documents by a space in case of
207 | ||| a horizontal alignment.
208 | export
209 | hangSep : {opts : _} -> Nat -> Doc opts -> Doc opts -> Doc opts
210 | hangSep k x y = (x <++> y) <|> vappend x (indent k y)
211 |
212 | ||| Tries to layout the two documents horizontally, but appends
213 | ||| the second indented by the given number of spaces below the
214 | ||| first if the horizontal version exceeds the width limit, or
215 | ||| if needs several lines.
216 | export
217 | hang' : {opts : _} -> Nat -> Doc opts -> Doc opts -> Doc opts
218 | hang' k x y = ifMultiline (x <+> y) (vappend x $ indent k y)
219 |
220 | ||| Like `hang'` but separates the two documents by a space in case of
221 | ||| a horizontal alignment.
222 | export
223 | hangSep' : {opts : _} -> Nat -> Doc opts -> Doc opts -> Doc opts
224 | hangSep' k x y = ifMultiline (x <++> y) (vappend x $ indent k y)
225 |
226 | ||| Tries to separate the given documents horizontally, but
227 | ||| concatenates them vertically if the horizontal layout exceeds the
228 | ||| width limit.
229 | export
230 | sep : {opts : _} -> List (Doc opts) -> Doc opts
231 | sep xs = hsep xs <|> vsep xs
232 |
233 | ||| Tries to separate the given documents horizontally, but
234 | ||| concatenates them vertically if the horizontal layout exceeds the
235 | ||| width limit, or horizontal layout leads to a multiline document.
236 | export
237 | sep' : {opts : _} -> List (Doc opts) -> Doc opts
238 | sep' xs = ifMultiline (hsep xs) (vsep xs)
239 |
240 | ||| Add the given document only when condition is true
241 | export
242 | when : Bool -> Doc opts -> Doc opts
243 | when True  = id
244 | when False = const empty
245 |
246 | --------------------------------------------------------------------------------
247 | --          Lists of Documents
248 | --------------------------------------------------------------------------------
249 |
250 | ||| Pretty prints a list of documents separated by the given delimiter
251 | ||| and wrapping them in opening and closing symbols.
252 | |||
253 | ||| If it fits the page width, the document is layed out horizontally,
254 | ||| otherwise it's layed out vertically with  leading commas.
255 | |||
256 | ||| Horizontal layout for `generalList "[" "]" "," [1,2,3]:
257 | |||
258 | ||| ```
259 | ||| [1, 2, 3]
260 | ||| ```
261 | |||
262 | ||| Vertical layout:
263 | |||
264 | ||| ```
265 | ||| [ 1
266 | ||| , 2
267 | ||| , 3
268 | ||| ]
269 | ||| ```
270 | export
271 | generalList : {opts : _} -> (o,c,sep : Doc opts) -> List (Doc opts) -> Doc opts
272 | generalList o c sep []        = o <+> c
273 | generalList o c sep (x :: xs) =
274 |   let xs' := map (sep <++>) xs ++ [c]
275 |    in ifMultiline (hcat $ o :: x :: xs') (vsep $ (o <++> x) :: xs')
276 |
277 | ||| Pretty prints a list of documents separated by commas
278 | ||| and wrapping them in brackets.
279 | |||
280 | ||| If it fits the page width, the document is layed out horizontally,
281 | ||| otherwise it's layed out vertically with leading delimiters.
282 | |||
283 | ||| Horizontal layout:
284 | |||
285 | ||| ```
286 | ||| [1, 2, 3]
287 | ||| ```
288 | |||
289 | ||| Vertical layout:
290 | |||
291 | ||| ```
292 | ||| [ 1
293 | ||| , 2
294 | ||| , 3
295 | ||| ]
296 | ||| ```
297 | export %inline
298 | list : {opts : _} -> List (Doc opts) -> Doc opts
299 | list = generalList lbracket rbracket comma
300 |
301 | ||| Pretty prints a `SnocList` of documents separated by commas
302 | ||| and wrapping them in brackets.
303 | |||
304 | ||| If it fits the page width, the document is layed out horizontally,
305 | ||| otherwise it's layed out vertically with  leading commas.
306 | |||
307 | ||| Horizontal layout:
308 | |||
309 | ||| ```
310 | ||| [<1, 2, 3]
311 | ||| ```
312 | |||
313 | ||| Vertical layout:
314 | |||
315 | ||| ```
316 | ||| [<1
317 | ||| , 2
318 | ||| , 3
319 | ||| ]
320 | ||| ```
321 | export
322 | snocList : {opts : _} -> List (Doc opts) -> Doc opts
323 | snocList = generalList (line "[<") rbracket comma
324 |
325 | ||| Pretty prints a list of documents separated by commas
326 | ||| and wrapping them in parentheses.
327 | |||
328 | ||| Horizontal layout:
329 | |||
330 | ||| ```
331 | ||| (x, y, z)
332 | ||| ```
333 | |||
334 | ||| Vertical layout:
335 | |||
336 | ||| ```
337 | ||| ( x
338 | ||| , y
339 | ||| , z
340 | ||| )
341 | ||| ]
342 | export
343 | tuple : {opts : _} -> List (Doc opts) -> Doc opts
344 | tuple = generalList lparen rparen comma
345 |
346 | ||| Pretty prints a list of documents separated by commas
347 | ||| and wrapping them in curly braces.
348 | |||
349 | ||| Horizontal layout:
350 | |||
351 | ||| ```
352 | ||| {x, y, z}
353 | ||| ```
354 | |||
355 | ||| Vertical layout:
356 | |||
357 | ||| ```
358 | ||| { x
359 | ||| , y
360 | ||| , z
361 | ||| }
362 | ||| ]
363 | export
364 | fields : {opts : _} -> List (Doc opts) -> Doc opts
365 | fields = generalList lbrace rbrace comma
366 |