aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-22 20:11:59 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-22 20:11:59 -0400
commit55ac3f4f2af733079401d83e98431e6d11b0fc59 (patch)
tree0ec02a2bc195bdd9ac6a3e3c5c2d22589cf02a03 /src/elaborate.sml
parent5d0d8cc5212faf5e2433fa2e9b6f05aa195e45ac (diff)
Signature duplicate entry checking for principal signatures
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml34
1 files changed, 34 insertions, 0 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 6cd587d9..64613703 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1578,6 +1578,40 @@ and elabStr env (str, loc) =
let
val (ds', env') = ListUtil.foldlMapConcat elabDecl env ds
val sgis = map sgiOfDecl ds'
+
+ val (sgis, _, _, _, _) =
+ foldr (fn (sgall as (sgi, loc), (sgis, cons, vals, sgns, strs)) =>
+ case sgi of
+ L'.SgiConAbs (x, _, _) =>
+ (if SS.member (cons, x) then
+ sgnError env (DuplicateCon (loc, x))
+ else
+ ();
+ (sgall :: sgis, SS.add (cons, x), vals, sgns, strs))
+ | L'.SgiCon (x, _, _, _) =>
+ (if SS.member (cons, x) then
+ sgnError env (DuplicateCon (loc, x))
+ else
+ ();
+ (sgall :: sgis, SS.add (cons, x), vals, sgns, strs))
+ | L'.SgiVal (x, _, _) =>
+ if SS.member (vals, x) then
+ (sgis, cons, vals, sgns, strs)
+ else
+ (sgall :: sgis, cons, SS.add (vals, x), sgns, strs)
+ | L'.SgiSgn (x, _, _) =>
+ (if SS.member (sgns, x) then
+ sgnError env (DuplicateSgn (loc, x))
+ else
+ ();
+ (sgall :: sgis, cons, vals, SS.add (sgns, x), strs))
+ | L'.SgiStr (x, _, _) =>
+ (if SS.member (strs, x) then
+ sgnError env (DuplicateStr (loc, x))
+ else
+ ();
+ (sgall :: sgis, cons, vals, sgns, SS.add (strs, x))))
+ ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
in
((L'.StrConst ds', loc), (L'.SgnConst sgis, loc))
end