Mercurial > urweb

comparison src/elaborate.sml @ 705:e6706a1df013

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Track uniqueness sets in table types
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 14:11:32 -0400
parents 70cbdcf5989b
children 1fb318c17546
comparison
equal deleted inserted replaced
704:70cbdcf5989b 705:e6706a1df013
878 878
879 case (c1, c2) of 879 case (c1, c2) of
880 (L'.CError, _) => () 880 (L'.CError, _) => ()
881 | (_, L'.CError) => () 881 | (_, L'.CError) => ()
882 882
883 | (L'.CRecord _, _) => isRecord ()
884 | (_, L'.CRecord _) => isRecord ()
885 | (L'.CConcat _, _) => isRecord ()
886 | (_, L'.CConcat _) => isRecord ()
887
888 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
889 if r1 = r2 then
890 ()
891 else
892 (unifyKinds env k1 k2;
893 r1 := SOME c2All)
894
895 | (L'.CUnif (_, _, _, r), _) =>
896 if occursCon r c2All then
897 err COccursCheckFailed
898 else
899 r := SOME c2All
900 | (_, L'.CUnif (_, _, _, r)) =>
901 if occursCon r c1All then
902 err COccursCheckFailed
903 else
904 r := SOME c1All
905
906 | (L'.CUnit, L'.CUnit) => ()
907
908 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
909 (unifyCons' env d1 d2;
910 unifyCons' env r1 r2)
911 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
912 if expl1 <> expl2 then
913 err CExplicitness
914 else
915 (unifyKinds env d1 d2;
916 let
917 (*val befor = Time.now ()*)
918 val env' = E.pushCRel env x1 d1
919 in
920 (*TextIO.print ("E.pushCRel: "
921 ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))
922 ^ "\n");*)
923 unifyCons' env' r1 r2
924 end)
925 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2
926 | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) =>
927 (unifyCons' env c1 c2;
928 unifyCons' env d1 d2;
929 unifyCons' env e1 e2)
930
931 | (L'.CRel n1, L'.CRel n2) =>
932 if n1 = n2 then
933 ()
934 else
935 err CIncompatible
936 | (L'.CNamed n1, L'.CNamed n2) =>
937 if n1 = n2 then
938 ()
939 else
940 err CIncompatible
941
942 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
943 (unifyCons' env d1 d2;
944 unifyCons' env r1 r2)
945 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
946 (unifyKinds env k1 k2;
947 unifyCons' (E.pushCRel env x1 k1) c1 c2)
948
949 | (L'.CName n1, L'.CName n2) =>
950 if n1 = n2 then
951 ()
952 else
953 err CIncompatible
954
955 | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
956 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
957 ()
958 else
959 err CIncompatible
960
961 | (L'.CTuple cs1, L'.CTuple cs2) =>
962 ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2))
963 handle ListPair.UnequalLengths => err CIncompatible)
964
965 | (L'.CProj (c1, n1), _) => 883 | (L'.CProj (c1, n1), _) =>
966 let 884 let
967 fun trySnd () = 885 fun trySnd () =
968 case #1 (hnormCon env c2All) of 886 case #1 (hnormCon env c2All) of
969 L'.CProj (c2, n2) => 887 L'.CProj (c2, n2) =>
1017 r := SOME (L'.CTuple us, loc); 935 r := SOME (L'.CTuple us, loc);
1018 unifyCons' env c1All (List.nth (us, n2 - 1)) 936 unifyCons' env c1All (List.nth (us, n2 - 1))
1019 end 937 end
1020 | _ => err CIncompatible) 938 | _ => err CIncompatible)
1021 | _ => err CIncompatible) 939 | _ => err CIncompatible)
940
941 | (L'.CRecord _, _) => isRecord ()
942 | (_, L'.CRecord _) => isRecord ()
943 | (L'.CConcat _, _) => isRecord ()
944 | (_, L'.CConcat _) => isRecord ()
945
946 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
947 if r1 = r2 then
948 ()
949 else
950 (unifyKinds env k1 k2;
951 r1 := SOME c2All)
952
953 | (L'.CUnif (_, _, _, r), _) =>
954 if occursCon r c2All then
955 err COccursCheckFailed
956 else
957 r := SOME c2All
958 | (_, L'.CUnif (_, _, _, r)) =>
959 if occursCon r c1All then
960 err COccursCheckFailed
961 else
962 r := SOME c1All
963
964 | (L'.CUnit, L'.CUnit) => ()
965
966 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
967 (unifyCons' env d1 d2;
968 unifyCons' env r1 r2)
969 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
970 if expl1 <> expl2 then
971 err CExplicitness
972 else
973 (unifyKinds env d1 d2;
974 let
975 (*val befor = Time.now ()*)
976 val env' = E.pushCRel env x1 d1
977 in
978 (*TextIO.print ("E.pushCRel: "
979 ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))
980 ^ "\n");*)
981 unifyCons' env' r1 r2
982 end)
983 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2
984 | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) =>
985 (unifyCons' env c1 c2;
986 unifyCons' env d1 d2;
987 unifyCons' env e1 e2)
988
989 | (L'.CRel n1, L'.CRel n2) =>
990 if n1 = n2 then
991 ()
992 else
993 err CIncompatible
994 | (L'.CNamed n1, L'.CNamed n2) =>
995 if n1 = n2 then
996 ()
997 else
998 err CIncompatible
999
1000 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
1001 (unifyCons' env d1 d2;
1002 unifyCons' env r1 r2)
1003 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
1004 (unifyKinds env k1 k2;
1005 unifyCons' (E.pushCRel env x1 k1) c1 c2)
1006
1007 | (L'.CName n1, L'.CName n2) =>
1008 if n1 = n2 then
1009 ()
1010 else
1011 err CIncompatible
1012
1013 | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
1014 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
1015 ()
1016 else
1017 err CIncompatible
1018
1019 | (L'.CTuple cs1, L'.CTuple cs2) =>
1020 ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2))
1021 handle ListPair.UnequalLengths => err CIncompatible)
1022 1022
1023 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => 1023 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
1024 (unifyKinds env dom1 dom2; 1024 (unifyKinds env dom1 dom2;
1025 unifyKinds env ran1 ran2) 1025 unifyKinds env ran1 ran2)
1026 1026
2317 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] 2317 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
2318 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] 2318 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
2319 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] 2319 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
2320 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] 2320 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
2321 | L'.DExport _ => [] 2321 | L'.DExport _ => []
2322 | L'.DTable (tn, x, n, c, _) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)] 2322 | L'.DTable (tn, x, n, c, _, cc) =>
2323 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), cc), loc)), loc)]
2323 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] 2324 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
2324 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] 2325 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
2325 | L'.DDatabase _ => [] 2326 | L'.DDatabase _ => []
2326 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] 2327 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
2327 2328
3266 end 3267 end
3267 3268
3268 | L.DTable (x, c, e) => 3269 | L.DTable (x, c, e) =>
3269 let 3270 let
3270 val (c', k, gs') = elabCon (env, denv) c 3271 val (c', k, gs') = elabCon (env, denv) c
3271 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) 3272 val uniques = cunif (loc, (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc))
3273
3274 val ct = tableOf ()
3275 val ct = (L'.CApp (ct, c'), loc)
3276 val ct = (L'.CApp (ct, uniques), loc)
3277
3278 val (env, n) = E.pushENamed env x ct
3272 val (e', et, gs'') = elabExp (env, denv) e 3279 val (e', et, gs'') = elabExp (env, denv) e
3273 3280
3274 val names = cunif (loc, (L'.KRecord (L'.KUnit, loc), loc))
3275 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) 3281 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
3276 val cst = (L'.CApp (cst, names), loc)
3277 val cst = (L'.CApp (cst, c'), loc) 3282 val cst = (L'.CApp (cst, c'), loc)
3283 val cst = (L'.CApp (cst, uniques), loc)
3278 in 3284 in
3279 checkKind env c' k (L'.KRecord (L'.KType, loc), loc); 3285 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
3280 checkCon env e' et cst; 3286 checkCon env e' et cst;
3281 ([(L'.DTable (!basis_r, x, n, c', e'), loc)], (env, denv, gs'' @ enD gs' @ gs)) 3287 ([(L'.DTable (!basis_r, x, n, c', e', uniques), loc)], (env, denv, gs'' @ enD gs' @ gs))
3282 end 3288 end
3283 | L.DSequence x => 3289 | L.DSequence x =>
3284 let 3290 let
3285 val (env, n) = E.pushENamed env x (sequenceOf ()) 3291 val (env, n) = E.pushENamed env x (sequenceOf ())
3286 in 3292 in