Mercurial > urweb
diff src/elaborate.sml @ 825:7f871c03e3a1
Destructing local let, to the point where demo compiles
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 28 May 2009 12:07:05 -0400 |
parents | d4e811beb8eb |
children | d07980bf1444 |
line wrap: on
line diff
--- a/src/elaborate.sml Thu May 28 11:45:45 2009 -0400 +++ b/src/elaborate.sml Thu May 28 12:07:05 2009 -0400 @@ -2093,7 +2093,7 @@ val (eds, (env, gs1)) = ListUtil.foldlMap (elabEdecl denv) (env, []) eds val (e, t, gs2) = elabExp (env, denv) e in - ((L'.ELet (eds, e), loc), t, gs1 @ gs2) + ((L'.ELet (eds, e, t), loc), t, gs1 @ gs2) end in (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*) @@ -2104,20 +2104,16 @@ let val r = case d of - L.EDVal (x, co, e) => + L.EDVal (p, e) => let - val (c', _, gs1) = case co of - NONE => (cunif (loc, ktype), ktype, []) - | SOME c => elabCon (env, denv) c - - val (e', et, gs2) = elabExp (env, denv) e - - val () = checkCon env e' et c' - - val c' = normClassConstraint env c' - val env' = E.pushERel env x c' + val ((p', pt), (env', _)) = elabPat (p, (env, SS.empty)) + val (e', et, gs1) = elabExp (env, denv) e + + val () = checkCon env e' et pt + + val pt = normClassConstraint env pt in - ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ gs)) + ((L'.EDVal (p', pt, e'), loc), (env', gs1 @ gs)) end | L.EDValRec vis => let