Mercurial > urweb

comparison src/elaborate.sml @ 622:d64533157f40

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Debug reverse-engineering unification
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 16:11:56 -0500
parents 8998114760c1
children 588b9d16b00a
comparison
equal deleted inserted replaced
621:8998114760c1 622:d64533157f40
780 | L'.CRecord (_, [(x, v)]) => 780 | L'.CRecord (_, [(x, v)]) =>
781 let 781 let
782 val v' = case dom of 782 val v' = case dom of
783 (L'.KUnit, _) => (L'.CUnit, loc) 783 (L'.KUnit, _) => (L'.CUnit, loc)
784 | _ => cunif (loc, dom) 784 | _ => cunif (loc, dom)
785 val gs2 = unifyCons (env, denv) v' (L'.CApp (f, v), loc) 785 val gs2 = unifyCons (env, denv) v (L'.CApp (f, v'), loc)
786 786
787 val gs3 = unifyCons (env, denv) r (L'.CRecord (dom, [(x, v')]), loc) 787 val gs3 = unifyCons (env, denv) r (L'.CRecord (dom, [(x, v')]), loc)
788 in 788 in
789 gs1 @ gs2 @ gs3 789 gs1 @ gs2 @ gs3
790 end 790 end
791 | L'.CRecord (_, (x, v) :: rest) => 791 | L'.CRecord (_, (x, v) :: rest) =>
792 let 792 let
793 val r1 = cunif (loc, (L'.KRecord dom, loc)) 793 val r1 = cunif (loc, (L'.KRecord dom, loc))
794 val r2 = cunif (loc, (L'.KRecord dom, loc)) 794 val r2 = cunif (loc, (L'.KRecord dom, loc))
795 val gs2 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc) 795
796 796 val gs2 = unfold (r1, (L'.CRecord (ran, [(x, v)]), loc))
797 val gs3 = unfold (r1, (L'.CRecord (ran, [(x, v)]), loc)) 797 val gs3 = unfold (r2, (L'.CRecord (ran, rest), loc))
798 val gs4 = unfold (r2, (L'.CRecord (ran, rest), loc)) 798 val gs4 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc)
799 in 799 in
800 gs1 @ gs2 @ gs3 @ gs4 800 gs1 @ gs2 @ gs3 @ gs4
801 end 801 end
802 | L'.CConcat (c1', c2') => 802 | L'.CConcat (c1', c2') =>
803 let 803 let
804 val r1 = cunif (loc, (L'.KRecord dom, loc)) 804 val r1 = cunif (loc, (L'.KRecord dom, loc))
805 val r2 = cunif (loc, (L'.KRecord dom, loc)) 805 val r2 = cunif (loc, (L'.KRecord dom, loc))
806 val gs2 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc) 806
807 807 val gs2 = unfold (r1, c1')
808 val gs3 = unfold (r1, c1') 808 val gs3 = unfold (r2, c2')
809 val gs4 = unfold (r2, c2') 809 val gs4 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc)
810 in 810 in
811 gs1 @ gs2 @ gs3 @ gs4 811 gs1 @ gs2 @ gs3 @ gs4
812 end 812 end
813 | _ => raise ex 813 | _ => raise ex
814 end 814 end
815 in 815 in
816 unfold (r, c) 816 unfold (r, c)
817 end 817 end
818 handle _ => raise ex 818 handle _ => (TextIO.print "Guess failure!\n"; raise ex)
819 in 819 in
820 case (#1 c1, #1 c2) of 820 case (#1 c1, #1 c2) of
821 (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) => 821 (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) =>
822 unfold (dom, ran, f, r, c2) 822 unfold (dom, ran, f, r, c2)
823 | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) => 823 | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) =>