Mercurial > urweb

comparison src/elaborate.sml @ 88:7bab29834cd6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Constraints in modules
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 15:58:02 -0400
parents 7f9bcc8bfa1e
children 94ef20a31550
comparison
equal deleted inserted replaced
87:275aaeb73f1f 88:7bab29834cd6
713 fun err f = raise CUnify' (f (c1All, c2All)) 713 fun err f = raise CUnify' (f (c1All, c2All))
714 714
715 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All) 715 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
716 in 716 in
717 case (c1, c2) of 717 case (c1, c2) of
718 (L'.TFun (d1, r1), L'.TFun (d2, r2)) => 718 (L'.CUnit, L'.CUnit) => []
719
720 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
719 unifyCons' (env, denv) d1 d2 721 unifyCons' (env, denv) d1 d2
720 @ unifyCons' (env, denv) r1 r2 722 @ unifyCons' (env, denv) r1 r2
721 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => 723 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
722 if expl1 <> expl2 then 724 if expl1 <> expl2 then
723 err CExplicitness 725 err CExplicitness
1135 | NotIncludable of L'.sgn 1137 | NotIncludable of L'.sgn
1136 | DuplicateCon of ErrorMsg.span * string 1138 | DuplicateCon of ErrorMsg.span * string
1137 | DuplicateVal of ErrorMsg.span * string 1139 | DuplicateVal of ErrorMsg.span * string
1138 | DuplicateSgn of ErrorMsg.span * string 1140 | DuplicateSgn of ErrorMsg.span * string
1139 | DuplicateStr of ErrorMsg.span * string 1141 | DuplicateStr of ErrorMsg.span * string
1142 | NotConstraintsable of L'.sgn
1140 1143
1141 fun sgnError env err = 1144 fun sgnError env err =
1142 case err of 1145 case err of
1143 UnboundSgn (loc, s) => 1146 UnboundSgn (loc, s) =>
1144 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s) 1147 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
1181 ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature") 1184 ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
1182 | DuplicateSgn (loc, s) => 1185 | DuplicateSgn (loc, s) =>
1183 ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature") 1186 ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
1184 | DuplicateStr (loc, s) => 1187 | DuplicateStr (loc, s) =>
1185 ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature") 1188 ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
1189 | NotConstraintsable sgn =>
1190 (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
1191 eprefaces' [("Signature", p_sgn env sgn)])
1186 1192
1187 datatype str_error = 1193 datatype str_error =
1188 UnboundStr of ErrorMsg.span * string 1194 UnboundStr of ErrorMsg.span * string
1189 | NotFunctor of L'.sgn 1195 | NotFunctor of L'.sgn
1190 | FunctorRebind of ErrorMsg.span 1196 | FunctorRebind of ErrorMsg.span
1210 ("Subkind 2", p_kind k2)]; 1216 ("Subkind 2", p_kind k2)];
1211 kunifyError ue) 1217 kunifyError ue)
1212 1218
1213 val hnormSgn = E.hnormSgn 1219 val hnormSgn = E.hnormSgn
1214 1220
1215 fun elabSgn_item denv ((sgi, loc), (env, gs)) = 1221 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
1216 case sgi of 1222 case sgi of
1217 L.SgiConAbs (x, k) => 1223 L.SgiConAbs (x, k) =>
1218 let 1224 let
1219 val k' = elabKind k 1225 val k' = elabKind k
1220 1226
1221 val (env', n) = E.pushCNamed env x k' NONE 1227 val (env', n) = E.pushCNamed env x k' NONE
1222 in 1228 in
1223 ([(L'.SgiConAbs (x, n, k'), loc)], (env', gs)) 1229 ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs))
1224 end 1230 end
1225 1231
1226 | L.SgiCon (x, ko, c) => 1232 | L.SgiCon (x, ko, c) =>
1227 let 1233 let
1228 val k' = case ko of 1234 val k' = case ko of
1232 val (c', ck, gs') = elabCon (env, denv) c 1238 val (c', ck, gs') = elabCon (env, denv) c
1233 val (env', n) = E.pushCNamed env x k' (SOME c') 1239 val (env', n) = E.pushCNamed env x k' (SOME c')
1234 in 1240 in
1235 checkKind env c' ck k'; 1241 checkKind env c' ck k';
1236 1242
1237 ([(L'.SgiCon (x, n, k', c'), loc)], (env', gs' @ gs)) 1243 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
1238 end 1244 end
1239 1245
1240 | L.SgiVal (x, c) => 1246 | L.SgiVal (x, c) =>
1241 let 1247 let
1242 val (c', ck, gs') = elabCon (env, denv) c 1248 val (c', ck, gs') = elabCon (env, denv) c
1244 val (env', n) = E.pushENamed env x c' 1250 val (env', n) = E.pushENamed env x c'
1245 in 1251 in
1246 (unifyKinds ck ktype 1252 (unifyKinds ck ktype
1247 handle KUnify ue => strError env (NotType (ck, ue))); 1253 handle KUnify ue => strError env (NotType (ck, ue)));
1248 1254
1249 ([(L'.SgiVal (x, n, c'), loc)], (env', gs' @ gs)) 1255 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
1250 end 1256 end
1251 1257
1252 | L.SgiStr (x, sgn) => 1258 | L.SgiStr (x, sgn) =>
1253 let 1259 let
1254 val (sgn', gs') = elabSgn (env, denv) sgn 1260 val (sgn', gs') = elabSgn (env, denv) sgn
1255 val (env', n) = E.pushStrNamed env x sgn' 1261 val (env', n) = E.pushStrNamed env x sgn'
1256 in 1262 in
1257 ([(L'.SgiStr (x, n, sgn'), loc)], (env', gs' @ gs)) 1263 ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
1258 end 1264 end
1259 1265
1260 | L.SgiSgn (x, sgn) => 1266 | L.SgiSgn (x, sgn) =>
1261 let 1267 let
1262 val (sgn', gs') = elabSgn (env, denv) sgn 1268 val (sgn', gs') = elabSgn (env, denv) sgn
1263 val (env', n) = E.pushSgnNamed env x sgn' 1269 val (env', n) = E.pushSgnNamed env x sgn'
1264 in 1270 in
1265 ([(L'.SgiSgn (x, n, sgn'), loc)], (env', gs' @ gs)) 1271 ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
1266 end 1272 end
1267 1273
1268 | L.SgiInclude sgn => 1274 | L.SgiInclude sgn =>
1269 let 1275 let
1270 val (sgn', gs') = elabSgn (env, denv) sgn 1276 val (sgn', gs') = elabSgn (env, denv) sgn
1271 in 1277 in
1272 case #1 (hnormSgn env sgn') of 1278 case #1 (hnormSgn env sgn') of
1273 L'.SgnConst sgis => 1279 L'.SgnConst sgis =>
1274 (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, gs' @ gs)) 1280 (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs))
1275 | _ => (sgnError env (NotIncludable sgn'); 1281 | _ => (sgnError env (NotIncludable sgn');
1276 ([], (env, []))) 1282 ([], (env, denv, [])))
1283 end
1284
1285 | L.SgiConstraint (c1, c2) =>
1286 let
1287 val (c1', k1, gs1) = elabCon (env, denv) c1
1288 val (c2', k2, gs2) = elabCon (env, denv) c2
1289
1290 val denv = D.assert env denv (c1', c2')
1291 in
1292 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
1293 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
1294
1295 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2))
1277 end 1296 end
1278 1297
1279 and elabSgn (env, denv) (sgn, loc) = 1298 and elabSgn (env, denv) (sgn, loc) =
1280 case sgn of 1299 case sgn of
1281 L.SgnConst sgis => 1300 L.SgnConst sgis =>
1282 let 1301 let
1283 val (sgis', (_, gs)) = ListUtil.foldlMapConcat (elabSgn_item denv) (env, []) sgis 1302 val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis
1284 1303
1285 val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) => 1304 val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) =>
1286 case sgi of 1305 case sgi of
1287 L'.SgiConAbs (x, _, _) => 1306 L'.SgiConAbs (x, _, _) =>
1288 (if SS.member (cons, x) then 1307 (if SS.member (cons, x) then
1311 | L'.SgiStr (x, _, _) => 1330 | L'.SgiStr (x, _, _) =>
1312 (if SS.member (strs, x) then 1331 (if SS.member (strs, x) then
1313 sgnError env (DuplicateStr (loc, x)) 1332 sgnError env (DuplicateStr (loc, x))
1314 else 1333 else
1315 (); 1334 ();
1316 (cons, vals, sgns, SS.add (strs, x)))) 1335 (cons, vals, sgns, SS.add (strs, x)))
1336 | L'.SgiConstraint _ => (cons, vals, sgns, strs))
1317 (SS.empty, SS.empty, SS.empty, SS.empty) sgis' 1337 (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
1318 in 1338 in
1319 ((L'.SgnConst sgis', loc), gs) 1339 ((L'.SgnConst sgis', loc), gs)
1320 end 1340 end
1321 | L.SgnVar x => 1341 | L.SgnVar x =>
1408 case self str of 1428 case self str of
1409 NONE => sgn 1429 NONE => sgn
1410 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} 1430 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
1411 end 1431 end
1412 1432
1413 fun dopen env {str, strs, sgn} = 1433 fun dopen (env, denv) {str, strs, sgn} =
1414 let 1434 let
1415 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) 1435 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
1416 (L'.StrVar str, #2 sgn) strs 1436 (L'.StrVar str, #2 sgn) strs
1417 in 1437 in
1418 case #1 (hnormSgn env sgn) of 1438 case #1 (hnormSgn env sgn) of
1419 L'.SgnConst sgis => 1439 L'.SgnConst sgis =>
1420 ListUtil.foldlMap (fn ((sgi, loc), env') => 1440 ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) =>
1421 case sgi of 1441 case sgi of
1422 L'.SgiConAbs (x, n, k) => 1442 L'.SgiConAbs (x, n, k) =>
1423 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc), 1443 let
1424 E.pushCNamedAs env' x n k NONE) 1444 val c = (L'.CModProj (str, strs, x), loc)
1445 in
1446 ((L'.DCon (x, n, k, c), loc),
1447 (E.pushCNamedAs env' x n k (SOME c), denv'))
1448 end
1425 | L'.SgiCon (x, n, k, c) => 1449 | L'.SgiCon (x, n, k, c) =>
1426 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc), 1450 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
1427 E.pushCNamedAs env' x n k (SOME c)) 1451 (E.pushCNamedAs env' x n k (SOME c), denv'))
1428 | L'.SgiVal (x, n, t) => 1452 | L'.SgiVal (x, n, t) =>
1429 ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc), 1453 ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc),
1430 E.pushENamedAs env' x n t) 1454 (E.pushENamedAs env' x n t, denv'))
1431 | L'.SgiStr (x, n, sgn) => 1455 | L'.SgiStr (x, n, sgn) =>
1432 ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc), 1456 ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc),
1433 E.pushStrNamedAs env' x n sgn) 1457 (E.pushStrNamedAs env' x n sgn, denv'))
1434 | L'.SgiSgn (x, n, sgn) => 1458 | L'.SgiSgn (x, n, sgn) =>
1435 ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc), 1459 ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc),
1436 E.pushSgnNamedAs env' x n sgn)) 1460 (E.pushSgnNamedAs env' x n sgn, denv'))
1437 env sgis 1461 | L'.SgiConstraint (c1, c2) =>
1462 ((L'.DConstraint (c1, c2), loc),
1463 (env', denv (* D.assert env denv (c1, c2) *) )))
1464 (env, denv) sgis
1438 | _ => (strError env (UnOpenable sgn); 1465 | _ => (strError env (UnOpenable sgn);
1439 ([], env)) 1466 ([], (env, denv)))
1440 end 1467 end
1468
1469 fun dopenConstraints (loc, env, denv) {str, strs} =
1470 case E.lookupStr env str of
1471 NONE => (strError env (UnboundStr (loc, str));
1472 denv)
1473 | SOME (n, sgn) =>
1474 let
1475 val (st, sgn) = foldl (fn (m, (str, sgn)) =>
1476 case E.projectStr env {str = str, sgn = sgn, field = m} of
1477 NONE => (strError env (UnboundStr (loc, m));
1478 (strerror, sgnerror))
1479 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1480 ((L'.StrVar n, loc), sgn) strs
1481
1482 val cso = E.projectConstraints env {sgn = sgn, str = st}
1483
1484 val denv = case cso of
1485 NONE => (strError env (UnboundStr (loc, str));
1486 denv)
1487 | SOME cs => foldl (fn ((c1, c2), denv) => D.assert env denv (c1, c2)) denv cs
1488 in
1489 denv
1490 end
1441 1491
1442 fun sgiOfDecl (d, loc) = 1492 fun sgiOfDecl (d, loc) =
1443 case d of 1493 case d of
1444 L'.DCon (x, n, k, c) => (L'.SgiCon (x, n, k, c), loc) 1494 L'.DCon (x, n, k, c) => (L'.SgiCon (x, n, k, c), loc)
1445 | L'.DVal (x, n, t, _) => (L'.SgiVal (x, n, t), loc) 1495 | L'.DVal (x, n, t, _) => (L'.SgiVal (x, n, t), loc)
1446 | L'.DSgn (x, n, sgn) => (L'.SgiSgn (x, n, sgn), loc) 1496 | L'.DSgn (x, n, sgn) => (L'.SgiSgn (x, n, sgn), loc)
1447 | L'.DStr (x, n, sgn, _) => (L'.SgiStr (x, n, sgn), loc) 1497 | L'.DStr (x, n, sgn, _) => (L'.SgiStr (x, n, sgn), loc)
1448 | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc) 1498 | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc)
1499 | L'.DConstraint cs => (L'.SgiConstraint cs, loc)
1500
1501 fun sgiBindsD (env, denv) (sgi, _) =
1502 case sgi of
1503 L'.SgiConstraint (c1, c2) => D.assert env denv (c1, c2)
1504 | _ => denv
1449 1505
1450 fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = 1506 fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
1451 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of 1507 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
1452 (L'.SgnError, _) => () 1508 (L'.SgnError, _) => ()
1453 | (_, L'.SgnError) => () 1509 | (_, L'.SgnError) => ()
1454 1510
1455 | (L'.SgnConst sgis1, L'.SgnConst sgis2) => 1511 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
1456 let 1512 let
1457 fun folder (sgi2All as (sgi, _), env) = 1513 fun folder (sgi2All as (sgi, _), (env, denv)) =
1458 let 1514 let
1459 fun seek p = 1515 fun seek p =
1460 let 1516 let
1461 fun seek env ls = 1517 fun seek (env, denv) ls =
1462 case ls of 1518 case ls of
1463 [] => (sgnError env (UnmatchedSgi sgi2All); 1519 [] => (sgnError env (UnmatchedSgi sgi2All);
1464 env) 1520 (env, denv))
1465 | h :: t => 1521 | h :: t =>
1466 case p h of 1522 case p h of
1467 NONE => seek (E.sgiBinds env h) t 1523 NONE => seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t
1468 | SOME env => env 1524 | SOME envs => envs
1469 in 1525 in
1470 seek env sgis1 1526 seek (env, denv) sgis1
1471 end 1527 end
1472 in 1528 in
1473 case sgi of 1529 case sgi of
1474 L'.SgiConAbs (x, n2, k2) => 1530 L'.SgiConAbs (x, n2, k2) =>
1475 seek (fn sgi1All as (sgi1, _) => 1531 seek (fn sgi1All as (sgi1, _) =>
1483 val env = E.pushCNamedAs env x n1 k1 co1 1539 val env = E.pushCNamedAs env x n1 k1 co1
1484 in 1540 in
1485 SOME (if n1 = n2 then 1541 SOME (if n1 = n2 then
1486 env 1542 env
1487 else 1543 else
1488 E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2))) 1544 E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)),
1545 denv)
1489 end 1546 end
1490 else 1547 else
1491 NONE 1548 NONE
1492 in 1549 in
1493 case sgi1 of 1550 case sgi1 of
1500 seek (fn sgi1All as (sgi1, _) => 1557 seek (fn sgi1All as (sgi1, _) =>
1501 case sgi1 of 1558 case sgi1 of
1502 L'.SgiCon (x', n1, k1, c1) => 1559 L'.SgiCon (x', n1, k1, c1) =>
1503 if x = x' then 1560 if x = x' then
1504 let 1561 let
1505 fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2)) 1562 fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv)
1506 in 1563 in
1507 (case unifyCons (env, denv) c1 c2 of 1564 (case unifyCons (env, denv) c1 c2 of
1508 [] => good () 1565 [] => good ()
1509 | _ => NONE) 1566 | _ => NONE)
1510 handle CUnify (c1, c2, err) => 1567 handle CUnify (c1, c2, err) =>
1519 seek (fn sgi1All as (sgi1, _) => 1576 seek (fn sgi1All as (sgi1, _) =>
1520 case sgi1 of 1577 case sgi1 of
1521 L'.SgiVal (x', n1, c1) => 1578 L'.SgiVal (x', n1, c1) =>
1522 if x = x' then 1579 if x = x' then
1523 (case unifyCons (env, denv) c1 c2 of 1580 (case unifyCons (env, denv) c1 c2 of
1524 [] => SOME env 1581 [] => SOME (env, denv)
1525 | _ => NONE) 1582 | _ => NONE)
1526 handle CUnify (c1, c2, err) => 1583 handle CUnify (c1, c2, err) =>
1527 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 1584 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
1528 SOME env) 1585 SOME (env, denv))
1529 else 1586 else
1530 NONE 1587 NONE
1531 | _ => NONE) 1588 | _ => NONE)
1532 1589
1533 | L'.SgiStr (x, n2, sgn2) => 1590 | L'.SgiStr (x, n2, sgn2) =>
1543 else 1600 else
1544 E.pushStrNamedAs env x n2 1601 E.pushStrNamedAs env x n2
1545 (selfifyAt env {str = (L'.StrVar n1, #2 sgn2), 1602 (selfifyAt env {str = (L'.StrVar n1, #2 sgn2),
1546 sgn = sgn2}) 1603 sgn = sgn2})
1547 in 1604 in
1548 SOME env 1605 SOME (env, denv)
1549 end 1606 end
1550 else 1607 else
1551 NONE 1608 NONE
1552 | _ => NONE) 1609 | _ => NONE)
1553 1610
1564 val env = if n1 = n2 then 1621 val env = if n1 = n2 then
1565 env 1622 env
1566 else 1623 else
1567 E.pushSgnNamedAs env x n1 sgn2 1624 E.pushSgnNamedAs env x n1 sgn2
1568 in 1625 in
1569 SOME env 1626 SOME (env, denv)
1570 end 1627 end
1571 else 1628 else
1572 NONE 1629 NONE
1573 | _ => NONE) 1630 | _ => NONE)
1631
1632 | L'.SgiConstraint (c2, d2) =>
1633 seek (fn sgi1All as (sgi1, _) =>
1634 case sgi1 of
1635 L'.SgiConstraint (c1, d1) =>
1636 if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then
1637 SOME (env, D.assert env denv (c2, d2))
1638 else
1639 NONE
1640 | _ => NONE)
1574 end 1641 end
1575 in 1642 in
1576 ignore (foldl folder env sgis2) 1643 ignore (foldl folder (env, denv) sgis2)
1577 end 1644 end
1578 1645
1579 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => 1646 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) =>
1580 let 1647 let
1581 val ran1 = 1648 val ran1 =
1589 end 1656 end
1590 1657
1591 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) 1658 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
1592 1659
1593 1660
1594 fun elabDecl denv ((d, loc), (env, gs)) = 1661 fun elabDecl ((d, loc), (env, denv, gs)) =
1595 case d of 1662 case d of
1596 L.DCon (x, ko, c) => 1663 L.DCon (x, ko, c) =>
1597 let 1664 let
1598 val k' = case ko of 1665 val k' = case ko of
1599 NONE => kunif loc 1666 NONE => kunif loc
1602 val (c', ck, gs') = elabCon (env, denv) c 1669 val (c', ck, gs') = elabCon (env, denv) c
1603 val (env', n) = E.pushCNamed env x k' (SOME c') 1670 val (env', n) = E.pushCNamed env x k' (SOME c')
1604 in 1671 in
1605 checkKind env c' ck k'; 1672 checkKind env c' ck k';
1606 1673
1607 ([(L'.DCon (x, n, k', c'), loc)], (env', gs' @ gs)) 1674 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
1608 end 1675 end
1609 | L.DVal (x, co, e) => 1676 | L.DVal (x, co, e) =>
1610 let 1677 let
1611 val (c', ck, gs1) = case co of 1678 val (c', ck, gs1) = case co of
1612 NONE => (cunif (loc, ktype), ktype, []) 1679 NONE => (cunif (loc, ktype), ktype, [])
1615 val (e', et, gs2) = elabExp (env, denv) e 1682 val (e', et, gs2) = elabExp (env, denv) e
1616 val (env', n) = E.pushENamed env x c' 1683 val (env', n) = E.pushENamed env x c'
1617 1684
1618 val gs3 = checkCon (env, denv) e' et c' 1685 val gs3 = checkCon (env, denv) e' et c'
1619 in 1686 in
1620 ([(L'.DVal (x, n, c', e'), loc)], (env', gs1 @ gs2 @ gs3 @ gs)) 1687 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs))
1621 end 1688 end
1622 1689
1623 | L.DSgn (x, sgn) => 1690 | L.DSgn (x, sgn) =>
1624 let 1691 let
1625 val (sgn', gs') = elabSgn (env, denv) sgn 1692 val (sgn', gs') = elabSgn (env, denv) sgn
1626 val (env', n) = E.pushSgnNamed env x sgn' 1693 val (env', n) = E.pushSgnNamed env x sgn'
1627 in 1694 in
1628 ([(L'.DSgn (x, n, sgn'), loc)], (env', gs' @ gs)) 1695 ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
1629 end 1696 end
1630 1697
1631 | L.DStr (x, sgno, str) => 1698 | L.DStr (x, sgno, str) =>
1632 let 1699 let
1633 val formal = Option.map (elabSgn (env, denv)) sgno 1700 val formal = Option.map (elabSgn (env, denv)) sgno
1689 (case #1 str' of 1756 (case #1 str' of
1690 L'.StrFun _ => () 1757 L'.StrFun _ => ()
1691 | _ => strError env (FunctorRebind loc)) 1758 | _ => strError env (FunctorRebind loc))
1692 | _ => (); 1759 | _ => ();
1693 1760
1694 ([(L'.DStr (x, n, sgn', str'), loc)], (env', gs' @ gs)) 1761 ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs))
1695 end 1762 end
1696 1763
1697 | L.DFfiStr (x, sgn) => 1764 | L.DFfiStr (x, sgn) =>
1698 let 1765 let
1699 val (sgn', gs') = elabSgn (env, denv) sgn 1766 val (sgn', gs') = elabSgn (env, denv) sgn
1700 1767
1701 val (env', n) = E.pushStrNamed env x sgn' 1768 val (env', n) = E.pushStrNamed env x sgn'
1702 in 1769 in
1703 ([(L'.DFfiStr (x, n, sgn'), loc)], (env', gs' @ gs)) 1770 ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
1704 end 1771 end
1705 1772
1706 | L.DOpen (m, ms) => 1773 | L.DOpen (m, ms) =>
1707 case E.lookupStr env m of 1774 (case E.lookupStr env m of
1708 NONE => (strError env (UnboundStr (loc, m)); 1775 NONE => (strError env (UnboundStr (loc, m));
1709 ([], (env, []))) 1776 ([], (env, denv, [])))
1710 | SOME (n, sgn) => 1777 | SOME (n, sgn) =>
1711 let 1778 let
1712 val (_, sgn) = foldl (fn (m, (str, sgn)) => 1779 val (_, sgn) = foldl (fn (m, (str, sgn)) =>
1713 case E.projectStr env {str = str, sgn = sgn, field = m} of 1780 case E.projectStr env {str = str, sgn = sgn, field = m} of
1714 NONE => (strError env (UnboundStr (loc, m)); 1781 NONE => (strError env (UnboundStr (loc, m));
1715 (strerror, sgnerror)) 1782 (strerror, sgnerror))
1716 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 1783 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1717 ((L'.StrVar n, loc), sgn) ms 1784 ((L'.StrVar n, loc), sgn) ms
1718 1785
1719 val (ds, env') = dopen env {str = n, strs = ms, sgn = sgn} 1786 val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn}
1720 in 1787 val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms}
1721 (ds, (env', [])) 1788 in
1722 end 1789 (ds, (env', denv', []))
1790 end)
1791
1792 | L.DConstraint (c1, c2) =>
1793 let
1794 val (c1', k1, gs1) = elabCon (env, denv) c1
1795 val (c2', k2, gs2) = elabCon (env, denv) c2
1796 val gs3 = map (fn cs => (loc, env, denv, cs)) (D.prove env denv (c1', c2', loc))
1797
1798 val denv' = D.assert env denv (c1', c2')
1799 in
1800 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
1801 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
1802
1803 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3))
1804 end
1805
1806 | L.DOpenConstraints (m, ms) =>
1807 let
1808 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
1809 in
1810 ([], (env, denv, []))
1811 end
1723 1812
1724 and elabStr (env, denv) (str, loc) = 1813 and elabStr (env, denv) (str, loc) =
1725 case str of 1814 case str of
1726 L.StrConst ds => 1815 L.StrConst ds =>
1727 let 1816 let
1728 val (ds', (env', gs)) = ListUtil.foldlMapConcat (elabDecl denv) (env, []) ds 1817 val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds
1729 val sgis = map sgiOfDecl ds' 1818 val sgis = map sgiOfDecl ds'
1730 1819
1731 val (sgis, _, _, _, _) = 1820 val (sgis, _, _, _, _) =
1732 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) => 1821 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
1733 case sgi of 1822 case sgi of
1779 (strs, "?" ^ x) 1868 (strs, "?" ^ x)
1780 else 1869 else
1781 (SS.add (strs, x), x) 1870 (SS.add (strs, x), x)
1782 in 1871 in
1783 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) 1872 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
1784 end) 1873 end
1874 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs))
1785 1875
1786 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis 1876 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
1787 in 1877 in
1788 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs) 1878 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)
1789 end 1879 end
1850 [] => () 1940 [] => ()
1851 | _ => raise Fail "Unresolved disjointness constraints in Basis" 1941 | _ => raise Fail "Unresolved disjointness constraints in Basis"
1852 1942
1853 val (env', basis_n) = E.pushStrNamed env "Basis" sgn 1943 val (env', basis_n) = E.pushStrNamed env "Basis" sgn
1854 1944
1855 val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn} 1945 val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn}
1856 1946
1857 fun discoverC r x = 1947 fun discoverC r x =
1858 case E.lookupC env' x of 1948 case E.lookupC env' x of
1859 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis") 1949 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis")
1860 | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis") 1950 | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis")
1866 1956
1867 fun elabDecl' (d, (env, gs)) = 1957 fun elabDecl' (d, (env, gs)) =
1868 let 1958 let
1869 val () = resetKunif () 1959 val () = resetKunif ()
1870 val () = resetCunif () 1960 val () = resetCunif ()
1871 val (ds, (env, gs)) = elabDecl D.empty (d, (env, gs)) 1961 val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs))
1872 in 1962 in
1873 if ErrorMsg.anyErrors () then 1963 if ErrorMsg.anyErrors () then
1874 () 1964 ()
1875 else ( 1965 else (
1876 if List.exists kunifsInDecl ds then 1966 if List.exists kunifsInDecl ds then