changeset 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 be0988e46336
children 78504d97410b
files src/elab.sml src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/source.sml src/source_print.sml src/termination.sml src/unnest.sml src/urweb.grm
diffstat 11 files changed, 87 insertions(+), 50 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab.sml	Thu May 28 11:45:45 2009 -0400
+++ b/src/elab.sml	Thu May 28 12:07:05 2009 -0400
@@ -120,10 +120,10 @@
        | EError
        | EUnif of exp option ref
 
-       | ELet of edecl list * exp
+       | ELet of edecl list * exp * con
 
 and edecl' =
-    EDVal of string * con * exp
+    EDVal of pat * con * exp
   | EDValRec of (string * con * exp) list
 
 withtype exp = exp' located
--- a/src/elab_env.sml	Thu May 28 11:45:45 2009 -0400
+++ b/src/elab_env.sml	Thu May 28 12:07:05 2009 -0400
@@ -1454,9 +1454,18 @@
       | SgnError => SOME []
       | _ => NONE
 
+fun patBinds env (p, loc) =
+    case p of
+        PWild => env
+      | PVar (x, t) => pushERel env x t
+      | PPrim _ => env
+      | PCon (_, _, _, NONE) => env
+      | PCon (_, _, _, SOME p) => patBinds env p
+      | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
+
 fun edeclBinds env (d, loc) =
     case d of
-        EDVal (x, t, _) => pushERel env x t
+        EDVal (p, _, _) => patBinds env p
       | EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis
 
 fun declBinds env (d, loc) =
@@ -1565,13 +1574,4 @@
             pushENamedAs env x n t
         end
 
-fun patBinds env (p, loc) =
-    case p of
-        PWild => env
-      | PVar (x, t) => pushERel env x t
-      | PPrim _ => env
-      | PCon (_, _, _, NONE) => env
-      | PCon (_, _, _, SOME p) => patBinds env p
-      | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
-
 end
--- a/src/elab_print.sml	Thu May 28 11:45:45 2009 -0400
+++ b/src/elab_print.sml	Thu May 28 12:07:05 2009 -0400
@@ -423,7 +423,7 @@
       | EUnif (ref (SOME e)) => p_exp env e
       | EUnif _ => string "_"
 
-      | ELet (ds, e) =>
+      | ELet (ds, e, _) =>
         let
             val (dsp, env) = ListUtil.foldlMap
                              (fn (d, env) =>
@@ -456,9 +456,17 @@
 
 and p_edecl env (dAll as (d, _)) =
     case d of
-        EDVal vi => box [string "val",
-                         space,
-                         p_evali env vi]
+        EDVal (p, t, e) => box [string "val",
+                                space,
+                                p_pat env p,
+                                space,
+                                string ":",
+                                space,
+                                p_con env t,
+                                space,
+                                string "=",
+                                space,
+                                p_exp env e]
       | EDValRec vis =>
         let
             val env = E.edeclBinds env dAll
--- a/src/elab_util.sml	Thu May 28 11:45:45 2009 -0400
+++ b/src/elab_util.sml	Thu May 28 12:07:05 2009 -0400
@@ -306,6 +306,17 @@
             end
         val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
 
+        fun doVars ((p, _), ctx) =
+            case p of
+                PWild => ctx
+              | PVar xt => bind (ctx, RelE xt)
+              | PPrim _ => ctx
+              | PCon (_, _, _, NONE) => ctx
+              | PCon (_, _, _, SOME p) => doVars (p, ctx)
+              | PRecord xpcs =>
+                foldl (fn ((_, p, _), ctx) => doVars (p, ctx))
+                      ctx xpcs
+
         fun mfe ctx e acc =
             S.bindP (mfe' ctx e acc, fe ctx)
 
@@ -425,13 +436,13 @@
               | EUnif (ref (SOME e)) => mfe ctx e
               | EUnif _ => S.return2 eAll
 
-              | ELet (des, e) =>
+              | ELet (des, e, t) =>
                 let
                     val (des, ctx) = foldl (fn (ed, (des, ctx)) =>
                                                let
                                                    val ctx' =
                                                        case #1 ed of
-                                                           EDVal (x, t, _) => bind (ctx, RelE (x, t))
+                                                           EDVal (p, _, _) => doVars (p, ctx)
                                                          | EDValRec vis =>
                                                            foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
                                                in
@@ -445,9 +456,11 @@
                 in
                     S.bind2 (des,
                          fn des' =>
-                            S.map2 (mfe ctx e,
+                            S.bind2 (mfe ctx e,
                                     fn e' =>
-                                       (ELet (des', e'), loc)))
+                                       S.map2 (mfc ctx t,
+                                               fn t' =>
+                                                  (ELet (des', e', t'), loc))))
                 end
 
               | EKAbs (x, e) =>
@@ -463,10 +476,12 @@
 
         and mfed ctx (dAll as (d, loc)) =
             case d of
-                EDVal vi =>
-                S.map2 (mfvi ctx vi,
-                     fn vi' =>
-                        (EDVal vi', loc))
+                EDVal (p, t, e) =>
+                S.bind2 (mfc ctx t,
+                         fn t' =>
+                            S.map2 (mfe (doVars (p, ctx)) e,
+                                 fn e' =>
+                                    (EDVal (p, t', e'), loc)))
               | EDValRec vis =>
                 let
                     val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
--- 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
--- a/src/explify.sml	Thu May 28 11:45:45 2009 -0400
+++ b/src/explify.sml	Thu May 28 12:07:05 2009 -0400
@@ -123,11 +123,14 @@
       | L.EUnif (ref (SOME e)) => explifyExp e
       | L.EUnif _ => raise Fail ("explifyExp: Undetermined EUnif at " ^ EM.spanToString loc)
 
-      | L.ELet (des, e) =>
+      | L.ELet (des, e, t) =>
         foldr (fn ((de, loc), e) =>
                   case de of
                       L.EDValRec _ => raise Fail "explifyExp: Local 'val rec' remains"
-                    | L.EDVal (x, t, e') => (L'.ELet (x, explifyCon t, explifyExp e', e), loc))
+                    | L.EDVal ((L.PVar (x, _), _), t', e') => (L'.ELet (x, explifyCon t', explifyExp e', e), loc)
+                    | L.EDVal (p, t', e') => (L'.ECase (explifyExp e',
+                                                        [(explifyPat p, e)],
+                                                        {disc = explifyCon t', result = explifyCon t}), loc))
         (explifyExp e) des
 
       | L.EKAbs (x, e) => (L'.EKAbs (x, explifyExp e), loc)
--- a/src/source.sml	Thu May 28 11:45:45 2009 -0400
+++ b/src/source.sml	Thu May 28 12:07:05 2009 -0400
@@ -138,7 +138,7 @@
   | ELet of edecl list * exp
 
 and edecl' =
-    EDVal of string * con option * exp
+    EDVal of pat * exp
   | EDValRec of (string * con option * exp) list
 
 withtype sgn_item = sgn_item' located
--- a/src/source_print.sml	Thu May 28 11:45:45 2009 -0400
+++ b/src/source_print.sml	Thu May 28 12:07:05 2009 -0400
@@ -338,9 +338,13 @@
 
 and p_edecl (d, _) =
   case d of
-      EDVal vi => box [string "val",
-                       space,
-                       p_vali vi]
+      EDVal (p, e) => box [string "val",
+                           space,
+                           p_pat p,
+                           space,
+                           string "=",
+                           space,
+                           p_exp e]
     | EDValRec vis => box [string "val",
                            space,
                            string "rec",
--- a/src/termination.sml	Thu May 28 11:45:45 2009 -0400
+++ b/src/termination.sml	Thu May 28 12:07:05 2009 -0400
@@ -306,7 +306,7 @@
                       | EUnif (ref (SOME e)) => exp parent (penv, calls) e
                       | EUnif (ref NONE) => (Rabble, calls)
 
-                      | ELet (eds, e) =>
+                      | ELet (eds, e, _) =>
                         let
                             fun extPenv ((ed, _), penv) =
                                 case ed of
--- a/src/unnest.sml	Thu May 28 11:45:45 2009 -0400
+++ b/src/unnest.sml	Thu May 28 12:07:05 2009 -0400
@@ -173,7 +173,7 @@
 
 fun exp ((ks, ts), e as old, st : state) =
     case e of
-        ELet (eds, e) =>
+        ELet (eds, e, t) =>
         let
             (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
 
@@ -190,12 +190,23 @@
                 ListUtil.foldlMapConcat
                 (fn (ed, (ts, maxName, ds, subs, by)) =>
                     case #1 ed of
-                        EDVal (x, t, e) =>
+                        EDVal (p, t, e) =>
                         let
                             val e = doSubst (e, subs, by)
+
+                            fun doVars ((p, _), ts) =
+                                case p of
+                                    PWild => ts
+                                  | PVar xt => xt :: ts
+                                  | PPrim _ => ts
+                                  | PCon (_, _, _, NONE) => ts
+                                  | PCon (_, _, _, SOME p) => doVars (p, ts)
+                                  | PRecord xpcs =>
+                                    foldl (fn ((_, p, _), ts) => doVars (p, ts))
+                                          ts xpcs
                         in
-                            ([(EDVal (x, t, e), #2 ed)],
-                             ((x, t) :: ts,
+                            ([(EDVal (p, t, e), #2 ed)],
+                             (doVars (p, ts),
                               maxName, ds,
                               ((0, (ERel 0, #2 ed))
                                :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs),
@@ -341,7 +352,7 @@
             (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e),
                                      ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))),
                                      ("e'", ElabPrint.p_exp ElabEnv.empty e')];*)
-            (ELet (eds, e'),
+            (ELet (eds, e', t),
              {maxName = maxName,
               decls = ds})
             (*(ELet (eds, doSubst (liftExpInExp (~(length subs - numRemaining)) (length subs) e) subs),*)
--- a/src/urweb.grm	Thu May 28 11:45:45 2009 -0400
+++ b/src/urweb.grm	Thu May 28 12:07:05 2009 -0400
@@ -1167,7 +1167,7 @@
 edecls :                                ([])
        | edecl edecls                   (edecl :: edecls)
 
-edecl  : VAL vali                       ((EDVal vali, s (VALleft, valiright)))
+edecl  : VAL pat EQ eexp                ((EDVal (pat, eexp), s (VALleft, eexpright)))
        | VAL REC valis                  ((EDValRec valis, s (VALleft, valisright)))
        | FUN valis                      ((EDValRec valis, s (FUNleft, valisright)))