From 2fe3fd104e8a4de9810e450d6d2e166f5534b360 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 11 Nov 2008 16:27:51 -0500 Subject: More ThreadedBlog progress --- src/monoize.sml | 2 +- src/unnest.sml | 13 +++++++++---- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/monoize.sml b/src/monoize.sml index ee509f52..a4f38dc6 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -406,7 +406,7 @@ fun fooifyExp fk env = fm) end - | _ => (E.errorAt loc "Don't know how to encode attribute type"; + | _ => (E.errorAt loc "Don't know how to encode attribute/URL type"; Print.eprefaces' [("Type", MonoPrint.p_typ MonoEnv.empty tAll)]; (dummyExp, fm)) in diff --git a/src/unnest.sml b/src/unnest.sml index fe63f9fe..8e363301 100644 --- a/src/unnest.sml +++ b/src/unnest.sml @@ -206,6 +206,14 @@ fun exp ((ks, ts), e as old, st : state) = val loc = #2 ed val nr = length vis + val subsLocal = List.filter (fn (_, (ERel _, _)) => false + | _ => true) subs + val subsLocal = map (fn (n, e) => (n + nr, liftExpInExp nr 0 e)) + subsLocal + + val vis = map (fn (x, t, e) => + (x, t, doSubst' (e, subsLocal))) vis + val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) => let val (cfv', efv') = fvsExp nr e @@ -243,15 +251,12 @@ fun exp ((ks, ts), e as old, st : state) = maxName + 1)) maxName vis - - 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 e = (ENamed n, loc) @@ -278,7 +283,7 @@ fun exp ((ks, ts), e as old, st : state) = 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)]*) -- cgit v1.2.3