adamc@16
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@16
|
2 * All rights reserved.
|
adamc@16
|
3 *
|
adamc@16
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@16
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@16
|
6 *
|
adamc@16
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@16
|
8 * this list of conditions and the following disclaimer.
|
adamc@16
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@16
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@16
|
11 * and/or other materials provided with the distribution.
|
adamc@16
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@16
|
13 * derived from this software without specific prior written permission.
|
adamc@16
|
14 *
|
adamc@16
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@16
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@16
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@16
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@16
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@16
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@16
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@16
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@16
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@16
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@16
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@16
|
26 *)
|
adamc@16
|
27
|
adamc@16
|
28 structure CoreUtil :> CORE_UTIL = struct
|
adamc@16
|
29
|
adamc@16
|
30 open Core
|
adamc@16
|
31
|
adamc@188
|
32 fun classifyDatatype xncs =
|
adamc@188
|
33 if List.all (fn (_, _, NONE) => true | _ => false) xncs then
|
adamc@188
|
34 Enum
|
adamc@188
|
35 else
|
adamc@188
|
36 Default
|
adamc@188
|
37
|
adamc@16
|
38 structure S = Search
|
adamc@16
|
39
|
adamc@16
|
40 structure Kind = struct
|
adamc@16
|
41
|
adamc@16
|
42 fun mapfold f =
|
adamc@16
|
43 let
|
adamc@16
|
44 fun mfk k acc =
|
adamc@16
|
45 S.bindP (mfk' k acc, f)
|
adamc@16
|
46
|
adamc@16
|
47 and mfk' (kAll as (k, loc)) =
|
adamc@16
|
48 case k of
|
adamc@16
|
49 KType => S.return2 kAll
|
adamc@16
|
50
|
adamc@16
|
51 | KArrow (k1, k2) =>
|
adamc@16
|
52 S.bind2 (mfk k1,
|
adamc@16
|
53 fn k1' =>
|
adamc@16
|
54 S.map2 (mfk k2,
|
adamc@16
|
55 fn k2' =>
|
adamc@16
|
56 (KArrow (k1', k2'), loc)))
|
adamc@16
|
57
|
adamc@16
|
58 | KName => S.return2 kAll
|
adamc@16
|
59
|
adamc@16
|
60 | KRecord k =>
|
adamc@16
|
61 S.map2 (mfk k,
|
adamc@16
|
62 fn k' =>
|
adamc@16
|
63 (KRecord k', loc))
|
adamc@87
|
64
|
adamc@87
|
65 | KUnit => S.return2 kAll
|
adamc@16
|
66 in
|
adamc@16
|
67 mfk
|
adamc@16
|
68 end
|
adamc@16
|
69
|
adamc@16
|
70 fun map f k =
|
adamc@16
|
71 case mapfold (fn k => fn () => S.Continue (f k, ())) k () of
|
adamc@16
|
72 S.Return () => raise Fail "Core_util.Kind.map"
|
adamc@16
|
73 | S.Continue (k, ()) => k
|
adamc@16
|
74
|
adamc@16
|
75 fun exists f k =
|
adamc@16
|
76 case mapfold (fn k => fn () =>
|
adamc@16
|
77 if f k then
|
adamc@16
|
78 S.Return ()
|
adamc@16
|
79 else
|
adamc@16
|
80 S.Continue (k, ())) k () of
|
adamc@16
|
81 S.Return _ => true
|
adamc@16
|
82 | S.Continue _ => false
|
adamc@16
|
83
|
adamc@16
|
84 end
|
adamc@16
|
85
|
adamc@16
|
86 structure Con = struct
|
adamc@16
|
87
|
adamc@16
|
88 datatype binder =
|
adamc@16
|
89 Rel of string * kind
|
adamc@20
|
90 | Named of string * int * kind * con option
|
adamc@16
|
91
|
adamc@16
|
92 fun mapfoldB {kind = fk, con = fc, bind} =
|
adamc@16
|
93 let
|
adamc@16
|
94 val mfk = Kind.mapfold fk
|
adamc@16
|
95
|
adamc@16
|
96 fun mfc ctx c acc =
|
adamc@16
|
97 S.bindP (mfc' ctx c acc, fc ctx)
|
adamc@16
|
98
|
adamc@16
|
99 and mfc' ctx (cAll as (c, loc)) =
|
adamc@16
|
100 case c of
|
adamc@16
|
101 TFun (c1, c2) =>
|
adamc@16
|
102 S.bind2 (mfc ctx c1,
|
adamc@16
|
103 fn c1' =>
|
adamc@16
|
104 S.map2 (mfc ctx c2,
|
adamc@16
|
105 fn c2' =>
|
adamc@16
|
106 (TFun (c1', c2'), loc)))
|
adamc@16
|
107 | TCFun (x, k, c) =>
|
adamc@16
|
108 S.bind2 (mfk k,
|
adamc@16
|
109 fn k' =>
|
adamc@16
|
110 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
|
adamc@16
|
111 fn c' =>
|
adamc@16
|
112 (TCFun (x, k', c'), loc)))
|
adamc@16
|
113 | TRecord c =>
|
adamc@16
|
114 S.map2 (mfc ctx c,
|
adamc@16
|
115 fn c' =>
|
adamc@16
|
116 (TRecord c', loc))
|
adamc@16
|
117
|
adamc@16
|
118 | CRel _ => S.return2 cAll
|
adamc@16
|
119 | CNamed _ => S.return2 cAll
|
adamc@48
|
120 | CFfi _ => S.return2 cAll
|
adamc@16
|
121 | CApp (c1, c2) =>
|
adamc@16
|
122 S.bind2 (mfc ctx c1,
|
adamc@16
|
123 fn c1' =>
|
adamc@16
|
124 S.map2 (mfc ctx c2,
|
adamc@16
|
125 fn c2' =>
|
adamc@16
|
126 (CApp (c1', c2'), loc)))
|
adamc@16
|
127 | CAbs (x, k, c) =>
|
adamc@16
|
128 S.bind2 (mfk k,
|
adamc@16
|
129 fn k' =>
|
adamc@16
|
130 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
|
adamc@16
|
131 fn c' =>
|
adamc@16
|
132 (CAbs (x, k', c'), loc)))
|
adamc@16
|
133
|
adamc@16
|
134 | CName _ => S.return2 cAll
|
adamc@16
|
135
|
adamc@16
|
136 | CRecord (k, xcs) =>
|
adamc@16
|
137 S.bind2 (mfk k,
|
adamc@16
|
138 fn k' =>
|
adamc@16
|
139 S.map2 (ListUtil.mapfold (fn (x, c) =>
|
adamc@16
|
140 S.bind2 (mfc ctx x,
|
adamc@16
|
141 fn x' =>
|
adamc@16
|
142 S.map2 (mfc ctx c,
|
adamc@16
|
143 fn c' =>
|
adamc@16
|
144 (x', c'))))
|
adamc@16
|
145 xcs,
|
adamc@16
|
146 fn xcs' =>
|
adamc@16
|
147 (CRecord (k', xcs'), loc)))
|
adamc@16
|
148 | CConcat (c1, c2) =>
|
adamc@16
|
149 S.bind2 (mfc ctx c1,
|
adamc@16
|
150 fn c1' =>
|
adamc@16
|
151 S.map2 (mfc ctx c2,
|
adamc@16
|
152 fn c2' =>
|
adamc@16
|
153 (CConcat (c1', c2'), loc)))
|
adamc@69
|
154 | CFold (k1, k2) =>
|
adamc@69
|
155 S.bind2 (mfk k1,
|
adamc@69
|
156 fn k1' =>
|
adamc@69
|
157 S.map2 (mfk k2,
|
adamc@69
|
158 fn k2' =>
|
adamc@69
|
159 (CFold (k1', k2'), loc)))
|
adamc@87
|
160
|
adamc@87
|
161 | CUnit => S.return2 cAll
|
adamc@16
|
162 in
|
adamc@16
|
163 mfc
|
adamc@16
|
164 end
|
adamc@16
|
165
|
adamc@16
|
166 fun mapfold {kind = fk, con = fc} =
|
adamc@16
|
167 mapfoldB {kind = fk,
|
adamc@16
|
168 con = fn () => fc,
|
adamc@16
|
169 bind = fn ((), _) => ()} ()
|
adamc@16
|
170
|
adamc@16
|
171 fun map {kind, con} c =
|
adamc@16
|
172 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@16
|
173 con = fn c => fn () => S.Continue (con c, ())} c () of
|
adamc@16
|
174 S.Return () => raise Fail "Core_util.Con.map"
|
adamc@16
|
175 | S.Continue (c, ()) => c
|
adamc@16
|
176
|
adamc@16
|
177 fun mapB {kind, con, bind} ctx c =
|
adamc@16
|
178 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@16
|
179 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
|
adamc@16
|
180 bind = bind} ctx c () of
|
adamc@16
|
181 S.Continue (c, ()) => c
|
adamc@20
|
182 | S.Return _ => raise Fail "CoreUtil.Con.mapB: Impossible"
|
adamc@16
|
183
|
adamc@23
|
184 fun fold {kind, con} s c =
|
adamc@23
|
185 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
|
adamc@23
|
186 con = fn c => fn s => S.Continue (c, con (c, s))} c s of
|
adamc@23
|
187 S.Continue (_, s) => s
|
adamc@23
|
188 | S.Return _ => raise Fail "CoreUtil.Con.fold: Impossible"
|
adamc@23
|
189
|
adamc@16
|
190 fun exists {kind, con} k =
|
adamc@16
|
191 case mapfold {kind = fn k => fn () =>
|
adamc@16
|
192 if kind k then
|
adamc@16
|
193 S.Return ()
|
adamc@16
|
194 else
|
adamc@16
|
195 S.Continue (k, ()),
|
adamc@16
|
196 con = fn c => fn () =>
|
adamc@16
|
197 if con c then
|
adamc@16
|
198 S.Return ()
|
adamc@16
|
199 else
|
adamc@16
|
200 S.Continue (c, ())} k () of
|
adamc@16
|
201 S.Return _ => true
|
adamc@16
|
202 | S.Continue _ => false
|
adamc@16
|
203
|
adamc@16
|
204 end
|
adamc@16
|
205
|
adamc@16
|
206 structure Exp = struct
|
adamc@16
|
207
|
adamc@16
|
208 datatype binder =
|
adamc@16
|
209 RelC of string * kind
|
adamc@20
|
210 | NamedC of string * int * kind * con option
|
adamc@16
|
211 | RelE of string * con
|
adamc@109
|
212 | NamedE of string * int * con * exp option * string
|
adamc@16
|
213
|
adamc@16
|
214 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
|
adamc@16
|
215 let
|
adamc@16
|
216 val mfk = Kind.mapfold fk
|
adamc@16
|
217
|
adamc@16
|
218 fun bind' (ctx, b) =
|
adamc@16
|
219 let
|
adamc@16
|
220 val b' = case b of
|
adamc@16
|
221 Con.Rel x => RelC x
|
adamc@16
|
222 | Con.Named x => NamedC x
|
adamc@16
|
223 in
|
adamc@16
|
224 bind (ctx, b')
|
adamc@16
|
225 end
|
adamc@16
|
226 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
|
adamc@16
|
227
|
adamc@16
|
228 fun mfe ctx e acc =
|
adamc@16
|
229 S.bindP (mfe' ctx e acc, fe ctx)
|
adamc@16
|
230
|
adamc@16
|
231 and mfe' ctx (eAll as (e, loc)) =
|
adamc@16
|
232 case e of
|
adamc@16
|
233 EPrim _ => S.return2 eAll
|
adamc@16
|
234 | ERel _ => S.return2 eAll
|
adamc@16
|
235 | ENamed _ => S.return2 eAll
|
adamc@188
|
236 | ECon (_, _, NONE) => S.return2 eAll
|
adamc@188
|
237 | ECon (dk, n, SOME e) =>
|
adamc@177
|
238 S.map2 (mfe ctx e,
|
adamc@177
|
239 fn e' =>
|
adamc@188
|
240 (ECon (dk, n, SOME e'), loc))
|
adamc@48
|
241 | EFfi _ => S.return2 eAll
|
adamc@48
|
242 | EFfiApp (m, x, es) =>
|
adamc@48
|
243 S.map2 (ListUtil.mapfold (fn e => mfe ctx e) es,
|
adamc@48
|
244 fn es' =>
|
adamc@48
|
245 (EFfiApp (m, x, es'), loc))
|
adamc@16
|
246 | EApp (e1, e2) =>
|
adamc@16
|
247 S.bind2 (mfe ctx e1,
|
adamc@16
|
248 fn e1' =>
|
adamc@16
|
249 S.map2 (mfe ctx e2,
|
adamc@16
|
250 fn e2' =>
|
adamc@16
|
251 (EApp (e1', e2'), loc)))
|
adamc@26
|
252 | EAbs (x, dom, ran, e) =>
|
adamc@26
|
253 S.bind2 (mfc ctx dom,
|
adamc@26
|
254 fn dom' =>
|
adamc@26
|
255 S.bind2 (mfc ctx ran,
|
adamc@26
|
256 fn ran' =>
|
adamc@26
|
257 S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
|
adamc@26
|
258 fn e' =>
|
adamc@26
|
259 (EAbs (x, dom', ran', e'), loc))))
|
adamc@16
|
260
|
adamc@16
|
261 | ECApp (e, c) =>
|
adamc@16
|
262 S.bind2 (mfe ctx e,
|
adamc@16
|
263 fn e' =>
|
adamc@16
|
264 S.map2 (mfc ctx c,
|
adamc@16
|
265 fn c' =>
|
adamc@16
|
266 (ECApp (e', c'), loc)))
|
adamc@16
|
267 | ECAbs (x, k, e) =>
|
adamc@16
|
268 S.bind2 (mfk k,
|
adamc@16
|
269 fn k' =>
|
adamc@16
|
270 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
|
adamc@16
|
271 fn e' =>
|
adamc@16
|
272 (ECAbs (x, k', e'), loc)))
|
adamc@16
|
273
|
adamc@16
|
274 | ERecord xes =>
|
adamc@29
|
275 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
|
adamc@16
|
276 S.bind2 (mfc ctx x,
|
adamc@16
|
277 fn x' =>
|
adamc@29
|
278 S.bind2 (mfe ctx e,
|
adamc@29
|
279 fn e' =>
|
adamc@29
|
280 S.map2 (mfc ctx t,
|
adamc@29
|
281 fn t' =>
|
adamc@29
|
282 (x', e', t')))))
|
adamc@16
|
283 xes,
|
adamc@16
|
284 fn xes' =>
|
adamc@16
|
285 (ERecord xes', loc))
|
adamc@16
|
286 | EField (e, c, {field, rest}) =>
|
adamc@16
|
287 S.bind2 (mfe ctx e,
|
adamc@16
|
288 fn e' =>
|
adamc@16
|
289 S.bind2 (mfc ctx c,
|
adamc@16
|
290 fn c' =>
|
adamc@16
|
291 S.bind2 (mfc ctx field,
|
adamc@16
|
292 fn field' =>
|
adamc@16
|
293 S.map2 (mfc ctx rest,
|
adamc@16
|
294 fn rest' =>
|
adamc@16
|
295 (EField (e', c', {field = field', rest = rest'}), loc)))))
|
adamc@149
|
296 | ECut (e, c, {field, rest}) =>
|
adamc@149
|
297 S.bind2 (mfe ctx e,
|
adamc@149
|
298 fn e' =>
|
adamc@149
|
299 S.bind2 (mfc ctx c,
|
adamc@149
|
300 fn c' =>
|
adamc@149
|
301 S.bind2 (mfc ctx field,
|
adamc@149
|
302 fn field' =>
|
adamc@149
|
303 S.map2 (mfc ctx rest,
|
adamc@149
|
304 fn rest' =>
|
adamc@149
|
305 (ECut (e', c', {field = field', rest = rest'}), loc)))))
|
adamc@73
|
306 | EFold k =>
|
adamc@73
|
307 S.map2 (mfk k,
|
adamc@73
|
308 fn k' =>
|
adamc@73
|
309 (EFold k', loc))
|
adamc@102
|
310
|
adamc@182
|
311 | ECase (e, pes, {disc, result}) =>
|
adamc@177
|
312 S.bind2 (mfe ctx e,
|
adamc@177
|
313 fn e' =>
|
adamc@177
|
314 S.bind2 (ListUtil.mapfold (fn (p, e) =>
|
adamc@177
|
315 S.map2 (mfe ctx e,
|
adamc@177
|
316 fn e' => (p, e'))) pes,
|
adamc@177
|
317 fn pes' =>
|
adamc@182
|
318 S.bind2 (mfc ctx disc,
|
adamc@182
|
319 fn disc' =>
|
adamc@182
|
320 S.map2 (mfc ctx result,
|
adamc@182
|
321 fn result' =>
|
adamc@182
|
322 (ECase (e', pes', {disc = disc', result = result'}), loc)))))
|
adamc@177
|
323
|
adamc@102
|
324 | EWrite e =>
|
adamc@102
|
325 S.map2 (mfe ctx e,
|
adamc@102
|
326 fn e' =>
|
adamc@102
|
327 (EWrite e', loc))
|
adamc@110
|
328
|
adamc@110
|
329 | EClosure (n, es) =>
|
adamc@110
|
330 S.map2 (ListUtil.mapfold (mfe ctx) es,
|
adamc@110
|
331 fn es' =>
|
adamc@110
|
332 (EClosure (n, es'), loc))
|
adamc@16
|
333 in
|
adamc@16
|
334 mfe
|
adamc@16
|
335 end
|
adamc@16
|
336
|
adamc@16
|
337 fun mapfold {kind = fk, con = fc, exp = fe} =
|
adamc@16
|
338 mapfoldB {kind = fk,
|
adamc@16
|
339 con = fn () => fc,
|
adamc@16
|
340 exp = fn () => fe,
|
adamc@16
|
341 bind = fn ((), _) => ()} ()
|
adamc@16
|
342
|
adamc@21
|
343 fun mapB {kind, con, exp, bind} ctx e =
|
adamc@21
|
344 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@21
|
345 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
|
adamc@21
|
346 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
|
adamc@21
|
347 bind = bind} ctx e () of
|
adamc@21
|
348 S.Continue (e, ()) => e
|
adamc@21
|
349 | S.Return _ => raise Fail "CoreUtil.Exp.mapB: Impossible"
|
adamc@21
|
350
|
adamc@16
|
351 fun map {kind, con, exp} e =
|
adamc@16
|
352 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@16
|
353 con = fn c => fn () => S.Continue (con c, ()),
|
adamc@16
|
354 exp = fn e => fn () => S.Continue (exp e, ())} e () of
|
adamc@16
|
355 S.Return () => raise Fail "Core_util.Exp.map"
|
adamc@16
|
356 | S.Continue (e, ()) => e
|
adamc@16
|
357
|
adamc@23
|
358 fun fold {kind, con, exp} s e =
|
adamc@23
|
359 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
|
adamc@23
|
360 con = fn c => fn s => S.Continue (c, con (c, s)),
|
adamc@23
|
361 exp = fn e => fn s => S.Continue (e, exp (e, s))} e s of
|
adamc@23
|
362 S.Continue (_, s) => s
|
adamc@23
|
363 | S.Return _ => raise Fail "CoreUtil.Exp.fold: Impossible"
|
adamc@23
|
364
|
adamc@16
|
365 fun exists {kind, con, exp} k =
|
adamc@16
|
366 case mapfold {kind = fn k => fn () =>
|
adamc@16
|
367 if kind k then
|
adamc@16
|
368 S.Return ()
|
adamc@16
|
369 else
|
adamc@16
|
370 S.Continue (k, ()),
|
adamc@16
|
371 con = fn c => fn () =>
|
adamc@16
|
372 if con c then
|
adamc@16
|
373 S.Return ()
|
adamc@16
|
374 else
|
adamc@16
|
375 S.Continue (c, ()),
|
adamc@16
|
376 exp = fn e => fn () =>
|
adamc@16
|
377 if exp e then
|
adamc@16
|
378 S.Return ()
|
adamc@16
|
379 else
|
adamc@16
|
380 S.Continue (e, ())} k () of
|
adamc@16
|
381 S.Return _ => true
|
adamc@16
|
382 | S.Continue _ => false
|
adamc@16
|
383
|
adamc@16
|
384 end
|
adamc@16
|
385
|
adamc@20
|
386 structure Decl = struct
|
adamc@20
|
387
|
adamc@20
|
388 datatype binder = datatype Exp.binder
|
adamc@20
|
389
|
adamc@20
|
390 fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
|
adamc@20
|
391 let
|
adamc@20
|
392 val mfk = Kind.mapfold fk
|
adamc@20
|
393
|
adamc@20
|
394 fun bind' (ctx, b) =
|
adamc@20
|
395 let
|
adamc@20
|
396 val b' = case b of
|
adamc@20
|
397 Con.Rel x => RelC x
|
adamc@20
|
398 | Con.Named x => NamedC x
|
adamc@20
|
399 in
|
adamc@20
|
400 bind (ctx, b')
|
adamc@20
|
401 end
|
adamc@20
|
402 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
|
adamc@20
|
403
|
adamc@20
|
404 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind}
|
adamc@20
|
405
|
adamc@20
|
406 fun mfd ctx d acc =
|
adamc@20
|
407 S.bindP (mfd' ctx d acc, fd ctx)
|
adamc@20
|
408
|
adamc@20
|
409 and mfd' ctx (dAll as (d, loc)) =
|
adamc@20
|
410 case d of
|
adamc@20
|
411 DCon (x, n, k, c) =>
|
adamc@20
|
412 S.bind2 (mfk k,
|
adamc@20
|
413 fn k' =>
|
adamc@20
|
414 S.map2 (mfc ctx c,
|
adamc@20
|
415 fn c' =>
|
adamc@20
|
416 (DCon (x, n, k', c'), loc)))
|
adamc@163
|
417 | DDatatype (x, n, xncs) =>
|
adamc@163
|
418 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
|
adamc@163
|
419 case c of
|
adamc@163
|
420 NONE => S.return2 (x, n, c)
|
adamc@163
|
421 | SOME c =>
|
adamc@163
|
422 S.map2 (mfc ctx c,
|
adamc@163
|
423 fn c' => (x, n, SOME c'))) xncs,
|
adamc@163
|
424 fn xncs' =>
|
adamc@163
|
425 (DDatatype (x, n, xncs'), loc))
|
adamc@125
|
426 | DVal vi =>
|
adamc@125
|
427 S.map2 (mfvi ctx vi,
|
adamc@125
|
428 fn vi' =>
|
adamc@125
|
429 (DVal vi', loc))
|
adamc@125
|
430 | DValRec vis =>
|
adamc@127
|
431 let
|
adamc@127
|
432 val ctx = foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
|
adamc@127
|
433 ctx vis
|
adamc@127
|
434 in
|
adamc@127
|
435 S.map2 (ListUtil.mapfold (mfvi ctx) vis,
|
adamc@127
|
436 fn vis' =>
|
adamc@127
|
437 (DValRec vis', loc))
|
adamc@127
|
438 end
|
adamc@109
|
439 | DExport _ => S.return2 dAll
|
adamc@125
|
440
|
adamc@125
|
441 and mfvi ctx (x, n, t, e, s) =
|
adamc@125
|
442 S.bind2 (mfc ctx t,
|
adamc@125
|
443 fn t' =>
|
adamc@125
|
444 S.map2 (mfe ctx e,
|
adamc@125
|
445 fn e' =>
|
adamc@125
|
446 (x, n, t', e', s)))
|
adamc@20
|
447 in
|
adamc@20
|
448 mfd
|
adamc@20
|
449 end
|
adamc@20
|
450
|
adamc@23
|
451 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
|
adamc@23
|
452 mapfoldB {kind = fk,
|
adamc@23
|
453 con = fn () => fc,
|
adamc@23
|
454 exp = fn () => fe,
|
adamc@23
|
455 decl = fn () => fd,
|
adamc@23
|
456 bind = fn ((), _) => ()} ()
|
adamc@23
|
457
|
adamc@23
|
458 fun fold {kind, con, exp, decl} s d =
|
adamc@23
|
459 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
|
adamc@23
|
460 con = fn c => fn s => S.Continue (c, con (c, s)),
|
adamc@23
|
461 exp = fn e => fn s => S.Continue (e, exp (e, s)),
|
adamc@23
|
462 decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
|
adamc@23
|
463 S.Continue (_, s) => s
|
adamc@23
|
464 | S.Return _ => raise Fail "CoreUtil.Decl.fold: Impossible"
|
adamc@23
|
465
|
adamc@110
|
466 fun foldMap {kind, con, exp, decl} s d =
|
adamc@110
|
467 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
|
adamc@110
|
468 con = fn c => fn s => S.Continue (con (c, s)),
|
adamc@110
|
469 exp = fn e => fn s => S.Continue (exp (e, s)),
|
adamc@110
|
470 decl = fn d => fn s => S.Continue (decl (d, s))} d s of
|
adamc@110
|
471 S.Continue v => v
|
adamc@110
|
472 | S.Return _ => raise Fail "CoreUtil.Decl.foldMap: Impossible"
|
adamc@110
|
473
|
adamc@16
|
474 end
|
adamc@20
|
475
|
adamc@20
|
476 structure File = struct
|
adamc@20
|
477
|
adamc@20
|
478 datatype binder = datatype Exp.binder
|
adamc@20
|
479
|
adamc@20
|
480 fun mapfoldB (all as {bind, ...}) =
|
adamc@20
|
481 let
|
adamc@20
|
482 val mfd = Decl.mapfoldB all
|
adamc@20
|
483
|
adamc@20
|
484 fun mff ctx ds =
|
adamc@20
|
485 case ds of
|
adamc@20
|
486 nil => S.return2 nil
|
adamc@20
|
487 | d :: ds' =>
|
adamc@20
|
488 S.bind2 (mfd ctx d,
|
adamc@20
|
489 fn d' =>
|
adamc@20
|
490 let
|
adamc@100
|
491 val ctx' =
|
adamc@20
|
492 case #1 d' of
|
adamc@100
|
493 DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c))
|
adamc@163
|
494 | DDatatype (x, n, xncs) =>
|
adamc@163
|
495 let
|
adamc@163
|
496 val ctx = bind (ctx, NamedC (x, n, (KType, #2 d'), NONE))
|
adamc@163
|
497 val t = (CNamed n, #2 d')
|
adamc@163
|
498 in
|
adamc@163
|
499 foldl (fn ((x, n, to), ctx) =>
|
adamc@163
|
500 let
|
adamc@163
|
501 val t = case to of
|
adamc@163
|
502 NONE => t
|
adamc@163
|
503 | SOME t' => (TFun (t', t), #2 d')
|
adamc@163
|
504 in
|
adamc@163
|
505 bind (ctx, NamedE (x, n, t, NONE, ""))
|
adamc@163
|
506 end)
|
adamc@163
|
507 ctx xncs
|
adamc@163
|
508 end
|
adamc@109
|
509 | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s))
|
adamc@125
|
510 | DValRec vis =>
|
adamc@127
|
511 foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
|
adamc@125
|
512 ctx vis
|
adamc@109
|
513 | DExport _ => ctx
|
adamc@20
|
514 in
|
adamc@20
|
515 S.map2 (mff ctx' ds',
|
adamc@20
|
516 fn ds' =>
|
adamc@20
|
517 d' :: ds')
|
adamc@20
|
518 end)
|
adamc@20
|
519 in
|
adamc@20
|
520 mff
|
adamc@20
|
521 end
|
adamc@20
|
522
|
adamc@23
|
523 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
|
adamc@23
|
524 mapfoldB {kind = fk,
|
adamc@23
|
525 con = fn () => fc,
|
adamc@23
|
526 exp = fn () => fe,
|
adamc@23
|
527 decl = fn () => fd,
|
adamc@23
|
528 bind = fn ((), _) => ()} ()
|
adamc@23
|
529
|
adamc@20
|
530 fun mapB {kind, con, exp, decl, bind} ctx ds =
|
adamc@20
|
531 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@20
|
532 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
|
adamc@20
|
533 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
|
adamc@20
|
534 decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()),
|
adamc@20
|
535 bind = bind} ctx ds () of
|
adamc@20
|
536 S.Continue (ds, ()) => ds
|
adamc@20
|
537 | S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible"
|
adamc@20
|
538
|
adamc@23
|
539 fun fold {kind, con, exp, decl} s d =
|
adamc@23
|
540 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
|
adamc@23
|
541 con = fn c => fn s => S.Continue (c, con (c, s)),
|
adamc@23
|
542 exp = fn e => fn s => S.Continue (e, exp (e, s)),
|
adamc@23
|
543 decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
|
adamc@23
|
544 S.Continue (_, s) => s
|
adamc@23
|
545 | S.Return _ => raise Fail "CoreUtil.File.fold: Impossible"
|
adamc@23
|
546
|
adamc@110
|
547 fun foldMap {kind, con, exp, decl} s d =
|
adamc@110
|
548 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
|
adamc@110
|
549 con = fn c => fn s => S.Continue (con (c, s)),
|
adamc@110
|
550 exp = fn e => fn s => S.Continue (exp (e, s)),
|
adamc@110
|
551 decl = fn d => fn s => S.Continue (decl (d, s))} d s of
|
adamc@110
|
552 S.Continue v => v
|
adamc@110
|
553 | S.Return _ => raise Fail "CoreUtil.File.foldMap: Impossible"
|
adamc@110
|
554
|
adamc@179
|
555 val maxName = foldl (fn ((d, _) : decl, count) =>
|
adamc@179
|
556 case d of
|
adamc@179
|
557 DCon (_, n, _, _) => Int.max (n, count)
|
adamc@179
|
558 | DDatatype (_, n, _) => Int.max (n, count)
|
adamc@179
|
559 | DVal (_, n, _, _, _) => Int.max (n, count)
|
adamc@179
|
560 | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis
|
adamc@179
|
561 | DExport _ => count) 0
|
adamc@179
|
562
|
adamc@20
|
563 end
|
adamc@20
|
564
|
adamc@20
|
565 end
|