Mercurial > urweb

comparison src/unnest.sml @ 2201:1091227f535a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unnest properly in presence of kind polymorphism
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Dec 2015 13:41:35 -0500
parents 403f0cc65b9c
children
comparison
equal deleted inserted replaced
2200:fc1c89627178 2201:1091227f535a
63 | _ => e, 63 | _ => e,
64 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, E.liftExpInExp 0 rep) 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) 65 | ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep)
66 | (ctx, _) => ctx} 66 | (ctx, _) => ctx}
67 67
68 val fvsCon = U.Con.foldB {kind = fn (_, _, st) => st, 68 val fvsKind = U.Kind.foldB {kind = fn (kb, k, kvs) =>
69 con = fn (cb, c, cvs) => 69 case k of
70 KRel n =>
71 if n >= kb then
72 IS.add (kvs, n - kb)
73 else
74 kvs
75 | _ => kvs,
76 bind = fn (kb, b) => kb + 1}
77 0 IS.empty
78
79 val fvsCon = U.Con.foldB {kind = fn ((kb, _), k, st as (kvs, cvs)) =>
80 case k of
81 KRel n =>
82 if n >= kb then
83 (IS.add (kvs, n - kb), cvs)
84 else
85 st
86 | _ => st,
87 con = fn ((_, cb), c, st as (kvs, cvs)) =>
70 case c of 88 case c of
71 CRel n => 89 CRel n =>
72 if n >= cb then 90 if n >= cb then
73 IS.add (cvs, n - cb) 91 (kvs, IS.add (cvs, n - cb))
74 else 92 else
75 cvs 93 st
76 | _ => cvs, 94 | _ => st,
77 bind = fn (cb, b) => 95 bind = fn (ctx as (kb, cb), b) =>
78 case b of 96 case b of
79 U.Con.RelC _ => cb + 1 97 U.Con.RelK _ => (kb + 1, cb + 1)
80 | _ => cb} 98 | U.Con.RelC _ => (kb, cb + 1)
81 0 IS.empty 99 | _ => ctx}
82 100 (0, 0) (IS.empty, IS.empty)
83 fun fvsExp nr = U.Exp.foldB {kind = fn (_, _, st) => st, 101
84 con = fn ((cb, eb), c, st as (cvs, evs)) => 102 fun fvsExp nr = U.Exp.foldB {kind = fn ((kb, _, _), k, st as (kvs, cvs, evs)) =>
103 case k of
104 KRel n =>
105 if n >= kb then
106 (IS.add (kvs, n - kb), cvs, evs)
107 else
108 st
109 | _ => st,
110 con = fn ((kb, cb, eb), c, st as (kvs, cvs, evs)) =>
85 case c of 111 case c of
86 CRel n => 112 CRel n =>
87 if n >= cb then 113 if n >= cb then
88 (IS.add (cvs, n - cb), evs) 114 (kvs, IS.add (cvs, n - cb), evs)
89 else 115 else
90 st 116 st
91 | _ => st, 117 | _ => st,
92 exp = fn ((cb, eb), e, st as (cvs, evs)) => 118 exp = fn ((kb, cb, eb), e, st as (kvs, cvs, evs)) =>
93 case e of 119 case e of
94 ERel n => 120 ERel n =>
95 if n >= eb then 121 if n >= eb then
96 (cvs, IS.add (evs, n - eb)) 122 (kvs, cvs, IS.add (evs, n - eb))
97 else 123 else
98 st 124 st
99 | _ => st, 125 | _ => st,
100 bind = fn (ctx as (cb, eb), b) => 126 bind = fn (ctx as (kb, cb, eb), b) =>
101 case b of 127 case b of
102 U.Exp.RelC _ => (cb + 1, eb) 128 U.Exp.RelK _ => (kb + 1, cb, eb)
103 | U.Exp.RelE _ => (cb, eb + 1) 129 | U.Exp.RelC _ => (kb, cb + 1, eb)
130 | U.Exp.RelE _ => (kb, cb, eb + 1)
104 | _ => ctx} 131 | _ => ctx}
105 (0, nr) (IS.empty, IS.empty) 132 (0, 0, nr) (IS.empty, IS.empty, IS.empty)
106 133
107 fun positionOf (x : int) ls = 134 fun positionOf (x : int) ls =
108 let 135 let
109 fun po n ls = 136 fun po n ls =
110 case ls of 137 case ls of
121 ^ ", " 148 ^ ", "
122 ^ String.concatWith ";" (map Int.toString ls) 149 ^ String.concatWith ";" (map Int.toString ls)
123 ^ ")") 150 ^ ")")
124 end 151 end
125 152
126 fun squishCon cfv = 153 fun squishCon (kfv, cfv) =
127 U.Con.mapB {kind = fn _ => fn k => k, 154 U.Con.mapB {kind = fn (kb, _) => fn k =>
128 con = fn cb => fn c => 155 case k of
129 case c of 156 KRel n =>
130 CRel n => 157 if n >= kb then
131 if n >= cb then 158 KRel (positionOf (n - kb) kfv + kb)
132 CRel (positionOf (n - cb) cfv + cb) 159 else
133 else 160 k
134 c 161 | _ => k,
135 | _ => c, 162 con = fn (_, cb) => fn c =>
136 bind = fn (cb, b) => 163 case c of
164 CRel n =>
165 if n >= cb then
166 CRel (positionOf (n - cb) cfv + cb)
167 else
168 c
169 | _ => c,
170 bind = fn (ctx as (kb, cb), b) =>
137 case b of 171 case b of
138 U.Con.RelC _ => cb + 1 172 U.Con.RelK _ => (kb + 1, cb)
139 | _ => cb} 173 | U.Con.RelC _ => (kb, cb + 1)
140 0 174 | _ => ctx}
141 175 (0, 0)
142 fun squishExp (nr, cfv, efv) = 176
143 U.Exp.mapB {kind = fn _ => fn k => k, 177 fun squishExp (nr, kfv, cfv, efv) =
144 con = fn (cb, eb) => fn c => 178 U.Exp.mapB {kind = fn (kb, _, _) => fn k =>
145 case c of 179 case k of
146 CRel n => 180 KRel n =>
147 if n >= cb then 181 if n >= kb then
148 CRel (positionOf (n - cb) cfv + cb) 182 KRel (positionOf (n - kb) kfv + kb)
149 else 183 else
150 c 184 k
151 | _ => c, 185 | _ => k,
152 exp = fn (cb, eb) => fn e => 186 con = fn (_, cb, _) => fn c =>
153 case e of 187 case c of
154 ERel n => 188 CRel n =>
155 if n >= eb then 189 if n >= cb then
156 ERel (positionOf (n - eb) efv + eb - nr) 190 CRel (positionOf (n - cb) cfv + cb)
157 else 191 else
158 e 192 c
159 | _ => e, 193 | _ => c,
160 bind = fn (ctx as (cb, eb), b) => 194 exp = fn (_, _, eb) => fn e =>
195 case e of
196 ERel n =>
197 if n >= eb then
198 ERel (positionOf (n - eb) efv + eb - nr)
199 else
200 e
201 | _ => e,
202 bind = fn (ctx as (kb, cb, eb), b) =>
161 case b of 203 case b of
162 U.Exp.RelC _ => (cb + 1, eb) 204 U.Exp.RelK _ => (kb + 1, cb, eb)
163 | U.Exp.RelE _ => (cb, eb + 1) 205 | U.Exp.RelC _ => (kb, cb + 1, eb)
206 | U.Exp.RelE _ => (kb, cb, eb + 1)
164 | _ => ctx} 207 | _ => ctx}
165 (0, nr) 208 (0, 0, nr)
166 209
167 type state = { 210 type state = {
168 maxName : int, 211 maxName : int,
169 decls : (string * int * con * exp) list 212 decls : (string * int * con * exp) list
170 } 213 }
171 214
172 fun kind (_, k, st) = (k, st) 215 fun kind (_, k, st) = (k, st)
173 216
174 val basis = ref 0 217 val basis = ref 0
175 218
176 fun exp ((ks, ts), e as old, st : state) = 219 fun exp ((ns, ks, ts), e as old, st : state) =
177 case e of 220 case e of
178 ELet (eds, e, t) => 221 ELet (eds, e, t) =>
179 let 222 let
180 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) 223 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
181 224
247 subsLocal 290 subsLocal
248 291
249 val vis = map (fn (x, t, e) => 292 val vis = map (fn (x, t, e) =>
250 (x, t, doSubst' (e, subsLocal))) vis 293 (x, t, doSubst' (e, subsLocal))) vis
251 294
252 val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) => 295 val (kfv, cfv, efv) =
253 let 296 foldl (fn ((_, t, e), (kfv, cfv, efv)) =>
254 val (cfv', efv') = fvsExp nr e 297 let
255 (*val () = Print.prefaces "fvsExp" 298 val (kfv', cfv', efv') = fvsExp nr e
256 [("e", ElabPrint.p_exp E.empty e), 299 (*val () = Print.prefaces "fvsExp"
257 ("cfv", Print.PD.string 300 [("e", ElabPrint.p_exp E.empty e),
258 (Int.toString (IS.numItems cfv'))), 301 ("cfv", Print.PD.string
259 ("efv", Print.PD.string 302 (Int.toString (IS.numItems cfv'))),
260 (Int.toString (IS.numItems efv')))]*) 303 ("efv", Print.PD.string
261 val cfv'' = fvsCon t 304 (Int.toString (IS.numItems efv')))]*)
262 in 305 val (kfv'', cfv'') = fvsCon t
263 (IS.union (cfv, IS.union (cfv', cfv'')), 306 in
264 IS.union (efv, efv')) 307 (IS.union (kfv, IS.union (kfv', kfv'')),
265 end) 308 IS.union (cfv, IS.union (cfv', cfv'')),
266 (IS.empty, IS.empty) vis 309 IS.union (efv, efv'))
310 end)
311 (IS.empty, IS.empty, IS.empty) vis
267 312
268 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) 313 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
269 (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*) 314 (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*)
270 (*val () = app (fn (x, t) => 315 (*val () = app (fn (x, t) =>
271 Print.prefaces "Var" [("x", Print.PD.string x), 316 Print.prefaces "Var" [("x", Print.PD.string x),
272 ("t", ElabPrint.p_con E.empty t)]) ts 317 ("t", ElabPrint.p_con E.empty t)]) ts
273 val () = IS.app (fn n => print ("Free: " ^ Int.toString n ^ "\n")) efv*) 318 val () = IS.app (fn n => print ("Free: " ^ Int.toString n ^ "\n")) efv*)
274 319
320 val kfv = IS.foldl (fn (x, kfv) =>
321 let
322 (*val () = print (Int.toString x ^ "\n")*)
323 val (_, k) = List.nth (ks, x)
324 in
325 IS.union (kfv, fvsKind k)
326 end)
327 kfv cfv
328
329 val kfv = IS.foldl (fn (x, kfv) =>
330 let
331 (*val () = print (Int.toString x ^ "\n")*)
332 val (_, t) = List.nth (ts, x)
333 in
334 IS.union (kfv, #1 (fvsCon t))
335 end)
336 kfv efv
337
275 val cfv = IS.foldl (fn (x, cfv) => 338 val cfv = IS.foldl (fn (x, cfv) =>
276 let 339 let
277 (*val () = print (Int.toString x ^ "\n")*) 340 (*val () = print (Int.toString x ^ "\n")*)
278 val (_, t) = List.nth (ts, x) 341 val (_, t) = List.nth (ts, x)
279 in 342 in
280 IS.union (cfv, fvsCon t) 343 IS.union (cfv, #2 (fvsCon t))
281 end) 344 end)
282 cfv efv 345 cfv efv
283 (*val () = print "B\n"*) 346 (*val () = print "B\n"*)
284 347
285 val (vis, maxName) = 348 val (vis, maxName) =
295 subs 358 subs
296 359
297 val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) => 360 val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
298 let 361 let
299 val e = (ENamed n, loc) 362 val e = (ENamed n, loc)
363
364 val e = IS.foldr (fn (x, e) =>
365 (EKApp (e, (KRel x, loc)), loc))
366 e kfv
300 367
301 val e = IS.foldr (fn (x, e) => 368 val e = IS.foldr (fn (x, e) =>
302 (ECApp (e, (CRel x, loc)), loc)) 369 (ECApp (e, (CRel x, loc)), loc))
303 e cfv 370 e cfv
304 371
309 in 376 in
310 (nr - i - 1, e) 377 (nr - i - 1, e)
311 end) 378 end)
312 vis 379 vis
313 380
381 val kfv = IS.listItems kfv
314 val cfv = IS.listItems cfv 382 val cfv = IS.listItems cfv
315 val efv = IS.listItems efv 383 val efv = IS.listItems efv
316 384
317 val subs = subs' @ subs 385 val subs = subs' @ subs
318 386
322 [("e", ElabPrint.p_exp E.empty e)]*) 390 [("e", ElabPrint.p_exp E.empty e)]*)
323 val e = doSubst' (e, subs') 391 val e = doSubst' (e, subs')
324 392
325 (*val () = Print.prefaces "squishCon" 393 (*val () = Print.prefaces "squishCon"
326 [("t", ElabPrint.p_con E.empty t)]*) 394 [("t", ElabPrint.p_con E.empty t)]*)
327 val t = squishCon cfv t 395 val t = squishCon (kfv, cfv) t
328 (*val () = Print.prefaces "squishExp" 396 (*val () = Print.prefaces "squishExp"
329 [("e", ElabPrint.p_exp E.empty e)]*) 397 [("e", ElabPrint.p_exp E.empty e)]*)
330 val e = squishExp (nr, cfv, efv) e 398 val e = squishExp (nr, kfv, cfv, efv) e
331 399
332 (*val () = print ("Avail: " ^ Int.toString (length ts) ^ "\n")*) 400 (*val () = print ("Avail: " ^ Int.toString (length ts) ^ "\n")*)
333 val (e, t) = foldl (fn (ex, (e, t)) => 401 val (e, t) = foldl (fn (ex, (e, t)) =>
334 let 402 let
335 (*val () = print (Int.toString ex ^ "\n")*) 403 (*val () = print (Int.toString ex ^ "\n")*)
336 val (name, t') = List.nth (ts, ex) 404 val (name, t') = List.nth (ts, ex)
337 val t' = squishCon cfv t' 405 val t' = squishCon (kfv, cfv) t'
338 in 406 in
339 ((EAbs (name, 407 ((EAbs (name,
340 t', 408 t',
341 t, 409 t,
342 e), loc), 410 e), loc),
358 name, 426 name,
359 k, 427 k,
360 t), loc)) 428 t), loc))
361 end) 429 end)
362 (e, t) cfv 430 (e, t) cfv
431
432 val (e, t) = foldl (fn (kx, (e, t)) =>
433 let
434 val name = List.nth (ns, kx)
435 in
436 ((EKAbs (name,
437 e), loc),
438 (TKFun (name,
439 t), loc))
440 end)
441 (e, t) kfv
363 in 442 in
364 (*Print.prefaces "Have a vi" 443 (*Print.prefaces "Have a vi"
365 [("x", Print.PD.string x), 444 [("x", Print.PD.string x),
366 ("e", ElabPrint.p_exp ElabEnv.empty e)];*) 445 ("e", ElabPrint.p_exp ElabEnv.empty e)];*)
367 ("$" ^ x, n, t, e) 446 ("$" ^ x, n, t, e)
389 468
390 | _ => (e, st) 469 | _ => (e, st)
391 470
392 fun default (ctx, d, st) = (d, st) 471 fun default (ctx, d, st) = (d, st)
393 472
394 fun bind ((ks, ts), b) = 473 fun bind ((ns, ks, ts), b) =
395 case b of 474 case b of
396 U.Decl.RelC p => (p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts) 475 U.Decl.RelK x => (x :: ns, ks, ts)
397 | U.Decl.RelE p => (ks, p :: ts) 476 | U.Decl.RelC p => (ns, p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts)
398 | _ => (ks, ts) 477 | U.Decl.RelE p => (ns, ks, p :: ts)
478 | _ => (ns, ks, ts)
399 479
400 val unnestDecl = U.Decl.foldMapB {kind = kind, 480 val unnestDecl = U.Decl.foldMapB {kind = kind,
401 con = default, 481 con = default,
402 exp = exp, 482 exp = exp,
403 sgn_item = default, 483 sgn_item = default,
404 sgn = default, 484 sgn = default,
405 str = default, 485 str = default,
406 decl = default, 486 decl = default,
407 bind = bind} 487 bind = bind}
408 ([], []) 488 ([], [], [])
409 489
410 fun unnest file = 490 fun unnest file =
411 let 491 let
412 fun doDecl (all as (d, loc), st : state) = 492 fun doDecl (all as (d, loc), st : state) =
413 let 493 let