Mercurial > urweb

comparison src/elaborate.sml @ 1093:8d3aa6c7cee0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make summary unification more conservative; infer implicit arguments after applications
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Dec 2009 11:56:40 -0500
parents 0657e5adc938
children 0b1d666bddb4
comparison
equal deleted inserted replaced
1092:6f4b05fc4361 1093:8d3aa6c7cee0
691 end 691 end
692 692
693 and consNeq env (c1, c2) = 693 and consNeq env (c1, c2) =
694 case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of 694 case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of
695 (L'.CName x1, L'.CName x2) => x1 <> x2 695 (L'.CName x1, L'.CName x2) => x1 <> x2
696 | (L'.CName _, L'.CRel _) => true
697 | (L'.CRel _, L'.CName _) => true
698 | (L'.CRel n1, L'.CRel n2) => n1 <> n2
699 | (L'.CRel _, L'.CNamed _) => true
700 | (L'.CNamed _, L'.CRel _) => true
701 | (L'.CRel _, L'.CModProj _) => true
702 | (L'.CModProj _, L'.CRel _) => true
696 | _ => false 703 | _ => false
697 704
698 and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) = 705 and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) =
699 let 706 let
700 (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)), 707 (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)),
1617 end 1624 end
1618 | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc) 1625 | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc)
1619 | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c 1626 | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c
1620 | _ => unmodCon env (c, loc) 1627 | _ => unmodCon env (c, loc)
1621 1628
1629 fun findHead e e' =
1630 let
1631 fun findHead (e, _) =
1632 case e of
1633 L.EVar (_, _, infer) =>
1634 let
1635 fun findHead' (e, _) =
1636 case e of
1637 L'.ENamed _ => true
1638 | L'.EModProj _ => true
1639 | L'.EApp (e, _) => findHead' e
1640 | L'.ECApp (e, _) => findHead' e
1641 | L'.EKApp (e, _) => findHead' e
1642 | _ => false
1643 in
1644 if findHead' e' then
1645 SOME infer
1646 else
1647 NONE
1648 end
1649 | L.EApp (e, _) => findHead e
1650 | L.ECApp (e, _) => findHead e
1651 | L.EDisjointApp e => findHead e
1652 | _ => NONE
1653 in
1654 findHead e
1655 end
1656
1622 fun elabExp (env, denv) (eAll as (e, loc)) = 1657 fun elabExp (env, denv) (eAll as (e, loc)) =
1623 let 1658 let
1624 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*) 1659 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*)
1625 (*val befor = Time.now ()*) 1660 (*val befor = Time.now ()*)
1626 1661
1672 end 1707 end
1673 1708
1674 | L.EApp (e1, e2) => 1709 | L.EApp (e1, e2) =>
1675 let 1710 let
1676 val (e1', t1, gs1) = elabExp (env, denv) e1 1711 val (e1', t1, gs1) = elabExp (env, denv) e1
1712
1677 val (e2', t2, gs2) = elabExp (env, denv) e2 1713 val (e2', t2, gs2) = elabExp (env, denv) e2
1678 1714
1679 val dom = cunif (loc, ktype) 1715 val dom = cunif (loc, ktype)
1680 val ran = cunif (loc, ktype) 1716 val ran = cunif (loc, ktype)
1681 val t = (L'.TFun (dom, ran), loc) 1717 val t = (L'.TFun (dom, ran), loc)
1718
1719 val () = checkCon env e1' t1 t
1720 val () = checkCon env e2' t2 dom
1721
1722 val ef = (L'.EApp (e1', e2'), loc)
1723 val (ef, et, gs3) =
1724 case findHead e1 e1' of
1725 NONE => (ef, ran, [])
1726 | SOME infer => elabHead (env, denv) infer ef ran
1682 in 1727 in
1683 checkCon env e1' t1 t; 1728 (ef, et, gs1 @ gs2 @ gs3)
1684 checkCon env e2' t2 dom;
1685 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2)
1686 end 1729 end
1687 | L.EAbs (x, to, e) => 1730 | L.EAbs (x, to, e) =>
1688 let 1731 let
1689 val (t', gs1) = case to of 1732 val (t', gs1) = case to of
1690 NONE => (cunif (loc, ktype), []) 1733 NONE => (cunif (loc, ktype), [])
1703 enD gs1 @ gs2) 1746 enD gs1 @ gs2)
1704 end 1747 end
1705 | L.ECApp (e, c) => 1748 | L.ECApp (e, c) =>
1706 let 1749 let
1707 val (e', et, gs1) = elabExp (env, denv) e 1750 val (e', et, gs1) = elabExp (env, denv) e
1751
1708 val oldEt = et 1752 val oldEt = et
1709 val (c', ck, gs2) = elabCon (env, denv) c 1753 val (c', ck, gs2) = elabCon (env, denv) c
1710 val (et', _) = hnormCon env et 1754 val (et', _) = hnormCon env et
1711 in 1755 in
1712 case et' of 1756 case et' of
1715 let 1759 let
1716 val () = checkKind env c' ck k 1760 val () = checkKind env c' ck k
1717 val eb' = subConInCon (0, c') eb 1761 val eb' = subConInCon (0, c') eb
1718 handle SynUnif => (expError env (Unif ("substitution", loc, eb)); 1762 handle SynUnif => (expError env (Unif ("substitution", loc, eb));
1719 cerror) 1763 cerror)
1764
1765 val ef = (L'.ECApp (e', c'), loc)
1766 val (ef, eb', gs3) =
1767 case findHead e e' of
1768 NONE => (ef, eb', [])
1769 | SOME infer => elabHead (env, denv) infer ef eb'
1720 in 1770 in
1721 (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll), 1771 (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll),
1722 ("et", p_con env oldEt), 1772 ("et", p_con env oldEt),
1723 ("x", PD.string x), 1773 ("x", PD.string x),
1724 ("eb", p_con (E.pushCRel env x k) eb), 1774 ("eb", p_con (E.pushCRel env x k) eb),
1725 ("c", p_con env c'), 1775 ("c", p_con env c'),
1726 ("eb'", p_con env eb')];*) 1776 ("eb'", p_con env eb')];*)
1727 ((L'.ECApp (e', c'), loc), eb', gs1 @ enD gs2) 1777 (ef, eb', gs1 @ enD gs2 @ gs3)
1728 end 1778 end
1729 1779
1730 | _ => 1780 | _ =>
1731 (expError env (WrongForm ("constructor function", e', et)); 1781 (expError env (WrongForm ("constructor function", e', et));
1732 (eerror, cerror, [])) 1782 (eerror, cerror, []))