Mercurial > urweb

comparison src/elaborate.sml @ 162:06a98129b23f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add datatype import constructor annotations; datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 12:30:04 -0400
parents a5ae7b3e37a4
children a158f8c5aa55
comparison
equal deleted inserted replaced
161:a5ae7b3e37a4 162:06a98129b23f
1357 | SOME t' => (L'.TFun (t', t), loc) 1357 | SOME t' => (L'.TFun (t', t), loc)
1358 in 1358 in
1359 E.pushENamedAs env x n t 1359 E.pushENamedAs env x n t
1360 end) env xncs 1360 end) env xncs
1361 in 1361 in
1362 ([(L'.SgiDatatypeImp (x, n', n, ms, s), loc)], (env, denv, gs)) 1362 ([(L'.SgiDatatypeImp (x, n', n, ms, s, xncs), loc)], (env, denv, gs))
1363 end) 1363 end)
1364 | _ => (strError env (NotDatatype loc); 1364 | _ => (strError env (NotDatatype loc);
1365 ([], (env, denv, []))) 1365 ([], (env, denv, [])))
1366 end) 1366 end)
1367 1367
1451 sgnError env (DuplicateCon (loc, x)) 1451 sgnError env (DuplicateCon (loc, x))
1452 else 1452 else
1453 (); 1453 ();
1454 (SS.add (cons, x), vals, sgns, strs) 1454 (SS.add (cons, x), vals, sgns, strs)
1455 end 1455 end
1456 | L'.SgiDatatypeImp (x, _, _, _, _) => 1456 | L'.SgiDatatypeImp (x, _, _, _, _, _) =>
1457 (if SS.member (cons, x) then 1457 (if SS.member (cons, x) then
1458 sgnError env (DuplicateCon (loc, x)) 1458 sgnError env (DuplicateCon (loc, x))
1459 else 1459 else
1460 (); 1460 ();
1461 (SS.add (cons, x), vals, sgns, strs)) 1461 (SS.add (cons, x), vals, sgns, strs))
1544 1544
1545 | L'.SgnConst sgis => 1545 | L'.SgnConst sgis =>
1546 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) => 1546 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
1547 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) 1547 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
1548 | (L'.SgiDatatype (x, n, xncs), loc) => 1548 | (L'.SgiDatatype (x, n, xncs), loc) =>
1549 (L'.SgiDatatypeImp (x, n, str, strs, x), loc) 1549 (L'.SgiDatatypeImp (x, n, str, strs, x, xncs), loc)
1550 | (L'.SgiStr (x, n, sgn), loc) => 1550 | (L'.SgiStr (x, n, sgn), loc) =>
1551 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) 1551 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
1552 | x => x) sgis), #2 sgn) 1552 | x => x) sgis), #2 sgn)
1553 | L'.SgnFun _ => sgn 1553 | L'.SgnFun _ => sgn
1554 | L'.SgnWhere _ => sgn 1554 | L'.SgnWhere _ => sgn
1582 (L'.StrVar str, #2 sgn) strs 1582 (L'.StrVar str, #2 sgn) strs
1583 in 1583 in
1584 case #1 (hnormSgn env sgn) of 1584 case #1 (hnormSgn env sgn) of
1585 L'.SgnConst sgis => 1585 L'.SgnConst sgis =>
1586 ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) => 1586 ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) =>
1587 case sgi of 1587 let
1588 L'.SgiConAbs (x, n, k) => 1588 val d =
1589 let 1589 case sgi of
1590 val c = (L'.CModProj (str, strs, x), loc) 1590 L'.SgiConAbs (x, n, k) =>
1591 in 1591 let
1592 ((L'.DCon (x, n, k, c), loc), 1592 val c = (L'.CModProj (str, strs, x), loc)
1593 (E.pushCNamedAs env' x n k (SOME c), denv')) 1593 in
1594 end 1594 (L'.DCon (x, n, k, c), loc)
1595 | L'.SgiCon (x, n, k, c) => 1595 end
1596 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc), 1596 | L'.SgiCon (x, n, k, c) =>
1597 (E.pushCNamedAs env' x n k (SOME c), denv')) 1597 (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
1598 | L'.SgiDatatype (x, n, xncs) => 1598 | L'.SgiDatatype (x, n, xncs) =>
1599 let 1599 (L'.DDatatypeImp (x, n, str, strs, x, xncs), loc)
1600 val k = (L'.KType, loc) 1600 | L'.SgiDatatypeImp (x, n, m1, ms, x', xncs) =>
1601 val c = (L'.CModProj (str, strs, x), loc) 1601 (L'.DDatatypeImp (x, n, m1, ms, x', xncs), loc)
1602 in 1602 | L'.SgiVal (x, n, t) =>
1603 ((L'.DDatatypeImp (x, n, str, strs, x), loc), 1603 (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)
1604 (E.pushCNamedAs env' x n k (SOME c), denv')) 1604 | L'.SgiStr (x, n, sgn) =>
1605 end 1605 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)
1606 | L'.SgiDatatypeImp (x, n, m1, ms, x') => 1606 | L'.SgiSgn (x, n, sgn) =>
1607 let 1607 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
1608 val k = (L'.KType, loc) 1608 | L'.SgiConstraint (c1, c2) =>
1609 val c = (L'.CModProj (m1, ms, x'), loc) 1609 (L'.DConstraint (c1, c2), loc)
1610 in 1610 in
1611 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc), 1611 (d, (E.declBinds env' d, denv'))
1612 (E.pushCNamedAs env' x n k (SOME c), denv')) 1612 end)
1613 end
1614 | L'.SgiVal (x, n, t) =>
1615 ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc),
1616 (E.pushENamedAs env' x n t, denv'))
1617 | L'.SgiStr (x, n, sgn) =>
1618 ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc),
1619 (E.pushStrNamedAs env' x n sgn, denv'))
1620 | L'.SgiSgn (x, n, sgn) =>
1621 ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc),
1622 (E.pushSgnNamedAs env' x n sgn, denv'))
1623 | L'.SgiConstraint (c1, c2) =>
1624 ((L'.DConstraint (c1, c2), loc),
1625 (env', denv)))
1626 (env, denv) sgis 1613 (env, denv) sgis
1627 | _ => (strError env (UnOpenable sgn); 1614 | _ => (strError env (UnOpenable sgn);
1628 ([], (env, denv))) 1615 ([], (env, denv)))
1629 end 1616 end
1630 1617
1727 in 1714 in
1728 case sgi1 of 1715 case sgi1 of
1729 L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE) 1716 L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
1730 | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1) 1717 | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1)
1731 | L'.SgiDatatype (x', n1, _) => found (x', n1, (L'.KType, loc), NONE) 1718 | L'.SgiDatatype (x', n1, _) => found (x', n1, (L'.KType, loc), NONE)
1732 | L'.SgiDatatypeImp (x', n1, m1, ms, s) => 1719 | L'.SgiDatatypeImp (x', n1, m1, ms, s, _) =>
1733 found (x', n1, (L'.KType, loc), SOME (L'.CModProj (m1, ms, s), loc)) 1720 found (x', n1, (L'.KType, loc), SOME (L'.CModProj (m1, ms, s), loc))
1734 | _ => NONE 1721 | _ => NONE
1735 end) 1722 end)
1736 1723
1737 | L'.SgiCon (x, n2, k2, c2) => 1724 | L'.SgiCon (x, n2, k2, c2) =>
1794 L'.SgiDatatype (x', n1, xncs1) => 1781 L'.SgiDatatype (x', n1, xncs1) =>
1795 if x' = x then 1782 if x' = x then
1796 found (n1, xncs1) 1783 found (n1, xncs1)
1797 else 1784 else
1798 NONE 1785 NONE
1799 | L'.SgiDatatypeImp (x', n1, m1, ms, s) => 1786 | L'.SgiDatatypeImp (x', n1, _, _, _, xncs1) =>
1800 let 1787 if x' = x then
1801 val (str, sgn) = E.chaseMpath env (m1, ms) 1788 found (n1, xncs1)
1802 in 1789 else
1803 case E.projectDatatype env {str = str, sgn = sgn, field = s} of 1790 NONE
1804 NONE => NONE
1805 | SOME xncs1 => found (n1, xncs1)
1806 end
1807 | _ => NONE 1791 | _ => NONE
1808 end) 1792 end)
1809 1793
1810 | L'.SgiDatatypeImp (x, n2, m11, ms1, s1) => 1794 | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, _) =>
1811 seek (fn sgi1All as (sgi1, _) => 1795 seek (fn sgi1All as (sgi1, _) =>
1812 case sgi1 of 1796 case sgi1 of
1813 L'.SgiDatatypeImp (x', n1, m12, ms2, s2) => 1797 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _) =>
1814 if x = x' then 1798 if x = x' then
1815 let 1799 let
1816 val k = (L'.KType, loc) 1800 val k = (L'.KType, loc)
1817 val t1 = (L'.CModProj (m11, ms1, s1), loc) 1801 val t1 = (L'.CModProj (m11, ms1, s1), loc)
1818 val t2 = (L'.CModProj (m12, ms2, s2), loc) 1802 val t2 = (L'.CModProj (m12, ms2, s2), loc)
2014 | SOME t' => (L'.TFun (t', t), loc) 1998 | SOME t' => (L'.TFun (t', t), loc)
2015 in 1999 in
2016 E.pushENamedAs env x n t 2000 E.pushENamedAs env x n t
2017 end) env xncs 2001 end) env xncs
2018 in 2002 in
2019 ([(L'.DDatatypeImp (x, n', n, ms, s), loc)], (env, denv, gs)) 2003 ([(L'.DDatatypeImp (x, n', n, ms, s, xncs), loc)], (env, denv, gs))
2020 end) 2004 end)
2021 | _ => (strError env (NotDatatype loc); 2005 | _ => (strError env (NotDatatype loc);
2022 ([], (env, denv, []))) 2006 ([], (env, denv, [])))
2023 end) 2007 end)
2024 2008
2292 ((x, n, t), SS.add (vals, x))) 2276 ((x, n, t), SS.add (vals, x)))
2293 vals xncs 2277 vals xncs
2294 in 2278 in
2295 ((L'.SgiDatatype (x, n, xncs), loc) :: sgis, cons, vals, sgns, strs) 2279 ((L'.SgiDatatype (x, n, xncs), loc) :: sgis, cons, vals, sgns, strs)
2296 end 2280 end
2297 | L'.SgiDatatypeImp (x, n, m1, ms, x') => 2281 | L'.SgiDatatypeImp (x, n, m1, ms, x', xncs) =>
2298 let 2282 let
2299 val (cons, x) = 2283 val (cons, x) =
2300 if SS.member (cons, x) then 2284 if SS.member (cons, x) then
2301 (cons, "?" ^ x) 2285 (cons, "?" ^ x)
2302 else 2286 else
2303 (SS.add (cons, x), x) 2287 (SS.add (cons, x), x)
2304 in 2288 in
2305 ((L'.SgiDatatypeImp (x, n, m1, ms, x'), loc) :: sgis, cons, vals, sgns, strs) 2289 ((L'.SgiDatatypeImp (x, n, m1, ms, x', xncs), loc) :: sgis, cons, vals, sgns, strs)
2306 end 2290 end
2307 | L'.SgiVal (x, n, c) => 2291 | L'.SgiVal (x, n, c) =>
2308 let 2292 let
2309 val (vals, x) = 2293 val (vals, x) =
2310 if SS.member (vals, x) then 2294 if SS.member (vals, x) then