diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-11-11 16:27:51 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-11-11 16:27:51 -0500 |
| commit | 2fe3fd104e8a4de9810e450d6d2e166f5534b360 (patch) | |
| tree | dfc7ea6b8feefe15f51e0581c1556cbf85763c2d /src | |
| parent | ecbd0aad2d719dd9b92362befe42d63ceacc5d56 (diff) | |
More ThreadedBlog progress
Diffstat (limited to 'src')
| -rw-r--r-- | src/monoize.sml | 2 | ||||
| -rw-r--r-- | 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)]*) |