Mercurial > urweb
changeset 487:33d5bd69da00
Get threadedBlog to work
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 11 Nov 2008 11:49:51 -0500 |
| parents | 8e055bbbd28b |
| children | 5521bb0b4014 |
| files | src/core_print.sml src/elab_env.sig src/especialize.sml src/unnest.sml |
| diffstat | 4 files changed, 111 insertions(+), 42 deletions(-) [+] |
line wrap: on
line diff
--- a/src/core_print.sml Sun Nov 09 18:19:47 2008 -0500 +++ b/src/core_print.sml Tue Nov 11 11:49:51 2008 -0500 @@ -227,7 +227,7 @@ string "(", p_list (p_exp env) es, string "))"] - | EApp (e1, e2) => parenIf par (box [p_exp env e1, + | EApp (e1, e2) => parenIf par (box [p_exp' true env e1, space, p_exp' true env e2]) | EAbs (x, t, _, e) => parenIf par (box [string "fn",
--- a/src/elab_env.sig Sun Nov 09 18:19:47 2008 -0500 +++ b/src/elab_env.sig Tue Nov 11 11:49:51 2008 -0500 @@ -30,6 +30,7 @@ exception SynUnif val liftConInCon : int -> Elab.con -> Elab.con + val liftConInExp : int -> Elab.exp -> Elab.exp val liftExpInExp : int -> Elab.exp -> Elab.exp val subExpInExp : (int * Elab.exp) -> Elab.exp -> Elab.exp
--- a/src/especialize.sml Sun Nov 09 18:19:47 2008 -0500 +++ b/src/especialize.sml Tue Nov 11 11:49:51 2008 -0500 @@ -188,9 +188,14 @@ andalso List.exists (fn (ERecord [], _) => false | _ => true) xs' andalso not (IS.member (actionable, f)) andalso hasFunarg (typ, xs') then - (#1 (foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan)) - body xs'), - st) + let + val e = foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan)) + body xs' + in + (*Print.prefaces "Unfolded" + [("e", CorePrint.p_exp CoreEnv.empty e)];*) + (#1 e, st) + end else (e, st) end) @@ -221,6 +226,9 @@ NONE => (e, st) | SOME (body', typ') => let + (*val () = Print.prefaces "sub'd" + [("body'", CorePrint.p_exp CoreEnv.empty body')]*) + val f' = #maxName st val funcs = IM.insert (#funcs st, f, {name = name, args = KM.insert (args, @@ -234,7 +242,13 @@ decls = #decls st } + (*val () = print ("Created " ^ Int.toString f' ^ " from " + ^ Int.toString f ^ "\n") + val () = Print.prefaces "body'" + [("body'", CorePrint.p_exp CoreEnv.empty body')]*) val (body', st) = specExp st body' + (*val () = Print.prefaces "body''" + [("body'", CorePrint.p_exp CoreEnv.empty body')]*) val e' = foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan)) (ENamed f', ErrorMsg.dummySpan) xs' in @@ -316,6 +330,7 @@ fun specialize file = let + (*val () = Print.prefaces "Intermediate" [("file", CorePrint.p_file CoreEnv.empty file)];*) val (changed, file) = specialize' file in if changed then
--- a/src/unnest.sml Sun Nov 09 18:19:47 2008 -0500 +++ b/src/unnest.sml Tue Nov 11 11:49:51 2008 -0500 @@ -36,6 +36,35 @@ structure IS = IntBinarySet +fun liftExpInExp by = + U.Exp.mapB {kind = fn k => k, + con = fn _ => fn c => c, + exp = fn bound => fn e => + case e of + ERel xn => + if xn < bound then + e + else + ERel (xn + by) + | _ => e, + bind = fn (bound, U.Exp.RelE _) => bound + 1 + | (bound, _) => bound} + +val subExpInExp = + U.Exp.mapB {kind = fn k => k, + con = fn _ => fn c => c, + exp = fn (xn, rep) => fn e => + case e of + ERel xn' => + if xn' = xn then + #1 rep + else + e + | _ => e, + bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, E.liftExpInExp 0 rep) + | ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep) + | (ctx, _) => ctx} + val fvsCon = U.Con.foldB {kind = fn (_, st) => st, con = fn (cb, c, cvs) => case c of @@ -87,7 +116,7 @@ po (n + 1) ls' in po 0 ls - handle Fail _ => raise Fail ("Unnset.positionOf(" + handle Fail _ => raise Fail ("Unnest.positionOf(" ^ Int.toString x ^ ", " ^ String.concatWith ";" (map Int.toString ls) @@ -124,7 +153,7 @@ case e of ERel n => if n >= eb then - ERel (positionOf (n - eb) efv + eb) + ERel (positionOf (n - eb) efv + eb - nr) else e | _ => e, @@ -146,17 +175,32 @@ case e of ELet (eds, e) => let - (*val () = Print.prefaces "let" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) + (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) - val doSubst = foldl (fn (p, e) => E.subExpInExp p e) + fun doSubst' (e, subs) = foldl (fn (p, e) => subExpInExp p e) e subs - val (eds, (ts, maxName, ds, subs)) = + fun doSubst (e, subs, by) = + let + val e = doSubst' (e, subs) + in + liftExpInExp (~by) (length subs) e + end + + val (eds, (ts, maxName, ds, subs, by)) = ListUtil.foldlMapConcat - (fn (ed, (ts, maxName, ds, subs)) => + (fn (ed, (ts, maxName, ds, subs, by)) => case #1 ed of - EDVal (x, t, _) => ([ed], - ((x, t) :: ts, - maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)) + EDVal (x, t, e) => + let + val e = doSubst (e, subs, by) + in + ([(EDVal (x, t, e), #2 ed)], + ((x, t) :: ts, + maxName, ds, + ((0, (ERel 0, #2 ed)) + :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs), + by)) + end | EDValRec vis => let val loc = #2 ed @@ -182,6 +226,7 @@ val () = app (fn (x, t) => Print.prefaces "Var" [("x", Print.PD.string x), ("t", ElabPrint.p_con E.empty t)]) ts*) + val cfv = IS.foldl (fn (x, cfv) => let (*val () = print (Int.toString x ^ "\n")*) @@ -198,56 +243,54 @@ maxName + 1)) maxName vis - fun apply e = - let - val e = IS.foldr (fn (x, e) => - (ECApp (e, (CRel x, loc)), loc)) - e cfv - in - IS.foldr (fn (x, e) => - (EApp (e, (ERel x, loc)), loc)) - e efv - end - val subs = map (fn (n, e) => (n + nr, E.liftExpInExp nr e)) subs + + val subs = map (fn (n, e) => (n + nr, + case e of + (ERel _, _) => e + | _ => liftExpInExp nr 0 e)) + subs + val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) => let - val dummy = (EError, ErrorMsg.dummySpan) - - fun repeatLift k = - if k = 0 then - apply (ENamed n, loc) - else - E.liftExpInExp 0 (repeatLift (k - 1)) + val e = (ENamed n, loc) + + val e = IS.foldr (fn (x, e) => + (ECApp (e, (CRel x, loc)), loc)) + e cfv + + val e = IS.foldr (fn (x, e) => + (EApp (e, (ERel (nr + x), loc)), + loc)) + e efv in - (0, repeatLift i) + (nr - i - 1, e) end) vis - val subs' = rev subs' - val cfv = IS.listItems cfv val efv = IS.listItems efv - val efn = length efv - val subs = subs @ subs' + val subs = subs' @ subs val vis = map (fn (x, n, t, e) => let (*val () = Print.prefaces "preSubst" [("e", ElabPrint.p_exp E.empty e)]*) - val e = doSubst e subs + val e = doSubst' (e, subs) (*val () = Print.prefaces "squishCon" [("t", ElabPrint.p_con E.empty t)]*) val t = squishCon cfv t (*val () = Print.prefaces "squishExp" [("e", ElabPrint.p_exp E.empty e)]*) - val e = squishExp (0(*nr*), cfv, efv) e + val e = squishExp (nr, cfv, efv) e + (*val () = print ("Avail: " ^ Int.toString (length ts) ^ "\n")*) val (e, t) = foldl (fn (ex, (e, t)) => let + (*val () = print (Int.toString ex ^ "\n")*) val (name, t') = List.nth (ts, ex) in ((EAbs (name, @@ -258,6 +301,7 @@ t), loc)) end) (e, t) efv + (*val () = print "Done\n"*) val (e, t) = foldl (fn (cx, (e, t)) => let @@ -274,19 +318,28 @@ end) (e, t) cfv in + (*Print.prefaces "Have a vi" + [("x", Print.PD.string x), + ("e", ElabPrint.p_exp ElabEnv.empty e)];*) (x, n, t, e) end) vis - val ts = map (fn (x, _, t, _) => (x, t)) vis @ ts + val ts = List.revAppend (map (fn (x, _, t, _) => (x, t)) vis, ts) in - ([], (ts, maxName, vis @ ds, subs)) + ([], (ts, maxName, vis @ ds, subs, by + nr)) end) - (ts, #maxName st, #decls st, []) eds + (ts, #maxName st, #decls st, [], 0) eds + + val e' = doSubst (e, subs, by) in - (ELet (eds, doSubst e subs), + (*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'), {maxName = maxName, decls = ds}) + (*(ELet (eds, doSubst (liftExpInExp (~(length subs - numRemaining)) (length subs) e) subs),*) end | _ => (e, st)