Rewrite rules cannot introduce variables (I think)

[ViciousDoormat]

Hi,

Given for example these theories:

t = @theory a begin
  true --> a ≥ a
end
saturate!(EGraph(:(a)), t)

f = @theory a begin
  0 --> a - a
end
saturate!(EGraph(:(0)), f)

Note that the rewrite rules are sound and complete.
When I saturate, I get the exception:

ERROR: UndefVarError: `σ-1` not defined in `Main`
Suggestion: check for spelling errors or missing imports.

I am using the ale/3.0 branch.
I assume that this happens because I introduce variables in these rewrite rules.
The error seems to arise at

var"##ematcher#1123"(g::EGraph{…}, rule_idx::Int64, root_id::UInt64, stack::OptBuffer{…}, ematch_buffer::OptBuffer{…})
   @ Main C:\...\.julia\dev\Metatheory\src\ematch_compiler.jl:355

[gkronber]

You defined a as a slot variable in the theories. That means it is a placeholder for any expression. The slot variable must be used on the LHS to be bound to an expression.

This works:

f = @theory a begin
         0 --> :a - :a
       end

g = EGraph(:(0))

saturate!(g, f)

g
EGraph{Int64, Nothing} with 2 e-classes:
  2 => [a]
  3 => [(-)(%2, %2), 0]

Nevertheless, MT should probably check the RHS of rules and produce a more helpful error message.

[ViciousDoormat]

Thanks for your lightning fast response!

[0x0f0f0f]

MT should probably check the RHS of rules and produce a more helpful error message.

Good idea. It was checking this before