alt-romes / alt-romes/hegg

E-Analysis in test/Sym.hs

Đang mở
#35 0 bình luận 1 reaction 0 người được giao Xem trên GitHub
Ngôn ngữ chính
Haskell
Star
98
Fork
17
Chỉ số merge pull request
Không có pull request nào được merge trong 30 ngày

Mô tả

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, `Nothing `can 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.

Hướng dẫn đóng góp

Chưa lập chỉ mục được hướng dẫn đóng góp cho kho mã nguồn này

Đánh giá

Issue này chưa được đánh giá.

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.