Mercurial > urweb

comparison src/mono_reduce.sml @ 470:7cb418e9714f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tree demo works
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 18:49:38 -0500
parents ddd363e856ff
children 2280193bf298
comparison
equal deleted inserted replaced
469:b393c2fc80f8 470:7cb418e9714f
32 open Mono 32 open Mono
33 33
34 structure E = MonoEnv 34 structure E = MonoEnv
35 structure U = MonoUtil 35 structure U = MonoUtil
36 36
37 structure IM = IntBinaryMap
38
37 39
38 fun impure (e, _) = 40 fun impure (e, _) =
39 case e of 41 case e of
40 EWrite _ => true 42 EWrite _ => true
41 | EQuery _ => true 43 | EQuery _ => true
210 | WriteDb => string "WriteDb" 212 | WriteDb => string "WriteDb"
211 | UseRel n => string ("UseRel" ^ Int.toString n) 213 | UseRel n => string ("UseRel" ^ Int.toString n)
212 | Unsure => string "Unsure" 214 | Unsure => string "Unsure"
213 end 215 end
214 216
217 val p_events = Print.p_list p_event
218
215 fun patBinds (p, _) = 219 fun patBinds (p, _) =
216 case p of 220 case p of
217 PWild => 0 221 PWild => 0
218 | PVar _ => 1 222 | PVar _ => 1
219 | PPrim _ => 0 223 | PPrim _ => 0
221 | PCon (_, _, SOME p) => patBinds p 225 | PCon (_, _, SOME p) => patBinds p
222 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts 226 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
223 | PNone _ => 0 227 | PNone _ => 0
224 | PSome (_, p) => patBinds p 228 | PSome (_, p) => patBinds p
225 229
226 fun summarize d (e, _) = 230 fun reduce file =
227 case e of
228 EPrim _ => []
229 | ERel n => if n >= d then [UseRel (n - d)] else []
230 | ENamed _ => []
231 | ECon (_, _, NONE) => []
232 | ECon (_, _, SOME e) => summarize d e
233 | ENone _ => []
234 | ESome (_, e) => summarize d e
235 | EFfi _ => []
236 | EFfiApp ("Basis", "set_cookie", _) => [Unsure]
237 | EFfiApp (_, _, es) => List.concat (map (summarize d) es)
238 | EApp ((EFfi _, _), e) => summarize d e
239 | EApp _ => [Unsure]
240 | EAbs _ => []
241
242 | EUnop (_, e) => summarize d e
243 | EBinop (_, e1, e2) => summarize d e1 @ summarize d e2
244
245 | ERecord xets => List.concat (map (summarize d o #2) xets)
246 | EField (e, _) => summarize d e
247
248 | ECase (e, pes, _) =>
249 let
250 val lss = map (fn (p, e) => summarize (d + patBinds p) e) pes
251 in
252 case lss of
253 [] => raise Fail "Empty pattern match"
254 | ls :: lss =>
255 if List.all (fn ls' => ls' = ls) lss then
256 summarize d e @ ls
257 else
258 [Unsure]
259 end
260 | EStrcat (e1, e2) => summarize d e1 @ summarize d e2
261
262 | EError (e, _) => summarize d e @ [Unsure]
263
264 | EWrite e => summarize d e @ [WritePage]
265
266 | ESeq (e1, e2) => summarize d e1 @ summarize d e2
267 | ELet (_, _, e1, e2) => summarize d e1 @ summarize (d + 1) e2
268
269 | EClosure (_, es) => List.concat (map (summarize d) es)
270
271 | EQuery {query, body, initial, ...} =>
272 List.concat [summarize d query,
273 summarize (d + 2) body,
274 summarize d initial,
275 [ReadDb]]
276
277 | EDml e => summarize d e @ [WriteDb]
278 | ENextval e => summarize d e @ [WriteDb]
279 | EUnurlify (e, _) => summarize d e
280
281 fun exp env e =
282 let 231 let
283 (*val () = Print.prefaces "exp" [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan))]*) 232 fun countAbs (e, _) =
284
285 val r =
286 case e of 233 case e of
287 ERel n => 234 EAbs (_, _, _, e) => 1 + countAbs e
288 (case E.lookupERel env n of 235 | _ => 0
289 (_, _, SOME e') => #1 e' 236
290 | _ => e) 237 val absCounts =
291 | ENamed n => 238 foldl (fn ((d, _), absCounts) =>
292 (case E.lookupENamed env n of 239 case d of
293 (_, _, SOME e', _) => ((*Print.prefaces "Switch" [("n", Print.PD.string (Int.toString n)), 240 DVal (_, n, _, e, _) =>
294 ("e'", MonoPrint.p_exp env e')];*) 241 IM.insert (absCounts, n, countAbs e)
295 #1 e') 242 | DValRec vis =>
296 | _ => e) 243 foldl (fn ((_, n, _, e, _), absCounts) =>
297 244 IM.insert (absCounts, n, countAbs e))
298 | EApp ((EAbs (x, t, _, e1), loc), e2) => 245 absCounts vis
299 ((*Print.prefaces "Considering" [("e1", MonoPrint.p_exp (E.pushERel env x t NONE) e1), 246 | _ => absCounts)
300 ("e2", MonoPrint.p_exp env e2), 247 IM.empty file
301 ("sub", MonoPrint.p_exp env (reduceExp env (subExpInExp (0, e2) e1)))];*) 248
302 if impure e2 then 249 fun summarize d (e, _) =
303 #1 (reduceExp env (ELet (x, t, e2, e1), loc)) 250 case e of
304 else 251 EPrim _ => []
305 #1 (reduceExp env (subExpInExp (0, e2) e1))) 252 | ERel n => if n >= d then [UseRel (n - d)] else []
306 253 | ENamed _ => []
307 | ECase (e', pes, {disc, result}) => 254 | ECon (_, _, NONE) => []
255 | ECon (_, _, SOME e) => summarize d e
256 | ENone _ => []
257 | ESome (_, e) => summarize d e
258 | EFfi _ => []
259 | EFfiApp ("Basis", "set_cookie", _) => [Unsure]
260 | EFfiApp (_, _, es) => List.concat (map (summarize d) es)
261 | EApp ((EFfi _, _), e) => summarize d e
262 | EApp _ =>
308 let 263 let
309 fun push () = 264 fun unravel (e, ls) =
310 case result of 265 case e of
311 (TFun (dom, result), loc) => 266 ENamed n =>
312 if List.all (fn (_, (EAbs _, _)) => true | _ => false) pes then 267 let
313 EAbs ("_", dom, result, 268 val ls = rev ls
314 (ECase (liftExpInExp 0 e', 269 in
315 map (fn (p, (EAbs (_, _, _, e), _)) => 270 case IM.find (absCounts, n) of
316 (p, swapExpVarsPat (0, patBinds p) e) 271 NONE => [Unsure]
317 | _ => raise Fail "MonoReduce ECase") pes, 272 | SOME len =>
318 {disc = disc, result = result}), loc)) 273 if length ls < len then
274 ls
275 else
276 [Unsure]
277 end
278 | ERel n => List.revAppend (ls, [UseRel (n - d), Unsure])
279 | EApp (f, x) =>
280 unravel (#1 f, summarize d x @ ls)
281 | _ => [Unsure]
282 in
283 unravel (e, [])
284 end
285
286 | EAbs _ => []
287
288 | EUnop (_, e) => summarize d e
289 | EBinop (_, e1, e2) => summarize d e1 @ summarize d e2
290
291 | ERecord xets => List.concat (map (summarize d o #2) xets)
292 | EField (e, _) => summarize d e
293
294 | ECase (e, pes, _) =>
295 let
296 val lss = map (fn (p, e) => summarize (d + patBinds p) e) pes
297 in
298 case lss of
299 [] => raise Fail "Empty pattern match"
300 | ls :: lss =>
301 if List.all (fn ls' => ls' = ls) lss then
302 summarize d e @ ls
303 else
304 [Unsure]
305 end
306 | EStrcat (e1, e2) => summarize d e1 @ summarize d e2
307
308 | EError (e, _) => summarize d e @ [Unsure]
309
310 | EWrite e => summarize d e @ [WritePage]
311
312 | ESeq (e1, e2) => summarize d e1 @ summarize d e2
313 | ELet (_, _, e1, e2) => summarize d e1 @ summarize (d + 1) e2
314
315 | EClosure (_, es) => List.concat (map (summarize d) es)
316
317 | EQuery {query, body, initial, ...} =>
318 List.concat [summarize d query,
319 summarize (d + 2) body,
320 summarize d initial,
321 [ReadDb]]
322
323 | EDml e => summarize d e @ [WriteDb]
324 | ENextval e => summarize d e @ [WriteDb]
325 | EUnurlify (e, _) => summarize d e
326
327
328 fun exp env e =
329 let
330 (*val () = Print.prefaces "exp" [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan))]*)
331
332 val r =
333 case e of
334 ERel n =>
335 (case E.lookupERel env n of
336 (_, _, SOME e') => #1 e'
337 | _ => e)
338 | ENamed n =>
339 (case E.lookupENamed env n of
340 (_, _, SOME e', _) => ((*Print.prefaces "Switch" [("n", Print.PD.string (Int.toString n)),
341 ("e'", MonoPrint.p_exp env e')];*)
342 #1 e')
343 | _ => e)
344
345 | EApp ((EAbs (x, t, _, e1), loc), e2) =>
346 ((*Print.prefaces "Considering" [("e1", MonoPrint.p_exp (E.pushERel env x t NONE) e1),
347 ("e2", MonoPrint.p_exp env e2),
348 ("sub", MonoPrint.p_exp env (reduceExp env (subExpInExp (0, e2) e1)))];*)
349 if impure e2 then
350 #1 (reduceExp env (ELet (x, t, e2, e1), loc))
351 else
352 #1 (reduceExp env (subExpInExp (0, e2) e1)))
353
354 | ECase (e', pes, {disc, result}) =>
355 let
356 fun push () =
357 case result of
358 (TFun (dom, result), loc) =>
359 if List.all (fn (_, (EAbs _, _)) => true | _ => false) pes then
360 EAbs ("_", dom, result,
361 (ECase (liftExpInExp 0 e',
362 map (fn (p, (EAbs (_, _, _, e), _)) =>
363 (p, swapExpVarsPat (0, patBinds p) e)
364 | _ => raise Fail "MonoReduce ECase") pes,
365 {disc = disc, result = result}), loc))
366 else
367 e
368 | _ => e
369
370 fun search pes =
371 case pes of
372 [] => push ()
373 | (p, body) :: pes =>
374 case match (env, p, e') of
375 No => search pes
376 | Maybe => push ()
377 | Yes env => #1 (reduceExp env body)
378 in
379 search pes
380 end
381
382 | EField ((ERecord xes, _), x) =>
383 (case List.find (fn (x', _, _) => x' = x) xes of
384 SOME (_, e, _) => #1 e
385 | NONE => e)
386
387 | ELet (x1, t1, (ELet (x2, t2, e1, b1), loc), b2) =>
388 let
389 val e' = (ELet (x2, t2, e1,
390 (ELet (x1, t1, b1,
391 liftExpInExp 1 b2), loc)), loc)
392 in
393 (*Print.prefaces "ELet commute" [("e", MonoPrint.p_exp env (e, loc)),
394 ("e'", MonoPrint.p_exp env e')];*)
395 #1 (reduceExp env e')
396 end
397 | EApp ((ELet (x, t, e, b), loc), e') =>
398 #1 (reduceExp env (ELet (x, t, e,
399 (EApp (b, liftExpInExp 0 e'), loc)), loc))
400
401 | ELet (x, t, e', (EAbs (x', t' as (TRecord [], _), ran, e''), loc)) =>
402 (*if impure e' then
403 e
404 else*)
405 (* Seems unsound in general without the check... should revisit later *)
406 EAbs (x', t', ran, (ELet (x, t, liftExpInExp 0 e', swapExpVars 0 e''), loc))
407
408 | ELet (x, t, e', b) =>
409 let
410 fun doSub () =
411 #1 (reduceExp env (subExpInExp (0, e') b))
412
413 fun trySub () =
414 case t of
415 (TFfi ("Basis", "string"), _) => doSub ()
416 | _ =>
417 case e' of
418 (ECase _, _) => e
419 | _ => doSub ()
420 in
421 if impure e' then
422 let
423 val effs_e' = summarize 0 e'
424 val effs_b = summarize 0 b
425
426 (*val () = Print.prefaces "Try"
427 [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan)),
428 ("e'", p_events effs_e'),
429 ("b", p_events effs_b)]*)
430
431 fun does eff = List.exists (fn eff' => eff' = eff) effs_e'
432 val writesPage = does WritePage
433 val readsDb = does ReadDb
434 val writesDb = does WriteDb
435
436 fun verifyUnused eff =
437 case eff of
438 UseRel r => r <> 0
439 | _ => true
440
441 fun verifyCompatible effs =
442 case effs of
443 [] => false
444 | eff :: effs =>
445 case eff of
446 Unsure => false
447 | UseRel r =>
448 if r = 0 then
449 List.all verifyUnused effs
450 else
451 verifyCompatible effs
452 | WritePage => not writesPage andalso verifyCompatible effs
453 | ReadDb => not writesDb andalso verifyCompatible effs
454 | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs
455 in
456 (*Print.prefaces "verifyCompatible"
457 [("e'", MonoPrint.p_exp env e'),
458 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b),
459 ("effs_e'", Print.p_list p_event effs_e'),
460 ("effs_b", Print.p_list p_event effs_b)];*)
461 if verifyCompatible effs_b then
462 trySub ()
463 else
464 e
465 end
319 else 466 else
320 e
321 | _ => e
322
323 fun search pes =
324 case pes of
325 [] => push ()
326 | (p, body) :: pes =>
327 case match (env, p, e') of
328 No => search pes
329 | Maybe => push ()
330 | Yes env => #1 (reduceExp env body)
331 in
332 search pes
333 end
334
335 | EField ((ERecord xes, _), x) =>
336 (case List.find (fn (x', _, _) => x' = x) xes of
337 SOME (_, e, _) => #1 e
338 | NONE => e)
339
340 | ELet (x1, t1, (ELet (x2, t2, e1, b1), loc), b2) =>
341 let
342 val e' = (ELet (x2, t2, e1,
343 (ELet (x1, t1, b1,
344 liftExpInExp 1 b2), loc)), loc)
345 in
346 (*Print.prefaces "ELet commute" [("e", MonoPrint.p_exp env (e, loc)),
347 ("e'", MonoPrint.p_exp env e')];*)
348 #1 (reduceExp env e')
349 end
350 | EApp ((ELet (x, t, e, b), loc), e') =>
351 #1 (reduceExp env (ELet (x, t, e,
352 (EApp (b, liftExpInExp 0 e'), loc)), loc))
353
354 | ELet (x, t, e', (EAbs (x', t' as (TRecord [], _), ran, e''), loc)) =>
355 (*if impure e' then
356 e
357 else*)
358 (* Seems unsound in general without the check... should revisit later *)
359 EAbs (x', t', ran, (ELet (x, t, liftExpInExp 0 e', swapExpVars 0 e''), loc))
360
361 | ELet (x, t, e', b) =>
362 let
363 fun doSub () =
364 #1 (reduceExp env (subExpInExp (0, e') b))
365
366 fun trySub () =
367 case t of
368 (TFfi ("Basis", "string"), _) => doSub ()
369 | _ =>
370 case e' of
371 (ECase _, _) => e
372 | _ => doSub ()
373 in
374 if impure e' then
375 let
376 val effs_e' = summarize 0 e'
377 val effs_b = summarize 0 b
378
379 fun does eff = List.exists (fn eff' => eff' = eff) effs_e'
380 val writesPage = does WritePage
381 val readsDb = does ReadDb
382 val writesDb = does WriteDb
383
384 fun verifyUnused eff =
385 case eff of
386 UseRel r => r <> 0
387 | Unsure => false
388 | _ => true
389
390 fun verifyCompatible effs =
391 case effs of
392 [] => false
393 | eff :: effs =>
394 case eff of
395 Unsure => false
396 | UseRel r =>
397 if r = 0 then
398 List.all verifyUnused effs
399 else
400 verifyCompatible effs
401 | WritePage => not writesPage andalso verifyCompatible effs
402 | ReadDb => not writesDb andalso verifyCompatible effs
403 | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs
404 in
405 (*Print.prefaces "verifyCompatible"
406 [("e'", MonoPrint.p_exp env e'),
407 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b),
408 ("effs_e'", Print.p_list p_event effs_e'),
409 ("effs_b", Print.p_list p_event effs_b)];*)
410 if verifyCompatible effs_b then
411 trySub () 467 trySub ()
412 else
413 e
414 end 468 end
415 else 469
416 trySub () 470 | EStrcat ((EPrim (Prim.String s1), _), (EPrim (Prim.String s2), _)) =>
417 end 471 EPrim (Prim.String (s1 ^ s2))
418 472
419 | EStrcat ((EPrim (Prim.String s1), _), (EPrim (Prim.String s2), _)) => 473 | _ => e
420 EPrim (Prim.String (s1 ^ s2)) 474 in
421 475 (*Print.prefaces "exp'" [("r", MonoPrint.p_exp env (r, ErrorMsg.dummySpan))];*)
422 | _ => e 476 r
477 end
478
479 and bind (env, b) =
480 case b of
481 U.Decl.Datatype (x, n, xncs) => E.pushDatatype env x n xncs
482 | U.Decl.RelE (x, t) => E.pushERel env x t NONE
483 | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t (Option.map (reduceExp env) eo) s
484
485 and reduceExp env = U.Exp.mapB {typ = typ, exp = exp, bind = bind} env
486
487 fun decl env d = d
423 in 488 in
424 (*Print.prefaces "exp'" [("r", MonoPrint.p_exp env (r, ErrorMsg.dummySpan))];*) 489 U.File.mapB {typ = typ, exp = exp, decl = decl, bind = bind} E.empty file
425 r
426 end 490 end
427 491
428 and bind (env, b) =
429 case b of
430 U.Decl.Datatype (x, n, xncs) => E.pushDatatype env x n xncs
431 | U.Decl.RelE (x, t) => E.pushERel env x t NONE
432 | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t (Option.map (reduceExp env) eo) s
433
434 and reduceExp env = U.Exp.mapB {typ = typ, exp = exp, bind = bind} env
435
436 fun decl env d = d
437
438 val reduce = U.File.mapB {typ = typ, exp = exp, decl = decl, bind = bind} E.empty
439
440 end 492 end