Mercurial > urweb

comparison src/elaborate.sml @ 621:8998114760c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
"Hello world" compiles, after replacing type-level fold with map
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 15:33:20 -0500
parents 7c3c21eb5b4c
children d64533157f40
comparison
equal deleted inserted replaced
620:d828b143e147 621:8998114760c1
180 | L.KRecord k => (L'.KRecord (elabKind k), loc) 180 | L.KRecord k => (L'.KRecord (elabKind k), loc)
181 | L.KUnit => (L'.KUnit, loc) 181 | L.KUnit => (L'.KUnit, loc)
182 | L.KTuple ks => (L'.KTuple (map elabKind ks), loc) 182 | L.KTuple ks => (L'.KTuple (map elabKind ks), loc)
183 | L.KWild => kunif loc 183 | L.KWild => kunif loc
184 184
185 fun foldKind (dom, ran, loc)= 185 fun mapKind (dom, ran, loc)=
186 (L'.KArrow ((L'.KArrow ((L'.KName, loc), 186 (L'.KArrow ((L'.KArrow (dom, ran), loc),
187 (L'.KArrow (dom, 187 (L'.KArrow ((L'.KRecord dom, loc),
188 (L'.KArrow (ran, ran), loc)), loc)), loc), 188 (L'.KRecord ran, loc)), loc)), loc)
189 (L'.KArrow (ran,
190 (L'.KArrow ((L'.KRecord dom, loc),
191 ran), loc)), loc)), loc)
192 189
193 fun hnormKind (kAll as (k, _)) = 190 fun hnormKind (kAll as (k, _)) =
194 case k of 191 case k of
195 L'.KUnif (_, _, ref (SOME k)) => hnormKind k 192 L'.KUnif (_, _, ref (SOME k)) => hnormKind k
196 | _ => kAll 193 | _ => kAll
353 checkKind env c1' k1 k; 350 checkKind env c1' k1 k;
354 checkKind env c2' k2 k; 351 checkKind env c2' k2 k;
355 ((L'.CConcat (c1', c2'), loc), k, 352 ((L'.CConcat (c1', c2'), loc), k,
356 D.prove env denv (c1', c2', loc) @ gs1 @ gs2) 353 D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
357 end 354 end
358 | L.CFold => 355 | L.CMap =>
359 let 356 let
360 val dom = kunif loc 357 val dom = kunif loc
361 val ran = kunif loc 358 val ran = kunif loc
362 in 359 in
363 ((L'.CFold (dom, ran), loc), 360 ((L'.CMap (dom, ran), loc),
364 foldKind (dom, ran, loc), 361 mapKind (dom, ran, loc),
365 []) 362 [])
366 end 363 end
367 364
368 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), []) 365 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), [])
369 366
487 484
488 | L'.CName _ => kname 485 | L'.CName _ => kname
489 486
490 | L'.CRecord (k, _) => (L'.KRecord k, loc) 487 | L'.CRecord (k, _) => (L'.KRecord k, loc)
491 | L'.CConcat (c, _) => kindof env c 488 | L'.CConcat (c, _) => kindof env c
492 | L'.CFold (dom, ran) => foldKind (dom, ran, loc) 489 | L'.CMap (dom, ran) => mapKind (dom, ran, loc)
493 490
494 | L'.CUnit => (L'.KUnit, loc) 491 | L'.CUnit => (L'.KUnit, loc)
495 492
496 | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc) 493 | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc)
497 | L'.CProj (c, n) => 494 | L'.CProj (c, n) =>
502 | L'.CError => kerror 499 | L'.CError => kerror
503 | L'.CUnif (_, k, _, _) => k 500 | L'.CUnif (_, k, _, _) => k
504 501
505 val hnormCon = D.hnormCon 502 val hnormCon = D.hnormCon
506 503
507 datatype con_summary = 504 fun deConstraintCon (env, denv) c =
508 Nil
509 | Cons
510 | Unknown
511
512 fun compatible cs =
513 case cs of
514 (Unknown, _) => false
515 | (_, Unknown) => false
516 | (s1, s2) => s1 = s2
517
518 fun summarizeCon (env, denv) c =
519 let 505 let
520 val (c, gs) = hnormCon (env, denv) c 506 val (c, gs) = hnormCon (env, denv) c
521 in 507 in
522 case #1 c of 508 case #1 c of
523 L'.CRecord (_, []) => (Nil, gs) 509 L'.CDisjoint (_, _, _, c) =>
524 | L'.CRecord (_, _ :: _) => (Cons, gs)
525 | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
526 | L'.CDisjoint (_, _, _, c) =>
527 let 510 let
528 val (s, gs') = summarizeCon (env, denv) c 511 val (c', gs') = deConstraintCon (env, denv) c
529 in 512 in
530 (s, gs @ gs') 513 (c', gs @ gs')
531 end 514 end
532 | _ => (Unknown, gs) 515 | _ => (c, gs)
533 end 516 end
534 517
535 fun p_con_summary s = 518 exception GuessFailure
536 Print.PD.string (case s of
537 Nil => "Nil"
538 | Cons => "Cons"
539 | Unknown => "Unknown")
540
541 exception SummaryFailure
542 519
543 fun isUnitCon env (c, loc) = 520 fun isUnitCon env (c, loc) =
544 case c of 521 case c of
545 L'.TFun _ => false 522 L'.TFun _ => false
546 | L'.TCFun _ => false 523 | L'.TCFun _ => false
572 549
573 | L'.CName _ => false 550 | L'.CName _ => false
574 551
575 | L'.CRecord _ => false 552 | L'.CRecord _ => false
576 | L'.CConcat _ => false 553 | L'.CConcat _ => false
577 | L'.CFold _ => false 554 | L'.CMap _ => false
578 555
579 | L'.CUnit => true 556 | L'.CUnit => true
580 557
581 | L'.CTuple _ => false 558 | L'.CTuple _ => false
582 | L'.CProj (c, n) => false 559 | L'.CProj (c, n) => false
718 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 695 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
719 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 696 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
720 697
721 fun isGuessable (other, fs) = 698 fun isGuessable (other, fs) =
722 let 699 let
723 val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure) 700 val gs = guessMap (env, denv) (other, (L'.CRecord (k, fs), loc), [], GuessFailure)
724 in 701 in
725 List.all (fn (loc, env, denv, c1, c2) => 702 List.all (fn (loc, env, denv, c1, c2) =>
726 case D.prove env denv (c1, c2, loc) of 703 case D.prove env denv (c1, c2, loc) of
727 [] => true 704 [] => true
728 | _ => false) gs 705 | _ => false) gs
729 end 706 end
730 handle SummaryFailure => false 707 handle GuessFailure => false
731 708
732 val (fs1, fs2, others1, others2) = 709 val (fs1, fs2, others1, others2) =
733 case (fs1, fs2, others1, others2) of 710 case (fs1, fs2, others1, others2) of
734 ([], _, [other1], []) => 711 ([], _, [other1], []) =>
735 if isGuessable (other1, fs2) then 712 if isGuessable (other1, fs2) then
781 pairOffUnifs (unifs1, unifs2) 758 pairOffUnifs (unifs1, unifs2)
782 (*before eprefaces "Summaries'" [("#1", p_summary env s1), 759 (*before eprefaces "Summaries'" [("#1", p_summary env s1),
783 ("#2", p_summary env s2)]*) 760 ("#2", p_summary env s2)]*)
784 end 761 end
785 762
786 and guessFold (env, denv) (c1, c2, gs, ex) = 763 and guessMap (env, denv) (c1, c2, gs, ex) =
787 let 764 let
788 val loc = #2 c1 765 val loc = #2 c1
789 766
790 fun unfold (dom, ran, f, i, r, c) = 767 fun unfold (dom, ran, f, r, c) =
791 let 768 let
792 val nm = cunif (loc, (L'.KName, loc)) 769 fun unfold (r, c) =
793 val v = 770 let
794 case dom of 771 val (c', gs1) = deConstraintCon (env, denv) c
795 (L'.KUnit, _) => (L'.CUnit, loc) 772 in
796 | _ => cunif (loc, dom) 773 case #1 c' of
797 val rest = cunif (loc, (L'.KRecord dom, loc)) 774 L'.CRecord (_, []) =>
798 val acc = (L'.CFold (dom, ran), loc) 775 let
799 val acc = (L'.CApp (acc, f), loc) 776 val gs2 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
800 val acc = (L'.CApp (acc, i), loc) 777 in
801 val acc = (L'.CApp (acc, rest), loc) 778 gs1 @ gs2
802 779 end
803 val (iS, gs3) = summarizeCon (env, denv) i 780 | L'.CRecord (_, [(x, v)]) =>
804 781 let
805 val app = (L'.CApp (f, nm), loc) 782 val v' = case dom of
806 val app = (L'.CApp (app, v), loc) 783 (L'.KUnit, _) => (L'.CUnit, loc)
807 val app = (L'.CApp (app, acc), loc) 784 | _ => cunif (loc, dom)
808 val (appS, gs4) = summarizeCon (env, denv) app 785 val gs2 = unifyCons (env, denv) v' (L'.CApp (f, v), loc)
809 786
810 val (cS, gs5) = summarizeCon (env, denv) c 787 val gs3 = unifyCons (env, denv) r (L'.CRecord (dom, [(x, v')]), loc)
788 in
789 gs1 @ gs2 @ gs3
790 end
791 | L'.CRecord (_, (x, v) :: rest) =>
792 let
793 val r1 = 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)
796
797 val gs3 = unfold (r1, (L'.CRecord (ran, [(x, v)]), loc))
798 val gs4 = unfold (r2, (L'.CRecord (ran, rest), loc))
799 in
800 gs1 @ gs2 @ gs3 @ gs4
801 end
802 | L'.CConcat (c1', c2') =>
803 let
804 val r1 = 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)
807
808 val gs3 = unfold (r1, c1')
809 val gs4 = unfold (r2, c2')
810 in
811 gs1 @ gs2 @ gs3 @ gs4
812 end
813 | _ => raise ex
814 end
811 in 815 in
812 (*prefaces "Summaries" [("iS", p_con_summary iS), 816 unfold (r, c)
813 ("appS", p_con_summary appS),
814 ("cS", p_con_summary cS)];*)
815
816 if compatible (iS, appS) then
817 raise ex
818 else if compatible (cS, iS) then
819 let
820 (*val () = prefaces "Same?" [("i", p_con env i),
821 ("c", p_con env c)]*)
822 val gs6 = unifyCons (env, denv) i c
823 (*val () = TextIO.print "Yes!\n"*)
824
825 val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
826 in
827 gs @ gs3 @ gs5 @ gs6 @ gs7
828 end
829 else if compatible (cS, appS) then
830 let
831 (*val () = prefaces "Same?" [("app", p_con env app),
832 ("c", p_con env c),
833 ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
834 val gs6 = unifyCons (env, denv) app c
835 (*val () = TextIO.print "Yes!\n"*)
836
837 val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
838 val concat = (L'.CConcat (singleton, rest), loc)
839 (*val () = prefaces "Pre-crew" [("r", p_con env r),
840 ("concat", p_con env concat)]*)
841 val gs7 = unifyCons (env, denv) r concat
842 in
843 (*prefaces "The crew" [("nm", p_con env nm),
844 ("v", p_con env v),
845 ("rest", p_con env rest)];*)
846
847 gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
848 end
849 else
850 raise ex
851 end 817 end
852 handle _ => raise ex 818 handle _ => raise ex
853 in 819 in
854 case (#1 c1, #1 c2) of 820 case (#1 c1, #1 c2) of
855 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) => 821 (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) =>
856 unfold (dom, ran, f, i, r, c2) 822 unfold (dom, ran, f, r, c2)
857 | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) => 823 | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) =>
858 unfold (dom, ran, f, i, r, c1) 824 unfold (dom, ran, f, r, c1)
859 | _ => raise ex 825 | _ => raise ex
860 end 826 end
861 827
862 and unifyCons' (env, denv) c1 c2 = 828 and unifyCons' (env, denv) c1 c2 =
863 case (#1 c1, #1 c2) of 829 case (#1 c1, #1 c2) of
888 ("c2", p_con env old2), 854 ("c2", p_con env old2),
889 ("t", PD.string (LargeReal.toString (Time.toReal 855 ("t", PD.string (LargeReal.toString (Time.toReal
890 (Time.- (Time.now (), befor)))))];*) 856 (Time.- (Time.now (), befor)))))];*)
891 gs1 @ gs2 @ gs3 857 gs1 @ gs2 @ gs3
892 end 858 end
893 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex) 859 handle ex => guessMap (env, denv) (c1, c2, gs1 @ gs2, ex)
894 end 860 end
895 861
896 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = 862 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
897 let 863 let
898 fun err f = raise CUnify' (f (c1All, c2All)) 864 fun err f = raise CUnify' (f (c1All, c2All))
1015 err COccursCheckFailed 981 err COccursCheckFailed
1016 else 982 else
1017 (r := SOME c1All; 983 (r := SOME c1All;
1018 []) 984 [])
1019 985
1020 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) => 986 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
1021 (unifyKinds dom1 dom2; 987 (unifyKinds dom1 dom2;
1022 unifyKinds ran1 ran2; 988 unifyKinds ran1 ran2;
1023 []) 989 [])
1024 990
1025 | _ => err CIncompatible 991 | _ => err CIncompatible
2738 2704
2739 | CName _ => true 2705 | CName _ => true
2740 2706
2741 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs 2707 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs
2742 | CConcat (c1, c2) => none c1 andalso none c2 2708 | CConcat (c1, c2) => none c1 andalso none c2
2743 | CFold => true 2709 | CMap => true
2744 2710
2745 | CUnit => true 2711 | CUnit => true
2746 2712
2747 | CTuple cs => List.all none cs 2713 | CTuple cs => List.all none cs
2748 | CProj (c, _) => none c 2714 | CProj (c, _) => none c
2764 2730
2765 | CName _ => true 2731 | CName _ => true
2766 2732
2767 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs 2733 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs
2768 | CConcat (c1, c2) => pos c1 andalso pos c2 2734 | CConcat (c1, c2) => pos c1 andalso pos c2
2769 | CFold => true 2735 | CMap => true
2770 2736
2771 | CUnit => true 2737 | CUnit => true
2772 2738
2773 | CTuple cs => List.all pos cs 2739 | CTuple cs => List.all pos cs
2774 | CProj (c, _) => pos c 2740 | CProj (c, _) => pos c