egraphs-good / eggcc

MIT License
51 stars 11 forks source link

[Tree Optimizer] Unnecessary Let deletion #247

Open oflatt opened 10 months ago

oflatt commented 10 months ago

An important optimization to enable other optimizations is to get rid of unnecessary lets. In the case of pure computations, let bindings are not necessary and they should be removed- maybe destructively?

For impure computations that are used just once, the let binding is not necessary. However, we must be careful to avoid bugs since later the e-class could have representatives that use it twice.

yihozhang commented 10 months ago

Let bindings save duplicate evaluations even for pure computations, e.g.

let x = sum(1, 10000) in
x+x

vs

sum(1, 10000) + sum(1, 10000) 

so we need to be careful here.

oflatt commented 10 months ago

Yeah, that's a great point. What if we used DAG-based extraction, even for trees? It could count things multiple times when they are impure

yihozhang commented 9 months ago

Related to gamma/switch pull in