Mercurial > urweb
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)))