Mercurial > urweb

comparison src/elaborate.sml @ 86:7f9bcc8bfa1e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More with disjointness assumptions
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 13:19:14 -0400
parents 1f85890c9846
children 7bab29834cd6
comparison
equal deleted inserted replaced
85:1f85890c9846 86:7f9bcc8bfa1e
543 | L'.CUnit => (L'.KUnit, loc) 543 | L'.CUnit => (L'.KUnit, loc)
544 544
545 | L'.CError => kerror 545 | L'.CError => kerror
546 | L'.CUnif (_, k, _, _) => k 546 | L'.CUnif (_, k, _, _) => k
547 547
548 fun unifyRecordCons env (c1, c2) = 548 fun hnormCon (env, denv) c =
549 let
550 val cAll as (c, loc) = ElabOps.hnormCon env c
551
552 fun doDisj (c1, c2, c) =
553 let
554 val (c, gs) = hnormCon (env, denv) c
555 in
556 (c,
557 map (fn cs => (loc, env, denv, cs)) (D.prove env denv (c1, c2, loc)) @ gs)
558 end
559 in
560 case c of
561 L'.CDisjoint cs => doDisj cs
562 | L'.TDisjoint cs => doDisj cs
563 | _ => (cAll, [])
564 end
565
566 fun unifyRecordCons (env, denv) (c1, c2) =
549 let 567 let
550 val k1 = kindof env c1 568 val k1 = kindof env c1
551 val k2 = kindof env c2 569 val k2 = kindof env c2
570
571 val (r1, gs1) = recordSummary (env, denv) c1
572 val (r2, gs2) = recordSummary (env, denv) c2
552 in 573 in
553 unifyKinds k1 k2; 574 unifyKinds k1 k2;
554 unifySummaries env (k1, recordSummary env c1, recordSummary env c2) 575 unifySummaries (env, denv) (k1, r1, r2);
576 gs1 @ gs2
555 end 577 end
556 578
557 and recordSummary env c : record_summary = 579 and recordSummary (env, denv) c =
558 case hnormCon env c of 580 let
559 (L'.CRecord (_, xcs), _) => {fields = xcs, unifs = [], others = []} 581 val (c, gs) = hnormCon (env, denv) c
560 | (L'.CConcat (c1, c2), _) => 582
561 let 583 val (sum, gs') =
562 val s1 = recordSummary env c1 584 case c of
563 val s2 = recordSummary env c2 585 (L'.CRecord (_, xcs), _) => ({fields = xcs, unifs = [], others = []}, [])
564 in 586 | (L'.CConcat (c1, c2), _) =>
565 {fields = #fields s1 @ #fields s2, 587 let
566 unifs = #unifs s1 @ #unifs s2, 588 val (s1, gs1) = recordSummary (env, denv) c1
567 others = #others s1 @ #others s2} 589 val (s2, gs2) = recordSummary (env, denv) c2
568 end 590 in
569 | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary env c 591 ({fields = #fields s1 @ #fields s2,
570 | c' as (L'.CUnif (_, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []} 592 unifs = #unifs s1 @ #unifs s2,
571 | c' => {fields = [], unifs = [], others = [c']} 593 others = #others s1 @ #others s2},
572 594 gs1 @ gs2)
573 and consEq env (c1, c2) = 595 end
574 (unifyCons env c1 c2; 596 | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary (env, denv) c
575 true) 597 | c' as (L'.CUnif (_, _, _, r), _) => ({fields = [], unifs = [(c', r)], others = []}, [])
598 | c' => ({fields = [], unifs = [], others = [c']}, [])
599 in
600 (sum, gs @ gs')
601 end
602
603 and consEq (env, denv) (c1, c2) =
604 (case unifyCons (env, denv) c1 c2 of
605 [] => true
606 | _ => false)
576 handle CUnify _ => false 607 handle CUnify _ => false
577 608
578 and consNeq env (c1, c2) = 609 and consNeq env (c1, c2) =
579 case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of 610 case (#1 (ElabOps.hnormCon env c1), #1 (ElabOps.hnormCon env c2)) of
580 (L'.CName x1, L'.CName x2) => x1 <> x2 611 (L'.CName x1, L'.CName x2) => x1 <> x2
581 | _ => false 612 | _ => false
582 613
583 and unifySummaries env (k, s1 : record_summary, s2 : record_summary) = 614 and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) =
584 let 615 let
585 (*val () = eprefaces "Summaries" [("#1", p_summary env s1), 616 (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
586 ("#2", p_summary env s2)]*) 617 ("#2", p_summary env s2)]*)
587 618
588 fun eatMatching p (ls1, ls2) = 619 fun eatMatching p (ls1, ls2) =
607 em (ls1, ls2, []) 638 em (ls1, ls2, [])
608 end 639 end
609 640
610 val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) => 641 val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
611 not (consNeq env (x1, x2)) 642 not (consNeq env (x1, x2))
612 andalso consEq env (c1, c2) 643 andalso consEq (env, denv) (c1, c2)
613 andalso consEq env (x1, x2)) 644 andalso consEq (env, denv) (x1, x2))
614 (#fields s1, #fields s2) 645 (#fields s1, #fields s2)
615 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}), 646 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
616 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*) 647 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
617 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2) 648 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
618 val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2) 649 val (others1, others2) = eatMatching (consEq (env, denv)) (#others s1, #others s2)
619 650
620 fun unifFields (fs, others, unifs) = 651 fun unifFields (fs, others, unifs) =
621 case (fs, others, unifs) of 652 case (fs, others, unifs) of
622 ([], [], _) => ([], [], unifs) 653 ([], [], _) => ([], [], unifs)
623 | (_, _, []) => (fs, others, []) 654 | (_, _, []) => (fs, others, [])
643 end 674 end
644 675
645 val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2) 676 val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
646 val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1) 677 val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
647 678
648 val clear1 = case (fs1, others1) of 679 val clear = case (fs1, others1, fs2, others2) of
649 ([], []) => true 680 ([], [], [], []) => true
650 | _ => false
651 val clear2 = case (fs2, others2) of
652 ([], []) => true
653 | _ => false 681 | _ => false
654 val empty = (L'.CRecord (k, []), dummy) 682 val empty = (L'.CRecord (k, []), dummy)
655 fun pairOffUnifs (unifs1, unifs2) = 683 fun pairOffUnifs (unifs1, unifs2) =
656 case (unifs1, unifs2) of 684 case (unifs1, unifs2) of
657 ([], _) => 685 ([], _) =>
658 if clear1 then 686 if clear then
659 List.app (fn (_, r) => r := SOME empty) unifs2 687 List.app (fn (_, r) => r := SOME empty) unifs2
660 else 688 else
661 raise CUnify' CRecordFailure 689 raise CUnify' CRecordFailure
662 | (_, []) => 690 | (_, []) =>
663 if clear2 then 691 if clear then
664 List.app (fn (_, r) => r := SOME empty) unifs1 692 List.app (fn (_, r) => r := SOME empty) unifs1
665 else 693 else
666 raise CUnify' CRecordFailure 694 raise CUnify' CRecordFailure
667 | ((c1, _) :: rest1, (_, r2) :: rest2) => 695 | ((c1, _) :: rest1, (_, r2) :: rest2) =>
668 (r2 := SOME c1; 696 (r2 := SOME c1;
669 pairOffUnifs (rest1, rest2)) 697 pairOffUnifs (rest1, rest2))
670 in 698 in
671 pairOffUnifs (unifs1, unifs2) 699 pairOffUnifs (unifs1, unifs2)
672 end 700 end
673 701
674 702 and unifyCons' (env, denv) c1 c2 =
675 and unifyCons' env c1 c2 = 703 let
676 unifyCons'' env (hnormCon env c1) (hnormCon env c2) 704 val (c1, gs1) = hnormCon (env, denv) c1
705 val (c2, gs2) = hnormCon (env, denv) c2
706 in
707 unifyCons'' (env, denv) c1 c2;
708 gs1 @ gs2
709 end
677 710
678 and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) = 711 and unifyCons'' (env, denv) (c1All as (c1, _)) (c2All as (c2, _)) =
679 let 712 let
680 fun err f = raise CUnify' (f (c1All, c2All)) 713 fun err f = raise CUnify' (f (c1All, c2All))
681 714
682 fun isRecord () = unifyRecordCons env (c1All, c2All) 715 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
683 in 716 in
684 case (c1, c2) of 717 case (c1, c2) of
685 (L'.TFun (d1, r1), L'.TFun (d2, r2)) => 718 (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
686 (unifyCons' env d1 d2; 719 unifyCons' (env, denv) d1 d2
687 unifyCons' env r1 r2) 720 @ unifyCons' (env, denv) r1 r2
688 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => 721 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
689 if expl1 <> expl2 then 722 if expl1 <> expl2 then
690 err CExplicitness 723 err CExplicitness
691 else 724 else
692 (unifyKinds d1 d2; 725 (unifyKinds d1 d2;
693 unifyCons' (E.pushCRel env x1 d1) r1 r2) 726 unifyCons' (E.pushCRel env x1 d1, D.enter denv) r1 r2)
694 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2 727 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2
695 728
696 | (L'.CRel n1, L'.CRel n2) => 729 | (L'.CRel n1, L'.CRel n2) =>
697 if n1 = n2 then 730 if n1 = n2 then
698 () 731 []
699 else 732 else
700 err CIncompatible 733 err CIncompatible
701 | (L'.CNamed n1, L'.CNamed n2) => 734 | (L'.CNamed n1, L'.CNamed n2) =>
702 if n1 = n2 then 735 if n1 = n2 then
703 () 736 []
704 else 737 else
705 err CIncompatible 738 err CIncompatible
706 739
707 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => 740 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
708 (unifyCons' env d1 d2; 741 (unifyCons' (env, denv) d1 d2;
709 unifyCons' env r1 r2) 742 unifyCons' (env, denv) r1 r2)
710 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => 743 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
711 (unifyKinds k1 k2; 744 (unifyKinds k1 k2;
712 unifyCons' (E.pushCRel env x1 k1) c1 c2) 745 unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2)
713 746
714 | (L'.CName n1, L'.CName n2) => 747 | (L'.CName n1, L'.CName n2) =>
715 if n1 = n2 then 748 if n1 = n2 then
716 () 749 []
717 else 750 else
718 err CIncompatible 751 err CIncompatible
719 752
720 | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) => 753 | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
721 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then 754 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
722 () 755 []
723 else 756 else
724 err CIncompatible 757 err CIncompatible
725 758
726 | (L'.CError, _) => () 759 | (L'.CError, _) => []
727 | (_, L'.CError) => () 760 | (_, L'.CError) => []
728 761
729 | (L'.CUnif (_, _, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All 762 | (L'.CUnif (_, _, _, ref (SOME c1All)), _) => unifyCons' (env, denv) c1All c2All
730 | (_, L'.CUnif (_, _, _, ref (SOME c2All))) => unifyCons' env c1All c2All 763 | (_, L'.CUnif (_, _, _, ref (SOME c2All))) => unifyCons' (env, denv) c1All c2All
731 764
732 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => 765 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
733 if r1 = r2 then 766 if r1 = r2 then
734 () 767 []
735 else 768 else
736 (unifyKinds k1 k2; 769 (unifyKinds k1 k2;
737 r1 := SOME c2All) 770 r1 := SOME c2All;
771 [])
738 772
739 | (L'.CUnif (_, _, _, r), _) => 773 | (L'.CUnif (_, _, _, r), _) =>
740 if occursCon r c2All then 774 if occursCon r c2All then
741 err COccursCheckFailed 775 err COccursCheckFailed
742 else 776 else
743 r := SOME c2All 777 (r := SOME c2All;
778 [])
744 | (_, L'.CUnif (_, _, _, r)) => 779 | (_, L'.CUnif (_, _, _, r)) =>
745 if occursCon r c1All then 780 if occursCon r c1All then
746 err COccursCheckFailed 781 err COccursCheckFailed
747 else 782 else
748 r := SOME c1All 783 (r := SOME c1All;
784 [])
749 785
750 | (L'.CRecord _, _) => isRecord () 786 | (L'.CRecord _, _) => isRecord ()
751 | (_, L'.CRecord _) => isRecord () 787 | (_, L'.CRecord _) => isRecord ()
752 | (L'.CConcat _, _) => isRecord () 788 | (L'.CConcat _, _) => isRecord ()
753 | (_, L'.CConcat _) => isRecord () 789 | (_, L'.CConcat _) => isRecord ()
754 790
755 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) => 791 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
756 (unifyKinds dom1 dom2; 792 (unifyKinds dom1 dom2;
757 unifyKinds ran1 ran2) 793 unifyKinds ran1 ran2;
794 [])
758 795
759 | _ => err CIncompatible 796 | _ => err CIncompatible
760 end 797 end
761 798
762 and unifyCons env c1 c2 = 799 and unifyCons (env, denv) c1 c2 =
763 unifyCons' env c1 c2 800 unifyCons' (env, denv) c1 c2
764 handle CUnify' err => raise CUnify (c1, c2, err) 801 handle CUnify' err => raise CUnify (c1, c2, err)
765 | KUnify args => raise CUnify (c1, c2, CKind args) 802 | KUnify args => raise CUnify (c1, c2, CKind args)
766 803
767 datatype exp_error = 804 datatype exp_error =
768 UnboundExp of ErrorMsg.span * string 805 UnboundExp of ErrorMsg.span * string
789 | WrongForm (variety, e, t) => 826 | WrongForm (variety, e, t) =>
790 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety); 827 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
791 eprefaces' [("Expression", p_exp env e), 828 eprefaces' [("Expression", p_exp env e),
792 ("Type", p_con env t)]) 829 ("Type", p_con env t)])
793 830
794 fun checkCon env e c1 c2 = 831 fun checkCon (env, denv) e c1 c2 =
795 unifyCons env c1 c2 832 unifyCons (env, denv) c1 c2
796 handle CUnify (c1, c2, err) => 833 handle CUnify (c1, c2, err) =>
797 expError env (Unify (e, c1, c2, err)) 834 (expError env (Unify (e, c1, c2, err));
835 [])
798 836
799 fun primType env p = 837 fun primType env p =
800 case p of 838 case p of
801 P.Int _ => !int 839 P.Int _ => !int
802 | P.Float _ => !float 840 | P.Float _ => !float
858 | L'.EField (_, _, {field, ...}) => field 896 | L'.EField (_, _, {field, ...}) => field
859 | L'.EFold dom => foldType (dom, loc) 897 | L'.EFold dom => foldType (dom, loc)
860 898
861 | L'.EError => cerror 899 | L'.EError => cerror
862 900
863 fun elabHead env (e as (_, loc)) t = 901 fun elabHead (env, denv) (e as (_, loc)) t =
864 let 902 let
865 fun unravel (t, e) = 903 fun unravel (t, e) =
866 case hnormCon env t of 904 let
867 (L'.TCFun (L'.Implicit, x, k, t'), _) => 905 val (t, gs) = hnormCon (env, denv) t
868 let 906 in
869 val u = cunif (loc, k) 907 case t of
870 in 908 (L'.TCFun (L'.Implicit, x, k, t'), _) =>
871 unravel (subConInCon (0, u) t', 909 let
872 (L'.ECApp (e, u), loc)) 910 val u = cunif (loc, k)
873 end 911
874 | _ => (e, t) 912 val (e, t, gs') = unravel (subConInCon (0, u) t',
913 (L'.ECApp (e, u), loc))
914 in
915 (e, t, gs @ gs')
916 end
917 | _ => (e, t, gs)
918 end
875 in 919 in
876 unravel (t, e) 920 unravel (t, e)
877 end 921 end
878 922
879 fun elabExp (env, denv) (e, loc) = 923 fun elabExp (env, denv) (e, loc) =
880 case e of 924 case e of
881 L.EAnnot (e, t) => 925 L.EAnnot (e, t) =>
882 let 926 let
883 val (e', et, gs1) = elabExp (env, denv) e 927 val (e', et, gs1) = elabExp (env, denv) e
884 val (t', _, gs2) = elabCon (env, denv) t 928 val (t', _, gs2) = elabCon (env, denv) t
885 in 929 val gs3 = checkCon (env, denv) e' et t'
886 checkCon env e' et t'; 930 in
887 (e', t', gs1 @ gs2) 931 (e', t', gs1 @ gs2 @ gs3)
888 end 932 end
889 933
890 | L.EPrim p => ((L'.EPrim p, loc), primType env p, []) 934 | L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
891 | L.EVar ([], s) => 935 | L.EVar ([], s) =>
892 (case E.lookupE env s of 936 (case E.lookupE env s of
917 end) 961 end)
918 962
919 | L.EApp (e1, e2) => 963 | L.EApp (e1, e2) =>
920 let 964 let
921 val (e1', t1, gs1) = elabExp (env, denv) e1 965 val (e1', t1, gs1) = elabExp (env, denv) e1
922 val (e1', t1) = elabHead env e1' t1 966 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
923 val (e2', t2, gs2) = elabExp (env, denv) e2 967 val (e2', t2, gs3) = elabExp (env, denv) e2
924 968
925 val dom = cunif (loc, ktype) 969 val dom = cunif (loc, ktype)
926 val ran = cunif (loc, ktype) 970 val ran = cunif (loc, ktype)
927 val t = (L'.TFun (dom, ran), dummy) 971 val t = (L'.TFun (dom, ran), dummy)
928 in 972
929 checkCon env e1' t1 t; 973 val gs4 = checkCon (env, denv) e1' t1 t
930 checkCon env e2' t2 dom; 974 val gs5 = checkCon (env, denv) e2' t2 dom
931 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2) 975 in
976 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2 @ gs3 @ gs4 @ gs5)
932 end 977 end
933 | L.EAbs (x, to, e) => 978 | L.EAbs (x, to, e) =>
934 let 979 let
935 val (t', gs1) = case to of 980 val (t', gs1) = case to of
936 NONE => (cunif (loc, ktype), []) 981 NONE => (cunif (loc, ktype), [])
948 gs1 @ gs2) 993 gs1 @ gs2)
949 end 994 end
950 | L.ECApp (e, c) => 995 | L.ECApp (e, c) =>
951 let 996 let
952 val (e', et, gs1) = elabExp (env, denv) e 997 val (e', et, gs1) = elabExp (env, denv) e
953 val (e', et) = elabHead env e' et 998 val (e', et, gs2) = elabHead (env, denv) e' et
954 val (c', ck, gs2) = elabCon (env, denv) c 999 val (c', ck, gs3) = elabCon (env, denv) c
955 in 1000 val ((et', _), gs4) = hnormCon (env, denv) et
956 case #1 (hnormCon env et) of 1001 in
1002 case et' of
957 L'.CError => (eerror, cerror, []) 1003 L'.CError => (eerror, cerror, [])
958 | L'.TCFun (_, _, k, eb) => 1004 | L'.TCFun (_, _, k, eb) =>
959 let 1005 let
960 val () = checkKind env c' ck k 1006 val () = checkKind env c' ck k
961 val eb' = subConInCon (0, c') eb 1007 val eb' = subConInCon (0, c') eb
962 handle SynUnif => (expError env (Unif ("substitution", eb)); 1008 handle SynUnif => (expError env (Unif ("substitution", eb));
963 cerror) 1009 cerror)
964 in 1010 in
965 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2) 1011 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ gs3 @ gs4)
966 end 1012 end
967 1013
968 | L'.CUnif _ => 1014 | L'.CUnif _ =>
969 (expError env (Unif ("application", et)); 1015 (expError env (Unif ("application", et));
970 (eerror, cerror, [])) 1016 (eerror, cerror, []))
1010 in 1056 in
1011 checkKind env x' xk kname; 1057 checkKind env x' xk kname;
1012 ((x', e', et), gs1 @ gs2 @ gs) 1058 ((x', e', et), gs1 @ gs2 @ gs)
1013 end) 1059 end)
1014 [] xes 1060 [] xes
1061
1062 val k = (L'.KType, loc)
1063
1064 fun prove (xets, gs) =
1065 case xets of
1066 [] => gs
1067 | (x, _, t) :: rest =>
1068 let
1069 val xc = (x, t)
1070 val r1 = (L'.CRecord (k, [xc]), loc)
1071 val gs = foldl (fn ((x', _, t'), gs) =>
1072 let
1073 val xc' = (x', t')
1074 val r2 = (L'.CRecord (k, [xc']), loc)
1075 in
1076 map (fn cs => (loc, env, denv, cs)) (D.prove env denv (r1, r2, loc))
1077 @ gs
1078 end)
1079 gs rest
1080 in
1081 prove (rest, gs)
1082 end
1015 in 1083 in
1016 ((L'.ERecord xes', loc), 1084 ((L'.ERecord xes', loc),
1017 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc), 1085 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
1018 gs) 1086 prove (xes', gs))
1019 end 1087 end
1020 1088
1021 | L.EField (e, c) => 1089 | L.EField (e, c) =>
1022 let 1090 let
1023 val (e', et, gs1) = elabExp (env, denv) e 1091 val (e', et, gs1) = elabExp (env, denv) e
1024 val (c', ck, gs2) = elabCon (env, denv) c 1092 val (c', ck, gs2) = elabCon (env, denv) c
1025 1093
1026 val ft = cunif (loc, ktype) 1094 val ft = cunif (loc, ktype)
1027 val rest = cunif (loc, ktype_record) 1095 val rest = cunif (loc, ktype_record)
1028 in 1096 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
1029 checkKind env c' ck kname; 1097
1030 checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc); 1098 val gs3 =
1031 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2) 1099 checkCon (env, denv) e' et
1100 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
1101 val gs4 =
1102 map (fn cs => (loc, env, denv, cs))
1103 (D.prove env denv (first, rest, loc))
1104 in
1105 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4)
1032 end 1106 end
1033 1107
1034 | L.EFold => 1108 | L.EFold =>
1035 let 1109 let
1036 val dom = kunif loc 1110 val dom = kunif loc
1371 | L'.DVal (x, n, t, _) => (L'.SgiVal (x, n, t), loc) 1445 | L'.DVal (x, n, t, _) => (L'.SgiVal (x, n, t), loc)
1372 | L'.DSgn (x, n, sgn) => (L'.SgiSgn (x, n, sgn), loc) 1446 | L'.DSgn (x, n, sgn) => (L'.SgiSgn (x, n, sgn), loc)
1373 | L'.DStr (x, n, sgn, _) => (L'.SgiStr (x, n, sgn), loc) 1447 | L'.DStr (x, n, sgn, _) => (L'.SgiStr (x, n, sgn), loc)
1374 | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc) 1448 | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc)
1375 1449
1376 fun subSgn env sgn1 (sgn2 as (_, loc2)) = 1450 fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
1377 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of 1451 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
1378 (L'.SgnError, _) => () 1452 (L'.SgnError, _) => ()
1379 | (_, L'.SgnError) => () 1453 | (_, L'.SgnError) => ()
1380 1454
1381 | (L'.SgnConst sgis1, L'.SgnConst sgis2) => 1455 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
1426 seek (fn sgi1All as (sgi1, _) => 1500 seek (fn sgi1All as (sgi1, _) =>
1427 case sgi1 of 1501 case sgi1 of
1428 L'.SgiCon (x', n1, k1, c1) => 1502 L'.SgiCon (x', n1, k1, c1) =>
1429 if x = x' then 1503 if x = x' then
1430 let 1504 let
1431 val () = unifyCons env c1 c2 1505 fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2))
1432 handle CUnify (c1, c2, err) =>
1433 sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err))
1434 in 1506 in
1435 SOME (E.pushCNamedAs env x n2 k2 (SOME c2)) 1507 (case unifyCons (env, denv) c1 c2 of
1508 [] => good ()
1509 | _ => NONE)
1510 handle CUnify (c1, c2, err) =>
1511 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
1512 good ())
1436 end 1513 end
1437 else 1514 else
1438 NONE 1515 NONE
1439 | _ => NONE) 1516 | _ => NONE)
1440 1517
1441 | L'.SgiVal (x, n2, c2) => 1518 | L'.SgiVal (x, n2, c2) =>
1442 seek (fn sgi1All as (sgi1, _) => 1519 seek (fn sgi1All as (sgi1, _) =>
1443 case sgi1 of 1520 case sgi1 of
1444 L'.SgiVal (x', n1, c1) => 1521 L'.SgiVal (x', n1, c1) =>
1445 if x = x' then 1522 if x = x' then
1446 let 1523 (case unifyCons (env, denv) c1 c2 of
1447 val () = unifyCons env c1 c2 1524 [] => SOME env
1448 handle CUnify (c1, c2, err) => 1525 | _ => NONE)
1449 sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)) 1526 handle CUnify (c1, c2, err) =>
1450 in 1527 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
1451 SOME env 1528 SOME env)
1452 end
1453 else 1529 else
1454 NONE 1530 NONE
1455 | _ => NONE) 1531 | _ => NONE)
1456 1532
1457 | L'.SgiStr (x, n2, sgn2) => 1533 | L'.SgiStr (x, n2, sgn2) =>
1458 seek (fn sgi1All as (sgi1, _) => 1534 seek (fn sgi1All as (sgi1, _) =>
1459 case sgi1 of 1535 case sgi1 of
1460 L'.SgiStr (x', n1, sgn1) => 1536 L'.SgiStr (x', n1, sgn1) =>
1461 if x = x' then 1537 if x = x' then
1462 let 1538 let
1463 val () = subSgn env sgn1 sgn2 1539 val () = subSgn (env, denv) sgn1 sgn2
1464 val env = E.pushStrNamedAs env x n1 sgn1 1540 val env = E.pushStrNamedAs env x n1 sgn1
1465 val env = if n1 = n2 then 1541 val env = if n1 = n2 then
1466 env 1542 env
1467 else 1543 else
1468 E.pushStrNamedAs env x n2 1544 E.pushStrNamedAs env x n2
1479 seek (fn sgi1All as (sgi1, _) => 1555 seek (fn sgi1All as (sgi1, _) =>
1480 case sgi1 of 1556 case sgi1 of
1481 L'.SgiSgn (x', n1, sgn1) => 1557 L'.SgiSgn (x', n1, sgn1) =>
1482 if x = x' then 1558 if x = x' then
1483 let 1559 let
1484 val () = subSgn env sgn1 sgn2 1560 val () = subSgn (env, denv) sgn1 sgn2
1485 val () = subSgn env sgn2 sgn1 1561 val () = subSgn (env, denv) sgn2 sgn1
1486 1562
1487 val env = E.pushSgnNamedAs env x n2 sgn2 1563 val env = E.pushSgnNamedAs env x n2 sgn2
1488 val env = if n1 = n2 then 1564 val env = if n1 = n2 then
1489 env 1565 env
1490 else 1566 else
1506 if n1 = n2 then 1582 if n1 = n2 then
1507 ran1 1583 ran1
1508 else 1584 else
1509 subStrInSgn (n1, n2) ran1 1585 subStrInSgn (n1, n2) ran1
1510 in 1586 in
1511 subSgn env dom2 dom1; 1587 subSgn (env, denv) dom2 dom1;
1512 subSgn (E.pushStrNamedAs env m2 n2 dom2) ran1 ran2 1588 subSgn (E.pushStrNamedAs env m2 n2 dom2, denv) ran1 ran2
1513 end 1589 end
1514 1590
1515 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) 1591 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
1516 1592
1517 1593
1536 NONE => (cunif (loc, ktype), ktype, []) 1612 NONE => (cunif (loc, ktype), ktype, [])
1537 | SOME c => elabCon (env, denv) c 1613 | SOME c => elabCon (env, denv) c
1538 1614
1539 val (e', et, gs2) = elabExp (env, denv) e 1615 val (e', et, gs2) = elabExp (env, denv) e
1540 val (env', n) = E.pushENamed env x c' 1616 val (env', n) = E.pushENamed env x c'
1541 in 1617
1542 checkCon env e' et c'; 1618 val gs3 = checkCon (env, denv) e' et c'
1543 1619 in
1544 ([(L'.DVal (x, n, c', e'), loc)], (env', gs1 @ gs2 @ gs)) 1620 ([(L'.DVal (x, n, c', e'), loc)], (env', gs1 @ gs2 @ gs3 @ gs))
1545 end 1621 end
1546 1622
1547 | L.DSgn (x, sgn) => 1623 | L.DSgn (x, sgn) =>
1548 let 1624 let
1549 val (sgn', gs') = elabSgn (env, denv) sgn 1625 val (sgn', gs') = elabSgn (env, denv) sgn
1600 | _ => str) 1676 | _ => str)
1601 | _ => str 1677 | _ => str
1602 1678
1603 val (str', actual, gs2) = elabStr (env, denv) str 1679 val (str', actual, gs2) = elabStr (env, denv) str
1604 in 1680 in
1605 subSgn env actual formal; 1681 subSgn (env, denv) actual formal;
1606 (str', formal, gs1 @ gs2) 1682 (str', formal, gs1 @ gs2)
1607 end 1683 end
1608 1684
1609 val (env', n) = E.pushStrNamed env x sgn' 1685 val (env', n) = E.pushStrNamed env x sgn'
1610 in 1686 in
1737 NONE => (actual, []) 1813 NONE => (actual, [])
1738 | SOME ran => 1814 | SOME ran =>
1739 let 1815 let
1740 val (ran', gs) = elabSgn (env', denv) ran 1816 val (ran', gs) = elabSgn (env', denv) ran
1741 in 1817 in
1742 subSgn env' actual ran'; 1818 subSgn (env', denv) actual ran';
1743 (ran', gs) 1819 (ran', gs)
1744 end 1820 end
1745 in 1821 in
1746 ((L'.StrFun (m, n, dom', formal, str'), loc), 1822 ((L'.StrFun (m, n, dom', formal, str'), loc),
1747 (L'.SgnFun (m, n, dom', formal), loc), 1823 (L'.SgnFun (m, n, dom', formal), loc),
1753 val (str2', sgn2, gs2) = elabStr (env, denv) str2 1829 val (str2', sgn2, gs2) = elabStr (env, denv) str2
1754 in 1830 in
1755 case #1 (hnormSgn env sgn1) of 1831 case #1 (hnormSgn env sgn1) of
1756 L'.SgnError => (strerror, sgnerror, []) 1832 L'.SgnError => (strerror, sgnerror, [])
1757 | L'.SgnFun (m, n, dom, ran) => 1833 | L'.SgnFun (m, n, dom, ran) =>
1758 (subSgn env sgn2 dom; 1834 (subSgn (env, denv) sgn2 dom;
1759 case #1 (hnormSgn env ran) of 1835 case #1 (hnormSgn env ran) of
1760 L'.SgnError => (strerror, sgnerror, []) 1836 L'.SgnError => (strerror, sgnerror, [])
1761 | L'.SgnConst sgis => 1837 | L'.SgnConst sgis =>
1762 ((L'.StrApp (str1', str2'), loc), 1838 ((L'.StrApp (str1', str2'), loc),
1763 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc), 1839 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
1818 else 1894 else
1819 app (fn (loc, env, denv, (c1, c2)) => 1895 app (fn (loc, env, denv, (c1, c2)) =>
1820 case D.prove env denv (c1, c2, loc) of 1896 case D.prove env denv (c1, c2, loc) of
1821 [] => () 1897 [] => ()
1822 | _ => 1898 | _ =>
1823 (ErrorMsg.errorAt loc "Remaining constraint"; 1899 (ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
1824 eprefaces' [("Con 1", p_con env c1), 1900 eprefaces' [("Con 1", p_con env c1),
1825 ("Con 2", p_con env c2)])) gs; 1901 ("Con 2", p_con env c2)])) gs;
1826 1902
1827 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file 1903 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
1828 end 1904 end