Mercurial > urweb

annotate src/mono_reduce.sml @ 1361:7a436b6267ab

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix soundness bug in Effectize, where it missed some functions that might have effectful RPCs
author Adam Chlipala <adam@chlipala.net>
date Thu, 23 Dec 2010 18:07:05 -0500
parents 02fc16faecf3
children 802c179dac1f
rev   line source
adamc@133 1 (* Copyright (c) 2008, Adam Chlipala
adamc@133 2 * All rights reserved.
adamc@133 3 *
adamc@133 4 * Redistribution and use in source and binary forms, with or without
adamc@133 5 * modification, are permitted provided that the following conditions are met:
adamc@133 6 *
adamc@133 7 * - Redistributions of source code must retain the above copyright notice,
adamc@133 8 * this list of conditions and the following disclaimer.
adamc@133 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@133 10 * this list of conditions and the following disclaimer in the documentation
adamc@133 11 * and/or other materials provided with the distribution.
adamc@133 12 * - The names of contributors may not be used to endorse or promote products
adamc@133 13 * derived from this software without specific prior written permission.
adamc@133 14 *
adamc@133 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@133 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@133 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@133 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@133 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@133 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@133 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@133 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@133 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@133 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@133 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@133 26 *)
adamc@133 27
adamc@133 28 (* Simplify a Mono program algebraically *)
adamc@133 29
adamc@133 30 structure MonoReduce :> MONO_REDUCE = struct
adamc@133 31
adamc@133 32 open Mono
adamc@133 33
adamc@133 34 structure E = MonoEnv
adamc@133 35 structure U = MonoUtil
adamc@133 36
adamc@470 37 structure IM = IntBinaryMap
adamc@916 38 structure IS = IntBinarySet
adamc@470 39
adamc@133 40
adamc@948 41 fun simpleTypeImpure tsyms =
adamc@919 42 U.Typ.exists (fn TFun _ => true
adamc@948 43 | TDatatype (n, _) => IS.member (tsyms, n)
adamc@919 44 | _ => false)
adamc@919 45
adamc@948 46 fun simpleImpure (tsyms, syms) =
adamc@919 47 U.Exp.existsB {typ = fn _ => false,
adamc@919 48 exp = fn (env, e) =>
adamc@919 49 case e of
adamc@919 50 EWrite _ => true
adamc@919 51 | EQuery _ => true
adamc@919 52 | EDml _ => true
adamc@919 53 | ENextval _ => true
adamc@1073 54 | ESetval _ => true
adamc@1171 55 | EFfiApp (m, x, _) => Settings.isEffectful (m, x) orelse Settings.isBenignEffectful (m, x)
adamc@919 56 | EServerCall _ => true
adamc@919 57 | ERecv _ => true
adamc@919 58 | ESleep _ => true
adamc@919 59 | ENamed n => IS.member (syms, n)
adamc@1069 60 | EError _ => true
adamc@919 61 | ERel n =>
adamc@919 62 let
adamc@919 63 val (_, t, _) = E.lookupERel env n
adamc@919 64 in
adamc@948 65 simpleTypeImpure tsyms t
adamc@919 66 end
adamc@919 67 | _ => false,
adamc@919 68 bind = fn (env, b) =>
adamc@919 69 case b of
adamc@919 70 U.Exp.RelE (x, t) => E.pushERel env x t NONE
adamc@919 71 | _ => env}
adamc@916 72
adamc@252 73 fun impure (e, _) =
adamc@252 74 case e of
adamc@252 75 EWrite _ => true
adamc@252 76 | EQuery _ => true
adamc@307 77 | EDml _ => true
adamc@338 78 | ENextval _ => true
adamc@1073 79 | ESetval _ => true
adamc@1225 80 | EUnurlify _ => false
adamc@252 81 | EAbs _ => false
adamc@252 82
adamc@252 83 | EPrim _ => false
adamc@252 84 | ERel _ => false
adamc@252 85 | ENamed _ => false
adamc@252 86 | ECon (_, _, eo) => (case eo of NONE => false | SOME e => impure e)
adamc@297 87 | ENone _ => false
adamc@290 88 | ESome (_, e) => impure e
adamc@252 89 | EFfi _ => false
adamc@1171 90 | EFfiApp (m, x, _) => Settings.isEffectful (m, x) orelse Settings.isBenignEffectful (m, x)
adamc@252 91 | EApp ((EFfi _, _), _) => false
adamc@252 92 | EApp _ => true
adamc@252 93
adamc@387 94 | EUnop (_, e) => impure e
adam@1360 95 | EBinop (_, _, e1, e2) => impure e1 orelse impure e2
adamc@387 96
adamc@252 97 | ERecord xes => List.exists (fn (_, e, _) => impure e) xes
adamc@252 98 | EField (e, _) => impure e
adamc@252 99
adamc@252 100 | ECase (e, pes, _) => impure e orelse List.exists (fn (_, e) => impure e) pes
adamc@252 101
adamc@1069 102 | EError _ => true
adamc@741 103 | EReturnBlob {blob = e1, mimeType = e2, ...} => impure e1 orelse impure e2
adamc@1065 104 | ERedirect (e, _) => impure e
adamc@283 105
adamc@252 106 | EStrcat (e1, e2) => impure e1 orelse impure e2
adamc@252 107
adamc@252 108 | ESeq (e1, e2) => impure e1 orelse impure e2
adamc@252 109 | ELet (_, _, e1, e2) => impure e1 orelse impure e2
adamc@252 110
adamc@252 111 | EClosure (_, es) => List.exists impure es
adamc@815 112 | EJavaScript (_, e) => impure e
adamc@568 113 | ESignalReturn e => impure e
adamc@572 114 | ESignalBind (e1, e2) => impure e1 orelse impure e2
adamc@574 115 | ESignalSource e => impure e
adamc@608 116 | EServerCall _ => true
adamc@670 117 | ERecv _ => true
adamc@695 118 | ESleep _ => true
adamc@1021 119 | ESpawn _ => true
adamc@252 120
adamc@252 121 val liftExpInExp = Monoize.liftExpInExp
adamc@252 122
adamc@829 123 fun multiLift n e =
adamc@829 124 case n of
adamc@829 125 0 => e
adamc@829 126 | _ => multiLift (n - 1) (liftExpInExp 0 e)
adamc@829 127
adamc@252 128 val subExpInExp' =
adamc@133 129 U.Exp.mapB {typ = fn t => t,
adamc@133 130 exp = fn (xn, rep) => fn e =>
adamc@133 131 case e of
adamc@133 132 ERel xn' =>
adamc@133 133 (case Int.compare (xn', xn) of
adamc@133 134 EQUAL => #1 rep
adamc@133 135 | GREATER=> ERel (xn' - 1)
adamc@133 136 | LESS => e)
adamc@133 137 | _ => e,
adamc@133 138 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
adamc@133 139 | (ctx, _) => ctx}
adamc@133 140
adamc@252 141 fun subExpInExp (n, e1) e2 =
adamc@252 142 let
adamc@252 143 val r = subExpInExp' (n, e1) e2
adamc@252 144 in
adamc@252 145 (*Print.prefaces "subExpInExp" [("e1", MonoPrint.p_exp MonoEnv.empty e1),
adamc@252 146 ("e2", MonoPrint.p_exp MonoEnv.empty e2),
adamc@252 147 ("r", MonoPrint.p_exp MonoEnv.empty r)];*)
adamc@252 148 r
adamc@252 149 end
adamc@133 150
adamc@133 151 fun typ c = c
adamc@133 152
adamc@316 153 val swapExpVars =
adamc@316 154 U.Exp.mapB {typ = fn t => t,
adamc@316 155 exp = fn lower => fn e =>
adamc@316 156 case e of
adamc@316 157 ERel xn =>
adamc@316 158 if xn = lower then
adamc@316 159 ERel (lower + 1)
adamc@316 160 else if xn = lower + 1 then
adamc@316 161 ERel lower
adamc@316 162 else
adamc@316 163 e
adamc@316 164 | _ => e,
adamc@316 165 bind = fn (lower, U.Exp.RelE _) => lower+1
adamc@316 166 | (lower, _) => lower}
adamc@316 167
adamc@341 168 val swapExpVarsPat =
adamc@341 169 U.Exp.mapB {typ = fn t => t,
adamc@341 170 exp = fn (lower, len) => fn e =>
adamc@341 171 case e of
adamc@341 172 ERel xn =>
adamc@341 173 if xn = lower then
adamc@827 174 ERel (lower + len)
adamc@341 175 else if xn >= lower + 1 andalso xn < lower + 1 + len then
adamc@341 176 ERel (xn - 1)
adamc@341 177 else
adamc@341 178 e
adamc@341 179 | _ => e,
adamc@341 180 bind = fn ((lower, len), U.Exp.RelE _) => (lower+1, len)
adamc@341 181 | (st, _) => st}
adamc@341 182
adamc@814 183 datatype result = Yes of exp list | No | Maybe
adamc@258 184
adamc@183 185 fun match (env, p : pat, e : exp) =
adamc@183 186 case (#1 p, #1 e) of
adamc@258 187 (PWild, _) => Yes env
adamc@814 188 | (PVar (x, t), _) => Yes (e :: env)
adamc@183 189
adamc@280 190 | (PPrim (Prim.String s), EStrcat ((EPrim (Prim.String s'), _), _)) =>
adamc@280 191 if String.isPrefix s' s then
adamc@280 192 Maybe
adamc@280 193 else
adamc@280 194 No
adamc@280 195
adamc@1207 196 | (PPrim (Prim.String s), EStrcat (_, (EPrim (Prim.String s'), _))) =>
adamc@1207 197 if String.isSuffix s' s then
adamc@1207 198 Maybe
adamc@1207 199 else
adamc@1207 200 No
adamc@1207 201
adamc@183 202 | (PPrim p, EPrim p') =>
adamc@183 203 if Prim.equal (p, p') then
adamc@258 204 Yes env
adamc@183 205 else
adamc@258 206 No
adamc@183 207
adamc@188 208 | (PCon (_, PConVar n1, NONE), ECon (_, PConVar n2, NONE)) =>
adamc@183 209 if n1 = n2 then
adamc@258 210 Yes env
adamc@183 211 else
adamc@258 212 No
adamc@183 213
adamc@188 214 | (PCon (_, PConVar n1, SOME p), ECon (_, PConVar n2, SOME e)) =>
adamc@183 215 if n1 = n2 then
adamc@183 216 match (env, p, e)
adamc@183 217 else
adamc@258 218 No
adamc@183 219
adamc@188 220 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, NONE), ECon (_, PConFfi {mod = m2, con = con2, ...}, NONE)) =>
adamc@185 221 if m1 = m2 andalso con1 = con2 then
adamc@258 222 Yes env
adamc@185 223 else
adamc@258 224 No
adamc@185 225
adamc@188 226 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, SOME ep), ECon (_, PConFfi {mod = m2, con = con2, ...}, SOME e)) =>
adamc@185 227 if m1 = m2 andalso con1 = con2 then
adamc@185 228 match (env, p, e)
adamc@185 229 else
adamc@258 230 No
adamc@185 231
adamc@183 232 | (PRecord xps, ERecord xes) =>
adamc@183 233 let
adamc@183 234 fun consider (xps, env) =
adamc@183 235 case xps of
adamc@258 236 [] => Yes env
adamc@183 237 | (x, p, _) :: rest =>
adamc@183 238 case List.find (fn (x', _, _) => x' = x) xes of
adamc@258 239 NONE => No
adamc@183 240 | SOME (_, e, _) =>
adamc@183 241 case match (env, p, e) of
adamc@258 242 No => No
adamc@258 243 | Maybe => Maybe
adamc@258 244 | Yes env => consider (rest, env)
adamc@183 245 in
adamc@183 246 consider (xps, env)
adamc@183 247 end
adamc@183 248
adamc@726 249 | (PNone _, ENone _) => Yes env
adamc@921 250 | (PNone _, ESome _) => No
adamc@726 251 | (PSome (_, p), ESome (_, e)) => match (env, p, e)
adamc@921 252 | (PSome _, ENone _) => No
adamc@726 253
adamc@258 254 | _ => Maybe
adamc@183 255
adamc@318 256 datatype event =
adamc@318 257 WritePage
adamc@318 258 | ReadDb
adamc@318 259 | WriteDb
adamc@1225 260 | ReadCookie
adamc@1225 261 | WriteCookie
adamc@481 262 | UseRel
adamc@318 263 | Unsure
adamc@1225 264 | Abort
adamc@318 265
adamc@318 266 fun p_event e =
adamc@318 267 let
adamc@318 268 open Print.PD
adamc@318 269 in
adamc@318 270 case e of
adamc@318 271 WritePage => string "WritePage"
adamc@318 272 | ReadDb => string "ReadDb"
adamc@318 273 | WriteDb => string "WriteDb"
adamc@1225 274 | ReadCookie => string "ReadCookie"
adamc@1225 275 | WriteCookie => string "WriteCookie"
adamc@481 276 | UseRel => string "UseRel"
adamc@318 277 | Unsure => string "Unsure"
adamc@1225 278 | Abort => string "Abort"
adamc@318 279 end
adamc@318 280
adamc@470 281 val p_events = Print.p_list p_event
adamc@470 282
adamc@318 283 fun patBinds (p, _) =
adamc@318 284 case p of
adamc@318 285 PWild => 0
adamc@318 286 | PVar _ => 1
adamc@318 287 | PPrim _ => 0
adamc@318 288 | PCon (_, _, NONE) => 0
adamc@318 289 | PCon (_, _, SOME p) => patBinds p
adamc@318 290 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
adamc@318 291 | PNone _ => 0
adamc@318 292 | PSome (_, p) => patBinds p
adamc@318 293
adamc@932 294 val countFree = U.Exp.foldB {typ = fn (_, n) => n,
adamc@932 295 exp = fn (x, e, n) =>
adamc@932 296 case e of
adamc@932 297 ERel x' => if x = x' then n + 1 else n
adamc@932 298 | _ => n,
adamc@932 299 bind = fn (n, b) =>
adamc@932 300 case b of
adamc@932 301 U.Exp.RelE _ => n + 1
adamc@975 302 | _ => n}
adamc@975 303
adamc@975 304 val freeInAbs = U.Exp.existsB {typ = fn _ => false,
adamc@975 305 exp = fn (n, e) =>
adamc@975 306 case e of
adamc@975 307 EAbs (_, _, _, b) => countFree n 0 b > 0
adamc@975 308 | EJavaScript (_, b) => countFree n 0 b > 0
adamc@975 309 | _ => false,
adamc@975 310 bind = fn (n, b) =>
adamc@975 311 case b of
adamc@975 312 U.Exp.RelE _ => n + 1
adamc@975 313 | _ => n} 0
adamc@932 314
adamc@470 315 fun reduce file =
adamc@470 316 let
adamc@948 317 val (timpures, impures, absCounts) =
adamc@948 318 foldl (fn ((d, _), (timpures, impures, absCounts)) =>
adamc@916 319 let
adamc@916 320 fun countAbs (e, _) =
adamc@916 321 case e of
adamc@916 322 EAbs (_, _, _, e) => 1 + countAbs e
adamc@916 323 | _ => 0
adamc@916 324 in
adamc@916 325 case d of
adamc@948 326 DDatatype dts =>
adamc@948 327 (if List.exists (fn (_, _, cs) =>
adamc@948 328 List.exists (fn (_, _, NONE) => false
adamc@948 329 | (_, _, SOME t) => simpleTypeImpure timpures t) cs)
adamc@948 330 dts then
adamc@948 331 IS.addList (timpures, map #2 dts)
adamc@948 332 else
adamc@948 333 timpures,
adamc@948 334 impures,
adamc@948 335 absCounts)
adamc@948 336 | DVal (_, n, _, e, _) =>
adamc@948 337 (timpures,
adamc@948 338 if simpleImpure (timpures, impures) E.empty e then
adamc@916 339 IS.add (impures, n)
adamc@916 340 else
adamc@916 341 impures,
adamc@916 342 IM.insert (absCounts, n, countAbs e))
adamc@916 343 | DValRec vis =>
adamc@948 344 (timpures,
adamc@948 345 if List.exists (fn (_, _, _, e, _) => simpleImpure (timpures, impures) E.empty e) vis then
adamc@916 346 foldl (fn ((_, n, _, _, _), impures) =>
adamc@916 347 IS.add (impures, n)) impures vis
adamc@916 348 else
adamc@916 349 impures,
adamc@916 350 foldl (fn ((x, n, _, e, _), absCounts) =>
adamc@916 351 IM.insert (absCounts, n, countAbs e))
adamc@916 352 absCounts vis)
adamc@948 353 | _ => (timpures, impures, absCounts)
adamc@916 354 end)
adamc@948 355 (IS.empty, IS.empty, IM.empty) file
adamc@387 356
adamc@1017 357 val uses = U.File.fold {typ = fn (_, m) => m,
adamc@1017 358 exp = fn (e, m) =>
adamc@1017 359 case e of
adamc@1017 360 ENamed n => IM.insert (m, n, 1 + Option.getOpt (IM.find (m, n), 0))
adamc@1017 361 | _ => m,
adamc@1017 362 decl = fn (_, m) => m}
adamc@1017 363 IM.empty file
adamc@1017 364
adamc@1017 365 val size = U.Exp.fold {typ = fn (_, n) => n,
adamc@1017 366 exp = fn (_, n) => n + 1} 0
adamc@1017 367
adam@1360 368 val functionInside' = U.Typ.exists (fn c => case c of
adam@1360 369 TFun _ => true
adam@1360 370 | _ => false)
adam@1360 371
adam@1360 372 fun functionInside t =
adam@1360 373 case #1 t of
adam@1360 374 TFun (t1, t2) => functionInside' t1 orelse functionInside t2
adam@1360 375 | _ => functionInside' t
adam@1360 376
adam@1360 377 fun mayInline (n, e, t) =
adamc@1017 378 case IM.find (uses, n) of
adamc@1017 379 NONE => false
adamc@1017 380 | SOME count => count <= 1
adamc@1017 381 orelse size e <= Settings.getMonoInline ()
adam@1360 382 orelse functionInside t
adamc@1017 383
adamc@470 384 fun summarize d (e, _) =
adamc@579 385 let
adamc@579 386 val s =
adamc@579 387 case e of
adamc@579 388 EPrim _ => []
adamc@579 389 | ERel n => if n = d then [UseRel] else []
adamc@579 390 | ENamed _ => []
adamc@579 391 | ECon (_, _, NONE) => []
adamc@579 392 | ECon (_, _, SOME e) => summarize d e
adamc@579 393 | ENone _ => []
adamc@579 394 | ESome (_, e) => summarize d e
adamc@579 395 | EFfi _ => []
adamc@1225 396 | EFfiApp ("Basis", "get_cookie", [e]) =>
adamc@1225 397 summarize d e @ [ReadCookie]
adamc@765 398 | EFfiApp (m, x, es) =>
adamc@1171 399 if Settings.isEffectful (m, x) orelse Settings.isBenignEffectful (m, x) then
adamc@765 400 List.concat (map (summarize d) es) @ [Unsure]
adamc@765 401 else
adamc@765 402 List.concat (map (summarize d) es)
adamc@579 403 | EApp ((EFfi _, _), e) => summarize d e
adamc@579 404 | EApp _ =>
adamc@579 405 let
adamc@694 406 fun unravel (e, passed, ls) =
adamc@579 407 case e of
adamc@579 408 ENamed n =>
adamc@579 409 let
adamc@579 410 val ls = rev ls
adamc@579 411 in
adamc@948 412 if IS.member (impures, n) then
adamc@948 413 case IM.find (absCounts, n) of
adamc@948 414 NONE => [Unsure]
adamc@948 415 | SOME len =>
adamc@948 416 if passed < len then
adamc@948 417 ls
adamc@948 418 else
adamc@948 419 ls @ [Unsure]
adamc@948 420 else
adamc@948 421 ls
adamc@579 422 end
adamc@579 423 | ERel n => List.revAppend (ls,
adamc@579 424 if n = d then
adamc@579 425 [UseRel, Unsure]
adamc@579 426 else
adamc@579 427 [Unsure])
adamc@579 428 | EApp (f, x) =>
adamc@995 429 unravel (#1 f, passed + 1, List.revAppend (summarize d x,
adamc@995 430 ls))
adamc@579 431 | _ => [Unsure]
adamc@579 432 in
adamc@694 433 unravel (e, 0, [])
adamc@579 434 end
adamc@252 435
adamc@941 436 | EAbs _ => []
adamc@316 437
adamc@579 438 | EUnop (_, e) => summarize d e
adam@1360 439 | EBinop (_, _, e1, e2) => summarize d e1 @ summarize d e2
adamc@470 440
adamc@579 441 | ERecord xets => List.concat (map (summarize d o #2) xets)
adamc@579 442 | EField (e, _) => summarize d e
adamc@470 443
adamc@1214 444 | ECase (e, pes, _) =>
adamc@1214 445 let
adamc@579 446 val lss = map (fn (p, e) => summarize (d + patBinds p) e) pes
adamc@579 447 in
adamc@579 448 case lss of
adam@1298 449 [] => summarize d e
adamc@579 450 | ls :: lss =>
adamc@1214 451 summarize d e
adamc@1214 452 @ (if List.all (fn ls' => ls' = ls) lss then
adamc@1214 453 ls
adamc@1214 454 else if length (List.filter (not o List.null) (ls :: lss)) <= 1 then
adamc@1214 455 valOf (List.find (not o List.null) (ls :: lss))
adamc@1214 456 else
adamc@1214 457 [Unsure])
adamc@1214 458 end
adamc@579 459 | EStrcat (e1, e2) => summarize d e1 @ summarize d e2
adamc@316 460
adamc@1225 461 | EError (e, _) => summarize d e @ [Abort]
adamc@1225 462 | EReturnBlob {blob = e1, mimeType = e2, ...} => summarize d e1 @ summarize d e2 @ [Abort]
adamc@1225 463 | ERedirect (e, _) => summarize d e @ [Abort]
adamc@318 464
adamc@579 465 | EWrite e => summarize d e @ [WritePage]
adamc@579 466
adamc@579 467 | ESeq (e1, e2) => summarize d e1 @ summarize d e2
adamc@579 468 | ELet (_, _, e1, e2) => summarize d e1 @ summarize (d + 1) e2
adamc@456 469
adamc@579 470 | EClosure (_, es) => List.concat (map (summarize d) es)
adamc@470 471
adamc@579 472 | EQuery {query, body, initial, ...} =>
adamc@579 473 List.concat [summarize d query,
adamc@579 474 summarize d initial,
adamc@941 475 [ReadDb],
adamc@941 476 summarize (d + 2) body]
adamc@470 477
adam@1293 478 | EDml (e, _) => summarize d e @ [WriteDb]
adamc@579 479 | ENextval e => summarize d e @ [WriteDb]
adamc@1073 480 | ESetval (e1, e2) => summarize d e1 @ summarize d e2 @ [WriteDb]
adamc@1112 481 | EUnurlify (e, _, _) => summarize d e
adamc@815 482 | EJavaScript (_, e) => summarize d e
adamc@579 483 | ESignalReturn e => summarize d e
adamc@579 484 | ESignalBind (e1, e2) => summarize d e1 @ summarize d e2
adamc@579 485 | ESignalSource e => summarize d e
adamc@608 486
adamc@1020 487 | EServerCall (e, _, _) => summarize d e @ [Unsure]
adamc@1021 488 | ERecv (e, _) => summarize d e @ [Unsure]
adamc@1021 489 | ESleep e => summarize d e @ [Unsure]
adamc@1021 490 | ESpawn e => summarize d e @ [Unsure]
adamc@579 491 in
adamc@579 492 (*Print.prefaces "Summarize"
adamc@579 493 [("e", MonoPrint.p_exp MonoEnv.empty (e, ErrorMsg.dummySpan)),
adamc@579 494 ("d", Print.PD.string (Int.toString d)),
adamc@579 495 ("s", p_events s)];*)
adamc@579 496 s
adamc@579 497 end
adamc@470 498
adamc@919 499 val impure = fn env => fn e =>
adamc@948 500 simpleImpure (timpures, impures) env e andalso impure e
adamc@916 501 andalso not (List.null (summarize ~1 e))
adamc@916 502
adamc@470 503 fun exp env e =
adamc@470 504 let
adamc@470 505 (*val () = Print.prefaces "exp" [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan))]*)
adamc@470 506
adamc@1017 507 fun doLet (x, t, e', b) =
adamc@1017 508 let
adamc@1017 509 fun doSub () =
adamc@1017 510 let
adamc@1017 511 val r = subExpInExp (0, e') b
adamc@1017 512 in
adamc@1017 513 (*Print.prefaces "doSub" [("e'", MonoPrint.p_exp env e'),
adamc@1017 514 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b),
adamc@1017 515 ("r", MonoPrint.p_exp env r)];*)
adamc@1017 516 #1 (reduceExp env r)
adamc@1017 517 end
adamc@1017 518
adamc@1017 519 fun trySub () =
adamc@1017 520 ((*Print.prefaces "trySub"
adamc@1017 521 [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan))];*)
adamc@1017 522 case t of
adamc@1017 523 (TFfi ("Basis", "string"), _) => doSub ()
adamc@1017 524 | (TSignal _, _) => e
adamc@1017 525 | _ =>
adamc@1017 526 case e' of
adamc@1017 527 (ECase _, _) => e
adamc@1017 528 | _ => doSub ())
adamc@1017 529 in
adamc@1017 530 if impure env e' then
adamc@1017 531 let
adamc@1017 532 val effs_e' = summarize 0 e'
adamc@1017 533 val effs_e' = List.filter (fn x => x <> UseRel) effs_e'
adamc@1017 534 val effs_b = summarize 0 b
adamc@1017 535
adamc@1017 536 (*val () = Print.prefaces "Try"
adamc@1017 537 [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan)),
adamc@1017 538 ("e'", MonoPrint.p_exp env e'),
adamc@1017 539 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b),
adamc@1017 540 ("e'_eff", p_events effs_e'),
adamc@1017 541 ("b_eff", p_events effs_b)]*)
adamc@1017 542
adamc@1017 543 fun does eff = List.exists (fn eff' => eff' = eff) effs_e'
adamc@1017 544 val writesPage = does WritePage
adamc@1017 545 val readsDb = does ReadDb
adamc@1017 546 val writesDb = does WriteDb
adamc@1225 547 val readsCookie = does ReadCookie
adamc@1225 548 val writesCookie = does ReadCookie
adamc@1017 549
adamc@1017 550 fun verifyUnused eff =
adamc@1017 551 case eff of
adamc@1017 552 UseRel => false
adamc@1017 553 | _ => true
adamc@1017 554
adamc@1017 555 fun verifyCompatible effs =
adamc@1017 556 case effs of
adamc@1017 557 [] => false
adamc@1017 558 | eff :: effs =>
adamc@1017 559 case eff of
adamc@1017 560 Unsure => false
adamc@1017 561 | UseRel => List.all verifyUnused effs
adamc@1017 562 | WritePage => not writesPage andalso verifyCompatible effs
adamc@1017 563 | ReadDb => not writesDb andalso verifyCompatible effs
adamc@1017 564 | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs
adamc@1225 565 | ReadCookie => not writesCookie andalso verifyCompatible effs
adamc@1225 566 | WriteCookie => not writesCookie andalso not readsCookie
adamc@1225 567 andalso verifyCompatible effs
adamc@1225 568 | Abort => true
adamc@1017 569 in
adamc@1017 570 (*Print.prefaces "verifyCompatible"
adamc@1017 571 [("e'", MonoPrint.p_exp env e'),
adamc@1017 572 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b),
adamc@1017 573 ("effs_e'", Print.p_list p_event effs_e'),
adamc@1017 574 ("effs_b", Print.p_list p_event effs_b)];*)
adamc@1017 575 if (List.null effs_e'
adamc@1017 576 orelse (List.all (fn eff => eff <> Unsure) effs_e'
adamc@1017 577 andalso verifyCompatible effs_b)
adamc@1017 578 orelse (case effs_b of
adamc@1017 579 UseRel :: effs => List.all verifyUnused effs
adamc@1017 580 | _ => false))
adamc@1017 581 andalso countFree 0 0 b = 1
adamc@1017 582 andalso not (freeInAbs b) then
adamc@1017 583 trySub ()
adamc@1017 584 else
adamc@1017 585 e
adamc@1017 586 end
adamc@1017 587 else
adamc@1017 588 trySub ()
adamc@1017 589 end
adamc@1017 590
adamc@470 591 val r =
adamc@470 592 case e of
adamc@470 593 ERel n =>
adamc@470 594 (case E.lookupERel env n of
adamc@470 595 (_, _, SOME e') => #1 e'
adamc@470 596 | _ => e)
adamc@470 597 | ENamed n =>
adamc@470 598 (case E.lookupENamed env n of
adamc@470 599 (_, _, SOME e', _) => ((*Print.prefaces "Switch" [("n", Print.PD.string (Int.toString n)),
adamc@470 600 ("e'", MonoPrint.p_exp env e')];*)
adamc@470 601 #1 e')
adamc@470 602 | _ => e)
adamc@470 603
adamc@470 604 | EApp ((EAbs (x, t, _, e1), loc), e2) =>
adamc@470 605 ((*Print.prefaces "Considering" [("e1", MonoPrint.p_exp (E.pushERel env x t NONE) e1),
adamc@694 606 ("e2", MonoPrint.p_exp env e2),
adamc@694 607 ("sub", MonoPrint.p_exp env (reduceExp env (subExpInExp (0, e2) e1)))];*)
adamc@975 608 if impure env e2 orelse countFree 0 0 e1 > 1 then
adamc@470 609 #1 (reduceExp env (ELet (x, t, e2, e1), loc))
adamc@470 610 else
adamc@470 611 #1 (reduceExp env (subExpInExp (0, e2) e1)))
adamc@470 612
adamc@470 613 | ECase (e', pes, {disc, result}) =>
adamc@442 614 let
adamc@470 615 fun push () =
adamc@470 616 case result of
adamc@470 617 (TFun (dom, result), loc) =>
adamc@1107 618 let
adamc@1107 619 fun safe (e, _) =
adamc@1107 620 case e of
adamc@1107 621 EAbs _ => true
adamc@1107 622 | _ => false
adamc@1107 623 in
adamc@1107 624 if List.all (safe o #2) pes then
adamc@1107 625 EAbs ("y", dom, result,
adamc@1107 626 (ECase (liftExpInExp 0 e',
adamc@1107 627 map (fn (p, (EAbs (_, _, _, e), _)) =>
adamc@1107 628 (p, swapExpVarsPat (0, patBinds p) e)
adamc@1107 629 | _ => raise Fail "MonoReduce ECase") pes,
adamc@1107 630 {disc = disc, result = result}), loc))
adamc@1107 631 else
adamc@1107 632 e
adamc@1107 633 end
adamc@470 634 | _ => e
adamc@318 635
adamc@470 636 fun search pes =
adamc@470 637 case pes of
adamc@470 638 [] => push ()
adamc@470 639 | (p, body) :: pes =>
adamc@814 640 case match ([], p, e') of
adamc@470 641 No => search pes
adamc@470 642 | Maybe => push ()
adamc@814 643 | Yes subs =>
adamc@800 644 let
adamc@829 645 val (body, remaining) =
adamc@829 646 foldl (fn (e, (body, remaining)) =>
adamc@829 647 (subExpInExp (0, multiLift remaining e) body, remaining - 1))
adamc@829 648 (body, length subs - 1) subs
adamc@920 649 val r = reduceExp (E.patBinds env p) body
adamc@800 650 in
adamc@829 651 (*Print.preface ("subs", Print.p_list (MonoPrint.p_exp env) subs);*)
adamc@800 652 (*Print.prefaces "ECase"
adamc@829 653 [("old", MonoPrint.p_exp env body),
adamc@829 654 ("body", MonoPrint.p_exp env body),
adamc@800 655 ("r", MonoPrint.p_exp env r)];*)
adamc@800 656 #1 r
adamc@800 657 end
adamc@470 658 in
adamc@941 659 if impure env e' then
adamc@941 660 e
adamc@941 661 else
adamc@941 662 search pes
adamc@470 663 end
adamc@318 664
adamc@470 665 | EField ((ERecord xes, _), x) =>
adamc@470 666 (case List.find (fn (x', _, _) => x' = x) xes of
adamc@470 667 SOME (_, e, _) => #1 e
adamc@470 668 | NONE => e)
adamc@398 669
adamc@470 670 | ELet (x1, t1, (ELet (x2, t2, e1, b1), loc), b2) =>
adamc@470 671 let
adamc@470 672 val e' = (ELet (x2, t2, e1,
adamc@470 673 (ELet (x1, t1, b1,
adamc@470 674 liftExpInExp 1 b2), loc)), loc)
adamc@442 675 in
adamc@470 676 (*Print.prefaces "ELet commute" [("e", MonoPrint.p_exp env (e, loc)),
adamc@470 677 ("e'", MonoPrint.p_exp env e')];*)
adamc@470 678 #1 (reduceExp env e')
adamc@470 679 end
adamc@470 680 | EApp ((ELet (x, t, e, b), loc), e') =>
adamc@470 681 #1 (reduceExp env (ELet (x, t, e,
adamc@470 682 (EApp (b, liftExpInExp 0 e'), loc)), loc))
adamc@470 683
adamc@1017 684 | ELet (x, t, e', b as (EAbs (x', t' as (TRecord [], _), ran, e''), loc)) =>
adamc@919 685 if impure env e' then
adamc@1017 686 doLet (x, t, e', b)
adamc@848 687 else
adamc@920 688 EAbs (x', t', ran, reduceExp (E.pushERel env x' t' NONE)
adamc@920 689 (ELet (x, t, liftExpInExp 0 e', swapExpVars 0 e''), loc))
adamc@470 690
adamc@1017 691 | ELet (x, t, e', b) => doLet (x, t, e', b)
adamc@252 692
adamc@470 693 | EStrcat ((EPrim (Prim.String s1), _), (EPrim (Prim.String s2), _)) =>
adamc@470 694 EPrim (Prim.String (s1 ^ s2))
adamc@268 695
adamc@572 696 | ESignalBind ((ESignalReturn e1, loc), e2) =>
adamc@572 697 #1 (reduceExp env (EApp (e2, e1), loc))
adamc@572 698
adamc@470 699 | _ => e
adamc@470 700 in
adamc@829 701 (*Print.prefaces "exp'" [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan)),
adamc@829 702 ("r", MonoPrint.p_exp env (r, ErrorMsg.dummySpan))];*)
adamc@470 703 r
adamc@470 704 end
adamc@470 705
adamc@470 706 and bind (env, b) =
adamc@470 707 case b of
adamc@470 708 U.Decl.Datatype (x, n, xncs) => E.pushDatatype env x n xncs
adamc@470 709 | U.Decl.RelE (x, t) => E.pushERel env x t NONE
adamc@1017 710 | U.Decl.NamedE (x, n, t, eo, s) =>
adamc@1017 711 let
adamc@1017 712 val eo = case eo of
adamc@1017 713 NONE => NONE
adam@1360 714 | SOME e => if mayInline (n, e, t) then
adamc@1017 715 SOME e
adamc@1017 716 else
adamc@1017 717 NONE
adamc@1017 718 in
adamc@1017 719 E.pushENamed env x n t (Option.map (reduceExp env) eo) s
adamc@1017 720 end
adamc@470 721
adamc@470 722 and reduceExp env = U.Exp.mapB {typ = typ, exp = exp, bind = bind} env
adamc@470 723
adamc@801 724 fun decl env d = ((*Print.preface ("d", MonoPrint.p_decl env (d, ErrorMsg.dummySpan));*)
adamc@801 725 d)
adamc@398 726 in
adamc@470 727 U.File.mapB {typ = typ, exp = exp, decl = decl, bind = bind} E.empty file
adamc@398 728 end
adamc@133 729
adamc@133 730 end