comparison src/mono_reduce.sml @ 1254:935a981f4380

Merge
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 May 2010 13:57:01 -0400
parents 950d1e540df6
children acabf3935060
comparison
equal deleted inserted replaced
1198:b52929351402 1254:935a981f4380
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
187 (PWild, _) => Yes env 187 (PWild, _) => Yes env
188 | (PVar (x, t), _) => Yes (e :: env) 188 | (PVar (x, t), _) => Yes (e :: env)
189 189
190 | (PPrim (Prim.String s), EStrcat ((EPrim (Prim.String s'), _), _)) => 190 | (PPrim (Prim.String s), EStrcat ((EPrim (Prim.String s'), _), _)) =>
191 if String.isPrefix s' s then 191 if String.isPrefix s' s then
192 Maybe
193 else
194 No
195
196 | (PPrim (Prim.String s), EStrcat (_, (EPrim (Prim.String s'), _))) =>
197 if String.isSuffix s' s then
192 Maybe 198 Maybe
193 else 199 else
194 No 200 No
195 201
196 | (PPrim p, EPrim p') => 202 | (PPrim p, EPrim p') =>
249 255
250 datatype event = 256 datatype event =
251 WritePage 257 WritePage
252 | ReadDb 258 | ReadDb
253 | WriteDb 259 | WriteDb
260 | ReadCookie
261 | WriteCookie
254 | UseRel 262 | UseRel
255 | Unsure 263 | Unsure
264 | Abort
256 265
257 fun p_event e = 266 fun p_event e =
258 let 267 let
259 open Print.PD 268 open Print.PD
260 in 269 in
261 case e of 270 case e of
262 WritePage => string "WritePage" 271 WritePage => string "WritePage"
263 | ReadDb => string "ReadDb" 272 | ReadDb => string "ReadDb"
264 | WriteDb => string "WriteDb" 273 | WriteDb => string "WriteDb"
274 | ReadCookie => string "ReadCookie"
275 | WriteCookie => string "WriteCookie"
265 | UseRel => string "UseRel" 276 | UseRel => string "UseRel"
266 | Unsure => string "Unsure" 277 | Unsure => string "Unsure"
278 | Abort => string "Abort"
267 end 279 end
268 280
269 val p_events = Print.p_list p_event 281 val p_events = Print.p_list p_event
270 282
271 fun patBinds (p, _) = 283 fun patBinds (p, _) =
369 | ECon (_, _, NONE) => [] 381 | ECon (_, _, NONE) => []
370 | ECon (_, _, SOME e) => summarize d e 382 | ECon (_, _, SOME e) => summarize d e
371 | ENone _ => [] 383 | ENone _ => []
372 | ESome (_, e) => summarize d e 384 | ESome (_, e) => summarize d e
373 | EFfi _ => [] 385 | EFfi _ => []
386 | EFfiApp ("Basis", "get_cookie", [e]) =>
387 summarize d e @ [ReadCookie]
374 | EFfiApp (m, x, es) => 388 | EFfiApp (m, x, es) =>
375 if Settings.isEffectful (m, x) orelse Settings.isBenignEffectful (m, x) then 389 if Settings.isEffectful (m, x) orelse Settings.isBenignEffectful (m, x) then
376 List.concat (map (summarize d) es) @ [Unsure] 390 List.concat (map (summarize d) es) @ [Unsure]
377 else 391 else
378 List.concat (map (summarize d) es) 392 List.concat (map (summarize d) es)
415 | EBinop (_, e1, e2) => summarize d e1 @ summarize d e2 429 | EBinop (_, e1, e2) => summarize d e1 @ summarize d e2
416 430
417 | ERecord xets => List.concat (map (summarize d o #2) xets) 431 | ERecord xets => List.concat (map (summarize d o #2) xets)
418 | EField (e, _) => summarize d e 432 | EField (e, _) => summarize d e
419 433
420 | ECase (e, pes, _) => summarize d e @ [Unsure] 434 | ECase (e, pes, _) =>
421 (*let 435 let
422 val lss = map (fn (p, e) => summarize (d + patBinds p) e) pes 436 val lss = map (fn (p, e) => summarize (d + patBinds p) e) pes
423 in 437 in
424 case lss of 438 case lss of
425 [] => raise Fail "Empty pattern match" 439 [] => raise Fail "Empty pattern match"
426 | ls :: lss => 440 | ls :: lss =>
427 if List.all (fn ls' => ls' = ls) lss then 441 summarize d e
428 summarize d e @ ls 442 @ (if List.all (fn ls' => ls' = ls) lss then
429 else 443 ls
430 [Unsure] 444 else if length (List.filter (not o List.null) (ls :: lss)) <= 1 then
431 end*) 445 valOf (List.find (not o List.null) (ls :: lss))
446 else
447 [Unsure])
448 end
432 | EStrcat (e1, e2) => summarize d e1 @ summarize d e2 449 | EStrcat (e1, e2) => summarize d e1 @ summarize d e2
433 450
434 | EError (e, _) => summarize d e @ [Unsure] 451 | EError (e, _) => summarize d e @ [Abort]
435 | 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]
436 | ERedirect (e, _) => summarize d e @ [Unsure] 453 | ERedirect (e, _) => summarize d e @ [Abort]
437 454
438 | EWrite e => summarize d e @ [WritePage] 455 | EWrite e => summarize d e @ [WritePage]
439 456
440 | ESeq (e1, e2) => summarize d e1 @ summarize d e2 457 | ESeq (e1, e2) => summarize d e1 @ summarize d e2
441 | ELet (_, _, e1, e2) => summarize d e1 @ summarize (d + 1) e2 458 | ELet (_, _, e1, e2) => summarize d e1 @ summarize (d + 1) e2
515 532
516 fun does eff = List.exists (fn eff' => eff' = eff) effs_e' 533 fun does eff = List.exists (fn eff' => eff' = eff) effs_e'
517 val writesPage = does WritePage 534 val writesPage = does WritePage
518 val readsDb = does ReadDb 535 val readsDb = does ReadDb
519 val writesDb = does WriteDb 536 val writesDb = does WriteDb
537 val readsCookie = does ReadCookie
538 val writesCookie = does ReadCookie
520 539
521 fun verifyUnused eff = 540 fun verifyUnused eff =
522 case eff of 541 case eff of
523 UseRel => false 542 UseRel => false
524 | _ => true 543 | _ => true
531 Unsure => false 550 Unsure => false
532 | UseRel => List.all verifyUnused effs 551 | UseRel => List.all verifyUnused effs
533 | WritePage => not writesPage andalso verifyCompatible effs 552 | WritePage => not writesPage andalso verifyCompatible effs
534 | ReadDb => not writesDb andalso verifyCompatible effs 553 | ReadDb => not writesDb andalso verifyCompatible effs
535 | 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
536 in 559 in
537 (*Print.prefaces "verifyCompatible" 560 (*Print.prefaces "verifyCompatible"
538 [("e'", MonoPrint.p_exp env e'), 561 [("e'", MonoPrint.p_exp env e'),
539 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b), 562 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b),
540 ("effs_e'", Print.p_list p_event effs_e'), 563 ("effs_e'", Print.p_list p_event effs_e'),