Mercurial > urweb

annotate src/unnest.sml @ 2063:83bdb52962c9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Check realloc's return code to prevent segfault on out of memoty condition
author Sergey Mironov <grrwlf@gmail.com>
date Sat, 23 Aug 2014 11:59:34 +0000
parents 403f0cc65b9c
children 1091227f535a
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 ()
adam@2010 455 | DFfi _ => default ()
adamc@448 456 end
adamc@448 457
adamc@448 458 and doStr (all as (str, loc), st) =
adamc@448 459 let
adamc@448 460 fun default () = (all, st)
adamc@448 461 in
adamc@448 462 case str of
adamc@448 463 StrConst ds =>
adamc@448 464 let
adamc@448 465 val (ds, st) = ListUtil.foldlMapConcat doDecl st ds
adamc@448 466 in
adamc@448 467 ((StrConst ds, loc), st)
adamc@448 468 end
adamc@448 469 | StrVar _ => default ()
adamc@448 470 | StrProj _ => default ()
adamc@448 471 | StrFun (x, n, dom, ran, str) =>
adamc@448 472 let
adamc@448 473 val (str, st) = doStr (str, st)
adamc@448 474 in
adamc@448 475 ((StrFun (x, n, dom, ran, str), loc), st)
adamc@448 476 end
adamc@448 477 | StrApp _ => default ()
adamc@448 478 | StrError => raise Fail "Unnest: StrError"
adamc@448 479 end
adamc@448 480
adamc@448 481 val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@448 482 {maxName = U.File.maxName file + 1,
adamc@448 483 decls = []} file
adamc@448 484 in
adamc@448 485 ds
adamc@448 486 end
adamc@448 487
adamc@448 488 end