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