Mercurial > urweb

comparison src/elaborate.sml @ 66:1ec5703c09c4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proper subsignaturing for sub-structures
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Jun 2008 09:09:30 -0400
parents 2adb20eebee3
children 9f89f0b00b84
comparison
equal deleted inserted replaced
65:2adb20eebee3 66:1ec5703c09c4
1244 NONE => (sgnError env (UnboundSgn (loc, x)); 1244 NONE => (sgnError env (UnboundSgn (loc, x));
1245 sgnerror) 1245 sgnerror)
1246 | SOME _ => (L'.SgnProj (n, ms, x), loc) 1246 | SOME _ => (L'.SgnProj (n, ms, x), loc)
1247 end) 1247 end)
1248 1248
1249
1250 fun selfify env {str, strs, sgn} =
1251 case #1 (hnormSgn env sgn) of
1252 L'.SgnError => sgn
1253 | L'.SgnVar _ => sgn
1254
1255 | L'.SgnConst sgis =>
1256 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
1257 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
1258 | (L'.SgiStr (x, n, sgn), loc) =>
1259 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
1260 | x => x) sgis), #2 sgn)
1261 | L'.SgnFun _ => sgn
1262 | L'.SgnWhere _ => sgn
1263 | L'.SgnProj (m, ms, x) =>
1264 case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
1265 (L'.StrVar m, #2 sgn) ms,
1266 sgn = #2 (E.lookupStrNamed env m),
1267 field = x} of
1268 NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE"
1269 | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn}
1270
1271 fun selfifyAt env {str, sgn} =
1272 let
1273 fun self (str, _) =
1274 case str of
1275 L'.StrVar x => SOME (x, [])
1276 | L'.StrProj (str, x) =>
1277 (case self str of
1278 NONE => NONE
1279 | SOME (m, ms) => SOME (m, ms @ [x]))
1280 | _ => NONE
1281 in
1282 case self str of
1283 NONE => sgn
1284 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
1285 end
1286
1287 fun dopen env {str, strs, sgn} =
1288 let
1289 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
1290 (L'.StrVar str, #2 sgn) strs
1291 in
1292 case #1 (hnormSgn env sgn) of
1293 L'.SgnConst sgis =>
1294 ListUtil.foldlMap (fn ((sgi, loc), env') =>
1295 case sgi of
1296 L'.SgiConAbs (x, n, k) =>
1297 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
1298 E.pushCNamedAs env' x n k NONE)
1299 | L'.SgiCon (x, n, k, c) =>
1300 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
1301 E.pushCNamedAs env' x n k (SOME c))
1302 | L'.SgiVal (x, n, t) =>
1303 ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc),
1304 E.pushENamedAs env' x n t)
1305 | L'.SgiStr (x, n, sgn) =>
1306 ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc),
1307 E.pushStrNamedAs env' x n sgn)
1308 | L'.SgiSgn (x, n, sgn) =>
1309 ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc),
1310 E.pushSgnNamedAs env' x n sgn))
1311 env sgis
1312 | _ => (strError env (UnOpenable sgn);
1313 ([], env))
1314 end
1249 1315
1250 fun sgiOfDecl (d, loc) = 1316 fun sgiOfDecl (d, loc) =
1251 case d of 1317 case d of
1252 L'.DCon (x, n, k, c) => (L'.SgiCon (x, n, k, c), loc) 1318 L'.DCon (x, n, k, c) => (L'.SgiCon (x, n, k, c), loc)
1253 | L'.DVal (x, n, t, _) => (L'.SgiVal (x, n, t), loc) 1319 | L'.DVal (x, n, t, _) => (L'.SgiVal (x, n, t), loc)
1339 | L'.SgiStr (x, n2, sgn2) => 1405 | L'.SgiStr (x, n2, sgn2) =>
1340 seek (fn sgi1All as (sgi1, _) => 1406 seek (fn sgi1All as (sgi1, _) =>
1341 case sgi1 of 1407 case sgi1 of
1342 L'.SgiStr (x', n1, sgn1) => 1408 L'.SgiStr (x', n1, sgn1) =>
1343 if x = x' then 1409 if x = x' then
1344 (subSgn env sgn1 sgn2; 1410 let
1345 SOME env) 1411 val () = subSgn env sgn1 sgn2
1412 val env = E.pushStrNamedAs env x n1 sgn1
1413 val env = if n1 = n2 then
1414 env
1415 else
1416 E.pushStrNamedAs env x n2
1417 (selfifyAt env {str = (L'.StrVar n1, #2 sgn2),
1418 sgn = sgn2})
1419 in
1420 SOME env
1421 end
1346 else 1422 else
1347 NONE 1423 NONE
1348 | _ => NONE) 1424 | _ => NONE)
1349 (* Add type equations between structures here some day. *)
1350 1425
1351 | L'.SgiSgn (x, n2, sgn2) => 1426 | L'.SgiSgn (x, n2, sgn2) =>
1352 seek (fn sgi1All as (sgi1, _) => 1427 seek (fn sgi1All as (sgi1, _) =>
1353 case sgi1 of 1428 case sgi1 of
1354 L'.SgiSgn (x', n1, sgn1) => 1429 L'.SgiSgn (x', n1, sgn1) =>
1385 subSgn (E.pushStrNamedAs env m2 n2 dom2) ran1 ran2 1460 subSgn (E.pushStrNamedAs env m2 n2 dom2) ran1 ran2
1386 end 1461 end
1387 1462
1388 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) 1463 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
1389 1464
1390 fun selfify env {str, strs, sgn} =
1391 case #1 (hnormSgn env sgn) of
1392 L'.SgnError => sgn
1393 | L'.SgnVar _ => sgn
1394
1395 | L'.SgnConst sgis =>
1396 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
1397 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
1398 | (L'.SgiStr (x, n, sgn), loc) =>
1399 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
1400 | x => x) sgis), #2 sgn)
1401 | L'.SgnFun _ => sgn
1402 | L'.SgnWhere _ => sgn
1403 | L'.SgnProj (m, ms, x) =>
1404 case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
1405 (L'.StrVar m, #2 sgn) ms,
1406 sgn = #2 (E.lookupStrNamed env m),
1407 field = x} of
1408 NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE"
1409 | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn}
1410
1411 fun selfifyAt env {str, sgn} =
1412 let
1413 fun self (str, _) =
1414 case str of
1415 L'.StrVar x => SOME (x, [])
1416 | L'.StrProj (str, x) =>
1417 (case self str of
1418 NONE => NONE
1419 | SOME (m, ms) => SOME (m, ms @ [x]))
1420 | _ => NONE
1421 in
1422 case self str of
1423 NONE => sgn
1424 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
1425 end
1426
1427 fun dopen env {str, strs, sgn} =
1428 let
1429 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
1430 (L'.StrVar str, #2 sgn) strs
1431 in
1432 case #1 (hnormSgn env sgn) of
1433 L'.SgnConst sgis =>
1434 ListUtil.foldlMap (fn ((sgi, loc), env') =>
1435 case sgi of
1436 L'.SgiConAbs (x, n, k) =>
1437 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
1438 E.pushCNamedAs env' x n k NONE)
1439 | L'.SgiCon (x, n, k, c) =>
1440 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
1441 E.pushCNamedAs env' x n k (SOME c))
1442 | L'.SgiVal (x, n, t) =>
1443 ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc),
1444 E.pushENamedAs env' x n t)
1445 | L'.SgiStr (x, n, sgn) =>
1446 ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc),
1447 E.pushStrNamedAs env' x n sgn)
1448 | L'.SgiSgn (x, n, sgn) =>
1449 ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc),
1450 E.pushSgnNamedAs env' x n sgn))
1451 env sgis
1452 | _ => (strError env (UnOpenable sgn);
1453 ([], env))
1454 end
1455 1465
1456 fun elabDecl ((d, loc), env) = 1466 fun elabDecl ((d, loc), env) =
1457 let 1467 let
1458 1468
1459 in 1469 in