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