comparison src/elaborate.sml @ 63:c5a503ad0d8c

Signature duplicate entry checking for principal signatures
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 20:11:59 -0400
parents d72b89a1b150
children d609820c5834
comparison
equal deleted inserted replaced
62:d72b89a1b150 63:c5a503ad0d8c
1576 case str of 1576 case str of
1577 L.StrConst ds => 1577 L.StrConst ds =>
1578 let 1578 let
1579 val (ds', env') = ListUtil.foldlMapConcat elabDecl env ds 1579 val (ds', env') = ListUtil.foldlMapConcat elabDecl env ds
1580 val sgis = map sgiOfDecl ds' 1580 val sgis = map sgiOfDecl ds'
1581
1582 val (sgis, _, _, _, _) =
1583 foldr (fn (sgall as (sgi, loc), (sgis, cons, vals, sgns, strs)) =>
1584 case sgi of
1585 L'.SgiConAbs (x, _, _) =>
1586 (if SS.member (cons, x) then
1587 sgnError env (DuplicateCon (loc, x))
1588 else
1589 ();
1590 (sgall :: sgis, SS.add (cons, x), vals, sgns, strs))
1591 | L'.SgiCon (x, _, _, _) =>
1592 (if SS.member (cons, x) then
1593 sgnError env (DuplicateCon (loc, x))
1594 else
1595 ();
1596 (sgall :: sgis, SS.add (cons, x), vals, sgns, strs))
1597 | L'.SgiVal (x, _, _) =>
1598 if SS.member (vals, x) then
1599 (sgis, cons, vals, sgns, strs)
1600 else
1601 (sgall :: sgis, cons, SS.add (vals, x), sgns, strs)
1602 | L'.SgiSgn (x, _, _) =>
1603 (if SS.member (sgns, x) then
1604 sgnError env (DuplicateSgn (loc, x))
1605 else
1606 ();
1607 (sgall :: sgis, cons, vals, SS.add (sgns, x), strs))
1608 | L'.SgiStr (x, _, _) =>
1609 (if SS.member (strs, x) then
1610 sgnError env (DuplicateStr (loc, x))
1611 else
1612 ();
1613 (sgall :: sgis, cons, vals, sgns, SS.add (strs, x))))
1614 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
1581 in 1615 in
1582 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc)) 1616 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc))
1583 end 1617 end
1584 | L.StrVar x => 1618 | L.StrVar x =>
1585 (case E.lookupStr env x of 1619 (case E.lookupStr env x of