Mercurial > urweb
changeset 447:b77863cd0be2
Elaborating 'let'
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 01 Nov 2008 11:17:29 -0400 |
| parents | 86c063fedc4d |
| children | 85819353a84f |
| files | src/elab.sml src/elab_env.sig src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml tests/let.ur |
| diffstat | 7 files changed, 192 insertions(+), 19 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab.sml Sat Nov 01 10:47:10 2008 -0400 +++ b/src/elab.sml Sat Nov 01 11:17:29 2008 -0400 @@ -117,7 +117,14 @@ | EError | EUnif of exp option ref + | ELet of edecl list * exp + +and edecl' = + EDVal of string * con * exp + | EDValRec of (string * con * exp) list + withtype exp = exp' located + and edecl = edecl' located datatype sgn_item' = SgiConAbs of string * int * kind
--- a/src/elab_env.sig Sat Nov 01 10:47:10 2008 -0400 +++ b/src/elab_env.sig Sat Nov 01 11:17:29 2008 -0400 @@ -85,6 +85,7 @@ val lookupStr : env -> string -> (int * Elab.sgn) option + val edeclBinds : env -> Elab.edecl -> env val declBinds : env -> Elab.decl -> env val sgiBinds : env -> Elab.sgn_item -> env
--- a/src/elab_env.sml Sat Nov 01 10:47:10 2008 -0400 +++ b/src/elab_env.sml Sat Nov 01 11:17:29 2008 -0400 @@ -1075,6 +1075,11 @@ | SgnError => SOME [] | _ => NONE +fun edeclBinds env (d, loc) = + case d of + EDVal (x, t, _) => pushERel env x t + | EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis + fun declBinds env (d, loc) = case d of DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
--- a/src/elab_print.sml Sat Nov 01 10:47:10 2008 -0400 +++ b/src/elab_print.sml Sat Nov 01 11:17:29 2008 -0400 @@ -378,15 +378,52 @@ | EUnif (ref (SOME e)) => p_exp env e | EUnif _ => string "_" + | ELet (ds, e) => + let + val (dsp, env) = ListUtil.foldlMap + (fn (d, env) => + (p_edecl env d, + E.edeclBinds env d)) + env ds + in + box [string "let", + newline, + box [p_list_sep newline (fn x => x) dsp], + newline, + string "in", + newline, + box [p_exp env e], + newline, + string "end"] + end + and p_exp env = p_exp' false env -fun p_named x n = - if !debug then - box [string x, - string "__", - string (Int.toString n)] - else - string x +and p_edecl env (dAll as (d, _)) = + case d of + EDVal vi => box [string "val", + space, + p_evali env vi] + | EDValRec vis => + let + val env = E.edeclBinds env dAll + in + box [string "val", + space, + string "rec", + space, + p_list_sep (box [newline, string "and", space]) (p_evali env) vis] + end + +and p_evali env (x, t, e) = box [string x, + space, + string ":", + space, + p_con env t, + space, + string "=", + space, + p_exp env e] fun p_datatype env (x, n, xs, cons) = let @@ -407,6 +444,14 @@ cons] end +fun p_named x n = + if !debug then + box [string x, + string "__", + string (Int.toString n)] + else + string x + fun p_sgn_item env (sgi, _) = case sgi of SgiConAbs (x, n, k) => box [string "con", @@ -556,6 +601,8 @@ space, p_exp env e] + + fun p_decl env (dAll as (d, _) : decl) = case d of DCon (x, n, k, c) => box [string "con",
--- a/src/elab_util.sml Sat Nov 01 10:47:10 2008 -0400 +++ b/src/elab_util.sml Sat Nov 01 11:17:29 2008 -0400 @@ -352,6 +352,48 @@ | EError => S.return2 eAll | EUnif (ref (SOME e)) => mfe ctx e | EUnif _ => S.return2 eAll + + | ELet (des, e) => + let + val (des, ctx) = foldl (fn (ed, (des, ctx)) => + (S.bind2 (des, + fn des' => + S.map2 (mfed ctx ed, + fn ed' => des' @ [ed'])), + case #1 ed of + EDVal (x, t, _) => bind (ctx, RelE (x, t)) + | EDValRec vis => + foldl (fn ((x, t, _), env) => bind (ctx, RelE (x, t))) ctx vis)) + (S.return2 [], ctx) des + in + S.bind2 (des, + fn des' => + S.map2 (mfe ctx e, + fn e' => + (ELet (des', e'), loc))) + end + + and mfed ctx (dAll as (d, loc)) = + case d of + EDVal vi => + S.map2 (mfvi ctx vi, + fn vi' => + (EDVal vi', loc)) + | EDValRec vis => + let + val ctx = foldl (fn ((x, t, _), env) => bind (ctx, RelE (x, t))) ctx vis + in + S.map2 (ListUtil.mapfold (mfvi ctx) vis, + fn vis' => + (EDValRec vis', loc)) + end + + and mfvi ctx (x, c, e) = + S.bind2 (mfc ctx c, + fn c' => + S.map2 (mfe ctx e, + fn e' => + (x, c', e'))) in mfe end
--- a/src/elaborate.sml Sat Nov 01 10:47:10 2008 -0400 +++ b/src/elaborate.sml Sat Nov 01 11:17:29 2008 -0400 @@ -1400,6 +1400,18 @@ end | _ => ((c, loc), []) + +val makeInstantiable = + let + fun kind k = k + fun con c = + case c of + L'.CDisjoint (L'.LeaveAlone, c1, c2, c) => L'.CDisjoint (L'.Instantiate, c1, c2, c) + | _ => c + in + U.Con.map {kind = kind, con = con} + end + fun elabExp (env, denv) (eAll as (e, loc)) = let (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*) @@ -1670,11 +1682,79 @@ ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs) end + + | L.ELet (eds, e) => + let + 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) + end in (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*) r end +and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) = + let + val r = + case d of + L.EDVal (x, co, 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 gs3 = checkCon (env, denv) e' et c' + val (c', gs4) = normClassConstraint (env, denv) c' + val env' = E.pushERel env x c' + val c' = makeInstantiable c' + in + ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs)) + end + | L.EDValRec vis => + let + fun allowable (e, _) = + case e of + L.EAbs _ => true + | L.ECAbs (_, _, _, e) => allowable e + | L.EDisjoint (_, _, e) => allowable e + | _ => false + + val (vis, gs) = ListUtil.foldlMap + (fn ((x, co, e), gs) => + let + val (c', _, gs1) = case co of + NONE => (cunif (loc, ktype), ktype, []) + | SOME c => elabCon (env, denv) c + in + ((x, c', e), enD gs1 @ gs) + end) gs vis + + val env = foldl (fn ((x, c', _), env) => E.pushERel env x c') env vis + + val (vis, gs) = ListUtil.foldlMap (fn ((x, c', e), gs) => + let + val (e', et, gs1) = elabExp (env, denv) e + + val gs2 = checkCon (env, denv) e' et c' + + val c' = makeInstantiable c' + in + if allowable e then + () + else + expError env (IllegalRec (x, e')); + ((x, c', e'), gs1 @ enD gs2 @ gs) + end) gs vis + in + ((L'.EDValRec vis, loc), (env, gs)) + end + in + r + end + val hnormSgn = E.hnormSgn fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan) @@ -2742,17 +2822,6 @@ | _ => str) | _ => str -val makeInstantiable = - let - fun kind k = k - fun con c = - case c of - L'.CDisjoint (L'.LeaveAlone, c1, c2, c) => L'.CDisjoint (L'.Instantiate, c1, c2, c) - | _ => c - in - U.Con.map {kind = kind, con = con} - end - fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = let (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)