Mercurial > urweb
comparison src/elaborate.sml @ 830:d07980bf1444
Defer pattern-matching exhaustiveness checks and normalize pattern types more thoroughly
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 30 May 2009 14:44:29 -0400 |
parents | 7f871c03e3a1 |
children | 9a1026e2b3f5 |
comparison
equal
deleted
inserted
replaced
829:20fe00fd81da | 830:d07980bf1444 |
---|---|
622 | 622 |
623 val recdCounter = ref 0 | 623 val recdCounter = ref 0 |
624 | 624 |
625 val mayDelay = ref false | 625 val mayDelay = ref false |
626 val delayedUnifs = ref ([] : (ErrorMsg.span * E.env * L'.kind * record_summary * record_summary) list) | 626 val delayedUnifs = ref ([] : (ErrorMsg.span * E.env * L'.kind * record_summary * record_summary) list) |
627 | |
628 val delayedExhaustives = ref ([] : (E.env * L'.con * L'.pat list * ErrorMsg.span) list) | |
627 | 629 |
628 fun unifyRecordCons env (loc, c1, c2) = | 630 fun unifyRecordCons env (loc, c1, c2) = |
629 let | 631 let |
630 fun rkindof c = | 632 fun rkindof c = |
631 case hnormKind (kindof env c) of | 633 case hnormKind (kindof env c) of |
1396 | q1 :: qs => | 1398 | q1 :: qs => |
1397 let | 1399 let |
1398 val loc = #2 q1 | 1400 val loc = #2 q1 |
1399 | 1401 |
1400 fun unapp (t, acc) = | 1402 fun unapp (t, acc) = |
1401 case t of | 1403 case #1 t of |
1402 L'.CApp ((t, _), arg) => unapp (t, arg :: acc) | 1404 L'.CApp (t, arg) => unapp (t, arg :: acc) |
1403 | _ => (t, rev acc) | 1405 | _ => (t, rev acc) |
1404 | 1406 |
1405 val (t1, args) = unapp (#1 (hnormCon env q1), []) | 1407 val (t1, args) = unapp (hnormCon env q1, []) |
1408 val t1 = hnormCon env t1 | |
1406 fun doSub t = foldl (fn (arg, t) => subConInCon (0, arg) t) t args | 1409 fun doSub t = foldl (fn (arg, t) => subConInCon (0, arg) t) t args |
1407 | 1410 |
1408 fun dtype (dtO, names) = | 1411 fun dtype (dtO, names) = |
1409 let | 1412 let |
1410 val nameSet = IS.addList (IS.empty, names) | 1413 val nameSet = IS.addList (IS.empty, names) |
1421 end | 1424 end |
1422 | 1425 |
1423 fun default () = (NONE, IS.singleton 0, []) | 1426 fun default () = (NONE, IS.singleton 0, []) |
1424 | 1427 |
1425 val (dtO, unused, cons) = | 1428 val (dtO, unused, cons) = |
1426 case t1 of | 1429 case #1 t1 of |
1427 L'.CNamed n => | 1430 L'.CNamed n => |
1428 let | 1431 let |
1429 val dt = E.lookupDatatype env n | 1432 val dt = E.lookupDatatype env n |
1430 val cons = E.constructors dt | 1433 val cons = E.constructors dt |
1431 in | 1434 in |
1450 (patConNum (L'.PConProj (m1, ms, s)), | 1453 (patConNum (L'.PConProj (m1, ms, s)), |
1451 case co of | 1454 case co of |
1452 NONE => [] | 1455 NONE => [] |
1453 | SOME t => [("", doSub t)])) cons) | 1456 | SOME t => [("", doSub t)])) cons) |
1454 end | 1457 end |
1455 | L'.TRecord (L'.CRecord (_, xts), _) => | 1458 | L'.TRecord t => |
1456 let | 1459 (case #1 (hnormCon env t) of |
1457 val xts = map (fn ((L'.CName x, _), co) => SOME (x, co) | 1460 L'.CRecord (_, xts) => |
1458 | _ => NONE) xts | 1461 let |
1459 in | 1462 val xts = map (fn ((L'.CName x, _), co) => SOME (x, co) |
1460 if List.all Option.isSome xts then | 1463 | _ => NONE) xts |
1461 let | 1464 in |
1462 val xts = List.mapPartial (fn x => x) xts | 1465 if List.all Option.isSome xts then |
1463 val xts = ListMergeSort.sort (fn ((x1, _), (x2, _)) => | 1466 let |
1464 String.compare (x1, x2) = GREATER) xts | 1467 val xts = List.mapPartial (fn x => x) xts |
1465 in | 1468 val xts = ListMergeSort.sort (fn ((x1, _), (x2, _)) => |
1466 (NONE, IS.empty, [(0, xts)]) | 1469 String.compare (x1, x2) = GREATER) xts |
1467 end | 1470 in |
1468 else | 1471 (NONE, IS.empty, [(0, xts)]) |
1469 default () | 1472 end |
1470 end | 1473 else |
1474 default () | |
1475 end | |
1476 | _ => default ()) | |
1471 | _ => default () | 1477 | _ => default () |
1472 in | 1478 in |
1473 if IS.isEmpty unused then | 1479 if IS.isEmpty unused then |
1474 let | 1480 let |
1475 fun recurse cons = | 1481 fun recurse cons = |
1487 | 1493 |
1488 val p = case name of | 1494 val p = case name of |
1489 0 => L'.PRecord (ListPair.map | 1495 0 => L'.PRecord (ListPair.map |
1490 (fn ((name, t), p) => (name, p, t)) | 1496 (fn ((name, t), p) => (name, p, t)) |
1491 (args, argPs)) | 1497 (args, argPs)) |
1492 | _ => L'.PCon (L'.Default, nameOfNum (t1, name), [], | 1498 | _ => L'.PCon (L'.Default, nameOfNum (#1 t1, name), [], |
1493 case argPs of | 1499 case argPs of |
1494 [] => NONE | 1500 [] => NONE |
1495 | [p] => SOME p | 1501 | [p] => SOME p |
1496 | _ => fail 3) | 1502 | _ => fail 3) |
1497 in | 1503 in |
1516 if name = name' then | 1522 if name = name' then |
1517 SOME (name', args) | 1523 SOME (name', args) |
1518 else | 1524 else |
1519 NONE) cons of | 1525 NONE) cons of |
1520 SOME (n, []) => | 1526 SOME (n, []) => |
1521 L'.PCon (L'.Default, nameOfNum (t1, n), [], NONE) | 1527 L'.PCon (L'.Default, nameOfNum (#1 t1, n), [], NONE) |
1522 | SOME (n, [_]) => | 1528 | SOME (n, [_]) => |
1523 L'.PCon (L'.Default, nameOfNum (t1, n), [], SOME (L'.PWild, loc)) | 1529 L'.PCon (L'.Default, nameOfNum (#1 t1, n), [], SOME (L'.PWild, loc)) |
1524 | _ => fail 7 | 1530 | _ => fail 7 |
1525 in | 1531 in |
1526 SOME ((p, loc) :: ps) | 1532 SOME ((p, loc) :: ps) |
1527 end | 1533 end |
1528 end | 1534 end |
1530 case I (map (fn x => [x]) ps, [t]) of | 1536 case I (map (fn x => [x]) ps, [t]) of |
1531 NONE => NONE | 1537 NONE => NONE |
1532 | SOME [p] => SOME p | 1538 | SOME [p] => SOME p |
1533 | _ => fail 7 | 1539 | _ => fail 7 |
1534 end | 1540 end |
1535 | |
1536 (*datatype coverage = | |
1537 Wild | |
1538 | None | |
1539 | Datatype of coverage IM.map | |
1540 | Record of coverage SM.map list | |
1541 | |
1542 fun c2s c = | |
1543 case c of | |
1544 Wild => "Wild" | |
1545 | None => "None" | |
1546 | Datatype _ => "Datatype" | |
1547 | Record _ => "Record" | |
1548 | |
1549 fun exhaustive (env, t, ps, loc) = | |
1550 let | |
1551 fun depth (p, _) = | |
1552 case p of | |
1553 L'.PWild => 0 | |
1554 | L'.PVar _ => 0 | |
1555 | L'.PPrim _ => 0 | |
1556 | L'.PCon (_, _, _, NONE) => 1 | |
1557 | L'.PCon (_, _, _, SOME p) => 1 + depth p | |
1558 | L'.PRecord xps => foldl (fn ((_, p, _), n) => Int.max (depth p, n)) 0 xps | |
1559 | |
1560 val depth = 1 + foldl (fn (p, n) => Int.max (depth p, n)) 0 ps | |
1561 | |
1562 fun pcCoverage pc = | |
1563 case pc of | |
1564 L'.PConVar n => n | |
1565 | L'.PConProj (m1, ms, x) => | |
1566 let | |
1567 val (str, sgn) = E.chaseMpath env (m1, ms) | |
1568 in | |
1569 case E.projectConstructor env {str = str, sgn = sgn, field = x} of | |
1570 NONE => raise Fail "exhaustive: Can't project constructor" | |
1571 | SOME (_, n, _, _, _) => n | |
1572 end | |
1573 | |
1574 fun coverage (p, _) = | |
1575 case p of | |
1576 L'.PWild => Wild | |
1577 | L'.PVar _ => Wild | |
1578 | L'.PPrim _ => None | |
1579 | L'.PCon (_, pc, _, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild)) | |
1580 | L'.PCon (_, pc, _, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p)) | |
1581 | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) => | |
1582 SM.insert (fmap, x, coverage p)) SM.empty xps] | |
1583 | |
1584 fun merge (c1, c2) = | |
1585 case (c1, c2) of | |
1586 (None, _) => c2 | |
1587 | (_, None) => c1 | |
1588 | |
1589 | (Wild, _) => Wild | |
1590 | (_, Wild) => Wild | |
1591 | |
1592 | (Datatype cm1, Datatype cm2) => Datatype (IM.unionWith merge (cm1, cm2)) | |
1593 | |
1594 | (Record fm1, Record fm2) => Record (fm1 @ fm2) | |
1595 | |
1596 | _ => None | |
1597 | |
1598 fun combinedCoverage ps = | |
1599 case ps of | |
1600 [] => raise Fail "Empty pattern list for coverage checking" | |
1601 | [p] => coverage p | |
1602 | p :: ps => merge (coverage p, combinedCoverage ps) | |
1603 | |
1604 fun enumerateCases depth t = | |
1605 (TextIO.print "enum'\n"; if depth <= 0 then | |
1606 [Wild] | |
1607 else | |
1608 let | |
1609 val dtype = | |
1610 ListUtil.mapConcat (fn (_, n, to) => | |
1611 case to of | |
1612 NONE => [Datatype (IM.insert (IM.empty, n, Wild))] | |
1613 | SOME t => map (fn c => Datatype (IM.insert (IM.empty, n, c))) | |
1614 (enumerateCases (depth-1) t)) | |
1615 in | |
1616 case #1 (hnormCon env t) of | |
1617 L'.CNamed n => | |
1618 (let | |
1619 val dt = E.lookupDatatype env n | |
1620 val cons = E.constructors dt | |
1621 in | |
1622 dtype cons | |
1623 end handle E.UnboundNamed _ => [Wild]) | |
1624 | L'.TRecord c => | |
1625 (case #1 (hnormCon env c) of | |
1626 L'.CRecord (_, xts) => | |
1627 let | |
1628 val xts = map (fn (x, t) => (hnormCon env x, t)) xts | |
1629 | |
1630 fun exponentiate fs = | |
1631 case fs of | |
1632 [] => [SM.empty] | |
1633 | ((L'.CName x, _), t) :: rest => | |
1634 let | |
1635 val this = enumerateCases depth t | |
1636 val rest = exponentiate rest | |
1637 in | |
1638 TextIO.print ("Before (" ^ Int.toString (length this) | |
1639 ^ ", " ^ Int.toString (length rest) ^ ")\n"); | |
1640 ListUtil.mapConcat (fn fmap => | |
1641 map (fn c => SM.insert (fmap, x, c)) this) rest | |
1642 before TextIO.print "After\n" | |
1643 end | |
1644 | _ => raise Fail "exponentiate: Not CName" | |
1645 in | |
1646 if List.exists (fn ((L'.CName _, _), _) => false | |
1647 | (c, _) => true) xts then | |
1648 [Wild] | |
1649 else | |
1650 map (fn ls => Record [ls]) (exponentiate xts) | |
1651 end | |
1652 | _ => [Wild]) | |
1653 | _ => [Wild] | |
1654 end before TextIO.print "/enum'\n") | |
1655 | |
1656 fun coverageImp (c1, c2) = | |
1657 let | |
1658 val r = | |
1659 case (c1, c2) of | |
1660 (Wild, _) => true | |
1661 | |
1662 | (Datatype cmap1, Datatype cmap2) => | |
1663 List.all (fn (n, c2) => | |
1664 case IM.find (cmap1, n) of | |
1665 NONE => false | |
1666 | SOME c1 => coverageImp (c1, c2)) (IM.listItemsi cmap2) | |
1667 | (Datatype cmap1, Wild) => | |
1668 List.all (fn (n, c1) => coverageImp (c1, Wild)) (IM.listItemsi cmap1) | |
1669 | |
1670 | (Record fmaps1, Record fmaps2) => | |
1671 List.all (fn fmap2 => | |
1672 List.exists (fn fmap1 => | |
1673 List.all (fn (x, c2) => | |
1674 case SM.find (fmap1, x) of | |
1675 NONE => true | |
1676 | SOME c1 => coverageImp (c1, c2)) | |
1677 (SM.listItemsi fmap2)) | |
1678 fmaps1) fmaps2 | |
1679 | |
1680 | (Record fmaps1, Wild) => | |
1681 List.exists (fn fmap1 => | |
1682 List.all (fn (x, c1) => coverageImp (c1, Wild)) | |
1683 (SM.listItemsi fmap1)) fmaps1 | |
1684 | |
1685 | _ => false | |
1686 in | |
1687 (*TextIO.print ("coverageImp(" ^ c2s c1 ^ ", " ^ c2s c2 ^ ") = " ^ Bool.toString r ^ "\n");*) | |
1688 r | |
1689 end | |
1690 | |
1691 fun isTotal (c, t) = | |
1692 case c of | |
1693 None => false | |
1694 | Wild => true | |
1695 | Datatype cm => | |
1696 let | |
1697 val (t, _) = hnormCon env t | |
1698 | |
1699 val dtype = | |
1700 List.all (fn (_, n, to) => | |
1701 case IM.find (cm, n) of | |
1702 NONE => false | |
1703 | SOME c' => | |
1704 case to of | |
1705 NONE => true | |
1706 | SOME t' => isTotal (c', t')) | |
1707 | |
1708 fun unapp t = | |
1709 case t of | |
1710 L'.CApp ((t, _), _) => unapp t | |
1711 | _ => t | |
1712 in | |
1713 case unapp t of | |
1714 L'.CNamed n => | |
1715 let | |
1716 val dt = E.lookupDatatype env n | |
1717 val cons = E.constructors dt | |
1718 in | |
1719 dtype cons | |
1720 end | |
1721 | L'.CModProj (m1, ms, x) => | |
1722 let | |
1723 val (str, sgn) = E.chaseMpath env (m1, ms) | |
1724 in | |
1725 case E.projectDatatype env {str = str, sgn = sgn, field = x} of | |
1726 NONE => raise Fail "isTotal: Can't project datatype" | |
1727 | SOME (_, cons) => dtype cons | |
1728 end | |
1729 | L'.CError => true | |
1730 | c => | |
1731 (prefaces "Not a datatype" [("loc", PD.string (ErrorMsg.spanToString loc)), | |
1732 ("c", p_con env (c, ErrorMsg.dummySpan))]; | |
1733 raise Fail "isTotal: Not a datatype") | |
1734 end | |
1735 | Record _ => List.all (fn c2 => coverageImp (c, c2)) | |
1736 (TextIO.print "enum\n"; enumerateCases depth t before TextIO.print "/enum\n") | |
1737 in | |
1738 isTotal (combinedCoverage ps, t) | |
1739 end*) | |
1740 | 1541 |
1741 fun unmodCon env (c, loc) = | 1542 fun unmodCon env (c, loc) = |
1742 case c of | 1543 case c of |
1743 L'.CNamed n => | 1544 L'.CNamed n => |
1744 (case E.lookupCNamed env n of | 1545 (case E.lookupCNamed env n of |
2081 end) | 1882 end) |
2082 gs1 pes | 1883 gs1 pes |
2083 in | 1884 in |
2084 case exhaustive (env, et, map #1 pes', loc) of | 1885 case exhaustive (env, et, map #1 pes', loc) of |
2085 NONE => () | 1886 NONE => () |
2086 | SOME p => expError env (Inexhaustive (loc, p)); | 1887 | SOME p => if !mayDelay then |
1888 delayedExhaustives := (env, et, map #1 pes', loc) :: !delayedExhaustives | |
1889 else | |
1890 expError env (Inexhaustive (loc, p)); | |
2087 | 1891 |
2088 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs) | 1892 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs) |
2089 end | 1893 end |
2090 | 1894 |
2091 | L.ELet (eds, e) => | 1895 | L.ELet (eds, e) => |
2111 | 1915 |
2112 val () = checkCon env e' et pt | 1916 val () = checkCon env e' et pt |
2113 | 1917 |
2114 val pt = normClassConstraint env pt | 1918 val pt = normClassConstraint env pt |
2115 in | 1919 in |
1920 case exhaustive (env, et, [p'], loc) of | |
1921 NONE => () | |
1922 | SOME p => if !mayDelay then | |
1923 delayedExhaustives := (env, et, [p'], loc) :: !delayedExhaustives | |
1924 else | |
1925 expError env (Inexhaustive (loc, p)); | |
1926 | |
2116 ((L'.EDVal (p', pt, e'), loc), (env', gs1 @ gs)) | 1927 ((L'.EDVal (p', pt, e'), loc), (env', gs1 @ gs)) |
2117 end | 1928 end |
2118 | L.EDValRec vis => | 1929 | L.EDValRec vis => |
2119 let | 1930 let |
2120 fun allowable (e, _) = | 1931 fun allowable (e, _) = |
3954 | 3765 |
3955 fun elabFile basis topStr topSgn env file = | 3766 fun elabFile basis topStr topSgn env file = |
3956 let | 3767 let |
3957 val () = mayDelay := true | 3768 val () = mayDelay := true |
3958 val () = delayedUnifs := [] | 3769 val () = delayedUnifs := [] |
3770 val () = delayedExhaustives := [] | |
3959 | 3771 |
3960 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) | 3772 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) |
3961 val () = case gs of | 3773 val () = case gs of |
3962 [] => () | 3774 [] => () |
3963 | _ => (app (fn (_, env, _, c1, c2) => | 3775 | _ => (app (fn (_, env, _, c1, c2) => |
4151 if ErrorMsg.anyErrors () then | 3963 if ErrorMsg.anyErrors () then |
4152 () | 3964 () |
4153 else | 3965 else |
4154 app (fn f => f ()) (!checks); | 3966 app (fn f => f ()) (!checks); |
4155 | 3967 |
3968 if ErrorMsg.anyErrors () then | |
3969 () | |
3970 else | |
3971 app (fn all as (_, _, _, loc) => | |
3972 case exhaustive all of | |
3973 NONE => () | |
3974 | SOME p => expError env (Inexhaustive (loc, p))) | |
3975 (!delayedExhaustives); | |
3976 | |
4156 (*preface ("file", p_file env' file);*) | 3977 (*preface ("file", p_file env' file);*) |
4157 | 3978 |
4158 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) | 3979 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) |
4159 :: ds | 3980 :: ds |
4160 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) | 3981 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) |