Mercurial > urweb

annotate 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
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
adam@2201 68 val fvsKind = U.Kind.foldB {kind = fn (kb, k, kvs) =>
adam@2201 69 case k of
adam@2201 70 KRel n =>
adam@2201 71 if n >= kb then
adam@2201 72 IS.add (kvs, n - kb)
adam@2201 73 else
adam@2201 74 kvs
adam@2201 75 | _ => kvs,
adam@2201 76 bind = fn (kb, b) => kb + 1}
adam@2201 77 0 IS.empty
adam@2201 78
adam@2201 79 val fvsCon = U.Con.foldB {kind = fn ((kb, _), k, st as (kvs, cvs)) =>
adam@2201 80 case k of
adam@2201 81 KRel n =>
adam@2201 82 if n >= kb then
adam@2201 83 (IS.add (kvs, n - kb), cvs)
adam@2201 84 else
adam@2201 85 st
adam@2201 86 | _ => st,
adam@2201 87 con = fn ((_, cb), c, st as (kvs, cvs)) =>
adamc@448 88 case c of
adamc@448 89 CRel n =>
adamc@448 90 if n >= cb then
adam@2201 91 (kvs, IS.add (cvs, n - cb))
adamc@448 92 else
adam@2201 93 st
adam@2201 94 | _ => st,
adam@2201 95 bind = fn (ctx as (kb, cb), b) =>
adamc@448 96 case b of
adam@2201 97 U.Con.RelK _ => (kb + 1, cb + 1)
adam@2201 98 | U.Con.RelC _ => (kb, cb + 1)
adam@2201 99 | _ => ctx}
adam@2201 100 (0, 0) (IS.empty, IS.empty)
adamc@448 101
adam@2201 102 fun fvsExp nr = U.Exp.foldB {kind = fn ((kb, _, _), k, st as (kvs, cvs, evs)) =>
adam@2201 103 case k of
adam@2201 104 KRel n =>
adam@2201 105 if n >= kb then
adam@2201 106 (IS.add (kvs, n - kb), cvs, evs)
adam@2201 107 else
adam@2201 108 st
adam@2201 109 | _ => st,
adam@2201 110 con = fn ((kb, cb, eb), c, st as (kvs, cvs, evs)) =>
adamc@448 111 case c of
adamc@448 112 CRel n =>
adamc@448 113 if n >= cb then
adam@2201 114 (kvs, IS.add (cvs, n - cb), evs)
adamc@448 115 else
adamc@448 116 st
adamc@448 117 | _ => st,
adam@2201 118 exp = fn ((kb, cb, eb), e, st as (kvs, cvs, evs)) =>
adamc@448 119 case e of
adamc@448 120 ERel n =>
adamc@448 121 if n >= eb then
adam@2201 122 (kvs, cvs, IS.add (evs, n - eb))
adamc@448 123 else
adamc@448 124 st
adamc@448 125 | _ => st,
adam@2201 126 bind = fn (ctx as (kb, cb, eb), b) =>
adamc@448 127 case b of
adam@2201 128 U.Exp.RelK _ => (kb + 1, cb, eb)
adam@2201 129 | U.Exp.RelC _ => (kb, cb + 1, eb)
adam@2201 130 | U.Exp.RelE _ => (kb, cb, eb + 1)
adamc@448 131 | _ => ctx}
adam@2201 132 (0, 0, nr) (IS.empty, IS.empty, IS.empty)
adamc@448 133
adamc@448 134 fun positionOf (x : int) ls =
adamc@448 135 let
adamc@448 136 fun po n ls =
adamc@448 137 case ls of
adamc@448 138 [] => raise Fail "Unnest.positionOf"
adamc@448 139 | x' :: ls' =>
adamc@448 140 if x' = x then
adamc@448 141 n
adamc@448 142 else
adamc@448 143 po (n + 1) ls'
adamc@448 144 in
adamc@448 145 po 0 ls
adamc@487 146 handle Fail _ => raise Fail ("Unnest.positionOf("
adamc@448 147 ^ Int.toString x
adamc@448 148 ^ ", "
adamc@448 149 ^ String.concatWith ";" (map Int.toString ls)
adamc@448 150 ^ ")")
adamc@448 151 end
adamc@448 152
adam@2201 153 fun squishCon (kfv, cfv) =
adam@2201 154 U.Con.mapB {kind = fn (kb, _) => fn k =>
adam@2201 155 case k of
adam@2201 156 KRel n =>
adam@2201 157 if n >= kb then
adam@2201 158 KRel (positionOf (n - kb) kfv + kb)
adam@2201 159 else
adam@2201 160 k
adam@2201 161 | _ => k,
adam@2201 162 con = fn (_, cb) => fn c =>
adam@2201 163 case c of
adam@2201 164 CRel n =>
adam@2201 165 if n >= cb then
adam@2201 166 CRel (positionOf (n - cb) cfv + cb)
adam@2201 167 else
adam@2201 168 c
adam@2201 169 | _ => c,
adam@2201 170 bind = fn (ctx as (kb, cb), b) =>
adamc@448 171 case b of
adam@2201 172 U.Con.RelK _ => (kb + 1, cb)
adam@2201 173 | U.Con.RelC _ => (kb, cb + 1)
adam@2201 174 | _ => ctx}
adam@2201 175 (0, 0)
adamc@448 176
adam@2201 177 fun squishExp (nr, kfv, cfv, efv) =
adam@2201 178 U.Exp.mapB {kind = fn (kb, _, _) => fn k =>
adam@2201 179 case k of
adam@2201 180 KRel n =>
adam@2201 181 if n >= kb then
adam@2201 182 KRel (positionOf (n - kb) kfv + kb)
adam@2201 183 else
adam@2201 184 k
adam@2201 185 | _ => k,
adam@2201 186 con = fn (_, cb, _) => fn c =>
adam@2201 187 case c of
adam@2201 188 CRel n =>
adam@2201 189 if n >= cb then
adam@2201 190 CRel (positionOf (n - cb) cfv + cb)
adam@2201 191 else
adam@2201 192 c
adam@2201 193 | _ => c,
adam@2201 194 exp = fn (_, _, eb) => fn e =>
adam@2201 195 case e of
adam@2201 196 ERel n =>
adam@2201 197 if n >= eb then
adam@2201 198 ERel (positionOf (n - eb) efv + eb - nr)
adam@2201 199 else
adam@2201 200 e
adam@2201 201 | _ => e,
adam@2201 202 bind = fn (ctx as (kb, cb, eb), b) =>
adamc@448 203 case b of
adam@2201 204 U.Exp.RelK _ => (kb + 1, cb, eb)
adam@2201 205 | U.Exp.RelC _ => (kb, cb + 1, eb)
adam@2201 206 | U.Exp.RelE _ => (kb, cb, eb + 1)
adamc@448 207 | _ => ctx}
adam@2201 208 (0, 0, nr)
adamc@448 209
adamc@448 210 type state = {
adamc@448 211 maxName : int,
adamc@455 212 decls : (string * int * con * exp) list
adamc@448 213 }
adamc@448 214
adamc@623 215 fun kind (_, k, st) = (k, st)
adamc@448 216
adam@1888 217 val basis = ref 0
adam@1888 218
adam@2201 219 fun exp ((ns, ks, ts), e as old, st : state) =
adamc@448 220 case e of
adamc@825 221 ELet (eds, e, t) =>
adamc@448 222 let
adamc@487 223 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
adamc@453 224
adamc@487 225 fun doSubst' (e, subs) = foldl (fn (p, e) => subExpInExp p e) e subs
adamc@448 226
adamc@487 227 fun doSubst (e, subs, by) =
adamc@487 228 let
adamc@487 229 val e = doSubst' (e, subs)
adamc@487 230 in
adamc@487 231 liftExpInExp (~by) (length subs) e
adamc@487 232 end
adamc@487 233
adam@1888 234 fun functionInside (t : con) =
adam@1888 235 case #1 t of
adam@1888 236 TFun _ => true
adam@1888 237 | CApp ((CModProj (basis', [], "transaction"), _), _) => basis' = !basis
adam@1888 238 | _ => false
adam@1888 239
adam@1888 240 val eds = map (fn ed =>
adam@1888 241 case #1 ed of
adam@1888 242 EDVal ((PVar (x, _), _), t, e) =>
adam@1888 243 if functionInside t then
adam@1888 244 (EDValRec [(x, t, E.liftExpInExp 0 e)], #2 ed)
adam@1888 245 else
adam@1888 246 ed
adam@1888 247 | _ => ed) eds
adam@1888 248
adamc@487 249 val (eds, (ts, maxName, ds, subs, by)) =
adamc@448 250 ListUtil.foldlMapConcat
adamc@487 251 (fn (ed, (ts, maxName, ds, subs, by)) =>
adamc@448 252 case #1 ed of
adamc@825 253 EDVal (p, t, e) =>
adamc@487 254 let
adamc@487 255 val e = doSubst (e, subs, by)
adamc@825 256
adamc@825 257 fun doVars ((p, _), ts) =
adamc@825 258 case p of
adamc@825 259 PWild => ts
adamc@825 260 | PVar xt => xt :: ts
adamc@825 261 | PPrim _ => ts
adamc@825 262 | PCon (_, _, _, NONE) => ts
adamc@825 263 | PCon (_, _, _, SOME p) => doVars (p, ts)
adamc@825 264 | PRecord xpcs =>
adamc@825 265 foldl (fn ((_, p, _), ts) => doVars (p, ts))
adamc@825 266 ts xpcs
adamc@1272 267
adamc@1272 268 fun bindOne subs = ((0, (ERel 0, #2 ed))
adamc@1272 269 :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)
adamc@1272 270
adamc@1272 271 fun bindMany (n, subs) =
adamc@1272 272 case n of
adamc@1272 273 0 => subs
adamc@1272 274 | _ => bindMany (n - 1, bindOne subs)
adamc@487 275 in
adamc@825 276 ([(EDVal (p, t, e), #2 ed)],
adamc@825 277 (doVars (p, ts),
adamc@487 278 maxName, ds,
adamc@1272 279 bindMany (E.patBindsN p, subs),
adamc@487 280 by))
adamc@487 281 end
adamc@448 282 | EDValRec vis =>
adamc@448 283 let
adamc@448 284 val loc = #2 ed
adamc@448 285
adamc@448 286 val nr = length vis
adamc@490 287 val subsLocal = List.filter (fn (_, (ERel _, _)) => false
adamc@490 288 | _ => true) subs
adamc@490 289 val subsLocal = map (fn (n, e) => (n + nr, liftExpInExp nr 0 e))
adamc@490 290 subsLocal
adamc@490 291
adamc@490 292 val vis = map (fn (x, t, e) =>
adamc@490 293 (x, t, doSubst' (e, subsLocal))) vis
adamc@490 294
adam@2201 295 val (kfv, cfv, efv) =
adam@2201 296 foldl (fn ((_, t, e), (kfv, cfv, efv)) =>
adam@2201 297 let
adam@2201 298 val (kfv', cfv', efv') = fvsExp nr e
adam@2201 299 (*val () = Print.prefaces "fvsExp"
adam@2201 300 [("e", ElabPrint.p_exp E.empty e),
adam@2201 301 ("cfv", Print.PD.string
adam@2201 302 (Int.toString (IS.numItems cfv'))),
adam@2201 303 ("efv", Print.PD.string
adam@2201 304 (Int.toString (IS.numItems efv')))]*)
adam@2201 305 val (kfv'', cfv'') = fvsCon t
adam@2201 306 in
adam@2201 307 (IS.union (kfv, IS.union (kfv', kfv'')),
adam@2201 308 IS.union (cfv, IS.union (cfv', cfv'')),
adam@2201 309 IS.union (efv, efv'))
adam@2201 310 end)
adam@2201 311 (IS.empty, IS.empty, IS.empty) vis
adamc@448 312
adamc@826 313 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
adamc@826 314 (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*)
adamc@826 315 (*val () = app (fn (x, t) =>
adamc@453 316 Print.prefaces "Var" [("x", Print.PD.string x),
adamc@826 317 ("t", ElabPrint.p_con E.empty t)]) ts
adamc@826 318 val () = IS.app (fn n => print ("Free: " ^ Int.toString n ^ "\n")) efv*)
adamc@487 319
adam@2201 320 val kfv = IS.foldl (fn (x, kfv) =>
adam@2201 321 let
adam@2201 322 (*val () = print (Int.toString x ^ "\n")*)
adam@2201 323 val (_, k) = List.nth (ks, x)
adam@2201 324 in
adam@2201 325 IS.union (kfv, fvsKind k)
adam@2201 326 end)
adam@2201 327 kfv cfv
adam@2201 328
adam@2201 329 val kfv = IS.foldl (fn (x, kfv) =>
adam@2201 330 let
adam@2201 331 (*val () = print (Int.toString x ^ "\n")*)
adam@2201 332 val (_, t) = List.nth (ts, x)
adam@2201 333 in
adam@2201 334 IS.union (kfv, #1 (fvsCon t))
adam@2201 335 end)
adam@2201 336 kfv efv
adam@2201 337
adamc@448 338 val cfv = IS.foldl (fn (x, cfv) =>
adamc@448 339 let
adamc@448 340 (*val () = print (Int.toString x ^ "\n")*)
adamc@448 341 val (_, t) = List.nth (ts, x)
adamc@448 342 in
adam@2201 343 IS.union (cfv, #2 (fvsCon t))
adamc@448 344 end)
adamc@448 345 cfv efv
adamc@448 346 (*val () = print "B\n"*)
adamc@448 347
adamc@448 348 val (vis, maxName) =
adamc@448 349 ListUtil.foldlMap (fn ((x, t, e), maxName) =>
adamc@448 350 ((x, maxName, t, e),
adamc@448 351 maxName + 1))
adamc@448 352 maxName vis
adamc@448 353
adamc@487 354 val subs = map (fn (n, e) => (n + nr,
adamc@487 355 case e of
adamc@487 356 (ERel _, _) => e
adamc@487 357 | _ => liftExpInExp nr 0 e))
adamc@487 358 subs
adamc@487 359
adamc@448 360 val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
adamc@448 361 let
adamc@487 362 val e = (ENamed n, loc)
adamc@487 363
adamc@487 364 val e = IS.foldr (fn (x, e) =>
adam@2201 365 (EKApp (e, (KRel x, loc)), loc))
adam@2201 366 e kfv
adam@2201 367
adam@2201 368 val e = IS.foldr (fn (x, e) =>
adamc@487 369 (ECApp (e, (CRel x, loc)), loc))
adamc@487 370 e cfv
adamc@487 371
adamc@487 372 val e = IS.foldr (fn (x, e) =>
adamc@487 373 (EApp (e, (ERel (nr + x), loc)),
adamc@487 374 loc))
adamc@487 375 e efv
adamc@448 376 in
adamc@487 377 (nr - i - 1, e)
adamc@448 378 end)
adamc@450 379 vis
adamc@450 380
adam@2201 381 val kfv = IS.listItems kfv
adamc@448 382 val cfv = IS.listItems cfv
adamc@448 383 val efv = IS.listItems efv
adamc@448 384
adamc@487 385 val subs = subs' @ subs
adamc@448 386
adamc@448 387 val vis = map (fn (x, n, t, e) =>
adamc@448 388 let
adamc@448 389 (*val () = Print.prefaces "preSubst"
adamc@448 390 [("e", ElabPrint.p_exp E.empty e)]*)
adamc@490 391 val e = doSubst' (e, subs')
adamc@448 392
adamc@448 393 (*val () = Print.prefaces "squishCon"
adamc@448 394 [("t", ElabPrint.p_con E.empty t)]*)
adam@2201 395 val t = squishCon (kfv, cfv) t
adamc@448 396 (*val () = Print.prefaces "squishExp"
adamc@448 397 [("e", ElabPrint.p_exp E.empty e)]*)
adam@2201 398 val e = squishExp (nr, kfv, cfv, efv) e
adamc@448 399
adamc@487 400 (*val () = print ("Avail: " ^ Int.toString (length ts) ^ "\n")*)
adamc@453 401 val (e, t) = foldl (fn (ex, (e, t)) =>
adamc@448 402 let
adamc@487 403 (*val () = print (Int.toString ex ^ "\n")*)
adamc@448 404 val (name, t') = List.nth (ts, ex)
adam@2201 405 val t' = squishCon (kfv, cfv) t'
adamc@448 406 in
adamc@448 407 ((EAbs (name,
adamc@448 408 t',
adamc@448 409 t,
adamc@448 410 e), loc),
adamc@448 411 (TFun (t',
adamc@448 412 t), loc))
adamc@448 413 end)
adamc@448 414 (e, t) efv
adamc@487 415 (*val () = print "Done\n"*)
adamc@448 416
adamc@453 417 val (e, t) = foldl (fn (cx, (e, t)) =>
adamc@448 418 let
adamc@448 419 val (name, k) = List.nth (ks, cx)
adamc@448 420 in
adamc@448 421 ((ECAbs (Explicit,
adamc@448 422 name,
adamc@448 423 k,
adamc@448 424 e), loc),
adamc@448 425 (TCFun (Explicit,
adamc@448 426 name,
adamc@448 427 k,
adamc@448 428 t), loc))
adamc@448 429 end)
adamc@448 430 (e, t) cfv
adam@2201 431
adam@2201 432 val (e, t) = foldl (fn (kx, (e, t)) =>
adam@2201 433 let
adam@2201 434 val name = List.nth (ns, kx)
adam@2201 435 in
adam@2201 436 ((EKAbs (name,
adam@2201 437 e), loc),
adam@2201 438 (TKFun (name,
adam@2201 439 t), loc))
adam@2201 440 end)
adam@2201 441 (e, t) kfv
adamc@448 442 in
adamc@487 443 (*Print.prefaces "Have a vi"
adamc@487 444 [("x", Print.PD.string x),
adamc@487 445 ("e", ElabPrint.p_exp ElabEnv.empty e)];*)
adamc@1017 446 ("$" ^ x, n, t, e)
adamc@448 447 end)
adamc@448 448 vis
adamc@448 449
adamc@487 450 val ts = List.revAppend (map (fn (x, _, t, _) => (x, t)) vis, ts)
adamc@448 451 in
adamc@487 452 ([], (ts, maxName, vis @ ds, subs, by + nr))
adamc@448 453 end)
adamc@487 454 (ts, #maxName st, #decls st, [], 0) eds
adamc@487 455
adamc@487 456 val e' = doSubst (e, subs, by)
adamc@448 457 in
adamc@487 458 (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e),
adamc@487 459 ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))),
adamc@487 460 ("e'", ElabPrint.p_exp ElabEnv.empty e')];*)
adamc@1272 461 (*Print.prefaces "Let" [("Before", ElabPrint.p_exp ElabEnv.empty (old, ErrorMsg.dummySpan)),
adamc@1272 462 ("After", ElabPrint.p_exp ElabEnv.empty (ELet (eds, e', t), ErrorMsg.dummySpan))];*)
adamc@825 463 (ELet (eds, e', t),
adamc@448 464 {maxName = maxName,
adamc@448 465 decls = ds})
adamc@487 466 (*(ELet (eds, doSubst (liftExpInExp (~(length subs - numRemaining)) (length subs) e) subs),*)
adamc@448 467 end
adamc@448 468
adamc@448 469 | _ => (e, st)
adamc@448 470
adamc@448 471 fun default (ctx, d, st) = (d, st)
adamc@448 472
adam@2201 473 fun bind ((ns, ks, ts), b) =
adamc@448 474 case b of
adam@2201 475 U.Decl.RelK x => (x :: ns, ks, ts)
adam@2201 476 | U.Decl.RelC p => (ns, p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts)
adam@2201 477 | U.Decl.RelE p => (ns, ks, p :: ts)
adam@2201 478 | _ => (ns, ks, ts)
adamc@448 479
adamc@448 480 val unnestDecl = U.Decl.foldMapB {kind = kind,
adamc@448 481 con = default,
adamc@448 482 exp = exp,
adamc@448 483 sgn_item = default,
adamc@448 484 sgn = default,
adamc@448 485 str = default,
adamc@448 486 decl = default,
adamc@448 487 bind = bind}
adam@2201 488 ([], [], [])
adamc@448 489
adamc@448 490 fun unnest file =
adamc@448 491 let
adamc@448 492 fun doDecl (all as (d, loc), st : state) =
adamc@448 493 let
adamc@448 494 fun default () = ([all], st)
adamc@448 495 fun explore () =
adamc@448 496 let
adamc@448 497 val (d, st) = unnestDecl st all
adamc@455 498
adamc@455 499 val ds =
adamc@455 500 case #1 d of
adamc@455 501 DValRec vis => [(DValRec (vis @ #decls st), #2 d)]
adamc@455 502 | _ => [(DValRec (#decls st), #2 d), d]
adamc@448 503 in
adamc@455 504 (ds,
adamc@448 505 {maxName = #maxName st,
adamc@448 506 decls = []})
adamc@448 507 end
adamc@448 508 in
adamc@448 509 case d of
adamc@448 510 DCon _ => default ()
adamc@448 511 | DDatatype _ => default ()
adamc@448 512 | DDatatypeImp _ => default ()
adamc@448 513 | DVal _ => explore ()
adamc@448 514 | DValRec _ => explore ()
adamc@448 515 | DSgn _ => default ()
adamc@448 516 | DStr (x, n, sgn, str) =>
adamc@448 517 let
adamc@448 518 val (str, st) = doStr (str, st)
adamc@448 519 in
adamc@448 520 ([(DStr (x, n, sgn, str), loc)], st)
adamc@448 521 end
adam@1888 522 | DFfiStr ("Basis", n, _) => (basis := n; default ())
adamc@448 523 | DFfiStr _ => default ()
adamc@448 524 | DConstraint _ => default ()
adamc@448 525 | DExport _ => default ()
adamc@448 526 | DTable _ => default ()
adamc@448 527 | DSequence _ => default ()
adamc@754 528 | DView _ => default ()
adamc@448 529 | DDatabase _ => default ()
adamc@459 530 | DCookie _ => default ()
adamc@718 531 | DStyle _ => default ()
adamc@1075 532 | DTask _ => explore ()
adamc@1199 533 | DPolicy _ => explore ()
adam@1294 534 | DOnError _ => default ()
adam@2010 535 | DFfi _ => default ()
adamc@448 536 end
adamc@448 537
adamc@448 538 and doStr (all as (str, loc), st) =
adamc@448 539 let
adamc@448 540 fun default () = (all, st)
adamc@448 541 in
adamc@448 542 case str of
adamc@448 543 StrConst ds =>
adamc@448 544 let
adamc@448 545 val (ds, st) = ListUtil.foldlMapConcat doDecl st ds
adamc@448 546 in
adamc@448 547 ((StrConst ds, loc), st)
adamc@448 548 end
adamc@448 549 | StrVar _ => default ()
adamc@448 550 | StrProj _ => default ()
adamc@448 551 | StrFun (x, n, dom, ran, str) =>
adamc@448 552 let
adamc@448 553 val (str, st) = doStr (str, st)
adamc@448 554 in
adamc@448 555 ((StrFun (x, n, dom, ran, str), loc), st)
adamc@448 556 end
adamc@448 557 | StrApp _ => default ()
adamc@448 558 | StrError => raise Fail "Unnest: StrError"
adamc@448 559 end
adamc@448 560
adamc@448 561 val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@448 562 {maxName = U.File.maxName file + 1,
adamc@448 563 decls = []} file
adamc@448 564 in
adamc@448 565 ds
adamc@448 566 end
adamc@448 567
adamc@448 568 end