comparison src/mono_reduce.sml @ 1225:950d1e540df6

Tweaks to table signatures and MonoOpt summarizing
author Adam Chlipala <adamc@hcoop.net>
date Sun, 11 Apr 2010 14:11:17 -0400
parents 648e6b087dfb
children acabf3935060
comparison
equal deleted inserted replaced
1224:3950cf1f5736 1225:950d1e540df6
75 EWrite _ => true 75 EWrite _ => true
76 | EQuery _ => true 76 | EQuery _ => true
77 | EDml _ => true 77 | EDml _ => true
78 | ENextval _ => true 78 | ENextval _ => true
79 | ESetval _ => true 79 | ESetval _ => true
80 | EUnurlify _ => true 80 | EUnurlify _ => false
81 | EAbs _ => false 81 | EAbs _ => false
82 82
83 | EPrim _ => false 83 | EPrim _ => false
84 | ERel _ => false 84 | ERel _ => false
85 | ENamed _ => false 85 | ENamed _ => false
255 255
256 datatype event = 256 datatype event =
257 WritePage 257 WritePage
258 | ReadDb 258 | ReadDb
259 | WriteDb 259 | WriteDb
260 | ReadCookie
261 | WriteCookie
260 | UseRel 262 | UseRel
261 | Unsure 263 | Unsure
264 | Abort
262 265
263 fun p_event e = 266 fun p_event e =
264 let 267 let
265 open Print.PD 268 open Print.PD
266 in 269 in
267 case e of 270 case e of
268 WritePage => string "WritePage" 271 WritePage => string "WritePage"
269 | ReadDb => string "ReadDb" 272 | ReadDb => string "ReadDb"
270 | WriteDb => string "WriteDb" 273 | WriteDb => string "WriteDb"
274 | ReadCookie => string "ReadCookie"
275 | WriteCookie => string "WriteCookie"
271 | UseRel => string "UseRel" 276 | UseRel => string "UseRel"
272 | Unsure => string "Unsure" 277 | Unsure => string "Unsure"
278 | Abort => string "Abort"
273 end 279 end
274 280
275 val p_events = Print.p_list p_event 281 val p_events = Print.p_list p_event
276 282
277 fun patBinds (p, _) = 283 fun patBinds (p, _) =
375 | ECon (_, _, NONE) => [] 381 | ECon (_, _, NONE) => []
376 | ECon (_, _, SOME e) => summarize d e 382 | ECon (_, _, SOME e) => summarize d e
377 | ENone _ => [] 383 | ENone _ => []
378 | ESome (_, e) => summarize d e 384 | ESome (_, e) => summarize d e
379 | EFfi _ => [] 385 | EFfi _ => []
386 | EFfiApp ("Basis", "get_cookie", [e]) =>
387 summarize d e @ [ReadCookie]
380 | EFfiApp (m, x, es) => 388 | EFfiApp (m, x, es) =>
381 if Settings.isEffectful (m, x) orelse Settings.isBenignEffectful (m, x) then 389 if Settings.isEffectful (m, x) orelse Settings.isBenignEffectful (m, x) then
382 List.concat (map (summarize d) es) @ [Unsure] 390 List.concat (map (summarize d) es) @ [Unsure]
383 else 391 else
384 List.concat (map (summarize d) es) 392 List.concat (map (summarize d) es)
438 else 446 else
439 [Unsure]) 447 [Unsure])
440 end 448 end
441 | EStrcat (e1, e2) => summarize d e1 @ summarize d e2 449 | EStrcat (e1, e2) => summarize d e1 @ summarize d e2
442 450
443 | EError (e, _) => summarize d e @ [Unsure] 451 | EError (e, _) => summarize d e @ [Abort]
444 | EReturnBlob {blob = e1, mimeType = e2, ...} => summarize d e1 @ summarize d e2 @ [Unsure] 452 | EReturnBlob {blob = e1, mimeType = e2, ...} => summarize d e1 @ summarize d e2 @ [Abort]
445 | ERedirect (e, _) => summarize d e @ [Unsure] 453 | ERedirect (e, _) => summarize d e @ [Abort]
446 454
447 | EWrite e => summarize d e @ [WritePage] 455 | EWrite e => summarize d e @ [WritePage]
448 456
449 | ESeq (e1, e2) => summarize d e1 @ summarize d e2 457 | ESeq (e1, e2) => summarize d e1 @ summarize d e2
450 | ELet (_, _, e1, e2) => summarize d e1 @ summarize (d + 1) e2 458 | ELet (_, _, e1, e2) => summarize d e1 @ summarize (d + 1) e2
524 532
525 fun does eff = List.exists (fn eff' => eff' = eff) effs_e' 533 fun does eff = List.exists (fn eff' => eff' = eff) effs_e'
526 val writesPage = does WritePage 534 val writesPage = does WritePage
527 val readsDb = does ReadDb 535 val readsDb = does ReadDb
528 val writesDb = does WriteDb 536 val writesDb = does WriteDb
537 val readsCookie = does ReadCookie
538 val writesCookie = does ReadCookie
529 539
530 fun verifyUnused eff = 540 fun verifyUnused eff =
531 case eff of 541 case eff of
532 UseRel => false 542 UseRel => false
533 | _ => true 543 | _ => true
540 Unsure => false 550 Unsure => false
541 | UseRel => List.all verifyUnused effs 551 | UseRel => List.all verifyUnused effs
542 | WritePage => not writesPage andalso verifyCompatible effs 552 | WritePage => not writesPage andalso verifyCompatible effs
543 | ReadDb => not writesDb andalso verifyCompatible effs 553 | ReadDb => not writesDb andalso verifyCompatible effs
544 | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs 554 | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs
555 | ReadCookie => not writesCookie andalso verifyCompatible effs
556 | WriteCookie => not writesCookie andalso not readsCookie
557 andalso verifyCompatible effs
558 | Abort => true
545 in 559 in
546 (*Print.prefaces "verifyCompatible" 560 (*Print.prefaces "verifyCompatible"
547 [("e'", MonoPrint.p_exp env e'), 561 [("e'", MonoPrint.p_exp env e'),
548 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b), 562 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b),
549 ("effs_e'", Print.p_list p_event effs_e'), 563 ("effs_e'", Print.p_list p_event effs_e'),