Mercurial > urweb

comparison src/unnest.sml @ 487:33d5bd69da00

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Get threadedBlog to work
author Adam Chlipala <adamc@hcoop.net>
date Tue, 11 Nov 2008 11:49:51 -0500
parents f542bc3133dc
children 366676f7bc88
comparison
equal deleted inserted replaced
486:8e055bbbd28b 487:33d5bd69da00
34 structure E = ElabEnv 34 structure E = ElabEnv
35 structure U = ElabUtil 35 structure U = ElabUtil
36 36
37 structure IS = IntBinarySet 37 structure IS = IntBinarySet
38 38
39 fun liftExpInExp by =
40 U.Exp.mapB {kind = fn k => k,
41 con = fn _ => fn c => c,
42 exp = fn bound => fn e =>
43 case e of
44 ERel xn =>
45 if xn < bound then
46 e
47 else
48 ERel (xn + by)
49 | _ => e,
50 bind = fn (bound, U.Exp.RelE _) => bound + 1
51 | (bound, _) => bound}
52
53 val subExpInExp =
54 U.Exp.mapB {kind = fn k => k,
55 con = fn _ => fn c => c,
56 exp = fn (xn, rep) => fn e =>
57 case e of
58 ERel xn' =>
59 if xn' = xn then
60 #1 rep
61 else
62 e
63 | _ => e,
64 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, E.liftExpInExp 0 rep)
65 | ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep)
66 | (ctx, _) => ctx}
67
39 val fvsCon = U.Con.foldB {kind = fn (_, st) => st, 68 val fvsCon = U.Con.foldB {kind = fn (_, st) => st,
40 con = fn (cb, c, cvs) => 69 con = fn (cb, c, cvs) =>
41 case c of 70 case c of
42 CRel n => 71 CRel n =>
43 if n >= cb then 72 if n >= cb then
85 n 114 n
86 else 115 else
87 po (n + 1) ls' 116 po (n + 1) ls'
88 in 117 in
89 po 0 ls 118 po 0 ls
90 handle Fail _ => raise Fail ("Unnset.positionOf(" 119 handle Fail _ => raise Fail ("Unnest.positionOf("
91 ^ Int.toString x 120 ^ Int.toString x
92 ^ ", " 121 ^ ", "
93 ^ String.concatWith ";" (map Int.toString ls) 122 ^ String.concatWith ";" (map Int.toString ls)
94 ^ ")") 123 ^ ")")
95 end 124 end
122 | _ => c, 151 | _ => c,
123 exp = fn (cb, eb) => fn e => 152 exp = fn (cb, eb) => fn e =>
124 case e of 153 case e of
125 ERel n => 154 ERel n =>
126 if n >= eb then 155 if n >= eb then
127 ERel (positionOf (n - eb) efv + eb) 156 ERel (positionOf (n - eb) efv + eb - nr)
128 else 157 else
129 e 158 e
130 | _ => e, 159 | _ => e,
131 bind = fn (ctx as (cb, eb), b) => 160 bind = fn (ctx as (cb, eb), b) =>
132 case b of 161 case b of
144 173
145 fun exp ((ks, ts), e as old, st : state) = 174 fun exp ((ks, ts), e as old, st : state) =
146 case e of 175 case e of
147 ELet (eds, e) => 176 ELet (eds, e) =>
148 let 177 let
149 (*val () = Print.prefaces "let" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) 178 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
150 179
151 val doSubst = foldl (fn (p, e) => E.subExpInExp p e) 180 fun doSubst' (e, subs) = foldl (fn (p, e) => subExpInExp p e) e subs
152 181
153 val (eds, (ts, maxName, ds, subs)) = 182 fun doSubst (e, subs, by) =
183 let
184 val e = doSubst' (e, subs)
185 in
186 liftExpInExp (~by) (length subs) e
187 end
188
189 val (eds, (ts, maxName, ds, subs, by)) =
154 ListUtil.foldlMapConcat 190 ListUtil.foldlMapConcat
155 (fn (ed, (ts, maxName, ds, subs)) => 191 (fn (ed, (ts, maxName, ds, subs, by)) =>
156 case #1 ed of 192 case #1 ed of
157 EDVal (x, t, _) => ([ed], 193 EDVal (x, t, e) =>
158 ((x, t) :: ts, 194 let
159 maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)) 195 val e = doSubst (e, subs, by)
196 in
197 ([(EDVal (x, t, e), #2 ed)],
198 ((x, t) :: ts,
199 maxName, ds,
200 ((0, (ERel 0, #2 ed))
201 :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs),
202 by))
203 end
160 | EDValRec vis => 204 | EDValRec vis =>
161 let 205 let
162 val loc = #2 ed 206 val loc = #2 ed
163 207
164 val nr = length vis 208 val nr = length vis
180 224
181 (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n") 225 (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")
182 val () = app (fn (x, t) => 226 val () = app (fn (x, t) =>
183 Print.prefaces "Var" [("x", Print.PD.string x), 227 Print.prefaces "Var" [("x", Print.PD.string x),
184 ("t", ElabPrint.p_con E.empty t)]) ts*) 228 ("t", ElabPrint.p_con E.empty t)]) ts*)
229
185 val cfv = IS.foldl (fn (x, cfv) => 230 val cfv = IS.foldl (fn (x, cfv) =>
186 let 231 let
187 (*val () = print (Int.toString x ^ "\n")*) 232 (*val () = print (Int.toString x ^ "\n")*)
188 val (_, t) = List.nth (ts, x) 233 val (_, t) = List.nth (ts, x)
189 in 234 in
196 ListUtil.foldlMap (fn ((x, t, e), maxName) => 241 ListUtil.foldlMap (fn ((x, t, e), maxName) =>
197 ((x, maxName, t, e), 242 ((x, maxName, t, e),
198 maxName + 1)) 243 maxName + 1))
199 maxName vis 244 maxName vis
200 245
201 fun apply e = 246
202 let 247
203 val e = IS.foldr (fn (x, e) => 248 val subs = map (fn (n, e) => (n + nr,
204 (ECApp (e, (CRel x, loc)), loc)) 249 case e of
205 e cfv 250 (ERel _, _) => e
206 in 251 | _ => liftExpInExp nr 0 e))
207 IS.foldr (fn (x, e) => 252 subs
208 (EApp (e, (ERel x, loc)), loc)) 253
209 e efv
210 end
211
212 val subs = map (fn (n, e) => (n + nr, E.liftExpInExp nr e)) subs
213 254
214 val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) => 255 val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
215 let 256 let
216 val dummy = (EError, ErrorMsg.dummySpan) 257 val e = (ENamed n, loc)
217 258
218 fun repeatLift k = 259 val e = IS.foldr (fn (x, e) =>
219 if k = 0 then 260 (ECApp (e, (CRel x, loc)), loc))
220 apply (ENamed n, loc) 261 e cfv
221 else 262
222 E.liftExpInExp 0 (repeatLift (k - 1)) 263 val e = IS.foldr (fn (x, e) =>
264 (EApp (e, (ERel (nr + x), loc)),
265 loc))
266 e efv
223 in 267 in
224 (0, repeatLift i) 268 (nr - i - 1, e)
225 end) 269 end)
226 vis 270 vis
227 271
228 val subs' = rev subs'
229
230 val cfv = IS.listItems cfv 272 val cfv = IS.listItems cfv
231 val efv = IS.listItems efv 273 val efv = IS.listItems efv
232 val efn = length efv 274
233 275 val subs = subs' @ subs
234 val subs = subs @ subs'
235 276
236 val vis = map (fn (x, n, t, e) => 277 val vis = map (fn (x, n, t, e) =>
237 let 278 let
238 (*val () = Print.prefaces "preSubst" 279 (*val () = Print.prefaces "preSubst"
239 [("e", ElabPrint.p_exp E.empty e)]*) 280 [("e", ElabPrint.p_exp E.empty e)]*)
240 val e = doSubst e subs 281 val e = doSubst' (e, subs)
241 282
242 (*val () = Print.prefaces "squishCon" 283 (*val () = Print.prefaces "squishCon"
243 [("t", ElabPrint.p_con E.empty t)]*) 284 [("t", ElabPrint.p_con E.empty t)]*)
244 val t = squishCon cfv t 285 val t = squishCon cfv t
245 (*val () = Print.prefaces "squishExp" 286 (*val () = Print.prefaces "squishExp"
246 [("e", ElabPrint.p_exp E.empty e)]*) 287 [("e", ElabPrint.p_exp E.empty e)]*)
247 val e = squishExp (0(*nr*), cfv, efv) e 288 val e = squishExp (nr, cfv, efv) e
248 289
290 (*val () = print ("Avail: " ^ Int.toString (length ts) ^ "\n")*)
249 val (e, t) = foldl (fn (ex, (e, t)) => 291 val (e, t) = foldl (fn (ex, (e, t)) =>
250 let 292 let
293 (*val () = print (Int.toString ex ^ "\n")*)
251 val (name, t') = List.nth (ts, ex) 294 val (name, t') = List.nth (ts, ex)
252 in 295 in
253 ((EAbs (name, 296 ((EAbs (name,
254 t', 297 t',
255 t, 298 t,
256 e), loc), 299 e), loc),
257 (TFun (t', 300 (TFun (t',
258 t), loc)) 301 t), loc))
259 end) 302 end)
260 (e, t) efv 303 (e, t) efv
304 (*val () = print "Done\n"*)
261 305
262 val (e, t) = foldl (fn (cx, (e, t)) => 306 val (e, t) = foldl (fn (cx, (e, t)) =>
263 let 307 let
264 val (name, k) = List.nth (ks, cx) 308 val (name, k) = List.nth (ks, cx)
265 in 309 in
272 k, 316 k,
273 t), loc)) 317 t), loc))
274 end) 318 end)
275 (e, t) cfv 319 (e, t) cfv
276 in 320 in
321 (*Print.prefaces "Have a vi"
322 [("x", Print.PD.string x),
323 ("e", ElabPrint.p_exp ElabEnv.empty e)];*)
277 (x, n, t, e) 324 (x, n, t, e)
278 end) 325 end)
279 vis 326 vis
280 327
281 val ts = map (fn (x, _, t, _) => (x, t)) vis @ ts 328 val ts = List.revAppend (map (fn (x, _, t, _) => (x, t)) vis, ts)
282 in 329 in
283 ([], (ts, maxName, vis @ ds, subs)) 330 ([], (ts, maxName, vis @ ds, subs, by + nr))
284 end) 331 end)
285 (ts, #maxName st, #decls st, []) eds 332 (ts, #maxName st, #decls st, [], 0) eds
333
334 val e' = doSubst (e, subs, by)
286 in 335 in
287 (ELet (eds, doSubst e subs), 336 (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e),
337 ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))),
338 ("e'", ElabPrint.p_exp ElabEnv.empty e')];*)
339 (ELet (eds, e'),
288 {maxName = maxName, 340 {maxName = maxName,
289 decls = ds}) 341 decls = ds})
342 (*(ELet (eds, doSubst (liftExpInExp (~(length subs - numRemaining)) (length subs) e) subs),*)
290 end 343 end
291 344
292 | _ => (e, st) 345 | _ => (e, st)
293 346
294 fun default (ctx, d, st) = (d, st) 347 fun default (ctx, d, st) = (d, st)