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@192
|
236 | ECon (dk, pc, cs, NONE) =>
|
adamc@192
|
237 S.map2 (ListUtil.mapfold (mfc ctx) cs,
|
adamc@192
|
238 fn cs' =>
|
adamc@192
|
239 (ECon (dk, pc, cs', NONE), loc))
|
adamc@192
|
240 | ECon (dk, n, cs, SOME e) =>
|
adamc@192
|
241 S.bind2 (mfe ctx e,
|
adamc@192
|
242 fn e' =>
|
adamc@192
|
243 S.map2 (ListUtil.mapfold (mfc ctx) cs,
|
adamc@192
|
244 fn cs' =>
|
adamc@192
|
245 (ECon (dk, n, cs', SOME e'), loc)))
|
adamc@48
|
246 | EFfi _ => S.return2 eAll
|
adamc@48
|
247 | EFfiApp (m, x, es) =>
|
adamc@192
|
248 S.map2 (ListUtil.mapfold (mfe ctx) es,
|
adamc@48
|
249 fn es' =>
|
adamc@48
|
250 (EFfiApp (m, x, es'), loc))
|
adamc@16
|
251 | EApp (e1, e2) =>
|
adamc@16
|
252 S.bind2 (mfe ctx e1,
|
adamc@16
|
253 fn e1' =>
|
adamc@16
|
254 S.map2 (mfe ctx e2,
|
adamc@16
|
255 fn e2' =>
|
adamc@16
|
256 (EApp (e1', e2'), loc)))
|
adamc@26
|
257 | EAbs (x, dom, ran, e) =>
|
adamc@26
|
258 S.bind2 (mfc ctx dom,
|
adamc@26
|
259 fn dom' =>
|
adamc@26
|
260 S.bind2 (mfc ctx ran,
|
adamc@26
|
261 fn ran' =>
|
adamc@26
|
262 S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
|
adamc@26
|
263 fn e' =>
|
adamc@26
|
264 (EAbs (x, dom', ran', e'), loc))))
|
adamc@16
|
265
|
adamc@16
|
266 | ECApp (e, c) =>
|
adamc@16
|
267 S.bind2 (mfe ctx e,
|
adamc@16
|
268 fn e' =>
|
adamc@16
|
269 S.map2 (mfc ctx c,
|
adamc@16
|
270 fn c' =>
|
adamc@16
|
271 (ECApp (e', c'), loc)))
|
adamc@16
|
272 | ECAbs (x, k, e) =>
|
adamc@16
|
273 S.bind2 (mfk k,
|
adamc@16
|
274 fn k' =>
|
adamc@16
|
275 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
|
adamc@16
|
276 fn e' =>
|
adamc@16
|
277 (ECAbs (x, k', e'), loc)))
|
adamc@16
|
278
|
adamc@16
|
279 | ERecord xes =>
|
adamc@29
|
280 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
|
adamc@16
|
281 S.bind2 (mfc ctx x,
|
adamc@16
|
282 fn x' =>
|
adamc@29
|
283 S.bind2 (mfe ctx e,
|
adamc@29
|
284 fn e' =>
|
adamc@29
|
285 S.map2 (mfc ctx t,
|
adamc@29
|
286 fn t' =>
|
adamc@29
|
287 (x', e', t')))))
|
adamc@16
|
288 xes,
|
adamc@16
|
289 fn xes' =>
|
adamc@16
|
290 (ERecord xes', loc))
|
adamc@16
|
291 | EField (e, c, {field, rest}) =>
|
adamc@16
|
292 S.bind2 (mfe ctx e,
|
adamc@16
|
293 fn e' =>
|
adamc@16
|
294 S.bind2 (mfc ctx c,
|
adamc@16
|
295 fn c' =>
|
adamc@16
|
296 S.bind2 (mfc ctx field,
|
adamc@16
|
297 fn field' =>
|
adamc@16
|
298 S.map2 (mfc ctx rest,
|
adamc@16
|
299 fn rest' =>
|
adamc@16
|
300 (EField (e', c', {field = field', rest = rest'}), loc)))))
|
adamc@149
|
301 | ECut (e, c, {field, rest}) =>
|
adamc@149
|
302 S.bind2 (mfe ctx e,
|
adamc@149
|
303 fn e' =>
|
adamc@149
|
304 S.bind2 (mfc ctx c,
|
adamc@149
|
305 fn c' =>
|
adamc@149
|
306 S.bind2 (mfc ctx field,
|
adamc@149
|
307 fn field' =>
|
adamc@149
|
308 S.map2 (mfc ctx rest,
|
adamc@149
|
309 fn rest' =>
|
adamc@149
|
310 (ECut (e', c', {field = field', rest = rest'}), loc)))))
|
adamc@73
|
311 | EFold k =>
|
adamc@73
|
312 S.map2 (mfk k,
|
adamc@73
|
313 fn k' =>
|
adamc@73
|
314 (EFold k', loc))
|
adamc@102
|
315
|
adamc@182
|
316 | ECase (e, pes, {disc, result}) =>
|
adamc@177
|
317 S.bind2 (mfe ctx e,
|
adamc@177
|
318 fn e' =>
|
adamc@177
|
319 S.bind2 (ListUtil.mapfold (fn (p, e) =>
|
adamc@177
|
320 S.map2 (mfe ctx e,
|
adamc@177
|
321 fn e' => (p, e'))) pes,
|
adamc@177
|
322 fn pes' =>
|
adamc@182
|
323 S.bind2 (mfc ctx disc,
|
adamc@182
|
324 fn disc' =>
|
adamc@182
|
325 S.map2 (mfc ctx result,
|
adamc@182
|
326 fn result' =>
|
adamc@182
|
327 (ECase (e', pes', {disc = disc', result = result'}), loc)))))
|
adamc@177
|
328
|
adamc@102
|
329 | EWrite e =>
|
adamc@102
|
330 S.map2 (mfe ctx e,
|
adamc@102
|
331 fn e' =>
|
adamc@102
|
332 (EWrite e', loc))
|
adamc@110
|
333
|
adamc@110
|
334 | EClosure (n, es) =>
|
adamc@110
|
335 S.map2 (ListUtil.mapfold (mfe ctx) es,
|
adamc@110
|
336 fn es' =>
|
adamc@110
|
337 (EClosure (n, es'), loc))
|
adamc@16
|
338 in
|
adamc@16
|
339 mfe
|
adamc@16
|
340 end
|
adamc@16
|
341
|
adamc@16
|
342 fun mapfold {kind = fk, con = fc, exp = fe} =
|
adamc@16
|
343 mapfoldB {kind = fk,
|
adamc@16
|
344 con = fn () => fc,
|
adamc@16
|
345 exp = fn () => fe,
|
adamc@16
|
346 bind = fn ((), _) => ()} ()
|
adamc@16
|
347
|
adamc@21
|
348 fun mapB {kind, con, exp, bind} ctx e =
|
adamc@21
|
349 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@21
|
350 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
|
adamc@21
|
351 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
|
adamc@21
|
352 bind = bind} ctx e () of
|
adamc@21
|
353 S.Continue (e, ()) => e
|
adamc@21
|
354 | S.Return _ => raise Fail "CoreUtil.Exp.mapB: Impossible"
|
adamc@21
|
355
|
adamc@16
|
356 fun map {kind, con, exp} e =
|
adamc@16
|
357 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@16
|
358 con = fn c => fn () => S.Continue (con c, ()),
|
adamc@16
|
359 exp = fn e => fn () => S.Continue (exp e, ())} e () of
|
adamc@16
|
360 S.Return () => raise Fail "Core_util.Exp.map"
|
adamc@16
|
361 | S.Continue (e, ()) => e
|
adamc@16
|
362
|
adamc@23
|
363 fun fold {kind, con, exp} s e =
|
adamc@23
|
364 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
|
adamc@23
|
365 con = fn c => fn s => S.Continue (c, con (c, s)),
|
adamc@23
|
366 exp = fn e => fn s => S.Continue (e, exp (e, s))} e s of
|
adamc@23
|
367 S.Continue (_, s) => s
|
adamc@23
|
368 | S.Return _ => raise Fail "CoreUtil.Exp.fold: Impossible"
|
adamc@23
|
369
|
adamc@16
|
370 fun exists {kind, con, exp} k =
|
adamc@16
|
371 case mapfold {kind = fn k => fn () =>
|
adamc@16
|
372 if kind k then
|
adamc@16
|
373 S.Return ()
|
adamc@16
|
374 else
|
adamc@16
|
375 S.Continue (k, ()),
|
adamc@16
|
376 con = fn c => fn () =>
|
adamc@16
|
377 if con c then
|
adamc@16
|
378 S.Return ()
|
adamc@16
|
379 else
|
adamc@16
|
380 S.Continue (c, ()),
|
adamc@16
|
381 exp = fn e => fn () =>
|
adamc@16
|
382 if exp e then
|
adamc@16
|
383 S.Return ()
|
adamc@16
|
384 else
|
adamc@16
|
385 S.Continue (e, ())} k () of
|
adamc@16
|
386 S.Return _ => true
|
adamc@16
|
387 | S.Continue _ => false
|
adamc@16
|
388
|
adamc@16
|
389 end
|
adamc@16
|
390
|
adamc@20
|
391 structure Decl = struct
|
adamc@20
|
392
|
adamc@20
|
393 datatype binder = datatype Exp.binder
|
adamc@20
|
394
|
adamc@20
|
395 fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
|
adamc@20
|
396 let
|
adamc@20
|
397 val mfk = Kind.mapfold fk
|
adamc@20
|
398
|
adamc@20
|
399 fun bind' (ctx, b) =
|
adamc@20
|
400 let
|
adamc@20
|
401 val b' = case b of
|
adamc@20
|
402 Con.Rel x => RelC x
|
adamc@20
|
403 | Con.Named x => NamedC x
|
adamc@20
|
404 in
|
adamc@20
|
405 bind (ctx, b')
|
adamc@20
|
406 end
|
adamc@20
|
407 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
|
adamc@20
|
408
|
adamc@20
|
409 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind}
|
adamc@20
|
410
|
adamc@20
|
411 fun mfd ctx d acc =
|
adamc@20
|
412 S.bindP (mfd' ctx d acc, fd ctx)
|
adamc@20
|
413
|
adamc@20
|
414 and mfd' ctx (dAll as (d, loc)) =
|
adamc@20
|
415 case d of
|
adamc@20
|
416 DCon (x, n, k, c) =>
|
adamc@20
|
417 S.bind2 (mfk k,
|
adamc@20
|
418 fn k' =>
|
adamc@20
|
419 S.map2 (mfc ctx c,
|
adamc@20
|
420 fn c' =>
|
adamc@20
|
421 (DCon (x, n, k', c'), loc)))
|
adamc@192
|
422 | DDatatype (x, n, xs, xncs) =>
|
adamc@163
|
423 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
|
adamc@163
|
424 case c of
|
adamc@163
|
425 NONE => S.return2 (x, n, c)
|
adamc@163
|
426 | SOME c =>
|
adamc@163
|
427 S.map2 (mfc ctx c,
|
adamc@163
|
428 fn c' => (x, n, SOME c'))) xncs,
|
adamc@163
|
429 fn xncs' =>
|
adamc@192
|
430 (DDatatype (x, n, xs, xncs'), loc))
|
adamc@125
|
431 | DVal vi =>
|
adamc@125
|
432 S.map2 (mfvi ctx vi,
|
adamc@125
|
433 fn vi' =>
|
adamc@125
|
434 (DVal vi', loc))
|
adamc@125
|
435 | DValRec vis =>
|
adamc@127
|
436 let
|
adamc@127
|
437 val ctx = foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
|
adamc@127
|
438 ctx vis
|
adamc@127
|
439 in
|
adamc@127
|
440 S.map2 (ListUtil.mapfold (mfvi ctx) vis,
|
adamc@127
|
441 fn vis' =>
|
adamc@127
|
442 (DValRec vis', loc))
|
adamc@127
|
443 end
|
adamc@109
|
444 | DExport _ => S.return2 dAll
|
adamc@125
|
445
|
adamc@125
|
446 and mfvi ctx (x, n, t, e, s) =
|
adamc@125
|
447 S.bind2 (mfc ctx t,
|
adamc@125
|
448 fn t' =>
|
adamc@125
|
449 S.map2 (mfe ctx e,
|
adamc@125
|
450 fn e' =>
|
adamc@125
|
451 (x, n, t', e', s)))
|
adamc@20
|
452 in
|
adamc@20
|
453 mfd
|
adamc@20
|
454 end
|
adamc@20
|
455
|
adamc@23
|
456 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
|
adamc@23
|
457 mapfoldB {kind = fk,
|
adamc@23
|
458 con = fn () => fc,
|
adamc@23
|
459 exp = fn () => fe,
|
adamc@23
|
460 decl = fn () => fd,
|
adamc@23
|
461 bind = fn ((), _) => ()} ()
|
adamc@23
|
462
|
adamc@23
|
463 fun fold {kind, con, exp, decl} s d =
|
adamc@23
|
464 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
|
adamc@23
|
465 con = fn c => fn s => S.Continue (c, con (c, s)),
|
adamc@23
|
466 exp = fn e => fn s => S.Continue (e, exp (e, s)),
|
adamc@23
|
467 decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
|
adamc@23
|
468 S.Continue (_, s) => s
|
adamc@23
|
469 | S.Return _ => raise Fail "CoreUtil.Decl.fold: Impossible"
|
adamc@23
|
470
|
adamc@110
|
471 fun foldMap {kind, con, exp, decl} s d =
|
adamc@110
|
472 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
|
adamc@110
|
473 con = fn c => fn s => S.Continue (con (c, s)),
|
adamc@110
|
474 exp = fn e => fn s => S.Continue (exp (e, s)),
|
adamc@110
|
475 decl = fn d => fn s => S.Continue (decl (d, s))} d s of
|
adamc@110
|
476 S.Continue v => v
|
adamc@110
|
477 | S.Return _ => raise Fail "CoreUtil.Decl.foldMap: Impossible"
|
adamc@110
|
478
|
adamc@16
|
479 end
|
adamc@20
|
480
|
adamc@20
|
481 structure File = struct
|
adamc@20
|
482
|
adamc@20
|
483 datatype binder = datatype Exp.binder
|
adamc@20
|
484
|
adamc@20
|
485 fun mapfoldB (all as {bind, ...}) =
|
adamc@20
|
486 let
|
adamc@20
|
487 val mfd = Decl.mapfoldB all
|
adamc@20
|
488
|
adamc@20
|
489 fun mff ctx ds =
|
adamc@20
|
490 case ds of
|
adamc@20
|
491 nil => S.return2 nil
|
adamc@20
|
492 | d :: ds' =>
|
adamc@20
|
493 S.bind2 (mfd ctx d,
|
adamc@20
|
494 fn d' =>
|
adamc@20
|
495 let
|
adamc@100
|
496 val ctx' =
|
adamc@20
|
497 case #1 d' of
|
adamc@100
|
498 DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c))
|
adamc@192
|
499 | DDatatype (x, n, xs, xncs) =>
|
adamc@163
|
500 let
|
adamc@192
|
501 val loc = #2 d'
|
adamc@192
|
502 val k = (KType, loc)
|
adamc@192
|
503 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
|
adamc@192
|
504
|
adamc@192
|
505 val ctx = bind (ctx, NamedC (x, n, k', NONE))
|
adamc@163
|
506 val t = (CNamed n, #2 d')
|
adamc@192
|
507 val t = ListUtil.foldli (fn (i, _, t) => (CApp (t, (CRel i, loc)), loc))
|
adamc@192
|
508 t xs
|
adamc@163
|
509 in
|
adamc@163
|
510 foldl (fn ((x, n, to), ctx) =>
|
adamc@163
|
511 let
|
adamc@163
|
512 val t = case to of
|
adamc@163
|
513 NONE => t
|
adamc@163
|
514 | SOME t' => (TFun (t', t), #2 d')
|
adamc@192
|
515 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc))
|
adamc@192
|
516 t xs
|
adamc@163
|
517 in
|
adamc@163
|
518 bind (ctx, NamedE (x, n, t, NONE, ""))
|
adamc@163
|
519 end)
|
adamc@163
|
520 ctx xncs
|
adamc@163
|
521 end
|
adamc@109
|
522 | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s))
|
adamc@125
|
523 | DValRec vis =>
|
adamc@127
|
524 foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
|
adamc@125
|
525 ctx vis
|
adamc@109
|
526 | DExport _ => ctx
|
adamc@20
|
527 in
|
adamc@20
|
528 S.map2 (mff ctx' ds',
|
adamc@20
|
529 fn ds' =>
|
adamc@20
|
530 d' :: ds')
|
adamc@20
|
531 end)
|
adamc@20
|
532 in
|
adamc@20
|
533 mff
|
adamc@20
|
534 end
|
adamc@20
|
535
|
adamc@23
|
536 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
|
adamc@23
|
537 mapfoldB {kind = fk,
|
adamc@23
|
538 con = fn () => fc,
|
adamc@23
|
539 exp = fn () => fe,
|
adamc@23
|
540 decl = fn () => fd,
|
adamc@23
|
541 bind = fn ((), _) => ()} ()
|
adamc@23
|
542
|
adamc@20
|
543 fun mapB {kind, con, exp, decl, bind} ctx ds =
|
adamc@20
|
544 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@20
|
545 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
|
adamc@20
|
546 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
|
adamc@20
|
547 decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()),
|
adamc@20
|
548 bind = bind} ctx ds () of
|
adamc@20
|
549 S.Continue (ds, ()) => ds
|
adamc@20
|
550 | S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible"
|
adamc@20
|
551
|
adamc@23
|
552 fun fold {kind, con, exp, decl} s d =
|
adamc@23
|
553 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
|
adamc@23
|
554 con = fn c => fn s => S.Continue (c, con (c, s)),
|
adamc@23
|
555 exp = fn e => fn s => S.Continue (e, exp (e, s)),
|
adamc@23
|
556 decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
|
adamc@23
|
557 S.Continue (_, s) => s
|
adamc@23
|
558 | S.Return _ => raise Fail "CoreUtil.File.fold: Impossible"
|
adamc@23
|
559
|
adamc@110
|
560 fun foldMap {kind, con, exp, decl} s d =
|
adamc@110
|
561 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
|
adamc@110
|
562 con = fn c => fn s => S.Continue (con (c, s)),
|
adamc@110
|
563 exp = fn e => fn s => S.Continue (exp (e, s)),
|
adamc@110
|
564 decl = fn d => fn s => S.Continue (decl (d, s))} d s of
|
adamc@110
|
565 S.Continue v => v
|
adamc@110
|
566 | S.Return _ => raise Fail "CoreUtil.File.foldMap: Impossible"
|
adamc@110
|
567
|
adamc@179
|
568 val maxName = foldl (fn ((d, _) : decl, count) =>
|
adamc@179
|
569 case d of
|
adamc@179
|
570 DCon (_, n, _, _) => Int.max (n, count)
|
adamc@192
|
571 | DDatatype (_, n, _, _) => Int.max (n, count)
|
adamc@179
|
572 | DVal (_, n, _, _, _) => Int.max (n, count)
|
adamc@179
|
573 | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis
|
adamc@179
|
574 | DExport _ => count) 0
|
adamc@179
|
575
|
adamc@20
|
576 end
|
adamc@20
|
577
|
adamc@20
|
578 end
|