adamc@1
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@1
|
2 * All rights reserved.
|
adamc@1
|
3 *
|
adamc@1
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@1
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@1
|
6 *
|
adamc@1
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@1
|
8 * this list of conditions and the following disclaimer.
|
adamc@1
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@1
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@1
|
11 * and/or other materials provided with the distribution.
|
adamc@1
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@1
|
13 * derived from this software without specific prior written permission.
|
adamc@1
|
14 *
|
adamc@1
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@1
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@1
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@1
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@1
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@1
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@1
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@1
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@1
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@1
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@1
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@1
|
26 *)
|
adamc@1
|
27
|
adamc@1
|
28 (* Pretty-printing Laconic/Web *)
|
adamc@1
|
29
|
adamc@4
|
30 structure SourcePrint :> SOURCE_PRINT = struct
|
adamc@1
|
31
|
adamc@1
|
32 open Print.PD
|
adamc@1
|
33 open Print
|
adamc@1
|
34
|
adamc@4
|
35 open Source
|
adamc@1
|
36
|
adamc@1
|
37 fun p_kind' par (k, _) =
|
adamc@1
|
38 case k of
|
adamc@1
|
39 KType => string "Type"
|
adamc@1
|
40 | KArrow (k1, k2) => parenIf par (box [p_kind' true k1,
|
adamc@1
|
41 space,
|
adamc@1
|
42 string "->",
|
adamc@1
|
43 space,
|
adamc@1
|
44 p_kind k2])
|
adamc@1
|
45 | KName => string "Name"
|
adamc@1
|
46 | KRecord k => box [string "{", p_kind k, string "}"]
|
adamc@82
|
47 | KUnit => string "Unit"
|
adamc@18
|
48 | KWild => string "_"
|
adamc@1
|
49
|
adamc@1
|
50 and p_kind k = p_kind' false k
|
adamc@1
|
51
|
adamc@1
|
52 fun p_explicitness e =
|
adamc@1
|
53 case e of
|
adamc@1
|
54 Explicit => string "::"
|
adamc@1
|
55 | Implicit => string ":::"
|
adamc@1
|
56
|
adamc@1
|
57 fun p_con' par (c, _) =
|
adamc@1
|
58 case c of
|
adamc@1
|
59 CAnnot (c, k) => box [string "(",
|
adamc@1
|
60 p_con c,
|
adamc@1
|
61 space,
|
adamc@1
|
62 string "::",
|
adamc@1
|
63 space,
|
adamc@1
|
64 p_kind k,
|
adamc@1
|
65 string ")"]
|
adamc@1
|
66
|
adamc@1
|
67 | TFun (t1, t2) => parenIf par (box [p_con' true t1,
|
adamc@1
|
68 space,
|
adamc@1
|
69 string "->",
|
adamc@1
|
70 space,
|
adamc@1
|
71 p_con t2])
|
adamc@1
|
72 | TCFun (e, x, k, c) => parenIf par (box [string x,
|
adamc@1
|
73 space,
|
adamc@1
|
74 p_explicitness e,
|
adamc@1
|
75 space,
|
adamc@1
|
76 p_kind k,
|
adamc@1
|
77 space,
|
adamc@1
|
78 string "->",
|
adamc@1
|
79 space,
|
adamc@1
|
80 p_con c])
|
adamc@85
|
81 | TDisjoint (c1, c2, c3) => parenIf par (box [p_con c1,
|
adamc@85
|
82 space,
|
adamc@85
|
83 string "~",
|
adamc@85
|
84 space,
|
adamc@85
|
85 p_con c2,
|
adamc@85
|
86 space,
|
adamc@85
|
87 string "->",
|
adamc@85
|
88 space,
|
adamc@85
|
89 p_con c3])
|
adamc@1
|
90 | TRecord (CRecord xcs, _) => box [string "{",
|
adamc@1
|
91 p_list (fn (x, c) =>
|
adamc@20
|
92 box [p_name x,
|
adamc@1
|
93 space,
|
adamc@1
|
94 string ":",
|
adamc@1
|
95 space,
|
adamc@1
|
96 p_con c]) xcs,
|
adamc@1
|
97 string "}"]
|
adamc@1
|
98 | TRecord c => box [string "$",
|
adamc@1
|
99 p_con' true c]
|
adamc@1
|
100
|
adamc@34
|
101 | CVar (ss, s) => p_list_sep (string ".") string (ss @ [s])
|
adamc@1
|
102 | CApp (c1, c2) => parenIf par (box [p_con c1,
|
adamc@1
|
103 space,
|
adamc@1
|
104 p_con' true c2])
|
adamc@67
|
105 | CAbs (x, NONE, c) => parenIf par (box [string "fn",
|
adamc@67
|
106 space,
|
adamc@67
|
107 string x,
|
adamc@67
|
108 space,
|
adamc@67
|
109 string "=>",
|
adamc@67
|
110 space,
|
adamc@67
|
111 p_con c])
|
adamc@67
|
112 | CAbs (x, SOME k, c) => parenIf par (box [string "fn",
|
adamc@67
|
113 space,
|
adamc@67
|
114 string x,
|
adamc@67
|
115 space,
|
adamc@67
|
116 string "::",
|
adamc@67
|
117 space,
|
adamc@67
|
118 p_kind k,
|
adamc@67
|
119 space,
|
adamc@67
|
120 string "=>",
|
adamc@67
|
121 space,
|
adamc@67
|
122 p_con c])
|
adamc@84
|
123 | CDisjoint (c1, c2, c3) => parenIf par (box [p_con c1,
|
adamc@84
|
124 space,
|
adamc@84
|
125 string "~",
|
adamc@84
|
126 space,
|
adamc@84
|
127 p_con c2,
|
adamc@84
|
128 space,
|
adamc@84
|
129 string "=>",
|
adamc@84
|
130 space,
|
adamc@84
|
131 p_con c3])
|
adamc@1
|
132
|
adamc@1
|
133 | CName s => box [string "#", string s]
|
adamc@1
|
134
|
adamc@1
|
135 | CRecord xcs => box [string "[",
|
adamc@1
|
136 p_list (fn (x, c) =>
|
adamc@1
|
137 box [p_con x,
|
adamc@1
|
138 space,
|
adamc@1
|
139 string "=",
|
adamc@1
|
140 space,
|
adamc@1
|
141 p_con c]) xcs,
|
adamc@1
|
142 string "]"]
|
adamc@1
|
143 | CConcat (c1, c2) => parenIf par (box [p_con' true c1,
|
adamc@1
|
144 space,
|
adamc@1
|
145 string "++",
|
adamc@1
|
146 space,
|
adamc@1
|
147 p_con c2])
|
adamc@67
|
148 | CFold => string "fold"
|
adamc@82
|
149
|
adamc@82
|
150 | CUnit => string "()"
|
adamc@82
|
151
|
adamc@18
|
152 | CWild k => box [string "(_",
|
adamc@18
|
153 space,
|
adamc@18
|
154 string "::",
|
adamc@18
|
155 space,
|
adamc@18
|
156 p_kind k]
|
adamc@1
|
157
|
adamc@1
|
158 and p_con c = p_con' false c
|
adamc@1
|
159
|
adamc@20
|
160 and p_name (all as (c, _)) =
|
adamc@20
|
161 case c of
|
adamc@20
|
162 CName s => string s
|
adamc@20
|
163 | _ => p_con all
|
adamc@20
|
164
|
adamc@8
|
165 fun p_exp' par (e, _) =
|
adamc@8
|
166 case e of
|
adamc@8
|
167 EAnnot (e, t) => box [string "(",
|
adamc@8
|
168 p_exp e,
|
adamc@8
|
169 space,
|
adamc@8
|
170 string ":",
|
adamc@8
|
171 space,
|
adamc@8
|
172 p_con t,
|
adamc@8
|
173 string ")"]
|
adamc@8
|
174
|
adamc@14
|
175 | EPrim p => Prim.p_t p
|
adamc@34
|
176 | EVar (ss, s) => p_list_sep (string ".") string (ss @ [s])
|
adamc@8
|
177 | EApp (e1, e2) => parenIf par (box [p_exp e1,
|
adamc@8
|
178 space,
|
adamc@8
|
179 p_exp' true e2])
|
adamc@8
|
180 | EAbs (x, NONE, e) => parenIf par (box [string "fn",
|
adamc@8
|
181 space,
|
adamc@8
|
182 string x,
|
adamc@8
|
183 space,
|
adamc@8
|
184 string "=>",
|
adamc@8
|
185 space,
|
adamc@8
|
186 p_exp e])
|
adamc@8
|
187 | EAbs (x, SOME t, e) => parenIf par (box [string "fn",
|
adamc@8
|
188 space,
|
adamc@8
|
189 string x,
|
adamc@8
|
190 space,
|
adamc@8
|
191 string ":",
|
adamc@8
|
192 space,
|
adamc@8
|
193 p_con t,
|
adamc@8
|
194 space,
|
adamc@8
|
195 string "=>",
|
adamc@8
|
196 space,
|
adamc@8
|
197 p_exp e])
|
adamc@8
|
198 | ECApp (e, c) => parenIf par (box [p_exp e,
|
adamc@8
|
199 space,
|
adamc@8
|
200 string "[",
|
adamc@8
|
201 p_con c,
|
adamc@8
|
202 string "]"])
|
adamc@8
|
203 | ECAbs (exp, x, k, e) => parenIf par (box [string "fn",
|
adamc@8
|
204 space,
|
adamc@8
|
205 string x,
|
adamc@8
|
206 space,
|
adamc@8
|
207 p_explicitness exp,
|
adamc@8
|
208 space,
|
adamc@8
|
209 p_kind k,
|
adamc@8
|
210 space,
|
adamc@8
|
211 string "=>",
|
adamc@8
|
212 space,
|
adamc@8
|
213 p_exp e])
|
adamc@85
|
214 | EDisjoint (c1, c2, e) => parenIf par (box [p_con c1,
|
adamc@85
|
215 space,
|
adamc@85
|
216 string "~",
|
adamc@85
|
217 space,
|
adamc@85
|
218 p_con c2,
|
adamc@85
|
219 space,
|
adamc@85
|
220 string "=>",
|
adamc@85
|
221 space,
|
adamc@85
|
222 p_exp e])
|
adamc@8
|
223
|
adamc@12
|
224 | ERecord xes => box [string "{",
|
adamc@12
|
225 p_list (fn (x, e) =>
|
adamc@21
|
226 box [p_name x,
|
adamc@12
|
227 space,
|
adamc@12
|
228 string "=",
|
adamc@12
|
229 space,
|
adamc@12
|
230 p_exp e]) xes,
|
adamc@12
|
231 string "}"]
|
adamc@12
|
232 | EField (e, c) => box [p_exp' true e,
|
adamc@12
|
233 string ".",
|
adamc@12
|
234 p_con' true c]
|
adamc@71
|
235 | EFold => string "fold"
|
adamc@12
|
236
|
adamc@8
|
237 and p_exp e = p_exp' false e
|
adamc@8
|
238
|
adamc@30
|
239 fun p_sgn_item (sgi, _) =
|
adamc@30
|
240 case sgi of
|
adamc@30
|
241 SgiConAbs (x, k) => box [string "con",
|
adamc@30
|
242 space,
|
adamc@30
|
243 string x,
|
adamc@30
|
244 space,
|
adamc@30
|
245 string "::",
|
adamc@30
|
246 space,
|
adamc@30
|
247 p_kind k]
|
adamc@30
|
248 | SgiCon (x, NONE, c) => box [string "con",
|
adamc@30
|
249 space,
|
adamc@30
|
250 string x,
|
adamc@30
|
251 space,
|
adamc@30
|
252 string "=",
|
adamc@30
|
253 space,
|
adamc@30
|
254 p_con c]
|
adamc@30
|
255 | SgiCon (x, SOME k, c) => box [string "con",
|
adamc@30
|
256 space,
|
adamc@30
|
257 string x,
|
adamc@30
|
258 space,
|
adamc@30
|
259 string "::",
|
adamc@30
|
260 space,
|
adamc@30
|
261 p_kind k,
|
adamc@30
|
262 space,
|
adamc@30
|
263 string "=",
|
adamc@30
|
264 space,
|
adamc@30
|
265 p_con c]
|
adamc@30
|
266 | SgiVal (x, c) => box [string "val",
|
adamc@30
|
267 space,
|
adamc@30
|
268 string x,
|
adamc@30
|
269 space,
|
adamc@30
|
270 string ":",
|
adamc@30
|
271 space,
|
adamc@30
|
272 p_con c]
|
adamc@30
|
273 | SgiStr (x, sgn) => box [string "structure",
|
adamc@30
|
274 space,
|
adamc@30
|
275 string x,
|
adamc@30
|
276 space,
|
adamc@30
|
277 string ":",
|
adamc@30
|
278 space,
|
adamc@30
|
279 p_sgn sgn]
|
adamc@59
|
280 | SgiSgn (x, sgn) => box [string "signature",
|
adamc@59
|
281 space,
|
adamc@59
|
282 string x,
|
adamc@59
|
283 space,
|
adamc@59
|
284 string "=",
|
adamc@59
|
285 space,
|
adamc@59
|
286 p_sgn sgn]
|
adamc@58
|
287 | SgiInclude sgn => box [string "include",
|
adamc@58
|
288 space,
|
adamc@58
|
289 p_sgn sgn]
|
adamc@88
|
290 | SgiConstraint (c1, c2) => box [string "constraint",
|
adamc@88
|
291 space,
|
adamc@88
|
292 p_con c1,
|
adamc@88
|
293 space,
|
adamc@88
|
294 string "~",
|
adamc@88
|
295 space,
|
adamc@88
|
296 p_con c2]
|
adamc@30
|
297
|
adamc@30
|
298 and p_sgn (sgn, _) =
|
adamc@30
|
299 case sgn of
|
adamc@30
|
300 SgnConst sgis => box [string "sig",
|
adamc@30
|
301 newline,
|
adamc@30
|
302 p_list_sep newline p_sgn_item sgis,
|
adamc@30
|
303 newline,
|
adamc@30
|
304 string "end"]
|
adamc@30
|
305 | SgnVar x => string x
|
adamc@40
|
306 | SgnFun (x, sgn, sgn') => box [string "functor",
|
adamc@40
|
307 space,
|
adamc@40
|
308 string "(",
|
adamc@40
|
309 string x,
|
adamc@40
|
310 space,
|
adamc@40
|
311 string ":",
|
adamc@40
|
312 p_sgn sgn,
|
adamc@40
|
313 string ")",
|
adamc@40
|
314 space,
|
adamc@40
|
315 string ":",
|
adamc@40
|
316 space,
|
adamc@40
|
317 p_sgn sgn']
|
adamc@42
|
318 | SgnWhere (sgn, x, c) => box [p_sgn sgn,
|
adamc@42
|
319 space,
|
adamc@42
|
320 string "where",
|
adamc@42
|
321 space,
|
adamc@42
|
322 string "con",
|
adamc@42
|
323 space,
|
adamc@42
|
324 string x,
|
adamc@42
|
325 space,
|
adamc@42
|
326 string "=",
|
adamc@42
|
327 space,
|
adamc@42
|
328 p_con c]
|
adamc@59
|
329 | SgnProj (m, ms, x) => p_list_sep (string ".") string (m :: ms @ [x])
|
adamc@59
|
330
|
adamc@42
|
331
|
adamc@1
|
332 fun p_decl ((d, _) : decl) =
|
adamc@1
|
333 case d of
|
adamc@1
|
334 DCon (x, NONE, c) => box [string "con",
|
adamc@1
|
335 space,
|
adamc@1
|
336 string x,
|
adamc@1
|
337 space,
|
adamc@1
|
338 string "=",
|
adamc@1
|
339 space,
|
adamc@1
|
340 p_con c]
|
adamc@1
|
341 | DCon (x, SOME k, c) => box [string "con",
|
adamc@1
|
342 space,
|
adamc@1
|
343 string x,
|
adamc@1
|
344 space,
|
adamc@1
|
345 string "::",
|
adamc@1
|
346 space,
|
adamc@1
|
347 p_kind k,
|
adamc@1
|
348 space,
|
adamc@1
|
349 string "=",
|
adamc@1
|
350 space,
|
adamc@1
|
351 p_con c]
|
adamc@8
|
352 | DVal (x, NONE, e) => box [string "val",
|
adamc@8
|
353 space,
|
adamc@8
|
354 string x,
|
adamc@8
|
355 space,
|
adamc@8
|
356 string "=",
|
adamc@8
|
357 space,
|
adamc@8
|
358 p_exp e]
|
adamc@8
|
359 | DVal (x, SOME t, e) => box [string "val",
|
adamc@8
|
360 space,
|
adamc@8
|
361 string x,
|
adamc@8
|
362 space,
|
adamc@8
|
363 string ":",
|
adamc@8
|
364 space,
|
adamc@8
|
365 p_con t,
|
adamc@8
|
366 space,
|
adamc@8
|
367 string "=",
|
adamc@8
|
368 space,
|
adamc@8
|
369 p_exp e]
|
adamc@1
|
370
|
adamc@30
|
371 | DSgn (x, sgn) => box [string "signature",
|
adamc@30
|
372 space,
|
adamc@30
|
373 string x,
|
adamc@30
|
374 space,
|
adamc@30
|
375 string "=",
|
adamc@30
|
376 space,
|
adamc@30
|
377 p_sgn sgn]
|
adamc@30
|
378 | DStr (x, NONE, str) => box [string "structure",
|
adamc@30
|
379 space,
|
adamc@30
|
380 string x,
|
adamc@30
|
381 space,
|
adamc@30
|
382 string "=",
|
adamc@30
|
383 space,
|
adamc@30
|
384 p_str str]
|
adamc@30
|
385 | DStr (x, SOME sgn, str) => box [string "structure",
|
adamc@30
|
386 space,
|
adamc@30
|
387 string x,
|
adamc@30
|
388 space,
|
adamc@30
|
389 string ":",
|
adamc@30
|
390 space,
|
adamc@30
|
391 p_sgn sgn,
|
adamc@30
|
392 space,
|
adamc@30
|
393 string "=",
|
adamc@30
|
394 space,
|
adamc@30
|
395 p_str str]
|
adamc@48
|
396 | DFfiStr (x, sgn) => box [string "extern",
|
adamc@48
|
397 space,
|
adamc@48
|
398 string "structure",
|
adamc@48
|
399 space,
|
adamc@48
|
400 string x,
|
adamc@48
|
401 space,
|
adamc@48
|
402 string ":",
|
adamc@48
|
403 space,
|
adamc@48
|
404 p_sgn sgn]
|
adamc@61
|
405 | DOpen (m, ms) => box [string "open",
|
adamc@61
|
406 space,
|
adamc@61
|
407 p_list_sep (string ".") string (m :: ms)]
|
adamc@88
|
408 | DConstraint (c1, c2) => box [string "constraint",
|
adamc@88
|
409 space,
|
adamc@88
|
410 p_con c1,
|
adamc@88
|
411 space,
|
adamc@88
|
412 string "~",
|
adamc@88
|
413 space,
|
adamc@88
|
414 p_con c2]
|
adamc@88
|
415 | DOpenConstraints (m, ms) => box [string "open",
|
adamc@88
|
416 space,
|
adamc@88
|
417 string "constraints",
|
adamc@88
|
418 space,
|
adamc@88
|
419 p_list_sep (string ".") string (m :: ms)]
|
adamc@30
|
420
|
adamc@30
|
421 and p_str (str, _) =
|
adamc@30
|
422 case str of
|
adamc@30
|
423 StrConst ds => box [string "struct",
|
adamc@30
|
424 newline,
|
adamc@30
|
425 p_list_sep newline p_decl ds,
|
adamc@30
|
426 newline,
|
adamc@30
|
427 string "end"]
|
adamc@30
|
428 | StrVar x => string x
|
adamc@34
|
429 | StrProj (str, x) => box [p_str str,
|
adamc@34
|
430 string ".",
|
adamc@34
|
431 string x]
|
adamc@40
|
432 | StrFun (x, sgn, NONE, str) => box [string "functor",
|
adamc@40
|
433 space,
|
adamc@40
|
434 string "(",
|
adamc@40
|
435 string x,
|
adamc@40
|
436 space,
|
adamc@40
|
437 string ":",
|
adamc@40
|
438 p_sgn sgn,
|
adamc@40
|
439 string ")",
|
adamc@40
|
440 space,
|
adamc@40
|
441 string "=>",
|
adamc@40
|
442 space,
|
adamc@40
|
443 p_str str]
|
adamc@40
|
444 | StrFun (x, sgn, SOME sgn', str) => box [string "functor",
|
adamc@40
|
445 space,
|
adamc@40
|
446 string "(",
|
adamc@40
|
447 string x,
|
adamc@40
|
448 space,
|
adamc@40
|
449 string ":",
|
adamc@40
|
450 p_sgn sgn,
|
adamc@40
|
451 string ")",
|
adamc@40
|
452 space,
|
adamc@40
|
453 string ":",
|
adamc@40
|
454 space,
|
adamc@40
|
455 p_sgn sgn',
|
adamc@40
|
456 space,
|
adamc@40
|
457 string "=>",
|
adamc@40
|
458 space,
|
adamc@40
|
459 p_str str]
|
adamc@44
|
460 | StrApp (str1, str2) => box [p_str str1,
|
adamc@44
|
461 string "(",
|
adamc@44
|
462 p_str str2,
|
adamc@44
|
463 string ")"]
|
adamc@30
|
464
|
adamc@1
|
465 val p_file = p_list_sep newline p_decl
|
adamc@1
|
466
|
adamc@1
|
467 end
|