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@193
|
42 open Order
|
adamc@193
|
43
|
adamc@193
|
44 fun compare ((k1, _), (k2, _)) =
|
adamc@193
|
45 case (k1, k2) of
|
adamc@193
|
46 (KType, KType) => EQUAL
|
adamc@193
|
47 | (KType, _) => LESS
|
adamc@193
|
48 | (_, KType) => GREATER
|
adamc@193
|
49
|
adamc@193
|
50 | (KArrow (d1, r1), KArrow (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2))
|
adamc@193
|
51 | (KArrow _, _) => LESS
|
adamc@193
|
52 | (_, KArrow _) => GREATER
|
adamc@193
|
53
|
adamc@193
|
54 | (KName, KName) => EQUAL
|
adamc@193
|
55 | (KName, _) => LESS
|
adamc@193
|
56 | (_, KName) => GREATER
|
adamc@193
|
57
|
adamc@193
|
58 | (KRecord k1, KRecord k2) => compare (k1, k2)
|
adamc@193
|
59 | (KRecord _, _) => LESS
|
adamc@193
|
60 | (_, KRecord _) => GREATER
|
adamc@193
|
61
|
adamc@193
|
62 | (KUnit, KUnit) => EQUAL
|
adamc@193
|
63
|
adamc@16
|
64 fun mapfold f =
|
adamc@16
|
65 let
|
adamc@16
|
66 fun mfk k acc =
|
adamc@16
|
67 S.bindP (mfk' k acc, f)
|
adamc@16
|
68
|
adamc@16
|
69 and mfk' (kAll as (k, loc)) =
|
adamc@16
|
70 case k of
|
adamc@16
|
71 KType => S.return2 kAll
|
adamc@16
|
72
|
adamc@16
|
73 | KArrow (k1, k2) =>
|
adamc@16
|
74 S.bind2 (mfk k1,
|
adamc@16
|
75 fn k1' =>
|
adamc@16
|
76 S.map2 (mfk k2,
|
adamc@16
|
77 fn k2' =>
|
adamc@16
|
78 (KArrow (k1', k2'), loc)))
|
adamc@16
|
79
|
adamc@16
|
80 | KName => S.return2 kAll
|
adamc@16
|
81
|
adamc@16
|
82 | KRecord k =>
|
adamc@16
|
83 S.map2 (mfk k,
|
adamc@16
|
84 fn k' =>
|
adamc@16
|
85 (KRecord k', loc))
|
adamc@87
|
86
|
adamc@87
|
87 | KUnit => S.return2 kAll
|
adamc@16
|
88 in
|
adamc@16
|
89 mfk
|
adamc@16
|
90 end
|
adamc@16
|
91
|
adamc@16
|
92 fun map f k =
|
adamc@16
|
93 case mapfold (fn k => fn () => S.Continue (f k, ())) k () of
|
adamc@16
|
94 S.Return () => raise Fail "Core_util.Kind.map"
|
adamc@16
|
95 | S.Continue (k, ()) => k
|
adamc@16
|
96
|
adamc@16
|
97 fun exists f k =
|
adamc@16
|
98 case mapfold (fn k => fn () =>
|
adamc@16
|
99 if f k then
|
adamc@16
|
100 S.Return ()
|
adamc@16
|
101 else
|
adamc@16
|
102 S.Continue (k, ())) k () of
|
adamc@16
|
103 S.Return _ => true
|
adamc@16
|
104 | S.Continue _ => false
|
adamc@16
|
105
|
adamc@16
|
106 end
|
adamc@16
|
107
|
adamc@16
|
108 structure Con = struct
|
adamc@16
|
109
|
adamc@193
|
110 open Order
|
adamc@193
|
111
|
adamc@193
|
112 fun compare ((c1, _), (c2, _)) =
|
adamc@193
|
113 case (c1, c2) of
|
adamc@193
|
114 (TFun (d1, r1), TFun (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2))
|
adamc@193
|
115 | (TFun _, _) => LESS
|
adamc@193
|
116 | (_, TFun _) => GREATER
|
adamc@193
|
117
|
adamc@193
|
118 | (TCFun (x1, k1, r1), TCFun (x2, k2, r2)) =>
|
adamc@193
|
119 join (String.compare (x1, x2),
|
adamc@193
|
120 fn () => join (Kind.compare (k1, k2),
|
adamc@193
|
121 fn () => compare (r1, r2)))
|
adamc@193
|
122 | (TCFun _, _) => LESS
|
adamc@193
|
123 | (_, TCFun _) => GREATER
|
adamc@193
|
124
|
adamc@193
|
125 | (TRecord c1, TRecord c2) => compare (c1, c2)
|
adamc@193
|
126 | (TRecord _, _) => LESS
|
adamc@193
|
127 | (_, TRecord _) => GREATER
|
adamc@193
|
128
|
adamc@193
|
129 | (CRel n1, CRel n2) => Int.compare (n1, n2)
|
adamc@193
|
130 | (CRel _, _) => LESS
|
adamc@193
|
131 | (_, CRel _) => GREATER
|
adamc@193
|
132
|
adamc@193
|
133 | (CNamed n1, CNamed n2) => Int.compare (n1, n2)
|
adamc@193
|
134 | (CNamed _, _) => LESS
|
adamc@193
|
135 | (_, CNamed _) => GREATER
|
adamc@193
|
136
|
adamc@193
|
137 | (CFfi (m1, s1), CFfi (m2, s2)) => join (String.compare (m1, m2),
|
adamc@193
|
138 fn () => String.compare (s1, s2))
|
adamc@193
|
139 | (CFfi _, _) => LESS
|
adamc@193
|
140 | (_, CFfi _) => GREATER
|
adamc@193
|
141
|
adamc@193
|
142 | (CApp (f1, x1), CApp (f2, x2)) => join (compare (f1, f2),
|
adamc@193
|
143 fn () => compare (x1, x2))
|
adamc@193
|
144 | (CApp _, _) => LESS
|
adamc@193
|
145 | (_, CApp _) => GREATER
|
adamc@193
|
146
|
adamc@193
|
147 | (CAbs (x1, k1, b1), CAbs (x2, k2, b2)) =>
|
adamc@193
|
148 join (String.compare (x1, x2),
|
adamc@193
|
149 fn () => join (Kind.compare (k1, k2),
|
adamc@193
|
150 fn () => compare (b1, b2)))
|
adamc@193
|
151 | (CAbs _, _) => LESS
|
adamc@193
|
152 | (_, CAbs _) => GREATER
|
adamc@193
|
153
|
adamc@193
|
154 | (CName s1, CName s2) => String.compare (s1, s2)
|
adamc@193
|
155 | (CName _, _) => LESS
|
adamc@193
|
156 | (_, CName _) => GREATER
|
adamc@193
|
157
|
adamc@193
|
158 | (CRecord (k1, xvs1), CRecord (k2, xvs2)) =>
|
adamc@193
|
159 join (Kind.compare (k1, k2),
|
adamc@193
|
160 fn () => joinL (fn ((x1, v1), (x2, v2)) =>
|
adamc@193
|
161 join (compare (x1, x2),
|
adamc@193
|
162 fn () => compare (v1, v2))) (xvs1, xvs2))
|
adamc@193
|
163 | (CRecord _, _) => LESS
|
adamc@193
|
164 | (_, CRecord _) => GREATER
|
adamc@193
|
165
|
adamc@193
|
166 | (CConcat (f1, s1), CConcat (f2, s2)) =>
|
adamc@193
|
167 join (compare (f1, f2),
|
adamc@193
|
168 fn () => compare (s1, s2))
|
adamc@193
|
169 | (CConcat _, _) => LESS
|
adamc@193
|
170 | (_, CConcat _) => GREATER
|
adamc@193
|
171
|
adamc@193
|
172 | (CFold (d1, r1), CFold (d2, r2)) =>
|
adamc@193
|
173 join (Kind.compare (d1, r2),
|
adamc@193
|
174 fn () => Kind.compare (r1, r2))
|
adamc@193
|
175 | (CFold _, _) => LESS
|
adamc@193
|
176 | (_, CFold _) => GREATER
|
adamc@193
|
177
|
adamc@193
|
178 | (CUnit, CUnit) => EQUAL
|
adamc@193
|
179
|
adamc@16
|
180 datatype binder =
|
adamc@16
|
181 Rel of string * kind
|
adamc@20
|
182 | Named of string * int * kind * con option
|
adamc@16
|
183
|
adamc@16
|
184 fun mapfoldB {kind = fk, con = fc, bind} =
|
adamc@16
|
185 let
|
adamc@16
|
186 val mfk = Kind.mapfold fk
|
adamc@16
|
187
|
adamc@16
|
188 fun mfc ctx c acc =
|
adamc@16
|
189 S.bindP (mfc' ctx c acc, fc ctx)
|
adamc@16
|
190
|
adamc@16
|
191 and mfc' ctx (cAll as (c, loc)) =
|
adamc@16
|
192 case c of
|
adamc@16
|
193 TFun (c1, c2) =>
|
adamc@16
|
194 S.bind2 (mfc ctx c1,
|
adamc@16
|
195 fn c1' =>
|
adamc@16
|
196 S.map2 (mfc ctx c2,
|
adamc@16
|
197 fn c2' =>
|
adamc@16
|
198 (TFun (c1', c2'), loc)))
|
adamc@16
|
199 | TCFun (x, k, c) =>
|
adamc@16
|
200 S.bind2 (mfk k,
|
adamc@16
|
201 fn k' =>
|
adamc@16
|
202 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
|
adamc@16
|
203 fn c' =>
|
adamc@16
|
204 (TCFun (x, k', c'), loc)))
|
adamc@16
|
205 | TRecord c =>
|
adamc@16
|
206 S.map2 (mfc ctx c,
|
adamc@16
|
207 fn c' =>
|
adamc@16
|
208 (TRecord c', loc))
|
adamc@16
|
209
|
adamc@16
|
210 | CRel _ => S.return2 cAll
|
adamc@16
|
211 | CNamed _ => S.return2 cAll
|
adamc@48
|
212 | CFfi _ => S.return2 cAll
|
adamc@16
|
213 | CApp (c1, c2) =>
|
adamc@16
|
214 S.bind2 (mfc ctx c1,
|
adamc@16
|
215 fn c1' =>
|
adamc@16
|
216 S.map2 (mfc ctx c2,
|
adamc@16
|
217 fn c2' =>
|
adamc@16
|
218 (CApp (c1', c2'), loc)))
|
adamc@16
|
219 | CAbs (x, k, c) =>
|
adamc@16
|
220 S.bind2 (mfk k,
|
adamc@16
|
221 fn k' =>
|
adamc@16
|
222 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
|
adamc@16
|
223 fn c' =>
|
adamc@16
|
224 (CAbs (x, k', c'), loc)))
|
adamc@16
|
225
|
adamc@16
|
226 | CName _ => S.return2 cAll
|
adamc@16
|
227
|
adamc@16
|
228 | CRecord (k, xcs) =>
|
adamc@16
|
229 S.bind2 (mfk k,
|
adamc@16
|
230 fn k' =>
|
adamc@16
|
231 S.map2 (ListUtil.mapfold (fn (x, c) =>
|
adamc@16
|
232 S.bind2 (mfc ctx x,
|
adamc@16
|
233 fn x' =>
|
adamc@16
|
234 S.map2 (mfc ctx c,
|
adamc@16
|
235 fn c' =>
|
adamc@16
|
236 (x', c'))))
|
adamc@16
|
237 xcs,
|
adamc@16
|
238 fn xcs' =>
|
adamc@16
|
239 (CRecord (k', xcs'), loc)))
|
adamc@16
|
240 | CConcat (c1, c2) =>
|
adamc@16
|
241 S.bind2 (mfc ctx c1,
|
adamc@16
|
242 fn c1' =>
|
adamc@16
|
243 S.map2 (mfc ctx c2,
|
adamc@16
|
244 fn c2' =>
|
adamc@16
|
245 (CConcat (c1', c2'), loc)))
|
adamc@69
|
246 | CFold (k1, k2) =>
|
adamc@69
|
247 S.bind2 (mfk k1,
|
adamc@69
|
248 fn k1' =>
|
adamc@69
|
249 S.map2 (mfk k2,
|
adamc@69
|
250 fn k2' =>
|
adamc@69
|
251 (CFold (k1', k2'), loc)))
|
adamc@87
|
252
|
adamc@87
|
253 | CUnit => S.return2 cAll
|
adamc@16
|
254 in
|
adamc@16
|
255 mfc
|
adamc@16
|
256 end
|
adamc@16
|
257
|
adamc@16
|
258 fun mapfold {kind = fk, con = fc} =
|
adamc@16
|
259 mapfoldB {kind = fk,
|
adamc@16
|
260 con = fn () => fc,
|
adamc@16
|
261 bind = fn ((), _) => ()} ()
|
adamc@16
|
262
|
adamc@16
|
263 fun map {kind, con} c =
|
adamc@16
|
264 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@16
|
265 con = fn c => fn () => S.Continue (con c, ())} c () of
|
adamc@16
|
266 S.Return () => raise Fail "Core_util.Con.map"
|
adamc@16
|
267 | S.Continue (c, ()) => c
|
adamc@16
|
268
|
adamc@16
|
269 fun mapB {kind, con, bind} ctx c =
|
adamc@16
|
270 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@16
|
271 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
|
adamc@16
|
272 bind = bind} ctx c () of
|
adamc@16
|
273 S.Continue (c, ()) => c
|
adamc@20
|
274 | S.Return _ => raise Fail "CoreUtil.Con.mapB: Impossible"
|
adamc@16
|
275
|
adamc@23
|
276 fun fold {kind, con} s c =
|
adamc@23
|
277 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
|
adamc@23
|
278 con = fn c => fn s => S.Continue (c, con (c, s))} c s of
|
adamc@23
|
279 S.Continue (_, s) => s
|
adamc@23
|
280 | S.Return _ => raise Fail "CoreUtil.Con.fold: Impossible"
|
adamc@23
|
281
|
adamc@16
|
282 fun exists {kind, con} k =
|
adamc@16
|
283 case mapfold {kind = fn k => fn () =>
|
adamc@16
|
284 if kind k then
|
adamc@16
|
285 S.Return ()
|
adamc@16
|
286 else
|
adamc@16
|
287 S.Continue (k, ()),
|
adamc@16
|
288 con = fn c => fn () =>
|
adamc@16
|
289 if con c then
|
adamc@16
|
290 S.Return ()
|
adamc@16
|
291 else
|
adamc@16
|
292 S.Continue (c, ())} k () of
|
adamc@16
|
293 S.Return _ => true
|
adamc@16
|
294 | S.Continue _ => false
|
adamc@16
|
295
|
adamc@193
|
296 fun foldMap {kind, con} s c =
|
adamc@193
|
297 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
|
adamc@193
|
298 con = fn c => fn s => S.Continue (con (c, s))} c s of
|
adamc@193
|
299 S.Continue v => v
|
adamc@193
|
300 | S.Return _ => raise Fail "CoreUtil.Con.foldMap: Impossible"
|
adamc@193
|
301
|
adamc@16
|
302 end
|
adamc@16
|
303
|
adamc@16
|
304 structure Exp = struct
|
adamc@16
|
305
|
adamc@16
|
306 datatype binder =
|
adamc@16
|
307 RelC of string * kind
|
adamc@20
|
308 | NamedC of string * int * kind * con option
|
adamc@16
|
309 | RelE of string * con
|
adamc@109
|
310 | NamedE of string * int * con * exp option * string
|
adamc@16
|
311
|
adamc@16
|
312 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
|
adamc@16
|
313 let
|
adamc@16
|
314 val mfk = Kind.mapfold fk
|
adamc@16
|
315
|
adamc@16
|
316 fun bind' (ctx, b) =
|
adamc@16
|
317 let
|
adamc@16
|
318 val b' = case b of
|
adamc@16
|
319 Con.Rel x => RelC x
|
adamc@16
|
320 | Con.Named x => NamedC x
|
adamc@16
|
321 in
|
adamc@16
|
322 bind (ctx, b')
|
adamc@16
|
323 end
|
adamc@16
|
324 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
|
adamc@16
|
325
|
adamc@16
|
326 fun mfe ctx e acc =
|
adamc@16
|
327 S.bindP (mfe' ctx e acc, fe ctx)
|
adamc@16
|
328
|
adamc@16
|
329 and mfe' ctx (eAll as (e, loc)) =
|
adamc@16
|
330 case e of
|
adamc@16
|
331 EPrim _ => S.return2 eAll
|
adamc@16
|
332 | ERel _ => S.return2 eAll
|
adamc@16
|
333 | ENamed _ => S.return2 eAll
|
adamc@192
|
334 | ECon (dk, pc, cs, NONE) =>
|
adamc@192
|
335 S.map2 (ListUtil.mapfold (mfc ctx) cs,
|
adamc@192
|
336 fn cs' =>
|
adamc@192
|
337 (ECon (dk, pc, cs', NONE), loc))
|
adamc@192
|
338 | ECon (dk, n, cs, SOME e) =>
|
adamc@192
|
339 S.bind2 (mfe ctx e,
|
adamc@192
|
340 fn e' =>
|
adamc@192
|
341 S.map2 (ListUtil.mapfold (mfc ctx) cs,
|
adamc@192
|
342 fn cs' =>
|
adamc@192
|
343 (ECon (dk, n, cs', SOME e'), loc)))
|
adamc@48
|
344 | EFfi _ => S.return2 eAll
|
adamc@48
|
345 | EFfiApp (m, x, es) =>
|
adamc@192
|
346 S.map2 (ListUtil.mapfold (mfe ctx) es,
|
adamc@48
|
347 fn es' =>
|
adamc@48
|
348 (EFfiApp (m, x, es'), loc))
|
adamc@16
|
349 | EApp (e1, e2) =>
|
adamc@16
|
350 S.bind2 (mfe ctx e1,
|
adamc@16
|
351 fn e1' =>
|
adamc@16
|
352 S.map2 (mfe ctx e2,
|
adamc@16
|
353 fn e2' =>
|
adamc@16
|
354 (EApp (e1', e2'), loc)))
|
adamc@26
|
355 | EAbs (x, dom, ran, e) =>
|
adamc@26
|
356 S.bind2 (mfc ctx dom,
|
adamc@26
|
357 fn dom' =>
|
adamc@26
|
358 S.bind2 (mfc ctx ran,
|
adamc@26
|
359 fn ran' =>
|
adamc@26
|
360 S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
|
adamc@26
|
361 fn e' =>
|
adamc@26
|
362 (EAbs (x, dom', ran', e'), loc))))
|
adamc@16
|
363
|
adamc@16
|
364 | ECApp (e, c) =>
|
adamc@16
|
365 S.bind2 (mfe ctx e,
|
adamc@16
|
366 fn e' =>
|
adamc@16
|
367 S.map2 (mfc ctx c,
|
adamc@16
|
368 fn c' =>
|
adamc@16
|
369 (ECApp (e', c'), loc)))
|
adamc@16
|
370 | ECAbs (x, k, e) =>
|
adamc@16
|
371 S.bind2 (mfk k,
|
adamc@16
|
372 fn k' =>
|
adamc@16
|
373 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
|
adamc@16
|
374 fn e' =>
|
adamc@16
|
375 (ECAbs (x, k', e'), loc)))
|
adamc@16
|
376
|
adamc@16
|
377 | ERecord xes =>
|
adamc@29
|
378 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
|
adamc@16
|
379 S.bind2 (mfc ctx x,
|
adamc@16
|
380 fn x' =>
|
adamc@29
|
381 S.bind2 (mfe ctx e,
|
adamc@29
|
382 fn e' =>
|
adamc@29
|
383 S.map2 (mfc ctx t,
|
adamc@29
|
384 fn t' =>
|
adamc@29
|
385 (x', e', t')))))
|
adamc@16
|
386 xes,
|
adamc@16
|
387 fn xes' =>
|
adamc@16
|
388 (ERecord xes', loc))
|
adamc@16
|
389 | EField (e, c, {field, rest}) =>
|
adamc@16
|
390 S.bind2 (mfe ctx e,
|
adamc@16
|
391 fn e' =>
|
adamc@16
|
392 S.bind2 (mfc ctx c,
|
adamc@16
|
393 fn c' =>
|
adamc@16
|
394 S.bind2 (mfc ctx field,
|
adamc@16
|
395 fn field' =>
|
adamc@16
|
396 S.map2 (mfc ctx rest,
|
adamc@16
|
397 fn rest' =>
|
adamc@16
|
398 (EField (e', c', {field = field', rest = rest'}), loc)))))
|
adamc@149
|
399 | ECut (e, c, {field, rest}) =>
|
adamc@149
|
400 S.bind2 (mfe ctx e,
|
adamc@149
|
401 fn e' =>
|
adamc@149
|
402 S.bind2 (mfc ctx c,
|
adamc@149
|
403 fn c' =>
|
adamc@149
|
404 S.bind2 (mfc ctx field,
|
adamc@149
|
405 fn field' =>
|
adamc@149
|
406 S.map2 (mfc ctx rest,
|
adamc@149
|
407 fn rest' =>
|
adamc@149
|
408 (ECut (e', c', {field = field', rest = rest'}), loc)))))
|
adamc@73
|
409 | EFold k =>
|
adamc@73
|
410 S.map2 (mfk k,
|
adamc@73
|
411 fn k' =>
|
adamc@73
|
412 (EFold k', loc))
|
adamc@102
|
413
|
adamc@182
|
414 | ECase (e, pes, {disc, result}) =>
|
adamc@177
|
415 S.bind2 (mfe ctx e,
|
adamc@177
|
416 fn e' =>
|
adamc@177
|
417 S.bind2 (ListUtil.mapfold (fn (p, e) =>
|
adamc@193
|
418 let
|
adamc@193
|
419 fun pb ((p, _), ctx) =
|
adamc@193
|
420 case p of
|
adamc@193
|
421 PWild => ctx
|
adamc@193
|
422 | PVar (x, t) => bind (ctx, RelE (x, t))
|
adamc@193
|
423 | PPrim _ => ctx
|
adamc@193
|
424 | PCon (_, _, _, NONE) => ctx
|
adamc@193
|
425 | PCon (_, _, _, SOME p) => pb (p, ctx)
|
adamc@193
|
426 | PRecord xps => foldl (fn ((_, p, _), ctx) =>
|
adamc@193
|
427 pb (p, ctx)) ctx xps
|
adamc@193
|
428 in
|
adamc@193
|
429 S.bind2 (mfp ctx p,
|
adamc@193
|
430 fn p' =>
|
adamc@193
|
431 S.map2 (mfe (pb (p', ctx)) e,
|
adamc@193
|
432 fn e' => (p', e')))
|
adamc@193
|
433 end) pes,
|
adamc@177
|
434 fn pes' =>
|
adamc@182
|
435 S.bind2 (mfc ctx disc,
|
adamc@182
|
436 fn disc' =>
|
adamc@182
|
437 S.map2 (mfc ctx result,
|
adamc@182
|
438 fn result' =>
|
adamc@182
|
439 (ECase (e', pes', {disc = disc', result = result'}), loc)))))
|
adamc@177
|
440
|
adamc@102
|
441 | EWrite e =>
|
adamc@102
|
442 S.map2 (mfe ctx e,
|
adamc@102
|
443 fn e' =>
|
adamc@102
|
444 (EWrite e', loc))
|
adamc@110
|
445
|
adamc@110
|
446 | EClosure (n, es) =>
|
adamc@110
|
447 S.map2 (ListUtil.mapfold (mfe ctx) es,
|
adamc@110
|
448 fn es' =>
|
adamc@110
|
449 (EClosure (n, es'), loc))
|
adamc@193
|
450
|
adamc@193
|
451 and mfp ctx (pAll as (p, loc)) =
|
adamc@193
|
452 case p of
|
adamc@193
|
453 PWild => S.return2 pAll
|
adamc@193
|
454 | PVar (x, t) =>
|
adamc@193
|
455 S.map2 (mfc ctx t,
|
adamc@193
|
456 fn t' =>
|
adamc@193
|
457 (PVar (x, t'), loc))
|
adamc@193
|
458 | PPrim _ => S.return2 pAll
|
adamc@193
|
459 | PCon (dk, pc, args, po) =>
|
adamc@193
|
460 S.bind2 (mfpc ctx pc,
|
adamc@193
|
461 fn pc' =>
|
adamc@193
|
462 S.bind2 (ListUtil.mapfold (mfc ctx) args,
|
adamc@193
|
463 fn args' =>
|
adamc@193
|
464 S.map2 ((case po of
|
adamc@193
|
465 NONE => S.return2 NONE
|
adamc@193
|
466 | SOME p => S.map2 (mfp ctx p, SOME)),
|
adamc@193
|
467 fn po' =>
|
adamc@193
|
468 (PCon (dk, pc', args', po'), loc))))
|
adamc@193
|
469 | PRecord xps =>
|
adamc@193
|
470 S.map2 (ListUtil.mapfold (fn (x, p, c) =>
|
adamc@193
|
471 S.bind2 (mfp ctx p,
|
adamc@193
|
472 fn p' =>
|
adamc@193
|
473 S.map2 (mfc ctx c,
|
adamc@193
|
474 fn c' =>
|
adamc@193
|
475 (x, p', c')))) xps,
|
adamc@193
|
476 fn xps' =>
|
adamc@193
|
477 (PRecord xps', loc))
|
adamc@193
|
478
|
adamc@193
|
479 and mfpc ctx pc =
|
adamc@193
|
480 case pc of
|
adamc@193
|
481 PConVar _ => S.return2 pc
|
adamc@193
|
482 | PConFfi {mod = m, datatyp, params, con, arg, kind} =>
|
adamc@193
|
483 S.map2 ((case arg of
|
adamc@193
|
484 NONE => S.return2 NONE
|
adamc@193
|
485 | SOME c => S.map2 (mfc ctx c, SOME)),
|
adamc@193
|
486 fn arg' =>
|
adamc@193
|
487 PConFfi {mod = m, datatyp = datatyp, params = params,
|
adamc@193
|
488 con = con, arg = arg', kind = kind})
|
adamc@16
|
489 in
|
adamc@16
|
490 mfe
|
adamc@16
|
491 end
|
adamc@16
|
492
|
adamc@16
|
493 fun mapfold {kind = fk, con = fc, exp = fe} =
|
adamc@16
|
494 mapfoldB {kind = fk,
|
adamc@16
|
495 con = fn () => fc,
|
adamc@16
|
496 exp = fn () => fe,
|
adamc@16
|
497 bind = fn ((), _) => ()} ()
|
adamc@16
|
498
|
adamc@21
|
499 fun mapB {kind, con, exp, bind} ctx e =
|
adamc@21
|
500 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@21
|
501 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
|
adamc@21
|
502 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
|
adamc@21
|
503 bind = bind} ctx e () of
|
adamc@21
|
504 S.Continue (e, ()) => e
|
adamc@21
|
505 | S.Return _ => raise Fail "CoreUtil.Exp.mapB: Impossible"
|
adamc@21
|
506
|
adamc@16
|
507 fun map {kind, con, exp} e =
|
adamc@16
|
508 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@16
|
509 con = fn c => fn () => S.Continue (con c, ()),
|
adamc@16
|
510 exp = fn e => fn () => S.Continue (exp e, ())} e () of
|
adamc@16
|
511 S.Return () => raise Fail "Core_util.Exp.map"
|
adamc@16
|
512 | S.Continue (e, ()) => e
|
adamc@16
|
513
|
adamc@23
|
514 fun fold {kind, con, exp} s e =
|
adamc@23
|
515 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
|
adamc@23
|
516 con = fn c => fn s => S.Continue (c, con (c, s)),
|
adamc@23
|
517 exp = fn e => fn s => S.Continue (e, exp (e, s))} e s of
|
adamc@23
|
518 S.Continue (_, s) => s
|
adamc@23
|
519 | S.Return _ => raise Fail "CoreUtil.Exp.fold: Impossible"
|
adamc@23
|
520
|
adamc@16
|
521 fun exists {kind, con, exp} k =
|
adamc@16
|
522 case mapfold {kind = fn k => fn () =>
|
adamc@16
|
523 if kind k then
|
adamc@16
|
524 S.Return ()
|
adamc@16
|
525 else
|
adamc@16
|
526 S.Continue (k, ()),
|
adamc@16
|
527 con = fn c => fn () =>
|
adamc@16
|
528 if con c then
|
adamc@16
|
529 S.Return ()
|
adamc@16
|
530 else
|
adamc@16
|
531 S.Continue (c, ()),
|
adamc@16
|
532 exp = fn e => fn () =>
|
adamc@16
|
533 if exp e then
|
adamc@16
|
534 S.Return ()
|
adamc@16
|
535 else
|
adamc@16
|
536 S.Continue (e, ())} k () of
|
adamc@16
|
537 S.Return _ => true
|
adamc@16
|
538 | S.Continue _ => false
|
adamc@16
|
539
|
adamc@16
|
540 end
|
adamc@16
|
541
|
adamc@20
|
542 structure Decl = struct
|
adamc@20
|
543
|
adamc@20
|
544 datatype binder = datatype Exp.binder
|
adamc@20
|
545
|
adamc@20
|
546 fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
|
adamc@20
|
547 let
|
adamc@20
|
548 val mfk = Kind.mapfold fk
|
adamc@20
|
549
|
adamc@20
|
550 fun bind' (ctx, b) =
|
adamc@20
|
551 let
|
adamc@20
|
552 val b' = case b of
|
adamc@20
|
553 Con.Rel x => RelC x
|
adamc@20
|
554 | Con.Named x => NamedC x
|
adamc@20
|
555 in
|
adamc@20
|
556 bind (ctx, b')
|
adamc@20
|
557 end
|
adamc@20
|
558 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
|
adamc@20
|
559
|
adamc@20
|
560 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind}
|
adamc@20
|
561
|
adamc@20
|
562 fun mfd ctx d acc =
|
adamc@20
|
563 S.bindP (mfd' ctx d acc, fd ctx)
|
adamc@20
|
564
|
adamc@20
|
565 and mfd' ctx (dAll as (d, loc)) =
|
adamc@20
|
566 case d of
|
adamc@20
|
567 DCon (x, n, k, c) =>
|
adamc@20
|
568 S.bind2 (mfk k,
|
adamc@20
|
569 fn k' =>
|
adamc@20
|
570 S.map2 (mfc ctx c,
|
adamc@20
|
571 fn c' =>
|
adamc@20
|
572 (DCon (x, n, k', c'), loc)))
|
adamc@192
|
573 | DDatatype (x, n, xs, xncs) =>
|
adamc@196
|
574 let
|
adamc@196
|
575 val k = (KType, loc)
|
adamc@196
|
576 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
|
adamc@196
|
577 val ctx' = bind (ctx, NamedC (x, n, k', NONE))
|
adamc@196
|
578 in
|
adamc@196
|
579 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
|
adamc@196
|
580 case c of
|
adamc@196
|
581 NONE => S.return2 (x, n, c)
|
adamc@196
|
582 | SOME c =>
|
adamc@196
|
583 S.map2 (mfc ctx' c,
|
adamc@196
|
584 fn c' => (x, n, SOME c'))) xncs,
|
adamc@196
|
585 fn xncs' =>
|
adamc@196
|
586 (DDatatype (x, n, xs, xncs'), loc))
|
adamc@196
|
587 end
|
adamc@125
|
588 | DVal vi =>
|
adamc@125
|
589 S.map2 (mfvi ctx vi,
|
adamc@125
|
590 fn vi' =>
|
adamc@125
|
591 (DVal vi', loc))
|
adamc@125
|
592 | DValRec vis =>
|
adamc@127
|
593 let
|
adamc@127
|
594 val ctx = foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
|
adamc@127
|
595 ctx vis
|
adamc@127
|
596 in
|
adamc@127
|
597 S.map2 (ListUtil.mapfold (mfvi ctx) vis,
|
adamc@127
|
598 fn vis' =>
|
adamc@127
|
599 (DValRec vis', loc))
|
adamc@127
|
600 end
|
adamc@109
|
601 | DExport _ => S.return2 dAll
|
adamc@125
|
602
|
adamc@125
|
603 and mfvi ctx (x, n, t, e, s) =
|
adamc@125
|
604 S.bind2 (mfc ctx t,
|
adamc@125
|
605 fn t' =>
|
adamc@125
|
606 S.map2 (mfe ctx e,
|
adamc@125
|
607 fn e' =>
|
adamc@125
|
608 (x, n, t', e', s)))
|
adamc@20
|
609 in
|
adamc@20
|
610 mfd
|
adamc@20
|
611 end
|
adamc@20
|
612
|
adamc@23
|
613 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
|
adamc@23
|
614 mapfoldB {kind = fk,
|
adamc@23
|
615 con = fn () => fc,
|
adamc@23
|
616 exp = fn () => fe,
|
adamc@23
|
617 decl = fn () => fd,
|
adamc@23
|
618 bind = fn ((), _) => ()} ()
|
adamc@23
|
619
|
adamc@23
|
620 fun fold {kind, con, exp, decl} s d =
|
adamc@23
|
621 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
|
adamc@23
|
622 con = fn c => fn s => S.Continue (c, con (c, s)),
|
adamc@23
|
623 exp = fn e => fn s => S.Continue (e, exp (e, s)),
|
adamc@23
|
624 decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
|
adamc@23
|
625 S.Continue (_, s) => s
|
adamc@23
|
626 | S.Return _ => raise Fail "CoreUtil.Decl.fold: Impossible"
|
adamc@23
|
627
|
adamc@110
|
628 fun foldMap {kind, con, exp, decl} s d =
|
adamc@110
|
629 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
|
adamc@110
|
630 con = fn c => fn s => S.Continue (con (c, s)),
|
adamc@110
|
631 exp = fn e => fn s => S.Continue (exp (e, s)),
|
adamc@110
|
632 decl = fn d => fn s => S.Continue (decl (d, s))} d s of
|
adamc@110
|
633 S.Continue v => v
|
adamc@110
|
634 | S.Return _ => raise Fail "CoreUtil.Decl.foldMap: Impossible"
|
adamc@110
|
635
|
adamc@16
|
636 end
|
adamc@20
|
637
|
adamc@20
|
638 structure File = struct
|
adamc@20
|
639
|
adamc@20
|
640 datatype binder = datatype Exp.binder
|
adamc@20
|
641
|
adamc@20
|
642 fun mapfoldB (all as {bind, ...}) =
|
adamc@20
|
643 let
|
adamc@20
|
644 val mfd = Decl.mapfoldB all
|
adamc@20
|
645
|
adamc@20
|
646 fun mff ctx ds =
|
adamc@20
|
647 case ds of
|
adamc@20
|
648 nil => S.return2 nil
|
adamc@20
|
649 | d :: ds' =>
|
adamc@20
|
650 S.bind2 (mfd ctx d,
|
adamc@20
|
651 fn d' =>
|
adamc@20
|
652 let
|
adamc@100
|
653 val ctx' =
|
adamc@20
|
654 case #1 d' of
|
adamc@100
|
655 DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c))
|
adamc@192
|
656 | DDatatype (x, n, xs, xncs) =>
|
adamc@163
|
657 let
|
adamc@192
|
658 val loc = #2 d'
|
adamc@192
|
659 val k = (KType, loc)
|
adamc@192
|
660 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
|
adamc@192
|
661
|
adamc@192
|
662 val ctx = bind (ctx, NamedC (x, n, k', NONE))
|
adamc@163
|
663 val t = (CNamed n, #2 d')
|
adamc@192
|
664 val t = ListUtil.foldli (fn (i, _, t) => (CApp (t, (CRel i, loc)), loc))
|
adamc@192
|
665 t xs
|
adamc@163
|
666 in
|
adamc@163
|
667 foldl (fn ((x, n, to), ctx) =>
|
adamc@163
|
668 let
|
adamc@163
|
669 val t = case to of
|
adamc@163
|
670 NONE => t
|
adamc@163
|
671 | SOME t' => (TFun (t', t), #2 d')
|
adamc@192
|
672 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc))
|
adamc@192
|
673 t xs
|
adamc@163
|
674 in
|
adamc@163
|
675 bind (ctx, NamedE (x, n, t, NONE, ""))
|
adamc@163
|
676 end)
|
adamc@163
|
677 ctx xncs
|
adamc@163
|
678 end
|
adamc@109
|
679 | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s))
|
adamc@125
|
680 | DValRec vis =>
|
adamc@127
|
681 foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
|
adamc@125
|
682 ctx vis
|
adamc@109
|
683 | DExport _ => ctx
|
adamc@20
|
684 in
|
adamc@20
|
685 S.map2 (mff ctx' ds',
|
adamc@20
|
686 fn ds' =>
|
adamc@20
|
687 d' :: ds')
|
adamc@20
|
688 end)
|
adamc@20
|
689 in
|
adamc@20
|
690 mff
|
adamc@20
|
691 end
|
adamc@20
|
692
|
adamc@23
|
693 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
|
adamc@23
|
694 mapfoldB {kind = fk,
|
adamc@23
|
695 con = fn () => fc,
|
adamc@23
|
696 exp = fn () => fe,
|
adamc@23
|
697 decl = fn () => fd,
|
adamc@23
|
698 bind = fn ((), _) => ()} ()
|
adamc@23
|
699
|
adamc@20
|
700 fun mapB {kind, con, exp, decl, bind} ctx ds =
|
adamc@20
|
701 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
|
adamc@20
|
702 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
|
adamc@20
|
703 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
|
adamc@20
|
704 decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()),
|
adamc@20
|
705 bind = bind} ctx ds () of
|
adamc@20
|
706 S.Continue (ds, ()) => ds
|
adamc@20
|
707 | S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible"
|
adamc@20
|
708
|
adamc@23
|
709 fun fold {kind, con, exp, decl} s d =
|
adamc@23
|
710 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
|
adamc@23
|
711 con = fn c => fn s => S.Continue (c, con (c, s)),
|
adamc@23
|
712 exp = fn e => fn s => S.Continue (e, exp (e, s)),
|
adamc@23
|
713 decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
|
adamc@23
|
714 S.Continue (_, s) => s
|
adamc@23
|
715 | S.Return _ => raise Fail "CoreUtil.File.fold: Impossible"
|
adamc@23
|
716
|
adamc@110
|
717 fun foldMap {kind, con, exp, decl} s d =
|
adamc@110
|
718 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
|
adamc@110
|
719 con = fn c => fn s => S.Continue (con (c, s)),
|
adamc@110
|
720 exp = fn e => fn s => S.Continue (exp (e, s)),
|
adamc@110
|
721 decl = fn d => fn s => S.Continue (decl (d, s))} d s of
|
adamc@110
|
722 S.Continue v => v
|
adamc@110
|
723 | S.Return _ => raise Fail "CoreUtil.File.foldMap: Impossible"
|
adamc@110
|
724
|
adamc@179
|
725 val maxName = foldl (fn ((d, _) : decl, count) =>
|
adamc@179
|
726 case d of
|
adamc@179
|
727 DCon (_, n, _, _) => Int.max (n, count)
|
adamc@192
|
728 | DDatatype (_, n, _, _) => Int.max (n, count)
|
adamc@179
|
729 | DVal (_, n, _, _, _) => Int.max (n, count)
|
adamc@179
|
730 | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis
|
adamc@179
|
731 | DExport _ => count) 0
|
adamc@179
|
732
|
adamc@20
|
733 end
|
adamc@20
|
734
|
adamc@20
|
735 end
|