Mercurial > urweb

comparison src/elaborate.sml @ 62:d72b89a1b150

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Signature duplicate entry checking
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 19:44:01 -0400
parents 48b6d2c3df46
children c5a503ad0d8c
comparison
equal deleted inserted replaced
61:48b6d2c3df46 62:d72b89a1b150
34 structure U = ElabUtil 34 structure U = ElabUtil
35 35
36 open Print 36 open Print
37 open ElabPrint 37 open ElabPrint
38 38
39 structure SS = BinarySetFn(struct
40 type ord_key = string
41 val compare = String.compare
42 end)
43
39 fun elabExplicitness e = 44 fun elabExplicitness e =
40 case e of 45 case e of
41 L.Explicit => L'.Explicit 46 L.Explicit => L'.Explicit
42 | L.Implicit => L'.Implicit 47 | L.Implicit => L'.Implicit
43 48
976 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error 981 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
977 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error 982 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
978 | SgnWrongForm of L'.sgn * L'.sgn 983 | SgnWrongForm of L'.sgn * L'.sgn
979 | UnWhereable of L'.sgn * string 984 | UnWhereable of L'.sgn * string
980 | NotIncludable of L'.sgn 985 | NotIncludable of L'.sgn
986 | DuplicateCon of ErrorMsg.span * string
987 | DuplicateVal of ErrorMsg.span * string
988 | DuplicateSgn of ErrorMsg.span * string
989 | DuplicateStr of ErrorMsg.span * string
981 990
982 fun sgnError env err = 991 fun sgnError env err =
983 case err of 992 case err of
984 UnboundSgn (loc, s) => 993 UnboundSgn (loc, s) =>
985 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s) 994 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
1009 eprefaces' [("Signature", p_sgn env sgn), 1018 eprefaces' [("Signature", p_sgn env sgn),
1010 ("Field", PD.string x)]) 1019 ("Field", PD.string x)])
1011 | NotIncludable sgn => 1020 | NotIncludable sgn =>
1012 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'"; 1021 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
1013 eprefaces' [("Signature", p_sgn env sgn)]) 1022 eprefaces' [("Signature", p_sgn env sgn)])
1023 | DuplicateCon (loc, s) =>
1024 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
1025 | DuplicateVal (loc, s) =>
1026 ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
1027 | DuplicateSgn (loc, s) =>
1028 ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
1029 | DuplicateStr (loc, s) =>
1030 ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
1014 1031
1015 datatype str_error = 1032 datatype str_error =
1016 UnboundStr of ErrorMsg.span * string 1033 UnboundStr of ErrorMsg.span * string
1017 | NotFunctor of L'.sgn 1034 | NotFunctor of L'.sgn
1018 | FunctorRebind of ErrorMsg.span 1035 | FunctorRebind of ErrorMsg.span
1138 and elabSgn env (sgn, loc) = 1155 and elabSgn env (sgn, loc) =
1139 case sgn of 1156 case sgn of
1140 L.SgnConst sgis => 1157 L.SgnConst sgis =>
1141 let 1158 let
1142 val (sgis', _) = ListUtil.foldlMapConcat elabSgn_item env sgis 1159 val (sgis', _) = ListUtil.foldlMapConcat elabSgn_item env sgis
1160
1161 val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) =>
1162 case sgi of
1163 L'.SgiConAbs (x, _, _) =>
1164 (if SS.member (cons, x) then
1165 sgnError env (DuplicateCon (loc, x))
1166 else
1167 ();
1168 (SS.add (cons, x), vals, sgns, strs))
1169 | L'.SgiCon (x, _, _, _) =>
1170 (if SS.member (cons, x) then
1171 sgnError env (DuplicateCon (loc, x))
1172 else
1173 ();
1174 (SS.add (cons, x), vals, sgns, strs))
1175 | L'.SgiVal (x, _, _) =>
1176 (if SS.member (vals, x) then
1177 sgnError env (DuplicateVal (loc, x))
1178 else
1179 ();
1180 (cons, SS.add (vals, x), sgns, strs))
1181 | L'.SgiSgn (x, _, _) =>
1182 (if SS.member (sgns, x) then
1183 sgnError env (DuplicateSgn (loc, x))
1184 else
1185 ();
1186 (cons, vals, SS.add (sgns, x), strs))
1187 | L'.SgiStr (x, _, _) =>
1188 (if SS.member (strs, x) then
1189 sgnError env (DuplicateStr (loc, x))
1190 else
1191 ();
1192 (cons, vals, sgns, SS.add (strs, x))))
1193 (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
1143 in 1194 in
1144 (L'.SgnConst sgis', loc) 1195 (L'.SgnConst sgis', loc)
1145 end 1196 end
1146 | L.SgnVar x => 1197 | L.SgnVar x =>
1147 (case E.lookupSgn env x of 1198 (case E.lookupSgn env x of