Mercurial > urweb

annotate src/especialize.sml @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
parents 066493f7f008
children a3273bee05a9
rev   line source
adamc@443 1 (* Copyright (c) 2008, Adam Chlipala
adamc@443 2 * All rights reserved.
adamc@443 3 *
adamc@443 4 * Redistribution and use in source and binary forms, with or without
adamc@443 5 * modification, are permitted provided that the following conditions are met:
adamc@443 6 *
adamc@443 7 * - Redistributions of source code must retain the above copyright notice,
adamc@443 8 * this list of conditions and the following disclaimer.
adamc@443 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@443 10 * this list of conditions and the following disclaimer in the documentation
adamc@443 11 * and/or other materials provided with the distribution.
adamc@443 12 * - The names of contributors may not be used to endorse or promote products
adamc@443 13 * derived from this software without specific prior written permission.
adamc@443 14 *
adamc@443 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@443 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@443 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@443 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@443 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@443 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@443 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@443 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@443 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@443 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@443 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@443 26 *)
adamc@443 27
adamc@443 28 structure ESpecialize :> ESPECIALIZE = struct
adamc@443 29
adamc@443 30 open Core
adamc@443 31
adamc@443 32 structure E = CoreEnv
adamc@443 33 structure U = CoreUtil
adamc@443 34
adamc@479 35 type skey = exp
adamc@453 36
adamc@453 37 structure K = struct
adamc@479 38 type ord_key = exp list
adamc@479 39 val compare = Order.joinL U.Exp.compare
adamc@443 40 end
adamc@443 41
adamc@453 42 structure KM = BinaryMapFn(K)
adamc@443 43 structure IM = IntBinaryMap
adamc@482 44 structure IS = IntBinarySet
adamc@443 45
adamc@626 46 val freeVars = U.Exp.foldB {kind = fn (_, _, xs) => xs,
adamc@488 47 con = fn (_, _, xs) => xs,
adamc@488 48 exp = fn (bound, e, xs) =>
adamc@488 49 case e of
adamc@488 50 ERel x =>
adamc@488 51 if x >= bound then
adamc@488 52 IS.add (xs, x - bound)
adamc@488 53 else
adamc@488 54 xs
adamc@488 55 | _ => xs,
adamc@488 56 bind = fn (bound, b) =>
adamc@488 57 case b of
adamc@488 58 U.Exp.RelE _ => bound + 1
adamc@488 59 | _ => bound}
adamc@488 60 0 IS.empty
adamc@479 61
adamc@522 62 val isPoly = U.Decl.exists {kind = fn _ => false,
adamc@522 63 con = fn _ => false,
adamc@522 64 exp = fn ECAbs _ => true
adamc@522 65 | _ => false,
adamc@522 66 decl = fn _ => false}
adamc@522 67
adamc@488 68 fun positionOf (v : int, ls) =
adamc@488 69 let
adamc@488 70 fun pof (pos, ls) =
adamc@488 71 case ls of
adamc@488 72 [] => raise Fail "Defunc.positionOf"
adamc@488 73 | v' :: ls' =>
adamc@488 74 if v = v' then
adamc@488 75 pos
adamc@488 76 else
adamc@488 77 pof (pos + 1, ls')
adamc@488 78 in
adamc@488 79 pof (0, ls)
adamc@488 80 end
adamc@488 81
adamc@488 82 fun squish fvs =
adamc@626 83 U.Exp.mapB {kind = fn _ => fn k => k,
adamc@488 84 con = fn _ => fn c => c,
adamc@488 85 exp = fn bound => fn e =>
adamc@479 86 case e of
adamc@488 87 ERel x =>
adamc@488 88 if x >= bound then
adamc@488 89 ERel (positionOf (x - bound, fvs) + bound)
adamc@488 90 else
adamc@488 91 e
adamc@488 92 | _ => e,
adamc@488 93 bind = fn (bound, b) =>
adamc@488 94 case b of
adamc@488 95 U.Exp.RelE _ => bound + 1
adamc@488 96 | _ => bound}
adamc@488 97 0
adamc@453 98
adamc@443 99 type func = {
adamc@443 100 name : string,
adamc@453 101 args : int KM.map,
adamc@443 102 body : exp,
adamc@443 103 typ : con,
adamc@443 104 tag : string
adamc@443 105 }
adamc@443 106
adamc@443 107 type state = {
adamc@443 108 maxName : int,
adamc@443 109 funcs : func IM.map,
adamc@443 110 decls : (string * int * con * exp * string) list
adamc@443 111 }
adamc@443 112
adamc@488 113 fun default (_, x, st) = (x, st)
adamc@443 114
adamc@800 115 structure SS = BinarySetFn(struct
adamc@800 116 type ord_key = string
adamc@800 117 val compare = String.compare
adamc@800 118 end)
adamc@800 119
adamc@800 120 val mayNotSpec = ref SS.empty
adamc@800 121
adamc@453 122 fun specialize' file =
adamc@443 123 let
adamc@488 124 fun bind (env, b) =
adamc@488 125 case b of
adamc@521 126 U.Decl.RelE xt => xt :: env
adamc@521 127 | _ => env
adamc@488 128
adamc@488 129 fun exp (env, e, st : state) =
adamc@482 130 let
adamc@721 131 (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty
adamc@721 132 (e, ErrorMsg.dummySpan))]*)
adamc@721 133
adamc@488 134 fun getApp e =
adamc@482 135 case e of
adamc@488 136 ENamed f => SOME (f, [])
adamc@482 137 | EApp (e1, e2) =>
adamc@488 138 (case getApp (#1 e1) of
adamc@482 139 NONE => NONE
adamc@488 140 | SOME (f, xs) => SOME (f, xs @ [e2]))
adamc@482 141 | _ => NONE
adamc@482 142 in
adamc@482 143 case getApp e of
adamc@721 144 NONE => ((*Print.prefaces "No" [("e", CorePrint.p_exp CoreEnv.empty
adamc@721 145 (e, ErrorMsg.dummySpan))];*)
adamc@721 146 (e, st))
adamc@488 147 | SOME (f, xs) =>
adamc@485 148 case IM.find (#funcs st, f) of
adamc@485 149 NONE => (e, st)
adamc@485 150 | SOME {name, args, body, typ, tag} =>
adamc@488 151 let
adamc@721 152 (*val () = Print.prefaces "Consider" [("e", CorePrint.p_exp CoreEnv.empty
adamc@721 153 (e, ErrorMsg.dummySpan))]*)
adamc@721 154
adamc@488 155 val functionInside = U.Con.exists {kind = fn _ => false,
adamc@488 156 con = fn TFun _ => true
adamc@488 157 | CFfi ("Basis", "transaction") => true
adamc@794 158 | CFfi ("Basis", "eq") => true
adamc@794 159 | CFfi ("Basis", "num") => true
adamc@794 160 | CFfi ("Basis", "ord") => true
adamc@794 161 | CFfi ("Basis", "show") => true
adamc@794 162 | CFfi ("Basis", "read") => true
adamc@794 163 | CFfi ("Basis", "sql_injectable_prim") => true
adamc@794 164 | CFfi ("Basis", "sql_injectable") => true
adamc@488 165 | _ => false}
adamc@488 166 val loc = ErrorMsg.dummySpan
adamc@488 167
adamc@488 168 fun findSplit (xs, typ, fxs, fvs) =
adamc@488 169 case (#1 typ, xs) of
adamc@488 170 (TFun (dom, ran), e :: xs') =>
adamc@488 171 if functionInside dom then
adamc@488 172 findSplit (xs',
adamc@488 173 ran,
adamc@488 174 e :: fxs,
adamc@488 175 IS.union (fvs, freeVars e))
adamc@488 176 else
adamc@488 177 (rev fxs, xs, fvs)
adamc@488 178 | _ => (rev fxs, xs, fvs)
adamc@488 179
adamc@488 180 val (fxs, xs, fvs) = findSplit (xs, typ, [], IS.empty)
adamc@488 181
adamc@488 182 val fxs' = map (squish (IS.listItems fvs)) fxs
adamc@488 183
adamc@488 184 fun firstRel () =
adamc@488 185 case fxs' of
adamc@488 186 (ERel _, _) :: _ => true
adamc@488 187 | _ => false
adamc@488 188 in
adamc@800 189 (*Print.preface ("fxs'", Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs');*)
adamc@488 190 if firstRel ()
adamc@488 191 orelse List.all (fn (ERel _, _) => true
adamc@488 192 | _ => false) fxs' then
adamc@488 193 (e, st)
adamc@488 194 else
adamc@800 195 case (KM.find (args, fxs'), SS.member (!mayNotSpec, name)) of
adamc@800 196 (SOME f', _) =>
adamc@485 197 let
adamc@488 198 val e = (ENamed f', loc)
adamc@488 199 val e = IS.foldr (fn (arg, e) => (EApp (e, (ERel arg, loc)), loc))
adamc@488 200 e fvs
adamc@488 201 val e = foldl (fn (arg, e) => (EApp (e, arg), loc))
adamc@488 202 e xs
adamc@488 203 in
adamc@488 204 (*Print.prefaces "Brand new (reuse)"
adamc@721 205 [("e'", CorePrint.p_exp CoreEnv.empty e)];*)
adamc@488 206 (#1 e, st)
adamc@488 207 end
adamc@818 208 | (_, true) => ((*Print.prefaces ("No(" ^ name ^ ")")
adamc@818 209 [("fxs'",
adamc@818 210 Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs')];*)
adamc@818 211 (e, st))
adamc@800 212 | (NONE, false) =>
adamc@488 213 let
adamc@800 214 (*val () = Print.prefaces "New one"
adamc@800 215 [("f", Print.PD.string (Int.toString f)),
adamc@800 216 ("mns", Print.p_list Print.PD.string
adamc@800 217 (SS.listItems (!mayNotSpec)))]*)
adamc@800 218
adamc@818 219 (*val () = Print.prefaces ("Yes(" ^ name ^ ")")
adamc@818 220 [("fxs'",
adamc@818 221 Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs')]*)
adamc@818 222
adamc@488 223 fun subBody (body, typ, fxs') =
adamc@488 224 case (#1 body, #1 typ, fxs') of
adamc@488 225 (_, _, []) => SOME (body, typ)
adamc@488 226 | (EAbs (_, _, _, body'), TFun (_, typ'), x :: fxs'') =>
adamc@488 227 let
adamc@488 228 val body'' = E.subExpInExp (0, x) body'
adamc@488 229 in
adamc@488 230 subBody (body'',
adamc@488 231 typ',
adamc@488 232 fxs'')
adamc@488 233 end
adamc@488 234 | _ => NONE
adamc@488 235 in
adamc@488 236 case subBody (body, typ, fxs') of
adamc@488 237 NONE => (e, st)
adamc@488 238 | SOME (body', typ') =>
adamc@488 239 let
adamc@488 240 val f' = #maxName st
adamc@488 241 val args = KM.insert (args, fxs', f')
adamc@488 242 val funcs = IM.insert (#funcs st, f, {name = name,
adamc@488 243 args = args,
adamc@488 244 body = body,
adamc@488 245 typ = typ,
adamc@488 246 tag = tag})
adamc@488 247 val st = {
adamc@488 248 maxName = f' + 1,
adamc@488 249 funcs = funcs,
adamc@488 250 decls = #decls st
adamc@488 251 }
adamc@487 252
adamc@488 253 (*val () = Print.prefaces "specExp"
adamc@488 254 [("f", CorePrint.p_exp env (ENamed f, loc)),
adamc@488 255 ("f'", CorePrint.p_exp env (ENamed f', loc)),
adamc@488 256 ("xs", Print.p_list (CorePrint.p_exp env) xs),
adamc@488 257 ("fxs'", Print.p_list
adamc@488 258 (CorePrint.p_exp E.empty) fxs'),
adamc@488 259 ("e", CorePrint.p_exp env (e, loc))]*)
adamc@488 260 val (body', typ') = IS.foldl (fn (n, (body', typ')) =>
adamc@488 261 let
adamc@521 262 val (x, xt) = List.nth (env, n)
adamc@488 263 in
adamc@488 264 ((EAbs (x, xt, typ', body'),
adamc@488 265 loc),
adamc@488 266 (TFun (xt, typ'), loc))
adamc@488 267 end)
adamc@488 268 (body', typ') fvs
adamc@800 269 val mns = !mayNotSpec
adamc@800 270 val () = mayNotSpec := SS.add (mns, name)
adamc@800 271 (*val () = Print.preface ("body'", CorePrint.p_exp CoreEnv.empty body')*)
adamc@488 272 val (body', st) = specExp env st body'
adamc@800 273 val () = mayNotSpec := mns
adamc@482 274
adamc@488 275 val e' = (ENamed f', loc)
adamc@488 276 val e' = IS.foldr (fn (arg, e) => (EApp (e, (ERel arg, loc)), loc))
adamc@488 277 e' fvs
adamc@488 278 val e' = foldl (fn (arg, e) => (EApp (e, arg), loc))
adamc@488 279 e' xs
adamc@488 280 (*val () = Print.prefaces "Brand new"
adamc@721 281 [("e'", CorePrint.p_exp CoreEnv.empty e'),
adamc@721 282 ("e", CorePrint.p_exp CoreEnv.empty (e, loc)),
adamc@721 283 ("body'", CorePrint.p_exp CoreEnv.empty body')]*)
adamc@488 284 in
adamc@488 285 (#1 e',
adamc@488 286 {maxName = #maxName st,
adamc@488 287 funcs = #funcs st,
adamc@488 288 decls = (name, f', typ', body', tag) :: #decls st})
adamc@488 289 end
adamc@485 290 end
adamc@488 291 end
adamc@485 292 end
adamc@482 293
adamc@626 294 and specExp env = U.Exp.foldMapB {kind = default, con = default, exp = exp, bind = bind} env
adamc@482 295
adamc@626 296 val specDecl = U.Decl.foldMapB {kind = default, con = default, exp = exp, decl = default, bind = bind}
adamc@482 297
adamc@521 298 fun doDecl (d, (st : state, changed)) =
adamc@488 299 let
adamc@521 300 (*val befor = Time.now ()*)
adamc@482 301
adamc@453 302 val funcs = #funcs st
adamc@453 303 val funcs =
adamc@453 304 case #1 d of
adamc@453 305 DValRec vis =>
adamc@453 306 foldl (fn ((x, n, c, e, tag), funcs) =>
adamc@453 307 IM.insert (funcs, n, {name = x,
adamc@453 308 args = KM.empty,
adamc@453 309 body = e,
adamc@453 310 typ = c,
adamc@453 311 tag = tag}))
adamc@453 312 funcs vis
adamc@453 313 | _ => funcs
adamc@453 314
adamc@453 315 val st = {maxName = #maxName st,
adamc@453 316 funcs = funcs,
adamc@453 317 decls = []}
adamc@453 318
adamc@482 319 (*val () = Print.prefaces "decl" [("d", CorePrint.p_decl CoreEnv.empty d)]*)
adamc@521 320
adamc@522 321 val (d', st) =
adamc@522 322 if isPoly d then
adamc@522 323 (d, st)
adamc@522 324 else
adamc@800 325 (mayNotSpec := (case #1 d of
adamc@800 326 DValRec vis => foldl (fn ((x, _, _, _, _), mns) =>
adamc@800 327 SS.add (mns, x)) SS.empty vis
adamc@800 328 | DVal (x, _, _, _, _) => SS.singleton x
adamc@800 329 | _ => SS.empty);
adamc@800 330 specDecl [] st d
adamc@800 331 before mayNotSpec := SS.empty)
adamc@521 332
adamc@482 333 (*val () = print "/decl\n"*)
adamc@443 334
adamc@443 335 val funcs = #funcs st
adamc@443 336 val funcs =
adamc@443 337 case #1 d of
adamc@443 338 DVal (x, n, c, e as (EAbs _, _), tag) =>
adamc@443 339 IM.insert (funcs, n, {name = x,
adamc@453 340 args = KM.empty,
adamc@443 341 body = e,
adamc@443 342 typ = c,
adamc@443 343 tag = tag})
adamc@469 344 | DVal (_, n, _, (ENamed n', _), _) =>
adamc@469 345 (case IM.find (funcs, n') of
adamc@469 346 NONE => funcs
adamc@469 347 | SOME v => IM.insert (funcs, n, v))
adamc@443 348 | _ => funcs
adamc@443 349
adamc@453 350 val (changed, ds) =
adamc@443 351 case #decls st of
adamc@453 352 [] => (changed, [d'])
adamc@453 353 | vis =>
adamc@453 354 (true, case d' of
adamc@453 355 (DValRec vis', _) => [(DValRec (vis @ vis'), ErrorMsg.dummySpan)]
adamc@453 356 | _ => [(DValRec vis, ErrorMsg.dummySpan), d'])
adamc@443 357 in
adamc@802 358 (*Print.prefaces "doDecl" [("d", CorePrint.p_decl E.empty d),
adamc@802 359 ("d'", CorePrint.p_decl E.empty d')];*)
adamc@521 360 (ds, ({maxName = #maxName st,
adamc@453 361 funcs = funcs,
adamc@453 362 decls = []}, changed))
adamc@443 363 end
adamc@443 364
adamc@521 365 val (ds, (_, changed)) = ListUtil.foldlMapConcat doDecl
adamc@521 366 ({maxName = U.File.maxName file + 1,
adamc@488 367 funcs = IM.empty,
adamc@488 368 decls = []},
adamc@488 369 false)
adamc@488 370 file
adamc@443 371 in
adamc@453 372 (changed, ds)
adamc@443 373 end
adamc@443 374
adamc@453 375 fun specialize file =
adamc@453 376 let
adamc@721 377 val file = ReduceLocal.reduce file
adamc@721 378 (*val () = Print.prefaces "Intermediate" [("file", CorePrint.p_file CoreEnv.empty file)]*)
adamc@520 379 (*val file = ReduceLocal.reduce file*)
adamc@453 380 val (changed, file) = specialize' file
adamc@520 381 (*val file = ReduceLocal.reduce file
adamc@520 382 val file = CoreUntangle.untangle file
adamc@488 383 val file = Shake.shake file*)
adamc@453 384 in
adamc@488 385 (*print "Round over\n";*)
adamc@453 386 if changed then
adamc@520 387 let
adamc@721 388 (*val file = ReduceLocal.reduce file*)
adamc@802 389 (*val () = Print.prefaces "Pre-untangle" [("file", CorePrint.p_file CoreEnv.empty file)]*)
adamc@520 390 val file = CoreUntangle.untangle file
adamc@802 391 (*val () = Print.prefaces "Post-untangle" [("file", CorePrint.p_file CoreEnv.empty file)]*)
adamc@520 392 val file = Shake.shake file
adamc@520 393 in
adamc@520 394 (*print "Again!\n";*)
adamc@520 395 specialize file
adamc@520 396 end
adamc@453 397 else
adamc@453 398 file
adamc@453 399 end
adamc@453 400
adamc@443 401 end