Mercurial > urweb

comparison src/elaborate.sml @ 191:aa54250f58ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parametrized datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 10:28:32 -0400
parents 8e9f97508f0d
children df5fd8f6913a
comparison
equal deleted inserted replaced
190:3eb53c957d10 191:aa54250f58ac
931 val perror = (L'.PWild, loc) 931 val perror = (L'.PWild, loc)
932 val terror = (L'.CError, loc) 932 val terror = (L'.CError, loc)
933 val pterror = (perror, terror) 933 val pterror = (perror, terror)
934 val rerror = (pterror, (env, bound)) 934 val rerror = (pterror, (env, bound))
935 935
936 fun pcon (pc, po, to, dn, dk) = 936 fun pcon (pc, po, xs, to, dn, dk) =
937 case (po, to) of 937 case (po, to) of
938 (NONE, SOME _) => (expError env (PatHasNoArg loc); 938 (NONE, SOME _) => (expError env (PatHasNoArg loc);
939 rerror) 939 rerror)
940 | (SOME _, NONE) => (expError env (PatHasArg loc); 940 | (SOME _, NONE) => (expError env (PatHasArg loc);
941 rerror) 941 rerror)
942 | (NONE, NONE) => (((L'.PCon (dk, pc, NONE), loc), dn), 942 | (NONE, NONE) =>
943 (env, bound)) 943 let
944 val k = (L'.KType, loc)
945 val unifs = map (fn _ => cunif (loc, k)) xs
946 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
947 in
948 (((L'.PCon (dk, pc, unifs, NONE), loc), dn),
949 (env, bound))
950 end
944 | (SOME p, SOME t) => 951 | (SOME p, SOME t) =>
945 let 952 let
946 val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound)) 953 val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound))
954
955 val k = (L'.KType, loc)
956 val unifs = map (fn _ => cunif (loc, k)) xs
957 val t = ListUtil.foldli (fn (i, u, t) => subConInCon (i, u) t) t unifs
958 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
947 in 959 in
948 (((L'.PCon (dk, pc, SOME p'), loc), dn), 960 ignore (checkPatCon (env, denv) p' pt t);
961 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn),
949 (env, bound)) 962 (env, bound))
950 end 963 end
951 in 964 in
952 case p of 965 case p of
953 L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))), 966 L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))),
967 (env, bound)) 980 (env, bound))
968 | L.PCon ([], x, po) => 981 | L.PCon ([], x, po) =>
969 (case E.lookupConstructor env x of 982 (case E.lookupConstructor env x of
970 NONE => (expError env (UnboundConstructor (loc, [], x)); 983 NONE => (expError env (UnboundConstructor (loc, [], x));
971 rerror) 984 rerror)
972 | SOME (dk, n, to, dn) => pcon (L'.PConVar n, po, to, (L'.CNamed dn, loc), dk)) 985 | SOME (dk, n, xs, to, dn) => pcon (L'.PConVar n, po, xs, to, (L'.CNamed dn, loc), dk))
973 | L.PCon (m1 :: ms, x, po) => 986 | L.PCon (m1 :: ms, x, po) =>
974 (case E.lookupStr env m1 of 987 (case E.lookupStr env m1 of
975 NONE => (expError env (UnboundStrInExp (loc, m1)); 988 NONE => (expError env (UnboundStrInExp (loc, m1));
976 rerror) 989 rerror)
977 | SOME (n, sgn) => 990 | SOME (n, sgn) =>
983 ((L'.StrVar n, loc), sgn) ms 996 ((L'.StrVar n, loc), sgn) ms
984 in 997 in
985 case E.projectConstructor env {str = str, sgn = sgn, field = x} of 998 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
986 NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x)); 999 NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x));
987 rerror) 1000 rerror)
988 | SOME (dk, _, to, dn) => pcon (L'.PConProj (n, ms, x), po, to, dn, dk) 1001 | SOME (dk, _, xs, to, dn) => pcon (L'.PConProj (n, ms, x), po, xs, to, dn, dk)
989 end) 1002 end)
990 1003
991 | L.PRecord (xps, flex) => 1004 | L.PRecord (xps, flex) =>
992 let 1005 let
993 val (xpts, (env, bound, _)) = 1006 val (xpts, (env, bound, _)) =
1033 let 1046 let
1034 val (str, sgn) = E.chaseMpath env (m1, ms) 1047 val (str, sgn) = E.chaseMpath env (m1, ms)
1035 in 1048 in
1036 case E.projectConstructor env {str = str, sgn = sgn, field = x} of 1049 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
1037 NONE => raise Fail "exhaustive: Can't project constructor" 1050 NONE => raise Fail "exhaustive: Can't project constructor"
1038 | SOME (_, n, _, _) => n 1051 | SOME (_, n, _, _, _) => n
1039 end 1052 end
1040 1053
1041 fun coverage (p, _) = 1054 fun coverage (p, _) =
1042 case p of 1055 case p of
1043 L'.PWild => Wild 1056 L'.PWild => Wild
1044 | L'.PVar _ => Wild 1057 | L'.PVar _ => Wild
1045 | L'.PPrim _ => None 1058 | L'.PPrim _ => None
1046 | L'.PCon (_, pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild)) 1059 | L'.PCon (_, pc, _, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
1047 | L'.PCon (_, pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p)) 1060 | L'.PCon (_, pc, _, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
1048 | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) => 1061 | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) =>
1049 SM.insert (fmap, x, coverage p)) SM.empty xps] 1062 SM.insert (fmap, x, coverage p)) SM.empty xps]
1050 1063
1051 fun merge (c1, c2) = 1064 fun merge (c1, c2) =
1052 case (c1, c2) of 1065 case (c1, c2) of
1156 val (total, gs') = isTotal (c', t') 1169 val (total, gs') = isTotal (c', t')
1157 in 1170 in
1158 (total, gs' @ gs) 1171 (total, gs' @ gs)
1159 end) 1172 end)
1160 (true, gs) cons 1173 (true, gs) cons
1174
1175 fun unapp t =
1176 case t of
1177 L'.CApp ((t, _), _) => unapp t
1178 | _ => t
1161 in 1179 in
1162 case t of 1180 case unapp t of
1163 L'.CNamed n => 1181 L'.CNamed n =>
1164 let 1182 let
1165 val dt = E.lookupDatatype env n 1183 val dt = E.lookupDatatype env n
1166 val cons = E.constructors dt 1184 val cons = E.constructors dt
1167 in 1185 in
1171 let 1189 let
1172 val (str, sgn) = E.chaseMpath env (m1, ms) 1190 val (str, sgn) = E.chaseMpath env (m1, ms)
1173 in 1191 in
1174 case E.projectDatatype env {str = str, sgn = sgn, field = x} of 1192 case E.projectDatatype env {str = str, sgn = sgn, field = x} of
1175 NONE => raise Fail "isTotal: Can't project datatype" 1193 NONE => raise Fail "isTotal: Can't project datatype"
1176 | SOME cons => dtype cons 1194 | SOME (_, cons) => dtype cons
1177 end 1195 end
1178 | L'.CError => (true, gs) 1196 | L'.CError => (true, gs)
1179 | _ => raise Fail "isTotal: Not a datatype" 1197 | _ => raise Fail "isTotal: Not a datatype"
1180 end 1198 end
1181 | Record _ => (List.all (fn c2 => coverageImp (c, c2)) (enumerateCases t), []) 1199 | Record _ => (List.all (fn c2 => coverageImp (c, c2)) (enumerateCases t), [])
1204 (case E.lookupE env s of 1222 (case E.lookupE env s of
1205 E.NotBound => 1223 E.NotBound =>
1206 (expError env (UnboundExp (loc, s)); 1224 (expError env (UnboundExp (loc, s));
1207 (eerror, cerror, [])) 1225 (eerror, cerror, []))
1208 | E.Rel (n, t) => ((L'.ERel n, loc), t, []) 1226 | E.Rel (n, t) => ((L'.ERel n, loc), t, [])
1209 | E.Named (n, t) => ((L'.ENamed n, loc), t, [])) 1227 | E.Named (n, t) =>
1228 if Char.isUpper (String.sub (s, 0)) then
1229 elabHead (env, denv) (L'.ENamed n, loc) t
1230 else
1231 ((L'.ENamed n, loc), t, []))
1210 | L.EVar (m1 :: ms, s) => 1232 | L.EVar (m1 :: ms, s) =>
1211 (case E.lookupStr env m1 of 1233 (case E.lookupStr env m1 of
1212 NONE => (expError env (UnboundStrInExp (loc, m1)); 1234 NONE => (expError env (UnboundStrInExp (loc, m1));
1213 (eerror, cerror, [])) 1235 (eerror, cerror, []))
1214 | SOME (n, sgn) => 1236 | SOME (n, sgn) =>
1570 checkKind env c' ck k'; 1592 checkKind env c' ck k';
1571 1593
1572 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) 1594 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
1573 end 1595 end
1574 1596
1575 | L.SgiDatatype (x, xcs) => 1597 | L.SgiDatatype (x, xs, xcs) =>
1576 let 1598 let
1577 val k = (L'.KType, loc) 1599 val k = (L'.KType, loc)
1578 val (env, n) = E.pushCNamed env x k NONE 1600 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
1601 val (env, n) = E.pushCNamed env x k' NONE
1579 val t = (L'.CNamed n, loc) 1602 val t = (L'.CNamed n, loc)
1603 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs
1580 1604
1581 val (xcs, (used, env, gs)) = 1605 val (xcs, (used, env, gs)) =
1582 ListUtil.foldlMap 1606 ListUtil.foldlMap
1583 (fn ((x, to), (used, env, gs)) => 1607 (fn ((x, to), (used, env, gs)) =>
1584 let 1608 let
1589 val (t', tk, gs') = elabCon (env, denv) t' 1613 val (t', tk, gs') = elabCon (env, denv) t'
1590 in 1614 in
1591 checkKind env t' tk k; 1615 checkKind env t' tk k;
1592 (SOME t', (L'.TFun (t', t), loc), gs' @ gs) 1616 (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
1593 end 1617 end
1618 val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
1594 1619
1595 val (env, n') = E.pushENamed env x t 1620 val (env, n') = E.pushENamed env x t
1596 in 1621 in
1597 if SS.member (used, x) then 1622 if SS.member (used, x) then
1598 strError env (DuplicateConstructor (x, loc)) 1623 strError env (DuplicateConstructor (x, loc))
1599 else 1624 else
1600 (); 1625 ();
1601 ((x, n', to), (SS.add (used, x), env, gs')) 1626 ((x, n', to), (SS.add (used, x), env, gs'))
1602 end) 1627 end)
1603 (SS.empty, env, []) xcs 1628 (SS.empty, env, []) xcs
1604 in 1629
1605 ([(L'.SgiDatatype (x, n, xcs), loc)], (env, denv, gs)) 1630 val env = E.pushDatatype env n xs xcs
1631 in
1632 ([(L'.SgiDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
1606 end 1633 end
1607 1634
1608 | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp" 1635 | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp"
1609 1636
1610 | L.SgiDatatypeImp (x, m1 :: ms, s) => 1637 | L.SgiDatatypeImp (x, m1 :: ms, s) =>
1623 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of 1650 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
1624 ((L'.CModProj (n, ms, s), _), gs) => 1651 ((L'.CModProj (n, ms, s), _), gs) =>
1625 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of 1652 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
1626 NONE => (conError env (UnboundDatatype (loc, s)); 1653 NONE => (conError env (UnboundDatatype (loc, s));
1627 ([], (env, denv, gs))) 1654 ([], (env, denv, gs)))
1628 | SOME xncs => 1655 | SOME (xs, xncs) =>
1629 let 1656 let
1630 val k = (L'.KType, loc) 1657 val k = (L'.KType, loc)
1658 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
1659
1631 val t = (L'.CModProj (n, ms, s), loc) 1660 val t = (L'.CModProj (n, ms, s), loc)
1632 val (env, n') = E.pushCNamed env x k (SOME t) 1661 val (env, n') = E.pushCNamed env x k' (SOME t)
1633 val env = E.pushDatatype env n' xncs 1662 val env = E.pushDatatype env n' xs xncs
1634 1663
1635 val t = (L'.CNamed n', loc) 1664 val t = (L'.CNamed n', loc)
1636 val env = foldl (fn ((x, n, to), env) => 1665 val env = foldl (fn ((x, n, to), env) =>
1637 let 1666 let
1638 val t = case to of 1667 val t = case to of
1639 NONE => t 1668 NONE => t
1640 | SOME t' => (L'.TFun (t', t), loc) 1669 | SOME t' => (L'.TFun (t', t), loc)
1670
1671 val t = foldr (fn (x, t) =>
1672 (L'.TCFun (L'.Implicit, x, k, t), loc))
1673 t xs
1641 in 1674 in
1642 E.pushENamedAs env x n t 1675 E.pushENamedAs env x n t
1643 end) env xncs 1676 end) env xncs
1644 in 1677 in
1645 ([(L'.SgiDatatypeImp (x, n', n, ms, s, xncs), loc)], (env, denv, gs)) 1678 ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs))
1646 end) 1679 end)
1647 | _ => (strError env (NotDatatype loc); 1680 | _ => (strError env (NotDatatype loc);
1648 ([], (env, denv, []))) 1681 ([], (env, denv, [])))
1649 end) 1682 end)
1650 1683
1718 (if SS.member (cons, x) then 1751 (if SS.member (cons, x) then
1719 sgnError env (DuplicateCon (loc, x)) 1752 sgnError env (DuplicateCon (loc, x))
1720 else 1753 else
1721 (); 1754 ();
1722 (SS.add (cons, x), vals, sgns, strs)) 1755 (SS.add (cons, x), vals, sgns, strs))
1723 | L'.SgiDatatype (x, _, xncs) => 1756 | L'.SgiDatatype (x, _, _, xncs) =>
1724 let 1757 let
1725 val vals = foldl (fn ((x, _, _), vals) => 1758 val vals = foldl (fn ((x, _, _), vals) =>
1726 (if SS.member (vals, x) then 1759 (if SS.member (vals, x) then
1727 sgnError env (DuplicateVal (loc, x)) 1760 sgnError env (DuplicateVal (loc, x))
1728 else 1761 else
1734 sgnError env (DuplicateCon (loc, x)) 1767 sgnError env (DuplicateCon (loc, x))
1735 else 1768 else
1736 (); 1769 ();
1737 (SS.add (cons, x), vals, sgns, strs) 1770 (SS.add (cons, x), vals, sgns, strs)
1738 end 1771 end
1739 | L'.SgiDatatypeImp (x, _, _, _, _, _) => 1772 | L'.SgiDatatypeImp (x, _, _, _, _, _, _) =>
1740 (if SS.member (cons, x) then 1773 (if SS.member (cons, x) then
1741 sgnError env (DuplicateCon (loc, x)) 1774 sgnError env (DuplicateCon (loc, x))
1742 else 1775 else
1743 (); 1776 ();
1744 (SS.add (cons, x), vals, sgns, strs)) 1777 (SS.add (cons, x), vals, sgns, strs))
1826 | L'.SgnVar _ => sgn 1859 | L'.SgnVar _ => sgn
1827 1860
1828 | L'.SgnConst sgis => 1861 | L'.SgnConst sgis =>
1829 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) => 1862 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
1830 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) 1863 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
1831 | (L'.SgiDatatype (x, n, xncs), loc) => 1864 | (L'.SgiDatatype (x, n, xs, xncs), loc) =>
1832 (L'.SgiDatatypeImp (x, n, str, strs, x, xncs), loc) 1865 (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
1833 | (L'.SgiStr (x, n, sgn), loc) => 1866 | (L'.SgiStr (x, n, sgn), loc) =>
1834 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) 1867 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
1835 | x => x) sgis), #2 sgn) 1868 | x => x) sgis), #2 sgn)
1836 | L'.SgnFun _ => sgn 1869 | L'.SgnFun _ => sgn
1837 | L'.SgnWhere _ => sgn 1870 | L'.SgnWhere _ => sgn
1876 in 1909 in
1877 (L'.DCon (x, n, k, c), loc) 1910 (L'.DCon (x, n, k, c), loc)
1878 end 1911 end
1879 | L'.SgiCon (x, n, k, c) => 1912 | L'.SgiCon (x, n, k, c) =>
1880 (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) 1913 (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
1881 | L'.SgiDatatype (x, n, xncs) => 1914 | L'.SgiDatatype (x, n, xs, xncs) =>
1882 (L'.DDatatypeImp (x, n, str, strs, x, xncs), loc) 1915 (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
1883 | L'.SgiDatatypeImp (x, n, m1, ms, x', xncs) => 1916 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
1884 (L'.DDatatypeImp (x, n, m1, ms, x', xncs), loc) 1917 (L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)
1885 | L'.SgiVal (x, n, t) => 1918 | L'.SgiVal (x, n, t) =>
1886 (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc) 1919 (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)
1887 | L'.SgiStr (x, n, sgn) => 1920 | L'.SgiStr (x, n, sgn) =>
1888 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc) 1921 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)
1889 | L'.SgiSgn (x, n, sgn) => 1922 | L'.SgiSgn (x, n, sgn) =>
1996 NONE 2029 NONE
1997 in 2030 in
1998 case sgi1 of 2031 case sgi1 of
1999 L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE) 2032 L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
2000 | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1) 2033 | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1)
2001 | L'.SgiDatatype (x', n1, _) => found (x', n1, (L'.KType, loc), NONE) 2034 | L'.SgiDatatype (x', n1, xs, _) =>
2002 | L'.SgiDatatypeImp (x', n1, m1, ms, s, _) => 2035 let
2003 found (x', n1, (L'.KType, loc), SOME (L'.CModProj (m1, ms, s), loc)) 2036 val k = (L'.KType, loc)
2037 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2038 in
2039 found (x', n1, k', NONE)
2040 end
2041 | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) =>
2042 let
2043 val k = (L'.KType, loc)
2044 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2045 in
2046 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
2047 end
2004 | _ => NONE 2048 | _ => NONE
2005 end) 2049 end)
2006 2050
2007 | L'.SgiCon (x, n2, k2, c2) => 2051 | L'.SgiCon (x, n2, k2, c2) =>
2008 seek (fn sgi1All as (sgi1, _) => 2052 seek (fn sgi1All as (sgi1, _) =>
2021 end 2065 end
2022 else 2066 else
2023 NONE 2067 NONE
2024 | _ => NONE) 2068 | _ => NONE)
2025 2069
2026 | L'.SgiDatatype (x, n2, xncs2) => 2070 | L'.SgiDatatype (x, n2, xs2, xncs2) =>
2027 seek (fn sgi1All as (sgi1, _) => 2071 seek (fn sgi1All as (sgi1, _) =>
2028 let 2072 let
2029 fun found (n1, xncs1) = 2073 fun found (n1, xs1, xncs1) =
2030 let 2074 let
2031 fun mismatched ue = 2075 fun mismatched ue =
2032 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); 2076 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
2033 SOME (env, denv)) 2077 SOME (env, denv))
2078
2079 val k = (L'.KType, loc)
2080 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1
2034 2081
2035 fun good () = 2082 fun good () =
2036 let 2083 let
2037 val env = E.sgiBinds env sgi2All 2084 val env = E.sgiBinds env sgi2All
2038 val env = if n1 = n2 then 2085 val env = if n1 = n2 then
2042 (SOME (L'.CNamed n1, loc)) 2089 (SOME (L'.CNamed n1, loc))
2043 in 2090 in
2044 SOME (env, denv) 2091 SOME (env, denv)
2045 end 2092 end
2046 2093
2094 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1
2047 fun xncBad ((x1, _, t1), (x2, _, t2)) = 2095 fun xncBad ((x1, _, t1), (x2, _, t2)) =
2048 String.compare (x1, x2) <> EQUAL 2096 String.compare (x1, x2) <> EQUAL
2049 orelse case (t1, t2) of 2097 orelse case (t1, t2) of
2050 (NONE, NONE) => false 2098 (NONE, NONE) => false
2051 | (SOME t1, SOME t2) => 2099 | (SOME t1, SOME t2) =>
2052 not (List.null (unifyCons (env, denv) t1 t2)) 2100 not (List.null (unifyCons (env, denv) t1 t2))
2053 | _ => true 2101 | _ => true
2054 in 2102 in
2055 (if length xncs1 <> length xncs2 2103 (if xs1 <> xs2
2104 orelse length xncs1 <> length xncs2
2056 orelse ListPair.exists xncBad (xncs1, xncs2) then 2105 orelse ListPair.exists xncBad (xncs1, xncs2) then
2057 mismatched NONE 2106 mismatched NONE
2058 else 2107 else
2059 good ()) 2108 good ())
2060 handle CUnify ue => mismatched (SOME ue) 2109 handle CUnify ue => mismatched (SOME ue)
2061 end 2110 end
2062 in 2111 in
2063 case sgi1 of 2112 case sgi1 of
2064 L'.SgiDatatype (x', n1, xncs1) => 2113 L'.SgiDatatype (x', n1, xs, xncs1) =>
2065 if x' = x then 2114 if x' = x then
2066 found (n1, xncs1) 2115 found (n1, xs, xncs1)
2067 else 2116 else
2068 NONE 2117 NONE
2069 | L'.SgiDatatypeImp (x', n1, _, _, _, xncs1) => 2118 | L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) =>
2070 if x' = x then 2119 if x' = x then
2071 found (n1, xncs1) 2120 found (n1, xs, xncs1)
2072 else 2121 else
2073 NONE 2122 NONE
2074 | _ => NONE 2123 | _ => NONE
2075 end) 2124 end)
2076 2125
2077 | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, _) => 2126 | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) =>
2078 seek (fn sgi1All as (sgi1, _) => 2127 seek (fn sgi1All as (sgi1, _) =>
2079 case sgi1 of 2128 case sgi1 of
2080 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _) => 2129 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) =>
2081 if x = x' then 2130 if x = x' then
2082 let 2131 let
2083 val k = (L'.KType, loc) 2132 val k = (L'.KType, loc)
2133 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2084 val t1 = (L'.CModProj (m11, ms1, s1), loc) 2134 val t1 = (L'.CModProj (m11, ms1, s1), loc)
2085 val t2 = (L'.CModProj (m12, ms2, s2), loc) 2135 val t2 = (L'.CModProj (m12, ms2, s2), loc)
2086 2136
2087 fun good () = 2137 fun good () =
2088 let 2138 let
2089 val env = E.pushCNamedAs env x n1 k (SOME t1) 2139 val env = E.pushCNamedAs env x n1 k' (SOME t1)
2090 val env = E.pushCNamedAs env x n2 k (SOME t2) 2140 val env = E.pushCNamedAs env x n2 k' (SOME t2)
2091 in 2141 in
2092 SOME (env, denv) 2142 SOME (env, denv)
2093 end 2143 end
2094 in 2144 in
2095 (case unifyCons (env, denv) t1 t2 of 2145 (case unifyCons (env, denv) t1 t2 of
2211 in 2261 in
2212 checkKind env c' ck k'; 2262 checkKind env c' ck k';
2213 2263
2214 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) 2264 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
2215 end 2265 end
2216 | L.DDatatype (x, xcs) => 2266 | L.DDatatype (x, xs, xcs) =>
2217 let 2267 let
2218 val k = (L'.KType, loc) 2268 val k = (L'.KType, loc)
2219 val (env, n) = E.pushCNamed env x k NONE 2269 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2270 val (env, n) = E.pushCNamed env x k' NONE
2220 val t = (L'.CNamed n, loc) 2271 val t = (L'.CNamed n, loc)
2272 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs
2273
2274 val (env', denv') = foldl (fn (x, (env', denv')) =>
2275 (E.pushCRel env' x k,
2276 D.enter denv')) (env, denv) xs
2221 2277
2222 val (xcs, (used, env, gs)) = 2278 val (xcs, (used, env, gs)) =
2223 ListUtil.foldlMap 2279 ListUtil.foldlMap
2224 (fn ((x, to), (used, env, gs)) => 2280 (fn ((x, to), (used, env, gs)) =>
2225 let 2281 let
2226 val (to, t, gs') = case to of 2282 val (to, t, gs') = case to of
2227 NONE => (NONE, t, gs) 2283 NONE => (NONE, t, gs)
2228 | SOME t' => 2284 | SOME t' =>
2229 let 2285 let
2230 val (t', tk, gs') = elabCon (env, denv) t' 2286 val (t', tk, gs') = elabCon (env', denv') t'
2231 in 2287 in
2232 checkKind env t' tk k; 2288 checkKind env' t' tk k;
2233 (SOME t', (L'.TFun (t', t), loc), gs' @ gs) 2289 (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
2234 end 2290 end
2291 val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
2235 2292
2236 val (env, n') = E.pushENamed env x t 2293 val (env, n') = E.pushENamed env x t
2237 in 2294 in
2238 if SS.member (used, x) then 2295 if SS.member (used, x) then
2239 strError env (DuplicateConstructor (x, loc)) 2296 strError env (DuplicateConstructor (x, loc))
2241 (); 2298 ();
2242 ((x, n', to), (SS.add (used, x), env, gs')) 2299 ((x, n', to), (SS.add (used, x), env, gs'))
2243 end) 2300 end)
2244 (SS.empty, env, []) xcs 2301 (SS.empty, env, []) xcs
2245 2302
2246 val env = E.pushDatatype env n xcs 2303 val env = E.pushDatatype env n xs xcs
2247 in 2304 in
2248 ([(L'.DDatatype (x, n, xcs), loc)], (env, denv, gs)) 2305 ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
2249 end 2306 end
2250 2307
2251 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" 2308 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
2252 2309
2253 | L.DDatatypeImp (x, m1 :: ms, s) => 2310 | L.DDatatypeImp (x, m1 :: ms, s) =>
2266 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of 2323 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
2267 ((L'.CModProj (n, ms, s), _), gs) => 2324 ((L'.CModProj (n, ms, s), _), gs) =>
2268 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of 2325 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
2269 NONE => (conError env (UnboundDatatype (loc, s)); 2326 NONE => (conError env (UnboundDatatype (loc, s));
2270 ([], (env, denv, gs))) 2327 ([], (env, denv, gs)))
2271 | SOME xncs => 2328 | SOME (xs, xncs) =>
2272 let 2329 let
2273 val k = (L'.KType, loc) 2330 val k = (L'.KType, loc)
2331 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2274 val t = (L'.CModProj (n, ms, s), loc) 2332 val t = (L'.CModProj (n, ms, s), loc)
2275 val (env, n') = E.pushCNamed env x k (SOME t) 2333 val (env, n') = E.pushCNamed env x k' (SOME t)
2276 val env = E.pushDatatype env n' xncs 2334 val env = E.pushDatatype env n' xs xncs
2277 2335
2278 val t = (L'.CNamed n', loc) 2336 val t = (L'.CNamed n', loc)
2279 val env = foldl (fn ((x, n, to), env) => 2337 val env = foldl (fn ((x, n, to), env) =>
2280 let 2338 let
2281 val t = case to of 2339 val t = case to of
2282 NONE => t 2340 NONE => t
2283 | SOME t' => (L'.TFun (t', t), loc) 2341 | SOME t' => (L'.TFun (t', t), loc)
2342
2343 val t = foldr (fn (x, t) =>
2344 (L'.TCFun (L'.Implicit, x, k, t), loc))
2345 t xs
2284 in 2346 in
2285 E.pushENamedAs env x n t 2347 E.pushENamedAs env x n t
2286 end) env xncs 2348 end) env xncs
2287 in 2349 in
2288 ([(L'.DDatatypeImp (x, n', n, ms, s, xncs), loc)], (env, denv, gs)) 2350 ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs))
2289 end) 2351 end)
2290 | _ => (strError env (NotDatatype loc); 2352 | _ => (strError env (NotDatatype loc);
2291 ([], (env, denv, []))) 2353 ([], (env, denv, [])))
2292 end) 2354 end)
2293 2355
2542 else 2604 else
2543 (SS.add (cons, x), x) 2605 (SS.add (cons, x), x)
2544 in 2606 in
2545 ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs) 2607 ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
2546 end 2608 end
2547 | L'.SgiDatatype (x, n, xncs) => 2609 | L'.SgiDatatype (x, n, xs, xncs) =>
2548 let 2610 let
2549 val (cons, x) = 2611 val (cons, x) =
2550 if SS.member (cons, x) then 2612 if SS.member (cons, x) then
2551 (cons, "?" ^ x) 2613 (cons, "?" ^ x)
2552 else 2614 else
2559 (("?" ^ x, n, t), vals) 2621 (("?" ^ x, n, t), vals)
2560 else 2622 else
2561 ((x, n, t), SS.add (vals, x))) 2623 ((x, n, t), SS.add (vals, x)))
2562 vals xncs 2624 vals xncs
2563 in 2625 in
2564 ((L'.SgiDatatype (x, n, xncs), loc) :: sgis, cons, vals, sgns, strs) 2626 ((L'.SgiDatatype (x, n, xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
2565 end 2627 end
2566 | L'.SgiDatatypeImp (x, n, m1, ms, x', xncs) => 2628 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
2567 let 2629 let
2568 val (cons, x) = 2630 val (cons, x) =
2569 if SS.member (cons, x) then 2631 if SS.member (cons, x) then
2570 (cons, "?" ^ x) 2632 (cons, "?" ^ x)
2571 else 2633 else
2572 (SS.add (cons, x), x) 2634 (SS.add (cons, x), x)
2573 in 2635 in
2574 ((L'.SgiDatatypeImp (x, n, m1, ms, x', xncs), loc) :: sgis, cons, vals, sgns, strs) 2636 ((L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
2575 end 2637 end
2576 | L'.SgiVal (x, n, c) => 2638 | L'.SgiVal (x, n, c) =>
2577 let 2639 let
2578 val (vals, x) = 2640 val (vals, x) =
2579 if SS.member (vals, x) then 2641 if SS.member (vals, x) then