From 596bf8121cb42b4db71d0cdec9c2260d33391d8c Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 28 May 2009 12:07:05 -0400 Subject: Destructing local let, to the point where demo compiles --- src/elab.sml | 4 ++-- src/elab_env.sml | 20 ++++++++++---------- src/elab_print.sml | 16 ++++++++++++---- src/elab_util.sml | 31 +++++++++++++++++++++++-------- src/elaborate.sml | 18 +++++++----------- src/explify.sml | 7 +++++-- src/source.sml | 2 +- src/source_print.sml | 10 +++++++--- src/termination.sml | 2 +- src/unnest.sml | 21 ++++++++++++++++----- src/urweb.grm | 2 +- 11 files changed, 85 insertions(+), 48 deletions(-) (limited to 'src') diff --git a/src/elab.sml b/src/elab.sml index de2db500..76ea6725 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -120,10 +120,10 @@ datatype exp' = | 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 diff --git a/src/elab_env.sml b/src/elab_env.sml index 88b2554b..2296d819 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -1454,9 +1454,18 @@ fun projectConstraints env {sgn, str} = | 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 @@ fun declBinds env (d, loc) = 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 diff --git a/src/elab_print.sml b/src/elab_print.sml index ab38c2e1..3e4ea659 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -423,7 +423,7 @@ fun p_exp' par env (e, _) = | 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_exp env = p_exp' false env 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 diff --git a/src/elab_util.sml b/src/elab_util.sml index 036aa867..c2101ae3 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -306,6 +306,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = | 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = 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 diff --git a/src/elaborate.sml b/src/elaborate.sml index 6f8575db..b4ce1861 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2093,7 +2093,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) = 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 @@ and elabEdecl denv (dAll as (d, loc), (env, gs)) = 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 ((p', pt), (env', _)) = elabPat (p, (env, SS.empty)) + val (e', et, gs1) = elabExp (env, denv) e - val (e', et, gs2) = elabExp (env, denv) e + val () = checkCon env e' et pt - val () = checkCon env e' et c' - - val c' = normClassConstraint env c' - val env' = E.pushERel env x c' + 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 diff --git a/src/explify.sml b/src/explify.sml index d8bd6bff..3ec588fa 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -123,11 +123,14 @@ fun explifyExp (e, loc) = | 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) diff --git a/src/source.sml b/src/source.sml index bfa270d8..c5950b36 100644 --- a/src/source.sml +++ b/src/source.sml @@ -138,7 +138,7 @@ and exp' = | 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 diff --git a/src/source_print.sml b/src/source_print.sml index a16b5bb1..7ec584d7 100644 --- a/src/source_print.sml +++ b/src/source_print.sml @@ -338,9 +338,13 @@ and p_exp e = p_exp' false e 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", diff --git a/src/termination.sml b/src/termination.sml index 5dd95f46..f0b21d99 100644 --- a/src/termination.sml +++ b/src/termination.sml @@ -306,7 +306,7 @@ fun declOk' env (d, loc) = | 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 diff --git a/src/unnest.sml b/src/unnest.sml index 51b66aa4..3dfa741d 100644 --- a/src/unnest.sml +++ b/src/unnest.sml @@ -173,7 +173,7 @@ fun kind (_, k, st) = (k, st) 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 @@ fun exp ((ks, ts), e as old, st : state) = 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 @@ fun exp ((ks, ts), e as old, st : state) = (*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),*) diff --git a/src/urweb.grm b/src/urweb.grm index 0d2c1d47..8cdf8063 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -1167,7 +1167,7 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) 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))) -- cgit v1.2.3