Mercurial > urweb

comparison src/elaborate.sml @ 59:abb2b32c19fb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Subsignatures
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 19:10:38 -0400
parents fd8a81ecd598
children 48b6d2c3df46
comparison
equal deleted inserted replaced
58:fd8a81ecd598 59:abb2b32c19fb
986 | UnmatchedSgi (sgi as (_, loc)) => 986 | UnmatchedSgi (sgi as (_, loc)) =>
987 (ErrorMsg.errorAt loc "Unmatched signature item"; 987 (ErrorMsg.errorAt loc "Unmatched signature item";
988 eprefaces' [("Item", p_sgn_item env sgi)]) 988 eprefaces' [("Item", p_sgn_item env sgi)])
989 | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) => 989 | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
990 (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:"; 990 (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
991 eprefaces' [("Item 1", p_sgn_item env sgi1), 991 eprefaces' [("Have", p_sgn_item env sgi1),
992 ("Item 2", p_sgn_item env sgi2), 992 ("Need", p_sgn_item env sgi2),
993 ("Kind 1", p_kind k1), 993 ("Kind 1", p_kind k1),
994 ("Kind 2", p_kind k2)]; 994 ("Kind 2", p_kind k2)];
995 kunifyError kerr) 995 kunifyError kerr)
996 | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) => 996 | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
997 (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:"; 997 (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
998 eprefaces' [("Item 1", p_sgn_item env sgi1), 998 eprefaces' [("Have", p_sgn_item env sgi1),
999 ("Item 2", p_sgn_item env sgi2), 999 ("Need", p_sgn_item env sgi2),
1000 ("Con 1", p_con env c1), 1000 ("Con 1", p_con env c1),
1001 ("Con 2", p_con env c2)]; 1001 ("Con 2", p_con env c2)];
1002 cunifyError env cerr) 1002 cunifyError env cerr)
1003 | SgnWrongForm (sgn1, sgn2) => 1003 | SgnWrongForm (sgn1, sgn2) =>
1004 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:"; 1004 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
1108 val (env', n) = E.pushStrNamed env x sgn' 1108 val (env', n) = E.pushStrNamed env x sgn'
1109 in 1109 in
1110 ([(L'.SgiStr (x, n, sgn'), loc)], env') 1110 ([(L'.SgiStr (x, n, sgn'), loc)], env')
1111 end 1111 end
1112 1112
1113 | L.SgiSgn (x, sgn) =>
1114 let
1115 val sgn' = elabSgn env sgn
1116 val (env', n) = E.pushSgnNamed env x sgn'
1117 in
1118 ([(L'.SgiSgn (x, n, sgn'), loc)], env')
1119 end
1120
1113 | L.SgiInclude sgn => 1121 | L.SgiInclude sgn =>
1114 let 1122 let
1115 val sgn' = elabSgn env sgn 1123 val sgn' = elabSgn env sgn
1116 in 1124 in
1117 case #1 (hnormSgn env sgn') of 1125 case #1 (hnormSgn env sgn') of
1118 L'.SgnConst sgis => 1126 L'.SgnConst sgis =>
1119 (sgis, foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis) 1127 (sgis, foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis)
1120 | _ => (sgnError env (NotIncludable sgn'); 1128 | _ => (sgnError env (NotIncludable sgn');
1121 ([], env)) 1129 ([], env))
1122 end 1130 end
1131
1123 end 1132 end
1124 1133
1125 and elabSgn env (sgn, loc) = 1134 and elabSgn env (sgn, loc) =
1126 case sgn of 1135 case sgn of
1127 L.SgnConst sgis => 1136 L.SgnConst sgis =>
1161 (sgnError env (UnWhereable (sgn', x)); 1170 (sgnError env (UnWhereable (sgn', x));
1162 sgnerror) 1171 sgnerror)
1163 | _ => (sgnError env (UnWhereable (sgn', x)); 1172 | _ => (sgnError env (UnWhereable (sgn', x));
1164 sgnerror) 1173 sgnerror)
1165 end 1174 end
1175 | L.SgnProj (m, ms, x) =>
1176 (case E.lookupStr env m of
1177 NONE => (strError env (UnboundStr (loc, m));
1178 sgnerror)
1179 | SOME (n, sgn) =>
1180 let
1181 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
1182 case E.projectStr env {sgn = sgn, str = str, field = m} of
1183 NONE => (strError env (UnboundStr (loc, m));
1184 (strerror, sgnerror))
1185 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1186 ((L'.StrVar n, loc), sgn) ms
1187 in
1188 case E.projectSgn env {sgn = sgn, str = str, field = x} of
1189 NONE => (sgnError env (UnboundSgn (loc, x));
1190 sgnerror)
1191 | SOME _ => (L'.SgnProj (n, ms, x), loc)
1192 end)
1193
1166 1194
1167 fun sgiOfDecl (d, loc) = 1195 fun sgiOfDecl (d, loc) =
1168 case d of 1196 case d of
1169 L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc) 1197 L'.DCon (x, n, k, c) => (L'.SgiCon (x, n, k, c), loc)
1170 | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc) 1198 | L'.DVal (x, n, t, _) => (L'.SgiVal (x, n, t), loc)
1171 | L'.DSgn _ => NONE 1199 | L'.DSgn (x, n, sgn) => (L'.SgiSgn (x, n, sgn), loc)
1172 | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc) 1200 | L'.DStr (x, n, sgn, _) => (L'.SgiStr (x, n, sgn), loc)
1173 | L'.DFfiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, sgn), loc) 1201 | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc)
1174 1202
1175 fun subSgn env sgn1 (sgn2 as (_, loc2)) = 1203 fun subSgn env sgn1 (sgn2 as (_, loc2)) =
1176 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of 1204 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
1177 (L'.SgnError, _) => () 1205 (L'.SgnError, _) => ()
1178 | (_, L'.SgnError) => () 1206 | (_, L'.SgnError) => ()
1262 SOME env) 1290 SOME env)
1263 else 1291 else
1264 NONE 1292 NONE
1265 | _ => NONE) 1293 | _ => NONE)
1266 (* Add type equations between structures here some day. *) 1294 (* Add type equations between structures here some day. *)
1295
1296 | L'.SgiSgn (x, n2, sgn2) =>
1297 seek (fn sgi1All as (sgi1, _) =>
1298 case sgi1 of
1299 L'.SgiSgn (x', n1, sgn1) =>
1300 if x = x' then
1301 (subSgn env sgn1 sgn2;
1302 subSgn env sgn2 sgn1;
1303 SOME env)
1304 else
1305 NONE
1306 | _ => NONE)
1267 end 1307 end
1268 in 1308 in
1269 ignore (foldl folder env sgis2) 1309 ignore (foldl folder env sgis2)
1270 end 1310 end
1271 1311
1294 | (L'.SgiStr (x, n, sgn), loc) => 1334 | (L'.SgiStr (x, n, sgn), loc) =>
1295 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) 1335 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
1296 | x => x) sgis), #2 sgn) 1336 | x => x) sgis), #2 sgn)
1297 | L'.SgnFun _ => sgn 1337 | L'.SgnFun _ => sgn
1298 | L'.SgnWhere _ => sgn 1338 | L'.SgnWhere _ => sgn
1339 | L'.SgnProj (m, ms, x) =>
1340 case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
1341 (L'.StrVar m, #2 sgn) ms,
1342 sgn = #2 (E.lookupStrNamed env m),
1343 field = x} of
1344 NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE"
1345 | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn}
1299 1346
1300 fun selfifyAt env {str, sgn} = 1347 fun selfifyAt env {str, sgn} =
1301 let 1348 let
1302 fun self (str, _) = 1349 fun self (str, _) =
1303 case str of 1350 case str of
1428 and elabStr env (str, loc) = 1475 and elabStr env (str, loc) =
1429 case str of 1476 case str of
1430 L.StrConst ds => 1477 L.StrConst ds =>
1431 let 1478 let
1432 val (ds', env') = ListUtil.foldlMap elabDecl env ds 1479 val (ds', env') = ListUtil.foldlMap elabDecl env ds
1433 val sgis = List.mapPartial sgiOfDecl ds' 1480 val sgis = map sgiOfDecl ds'
1434 in 1481 in
1435 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc)) 1482 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc))
1436 end 1483 end
1437 | L.StrVar x => 1484 | L.StrVar x =>
1438 (case E.lookupStr env x of 1485 (case E.lookupStr env x of
1507 | L'.SgiVal (x, n, t) => 1554 | L'.SgiVal (x, n, t) =>
1508 ((L'.DVal (x, n, t, (L'.EModProj (basis_n, [], x), loc)), loc), 1555 ((L'.DVal (x, n, t, (L'.EModProj (basis_n, [], x), loc)), loc),
1509 E.pushENamedAs env' x n t) 1556 E.pushENamedAs env' x n t)
1510 | L'.SgiStr (x, n, sgn) => 1557 | L'.SgiStr (x, n, sgn) =>
1511 ((L'.DStr (x, n, sgn, (L'.StrProj ((L'.StrVar basis_n, loc), x), loc)), loc), 1558 ((L'.DStr (x, n, sgn, (L'.StrProj ((L'.StrVar basis_n, loc), x), loc)), loc),
1512 E.pushStrNamedAs env' x n sgn)) 1559 E.pushStrNamedAs env' x n sgn)
1560 | L'.SgiSgn (x, n, sgn) =>
1561 ((L'.DSgn (x, n, (L'.SgnProj (basis_n, [], x), loc)), loc),
1562 E.pushSgnNamedAs env' x n sgn))
1513 env' sgis 1563 env' sgis
1514 | _ => raise Fail "Non-constant Basis signature" 1564 | _ => raise Fail "Non-constant Basis signature"
1515 1565
1516 fun discoverC r x = 1566 fun discoverC r x =
1517 case E.lookupC env' x of 1567 case E.lookupC env' x of