egraphs-good / egglog

egraphs + datalog!
https://egraphs-good.github.io/egglog/
MIT License
459 stars 54 forks source link

Disallow unused variables #408

Open oflatt opened 3 months ago

oflatt commented 3 months ago

If you write a rule with an unused pattern variable, we should throw an error:

(rule ((Add a b))
         ((Neg b)))

If you want to ignore something, use an underscore

(rule ((Add _a b))
        ((Neg b)))
yihozhang commented 3 months ago

Will this be too radical? Will a warning / opt-in feature be more appropriate? For instance, in eggcc, we have templates for generating query atoms like (= e (Add e1 e2)) and now all of a sudden we need to condition on whether e,e1,e2 are used in the body, which is a burden to users.

yihozhang commented 1 month ago

Actually, reopening this issue since this can be part of a (set-option strict) similar to #325