Mercurial > urweb

comparison src/elaborate.sml @ 830:d07980bf1444

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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)