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