Unable to reason over ADT

[adrianleh]

Hi,

I'm using the ale/3.0 branch, and I am trying to reason over an ADT implemented with abstract types (code below)

using Metatheory
using Metatheory.TermInterface

# Define the Dim data type
abstract type Dim end


struct Lit <: Dim
    value::Int64
end


# Define constructors for Dim
struct Plus{T<:Dim, U<:Dim} <: Dim
    dim1::T
    dim2::U
end

@rule Plus(Lit(0), ~dim1) --> ~dim1;

It fails with the following error:

ERROR: LoadError: MethodError: no method matching match_term_op(::Metatheory.Patterns.PatExpr, ::Symbol, ::Type{Main.dcac.Plus})
The function `match_term_op` exists, but no method is defined for this combination of argument types.

Closest candidates are:
  match_term_op(::Metatheory.Patterns.AbstractPat, ::Any, ::Metatheory.Patterns.PatVar)
   @ Metatheory ~/.julia/packages/Metatheory/HvfSQ/src/match_compiler.jl:215
  match_term_op(::Any, ::Any, ::Union{Expr, Symbol})
   @ Metatheory ~/.julia/packages/Metatheory/HvfSQ/src/match_compiler.jl:212
  match_term_op(::Any, ::Any, ::Union{DataType, Function})
   @ Metatheory ~/.julia/packages/Metatheory/HvfSQ/src/match_compiler.jl:207

Stacktrace:
 [1] match_term_expr(pattern::Metatheory.Patterns.PatExpr, coordinate::Vector{Int64}, segments_so_far::Vector{Symbol})
   @ Metatheory ~/.julia/packages/Metatheory/HvfSQ/src/match_compiler.jl:224
 [2] match_compile!(pattern::Metatheory.Patterns.PatExpr, state::Metatheory.MatchCompilerState, coordinate::Vector{Int64}, parent_segments::Vector{Symbol})
   @ Metatheory ~/.julia/packages/Metatheory/HvfSQ/src/match_compiler.jl:144
 [3] match_compile(p::Metatheory.Patterns.PatExpr, pvars::Vector{Symbol})
   @ Metatheory ~/.julia/packages/Metatheory/HvfSQ/src/match_compiler.jl:34
 [4] var"@rule"(__source__::LineNumberNode, __module__::Module, args::Vararg{Any})
   @ Metatheory.Syntax ~/.julia/packages/Metatheory/HvfSQ/src/Syntax.jl:428
 [5] include(fname::String)
   @ Main ./sysimg.jl:38
 [6] top-level scope
   @ REPL[3]:1

Is there a workaround for this, or is this a metatheory.jl issue?

[adrianleh]

Might be related to #209

[0x0f0f0f]

Ah, I see, the method for ::Union{DataType, Function} may not cover ::Type{Main.dcac.Plus}

[0x0f0f0f]

Ah, I see, the method for ::Union{DataType, Function} may not cover ::Type{Main.dcac.Plus}

julia> Plus isa DataType
false

[adrianleh]

How could it be covered?

[0x0f0f0f]

Did you make the types matchable by satisfying TermInterface?

[0x0f0f0f]

Nvm, verified. I just pushed a bugfix. You should use TermInterface.jl if you define custom AST types. See test/tutorials/custom_types.jl

[0x0f0f0f]

Let me know if it works for your use case :)

[adrianleh]

Thanks for the pointer and the fix! This is super helpful

I was able to get it at least running, but it doesn't seem to simplify my expressions. Also, the metadata does not seem to work for my leaf nodes (Lit) and I have to stick it into the children, which I think might be related. I put my updated code below!

module dcac
using Metatheory, Metatheory.TermInterface, Metatheory.EGraphs
# Define the Dim data type
abstract type Dim end


struct Lit <: Dim
    value::Int64
end

TermInterface.isexpr(::Dim) = true
TermInterface.children(l::Lit) = [l.value]
TermInterface.metadata(l::Lit) = l.value # This doesn't seem to work
TermInterface.head(l::Lit) = "lit"

# Define constructors for Dim
struct Plus{T<:Dim,U<:Dim} <: Dim
    dim1::T
    dim2::U
end

TermInterface.children(p::Plus) = [p.dim1, p.dim2]
TermInterface.head(::Plus) = "plus"

TermInterface.maketerm(::Type{Dim}, h, c, metadata) = 
    if h == "plus"
        return Plus(c[1], c[2])
    elseif h == "lit"
        return Lit(c[1])
    end
    return false


t = @theory dim1 a b begin
    Plus(Lit(0), ~dim1) --> ~dim1
end


ex = Plus(Lit(0), Lit(0))
g= EGraph{Dim}(ex)

saturate!(g,t)
print(extract!(g,astsize))




end

[0x0f0f0f]

Metadata is not yet agreed on on 3.0 and on e-graphs. It works on classical rewriting though. The issue is that the fix I've pushed only works on Julia 1.10 - it seems to not work on 1.8 or 1.11 which are the versions used by CI

[adrianleh]

sorry, I missed your reply on this. Is there an inherent reason for it not working on 1.11?

[adrianleh]

And even with the workaround, the simplification is not working

[0x0f0f0f]

sorry, I missed your reply on this. Is there an inherent reason for it not working on 1.11?

If you pull latest 3.0 branch the original example you sent at the beginning now works. The bug is fixed. The testcase was not working because the struct definition was inside a @testset block, and it triggered some scope problems with @rule, which is a separate issue. It works on 1.11 perfectly.

I still have to take a look at your second problem. I recommend to use the @matchable macro that automatically defines TermInterface, also a Lit should not be a tree (isexpr should be false), because it's a literal, so no need to overload any TermInterface method. For Plus, head can just be Plus, but you should also define TermInterface.iscall to be true

[adrianleh]

Sorry, the isexpr was a copy-paste issue. Nevertheless, even with those changes the simplification doesn't trigger. Also, where is @matchable documented; I couldn't find it in the docs of metatheory or terminterface