Mercurial > urweb

comparison src/elaborate.sml @ 632:6c4643880df5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Demos compile again, with manual folders
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 15:12:13 -0500
parents e68de2a5506b
children 03ab853c8e4b
comparison
equal deleted inserted replaced
631:effa7d43aac3 632:6c4643880df5
837 end 837 end
838 | _ => raise ex 838 | _ => raise ex
839 in 839 in
840 unfold (r, c) 840 unfold (r, c)
841 end 841 end
842 handle _ => (TextIO.print "Guess failure!\n"; raise ex) 842 handle _ => raise ex
843 in 843 in
844 case (#1 c1, #1 c2) of 844 case (#1 c1, #1 c2) of
845 (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) => 845 (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) =>
846 unfold (dom, ran, f, r, c2) 846 unfold (dom, ran, f, r, c2)
847 | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) => 847 | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) =>
872 in 872 in
873 (*eprefaces "unifyCons''" [("c1All", p_con env c1All), 873 (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
874 ("c2All", p_con env c2All)];*) 874 ("c2All", p_con env c2All)];*)
875 875
876 case (c1, c2) of 876 case (c1, c2) of
877 (L'.CUnit, L'.CUnit) => () 877 (L'.CError, _) => ()
878 | (_, L'.CError) => ()
879
880 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
881 if r1 = r2 then
882 ()
883 else
884 (unifyKinds env k1 k2;
885 r1 := SOME c2All)
886
887 | (L'.CUnif (_, _, _, r), _) =>
888 if occursCon r c2All then
889 err COccursCheckFailed
890 else
891 r := SOME c2All
892 | (_, L'.CUnif (_, _, _, r)) =>
893 if occursCon r c1All then
894 err COccursCheckFailed
895 else
896 r := SOME c1All
897
898 | (L'.CUnit, L'.CUnit) => ()
878 899
879 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => 900 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
880 (unifyCons' env d1 d2; 901 (unifyCons' env d1 d2;
881 unifyCons' env r1 r2) 902 unifyCons' env r1 r2)
882 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => 903 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
931 952
932 | (L'.CTuple cs1, L'.CTuple cs2) => 953 | (L'.CTuple cs1, L'.CTuple cs2) =>
933 ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2)) 954 ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2))
934 handle ListPair.UnequalLengths => err CIncompatible) 955 handle ListPair.UnequalLengths => err CIncompatible)
935 956
936 | (L'.CProj ((L'.CUnif (_, _, _, ref (SOME c1)), loc), n1), _) => 957 | (L'.CProj (c1, n1), _) =>
937 unifyCons' env (L'.CProj (c1, n1), loc) c2All
938 | (_, L'.CProj ((L'.CUnif (_, _, _, ref (SOME c2)), loc), n2)) =>
939 unifyCons' env c1All (L'.CProj (c2, n2), loc)
940 | (L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n), _) =>
941 let 958 let
942 val us = map (fn k => cunif (loc, k)) ks 959 fun trySnd () =
960 case #1 (hnormCon env c2All) of
961 L'.CProj (c2, n2) =>
962 let
963 fun tryNormal () =
964 if n1 = n2 then
965 unifyCons' env c1 c2
966 else
967 err CIncompatible
968 in
969 case #1 (hnormCon env c2) of
970 L'.CUnif (_, k, _, r) =>
971 (case #1 (hnormKind k) of
972 L'.KTuple ks =>
973 let
974 val loc = #2 c2
975 val us = map (fn k => cunif (loc, k)) ks
976 in
977 r := SOME (L'.CTuple us, loc);
978 unifyCons' env c1All (List.nth (us, n2 - 1))
979 end
980 | _ => tryNormal ())
981 | _ => tryNormal ()
982 end
983 | _ => err CIncompatible
943 in 984 in
944 r := SOME (L'.CTuple us, loc); 985 case #1 (hnormCon env c1) of
945 unifyCons' env (List.nth (us, n - 1)) c2All 986 L'.CUnif (_, k, _, r) =>
987 (case #1 (hnormKind k) of
988 L'.KTuple ks =>
989 let
990 val loc = #2 c1
991 val us = map (fn k => cunif (loc, k)) ks
992 in
993 r := SOME (L'.CTuple us, loc);
994 unifyCons' env (List.nth (us, n1 - 1)) c2All
995 end
996 | _ => trySnd ())
997 | _ => trySnd ()
946 end 998 end
947 | (_, L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n)) => 999
948 let 1000 | (_, L'.CProj (c2, n2)) =>
949 val us = map (fn k => cunif (loc, k)) ks 1001 (case #1 (hnormCon env c2) of
950 in 1002 L'.CUnif (_, k, _, r) =>
951 r := SOME (L'.CTuple us, loc); 1003 (case #1 (hnormKind k) of
952 unifyCons' env c1All (List.nth (us, n - 1)) 1004 L'.KTuple ks =>
953 end 1005 let
954 | (L'.CProj (c1, n1), L'.CProj (c2, n2)) => 1006 val loc = #2 c2
955 if n1 = n2 then 1007 val us = map (fn k => cunif (loc, k)) ks
956 unifyCons' env c1 c2 1008 in
957 else 1009 r := SOME (L'.CTuple us, loc);
958 err CIncompatible 1010 unifyCons' env c1All (List.nth (us, n2 - 1))
1011 end
1012 | _ => err CIncompatible)
1013 | _ => err CIncompatible)
959 1014
960 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => 1015 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
961 (unifyKinds env dom1 dom2; 1016 (unifyKinds env dom1 dom2;
962 unifyKinds env ran1 ran2) 1017 unifyKinds env ran1 ran2)
963 1018
967 (unifyKinds env k1 k2; 1022 (unifyKinds env k1 k2;
968 unifyCons' env c1 c2) 1023 unifyCons' env c1 c2)
969 | (L'.TKFun (x, c1), L'.TKFun (_, c2)) => 1024 | (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
970 unifyCons' (E.pushKRel env x) c1 c2 1025 unifyCons' (E.pushKRel env x) c1 c2
971 1026
972 | (L'.CError, _) => ()
973 | (_, L'.CError) => ()
974
975 | (L'.CRecord _, _) => isRecord () 1027 | (L'.CRecord _, _) => isRecord ()
976 | (_, L'.CRecord _) => isRecord () 1028 | (_, L'.CRecord _) => isRecord ()
977 | (L'.CConcat _, _) => isRecord () 1029 | (L'.CConcat _, _) => isRecord ()
978 | (_, L'.CConcat _) => isRecord () 1030 | (_, L'.CConcat _) => isRecord ()
979
980 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
981 if r1 = r2 then
982 ()
983 else
984 (unifyKinds env k1 k2;
985 r1 := SOME c2All)
986
987 | (L'.CUnif (_, _, _, r), _) =>
988 if occursCon r c2All then
989 err COccursCheckFailed
990 else
991 r := SOME c2All
992 | (_, L'.CUnif (_, _, _, r)) =>
993 if occursCon r c1All then
994 err COccursCheckFailed
995 else
996 r := SOME c1All
997 1031
998 | _ => err CIncompatible 1032 | _ => err CIncompatible
999 end 1033 end
1000 1034
1001 and unifyCons env c1 c2 = 1035 and unifyCons env c1 c2 =