Mercurial > urweb

comparison src/elaborate.sml @ 61:48b6d2c3df46

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
open
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 19:34:35 -0400
parents abb2b32c19fb
children d72b89a1b150
comparison
equal deleted inserted replaced
60:8bce148070a7 61:48b6d2c3df46
1014 1014
1015 datatype str_error = 1015 datatype str_error =
1016 UnboundStr of ErrorMsg.span * string 1016 UnboundStr of ErrorMsg.span * string
1017 | NotFunctor of L'.sgn 1017 | NotFunctor of L'.sgn
1018 | FunctorRebind of ErrorMsg.span 1018 | FunctorRebind of ErrorMsg.span
1019 | UnOpenable of L'.sgn
1019 1020
1020 fun strError env err = 1021 fun strError env err =
1021 case err of 1022 case err of
1022 UnboundStr (loc, s) => 1023 UnboundStr (loc, s) =>
1023 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s) 1024 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
1024 | NotFunctor sgn => 1025 | NotFunctor sgn =>
1025 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor"; 1026 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
1026 eprefaces' [("Signature", p_sgn env sgn)]) 1027 eprefaces' [("Signature", p_sgn env sgn)])
1027 | FunctorRebind loc => 1028 | FunctorRebind loc =>
1028 ErrorMsg.errorAt loc "Attempt to rebind functor" 1029 ErrorMsg.errorAt loc "Attempt to rebind functor"
1030 | UnOpenable sgn =>
1031 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
1032 eprefaces' [("Signature", p_sgn env sgn)])
1029 1033
1030 val hnormSgn = E.hnormSgn 1034 val hnormSgn = E.hnormSgn
1031 1035
1032 fun elabSgn_item ((sgi, loc), env) = 1036 fun elabSgn_item ((sgi, loc), env) =
1033 let 1037 let
1358 case self str of 1362 case self str of
1359 NONE => sgn 1363 NONE => sgn
1360 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} 1364 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
1361 end 1365 end
1362 1366
1367 fun dopen env {str, strs, sgn} =
1368 let
1369 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
1370 (L'.StrVar str, #2 sgn) strs
1371 in
1372 case #1 (hnormSgn env sgn) of
1373 L'.SgnConst sgis =>
1374 ListUtil.foldlMap (fn ((sgi, loc), env') =>
1375 case sgi of
1376 L'.SgiConAbs (x, n, k) =>
1377 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
1378 E.pushCNamedAs env' x n k NONE)
1379 | L'.SgiCon (x, n, k, c) =>
1380 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
1381 E.pushCNamedAs env' x n k (SOME c))
1382 | L'.SgiVal (x, n, t) =>
1383 ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc),
1384 E.pushENamedAs env' x n t)
1385 | L'.SgiStr (x, n, sgn) =>
1386 ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc),
1387 E.pushStrNamedAs env' x n sgn)
1388 | L'.SgiSgn (x, n, sgn) =>
1389 ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc),
1390 E.pushSgnNamedAs env' x n sgn))
1391 env sgis
1392 | _ => (strError env (UnOpenable sgn);
1393 ([], env))
1394 end
1395
1363 fun elabDecl ((d, loc), env) = 1396 fun elabDecl ((d, loc), env) =
1364 let 1397 let
1365 1398
1366 in 1399 in
1367 resetKunif (); 1400 resetKunif ();
1390 declError env (KunifsRemainCon (loc, c')) 1423 declError env (KunifsRemainCon (loc, c'))
1391 else 1424 else
1392 () 1425 ()
1393 ); 1426 );
1394 1427
1395 ((L'.DCon (x, n, k', c'), loc), env') 1428 ([(L'.DCon (x, n, k', c'), loc)], env')
1396 end 1429 end
1397 | L.DVal (x, co, e) => 1430 | L.DVal (x, co, e) =>
1398 let 1431 let
1399 val (c', ck) = case co of 1432 val (c', ck) = case co of
1400 NONE => (cunif ktype, ktype) 1433 NONE => (cunif ktype, ktype)
1426 if cunifsInExp e' then 1459 if cunifsInExp e' then
1427 declError env (CunifsRemainExp (loc, e')) 1460 declError env (CunifsRemainExp (loc, e'))
1428 else 1461 else
1429 ()); 1462 ());
1430 1463
1431 ((L'.DVal (x, n, c', e'), loc), env') 1464 ([(L'.DVal (x, n, c', e'), loc)], env')
1432 end 1465 end
1433 1466
1434 | L.DSgn (x, sgn) => 1467 | L.DSgn (x, sgn) =>
1435 let 1468 let
1436 val sgn' = elabSgn env sgn 1469 val sgn' = elabSgn env sgn
1437 val (env', n) = E.pushSgnNamed env x sgn' 1470 val (env', n) = E.pushSgnNamed env x sgn'
1438 in 1471 in
1439 ((L'.DSgn (x, n, sgn'), loc), env') 1472 ([(L'.DSgn (x, n, sgn'), loc)], env')
1440 end 1473 end
1441 1474
1442 | L.DStr (x, sgno, str) => 1475 | L.DStr (x, sgno, str) =>
1443 let 1476 let
1444 val formal = Option.map (elabSgn env) sgno 1477 val formal = Option.map (elabSgn env) sgno
1457 (case #1 str' of 1490 (case #1 str' of
1458 L'.StrFun _ => () 1491 L'.StrFun _ => ()
1459 | _ => strError env (FunctorRebind loc)) 1492 | _ => strError env (FunctorRebind loc))
1460 | _ => (); 1493 | _ => ();
1461 1494
1462 ((L'.DStr (x, n, sgn', str'), loc), env') 1495 ([(L'.DStr (x, n, sgn', str'), loc)], env')
1463 end 1496 end
1464 1497
1465 | L.DFfiStr (x, sgn) => 1498 | L.DFfiStr (x, sgn) =>
1466 let 1499 let
1467 val sgn' = elabSgn env sgn 1500 val sgn' = elabSgn env sgn
1468 1501
1469 val (env', n) = E.pushStrNamed env x sgn' 1502 val (env', n) = E.pushStrNamed env x sgn'
1470 in 1503 in
1471 ((L'.DFfiStr (x, n, sgn'), loc), env') 1504 ([(L'.DFfiStr (x, n, sgn'), loc)], env')
1472 end 1505 end
1506
1507 | L.DOpen (m, ms) =>
1508 (case E.lookupStr env m of
1509 NONE => (strError env (UnboundStr (loc, m));
1510 ([], env))
1511 | SOME (n, sgn) =>
1512 let
1513 val (_, sgn) = foldl (fn (m, (str, sgn)) =>
1514 case E.projectStr env {str = str, sgn = sgn, field = m} of
1515 NONE => (strError env (UnboundStr (loc, m));
1516 (strerror, sgnerror))
1517 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1518 ((L'.StrVar n, loc), sgn) ms
1519 in
1520 dopen env {str = n, strs = ms, sgn = sgn}
1521 end)
1473 end 1522 end
1474 1523
1475 and elabStr env (str, loc) = 1524 and elabStr env (str, loc) =
1476 case str of 1525 case str of
1477 L.StrConst ds => 1526 L.StrConst ds =>
1478 let 1527 let
1479 val (ds', env') = ListUtil.foldlMap elabDecl env ds 1528 val (ds', env') = ListUtil.foldlMapConcat elabDecl env ds
1480 val sgis = map sgiOfDecl ds' 1529 val sgis = map sgiOfDecl ds'
1481 in 1530 in
1482 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc)) 1531 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc))
1483 end 1532 end
1484 | L.StrVar x => 1533 | L.StrVar x =>
1538 fun elabFile basis env file = 1587 fun elabFile basis env file =
1539 let 1588 let
1540 val sgn = elabSgn env (L.SgnConst basis, ErrorMsg.dummySpan) 1589 val sgn = elabSgn env (L.SgnConst basis, ErrorMsg.dummySpan)
1541 val (env', basis_n) = E.pushStrNamed env "Basis" sgn 1590 val (env', basis_n) = E.pushStrNamed env "Basis" sgn
1542 1591
1543 val (ds, env') = 1592 val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn}
1544 case #1 (hnormSgn env' sgn) of
1545 L'.SgnConst sgis =>
1546 ListUtil.foldlMap (fn ((sgi, loc), env') =>
1547 case sgi of
1548 L'.SgiConAbs (x, n, k) =>
1549 ((L'.DCon (x, n, k, (L'.CModProj (basis_n, [], x), loc)), loc),
1550 E.pushCNamedAs env' x n k NONE)
1551 | L'.SgiCon (x, n, k, c) =>
1552 ((L'.DCon (x, n, k, (L'.CModProj (basis_n, [], x), loc)), loc),
1553 E.pushCNamedAs env' x n k (SOME c))
1554 | L'.SgiVal (x, n, t) =>
1555 ((L'.DVal (x, n, t, (L'.EModProj (basis_n, [], x), loc)), loc),
1556 E.pushENamedAs env' x n t)
1557 | L'.SgiStr (x, n, sgn) =>
1558 ((L'.DStr (x, n, sgn, (L'.StrProj ((L'.StrVar basis_n, loc), x), loc)), loc),
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))
1563 env' sgis
1564 | _ => raise Fail "Non-constant Basis signature"
1565 1593
1566 fun discoverC r x = 1594 fun discoverC r x =
1567 case E.lookupC env' x of 1595 case E.lookupC env' x of
1568 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis") 1596 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis")
1569 | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis") 1597 | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis")
1571 1599
1572 val () = discoverC int "int" 1600 val () = discoverC int "int"
1573 val () = discoverC float "float" 1601 val () = discoverC float "float"
1574 val () = discoverC string "string" 1602 val () = discoverC string "string"
1575 1603
1576 val (file, _) = ListUtil.foldlMap elabDecl env' file 1604 val (file, _) = ListUtil.foldlMapConcat elabDecl env' file
1577 in 1605 in
1578 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file 1606 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
1579 end 1607 end
1580 1608
1581 end 1609 end