JuliaSymbolics / Metatheory.jl

Makes Julia reason with equations. General purpose metaprogramming, symbolic computation and algebraic equational reasoning library for the Julia programming language: E-Graphs & equality saturation, term rewriting and more.
https://juliasymbolics.github.io/Metatheory.jl/dev/
MIT License
362 stars 47 forks source link

`@areequal` not working with matching multiple sub-expressions (`xs...`) #141

Closed adomasbaliuka closed 2 years ago

adomasbaliuka commented 2 years ago

Working with matching single sub-expressions,

julia> r = @rule *(~y, 3)^~x => :($y^$x * 3^$x);

julia> r(:((7* 3)^4))
:(7 ^ 4 * 3 ^ 4)

julia> @areequal [r] (7 ^ 4 * 3 ^ 4) (7* 3)^4
true

so far so good.

But macro call crashes when matching multiple sub-expressions:

julia> r3 = @rule *(~ys...)^~x => :((*)($(map(y-> :($y^$x), ys)...)));  # from docs

julia> r3(:((w*w*α*β)^2))   # from docs
:(w ^ 2 * w ^ 2 * α ^ 2 * β ^ 2)

julia> @areequal [r3] (w*w*α*β)^2  (w ^ 2 * w ^ 2 * α ^ 2 * β ^ 2)
ERROR: MethodError: no method matching (::Metatheory.EGraphs.Machine)(::Fail, ::Int64)
Closest candidates are:
  (::Metatheory.EGraphs.Machine)(::Bind, ::Any) at ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/ematch.jl:211
  (::Metatheory.EGraphs.Machine)(::Lookup, ::Any) at ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/ematch.jl:200
  (::Metatheory.EGraphs.Machine)(::Filter, ::Any) at ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/ematch.jl:162
  ...
Stacktrace:
  [1] (::Metatheory.EGraphs.Machine)()
    @ Metatheory.EGraphs ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/ematch.jl:92
  [2] #38
    @ ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/ematch.jl:267 [inlined]
  [3] lock(f::Metatheory.EGraphs.var"#38#39"{EGraph, Program, Int64, Metatheory.EGraphs.Machine}, l::ReentrantLock)
    @ Base ./lock.jl:185
  [4] ematch
    @ ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/ematch.jl:265 [inlined]
  [5] (::DynamicRule)(g::EGraph, id::Int64)
    @ Metatheory.EGraphs ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/saturation.jl:144
  [6] #60
    @ ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/saturation.jl:196 [inlined]
  [7] iterate
    @ ./generator.jl:47 [inlined]
  [8] _collect(c::Vector{Int64}, itr::Base.Generator{Vector{Int64}, Metatheory.EGraphs.var"#60#64"{EGraph, DynamicRule}}, #unused#::Base.EltypeUnknown, isz::Base.HasShape{1})
    @ Base ./array.jl:807
  [9] collect_similar(cont::Vector{Int64}, itr::Base.Generator{Vector{Int64}, Metatheory.EGraphs.var"#60#64"{EGraph, DynamicRule}})
    @ Base ./array.jl:716
 [10] map(f::Function, A::Vector{Int64})
    @ Base ./abstractarray.jl:2933
 [11] (::Metatheory.EGraphs.var"#pmap#61"{Bool})(f::Function, xs::Vector{Int64})
    @ Metatheory.EGraphs ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/saturation.jl:168
 [12] macro expansion
    @ ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/saturation.jl:196 [inlined]
 [13] macro expansion
    @ ~/.julia/packages/TimerOutputs/4yHI4/src/TimerOutput.jl:237 [inlined]
 [14] eqsat_search!(egraph::EGraph, theory::Vector{DynamicRule}, scheduler::Metatheory.EGraphs.Schedulers.BackoffScheduler, report::Metatheory.EGraphs.Report; threaded::Bool)
    @ Metatheory.EGraphs ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/saturation.jl:189
 [15] macro expansion
    @ ~/.julia/packages/TimerOutputs/4yHI4/src/TimerOutput.jl:237 [inlined]
 [16] eqsat_step!(g::EGraph, theory::Vector{DynamicRule}, curr_iter::Int64, scheduler::Metatheory.EGraphs.Schedulers.BackoffScheduler, match_hist::Vector{Metatheory.EGraphs.Match}, params::SaturationParams, report::Metatheory.EGraphs.Report)
    @ Metatheory.EGraphs ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/saturation.jl:299
 [17] saturate!(g::EGraph, theory::Vector{DynamicRule}, params::SaturationParams)
    @ Metatheory.EGraphs ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/saturation.jl:338
 [18] areequal(::EGraph, ::Vector{DynamicRule}, ::Expr, ::Vararg{Expr}; params::SaturationParams)
    @ Metatheory.EGraphs ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/saturation.jl:402
 [19] #areequal#70
    @ ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/saturation.jl:376 [inlined]
 [20] areequal(::Vector{DynamicRule}, ::Expr, ::Expr)
    @ Metatheory.EGraphs ~/.julia/packages/Metatheory/wqlT2/src/EGraphs/saturation.jl:374
 [21] top-level scope
    @ REPL[162]:1

Why is this so? If I'm missing something, maybe the error message can be improved?

0x0f0f0f commented 2 years ago

E-Graph pattern matching does not support splatting ys... - duplicate issue #3

Yes - the error message could be improved