comparison src/reduce.sml @ 1179:c58453683bbb

Dead code elimination in Reduce code
author Adam Chlipala <adamc@hcoop.net>
date Thu, 04 Mar 2010 16:59:13 -0500
parents 51e596feec37
children 618f9f458da9
comparison
equal deleted inserted replaced
1178:6373a0432338 1179:c58453683bbb
40 if n = 0 then 40 if n = 0 then
41 e 41 e
42 else 42 else
43 multiLiftExpInExp (n - 1) (E.liftExpInExp 0 e) 43 multiLiftExpInExp (n - 1) (E.liftExpInExp 0 e)
44 44
45 val count = CoreUtil.Exp.foldB {kind = fn (_, _, c) => c,
46 con = fn (_, _, c) => c,
47 exp = fn (x, e, c) =>
48 case e of
49 ERel x' => if x = x' then c + 1 else c
50 | _ => c,
51 bind = fn (x, b) =>
52 case b of
53 CoreUtil.Exp.RelE _ => x+1
54 | _ => x} 0 0
55
45 val dangling = 56 val dangling =
46 CoreUtil.Exp.existsB {kind = fn _ => false, 57 CoreUtil.Exp.existsB {kind = fn _ => false,
47 con = fn _ => false, 58 con = fn _ => false,
48 exp = fn (n, e) => 59 exp = fn (n, e) =>
49 case e of 60 case e of
405 416
406 | EApp (e1, e2) => 417 | EApp (e1, e2) =>
407 let 418 let
408 val env' = deKnown env 419 val env' = deKnown env
409 420
410 fun reassoc e =
411 case #1 e of
412 EApp
413 ((EApp
414 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), mt),
415 _), _), _), t3), _),
416 me), _),
417 (EApp ((EApp
418 ((EApp ((ECApp ((ECApp ((ECApp (
419 (EFfi ("Basis", "bind"), _), _), _),
420 t1), _), t2), _),
421 _), _),
422 trans1), _), (EAbs (_, _, _, trans2), _)), _)), _),
423 trans3) =>
424 let
425 val e'' = (EFfi ("Basis", "bind"), loc)
426 val e'' = (ECApp (e'', mt), loc)
427 val e'' = (ECApp (e'', t2), loc)
428 val e'' = (ECApp (e'', t3), loc)
429 val e'' = (EApp (e'', me), loc)
430 val e'' = (EApp (e'', trans2), loc)
431 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
432 val e'' = reassoc e''
433 val e'' = (EAbs ("xb", t1, (CApp (mt, t3), loc), e''), loc)
434
435 val e' = (EFfi ("Basis", "bind"), loc)
436 val e' = (ECApp (e', mt), loc)
437 val e' = (ECApp (e', t1), loc)
438 val e' = (ECApp (e', t3), loc)
439 val e' = (EApp (e', me), loc)
440 val e' = (EApp (e', trans1), loc)
441 val e' = (EApp (e', e''), loc)
442 in
443 e'
444 end
445
446 | EApp
447 ((EApp
448 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), mt),
449 _), _), _), t3), _),
450 me), _),
451 (EApp ((EApp
452 ((EApp ((ECApp ((ECApp ((ECApp (
453 (EFfi ("Basis", "bind"), _), _), _),
454 t1), _), t2), _),
455 _), _),
456 trans1), _), trans2), _)), _),
457 trans3) =>
458 let
459 val e'' = (EFfi ("Basis", "bind"), loc)
460 val e'' = (ECApp (e'', mt), loc)
461 val e'' = (ECApp (e'', t2), loc)
462 val e'' = (ECApp (e'', t3), loc)
463 val e'' = (EApp (e'', me), loc)
464 val () = print "In2\n"
465 val e'' = (EApp (e'', exp (UnknownE :: env')
466 (EApp (E.liftExpInExp 0 trans2, (ERel 0, loc)),
467 loc)),
468 loc)
469 val () = print "Out2\n"
470 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
471 val e'' = reassoc e''
472 val e'' = (EAbs ("xb", t1, (CApp (mt, t3), loc), e''), loc)
473
474 val e' = (EFfi ("Basis", "bind"), loc)
475 val e' = (ECApp (e', mt), loc)
476 val e' = (ECApp (e', t1), loc)
477 val e' = (ECApp (e', t3), loc)
478 val e' = (EApp (e', me), loc)
479 val e' = (EApp (e', trans1), loc)
480 val e' = (EApp (e', e''), loc)
481 in
482 e'
483 end
484
485 | EApp
486 ((EApp
487 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _),
488 t1),
489 _), t2), _),
490 (EFfi ("Basis", "transaction_monad"), _)), _),
491 (ECase (e, pes, {disc, ...}), _)), _), trans) =>
492 let
493 val e' = (EFfi ("Basis", "bind"), loc)
494 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
495 val e' = (ECApp (e', t1), loc)
496 val e' = (ECApp (e', t2), loc)
497 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
498
499 fun doCase (p, e) =
500 let
501 val e' = (EApp (e', e), loc)
502 val e' = (EApp (e',
503 multiLiftExpInExp (E.patBindsN p)
504 trans), loc)
505 in
506 (p, reassoc e')
507 end
508 in
509 (ECase (e, map doCase pes,
510 {disc = disc,
511 result = (CApp ((CFfi ("Basis", "transaction"), loc),
512 t2), loc)}), loc)
513 end
514
515 | _ => e
516
517 val e1 = exp env e1 421 val e1 = exp env e1
518 val e2 = exp env e2 422 val e2 = exp env e2
519 val e12 = (*reassoc*) (EApp (e1, e2), loc) 423 in
520 in 424 case #1 e1 of
521 case #1 e12 of 425 EAbs (_, _, _, b) =>
522 EApp ((EAbs (_, _, _, b), _), e2) =>
523 exp (KnownE e2 :: env') b 426 exp (KnownE e2 :: env') b
524 | _ => e12 427 | _ => (EApp (e1, e2), loc)
525 end 428 end
526 429
527 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc) 430 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc)
528 431
529 | ECApp (e, c) => 432 | ECApp (e, c) =>