Mercurial > urweb

annotate src/unnest.sml @ 1987:fa044101ad99

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Closing old datetime branch.
author Patrick Hurst <phurst@mit.edu>
date Mon, 17 Feb 2014 19:25:30 -0500
parents 5f478ecf65e4
children 403f0cc65b9c
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
adam@1888 174 val basis = ref 0
adam@1888 175
adamc@453 176 fun exp ((ks, ts), e as old, st : state) =
adamc@448 177 case e of
adamc@825 178 ELet (eds, e, t) =>
adamc@448 179 let
adamc@487 180 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
adamc@453 181
adamc@487 182 fun doSubst' (e, subs) = foldl (fn (p, e) => subExpInExp p e) e subs
adamc@448 183
adamc@487 184 fun doSubst (e, subs, by) =
adamc@487 185 let
adamc@487 186 val e = doSubst' (e, subs)
adamc@487 187 in
adamc@487 188 liftExpInExp (~by) (length subs) e
adamc@487 189 end
adamc@487 190
adam@1888 191 fun functionInside (t : con) =
adam@1888 192 case #1 t of
adam@1888 193 TFun _ => true
adam@1888 194 | CApp ((CModProj (basis', [], "transaction"), _), _) => basis' = !basis
adam@1888 195 | _ => false
adam@1888 196
adam@1888 197 val eds = map (fn ed =>
adam@1888 198 case #1 ed of
adam@1888 199 EDVal ((PVar (x, _), _), t, e) =>
adam@1888 200 if functionInside t then
adam@1888 201 (EDValRec [(x, t, E.liftExpInExp 0 e)], #2 ed)
adam@1888 202 else
adam@1888 203 ed
adam@1888 204 | _ => ed) eds
adam@1888 205
adamc@487 206 val (eds, (ts, maxName, ds, subs, by)) =
adamc@448 207 ListUtil.foldlMapConcat
adamc@487 208 (fn (ed, (ts, maxName, ds, subs, by)) =>
adamc@448 209 case #1 ed of
adamc@825 210 EDVal (p, t, e) =>
adamc@487 211 let
adamc@487 212 val e = doSubst (e, subs, by)
adamc@825 213
adamc@825 214 fun doVars ((p, _), ts) =
adamc@825 215 case p of
adamc@825 216 PWild => ts
adamc@825 217 | PVar xt => xt :: ts
adamc@825 218 | PPrim _ => ts
adamc@825 219 | PCon (_, _, _, NONE) => ts
adamc@825 220 | PCon (_, _, _, SOME p) => doVars (p, ts)
adamc@825 221 | PRecord xpcs =>
adamc@825 222 foldl (fn ((_, p, _), ts) => doVars (p, ts))
adamc@825 223 ts xpcs
adamc@1272 224
adamc@1272 225 fun bindOne subs = ((0, (ERel 0, #2 ed))
adamc@1272 226 :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)
adamc@1272 227
adamc@1272 228 fun bindMany (n, subs) =
adamc@1272 229 case n of
adamc@1272 230 0 => subs
adamc@1272 231 | _ => bindMany (n - 1, bindOne subs)
adamc@487 232 in
adamc@825 233 ([(EDVal (p, t, e), #2 ed)],
adamc@825 234 (doVars (p, ts),
adamc@487 235 maxName, ds,
adamc@1272 236 bindMany (E.patBindsN p, subs),
adamc@487 237 by))
adamc@487 238 end
adamc@448 239 | EDValRec vis =>
adamc@448 240 let
adamc@448 241 val loc = #2 ed
adamc@448 242
adamc@448 243 val nr = length vis
adamc@490 244 val subsLocal = List.filter (fn (_, (ERel _, _)) => false
adamc@490 245 | _ => true) subs
adamc@490 246 val subsLocal = map (fn (n, e) => (n + nr, liftExpInExp nr 0 e))
adamc@490 247 subsLocal
adamc@490 248
adamc@490 249 val vis = map (fn (x, t, e) =>
adamc@490 250 (x, t, doSubst' (e, subsLocal))) vis
adamc@490 251
adamc@448 252 val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) =>
adamc@448 253 let
adamc@448 254 val (cfv', efv') = fvsExp nr e
adamc@448 255 (*val () = Print.prefaces "fvsExp"
adamc@448 256 [("e", ElabPrint.p_exp E.empty e),
adamc@448 257 ("cfv", Print.PD.string
adamc@448 258 (Int.toString (IS.numItems cfv'))),
adamc@448 259 ("efv", Print.PD.string
adamc@448 260 (Int.toString (IS.numItems efv')))]*)
adamc@448 261 val cfv'' = fvsCon t
adamc@448 262 in
adamc@448 263 (IS.union (cfv, IS.union (cfv', cfv'')),
adamc@448 264 IS.union (efv, efv'))
adamc@448 265 end)
adamc@448 266 (IS.empty, IS.empty) vis
adamc@448 267
adamc@826 268 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
adamc@826 269 (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*)
adamc@826 270 (*val () = app (fn (x, t) =>
adamc@453 271 Print.prefaces "Var" [("x", Print.PD.string x),
adamc@826 272 ("t", ElabPrint.p_con E.empty t)]) ts
adamc@826 273 val () = IS.app (fn n => print ("Free: " ^ Int.toString n ^ "\n")) efv*)
adamc@487 274
adamc@448 275 val cfv = IS.foldl (fn (x, cfv) =>
adamc@448 276 let
adamc@448 277 (*val () = print (Int.toString x ^ "\n")*)
adamc@448 278 val (_, t) = List.nth (ts, x)
adamc@448 279 in
adamc@448 280 IS.union (cfv, fvsCon t)
adamc@448 281 end)
adamc@448 282 cfv efv
adamc@448 283 (*val () = print "B\n"*)
adamc@448 284
adamc@448 285 val (vis, maxName) =
adamc@448 286 ListUtil.foldlMap (fn ((x, t, e), maxName) =>
adamc@448 287 ((x, maxName, t, e),
adamc@448 288 maxName + 1))
adamc@448 289 maxName vis
adamc@448 290
adamc@487 291 val subs = map (fn (n, e) => (n + nr,
adamc@487 292 case e of
adamc@487 293 (ERel _, _) => e
adamc@487 294 | _ => liftExpInExp nr 0 e))
adamc@487 295 subs
adamc@487 296
adamc@448 297 val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
adamc@448 298 let
adamc@487 299 val e = (ENamed n, loc)
adamc@487 300
adamc@487 301 val e = IS.foldr (fn (x, e) =>
adamc@487 302 (ECApp (e, (CRel x, loc)), loc))
adamc@487 303 e cfv
adamc@487 304
adamc@487 305 val e = IS.foldr (fn (x, e) =>
adamc@487 306 (EApp (e, (ERel (nr + x), loc)),
adamc@487 307 loc))
adamc@487 308 e efv
adamc@448 309 in
adamc@487 310 (nr - i - 1, e)
adamc@448 311 end)
adamc@450 312 vis
adamc@450 313
adamc@448 314 val cfv = IS.listItems cfv
adamc@448 315 val efv = IS.listItems efv
adamc@448 316
adamc@487 317 val subs = subs' @ subs
adamc@448 318
adamc@448 319 val vis = map (fn (x, n, t, e) =>
adamc@448 320 let
adamc@448 321 (*val () = Print.prefaces "preSubst"
adamc@448 322 [("e", ElabPrint.p_exp E.empty e)]*)
adamc@490 323 val e = doSubst' (e, subs')
adamc@448 324
adamc@448 325 (*val () = Print.prefaces "squishCon"
adamc@448 326 [("t", ElabPrint.p_con E.empty t)]*)
adamc@448 327 val t = squishCon cfv t
adamc@448 328 (*val () = Print.prefaces "squishExp"
adamc@448 329 [("e", ElabPrint.p_exp E.empty e)]*)
adamc@487 330 val e = squishExp (nr, cfv, efv) e
adamc@448 331
adamc@487 332 (*val () = print ("Avail: " ^ Int.toString (length ts) ^ "\n")*)
adamc@453 333 val (e, t) = foldl (fn (ex, (e, t)) =>
adamc@448 334 let
adamc@487 335 (*val () = print (Int.toString ex ^ "\n")*)
adamc@448 336 val (name, t') = List.nth (ts, ex)
adamc@1272 337 val t' = squishCon cfv t'
adamc@448 338 in
adamc@448 339 ((EAbs (name,
adamc@448 340 t',
adamc@448 341 t,
adamc@448 342 e), loc),
adamc@448 343 (TFun (t',
adamc@448 344 t), loc))
adamc@448 345 end)
adamc@448 346 (e, t) efv
adamc@487 347 (*val () = print "Done\n"*)
adamc@448 348
adamc@453 349 val (e, t) = foldl (fn (cx, (e, t)) =>
adamc@448 350 let
adamc@448 351 val (name, k) = List.nth (ks, cx)
adamc@448 352 in
adamc@448 353 ((ECAbs (Explicit,
adamc@448 354 name,
adamc@448 355 k,
adamc@448 356 e), loc),
adamc@448 357 (TCFun (Explicit,
adamc@448 358 name,
adamc@448 359 k,
adamc@448 360 t), loc))
adamc@448 361 end)
adamc@448 362 (e, t) cfv
adamc@448 363 in
adamc@487 364 (*Print.prefaces "Have a vi"
adamc@487 365 [("x", Print.PD.string x),
adamc@487 366 ("e", ElabPrint.p_exp ElabEnv.empty e)];*)
adamc@1017 367 ("$" ^ x, n, t, e)
adamc@448 368 end)
adamc@448 369 vis
adamc@448 370
adamc@487 371 val ts = List.revAppend (map (fn (x, _, t, _) => (x, t)) vis, ts)
adamc@448 372 in
adamc@487 373 ([], (ts, maxName, vis @ ds, subs, by + nr))
adamc@448 374 end)
adamc@487 375 (ts, #maxName st, #decls st, [], 0) eds
adamc@487 376
adamc@487 377 val e' = doSubst (e, subs, by)
adamc@448 378 in
adamc@487 379 (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e),
adamc@487 380 ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))),
adamc@487 381 ("e'", ElabPrint.p_exp ElabEnv.empty e')];*)
adamc@1272 382 (*Print.prefaces "Let" [("Before", ElabPrint.p_exp ElabEnv.empty (old, ErrorMsg.dummySpan)),
adamc@1272 383 ("After", ElabPrint.p_exp ElabEnv.empty (ELet (eds, e', t), ErrorMsg.dummySpan))];*)
adamc@825 384 (ELet (eds, e', t),
adamc@448 385 {maxName = maxName,
adamc@448 386 decls = ds})
adamc@487 387 (*(ELet (eds, doSubst (liftExpInExp (~(length subs - numRemaining)) (length subs) e) subs),*)
adamc@448 388 end
adamc@448 389
adamc@448 390 | _ => (e, st)
adamc@448 391
adamc@448 392 fun default (ctx, d, st) = (d, st)
adamc@448 393
adamc@448 394 fun bind ((ks, ts), b) =
adamc@448 395 case b of
adamc@448 396 U.Decl.RelC p => (p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts)
adamc@448 397 | U.Decl.RelE p => (ks, p :: ts)
adamc@448 398 | _ => (ks, ts)
adamc@448 399
adamc@448 400 val unnestDecl = U.Decl.foldMapB {kind = kind,
adamc@448 401 con = default,
adamc@448 402 exp = exp,
adamc@448 403 sgn_item = default,
adamc@448 404 sgn = default,
adamc@448 405 str = default,
adamc@448 406 decl = default,
adamc@448 407 bind = bind}
adamc@448 408 ([], [])
adamc@448 409
adamc@448 410 fun unnest file =
adamc@448 411 let
adamc@448 412 fun doDecl (all as (d, loc), st : state) =
adamc@448 413 let
adamc@448 414 fun default () = ([all], st)
adamc@448 415 fun explore () =
adamc@448 416 let
adamc@448 417 val (d, st) = unnestDecl st all
adamc@455 418
adamc@455 419 val ds =
adamc@455 420 case #1 d of
adamc@455 421 DValRec vis => [(DValRec (vis @ #decls st), #2 d)]
adamc@455 422 | _ => [(DValRec (#decls st), #2 d), d]
adamc@448 423 in
adamc@455 424 (ds,
adamc@448 425 {maxName = #maxName st,
adamc@448 426 decls = []})
adamc@448 427 end
adamc@448 428 in
adamc@448 429 case d of
adamc@448 430 DCon _ => default ()
adamc@448 431 | DDatatype _ => default ()
adamc@448 432 | DDatatypeImp _ => default ()
adamc@448 433 | DVal _ => explore ()
adamc@448 434 | DValRec _ => explore ()
adamc@448 435 | DSgn _ => default ()
adamc@448 436 | DStr (x, n, sgn, str) =>
adamc@448 437 let
adamc@448 438 val (str, st) = doStr (str, st)
adamc@448 439 in
adamc@448 440 ([(DStr (x, n, sgn, str), loc)], st)
adamc@448 441 end
adam@1888 442 | DFfiStr ("Basis", n, _) => (basis := n; default ())
adamc@448 443 | DFfiStr _ => default ()
adamc@448 444 | DConstraint _ => default ()
adamc@448 445 | DExport _ => default ()
adamc@448 446 | DTable _ => default ()
adamc@448 447 | DSequence _ => default ()
adamc@754 448 | DView _ => default ()
adamc@448 449 | DDatabase _ => default ()
adamc@459 450 | DCookie _ => default ()
adamc@718 451 | DStyle _ => default ()
adamc@1075 452 | DTask _ => explore ()
adamc@1199 453 | DPolicy _ => explore ()
adam@1294 454 | DOnError _ => default ()
adamc@448 455 end
adamc@448 456
adamc@448 457 and doStr (all as (str, loc), st) =
adamc@448 458 let
adamc@448 459 fun default () = (all, st)
adamc@448 460 in
adamc@448 461 case str of
adamc@448 462 StrConst ds =>
adamc@448 463 let
adamc@448 464 val (ds, st) = ListUtil.foldlMapConcat doDecl st ds
adamc@448 465 in
adamc@448 466 ((StrConst ds, loc), st)
adamc@448 467 end
adamc@448 468 | StrVar _ => default ()
adamc@448 469 | StrProj _ => default ()
adamc@448 470 | StrFun (x, n, dom, ran, str) =>
adamc@448 471 let
adamc@448 472 val (str, st) = doStr (str, st)
adamc@448 473 in
adamc@448 474 ((StrFun (x, n, dom, ran, str), loc), st)
adamc@448 475 end
adamc@448 476 | StrApp _ => default ()
adamc@448 477 | StrError => raise Fail "Unnest: StrError"
adamc@448 478 end
adamc@448 479
adamc@448 480 val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@448 481 {maxName = U.File.maxName file + 1,
adamc@448 482 decls = []} file
adamc@448 483 in
adamc@448 484 ds
adamc@448 485 end
adamc@448 486
adamc@448 487 end