Mercurial > urweb
comparison src/core_util.sml @ 20:1ab48e37d0ef
Some con reducing
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 08 Jun 2008 15:47:44 -0400 |
parents | bc7b76ca57e0 |
children | 067029c748e9 |
comparison
equal
deleted
inserted
replaced
19:e634ae817a8e | 20:1ab48e37d0ef |
---|---|
77 | 77 |
78 structure Con = struct | 78 structure Con = struct |
79 | 79 |
80 datatype binder = | 80 datatype binder = |
81 Rel of string * kind | 81 Rel of string * kind |
82 | Named of string * kind | 82 | Named of string * int * kind * con option |
83 | 83 |
84 fun mapfoldB {kind = fk, con = fc, bind} = | 84 fun mapfoldB {kind = fk, con = fc, bind} = |
85 let | 85 let |
86 val mfk = Kind.mapfold fk | 86 val mfk = Kind.mapfold fk |
87 | 87 |
160 fun mapB {kind, con, bind} ctx c = | 160 fun mapB {kind, con, bind} ctx c = |
161 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), | 161 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), |
162 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), | 162 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), |
163 bind = bind} ctx c () of | 163 bind = bind} ctx c () of |
164 S.Continue (c, ()) => c | 164 S.Continue (c, ()) => c |
165 | S.Return _ => raise Fail "Con.mapB: Impossible" | 165 | S.Return _ => raise Fail "CoreUtil.Con.mapB: Impossible" |
166 | 166 |
167 fun exists {kind, con} k = | 167 fun exists {kind, con} k = |
168 case mapfold {kind = fn k => fn () => | 168 case mapfold {kind = fn k => fn () => |
169 if kind k then | 169 if kind k then |
170 S.Return () | 170 S.Return () |
182 | 182 |
183 structure Exp = struct | 183 structure Exp = struct |
184 | 184 |
185 datatype binder = | 185 datatype binder = |
186 RelC of string * kind | 186 RelC of string * kind |
187 | NamedC of string * kind | 187 | NamedC of string * int * kind * con option |
188 | RelE of string * con | 188 | RelE of string * con |
189 | NamedE of string * con | 189 | NamedE of string * int * con * exp option |
190 | 190 |
191 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = | 191 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = |
192 let | 192 let |
193 val mfk = Kind.mapfold fk | 193 val mfk = Kind.mapfold fk |
194 | 194 |
292 S.Return _ => true | 292 S.Return _ => true |
293 | S.Continue _ => false | 293 | S.Continue _ => false |
294 | 294 |
295 end | 295 end |
296 | 296 |
297 end | 297 structure Decl = struct |
298 | |
299 datatype binder = datatype Exp.binder | |
300 | |
301 fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} = | |
302 let | |
303 val mfk = Kind.mapfold fk | |
304 | |
305 fun bind' (ctx, b) = | |
306 let | |
307 val b' = case b of | |
308 Con.Rel x => RelC x | |
309 | Con.Named x => NamedC x | |
310 in | |
311 bind (ctx, b') | |
312 end | |
313 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'} | |
314 | |
315 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind} | |
316 | |
317 fun mfd ctx d acc = | |
318 S.bindP (mfd' ctx d acc, fd ctx) | |
319 | |
320 and mfd' ctx (dAll as (d, loc)) = | |
321 case d of | |
322 DCon (x, n, k, c) => | |
323 S.bind2 (mfk k, | |
324 fn k' => | |
325 S.map2 (mfc ctx c, | |
326 fn c' => | |
327 (DCon (x, n, k', c'), loc))) | |
328 | DVal (x, n, t, e) => | |
329 S.bind2 (mfc ctx t, | |
330 fn t' => | |
331 S.map2 (mfe ctx e, | |
332 fn e' => | |
333 (DVal (x, n, t', e'), loc))) | |
334 in | |
335 mfd | |
336 end | |
337 | |
338 end | |
339 | |
340 structure File = struct | |
341 | |
342 datatype binder = datatype Exp.binder | |
343 | |
344 fun mapfoldB (all as {bind, ...}) = | |
345 let | |
346 val mfd = Decl.mapfoldB all | |
347 | |
348 fun mff ctx ds = | |
349 case ds of | |
350 nil => S.return2 nil | |
351 | d :: ds' => | |
352 S.bind2 (mfd ctx d, | |
353 fn d' => | |
354 let | |
355 val b = | |
356 case #1 d' of | |
357 DCon (x, n, k, c) => NamedC (x, n, k, SOME c) | |
358 | DVal (x, n, t, e) => NamedE (x, n, t, SOME e) | |
359 val ctx' = bind (ctx, b) | |
360 in | |
361 S.map2 (mff ctx' ds', | |
362 fn ds' => | |
363 d' :: ds') | |
364 end) | |
365 in | |
366 mff | |
367 end | |
368 | |
369 fun mapB {kind, con, exp, decl, bind} ctx ds = | |
370 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), | |
371 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), | |
372 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()), | |
373 decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()), | |
374 bind = bind} ctx ds () of | |
375 S.Continue (ds, ()) => ds | |
376 | S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible" | |
377 | |
378 end | |
379 | |
380 end |