Mercurial > urweb

comparison src/expl_print.sml @ 38:d16ef24de78b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Explify
author Adam Chlipala <adamc@hcoop.net>
date Thu, 19 Jun 2008 10:06:59 -0400
parents
children 3c1ce1b4eb3d
comparison
equal deleted inserted replaced
37:367f058aba23 38:d16ef24de78b
1 (* Copyright (c) 2008, Adam Chlipala
2 * All rights reserved.
3 *
4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met:
6 *
7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission.
14 *
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE.
26 *)
27
28 (* Pretty-printing elaborated Laconic/Web *)
29
30 structure ExplPrint :> EXPL_PRINT = struct
31
32 open Print.PD
33 open Print
34
35 open Expl
36
37 structure E = ExplEnv
38
39 val debug = ref false
40
41 fun p_kind' par (k, _) =
42 case k of
43 KType => string "Type"
44 | KArrow (k1, k2) => parenIf par (box [p_kind' true k1,
45 space,
46 string "->",
47 space,
48 p_kind k2])
49 | KName => string "Name"
50 | KRecord k => box [string "{", p_kind k, string "}"]
51
52 and p_kind k = p_kind' false k
53
54 fun p_con' par env (c, _) =
55 case c of
56 TFun (t1, t2) => parenIf par (box [p_con' true env t1,
57 space,
58 string "->",
59 space,
60 p_con env t2])
61 | TCFun (x, k, c) => parenIf par (box [string x,
62 space,
63 string "::",
64 space,
65 p_kind k,
66 space,
67 string "->",
68 space,
69 p_con (E.pushCRel env x k) c])
70 | TRecord (CRecord (_, xcs), _) => box [string "{",
71 p_list (fn (x, c) =>
72 box [p_name env x,
73 space,
74 string ":",
75 space,
76 p_con env c]) xcs,
77 string "}"]
78 | TRecord c => box [string "$",
79 p_con' true env c]
80
81 | CRel n =>
82 if !debug then
83 string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n)
84 else
85 string (#1 (E.lookupCRel env n))
86 | CNamed n =>
87 ((if !debug then
88 string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
89 else
90 string (#1 (E.lookupCNamed env n)))
91 handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
92 | CModProj (m1, ms, x) =>
93 let
94 val (m1x, sgn) = E.lookupStrNamed env m1
95
96 val m1s = if !debug then
97 m1x ^ "__" ^ Int.toString m1
98 else
99 m1x
100 in
101 p_list_sep (string ".") string (m1x :: ms @ [x])
102 end
103
104 | CApp (c1, c2) => parenIf par (box [p_con env c1,
105 space,
106 p_con' true env c2])
107 | CAbs (x, k, c) => parenIf par (box [string "fn",
108 space,
109 string x,
110 space,
111 string "::",
112 space,
113 p_kind k,
114 space,
115 string "=>",
116 space,
117 p_con (E.pushCRel env x k) c])
118
119 | CName s => box [string "#", string s]
120
121 | CRecord (k, xcs) =>
122 if !debug then
123 parenIf par (box [string "[",
124 p_list (fn (x, c) =>
125 box [p_con env x,
126 space,
127 string "=",
128 space,
129 p_con env c]) xcs,
130 string "]::",
131 p_kind k])
132 else
133 parenIf par (box [string "[",
134 p_list (fn (x, c) =>
135 box [p_con env x,
136 space,
137 string "=",
138 space,
139 p_con env c]) xcs,
140 string "]"])
141 | CConcat (c1, c2) => parenIf par (box [p_con' true env c1,
142 space,
143 string "++",
144 space,
145 p_con env c2])
146
147 and p_con env = p_con' false env
148
149 and p_name env (all as (c, _)) =
150 case c of
151 CName s => string s
152 | _ => p_con env all
153
154 fun p_exp' par env (e, _) =
155 case e of
156 EPrim p => Prim.p_t p
157 | ERel n =>
158 if !debug then
159 string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n)
160 else
161 string (#1 (E.lookupERel env n))
162 | ENamed n =>
163 if !debug then
164 string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
165 else
166 string (#1 (E.lookupENamed env n))
167 | EModProj (m1, ms, x) =>
168 let
169 val (m1x, sgn) = E.lookupStrNamed env m1
170
171 val m1s = if !debug then
172 m1x ^ "__" ^ Int.toString m1
173 else
174 m1x
175 in
176 p_list_sep (string ".") string (m1x :: ms @ [x])
177 end
178
179 | EApp (e1, e2) => parenIf par (box [p_exp env e1,
180 space,
181 p_exp' true env e2])
182 | EAbs (x, t, _, e) => parenIf par (box [string "fn",
183 space,
184 string x,
185 space,
186 string ":",
187 space,
188 p_con env t,
189 space,
190 string "=>",
191 space,
192 p_exp (E.pushERel env x t) e])
193 | ECApp (e, c) => parenIf par (box [p_exp env e,
194 space,
195 string "[",
196 p_con env c,
197 string "]"])
198 | ECAbs (x, k, e) => parenIf par (box [string "fn",
199 space,
200 string x,
201 space,
202 string "::",
203 space,
204 p_kind k,
205 space,
206 string "=>",
207 space,
208 p_exp (E.pushCRel env x k) e])
209
210 | ERecord xes => box [string "{",
211 p_list (fn (x, e, _) =>
212 box [p_name env x,
213 space,
214 string "=",
215 space,
216 p_exp env e]) xes,
217 string "}"]
218 | EField (e, c, {field, rest}) =>
219 if !debug then
220 box [p_exp' true env e,
221 string ".",
222 p_con' true env c,
223 space,
224 string "[",
225 p_con env field,
226 space,
227 string " in ",
228 space,
229 p_con env rest,
230 string "]"]
231 else
232 box [p_exp' true env e,
233 string ".",
234 p_con' true env c]
235
236 and p_exp env = p_exp' false env
237
238 fun p_named x n =
239 if !debug then
240 box [string x,
241 string "__",
242 string (Int.toString n)]
243 else
244 string x
245
246 fun p_sgn_item env (sgi, _) =
247 case sgi of
248 SgiConAbs (x, n, k) => box [string "con",
249 space,
250 p_named x n,
251 space,
252 string "::",
253 space,
254 p_kind k]
255 | SgiCon (x, n, k, c) => box [string "con",
256 space,
257 p_named x n,
258 space,
259 string "::",
260 space,
261 p_kind k,
262 space,
263 string "=",
264 space,
265 p_con env c]
266 | SgiVal (x, n, c) => box [string "val",
267 space,
268 p_named x n,
269 space,
270 string ":",
271 space,
272 p_con env c]
273 | SgiStr (x, n, sgn) => box [string "structure",
274 space,
275 p_named x n,
276 space,
277 string ":",
278 space,
279 p_sgn env sgn]
280
281 and p_sgn env (sgn, _) =
282 case sgn of
283 SgnConst sgis => box [string "sig",
284 newline,
285 let
286 val (psgis, _) = ListUtil.foldlMap (fn (sgi, env) =>
287 (p_sgn_item env sgi,
288 E.sgiBinds env sgi))
289 env sgis
290 in
291 p_list_sep newline (fn x => x) psgis
292 end,
293 newline,
294 string "end"]
295 | SgnVar n => string (#1 (E.lookupSgnNamed env n))
296
297 fun p_decl env ((d, _) : decl) =
298 case d of
299 DCon (x, n, k, c) => box [string "con",
300 space,
301 p_named x n,
302 space,
303 string "::",
304 space,
305 p_kind k,
306 space,
307 string "=",
308 space,
309 p_con env c]
310 | DVal (x, n, t, e) => box [string "val",
311 space,
312 p_named x n,
313 space,
314 string ":",
315 space,
316 p_con env t,
317 space,
318 string "=",
319 space,
320 p_exp env e]
321
322 | DSgn (x, n, sgn) => box [string "signature",
323 space,
324 p_named x n,
325 space,
326 string "=",
327 space,
328 p_sgn env sgn]
329 | DStr (x, n, sgn, str) => box [string "structure",
330 space,
331 p_named x n,
332 space,
333 string ":",
334 space,
335 p_sgn env sgn,
336 space,
337 string "=",
338 space,
339 p_str env str]
340
341 and p_str env (str, _) =
342 case str of
343 StrConst ds => box [string "struct",
344 newline,
345 p_file env ds,
346 newline,
347 string "end"]
348 | StrVar n => string (#1 (E.lookupStrNamed env n))
349 | StrProj (str, s) => box [p_str env str,
350 string ".",
351 string s]
352
353 and p_file env file =
354 let
355 val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
356 (p_decl env d,
357 E.declBinds env d))
358 env file
359 in
360 p_list_sep newline (fn x => x) pds
361 end
362
363 end