Mercurial > urweb

annotate src/unnest.sml @ 448:85819353a84f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
First Unnest tests working
author Adam Chlipala <adamc@hcoop.net>
date Sat, 01 Nov 2008 15:58:55 -0400
parents
children 07f6576aeb0a
rev   line source
adamc@448 1 (* Copyright (c) 2008, 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@448 39 val fvsCon = U.Con.foldB {kind = fn (_, st) => st,
adamc@448 40 con = fn (cb, c, cvs) =>
adamc@448 41 case c of
adamc@448 42 CRel n =>
adamc@448 43 if n >= cb then
adamc@448 44 IS.add (cvs, n - cb)
adamc@448 45 else
adamc@448 46 cvs
adamc@448 47 | _ => cvs,
adamc@448 48 bind = fn (cb, b) =>
adamc@448 49 case b of
adamc@448 50 U.Con.Rel _ => cb + 1
adamc@448 51 | _ => cb}
adamc@448 52 0 IS.empty
adamc@448 53
adamc@448 54 fun fvsExp nr = U.Exp.foldB {kind = fn (_, st) => st,
adamc@448 55 con = fn ((cb, eb), c, st as (cvs, evs)) =>
adamc@448 56 case c of
adamc@448 57 CRel n =>
adamc@448 58 if n >= cb then
adamc@448 59 (IS.add (cvs, n - cb), evs)
adamc@448 60 else
adamc@448 61 st
adamc@448 62 | _ => st,
adamc@448 63 exp = fn ((cb, eb), e, st as (cvs, evs)) =>
adamc@448 64 case e of
adamc@448 65 ERel n =>
adamc@448 66 if n >= eb then
adamc@448 67 (cvs, IS.add (evs, n - eb))
adamc@448 68 else
adamc@448 69 st
adamc@448 70 | _ => st,
adamc@448 71 bind = fn (ctx as (cb, eb), b) =>
adamc@448 72 case b of
adamc@448 73 U.Exp.RelC _ => (cb + 1, eb)
adamc@448 74 | U.Exp.RelE _ => (cb, eb + 1)
adamc@448 75 | _ => ctx}
adamc@448 76 (0, nr) (IS.empty, IS.empty)
adamc@448 77
adamc@448 78 fun positionOf (x : int) ls =
adamc@448 79 let
adamc@448 80 fun po n ls =
adamc@448 81 case ls of
adamc@448 82 [] => raise Fail "Unnest.positionOf"
adamc@448 83 | x' :: ls' =>
adamc@448 84 if x' = x then
adamc@448 85 n
adamc@448 86 else
adamc@448 87 po (n + 1) ls'
adamc@448 88 in
adamc@448 89 po 0 ls
adamc@448 90 handle Fail _ => raise Fail ("Unnset.positionOf("
adamc@448 91 ^ Int.toString x
adamc@448 92 ^ ", "
adamc@448 93 ^ String.concatWith ";" (map Int.toString ls)
adamc@448 94 ^ ")")
adamc@448 95 end
adamc@448 96
adamc@448 97 fun squishCon cfv =
adamc@448 98 U.Con.mapB {kind = fn k => k,
adamc@448 99 con = fn cb => fn c =>
adamc@448 100 case c of
adamc@448 101 CRel n =>
adamc@448 102 if n >= cb then
adamc@448 103 CRel (positionOf (n - cb) cfv + cb)
adamc@448 104 else
adamc@448 105 c
adamc@448 106 | _ => c,
adamc@448 107 bind = fn (cb, b) =>
adamc@448 108 case b of
adamc@448 109 U.Con.Rel _ => cb + 1
adamc@448 110 | _ => cb}
adamc@448 111 0
adamc@448 112
adamc@448 113 fun squishExp (nr, cfv, efv) =
adamc@448 114 U.Exp.mapB {kind = fn k => k,
adamc@448 115 con = fn (cb, eb) => fn c =>
adamc@448 116 case c of
adamc@448 117 CRel n =>
adamc@448 118 if n >= cb then
adamc@448 119 CRel (positionOf (n - cb) cfv + cb)
adamc@448 120 else
adamc@448 121 c
adamc@448 122 | _ => c,
adamc@448 123 exp = fn (cb, eb) => fn e =>
adamc@448 124 case e of
adamc@448 125 ERel n =>
adamc@448 126 if n >= eb then
adamc@448 127 ERel (positionOf (n - eb) efv + eb)
adamc@448 128 else
adamc@448 129 e
adamc@448 130 | _ => e,
adamc@448 131 bind = fn (ctx as (cb, eb), b) =>
adamc@448 132 case b of
adamc@448 133 U.Exp.RelC _ => (cb + 1, eb)
adamc@448 134 | U.Exp.RelE _ => (cb, eb + 1)
adamc@448 135 | _ => ctx}
adamc@448 136 (0, nr)
adamc@448 137
adamc@448 138 type state = {
adamc@448 139 maxName : int,
adamc@448 140 decls : decl list
adamc@448 141 }
adamc@448 142
adamc@448 143 fun kind (k, st) = (k, st)
adamc@448 144
adamc@448 145 fun exp ((ks, ts), e, st : state) =
adamc@448 146 case e of
adamc@448 147 ELet (eds, e) =>
adamc@448 148 let
adamc@448 149 val doSubst = foldl (fn (p, e) => E.subExpInExp p e)
adamc@448 150
adamc@448 151 val (eds, (maxName, ds, subs)) =
adamc@448 152 ListUtil.foldlMapConcat
adamc@448 153 (fn (ed, (maxName, ds, subs)) =>
adamc@448 154 case #1 ed of
adamc@448 155 EDVal _ => ([ed], (maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs))
adamc@448 156 | EDValRec vis =>
adamc@448 157 let
adamc@448 158 val loc = #2 ed
adamc@448 159
adamc@448 160 val nr = length vis
adamc@448 161 val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) =>
adamc@448 162 let
adamc@448 163 val (cfv', efv') = fvsExp nr e
adamc@448 164 (*val () = Print.prefaces "fvsExp"
adamc@448 165 [("e", ElabPrint.p_exp E.empty e),
adamc@448 166 ("cfv", Print.PD.string
adamc@448 167 (Int.toString (IS.numItems cfv'))),
adamc@448 168 ("efv", Print.PD.string
adamc@448 169 (Int.toString (IS.numItems efv')))]*)
adamc@448 170 val cfv'' = fvsCon t
adamc@448 171 in
adamc@448 172 (IS.union (cfv, IS.union (cfv', cfv'')),
adamc@448 173 IS.union (efv, efv'))
adamc@448 174 end)
adamc@448 175 (IS.empty, IS.empty) vis
adamc@448 176
adamc@448 177 (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*)
adamc@448 178 val cfv = IS.foldl (fn (x, cfv) =>
adamc@448 179 let
adamc@448 180 (*val () = print (Int.toString x ^ "\n")*)
adamc@448 181 val (_, t) = List.nth (ts, x)
adamc@448 182 in
adamc@448 183 IS.union (cfv, fvsCon t)
adamc@448 184 end)
adamc@448 185 cfv efv
adamc@448 186 (*val () = print "B\n"*)
adamc@448 187
adamc@448 188 val (vis, maxName) =
adamc@448 189 ListUtil.foldlMap (fn ((x, t, e), maxName) =>
adamc@448 190 ((x, maxName, t, e),
adamc@448 191 maxName + 1))
adamc@448 192 maxName vis
adamc@448 193
adamc@448 194 fun apply e =
adamc@448 195 let
adamc@448 196 val e = IS.foldl (fn (x, e) =>
adamc@448 197 (ECApp (e, (CRel x, loc)), loc))
adamc@448 198 e cfv
adamc@448 199 in
adamc@448 200 IS.foldl (fn (x, e) =>
adamc@448 201 (EApp (e, (ERel x, loc)), loc))
adamc@448 202 e efv
adamc@448 203 end
adamc@448 204
adamc@448 205 val subs = map (fn (n, e) => (n + nr, E.liftExpInExp nr e)) subs
adamc@448 206
adamc@448 207 val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
adamc@448 208 let
adamc@448 209 val e = apply (ENamed n, loc)
adamc@448 210 in
adamc@448 211 (0, E.liftExpInExp (nr - i - 1) e)
adamc@448 212 end)
adamc@448 213 vis
adamc@448 214 val subs' = rev subs'
adamc@448 215
adamc@448 216 val cfv = IS.listItems cfv
adamc@448 217 val efv = IS.listItems efv
adamc@448 218 val efn = length efv
adamc@448 219
adamc@448 220 (*val subsInner = subs
adamc@448 221 @ map (fn (i, e) =>
adamc@448 222 (i + efn,
adamc@448 223 E.liftExpInExp efn e)) subs'*)
adamc@448 224
adamc@448 225 val subs = subs @ subs'
adamc@448 226
adamc@448 227 val vis = map (fn (x, n, t, e) =>
adamc@448 228 let
adamc@448 229 (*val () = Print.prefaces "preSubst"
adamc@448 230 [("e", ElabPrint.p_exp E.empty e)]*)
adamc@448 231 val e = doSubst e subs(*Inner*)
adamc@448 232
adamc@448 233 (*val () = Print.prefaces "squishCon"
adamc@448 234 [("t", ElabPrint.p_con E.empty t)]*)
adamc@448 235 val t = squishCon cfv t
adamc@448 236 (*val () = Print.prefaces "squishExp"
adamc@448 237 [("e", ElabPrint.p_exp E.empty e)]*)
adamc@448 238 val e = squishExp (nr, cfv, efv) e
adamc@448 239
adamc@448 240 val (e, t) = foldr (fn (ex, (e, t)) =>
adamc@448 241 let
adamc@448 242 val (name, t') = List.nth (ts, ex)
adamc@448 243 in
adamc@448 244 ((EAbs (name,
adamc@448 245 t',
adamc@448 246 t,
adamc@448 247 e), loc),
adamc@448 248 (TFun (t',
adamc@448 249 t), loc))
adamc@448 250 end)
adamc@448 251 (e, t) efv
adamc@448 252
adamc@448 253 val (e, t) = foldr (fn (cx, (e, t)) =>
adamc@448 254 let
adamc@448 255 val (name, k) = List.nth (ks, cx)
adamc@448 256 in
adamc@448 257 ((ECAbs (Explicit,
adamc@448 258 name,
adamc@448 259 k,
adamc@448 260 e), loc),
adamc@448 261 (TCFun (Explicit,
adamc@448 262 name,
adamc@448 263 k,
adamc@448 264 t), loc))
adamc@448 265 end)
adamc@448 266 (e, t) cfv
adamc@448 267 in
adamc@448 268 (x, n, t, e)
adamc@448 269 end)
adamc@448 270 vis
adamc@448 271
adamc@448 272 val d = (DValRec vis, #2 ed)
adamc@448 273 in
adamc@448 274 ([], (maxName, d :: ds, subs))
adamc@448 275 end)
adamc@448 276 (#maxName st, #decls st, []) eds
adamc@448 277 in
adamc@448 278 (ELet (eds, doSubst e subs),
adamc@448 279 {maxName = maxName,
adamc@448 280 decls = ds})
adamc@448 281 end
adamc@448 282
adamc@448 283 | _ => (e, st)
adamc@448 284
adamc@448 285 fun default (ctx, d, st) = (d, st)
adamc@448 286
adamc@448 287 fun bind ((ks, ts), b) =
adamc@448 288 case b of
adamc@448 289 U.Decl.RelC p => (p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts)
adamc@448 290 | U.Decl.RelE p => (ks, p :: ts)
adamc@448 291 | _ => (ks, ts)
adamc@448 292
adamc@448 293 val unnestDecl = U.Decl.foldMapB {kind = kind,
adamc@448 294 con = default,
adamc@448 295 exp = exp,
adamc@448 296 sgn_item = default,
adamc@448 297 sgn = default,
adamc@448 298 str = default,
adamc@448 299 decl = default,
adamc@448 300 bind = bind}
adamc@448 301 ([], [])
adamc@448 302
adamc@448 303 fun unnest file =
adamc@448 304 let
adamc@448 305 fun doDecl (all as (d, loc), st : state) =
adamc@448 306 let
adamc@448 307 fun default () = ([all], st)
adamc@448 308 fun explore () =
adamc@448 309 let
adamc@448 310 val (d, st) = unnestDecl st all
adamc@448 311 in
adamc@448 312 (rev (d :: #decls st),
adamc@448 313 {maxName = #maxName st,
adamc@448 314 decls = []})
adamc@448 315 end
adamc@448 316 in
adamc@448 317 case d of
adamc@448 318 DCon _ => default ()
adamc@448 319 | DDatatype _ => default ()
adamc@448 320 | DDatatypeImp _ => default ()
adamc@448 321 | DVal _ => explore ()
adamc@448 322 | DValRec _ => explore ()
adamc@448 323 | DSgn _ => default ()
adamc@448 324 | DStr (x, n, sgn, str) =>
adamc@448 325 let
adamc@448 326 val (str, st) = doStr (str, st)
adamc@448 327 in
adamc@448 328 ([(DStr (x, n, sgn, str), loc)], st)
adamc@448 329 end
adamc@448 330 | DFfiStr _ => default ()
adamc@448 331 | DConstraint _ => default ()
adamc@448 332 | DExport _ => default ()
adamc@448 333 | DTable _ => default ()
adamc@448 334 | DSequence _ => default ()
adamc@448 335 | DClass _ => default ()
adamc@448 336 | DDatabase _ => default ()
adamc@448 337 end
adamc@448 338
adamc@448 339 and doStr (all as (str, loc), st) =
adamc@448 340 let
adamc@448 341 fun default () = (all, st)
adamc@448 342 in
adamc@448 343 case str of
adamc@448 344 StrConst ds =>
adamc@448 345 let
adamc@448 346 val (ds, st) = ListUtil.foldlMapConcat doDecl st ds
adamc@448 347 in
adamc@448 348 ((StrConst ds, loc), st)
adamc@448 349 end
adamc@448 350 | StrVar _ => default ()
adamc@448 351 | StrProj _ => default ()
adamc@448 352 | StrFun (x, n, dom, ran, str) =>
adamc@448 353 let
adamc@448 354 val (str, st) = doStr (str, st)
adamc@448 355 in
adamc@448 356 ((StrFun (x, n, dom, ran, str), loc), st)
adamc@448 357 end
adamc@448 358 | StrApp _ => default ()
adamc@448 359 | StrError => raise Fail "Unnest: StrError"
adamc@448 360 end
adamc@448 361
adamc@448 362 val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@448 363 {maxName = U.File.maxName file + 1,
adamc@448 364 decls = []} file
adamc@448 365 in
adamc@448 366 ds
adamc@448 367 end
adamc@448 368
adamc@448 369 end