Predicates for pattern variables are not checked consistently

[gkronber]

I was surprised by some inconsistent behaviour of pattern variable predicates (when using the same pattern variable). If a pattern variable occurs twice, it seems that only the predicate for the first occurrance is checked. Here is a minimal example:

using Metatheory

is_nonzero(::EGraph, ::EClass) = false # just for the test

theory1 = @theory a begin
  a / a --> 1
end

theory2 = @theory a begin
  a::is_nonzero / a --> 1
end

theory3 = @theory a begin
  a / a::is_nonzero --> 1
end

theory4 = @theory a begin
  a::is_nonzero / a::is_nonzero --> 1
end

function test(theo)
  g = EGraph(:(x / x))
  saturate!(g, theo)
  extract!(g, astsize)
end

test(theory1) # --> 1 (as expected)
test(theory2) # --> :(x / x) (as expected because the predicate works)
test(theory3) # --> 1 (incorrect! predicate only used for the second variable)
test(theory4) # --> :(x / x) ok

There is also no warning about inconsistent predicates. People might use different predicates for different occurances of pattern variables.

[gkronber]

Related:

MT supports rule predicates for dynamic rules for example:

   ~a * ~b => 0 where (iszero(a) || iszero(b))

where iszero is a function that takes an EClass as argument. This is implemented as syntactic sugar. The rule is simply transformed to

  ~a * ~b => (iszero(a) || iszero(b)) ? 0 : nothing

It would be great to allow the same pattern for directed rewrite rules as well.

   ~a * ~b --> 0 where (iszero(a) || iszero(b))

But that would probably require handling the predicate in the compiled matching function.

[0x0f0f0f]

But that would probably require handling the predicate in the compiled matching function.

Yes indeed

[0x0f0f0f]

@gkronber

This suggests that we probably need a nicer way to attaching predicates to variables. Probably a per-scope dictionary in patterns:

When parsing pattern

  a / a::is_nonzero

The issue is that the predicate is attached only to the second variable, and not to the first one. In order to solve this issue, we need some way of re-walking the pattern after it's parsed and attach the correct predicates to each variables.

When parsing predicate we could use a Dict{Int, Predicate} (Int is OK due to debruijn indexing of variables) where Predicate = Union{Function, DataType} or some struct for performance improvements due to runtime dispatch