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