adamc@3
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@3
|
2 * All rights reserved.
|
adamc@3
|
3 *
|
adamc@3
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@3
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@3
|
6 *
|
adamc@3
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@3
|
8 * this list of conditions and the following disclaimer.
|
adamc@3
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@3
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@3
|
11 * and/or other materials provided with the distribution.
|
adamc@3
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@3
|
13 * derived from this software without specific prior written permission.
|
adamc@3
|
14 *
|
adamc@3
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@3
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@3
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@3
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@3
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@3
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@3
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@3
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@3
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@3
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@3
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@3
|
26 *)
|
adamc@3
|
27
|
adamc@244
|
28 (* Pretty-printing elaborated Ur/Web *)
|
adamc@3
|
29
|
adamc@3
|
30 structure ElabPrint :> ELAB_PRINT = struct
|
adamc@3
|
31
|
adamc@3
|
32 open Print.PD
|
adamc@3
|
33 open Print
|
adamc@3
|
34
|
adamc@3
|
35 open Elab
|
adamc@3
|
36
|
adamc@3
|
37 structure E = ElabEnv
|
adamc@3
|
38
|
adamc@11
|
39 val debug = ref false
|
adamc@11
|
40
|
adamc@623
|
41 fun p_kind' par env (k, _) =
|
adamc@3
|
42 case k of
|
adamc@3
|
43 KType => string "Type"
|
adamc@623
|
44 | KArrow (k1, k2) => parenIf par (box [p_kind' true env k1,
|
adamc@3
|
45 space,
|
adamc@3
|
46 string "->",
|
adamc@3
|
47 space,
|
adamc@623
|
48 p_kind env k2])
|
adamc@3
|
49 | KName => string "Name"
|
adamc@623
|
50 | KRecord k => box [string "{", p_kind env k, string "}"]
|
adamc@82
|
51 | KUnit => string "Unit"
|
adamc@207
|
52 | KTuple ks => box [string "(",
|
adamc@623
|
53 p_list_sep (box [space, string "*", space]) (p_kind env) ks,
|
adamc@207
|
54 string ")"]
|
adamc@3
|
55
|
adamc@3
|
56 | KError => string "<ERROR>"
|
adam@1639
|
57 | KUnif (_, _, ref (KKnown k)) => p_kind' par env k
|
adamc@76
|
58 | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">")
|
adam@1639
|
59 | KTupleUnif (_, _, ref (KKnown k)) => p_kind' par env k
|
adam@1302
|
60 | KTupleUnif (_, nks, _) => box [string "(",
|
adam@1302
|
61 p_list_sep (box [space, string "*", space])
|
adam@1302
|
62 (fn (n, k) => box [string (Int.toString n ^ ":"),
|
adam@1302
|
63 space,
|
adam@1302
|
64 p_kind env k]) nks,
|
adam@1302
|
65 space,
|
adam@1302
|
66 string "*",
|
adam@1302
|
67 space,
|
adam@1302
|
68 string "...)"]
|
adamc@3
|
69
|
adamc@623
|
70 | KRel n => ((if !debug then
|
adamc@623
|
71 string (E.lookupKRel env n ^ "_" ^ Int.toString n)
|
adamc@623
|
72 else
|
adamc@623
|
73 string (E.lookupKRel env n))
|
adamc@623
|
74 handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
|
adamc@623
|
75 | KFun (x, k) => box [string x,
|
adamc@623
|
76 space,
|
adamc@623
|
77 string "-->",
|
adamc@623
|
78 space,
|
adamc@623
|
79 p_kind (E.pushKRel env x) k]
|
adamc@623
|
80
|
adamc@624
|
81 and p_kind env = p_kind' false env
|
adamc@3
|
82
|
adamc@3
|
83 fun p_explicitness e =
|
adamc@3
|
84 case e of
|
adamc@3
|
85 Explicit => string "::"
|
adamc@3
|
86 | Implicit => string ":::"
|
adamc@3
|
87
|
adamc@3
|
88 fun p_con' par env (c, _) =
|
adamc@3
|
89 case c of
|
adam@1727
|
90 TFun (t1, t2) => parenIf par (box [p_con' true env t1,
|
adamc@3
|
91 space,
|
adamc@3
|
92 string "->",
|
adamc@3
|
93 space,
|
adamc@3
|
94 p_con env t2])
|
adamc@3
|
95 | TCFun (e, x, k, c) => parenIf par (box [string x,
|
adamc@3
|
96 space,
|
adamc@3
|
97 p_explicitness e,
|
adamc@3
|
98 space,
|
adamc@623
|
99 p_kind env k,
|
adamc@3
|
100 space,
|
adamc@3
|
101 string "->",
|
adamc@3
|
102 space,
|
adamc@3
|
103 p_con (E.pushCRel env x k) c])
|
adamc@628
|
104 | TDisjoint (c1, c2, c3) => parenIf par (box [string "[",
|
adamc@628
|
105 p_con env c1,
|
adamc@628
|
106 space,
|
adamc@628
|
107 string "~",
|
adamc@628
|
108 space,
|
adamc@628
|
109 p_con env c2,
|
adamc@628
|
110 string "]",
|
adamc@628
|
111 space,
|
adamc@628
|
112 string "=>",
|
adamc@628
|
113 space,
|
adamc@628
|
114 p_con env c3])
|
adam@1720
|
115 | TRecord (CRecord (_, xcs), _) =>
|
adam@1720
|
116 let
|
adam@1720
|
117 fun isTuple (n, xcs) =
|
adam@1720
|
118 case xcs of
|
adam@1720
|
119 [] => n > 2
|
adam@1720
|
120 | ((CName s, _), _) :: xcs' =>
|
adam@1720
|
121 s = Int.toString n andalso isTuple (n+1, xcs')
|
adam@1720
|
122 | _ => false
|
adam@1720
|
123 in
|
adam@1720
|
124 if isTuple (1, xcs) then
|
adam@1720
|
125 case xcs of
|
adam@1720
|
126 (_, c) :: xcs =>
|
adam@1720
|
127 parenIf par (box [p_con' true env c,
|
adam@1720
|
128 p_list_sep (box []) (fn (_, c) => box [space,
|
adam@1720
|
129 string "*",
|
adam@1720
|
130 space,
|
adam@1720
|
131 p_con' true env c]) xcs])
|
adam@1720
|
132 | _ => raise Fail "ElabPrint: surprise empty tuple"
|
adam@1720
|
133 else
|
adam@1720
|
134 box [string "{",
|
adam@1720
|
135 p_list (fn (x, c) =>
|
adam@1720
|
136 box [p_name env x,
|
adam@1720
|
137 space,
|
adam@1720
|
138 string ":",
|
adam@1720
|
139 space,
|
adam@1720
|
140 p_con env c]) xcs,
|
adam@1720
|
141 string "}"]
|
adam@1720
|
142 end
|
adamc@3
|
143 | TRecord c => box [string "$",
|
adamc@3
|
144 p_con' true env c]
|
adamc@3
|
145
|
adamc@11
|
146 | CRel n =>
|
adamc@71
|
147 ((if !debug then
|
adamc@71
|
148 string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n)
|
adamc@71
|
149 else
|
adamc@71
|
150 string (#1 (E.lookupCRel env n)))
|
adamc@71
|
151 handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
|
adamc@11
|
152 | CNamed n =>
|
adamc@34
|
153 ((if !debug then
|
adamc@34
|
154 string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
|
adamc@34
|
155 else
|
adamc@34
|
156 string (#1 (E.lookupCNamed env n)))
|
adamc@34
|
157 handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
|
adamc@34
|
158 | CModProj (m1, ms, x) =>
|
adamc@34
|
159 let
|
adamc@88
|
160 val m1x = #1 (E.lookupStrNamed env m1)
|
adamc@88
|
161 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
|
adamc@88
|
162
|
adamc@34
|
163 val m1s = if !debug then
|
adamc@34
|
164 m1x ^ "__" ^ Int.toString m1
|
adamc@34
|
165 else
|
adamc@34
|
166 m1x
|
adamc@34
|
167 in
|
adam@1721
|
168 if m1x = "Basis" andalso (case E.lookupC env x of
|
adam@1721
|
169 E.Named (n, _) =>
|
adam@1721
|
170 let
|
adam@1721
|
171 val (_, _, co) = E.lookupCNamed env n
|
adam@1721
|
172 in
|
adam@1721
|
173 case co of
|
adam@1721
|
174 SOME (CModProj (m1', [], x'), _) => m1' = m1 andalso x' = x
|
adam@1721
|
175 | _ => false
|
adam@1721
|
176 end
|
adam@1721
|
177 | E.NotBound => true
|
adam@1721
|
178 | _ => false) then
|
adam@1721
|
179 string x
|
adam@1721
|
180 else
|
adam@1721
|
181 p_list_sep (string ".") string (m1s :: ms @ [x])
|
adamc@88
|
182 end
|
adamc@3
|
183
|
adamc@3
|
184 | CApp (c1, c2) => parenIf par (box [p_con env c1,
|
adamc@3
|
185 space,
|
adamc@3
|
186 p_con' true env c2])
|
adamc@147
|
187 | CAbs (x, k, c) => parenIf true (box [string "fn",
|
adamc@147
|
188 space,
|
adamc@147
|
189 string x,
|
adamc@147
|
190 space,
|
adamc@147
|
191 string "::",
|
adamc@147
|
192 space,
|
adamc@623
|
193 p_kind env k,
|
adamc@147
|
194 space,
|
adamc@147
|
195 string "=>",
|
adamc@147
|
196 space,
|
adamc@147
|
197 p_con (E.pushCRel env x k) c])
|
adamc@3
|
198
|
adamc@3
|
199 | CName s => box [string "#", string s]
|
adamc@3
|
200
|
adamc@12
|
201 | CRecord (k, xcs) =>
|
adamc@12
|
202 if !debug then
|
adamc@12
|
203 parenIf par (box [string "[",
|
adamc@12
|
204 p_list (fn (x, c) =>
|
adam@1716
|
205 box [p_name env x,
|
adamc@12
|
206 space,
|
adamc@12
|
207 string "=",
|
adamc@12
|
208 space,
|
adamc@12
|
209 p_con env c]) xcs,
|
adamc@12
|
210 string "]::",
|
adamc@623
|
211 p_kind env k])
|
adamc@12
|
212 else
|
adamc@12
|
213 parenIf par (box [string "[",
|
adamc@12
|
214 p_list (fn (x, c) =>
|
adam@1716
|
215 box [p_name env x,
|
adamc@12
|
216 space,
|
adamc@12
|
217 string "=",
|
adamc@12
|
218 space,
|
adamc@12
|
219 p_con env c]) xcs,
|
adamc@12
|
220 string "]"])
|
adamc@3
|
221 | CConcat (c1, c2) => parenIf par (box [p_con' true env c1,
|
adamc@3
|
222 space,
|
adamc@3
|
223 string "++",
|
adamc@3
|
224 space,
|
adamc@3
|
225 p_con env c2])
|
adamc@621
|
226 | CMap _ => string "map"
|
adamc@3
|
227
|
adamc@82
|
228 | CUnit => string "()"
|
adamc@82
|
229
|
adamc@207
|
230 | CTuple cs => box [string "(",
|
adamc@207
|
231 p_list (p_con env) cs,
|
adamc@207
|
232 string ")"]
|
adamc@207
|
233 | CProj (c, n) => box [p_con env c,
|
adamc@207
|
234 string ".",
|
adamc@207
|
235 string (Int.toString n)]
|
adamc@207
|
236
|
adamc@3
|
237 | CError => string "<ERROR>"
|
adam@1639
|
238 | CUnif (nl, _, _, _, ref (Known c)) => p_con' par env (E.mliftConInCon nl c)
|
adam@1303
|
239 | CUnif (nl, _, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
|
adam@1303
|
240 p_kind env k,
|
adam@1303
|
241 case nl of
|
adam@1303
|
242 0 => box []
|
adam@1303
|
243 | _ => string ("+" ^ Int.toString nl),
|
adam@1303
|
244 string ">"]
|
adamc@623
|
245
|
adamc@623
|
246 | CKAbs (x, c) => box [string x,
|
adamc@623
|
247 space,
|
adamc@623
|
248 string "==>",
|
adamc@623
|
249 space,
|
adamc@623
|
250 p_con (E.pushKRel env x) c]
|
adamc@623
|
251 | CKApp (c, k) => box [p_con env c,
|
adamc@623
|
252 string "[[",
|
adamc@623
|
253 p_kind env k,
|
adamc@623
|
254 string "]]"]
|
adamc@623
|
255 | TKFun (x, c) => box [string x,
|
adamc@623
|
256 space,
|
adamc@623
|
257 string "-->",
|
adamc@623
|
258 space,
|
adamc@623
|
259 p_con (E.pushKRel env x) c]
|
adamc@623
|
260
|
adamc@3
|
261
|
adamc@3
|
262 and p_con env = p_con' false env
|
adamc@3
|
263
|
adamc@20
|
264 and p_name env (all as (c, _)) =
|
adamc@20
|
265 case c of
|
adamc@20
|
266 CName s => string s
|
adamc@20
|
267 | _ => p_con env all
|
adamc@20
|
268
|
adamc@171
|
269 fun p_patCon env pc =
|
adamc@171
|
270 case pc of
|
adamc@171
|
271 PConVar n =>
|
adamc@171
|
272 ((if !debug then
|
adamc@171
|
273 string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
|
adamc@171
|
274 else
|
adamc@171
|
275 string (#1 (E.lookupENamed env n)))
|
adamc@448
|
276 handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
|
adamc@171
|
277 | PConProj (m1, ms, x) =>
|
adamc@171
|
278 let
|
adamc@171
|
279 val m1x = #1 (E.lookupStrNamed env m1)
|
adamc@171
|
280 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
|
adamc@171
|
281
|
adamc@171
|
282 val m1s = if !debug then
|
adamc@171
|
283 m1x ^ "__" ^ Int.toString m1
|
adamc@171
|
284 else
|
adamc@171
|
285 m1x
|
adamc@171
|
286 in
|
adamc@171
|
287 p_list_sep (string ".") string (m1x :: ms @ [x])
|
adamc@171
|
288 end
|
adamc@171
|
289
|
adamc@171
|
290 fun p_pat' par env (p, _) =
|
adamc@171
|
291 case p of
|
adamc@171
|
292 PWild => string "_"
|
adamc@182
|
293 | PVar (s, _) => string s
|
adamc@173
|
294 | PPrim p => Prim.p_t p
|
adamc@191
|
295 | PCon (_, pc, _, NONE) => p_patCon env pc
|
adamc@191
|
296 | PCon (_, pc, _, SOME p) => parenIf par (box [p_patCon env pc,
|
adamc@188
|
297 space,
|
adamc@188
|
298 p_pat' true env p])
|
adamc@176
|
299 | PRecord xps =>
|
adamc@176
|
300 box [string "{",
|
adamc@1272
|
301 p_list_sep (box [string ",", space]) (fn (x, p, t) =>
|
adamc@176
|
302 box [string x,
|
adamc@176
|
303 space,
|
adamc@176
|
304 string "=",
|
adamc@176
|
305 space,
|
adamc@1272
|
306 p_pat env p,
|
adamc@1272
|
307 if !debug then
|
adamc@1272
|
308 box [space,
|
adamc@1272
|
309 string ":",
|
adamc@1272
|
310 space,
|
adamc@1272
|
311 p_con env t]
|
adamc@1272
|
312 else
|
adamc@1272
|
313 box []]) xps,
|
adamc@176
|
314 string "}"]
|
adamc@171
|
315
|
adamc@175
|
316 and p_pat x = p_pat' false x
|
adamc@171
|
317
|
adamc@9
|
318 fun p_exp' par env (e, _) =
|
adamc@9
|
319 case e of
|
adamc@14
|
320 EPrim p => Prim.p_t p
|
adamc@14
|
321 | ERel n =>
|
adamc@88
|
322 ((if !debug then
|
adamc@88
|
323 string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n)
|
adamc@88
|
324 else
|
adamc@88
|
325 string (#1 (E.lookupERel env n)))
|
adamc@88
|
326 handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
|
adamc@11
|
327 | ENamed n =>
|
adamc@88
|
328 ((if !debug then
|
adamc@88
|
329 string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
|
adamc@88
|
330 else
|
adamc@88
|
331 string (#1 (E.lookupENamed env n)))
|
adamc@448
|
332 handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
|
adamc@34
|
333 | EModProj (m1, ms, x) =>
|
adamc@34
|
334 let
|
adamc@88
|
335 val m1x = #1 (E.lookupStrNamed env m1)
|
adamc@88
|
336 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
|
adamc@88
|
337
|
adamc@34
|
338 val m1s = if !debug then
|
adamc@34
|
339 m1x ^ "__" ^ Int.toString m1
|
adamc@34
|
340 else
|
adamc@34
|
341 m1x
|
adamc@34
|
342 in
|
adamc@34
|
343 p_list_sep (string ".") string (m1x :: ms @ [x])
|
adamc@34
|
344 end
|
adamc@34
|
345
|
adamc@9
|
346 | EApp (e1, e2) => parenIf par (box [p_exp env e1,
|
adamc@9
|
347 space,
|
adamc@9
|
348 p_exp' true env e2])
|
adamc@26
|
349 | EAbs (x, t, _, e) => parenIf par (box [string "fn",
|
adamc@26
|
350 space,
|
adamc@26
|
351 string x,
|
adamc@26
|
352 space,
|
adamc@26
|
353 string ":",
|
adamc@26
|
354 space,
|
adamc@26
|
355 p_con env t,
|
adamc@26
|
356 space,
|
adamc@26
|
357 string "=>",
|
adamc@26
|
358 space,
|
adamc@26
|
359 p_exp (E.pushERel env x t) e])
|
adamc@9
|
360 | ECApp (e, c) => parenIf par (box [p_exp env e,
|
adamc@9
|
361 space,
|
adamc@9
|
362 string "[",
|
adamc@9
|
363 p_con env c,
|
adamc@9
|
364 string "]"])
|
adamc@9
|
365 | ECAbs (exp, x, k, e) => parenIf par (box [string "fn",
|
adamc@9
|
366 space,
|
adamc@9
|
367 string x,
|
adamc@9
|
368 space,
|
adamc@9
|
369 p_explicitness exp,
|
adamc@9
|
370 space,
|
adamc@623
|
371 p_kind env k,
|
adamc@9
|
372 space,
|
adamc@9
|
373 string "=>",
|
adamc@9
|
374 space,
|
adamc@9
|
375 p_exp (E.pushCRel env x k) e])
|
adamc@9
|
376
|
adamc@12
|
377 | ERecord xes => box [string "{",
|
adamc@29
|
378 p_list (fn (x, e, _) =>
|
adamc@21
|
379 box [p_name env x,
|
adamc@12
|
380 space,
|
adamc@12
|
381 string "=",
|
adamc@12
|
382 space,
|
adamc@12
|
383 p_exp env e]) xes,
|
adamc@12
|
384 string "}"]
|
adamc@12
|
385 | EField (e, c, {field, rest}) =>
|
adamc@12
|
386 if !debug then
|
adamc@12
|
387 box [p_exp' true env e,
|
adamc@12
|
388 string ".",
|
adamc@12
|
389 p_con' true env c,
|
adamc@12
|
390 space,
|
adamc@12
|
391 string "[",
|
adamc@12
|
392 p_con env field,
|
adamc@12
|
393 space,
|
adamc@12
|
394 string " in ",
|
adamc@12
|
395 space,
|
adamc@12
|
396 p_con env rest,
|
adamc@12
|
397 string "]"]
|
adamc@12
|
398 else
|
adamc@12
|
399 box [p_exp' true env e,
|
adamc@12
|
400 string ".",
|
adamc@12
|
401 p_con' true env c]
|
adamc@445
|
402 | EConcat (e1, c1, e2, c2) =>
|
adamc@339
|
403 parenIf par (if !debug then
|
adamc@445
|
404 box [p_exp' true env e1,
|
adamc@445
|
405 space,
|
adamc@445
|
406 string ":",
|
adamc@445
|
407 space,
|
adamc@445
|
408 p_con env c1,
|
adamc@445
|
409 space,
|
adamc@445
|
410 string "++",
|
adamc@445
|
411 space,
|
adamc@445
|
412 p_exp' true env e2,
|
adamc@445
|
413 space,
|
adamc@445
|
414 string ":",
|
adamc@445
|
415 space,
|
adamc@445
|
416 p_con env c2]
|
adamc@445
|
417 else
|
adamc@445
|
418 box [p_exp' true env e1,
|
adamc@339
|
419 space,
|
adamc@494
|
420 string "++",
|
adamc@339
|
421 space,
|
adamc@339
|
422 p_exp' true env e2])
|
adamc@149
|
423 | ECut (e, c, {field, rest}) =>
|
adamc@149
|
424 parenIf par (if !debug then
|
adamc@149
|
425 box [p_exp' true env e,
|
adamc@149
|
426 space,
|
adamc@149
|
427 string "--",
|
adamc@149
|
428 space,
|
adamc@149
|
429 p_con' true env c,
|
adamc@149
|
430 space,
|
adamc@149
|
431 string "[",
|
adamc@149
|
432 p_con env field,
|
adamc@149
|
433 space,
|
adamc@149
|
434 string " in ",
|
adamc@149
|
435 space,
|
adamc@149
|
436 p_con env rest,
|
adamc@149
|
437 string "]"]
|
adamc@149
|
438 else
|
adamc@149
|
439 box [p_exp' true env e,
|
adamc@149
|
440 space,
|
adamc@149
|
441 string "--",
|
adamc@149
|
442 space,
|
adamc@149
|
443 p_con' true env c])
|
adamc@493
|
444 | ECutMulti (e, c, {rest}) =>
|
adamc@493
|
445 parenIf par (if !debug then
|
adamc@493
|
446 box [p_exp' true env e,
|
adamc@493
|
447 space,
|
adamc@493
|
448 string "---",
|
adamc@493
|
449 space,
|
adamc@493
|
450 p_con' true env c,
|
adamc@493
|
451 space,
|
adamc@493
|
452 string "[",
|
adamc@493
|
453 p_con env rest,
|
adamc@493
|
454 string "]"]
|
adamc@493
|
455 else
|
adamc@493
|
456 box [p_exp' true env e,
|
adamc@493
|
457 space,
|
adamc@493
|
458 string "---",
|
adamc@493
|
459 space,
|
adamc@493
|
460 p_con' true env c])
|
adamc@493
|
461
|
adamc@171
|
462 | ECase (e, pes, _) => parenIf par (box [string "case",
|
adamc@171
|
463 space,
|
adamc@171
|
464 p_exp env e,
|
adamc@171
|
465 space,
|
adamc@171
|
466 string "of",
|
adamc@171
|
467 space,
|
adamc@171
|
468 p_list_sep (box [space, string "|", space])
|
adamc@171
|
469 (fn (p, e) => box [p_pat env p,
|
adamc@171
|
470 space,
|
adamc@171
|
471 string "=>",
|
adamc@171
|
472 space,
|
adamc@243
|
473 p_exp (E.patBinds env p) e]) pes])
|
adamc@171
|
474
|
adamc@9
|
475 | EError => string "<ERROR>"
|
adamc@228
|
476 | EUnif (ref (SOME e)) => p_exp env e
|
adamc@228
|
477 | EUnif _ => string "_"
|
adamc@9
|
478
|
adamc@825
|
479 | ELet (ds, e, _) =>
|
adamc@447
|
480 let
|
adamc@447
|
481 val (dsp, env) = ListUtil.foldlMap
|
adamc@447
|
482 (fn (d, env) =>
|
adamc@447
|
483 (p_edecl env d,
|
adamc@447
|
484 E.edeclBinds env d))
|
adamc@447
|
485 env ds
|
adamc@447
|
486 in
|
adamc@447
|
487 box [string "let",
|
adamc@447
|
488 newline,
|
adamc@447
|
489 box [p_list_sep newline (fn x => x) dsp],
|
adamc@447
|
490 newline,
|
adamc@447
|
491 string "in",
|
adamc@447
|
492 newline,
|
adamc@447
|
493 box [p_exp env e],
|
adamc@447
|
494 newline,
|
adamc@447
|
495 string "end"]
|
adamc@447
|
496 end
|
adamc@447
|
497
|
adamc@623
|
498 | EKAbs (x, e) => box [string x,
|
adamc@623
|
499 space,
|
adamc@623
|
500 string "==>",
|
adamc@623
|
501 space,
|
adamc@623
|
502 p_exp (E.pushKRel env x) e]
|
adamc@623
|
503 | EKApp (e, k) => box [p_exp env e,
|
adamc@623
|
504 string "[[",
|
adamc@623
|
505 p_kind env k,
|
adamc@623
|
506 string "]]"]
|
adamc@623
|
507
|
adamc@9
|
508 and p_exp env = p_exp' false env
|
adamc@9
|
509
|
adamc@447
|
510 and p_edecl env (dAll as (d, _)) =
|
adamc@447
|
511 case d of
|
adamc@825
|
512 EDVal (p, t, e) => box [string "val",
|
adamc@825
|
513 space,
|
adamc@825
|
514 p_pat env p,
|
adamc@825
|
515 space,
|
adamc@825
|
516 string ":",
|
adamc@825
|
517 space,
|
adamc@825
|
518 p_con env t,
|
adamc@825
|
519 space,
|
adamc@825
|
520 string "=",
|
adamc@825
|
521 space,
|
adamc@825
|
522 p_exp env e]
|
adamc@447
|
523 | EDValRec vis =>
|
adamc@447
|
524 let
|
adamc@447
|
525 val env = E.edeclBinds env dAll
|
adamc@447
|
526 in
|
adamc@447
|
527 box [string "val",
|
adamc@447
|
528 space,
|
adamc@447
|
529 string "rec",
|
adamc@447
|
530 space,
|
adamc@447
|
531 p_list_sep (box [newline, string "and", space]) (p_evali env) vis]
|
adamc@447
|
532 end
|
adamc@447
|
533
|
adamc@447
|
534 and p_evali env (x, t, e) = box [string x,
|
adamc@447
|
535 space,
|
adamc@447
|
536 string ":",
|
adamc@447
|
537 space,
|
adamc@447
|
538 p_con env t,
|
adamc@447
|
539 space,
|
adamc@447
|
540 string "=",
|
adamc@447
|
541 space,
|
adamc@447
|
542 p_exp env e]
|
adamc@31
|
543
|
adamc@191
|
544 fun p_datatype env (x, n, xs, cons) =
|
adamc@156
|
545 let
|
adamc@191
|
546 val k = (KType, ErrorMsg.dummySpan)
|
adamc@191
|
547 val env = E.pushCNamedAs env x n k NONE
|
adamc@191
|
548 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
|
adamc@156
|
549 in
|
adamc@805
|
550 box [string x,
|
adamc@191
|
551 p_list_sep (box []) (fn x => box [space, string x]) xs,
|
adamc@156
|
552 space,
|
adamc@156
|
553 string "=",
|
adamc@156
|
554 space,
|
adamc@156
|
555 p_list_sep (box [space, string "|", space])
|
adamc@156
|
556 (fn (x, _, NONE) => string x
|
adamc@156
|
557 | (x, _, SOME t) => box [string x, space, string "of", space, p_con env t])
|
adamc@156
|
558 cons]
|
adamc@156
|
559 end
|
adamc@156
|
560
|
adamc@447
|
561 fun p_named x n =
|
adamc@447
|
562 if !debug then
|
adamc@447
|
563 box [string x,
|
adamc@447
|
564 string "__",
|
adamc@447
|
565 string (Int.toString n)]
|
adamc@447
|
566 else
|
adamc@447
|
567 string x
|
adamc@447
|
568
|
adamc@805
|
569 fun p_sgn_item env (sgiAll as (sgi, _)) =
|
adamc@31
|
570 case sgi of
|
adamc@31
|
571 SgiConAbs (x, n, k) => box [string "con",
|
adamc@31
|
572 space,
|
adamc@31
|
573 p_named x n,
|
adamc@31
|
574 space,
|
adamc@31
|
575 string "::",
|
adamc@31
|
576 space,
|
adamc@623
|
577 p_kind env k]
|
adamc@31
|
578 | SgiCon (x, n, k, c) => box [string "con",
|
adamc@31
|
579 space,
|
adamc@31
|
580 p_named x n,
|
adamc@31
|
581 space,
|
adamc@31
|
582 string "::",
|
adamc@31
|
583 space,
|
adamc@623
|
584 p_kind env k,
|
adamc@31
|
585 space,
|
adamc@31
|
586 string "=",
|
adamc@31
|
587 space,
|
adamc@31
|
588 p_con env c]
|
adamc@805
|
589 | SgiDatatype x => box [string "datatype",
|
adamc@805
|
590 space,
|
adamc@805
|
591 p_list_sep (box [space, string "and", space]) (p_datatype (E.sgiBinds env sgiAll)) x]
|
adamc@191
|
592 | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
|
adamc@156
|
593 let
|
adamc@156
|
594 val m1x = #1 (E.lookupStrNamed env m1)
|
adamc@156
|
595 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
|
adamc@156
|
596 in
|
adamc@156
|
597 box [string "datatype",
|
adamc@156
|
598 space,
|
adamc@156
|
599 string x,
|
adamc@156
|
600 space,
|
adamc@156
|
601 string "=",
|
adamc@156
|
602 space,
|
adamc@156
|
603 string "datatype",
|
adamc@156
|
604 space,
|
adamc@156
|
605 p_list_sep (string ".") string (m1x :: ms @ [x'])]
|
adamc@156
|
606 end
|
adamc@31
|
607 | SgiVal (x, n, c) => box [string "val",
|
adamc@31
|
608 space,
|
adamc@31
|
609 p_named x n,
|
adamc@31
|
610 space,
|
adamc@31
|
611 string ":",
|
adamc@31
|
612 space,
|
adamc@31
|
613 p_con env c]
|
adamc@31
|
614 | SgiStr (x, n, sgn) => box [string "structure",
|
adamc@31
|
615 space,
|
adamc@31
|
616 p_named x n,
|
adamc@31
|
617 space,
|
adamc@31
|
618 string ":",
|
adamc@31
|
619 space,
|
adamc@31
|
620 p_sgn env sgn]
|
adamc@59
|
621 | SgiSgn (x, n, sgn) => box [string "signature",
|
adamc@59
|
622 space,
|
adamc@59
|
623 p_named x n,
|
adamc@59
|
624 space,
|
adamc@59
|
625 string "=",
|
adamc@59
|
626 space,
|
adamc@59
|
627 p_sgn env sgn]
|
adamc@88
|
628 | SgiConstraint (c1, c2) => box [string "constraint",
|
adamc@88
|
629 space,
|
adamc@88
|
630 p_con env c1,
|
adamc@88
|
631 space,
|
adamc@88
|
632 string "~",
|
adamc@88
|
633 space,
|
adamc@88
|
634 p_con env c2]
|
adamc@563
|
635 | SgiClassAbs (x, n, k) => box [string "class",
|
adamc@563
|
636 space,
|
adamc@563
|
637 p_named x n,
|
adamc@563
|
638 space,
|
adamc@563
|
639 string "::",
|
adamc@563
|
640 space,
|
adamc@623
|
641 p_kind env k]
|
adamc@563
|
642 | SgiClass (x, n, k, c) => box [string "class",
|
adamc@563
|
643 space,
|
adamc@563
|
644 p_named x n,
|
adamc@563
|
645 space,
|
adamc@563
|
646 string "::",
|
adamc@563
|
647 space,
|
adamc@623
|
648 p_kind env k,
|
adamc@563
|
649 space,
|
adamc@563
|
650 string "=",
|
adamc@563
|
651 space,
|
adamc@563
|
652 p_con env c]
|
adamc@31
|
653
|
adamc@31
|
654 and p_sgn env (sgn, _) =
|
adamc@31
|
655 case sgn of
|
adamc@31
|
656 SgnConst sgis => box [string "sig",
|
adamc@31
|
657 newline,
|
adamc@32
|
658 let
|
adamc@32
|
659 val (psgis, _) = ListUtil.foldlMap (fn (sgi, env) =>
|
adamc@32
|
660 (p_sgn_item env sgi,
|
adamc@32
|
661 E.sgiBinds env sgi))
|
adamc@32
|
662 env sgis
|
adamc@32
|
663 in
|
adamc@32
|
664 p_list_sep newline (fn x => x) psgis
|
adamc@32
|
665 end,
|
adamc@31
|
666 newline,
|
adamc@31
|
667 string "end"]
|
adamc@88
|
668 | SgnVar n => ((string (#1 (E.lookupSgnNamed env n)))
|
adamc@88
|
669 handle E.UnboundNamed _ => string ("UNBOUND_SGN_" ^ Int.toString n))
|
adamc@41
|
670 | SgnFun (x, n, sgn, sgn') => box [string "functor",
|
adamc@41
|
671 space,
|
adamc@41
|
672 string "(",
|
adamc@41
|
673 string x,
|
adamc@41
|
674 space,
|
adamc@41
|
675 string ":",
|
adamc@41
|
676 space,
|
adamc@41
|
677 p_sgn env sgn,
|
adamc@41
|
678 string ")",
|
adamc@41
|
679 space,
|
adamc@41
|
680 string ":",
|
adamc@41
|
681 space,
|
adamc@41
|
682 p_sgn (E.pushStrNamedAs env x n sgn) sgn']
|
adam@1864
|
683 | SgnWhere (sgn, ms, x, c) => box [p_sgn env sgn,
|
adam@1864
|
684 space,
|
adam@1864
|
685 string "where",
|
adam@1864
|
686 space,
|
adam@1864
|
687 string "con",
|
adam@1864
|
688 space,
|
adam@1864
|
689 p_list_sep (string ".") string (ms @ [x]),
|
adam@1864
|
690 space,
|
adam@1864
|
691 string "=",
|
adam@1864
|
692 space,
|
adam@1864
|
693 p_con env c]
|
adamc@59
|
694 | SgnProj (m1, ms, x) =>
|
adamc@59
|
695 let
|
adamc@88
|
696 val m1x = #1 (E.lookupStrNamed env m1)
|
adamc@88
|
697 handle E.UnboundNamed _ => "UNBOUND_SGN_" ^ Int.toString m1
|
adamc@88
|
698
|
adamc@59
|
699 val m1s = if !debug then
|
adamc@59
|
700 m1x ^ "__" ^ Int.toString m1
|
adamc@59
|
701 else
|
adamc@59
|
702 m1x
|
adamc@88
|
703 in
|
adamc@59
|
704 p_list_sep (string ".") string (m1x :: ms @ [x])
|
adamc@59
|
705 end
|
adamc@31
|
706 | SgnError => string "<ERROR>"
|
adamc@31
|
707
|
adamc@123
|
708 fun p_vali env (x, n, t, e) = box [p_named x n,
|
adamc@123
|
709 space,
|
adamc@123
|
710 string ":",
|
adamc@123
|
711 space,
|
adamc@123
|
712 p_con env t,
|
adamc@123
|
713 space,
|
adamc@123
|
714 string "=",
|
adamc@123
|
715 space,
|
adamc@123
|
716 p_exp env e]
|
adamc@123
|
717
|
adamc@447
|
718
|
adamc@447
|
719
|
adamc@123
|
720 fun p_decl env (dAll as (d, _) : decl) =
|
adamc@3
|
721 case d of
|
adamc@31
|
722 DCon (x, n, k, c) => box [string "con",
|
adamc@31
|
723 space,
|
adamc@31
|
724 p_named x n,
|
adamc@31
|
725 space,
|
adamc@31
|
726 string "::",
|
adamc@31
|
727 space,
|
adamc@623
|
728 p_kind env k,
|
adamc@31
|
729 space,
|
adamc@31
|
730 string "=",
|
adamc@31
|
731 space,
|
adamc@31
|
732 p_con env c]
|
adamc@805
|
733 | DDatatype x => box [string "datatype",
|
adamc@805
|
734 space,
|
adamc@805
|
735 p_list_sep (box [space, string "and", space]) (p_datatype (E.declBinds env dAll)) x]
|
adamc@191
|
736 | DDatatypeImp (x, _, m1, ms, x', _, _) =>
|
adamc@156
|
737 let
|
adamc@156
|
738 val m1x = #1 (E.lookupStrNamed env m1)
|
adamc@156
|
739 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
|
adamc@156
|
740 in
|
adamc@156
|
741 box [string "datatype",
|
adamc@156
|
742 space,
|
adamc@156
|
743 string x,
|
adamc@156
|
744 space,
|
adamc@156
|
745 string "=",
|
adamc@156
|
746 space,
|
adamc@156
|
747 string "datatype",
|
adamc@156
|
748 space,
|
adamc@156
|
749 p_list_sep (string ".") string (m1x :: ms @ [x'])]
|
adamc@156
|
750 end
|
adamc@123
|
751 | DVal vi => box [string "val",
|
adamc@123
|
752 space,
|
adamc@123
|
753 p_vali env vi]
|
adamc@123
|
754 | DValRec vis =>
|
adamc@123
|
755 let
|
adamc@123
|
756 val env = E.declBinds env dAll
|
adamc@123
|
757 in
|
adamc@123
|
758 box [string "val",
|
adamc@123
|
759 space,
|
adamc@123
|
760 string "rec",
|
adamc@123
|
761 space,
|
adamc@123
|
762 p_list_sep (box [newline, string "and", space]) (p_vali env) vis]
|
adamc@123
|
763 end
|
adamc@31
|
764
|
adamc@31
|
765 | DSgn (x, n, sgn) => box [string "signature",
|
adamc@31
|
766 space,
|
adamc@31
|
767 p_named x n,
|
adamc@31
|
768 space,
|
adamc@31
|
769 string "=",
|
adamc@31
|
770 space,
|
adamc@31
|
771 p_sgn env sgn]
|
adamc@31
|
772 | DStr (x, n, sgn, str) => box [string "structure",
|
adamc@31
|
773 space,
|
adamc@31
|
774 p_named x n,
|
adamc@31
|
775 space,
|
adamc@31
|
776 string ":",
|
adamc@31
|
777 space,
|
adamc@31
|
778 p_sgn env sgn,
|
adamc@31
|
779 space,
|
adamc@31
|
780 string "=",
|
adamc@31
|
781 space,
|
adamc@31
|
782 p_str env str]
|
adamc@48
|
783 | DFfiStr (x, n, sgn) => box [string "extern",
|
adamc@48
|
784 space,
|
adamc@48
|
785 string "structure",
|
adamc@48
|
786 space,
|
adamc@48
|
787 p_named x n,
|
adamc@48
|
788 space,
|
adamc@48
|
789 string ":",
|
adamc@48
|
790 space,
|
adamc@48
|
791 p_sgn env sgn]
|
adamc@88
|
792 | DConstraint (c1, c2) => box [string "constraint",
|
adamc@88
|
793 space,
|
adamc@88
|
794 p_con env c1,
|
adamc@88
|
795 space,
|
adamc@88
|
796 string "~",
|
adamc@88
|
797 space,
|
adamc@88
|
798 p_con env c2]
|
adamc@109
|
799 | DExport (_, sgn, str) => box [string "export",
|
adamc@110
|
800 space,
|
adamc@109
|
801 p_str env str,
|
adamc@109
|
802 space,
|
adamc@109
|
803 string ":",
|
adamc@109
|
804 space,
|
adamc@109
|
805 p_sgn env sgn]
|
adamc@707
|
806 | DTable (_, x, n, c, pe, _, ce, _) => box [string "table",
|
adamc@707
|
807 space,
|
adamc@707
|
808 p_named x n,
|
adamc@707
|
809 space,
|
adamc@707
|
810 string ":",
|
adamc@707
|
811 space,
|
adamc@707
|
812 p_con env c,
|
adamc@707
|
813 space,
|
adamc@707
|
814 string "keys",
|
adamc@707
|
815 space,
|
adamc@707
|
816 p_exp env pe,
|
adamc@707
|
817 space,
|
adamc@707
|
818 string "constraints",
|
adamc@707
|
819 space,
|
adamc@707
|
820 p_exp env ce]
|
adamc@338
|
821 | DSequence (_, x, n) => box [string "sequence",
|
adamc@338
|
822 space,
|
adamc@338
|
823 p_named x n]
|
adamc@754
|
824 | DView (_, x, n, e, _) => box [string "view",
|
adamc@754
|
825 space,
|
adamc@754
|
826 p_named x n,
|
adamc@754
|
827 space,
|
adamc@754
|
828 string "as",
|
adamc@754
|
829 space,
|
adamc@754
|
830 p_exp env e]
|
adamc@271
|
831 | DDatabase s => box [string "database",
|
adamc@271
|
832 space,
|
adamc@271
|
833 string s]
|
adamc@459
|
834 | DCookie (_, x, n, c) => box [string "cookie",
|
adamc@459
|
835 space,
|
adamc@459
|
836 p_named x n,
|
adamc@459
|
837 space,
|
adamc@459
|
838 string ":",
|
adamc@459
|
839 space,
|
adamc@459
|
840 p_con env c]
|
adamc@720
|
841 | DStyle (_, x, n) => box [string "style",
|
adamc@720
|
842 space,
|
adamc@720
|
843 p_named x n]
|
adamc@1075
|
844 | DTask (e1, e2) => box [string "task",
|
adamc@1073
|
845 space,
|
adamc@1075
|
846 p_exp env e1,
|
adamc@1075
|
847 space,
|
adamc@1075
|
848 string "=",
|
adamc@1075
|
849 space,
|
adamc@1075
|
850 p_exp env e2]
|
adamc@1199
|
851 | DPolicy e1 => box [string "policy",
|
adamc@1199
|
852 space,
|
adamc@1199
|
853 p_exp env e1]
|
adam@1294
|
854 | DOnError _ => string "ONERROR"
|
adamc@31
|
855
|
adamc@31
|
856 and p_str env (str, _) =
|
adamc@31
|
857 case str of
|
adamc@31
|
858 StrConst ds => box [string "struct",
|
adamc@31
|
859 newline,
|
adamc@32
|
860 p_file env ds,
|
adamc@31
|
861 newline,
|
adamc@31
|
862 string "end"]
|
adamc@88
|
863 | StrVar n => ((string (#1 (E.lookupStrNamed env n)))
|
adamc@88
|
864 handle E.UnboundNamed _ => string ("UNBOUND_STR_" ^ Int.toString n))
|
adamc@34
|
865 | StrProj (str, s) => box [p_str env str,
|
adamc@34
|
866 string ".",
|
adamc@34
|
867 string s]
|
adamc@41
|
868 | StrFun (x, n, sgn, sgn', str) =>
|
adamc@41
|
869 let
|
adamc@41
|
870 val env' = E.pushStrNamedAs env x n sgn
|
adamc@41
|
871 in
|
adamc@41
|
872 box [string "functor",
|
adamc@41
|
873 space,
|
adamc@41
|
874 string "(",
|
adamc@41
|
875 string x,
|
adamc@41
|
876 space,
|
adamc@41
|
877 string ":",
|
adamc@41
|
878 space,
|
adamc@41
|
879 p_sgn env sgn,
|
adamc@41
|
880 string ")",
|
adamc@41
|
881 space,
|
adamc@41
|
882 string ":",
|
adamc@41
|
883 space,
|
adamc@41
|
884 p_sgn env' sgn',
|
adamc@41
|
885 space,
|
adamc@41
|
886 string "=>",
|
adamc@41
|
887 space,
|
adamc@41
|
888 p_str env' str]
|
adamc@41
|
889 end
|
adamc@44
|
890 | StrApp (str1, str2) => box [p_str env str1,
|
adamc@44
|
891 string "(",
|
adamc@44
|
892 p_str env str2,
|
adamc@44
|
893 string ")"]
|
adamc@31
|
894 | StrError => string "<ERROR>"
|
adamc@3
|
895
|
adamc@32
|
896 and p_file env file =
|
adamc@3
|
897 let
|
adamc@31
|
898 val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
|
adamc@31
|
899 (p_decl env d,
|
adamc@31
|
900 E.declBinds env d))
|
adamc@31
|
901 env file
|
adamc@3
|
902 in
|
adamc@3
|
903 p_list_sep newline (fn x => x) pds
|
adamc@3
|
904 end
|
adamc@3
|
905
|
adamc@3
|
906 end
|