Mercurial > urweb

comparison src/elaborate.sml @ 256:e52243e20858

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'eq' type class
author Adam Chlipala <adamc@hcoop.net>
date Sun, 31 Aug 2008 15:15:41 -0400
parents 69d337f186eb
children 42dfb0d61cf0
comparison
equal deleted inserted replaced
255:69d337f186eb 256:e52243e20858
1582 val (t', tk, gs) = elabCon (env, denv) t 1582 val (t', tk, gs) = elabCon (env, denv) t
1583 in 1583 in
1584 checkKind env t' tk ktype; 1584 checkKind env t' tk ktype;
1585 (t', gs) 1585 (t', gs)
1586 end 1586 end
1587 val (e', et, gs2) = elabExp (E.pushERel env x t', denv) e 1587 val (dom, gs2) = normClassConstraint (env, denv) t'
1588 val (e', et, gs3) = elabExp (E.pushERel env x dom, denv) e
1588 in 1589 in
1589 ((L'.EAbs (x, t', et, e'), loc), 1590 ((L'.EAbs (x, t', et, e'), loc),
1590 (L'.TFun (t', et), loc), 1591 (L'.TFun (t', et), loc),
1591 enD gs1 @ gs2) 1592 enD gs1 @ enD gs2 @ gs3)
1592 end 1593 end
1593 | L.ECApp (e, c) => 1594 | L.ECApp (e, c) =>
1594 let 1595 let
1595 val (e', et, gs1) = elabExp (env, denv) e 1596 val (e', et, gs1) = elabExp (env, denv) e
1596 val (e', et, gs2) = elabHead (env, denv) e' et 1597 val (e', et, gs2) = elabHead (env, denv) e' et