I believe the Sym.hs test has some weird corners. Not sure if the test has to be fixed, it seems to test everything it should. Maybe a comment for folks who are looking for examples is fine?
The Maybe Double E-Analysis is basically a coarse grained set. Either it represents all Double's or a singleton set of a specific Double.
The join should be set-intersection, but then we should have joinA Nothing x = x and joinA x Nothing = x.
The current implementation is not unsound, but it loses a lot of accuracy and results depend on the ordering of rules and merges.
Secondly, some rules have the conditional
is_not_zero :: Pattern Expr -> RewriteCondition (Maybe Double) Expr
is_not_zero v subst egr =
egr^._class (unsafeGetSubst v subst)._data /= Just 0
This is very dangerous because Nothing stands for all Doubles. With a fixed joinA, Nothingcan be refined to Just 0 later. Fixing the condition to not fire on Nothing makes the test-suite fail, though. In datalogs with lattices this is sometimes solved with stratification, so the stratified rules run only after all rules that could refine the e-analysis finished. But because congruence and e-analysis always run this doesn't seem feasible, so is_not_zero should only fire if the e-class has a known distinct value. Optionally the lattice could be enriched with a specific non-zero case.
I believe the Sym.hs test has some weird corners. Not sure if the test has to be fixed, it seems to test everything it should. Maybe a comment for folks who are looking for examples is fine?
The
Maybe DoubleE-Analysis is basically a coarse grained set. Either it represents all Double's or a singleton set of a specific Double.The join should be set-intersection, but then we should have
joinA Nothing x = xandjoinA x Nothing = x. The current implementation is not unsound, but it loses a lot of accuracy and results depend on the ordering of rules and merges.Secondly, some rules have the conditional
This is very dangerous because
Nothingstands for all Doubles. With a fixed joinA,Nothingcan be refined toJust 0later. Fixing the condition to not fire on Nothing makes the test-suite fail, though. In datalogs with lattices this is sometimes solved with stratification, so the stratified rules run only after all rules that could refine the e-analysis finished. But because congruence and e-analysis always run this doesn't seem feasible, so is_not_zero should only fire if the e-class has a known distinct value. Optionally the lattice could be enriched with a specific non-zero case.