comparison src/mono_reduce.sml @ 481:2280193bf298

Better detection of [let] substitution opportunities
author Adam Chlipala <adamc@hcoop.net>
date Sat, 08 Nov 2008 16:47:04 -0500
parents 7cb418e9714f
children 463dad880470
comparison
equal deleted inserted replaced
480:40c737913075 481:2280193bf298
197 197
198 datatype event = 198 datatype event =
199 WritePage 199 WritePage
200 | ReadDb 200 | ReadDb
201 | WriteDb 201 | WriteDb
202 | UseRel of int 202 | UseRel
203 | Unsure 203 | Unsure
204 204
205 fun p_event e = 205 fun p_event e =
206 let 206 let
207 open Print.PD 207 open Print.PD
208 in 208 in
209 case e of 209 case e of
210 WritePage => string "WritePage" 210 WritePage => string "WritePage"
211 | ReadDb => string "ReadDb" 211 | ReadDb => string "ReadDb"
212 | WriteDb => string "WriteDb" 212 | WriteDb => string "WriteDb"
213 | UseRel n => string ("UseRel" ^ Int.toString n) 213 | UseRel => string "UseRel"
214 | Unsure => string "Unsure" 214 | Unsure => string "Unsure"
215 end 215 end
216 216
217 val p_events = Print.p_list p_event 217 val p_events = Print.p_list p_event
218 218
247 IM.empty file 247 IM.empty file
248 248
249 fun summarize d (e, _) = 249 fun summarize d (e, _) =
250 case e of 250 case e of
251 EPrim _ => [] 251 EPrim _ => []
252 | ERel n => if n >= d then [UseRel (n - d)] else [] 252 | ERel n => if n = d then [UseRel] else []
253 | ENamed _ => [] 253 | ENamed _ => []
254 | ECon (_, _, NONE) => [] 254 | ECon (_, _, NONE) => []
255 | ECon (_, _, SOME e) => summarize d e 255 | ECon (_, _, SOME e) => summarize d e
256 | ENone _ => [] 256 | ENone _ => []
257 | ESome (_, e) => summarize d e 257 | ESome (_, e) => summarize d e
273 if length ls < len then 273 if length ls < len then
274 ls 274 ls
275 else 275 else
276 [Unsure] 276 [Unsure]
277 end 277 end
278 | ERel n => List.revAppend (ls, [UseRel (n - d), Unsure]) 278 | ERel n => List.revAppend (ls,
279 if n = d then
280 [UseRel, Unsure]
281 else
282 [Unsure])
279 | EApp (f, x) => 283 | EApp (f, x) =>
280 unravel (#1 f, summarize d x @ ls) 284 unravel (#1 f, summarize d x @ ls)
281 | _ => [Unsure] 285 | _ => [Unsure]
282 in 286 in
283 unravel (e, []) 287 unravel (e, [])
433 val readsDb = does ReadDb 437 val readsDb = does ReadDb
434 val writesDb = does WriteDb 438 val writesDb = does WriteDb
435 439
436 fun verifyUnused eff = 440 fun verifyUnused eff =
437 case eff of 441 case eff of
438 UseRel r => r <> 0 442 UseRel => false
439 | _ => true 443 | _ => true
440 444
441 fun verifyCompatible effs = 445 fun verifyCompatible effs =
442 case effs of 446 case effs of
443 [] => false 447 [] => false
444 | eff :: effs => 448 | eff :: effs =>
445 case eff of 449 case eff of
446 Unsure => false 450 Unsure => false
447 | UseRel r => 451 | UseRel => List.all verifyUnused effs
448 if r = 0 then
449 List.all verifyUnused effs
450 else
451 verifyCompatible effs
452 | WritePage => not writesPage andalso verifyCompatible effs 452 | WritePage => not writesPage andalso verifyCompatible effs
453 | ReadDb => not writesDb andalso verifyCompatible effs 453 | ReadDb => not writesDb andalso verifyCompatible effs
454 | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs 454 | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs
455 in 455 in
456 (*Print.prefaces "verifyCompatible" 456 (*Print.prefaces "verifyCompatible"
457 [("e'", MonoPrint.p_exp env e'), 457 [("e'", MonoPrint.p_exp env e'),
458 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b), 458 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b),
459 ("effs_e'", Print.p_list p_event effs_e'), 459 ("effs_e'", Print.p_list p_event effs_e'),
460 ("effs_b", Print.p_list p_event effs_b)];*) 460 ("effs_b", Print.p_list p_event effs_b)];*)
461 if verifyCompatible effs_b then 461 if List.null effs_e' orelse verifyCompatible effs_b then
462 trySub () 462 trySub ()
463 else 463 else
464 e 464 e
465 end 465 end
466 else 466 else