Mercurial > urweb

comparison src/elaborate.sml @ 328:58f1260f293f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed a mind-numbing De Bruijn bug
author Adam Chlipala <adamc@hcoop.net>
date Thu, 11 Sep 2008 19:59:31 -0400
parents 3a57f3b3a3f8
children eec65c11d3e2
comparison
equal deleted inserted replaced
327:3a57f3b3a3f8 328:58f1260f293f
1607 enD gs1 @ enD gs2 @ gs3) 1607 enD gs1 @ enD gs2 @ gs3)
1608 end 1608 end
1609 | L.ECApp (e, c) => 1609 | L.ECApp (e, c) =>
1610 let 1610 let
1611 val (e', et, gs1) = elabExp (env, denv) e 1611 val (e', et, gs1) = elabExp (env, denv) e
1612 val oldEt = et
1612 val (e', et, gs2) = elabHead (env, denv) e' et 1613 val (e', et, gs2) = elabHead (env, denv) e' et
1613 val (c', ck, gs3) = elabCon (env, denv) c 1614 val (c', ck, gs3) = elabCon (env, denv) c
1614 val ((et', _), gs4) = hnormCon (env, denv) et 1615 val ((et', _), gs4) = hnormCon (env, denv) et
1615 in 1616 in
1616 case et' of 1617 case et' of
1617 L'.CError => (eerror, cerror, []) 1618 L'.CError => (eerror, cerror, [])
1618 | L'.TCFun (_, _, k, eb) => 1619 | L'.TCFun (_, x, k, eb) =>
1619 let 1620 let
1620 val () = checkKind env c' ck k 1621 val () = checkKind env c' ck k
1621 val eb' = subConInCon (0, c') eb 1622 val eb' = subConInCon (0, c') eb
1622 handle SynUnif => (expError env (Unif ("substitution", eb)); 1623 handle SynUnif => (expError env (Unif ("substitution", eb));
1623 cerror) 1624 cerror)
1624 in 1625 in
1626 (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll),
1627 ("et", p_con env oldEt),
1628 ("x", PD.string x),
1629 ("eb", p_con (E.pushCRel env x k) eb),
1630 ("c", p_con env c'),
1631 ("eb'", p_con env eb')];*)
1625 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4) 1632 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4)
1626 end 1633 end
1627 1634
1628 | L'.CUnif _ => 1635 | L'.CUnif _ =>
1629 (expError env (Unif ("application", et)); 1636 (expError env (Unif ("application", et));
1635 end 1642 end
1636 | L.ECAbs (expl, x, k, e) => 1643 | L.ECAbs (expl, x, k, e) =>
1637 let 1644 let
1638 val expl' = elabExplicitness expl 1645 val expl' = elabExplicitness expl
1639 val k' = elabKind k 1646 val k' = elabKind k
1640 val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e 1647
1648 val env' = E.pushCRel env x k'
1649 val (e', et, gs) = elabExp (env', D.enter denv) e
1641 in 1650 in
1642 ((L'.ECAbs (expl', x, k', e'), loc), 1651 ((L'.ECAbs (expl', x, k', e'), loc),
1643 (L'.TCFun (expl', x, k', et), loc), 1652 (L'.TCFun (expl', x, k', et), loc),
1644 gs) 1653 gs)
1645 end 1654 end