Mercurial > urweb

comparison src/elaborate.sml @ 75:88ffb3d61817

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Folding through a functor
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Jun 2008 12:35:26 -0400
parents 144d082b47ae
children 522f4bd3955e
comparison
equal deleted inserted replaced
74:144d082b47ae 75:88ffb3d61817
1080 | UnmatchedSgi of L'.sgn_item 1080 | UnmatchedSgi of L'.sgn_item
1081 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error 1081 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
1082 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error 1082 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
1083 | SgnWrongForm of L'.sgn * L'.sgn 1083 | SgnWrongForm of L'.sgn * L'.sgn
1084 | UnWhereable of L'.sgn * string 1084 | UnWhereable of L'.sgn * string
1085 | WhereWrongKind of L'.kind * L'.kind * kunify_error
1085 | NotIncludable of L'.sgn 1086 | NotIncludable of L'.sgn
1086 | DuplicateCon of ErrorMsg.span * string 1087 | DuplicateCon of ErrorMsg.span * string
1087 | DuplicateVal of ErrorMsg.span * string 1088 | DuplicateVal of ErrorMsg.span * string
1088 | DuplicateSgn of ErrorMsg.span * string 1089 | DuplicateSgn of ErrorMsg.span * string
1089 | DuplicateStr of ErrorMsg.span * string 1090 | DuplicateStr of ErrorMsg.span * string
1115 ("Sig 2", p_sgn env sgn2)]) 1116 ("Sig 2", p_sgn env sgn2)])
1116 | UnWhereable (sgn, x) => 1117 | UnWhereable (sgn, x) =>
1117 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'"; 1118 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
1118 eprefaces' [("Signature", p_sgn env sgn), 1119 eprefaces' [("Signature", p_sgn env sgn),
1119 ("Field", PD.string x)]) 1120 ("Field", PD.string x)])
1121 | WhereWrongKind (k1, k2, kerr) =>
1122 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
1123 eprefaces' [("Have", p_kind k1),
1124 ("Need", p_kind k2)];
1125 kunifyError kerr)
1120 | NotIncludable sgn => 1126 | NotIncludable sgn =>
1121 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'"; 1127 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
1122 eprefaces' [("Signature", p_sgn env sgn)]) 1128 eprefaces' [("Signature", p_sgn env sgn)])
1123 | DuplicateCon (loc, s) => 1129 | DuplicateCon (loc, s) =>
1124 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature") 1130 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
1132 datatype str_error = 1138 datatype str_error =
1133 UnboundStr of ErrorMsg.span * string 1139 UnboundStr of ErrorMsg.span * string
1134 | NotFunctor of L'.sgn 1140 | NotFunctor of L'.sgn
1135 | FunctorRebind of ErrorMsg.span 1141 | FunctorRebind of ErrorMsg.span
1136 | UnOpenable of L'.sgn 1142 | UnOpenable of L'.sgn
1143 | NotType of L'.kind * (L'.kind * L'.kind * kunify_error)
1137 1144
1138 fun strError env err = 1145 fun strError env err =
1139 case err of 1146 case err of
1140 UnboundStr (loc, s) => 1147 UnboundStr (loc, s) =>
1141 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s) 1148 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
1145 | FunctorRebind loc => 1152 | FunctorRebind loc =>
1146 ErrorMsg.errorAt loc "Attempt to rebind functor" 1153 ErrorMsg.errorAt loc "Attempt to rebind functor"
1147 | UnOpenable sgn => 1154 | UnOpenable sgn =>
1148 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure"; 1155 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
1149 eprefaces' [("Signature", p_sgn env sgn)]) 1156 eprefaces' [("Signature", p_sgn env sgn)])
1157 | NotType (k, (k1, k2, ue)) =>
1158 (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
1159 eprefaces' [("Kind", p_kind k),
1160 ("Subkind 1", p_kind k1),
1161 ("Subkind 2", p_kind k2)];
1162 kunifyError ue)
1150 1163
1151 val hnormSgn = E.hnormSgn 1164 val hnormSgn = E.hnormSgn
1152 1165
1153 fun elabSgn_item ((sgi, loc), env) = 1166 fun elabSgn_item ((sgi, loc), env) =
1154 let 1167 let
1207 let 1220 let
1208 val (c', ck) = elabCon env c 1221 val (c', ck) = elabCon env c
1209 1222
1210 val (env', n) = E.pushENamed env x c' 1223 val (env', n) = E.pushENamed env x c'
1211 in 1224 in
1212 unifyKinds ck ktype; 1225 (unifyKinds ck ktype
1226 handle KUnify ue => strError env (NotType (ck, ue)));
1213 1227
1214 if ErrorMsg.anyErrors () then 1228 if ErrorMsg.anyErrors () then
1215 () 1229 ()
1216 else ( 1230 else (
1217 if kunifsInCon c' then 1231 if kunifsInCon c' then
1314 val (c', ck) = elabCon env c 1328 val (c', ck) = elabCon env c
1315 in 1329 in
1316 case #1 (hnormSgn env sgn') of 1330 case #1 (hnormSgn env sgn') of
1317 L'.SgnError => sgnerror 1331 L'.SgnError => sgnerror
1318 | L'.SgnConst sgis => 1332 | L'.SgnConst sgis =>
1319 if List.exists (fn (L'.SgiConAbs (x, _, k), _) => 1333 if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
1320 (unifyKinds k ck; 1334 x' = x andalso
1335 (unifyKinds k ck
1336 handle KUnify x => sgnError env (WhereWrongKind x);
1321 true) 1337 true)
1322 | _ => false) sgis then 1338 | _ => false) sgis then
1323 (L'.SgnWhere (sgn', x, c'), loc) 1339 (L'.SgnWhere (sgn', x, c'), loc)
1324 else 1340 else
1325 (sgnError env (UnWhereable (sgn', x)); 1341 (sgnError env (UnWhereable (sgn', x));