Mercurial > urweb

annotate src/unnest.sml @ 1327:1cc67fdac4d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New argument to transactional free functions, to specify whether we are about to retry
author Adam Chlipala <adam@chlipala.net>
date Sat, 04 Dec 2010 11:15:20 -0500
parents b4480a56cab7
children bb942416bf1c
rev   line source
adamc@1272 1 (* Copyright (c) 2008-2010, Adam Chlipala
adamc@448 2 * All rights reserved.
adamc@448 3 *
adamc@448 4 * Redistribution and use in source and binary forms, with or without
adamc@448 5 * modification, are permitted provided that the following conditions are met:
adamc@448 6 *
adamc@448 7 * - Redistributions of source code must retain the above copyright notice,
adamc@448 8 * this list of conditions and the following disclaimer.
adamc@448 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@448 10 * this list of conditions and the following disclaimer in the documentation
adamc@448 11 * and/or other materials provided with the distribution.
adamc@448 12 * - The names of contributors may not be used to endorse or promote products
adamc@448 13 * derived from this software without specific prior written permission.
adamc@448 14 *
adamc@448 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@448 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@448 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@448 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@448 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@448 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@448 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@448 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@448 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@448 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@448 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@448 26 *)
adamc@448 27
adamc@448 28 (* Remove nested function definitions *)
adamc@448 29
adamc@448 30 structure Unnest :> UNNEST = struct
adamc@448 31
adamc@448 32 open Elab
adamc@448 33
adamc@448 34 structure E = ElabEnv
adamc@448 35 structure U = ElabUtil
adamc@448 36
adamc@448 37 structure IS = IntBinarySet
adamc@448 38
adamc@487 39 fun liftExpInExp by =
adamc@623 40 U.Exp.mapB {kind = fn _ => fn k => k,
adamc@487 41 con = fn _ => fn c => c,
adamc@487 42 exp = fn bound => fn e =>
adamc@487 43 case e of
adamc@487 44 ERel xn =>
adamc@487 45 if xn < bound then
adamc@487 46 e
adamc@487 47 else
adamc@487 48 ERel (xn + by)
adamc@487 49 | _ => e,
adamc@487 50 bind = fn (bound, U.Exp.RelE _) => bound + 1
adamc@487 51 | (bound, _) => bound}
adamc@487 52
adamc@487 53 val subExpInExp =
adamc@623 54 U.Exp.mapB {kind = fn _ => fn k => k,
adamc@487 55 con = fn _ => fn c => c,
adamc@487 56 exp = fn (xn, rep) => fn e =>
adamc@487 57 case e of
adamc@487 58 ERel xn' =>
adamc@487 59 if xn' = xn then
adamc@487 60 #1 rep
adamc@487 61 else
adamc@487 62 e
adamc@487 63 | _ => e,
adamc@487 64 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, E.liftExpInExp 0 rep)
adamc@487 65 | ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep)
adamc@487 66 | (ctx, _) => ctx}
adamc@487 67
adamc@623 68 val fvsCon = U.Con.foldB {kind = fn (_, _, st) => st,
adamc@448 69 con = fn (cb, c, cvs) =>
adamc@448 70 case c of
adamc@448 71 CRel n =>
adamc@448 72 if n >= cb then
adamc@448 73 IS.add (cvs, n - cb)
adamc@448 74 else
adamc@448 75 cvs
adamc@448 76 | _ => cvs,
adamc@448 77 bind = fn (cb, b) =>
adamc@448 78 case b of
adamc@623 79 U.Con.RelC _ => cb + 1
adamc@448 80 | _ => cb}
adamc@448 81 0 IS.empty
adamc@448 82
adamc@623 83 fun fvsExp nr = U.Exp.foldB {kind = fn (_, _, st) => st,
adamc@448 84 con = fn ((cb, eb), c, st as (cvs, evs)) =>
adamc@448 85 case c of
adamc@448 86 CRel n =>
adamc@448 87 if n >= cb then
adamc@448 88 (IS.add (cvs, n - cb), evs)
adamc@448 89 else
adamc@448 90 st
adamc@448 91 | _ => st,
adamc@448 92 exp = fn ((cb, eb), e, st as (cvs, evs)) =>
adamc@448 93 case e of
adamc@448 94 ERel n =>
adamc@448 95 if n >= eb then
adamc@448 96 (cvs, IS.add (evs, n - eb))
adamc@448 97 else
adamc@448 98 st
adamc@448 99 | _ => st,
adamc@448 100 bind = fn (ctx as (cb, eb), b) =>
adamc@448 101 case b of
adamc@448 102 U.Exp.RelC _ => (cb + 1, eb)
adamc@448 103 | U.Exp.RelE _ => (cb, eb + 1)
adamc@448 104 | _ => ctx}
adamc@448 105 (0, nr) (IS.empty, IS.empty)
adamc@448 106
adamc@448 107 fun positionOf (x : int) ls =
adamc@448 108 let
adamc@448 109 fun po n ls =
adamc@448 110 case ls of
adamc@448 111 [] => raise Fail "Unnest.positionOf"
adamc@448 112 | x' :: ls' =>
adamc@448 113 if x' = x then
adamc@448 114 n
adamc@448 115 else
adamc@448 116 po (n + 1) ls'
adamc@448 117 in
adamc@448 118 po 0 ls
adamc@487 119 handle Fail _ => raise Fail ("Unnest.positionOf("
adamc@448 120 ^ Int.toString x
adamc@448 121 ^ ", "
adamc@448 122 ^ String.concatWith ";" (map Int.toString ls)
adamc@448 123 ^ ")")
adamc@448 124 end
adamc@448 125
adamc@448 126 fun squishCon cfv =
adamc@623 127 U.Con.mapB {kind = fn _ => fn k => k,
adamc@448 128 con = fn cb => fn c =>
adamc@448 129 case c of
adamc@448 130 CRel n =>
adamc@448 131 if n >= cb then
adamc@448 132 CRel (positionOf (n - cb) cfv + cb)
adamc@448 133 else
adamc@448 134 c
adamc@448 135 | _ => c,
adamc@448 136 bind = fn (cb, b) =>
adamc@448 137 case b of
adamc@623 138 U.Con.RelC _ => cb + 1
adamc@448 139 | _ => cb}
adamc@448 140 0
adamc@448 141
adamc@448 142 fun squishExp (nr, cfv, efv) =
adamc@623 143 U.Exp.mapB {kind = fn _ => fn k => k,
adamc@448 144 con = fn (cb, eb) => fn c =>
adamc@448 145 case c of
adamc@448 146 CRel n =>
adamc@448 147 if n >= cb then
adamc@448 148 CRel (positionOf (n - cb) cfv + cb)
adamc@448 149 else
adamc@448 150 c
adamc@448 151 | _ => c,
adamc@448 152 exp = fn (cb, eb) => fn e =>
adamc@448 153 case e of
adamc@448 154 ERel n =>
adamc@448 155 if n >= eb then
adamc@487 156 ERel (positionOf (n - eb) efv + eb - nr)
adamc@448 157 else
adamc@448 158 e
adamc@448 159 | _ => e,
adamc@448 160 bind = fn (ctx as (cb, eb), b) =>
adamc@448 161 case b of
adamc@448 162 U.Exp.RelC _ => (cb + 1, eb)
adamc@448 163 | U.Exp.RelE _ => (cb, eb + 1)
adamc@448 164 | _ => ctx}
adamc@448 165 (0, nr)
adamc@448 166
adamc@448 167 type state = {
adamc@448 168 maxName : int,
adamc@455 169 decls : (string * int * con * exp) list
adamc@448 170 }
adamc@448 171
adamc@623 172 fun kind (_, k, st) = (k, st)
adamc@448 173
adamc@453 174 fun exp ((ks, ts), e as old, st : state) =
adamc@448 175 case e of
adamc@825 176 ELet (eds, e, t) =>
adamc@448 177 let
adamc@487 178 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
adamc@453 179
adamc@487 180 fun doSubst' (e, subs) = foldl (fn (p, e) => subExpInExp p e) e subs
adamc@448 181
adamc@487 182 fun doSubst (e, subs, by) =
adamc@487 183 let
adamc@487 184 val e = doSubst' (e, subs)
adamc@487 185 in
adamc@487 186 liftExpInExp (~by) (length subs) e
adamc@487 187 end
adamc@487 188
adamc@487 189 val (eds, (ts, maxName, ds, subs, by)) =
adamc@448 190 ListUtil.foldlMapConcat
adamc@487 191 (fn (ed, (ts, maxName, ds, subs, by)) =>
adamc@448 192 case #1 ed of
adamc@825 193 EDVal (p, t, e) =>
adamc@487 194 let
adamc@487 195 val e = doSubst (e, subs, by)
adamc@825 196
adamc@825 197 fun doVars ((p, _), ts) =
adamc@825 198 case p of
adamc@825 199 PWild => ts
adamc@825 200 | PVar xt => xt :: ts
adamc@825 201 | PPrim _ => ts
adamc@825 202 | PCon (_, _, _, NONE) => ts
adamc@825 203 | PCon (_, _, _, SOME p) => doVars (p, ts)
adamc@825 204 | PRecord xpcs =>
adamc@825 205 foldl (fn ((_, p, _), ts) => doVars (p, ts))
adamc@825 206 ts xpcs
adamc@1272 207
adamc@1272 208 fun bindOne subs = ((0, (ERel 0, #2 ed))
adamc@1272 209 :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)
adamc@1272 210
adamc@1272 211 fun bindMany (n, subs) =
adamc@1272 212 case n of
adamc@1272 213 0 => subs
adamc@1272 214 | _ => bindMany (n - 1, bindOne subs)
adamc@487 215 in
adamc@825 216 ([(EDVal (p, t, e), #2 ed)],
adamc@825 217 (doVars (p, ts),
adamc@487 218 maxName, ds,
adamc@1272 219 bindMany (E.patBindsN p, subs),
adamc@487 220 by))
adamc@487 221 end
adamc@448 222 | EDValRec vis =>
adamc@448 223 let
adamc@448 224 val loc = #2 ed
adamc@448 225
adamc@448 226 val nr = length vis
adamc@490 227 val subsLocal = List.filter (fn (_, (ERel _, _)) => false
adamc@490 228 | _ => true) subs
adamc@490 229 val subsLocal = map (fn (n, e) => (n + nr, liftExpInExp nr 0 e))
adamc@490 230 subsLocal
adamc@490 231
adamc@490 232 val vis = map (fn (x, t, e) =>
adamc@490 233 (x, t, doSubst' (e, subsLocal))) vis
adamc@490 234
adamc@448 235 val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) =>
adamc@448 236 let
adamc@448 237 val (cfv', efv') = fvsExp nr e
adamc@448 238 (*val () = Print.prefaces "fvsExp"
adamc@448 239 [("e", ElabPrint.p_exp E.empty e),
adamc@448 240 ("cfv", Print.PD.string
adamc@448 241 (Int.toString (IS.numItems cfv'))),
adamc@448 242 ("efv", Print.PD.string
adamc@448 243 (Int.toString (IS.numItems efv')))]*)
adamc@448 244 val cfv'' = fvsCon t
adamc@448 245 in
adamc@448 246 (IS.union (cfv, IS.union (cfv', cfv'')),
adamc@448 247 IS.union (efv, efv'))
adamc@448 248 end)
adamc@448 249 (IS.empty, IS.empty) vis
adamc@448 250
adamc@826 251 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
adamc@826 252 (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*)
adamc@826 253 (*val () = app (fn (x, t) =>
adamc@453 254 Print.prefaces "Var" [("x", Print.PD.string x),
adamc@826 255 ("t", ElabPrint.p_con E.empty t)]) ts
adamc@826 256 val () = IS.app (fn n => print ("Free: " ^ Int.toString n ^ "\n")) efv*)
adamc@487 257
adamc@448 258 val cfv = IS.foldl (fn (x, cfv) =>
adamc@448 259 let
adamc@448 260 (*val () = print (Int.toString x ^ "\n")*)
adamc@448 261 val (_, t) = List.nth (ts, x)
adamc@448 262 in
adamc@448 263 IS.union (cfv, fvsCon t)
adamc@448 264 end)
adamc@448 265 cfv efv
adamc@448 266 (*val () = print "B\n"*)
adamc@448 267
adamc@448 268 val (vis, maxName) =
adamc@448 269 ListUtil.foldlMap (fn ((x, t, e), maxName) =>
adamc@448 270 ((x, maxName, t, e),
adamc@448 271 maxName + 1))
adamc@448 272 maxName vis
adamc@448 273
adamc@487 274 val subs = map (fn (n, e) => (n + nr,
adamc@487 275 case e of
adamc@487 276 (ERel _, _) => e
adamc@487 277 | _ => liftExpInExp nr 0 e))
adamc@487 278 subs
adamc@487 279
adamc@448 280 val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
adamc@448 281 let
adamc@487 282 val e = (ENamed n, loc)
adamc@487 283
adamc@487 284 val e = IS.foldr (fn (x, e) =>
adamc@487 285 (ECApp (e, (CRel x, loc)), loc))
adamc@487 286 e cfv
adamc@487 287
adamc@487 288 val e = IS.foldr (fn (x, e) =>
adamc@487 289 (EApp (e, (ERel (nr + x), loc)),
adamc@487 290 loc))
adamc@487 291 e efv
adamc@448 292 in
adamc@487 293 (nr - i - 1, e)
adamc@448 294 end)
adamc@450 295 vis
adamc@450 296
adamc@448 297 val cfv = IS.listItems cfv
adamc@448 298 val efv = IS.listItems efv
adamc@448 299
adamc@487 300 val subs = subs' @ subs
adamc@448 301
adamc@448 302 val vis = map (fn (x, n, t, e) =>
adamc@448 303 let
adamc@448 304 (*val () = Print.prefaces "preSubst"
adamc@448 305 [("e", ElabPrint.p_exp E.empty e)]*)
adamc@490 306 val e = doSubst' (e, subs')
adamc@448 307
adamc@448 308 (*val () = Print.prefaces "squishCon"
adamc@448 309 [("t", ElabPrint.p_con E.empty t)]*)
adamc@448 310 val t = squishCon cfv t
adamc@448 311 (*val () = Print.prefaces "squishExp"
adamc@448 312 [("e", ElabPrint.p_exp E.empty e)]*)
adamc@487 313 val e = squishExp (nr, cfv, efv) e
adamc@448 314
adamc@487 315 (*val () = print ("Avail: " ^ Int.toString (length ts) ^ "\n")*)
adamc@453 316 val (e, t) = foldl (fn (ex, (e, t)) =>
adamc@448 317 let
adamc@487 318 (*val () = print (Int.toString ex ^ "\n")*)
adamc@448 319 val (name, t') = List.nth (ts, ex)
adamc@1272 320 val t' = squishCon cfv t'
adamc@448 321 in
adamc@448 322 ((EAbs (name,
adamc@448 323 t',
adamc@448 324 t,
adamc@448 325 e), loc),
adamc@448 326 (TFun (t',
adamc@448 327 t), loc))
adamc@448 328 end)
adamc@448 329 (e, t) efv
adamc@487 330 (*val () = print "Done\n"*)
adamc@448 331
adamc@453 332 val (e, t) = foldl (fn (cx, (e, t)) =>
adamc@448 333 let
adamc@448 334 val (name, k) = List.nth (ks, cx)
adamc@448 335 in
adamc@448 336 ((ECAbs (Explicit,
adamc@448 337 name,
adamc@448 338 k,
adamc@448 339 e), loc),
adamc@448 340 (TCFun (Explicit,
adamc@448 341 name,
adamc@448 342 k,
adamc@448 343 t), loc))
adamc@448 344 end)
adamc@448 345 (e, t) cfv
adamc@448 346 in
adamc@487 347 (*Print.prefaces "Have a vi"
adamc@487 348 [("x", Print.PD.string x),
adamc@487 349 ("e", ElabPrint.p_exp ElabEnv.empty e)];*)
adamc@1017 350 ("$" ^ x, n, t, e)
adamc@448 351 end)
adamc@448 352 vis
adamc@448 353
adamc@487 354 val ts = List.revAppend (map (fn (x, _, t, _) => (x, t)) vis, ts)
adamc@448 355 in
adamc@487 356 ([], (ts, maxName, vis @ ds, subs, by + nr))
adamc@448 357 end)
adamc@487 358 (ts, #maxName st, #decls st, [], 0) eds
adamc@487 359
adamc@487 360 val e' = doSubst (e, subs, by)
adamc@448 361 in
adamc@487 362 (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e),
adamc@487 363 ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))),
adamc@487 364 ("e'", ElabPrint.p_exp ElabEnv.empty e')];*)
adamc@1272 365 (*Print.prefaces "Let" [("Before", ElabPrint.p_exp ElabEnv.empty (old, ErrorMsg.dummySpan)),
adamc@1272 366 ("After", ElabPrint.p_exp ElabEnv.empty (ELet (eds, e', t), ErrorMsg.dummySpan))];*)
adamc@825 367 (ELet (eds, e', t),
adamc@448 368 {maxName = maxName,
adamc@448 369 decls = ds})
adamc@487 370 (*(ELet (eds, doSubst (liftExpInExp (~(length subs - numRemaining)) (length subs) e) subs),*)
adamc@448 371 end
adamc@448 372
adamc@448 373 | _ => (e, st)
adamc@448 374
adamc@448 375 fun default (ctx, d, st) = (d, st)
adamc@448 376
adamc@448 377 fun bind ((ks, ts), b) =
adamc@448 378 case b of
adamc@448 379 U.Decl.RelC p => (p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts)
adamc@448 380 | U.Decl.RelE p => (ks, p :: ts)
adamc@448 381 | _ => (ks, ts)
adamc@448 382
adamc@448 383 val unnestDecl = U.Decl.foldMapB {kind = kind,
adamc@448 384 con = default,
adamc@448 385 exp = exp,
adamc@448 386 sgn_item = default,
adamc@448 387 sgn = default,
adamc@448 388 str = default,
adamc@448 389 decl = default,
adamc@448 390 bind = bind}
adamc@448 391 ([], [])
adamc@448 392
adamc@448 393 fun unnest file =
adamc@448 394 let
adamc@448 395 fun doDecl (all as (d, loc), st : state) =
adamc@448 396 let
adamc@448 397 fun default () = ([all], st)
adamc@448 398 fun explore () =
adamc@448 399 let
adamc@448 400 val (d, st) = unnestDecl st all
adamc@455 401
adamc@455 402 val ds =
adamc@455 403 case #1 d of
adamc@455 404 DValRec vis => [(DValRec (vis @ #decls st), #2 d)]
adamc@455 405 | _ => [(DValRec (#decls st), #2 d), d]
adamc@448 406 in
adamc@455 407 (ds,
adamc@448 408 {maxName = #maxName st,
adamc@448 409 decls = []})
adamc@448 410 end
adamc@448 411 in
adamc@448 412 case d of
adamc@448 413 DCon _ => default ()
adamc@448 414 | DDatatype _ => default ()
adamc@448 415 | DDatatypeImp _ => default ()
adamc@448 416 | DVal _ => explore ()
adamc@448 417 | DValRec _ => explore ()
adamc@448 418 | DSgn _ => default ()
adamc@448 419 | DStr (x, n, sgn, str) =>
adamc@448 420 let
adamc@448 421 val (str, st) = doStr (str, st)
adamc@448 422 in
adamc@448 423 ([(DStr (x, n, sgn, str), loc)], st)
adamc@448 424 end
adamc@448 425 | DFfiStr _ => default ()
adamc@448 426 | DConstraint _ => default ()
adamc@448 427 | DExport _ => default ()
adamc@448 428 | DTable _ => default ()
adamc@448 429 | DSequence _ => default ()
adamc@754 430 | DView _ => default ()
adamc@448 431 | DClass _ => default ()
adamc@448 432 | DDatabase _ => default ()
adamc@459 433 | DCookie _ => default ()
adamc@718 434 | DStyle _ => default ()
adamc@1075 435 | DTask _ => explore ()
adamc@1199 436 | DPolicy _ => explore ()
adam@1294 437 | DOnError _ => default ()
adamc@448 438 end
adamc@448 439
adamc@448 440 and doStr (all as (str, loc), st) =
adamc@448 441 let
adamc@448 442 fun default () = (all, st)
adamc@448 443 in
adamc@448 444 case str of
adamc@448 445 StrConst ds =>
adamc@448 446 let
adamc@448 447 val (ds, st) = ListUtil.foldlMapConcat doDecl st ds
adamc@448 448 in
adamc@448 449 ((StrConst ds, loc), st)
adamc@448 450 end
adamc@448 451 | StrVar _ => default ()
adamc@448 452 | StrProj _ => default ()
adamc@448 453 | StrFun (x, n, dom, ran, str) =>
adamc@448 454 let
adamc@448 455 val (str, st) = doStr (str, st)
adamc@448 456 in
adamc@448 457 ((StrFun (x, n, dom, ran, str), loc), st)
adamc@448 458 end
adamc@448 459 | StrApp _ => default ()
adamc@448 460 | StrError => raise Fail "Unnest: StrError"
adamc@448 461 end
adamc@448 462
adamc@448 463 val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@448 464 {maxName = U.File.maxName file + 1,
adamc@448 465 decls = []} file
adamc@448 466 in
adamc@448 467 ds
adamc@448 468 end
adamc@448 469
adamc@448 470 end