Mercurial > urweb

comparison src/elaborate.sml @ 629:e68de2a5506b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Top.Fold.concat elaborates
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 13:46:08 -0500
parents 12b73f3c108e
children 6c4643880df5
comparison
equal deleted inserted replaced
628:12b73f3c108e 629:e68de2a5506b
1023 Disjoint of D.goal 1023 Disjoint of D.goal
1024 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span 1024 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
1025 1025
1026 val enD = map Disjoint 1026 val enD = map Disjoint
1027 1027
1028 fun elabHead env infer (e as (_, loc)) t = 1028 fun elabHead (env, denv) infer (e as (_, loc)) t =
1029 let 1029 let
1030 fun unravel (t, e) = 1030 fun unravel (t, e) =
1031 case hnormCon env t of 1031 case hnormCon env t of
1032 (L'.TKFun (x, t'), _) => 1032 (L'.TKFun (x, t'), _) =>
1033 let 1033 let
1057 (e, t, TypeClass (env, dom, r, loc) :: gs) 1057 (e, t, TypeClass (env, dom, r, loc) :: gs)
1058 end 1058 end
1059 else 1059 else
1060 (e, t, []) 1060 (e, t, [])
1061 end 1061 end
1062 | (L'.TDisjoint (r1, r2, t'), loc) =>
1063 if infer <> L.TypesOnly then
1064 let
1065 val gs = D.prove env denv (r1, r2, loc)
1066 val (e, t, gs') = unravel (t', e)
1067 in
1068 (e, t, enD gs @ gs')
1069 end
1070 else
1071 (e, t, [])
1062 | t => (e, t, []) 1072 | t => (e, t, [])
1063 in 1073 in
1064 case infer of 1074 case infer of
1065 L.DontInfer => (e, t, []) 1075 L.DontInfer => (e, t, [])
1066 | _ => unravel (t, e) 1076 | _ => unravel (t, e)
1183 Wild => "Wild" 1193 Wild => "Wild"
1184 | None => "None" 1194 | None => "None"
1185 | Datatype _ => "Datatype" 1195 | Datatype _ => "Datatype"
1186 | Record _ => "Record" 1196 | Record _ => "Record"
1187 1197
1188 fun exhaustive (env, t, ps) = 1198 fun exhaustive (env, t, ps, loc) =
1189 let 1199 let
1190 fun depth (p, _) = 1200 fun depth (p, _) =
1191 case p of 1201 case p of
1192 L'.PWild => 0 1202 L'.PWild => 0
1193 | L'.PVar _ => 0 1203 | L'.PVar _ => 0
1362 NONE => raise Fail "isTotal: Can't project datatype" 1372 NONE => raise Fail "isTotal: Can't project datatype"
1363 | SOME (_, cons) => dtype cons 1373 | SOME (_, cons) => dtype cons
1364 end 1374 end
1365 | L'.CError => true 1375 | L'.CError => true
1366 | c => 1376 | c =>
1367 (prefaces "Not a datatype" [("c", p_con env (c, ErrorMsg.dummySpan))]; 1377 (prefaces "Not a datatype" [("loc", PD.string (ErrorMsg.spanToString loc)),
1378 ("c", p_con env (c, ErrorMsg.dummySpan))];
1368 raise Fail "isTotal: Not a datatype") 1379 raise Fail "isTotal: Not a datatype")
1369 end 1380 end
1370 | Record _ => List.all (fn c2 => coverageImp (c, c2)) (enumerateCases depth t) 1381 | Record _ => List.all (fn c2 => coverageImp (c, c2)) (enumerateCases depth t)
1371 in 1382 in
1372 isTotal (combinedCoverage ps, t) 1383 isTotal (combinedCoverage ps, t)
1435 | L.EVar ([], s, infer) => 1446 | L.EVar ([], s, infer) =>
1436 (case E.lookupE env s of 1447 (case E.lookupE env s of
1437 E.NotBound => 1448 E.NotBound =>
1438 (expError env (UnboundExp (loc, s)); 1449 (expError env (UnboundExp (loc, s));
1439 (eerror, cerror, [])) 1450 (eerror, cerror, []))
1440 | E.Rel (n, t) => elabHead env infer (L'.ERel n, loc) t 1451 | E.Rel (n, t) => elabHead (env, denv) infer (L'.ERel n, loc) t
1441 | E.Named (n, t) => elabHead env infer (L'.ENamed n, loc) t) 1452 | E.Named (n, t) => elabHead (env, denv) infer (L'.ENamed n, loc) t)
1442 | L.EVar (m1 :: ms, s, infer) => 1453 | L.EVar (m1 :: ms, s, infer) =>
1443 (case E.lookupStr env m1 of 1454 (case E.lookupStr env m1 of
1444 NONE => (expError env (UnboundStrInExp (loc, m1)); 1455 NONE => (expError env (UnboundStrInExp (loc, m1));
1445 (eerror, cerror, [])) 1456 (eerror, cerror, []))
1446 | SOME (n, sgn) => 1457 | SOME (n, sgn) =>
1455 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of 1466 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
1456 NONE => (expError env (UnboundExp (loc, s)); 1467 NONE => (expError env (UnboundExp (loc, s));
1457 cerror) 1468 cerror)
1458 | SOME t => t 1469 | SOME t => t
1459 in 1470 in
1460 elabHead env infer (L'.EModProj (n, ms, s), loc) t 1471 elabHead (env, denv) infer (L'.EModProj (n, ms, s), loc) t
1461 end) 1472 end)
1462 1473
1463 | L.EWild => 1474 | L.EWild =>
1464 let 1475 let
1465 val r = ref NONE 1476 val r = ref NONE
1564 checkKind env c1' k1 (L'.KRecord ku1, loc); 1575 checkKind env c1' k1 (L'.KRecord ku1, loc);
1565 checkKind env c2' k2 (L'.KRecord ku2, loc); 1576 checkKind env c2' k2 (L'.KRecord ku2, loc);
1566 1577
1567 (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ gs3) 1578 (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ gs3)
1568 end 1579 end
1580 | L.EDisjointApp e =>
1581 let
1582 val (e', t, gs1) = elabExp (env, denv) e
1583
1584 val k1 = kunif loc
1585 val c1 = cunif (loc, (L'.KRecord k1, loc))
1586 val k2 = kunif loc
1587 val c2 = cunif (loc, (L'.KRecord k2, loc))
1588 val t' = cunif (loc, ktype)
1589 val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc)
1590 val gs2 = D.prove env denv (c1, c2, loc)
1591 in
1592 (e', t', enD gs2 @ gs1)
1593 end
1569 1594
1570 | L.ERecord xes => 1595 | L.ERecord xes =>
1571 let 1596 let
1572 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) => 1597 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
1573 let 1598 let
1615 val (c', ck, gs2) = elabCon (env, denv) c 1640 val (c', ck, gs2) = elabCon (env, denv) c
1616 1641
1617 val ft = cunif (loc, ktype) 1642 val ft = cunif (loc, ktype)
1618 val rest = cunif (loc, ktype_record) 1643 val rest = cunif (loc, ktype_record)
1619 val first = (L'.CRecord (ktype, [(c', ft)]), loc) 1644 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
1620 1645 val () = checkCon env e' et
1646 (L'.TRecord (L'.CConcat (first, rest), loc), loc);
1621 val gs3 = D.prove env denv (first, rest, loc) 1647 val gs3 = D.prove env denv (first, rest, loc)
1622 in 1648 in
1623 checkCon env e' et
1624 (L'.TRecord (L'.CConcat (first, rest), loc), loc);
1625 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3) 1649 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3)
1626 end 1650 end
1627 1651
1628 | L.EConcat (e1, e2) => 1652 | L.EConcat (e1, e2) =>
1629 let 1653 let
1631 val (e2', e2t, gs2) = elabExp (env, denv) e2 1655 val (e2', e2t, gs2) = elabExp (env, denv) e2
1632 1656
1633 val r1 = cunif (loc, ktype_record) 1657 val r1 = cunif (loc, ktype_record)
1634 val r2 = cunif (loc, ktype_record) 1658 val r2 = cunif (loc, ktype_record)
1635 1659
1660 val () = checkCon env e1' e1t (L'.TRecord r1, loc)
1661 val () = checkCon env e2' e2t (L'.TRecord r2, loc)
1662
1636 val gs3 = D.prove env denv (r1, r2, loc) 1663 val gs3 = D.prove env denv (r1, r2, loc)
1637 in 1664 in
1638 checkCon env e1' e1t (L'.TRecord r1, loc);
1639 checkCon env e2' e2t (L'.TRecord r2, loc);
1640 ((L'.EConcat (e1', r1, e2', r2), loc), 1665 ((L'.EConcat (e1', r1, e2', r2), loc),
1641 (L'.TRecord ((L'.CConcat (r1, r2), loc)), loc), 1666 (L'.TRecord ((L'.CConcat (r1, r2), loc)), loc),
1642 gs1 @ gs2 @ enD gs3) 1667 gs1 @ gs2 @ enD gs3)
1643 end 1668 end
1644 | L.ECut (e, c) => 1669 | L.ECut (e, c) =>
1647 val (c', ck, gs2) = elabCon (env, denv) c 1672 val (c', ck, gs2) = elabCon (env, denv) c
1648 1673
1649 val ft = cunif (loc, ktype) 1674 val ft = cunif (loc, ktype)
1650 val rest = cunif (loc, ktype_record) 1675 val rest = cunif (loc, ktype_record)
1651 val first = (L'.CRecord (ktype, [(c', ft)]), loc) 1676 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
1677
1678 val () = checkCon env e' et
1679 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
1652 1680
1653 val gs3 = D.prove env denv (first, rest, loc) 1681 val gs3 = D.prove env denv (first, rest, loc)
1654 in 1682 in
1655 checkCon env e' et
1656 (L'.TRecord (L'.CConcat (first, rest), loc), loc);
1657 ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), 1683 ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc),
1658 gs1 @ enD gs2 @ enD gs3) 1684 gs1 @ enD gs2 @ enD gs3)
1659 end 1685 end
1660 | L.ECutMulti (e, c) => 1686 | L.ECutMulti (e, c) =>
1661 let 1687 let
1662 val (e', et, gs1) = elabExp (env, denv) e 1688 val (e', et, gs1) = elabExp (env, denv) e
1663 val (c', ck, gs2) = elabCon (env, denv) c 1689 val (c', ck, gs2) = elabCon (env, denv) c
1664 1690
1665 val rest = cunif (loc, ktype_record) 1691 val rest = cunif (loc, ktype_record)
1692
1693 val () = checkCon env e' et
1694 (L'.TRecord (L'.CConcat (c', rest), loc), loc)
1666 1695
1667 val gs3 = D.prove env denv (c', rest, loc) 1696 val gs3 = D.prove env denv (c', rest, loc)
1668 in 1697 in
1669 checkCon env e' et
1670 (L'.TRecord (L'.CConcat (c', rest), loc), loc);
1671 ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc), 1698 ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc),
1672 gs1 @ enD gs2 @ enD gs3) 1699 gs1 @ enD gs2 @ enD gs3)
1673 end 1700 end
1674 1701
1675 | L.ECase (e, pes) => 1702 | L.ECase (e, pes) =>
1679 val (pes', gs) = ListUtil.foldlMap 1706 val (pes', gs) = ListUtil.foldlMap
1680 (fn ((p, e), gs) => 1707 (fn ((p, e), gs) =>
1681 let 1708 let
1682 val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty)) 1709 val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty))
1683 1710
1684 val (e', et, gs1) = elabExp (env, denv) e 1711 val (e', et', gs1) = elabExp (env, denv) e
1685 in 1712 in
1686 checkPatCon env p' pt et; 1713 checkPatCon env p' pt et;
1687 checkCon env e' et result; 1714 checkCon env e' et' result;
1688 ((p', e'), gs1 @ gs) 1715 ((p', e'), gs1 @ gs)
1689 end) 1716 end)
1690 gs1 pes 1717 gs1 pes
1691 in 1718 in
1692 if exhaustive (env, et, map #1 pes') then 1719 if exhaustive (env, et, map #1 pes', loc) then
1693 () 1720 ()
1694 else 1721 else
1695 expError env (Inexhaustive loc); 1722 expError env (Inexhaustive loc);
1696 1723
1697 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs) 1724 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs)
1720 NONE => (cunif (loc, ktype), ktype, []) 1747 NONE => (cunif (loc, ktype), ktype, [])
1721 | SOME c => elabCon (env, denv) c 1748 | SOME c => elabCon (env, denv) c
1722 1749
1723 val (e', et, gs2) = elabExp (env, denv) e 1750 val (e', et, gs2) = elabExp (env, denv) e
1724 1751
1752 val () = checkCon env e' et c'
1753
1725 val c' = normClassConstraint env c' 1754 val c' = normClassConstraint env c'
1726 val env' = E.pushERel env x c' 1755 val env' = E.pushERel env x c'
1727 in 1756 in
1728 checkCon env e' et c';
1729 ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ gs)) 1757 ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ gs))
1730 end 1758 end
1731 | L.EDValRec vis => 1759 | L.EDValRec vis =>
1732 let 1760 let
1733 fun allowable (e, _) = 1761 fun allowable (e, _) =
2956 val (c', _, gs1) = case co of 2984 val (c', _, gs1) = case co of
2957 NONE => (cunif (loc, ktype), ktype, []) 2985 NONE => (cunif (loc, ktype), ktype, [])
2958 | SOME c => elabCon (env, denv) c 2986 | SOME c => elabCon (env, denv) c
2959 2987
2960 val (e', et, gs2) = elabExp (env, denv) e 2988 val (e', et, gs2) = elabExp (env, denv) e
2989
2990 val () = checkCon env e' et c'
2991
2961 val c = normClassConstraint env c' 2992 val c = normClassConstraint env c'
2962 val (env', n) = E.pushENamed env x c' 2993 val (env', n) = E.pushENamed env x c'
2963 in 2994 in
2964 checkCon env e' et c';
2965 (*prefaces "DVal" [("x", Print.PD.string x), 2995 (*prefaces "DVal" [("x", Print.PD.string x),
2966 ("c'", p_con env c')];*) 2996 ("c'", p_con env c')];*)
2967 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ gs)) 2997 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ gs))
2968 end 2998 end
2969 | L.DValRec vis => 2999 | L.DValRec vis =>