Mercurial > urweb

comparison src/elaborate.sml @ 74:144d082b47ae

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Reduce efold
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Jun 2008 12:12:06 -0400
parents 6431b315a1e3
children 88ffb3d61817
comparison
equal deleted inserted replaced
73:8b611ecc5f2d 74:144d082b47ae
418 val subConInCon = 418 val subConInCon =
419 U.Con.mapB {kind = fn k => k, 419 U.Con.mapB {kind = fn k => k,
420 con = fn (xn, rep) => fn c => 420 con = fn (xn, rep) => fn c =>
421 case c of 421 case c of
422 L'.CRel xn' => 422 L'.CRel xn' =>
423 if xn = xn' then 423 (case Int.compare (xn', xn) of
424 #1 rep 424 EQUAL => #1 rep
425 else 425 | GREATER => L'.CRel (xn' - 1)
426 c 426 | LESS => c)
427 (*| L'.CUnif _ => raise SynUnif*) 427 (*| L'.CUnif _ => raise SynUnif*)
428 | _ => c, 428 | _ => c,
429 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) 429 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
430 | (ctx, _) => ctx} 430 | (ctx, _) => ctx}
431 431
648 | SOME (_, SOME c) => hnormCon env c 648 | SOME (_, SOME c) => hnormCon env c
649 end 649 end
650 650
651 | L'.CApp (c1, c2) => 651 | L'.CApp (c1, c2) =>
652 (case #1 (hnormCon env c1) of 652 (case #1 (hnormCon env c1) of
653 L'.CAbs (_, _, cb) => 653 L'.CAbs (x, k, cb) =>
654 ((hnormCon env (subConInCon (0, c2) cb)) 654 let
655 handle SynUnif => cAll) 655 val sc = (hnormCon env (subConInCon (0, c2) cb))
656 handle SynUnif => cAll
657 (*val env' = E.pushCRel env x k*)
658 in
659 (*eprefaces "Subst" [("x", Print.PD.string x),
660 ("cb", p_con env' cb),
661 ("c2", p_con env c2),
662 ("sc", p_con env sc)];*)
663 sc
664 end
656 | L'.CApp (c', i) => 665 | L'.CApp (c', i) =>
657 (case #1 (hnormCon env c') of 666 (case #1 (hnormCon env c') of
658 L'.CApp (c', f) => 667 L'.CApp (c', f) =>
659 (case #1 (hnormCon env c') of 668 (case #1 (hnormCon env c') of
660 L'.CFold ks => 669 L'.CFold ks =>
666 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc), 675 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
667 (L'.CRecord (k, rest), loc)), loc)), loc) 676 (L'.CRecord (k, rest), loc)), loc)), loc)
668 | L'.CConcat ((L'.CRecord (k, (x, c) :: rest), _), rest') => 677 | L'.CConcat ((L'.CRecord (k, (x, c) :: rest), _), rest') =>
669 let 678 let
670 val rest'' = (L'.CConcat ((L'.CRecord (k, rest), loc), rest'), loc) 679 val rest'' = (L'.CConcat ((L'.CRecord (k, rest), loc), rest'), loc)
680
681 (*val ccc = (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
682 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
683 rest''), loc)), loc)*)
671 in 684 in
685 (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*)
672 hnormCon env 686 hnormCon env
673 (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc), 687 (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
674 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc), 688 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
675 rest''), loc)), loc) 689 rest''), loc)), loc)
676 end 690 end