Mercurial > urweb

comparison src/elaborate.sml @ 156:34ccd7d2bea8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of datatype support
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 15:02:03 -0400
parents cfe6f9db74aa
children adc4e42e3adc
comparison
equal deleted inserted replaced
155:4334bb734187 156:34ccd7d2bea8
1156 datatype sgn_error = 1156 datatype sgn_error =
1157 UnboundSgn of ErrorMsg.span * string 1157 UnboundSgn of ErrorMsg.span * string
1158 | UnmatchedSgi of L'.sgn_item 1158 | UnmatchedSgi of L'.sgn_item
1159 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error 1159 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
1160 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error 1160 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
1161 | SgiMismatchedDatatypes of L'.sgn_item * L'.sgn_item * (L'.con * L'.con * cunify_error) option
1161 | SgnWrongForm of L'.sgn * L'.sgn 1162 | SgnWrongForm of L'.sgn * L'.sgn
1162 | UnWhereable of L'.sgn * string 1163 | UnWhereable of L'.sgn * string
1163 | WhereWrongKind of L'.kind * L'.kind * kunify_error 1164 | WhereWrongKind of L'.kind * L'.kind * kunify_error
1164 | NotIncludable of L'.sgn 1165 | NotIncludable of L'.sgn
1165 | DuplicateCon of ErrorMsg.span * string 1166 | DuplicateCon of ErrorMsg.span * string
1187 eprefaces' [("Have", p_sgn_item env sgi1), 1188 eprefaces' [("Have", p_sgn_item env sgi1),
1188 ("Need", p_sgn_item env sgi2), 1189 ("Need", p_sgn_item env sgi2),
1189 ("Con 1", p_con env c1), 1190 ("Con 1", p_con env c1),
1190 ("Con 2", p_con env c2)]; 1191 ("Con 2", p_con env c2)];
1191 cunifyError env cerr) 1192 cunifyError env cerr)
1193 | SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
1194 (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
1195 eprefaces' [("Have", p_sgn_item env sgi1),
1196 ("Need", p_sgn_item env sgi2)];
1197 Option.app (fn (c1, c2, ue) =>
1198 (eprefaces "Unification error"
1199 [("Con 1", p_con env c1),
1200 ("Con 2", p_con env c2)];
1201 cunifyError env ue)) cerro)
1192 | SgnWrongForm (sgn1, sgn2) => 1202 | SgnWrongForm (sgn1, sgn2) =>
1193 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:"; 1203 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
1194 eprefaces' [("Sig 1", p_sgn env sgn1), 1204 eprefaces' [("Sig 1", p_sgn env sgn1),
1195 ("Sig 2", p_sgn env sgn2)]) 1205 ("Sig 2", p_sgn env sgn2)])
1196 | UnWhereable (sgn, x) => 1206 | UnWhereable (sgn, x) =>
1221 UnboundStr of ErrorMsg.span * string 1231 UnboundStr of ErrorMsg.span * string
1222 | NotFunctor of L'.sgn 1232 | NotFunctor of L'.sgn
1223 | FunctorRebind of ErrorMsg.span 1233 | FunctorRebind of ErrorMsg.span
1224 | UnOpenable of L'.sgn 1234 | UnOpenable of L'.sgn
1225 | NotType of L'.kind * (L'.kind * L'.kind * kunify_error) 1235 | NotType of L'.kind * (L'.kind * L'.kind * kunify_error)
1236 | DuplicateConstructor of string * ErrorMsg.span
1226 1237
1227 fun strError env err = 1238 fun strError env err =
1228 case err of 1239 case err of
1229 UnboundStr (loc, s) => 1240 UnboundStr (loc, s) =>
1230 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s) 1241 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
1240 (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'"; 1251 (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
1241 eprefaces' [("Kind", p_kind k), 1252 eprefaces' [("Kind", p_kind k),
1242 ("Subkind 1", p_kind k1), 1253 ("Subkind 1", p_kind k1),
1243 ("Subkind 2", p_kind k2)]; 1254 ("Subkind 2", p_kind k2)];
1244 kunifyError ue) 1255 kunifyError ue)
1256 | DuplicateConstructor (x, loc) =>
1257 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
1245 1258
1246 val hnormSgn = E.hnormSgn 1259 val hnormSgn = E.hnormSgn
1247 1260
1248 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = 1261 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
1249 case sgi of 1262 case sgi of
1267 in 1280 in
1268 checkKind env c' ck k'; 1281 checkKind env c' ck k';
1269 1282
1270 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) 1283 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
1271 end 1284 end
1285
1286 | L.SgiDatatype _ => raise Fail "Elaborate SgiDatatype"
1287
1288 | L.SgiDatatypeImp _ => raise Fail "Elaborate SgiDatatypeImp"
1272 1289
1273 | L.SgiVal (x, c) => 1290 | L.SgiVal (x, c) =>
1274 let 1291 let
1275 val (c', ck, gs') = elabCon (env, denv) c 1292 val (c', ck, gs') = elabCon (env, denv) c
1276 1293
1335 sgnError env (DuplicateCon (loc, x)) 1352 sgnError env (DuplicateCon (loc, x))
1336 else 1353 else
1337 (); 1354 ();
1338 (SS.add (cons, x), vals, sgns, strs)) 1355 (SS.add (cons, x), vals, sgns, strs))
1339 | L'.SgiCon (x, _, _, _) => 1356 | L'.SgiCon (x, _, _, _) =>
1357 (if SS.member (cons, x) then
1358 sgnError env (DuplicateCon (loc, x))
1359 else
1360 ();
1361 (SS.add (cons, x), vals, sgns, strs))
1362 | L'.SgiDatatype (x, _, xncs) =>
1363 let
1364 val vals = foldl (fn ((x, _, _), vals) =>
1365 (if SS.member (vals, x) then
1366 sgnError env (DuplicateVal (loc, x))
1367 else
1368 ();
1369 SS.add (vals, x)))
1370 vals xncs
1371 in
1372 if SS.member (cons, x) then
1373 sgnError env (DuplicateCon (loc, x))
1374 else
1375 ();
1376 (SS.add (cons, x), vals, sgns, strs)
1377 end
1378 | L'.SgiDatatypeImp (x, _, _, _, _) =>
1340 (if SS.member (cons, x) then 1379 (if SS.member (cons, x) then
1341 sgnError env (DuplicateCon (loc, x)) 1380 sgnError env (DuplicateCon (loc, x))
1342 else 1381 else
1343 (); 1382 ();
1344 (SS.add (cons, x), vals, sgns, strs)) 1383 (SS.add (cons, x), vals, sgns, strs))
1474 (E.pushCNamedAs env' x n k (SOME c), denv')) 1513 (E.pushCNamedAs env' x n k (SOME c), denv'))
1475 end 1514 end
1476 | L'.SgiCon (x, n, k, c) => 1515 | L'.SgiCon (x, n, k, c) =>
1477 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc), 1516 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
1478 (E.pushCNamedAs env' x n k (SOME c), denv')) 1517 (E.pushCNamedAs env' x n k (SOME c), denv'))
1518 | L'.SgiDatatype (x, n, xncs) =>
1519 let
1520 val k = (L'.KType, loc)
1521 val c = (L'.CModProj (str, strs, x), loc)
1522 in
1523 ((L'.DDatatypeImp (x, n, str, strs, x), loc),
1524 (E.pushCNamedAs env' x n k (SOME c), denv'))
1525 end
1526 | L'.SgiDatatypeImp (x, n, m1, ms, x') =>
1527 let
1528 val k = (L'.KType, loc)
1529 val c = (L'.CModProj (m1, ms, x'), loc)
1530 in
1531 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
1532 (E.pushCNamedAs env' x n k (SOME c), denv'))
1533 end
1479 | L'.SgiVal (x, n, t) => 1534 | L'.SgiVal (x, n, t) =>
1480 ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc), 1535 ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc),
1481 (E.pushENamedAs env' x n t, denv')) 1536 (E.pushENamedAs env' x n t, denv'))
1482 | L'.SgiStr (x, n, sgn) => 1537 | L'.SgiStr (x, n, sgn) =>
1483 ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc), 1538 ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc),
1485 | L'.SgiSgn (x, n, sgn) => 1540 | L'.SgiSgn (x, n, sgn) =>
1486 ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc), 1541 ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc),
1487 (E.pushSgnNamedAs env' x n sgn, denv')) 1542 (E.pushSgnNamedAs env' x n sgn, denv'))
1488 | L'.SgiConstraint (c1, c2) => 1543 | L'.SgiConstraint (c1, c2) =>
1489 ((L'.DConstraint (c1, c2), loc), 1544 ((L'.DConstraint (c1, c2), loc),
1490 (env', denv (* D.assert env denv (c1, c2) *) ))) 1545 (env', denv)))
1491 (env, denv) sgis 1546 (env, denv) sgis
1492 | _ => (strError env (UnOpenable sgn); 1547 | _ => (strError env (UnOpenable sgn);
1493 ([], (env, denv))) 1548 ([], (env, denv)))
1494 end 1549 end
1495 1550
1526 end 1581 end
1527 1582
1528 fun sgiOfDecl (d, loc) = 1583 fun sgiOfDecl (d, loc) =
1529 case d of 1584 case d of
1530 L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)] 1585 L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
1586 | L'.DDatatype x => [(L'.SgiDatatype x, loc)]
1587 | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)]
1531 | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)] 1588 | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)]
1532 | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis 1589 | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis
1533 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] 1590 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
1534 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] 1591 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
1535 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] 1592 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
1549 (L'.SgnError, _) => () 1606 (L'.SgnError, _) => ()
1550 | (_, L'.SgnError) => () 1607 | (_, L'.SgnError) => ()
1551 1608
1552 | (L'.SgnConst sgis1, L'.SgnConst sgis2) => 1609 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
1553 let 1610 let
1554 fun folder (sgi2All as (sgi, _), (env, denv)) = 1611 fun folder (sgi2All as (sgi, loc), (env, denv)) =
1555 let 1612 let
1556 fun seek p = 1613 fun seek p =
1557 let 1614 let
1558 fun seek (env, denv) ls = 1615 fun seek (env, denv) ls =
1559 case ls of 1616 case ls of
1611 end 1668 end
1612 else 1669 else
1613 NONE 1670 NONE
1614 | _ => NONE) 1671 | _ => NONE)
1615 1672
1673 | L'.SgiDatatype (x, n2, xncs2) =>
1674 seek (fn sgi1All as (sgi1, _) =>
1675 case sgi1 of
1676 L'.SgiDatatype (x', n1, xncs1) =>
1677 let
1678 fun mismatched ue =
1679 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
1680 SOME (env, denv))
1681
1682 fun good () =
1683 let
1684 val env = E.sgiBinds env sgi2All
1685 val env = if n1 = n2 then
1686 env
1687 else
1688 E.pushCNamedAs env x n1 (L'.KType, loc)
1689 (SOME (L'.CNamed n1, loc))
1690 in
1691 SOME (env, denv)
1692 end
1693
1694 fun xncBad ((x1, _, t1), (x2, _, t2)) =
1695 String.compare (x1, x2) <> EQUAL
1696 orelse case (t1, t2) of
1697 (NONE, NONE) => false
1698 | (SOME t1, SOME t2) =>
1699 not (List.null (unifyCons (env, denv) t1 t2))
1700 | _ => true
1701 in
1702 (if x = x' then
1703 if length xncs1 <> length xncs2
1704 orelse ListPair.exists xncBad (xncs1, xncs2) then
1705 mismatched NONE
1706 else
1707 good ()
1708 else
1709 NONE)
1710 handle CUnify ue => mismatched (SOME ue)
1711 end
1712 | _ => NONE)
1713
1714 | L'.SgiDatatypeImp _ => raise Fail "SgiDatatypeImp in subsgn"
1715
1616 | L'.SgiVal (x, n2, c2) => 1716 | L'.SgiVal (x, n2, c2) =>
1617 seek (fn sgi1All as (sgi1, _) => 1717 seek (fn sgi1All as (sgi1, _) =>
1618 case sgi1 of 1718 case sgi1 of
1619 L'.SgiVal (x', n1, c1) => 1719 L'.SgiVal (x', n1, c1) =>
1620 if x = x' then 1720 if x = x' then
1720 in 1820 in
1721 checkKind env c' ck k'; 1821 checkKind env c' ck k';
1722 1822
1723 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) 1823 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
1724 end 1824 end
1825 | L.DDatatype (x, xcs) =>
1826 let
1827 val k = (L'.KType, loc)
1828 val (env, n) = E.pushCNamed env x k NONE
1829 val t = (L'.CNamed n, loc)
1830
1831 val (xcs, (used, env, gs)) =
1832 ListUtil.foldlMap
1833 (fn ((x, to), (used, env, gs)) =>
1834 let
1835 val (to, t, gs') = case to of
1836 NONE => (NONE, t, gs)
1837 | SOME t' =>
1838 let
1839 val (t', tk, gs') = elabCon (env, denv) t'
1840 in
1841 checkKind env t' tk k;
1842 (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
1843 end
1844
1845 val (env, n') = E.pushENamed env x t
1846 in
1847 if SS.member (used, x) then
1848 strError env (DuplicateConstructor (x, loc))
1849 else
1850 ();
1851 ((x, n', to), (SS.add (used, x), env, gs'))
1852 end)
1853 (SS.empty, env, []) xcs
1854 in
1855 ([(L'.DDatatype (x, n, xcs), loc)], (env, denv, gs))
1856 end
1857
1858 | L.DDatatypeImp _ => raise Fail "Elaborate DDatatypeImp"
1725 | L.DVal (x, co, e) => 1859 | L.DVal (x, co, e) =>
1726 let 1860 let
1727 val (c', _, gs1) = case co of 1861 val (c', _, gs1) = case co of
1728 NONE => (cunif (loc, ktype), ktype, []) 1862 NONE => (cunif (loc, ktype), ktype, [])
1729 | SOME c => elabCon (env, denv) c 1863 | SOME c => elabCon (env, denv) c
1973 else 2107 else
1974 (SS.add (cons, x), x) 2108 (SS.add (cons, x), x)
1975 in 2109 in
1976 ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs) 2110 ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
1977 end 2111 end
2112 | L'.SgiDatatype (x, n, xncs) =>
2113 let
2114 val (cons, x) =
2115 if SS.member (cons, x) then
2116 (cons, "?" ^ x)
2117 else
2118 (SS.add (cons, x), x)
2119
2120 val (xncs, vals) =
2121 ListUtil.foldlMap
2122 (fn ((x, n, t), vals) =>
2123 if SS.member (vals, x) then
2124 (("?" ^ x, n, t), vals)
2125 else
2126 ((x, n, t), SS.add (vals, x)))
2127 vals xncs
2128 in
2129 ((L'.SgiDatatype (x, n, xncs), loc) :: sgis, cons, vals, sgns, strs)
2130 end
2131 | L'.SgiDatatypeImp (x, n, m1, ms, x') =>
2132 let
2133 val (cons, x) =
2134 if SS.member (cons, x) then
2135 (cons, "?" ^ x)
2136 else
2137 (SS.add (cons, x), x)
2138 in
2139 ((L'.SgiDatatypeImp (x, n, m1, ms, x'), loc) :: sgis, cons, vals, sgns, strs)
2140 end
1978 | L'.SgiVal (x, n, c) => 2141 | L'.SgiVal (x, n, c) =>
1979 let 2142 let
1980 val (vals, x) = 2143 val (vals, x) =
1981 if SS.member (vals, x) then 2144 if SS.member (vals, x) then
1982 (vals, "?" ^ x) 2145 (vals, "?" ^ x)