Issues in E-graph matching for parametrized types

[ChenZhao44]

Here is an example.

using Metatheory， TermInterface

struct Foo{A}
    x::A
end

TermInterface.istree(::Foo{T}) where T = true
TermInterface.istree(::Type{Foo{T}}) where T = true
TermInterface.exprhead(::Foo) = :call
TermInterface.operation(::Foo{T}) where T = :(Foo{$T})
TermInterface.arguments(f::Foo) = f.x

function TermInterface.similarterm(::Type{Foo{T}}, f, args; metadata=nothing, exprhead = :call) where T
    return Foo(args...)
end

t = @theory T A begin
    Foo{T}(A) => A
end

f = Foo([:x])
eg = EGraph(f)
saturate!(eg, t)
extract!(eg, astsize) # this returns Foo([:x]) instead of [:x]

[ChenZhao44]

I guess I have find where the problem comes from.

The operation of :(Foo{T})(A) is :(Foo{T}) which is another Expr. So when you generate a match pattern in makepattern, op will become another match pattern PatTerm because istree(op) is true. See: https://github.com/JuliaSymbolics/Metatheory.jl/blob/c2ce9bd3ec37a47fb5f1b1ea648f84750cca4c3e/src/Syntax.jl#L90

However, it just compare whether the operation of a enode equals to the pattern instead of being matched with the pattern. See: https://github.com/JuliaSymbolics/Metatheory.jl/blob/c2ce9bd3ec37a47fb5f1b1ea648f84750cca4c3e/src/ematch_compiler.jl#L163

So a parameterized type will never be matched because its operation could never equals PatTerm.

[0x0f0f0f]

Thanks for reporting! This feature may be added in 2.0 branch https://github.com/JuliaSymbolics/Metatheory.jl/tree/2.0.0-DEV

[0x0f0f0f]

I believe that with the new pattern matcher we can now attack this easily

[willow-ahrens]

I think this is also related to https://github.com/JuliaSymbolics/Metatheory.jl/issues/87.

You also can't use enums as head types (as is sometimes recommended when developing custom Julia ASTs), since those get quoted too and won't hit the special case in https://github.com/JuliaSymbolics/Metatheory.jl/blob/38719ae889c7857625cee879e9a0ea682873c853/src/matchers.jl#L96 that tries to undo the quoting.

[0x0f0f0f]

I think this is also related to #87.

You also can't use enums as head types (as is sometimes recommended when developing custom Julia ASTs), since those get quoted too and won't hit the special case in

https://github.com/JuliaSymbolics/Metatheory.jl/blob/38719ae889c7857625cee879e9a0ea682873c853/src/matchers.jl#L96 that tries to undo the quoting.

You can try adding a specialized head_matcher pattern matcher function. LMK if you have any further questions.

[olynch]

It seems like the general problem here is that there isn't support for "curried" functions. That is, we'd also have trouble matching f(a)(b), correct? It's the same problem, because the expression looks like Expr(:call, Expr(:curly, :Foo, :T), :A). If there were support for curried functions, then this could be treated as some kind of curried function.