Issue with birewrite

[RafaeNoor]

Hello,
I'm experimenting with egglog and I've run into an issue which I'm not sure if it's a bug or a not-supported behavior. I've narrowed down the failure to a minimal example:

(datatype DATA 
 (INPUT i64)
 (operation DATA DATA)
)


(birewrite 
 (operation
  argument0 
  argument0
 )
 argument0
)

Upon compiling it with cargo run example.egg I get the following issue:

thread 'main' panicked at 'Unbound variable argument0', src/ast/desugar.rs:108:13
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Is the following behavior not supported?

[oflatt]

This is subtle problem that we have right now in egglog.
In fact, the following rule is not valid:
(rewrite argument0 (operation argument0 argument0))

The reason is the unbound variable argument0- right now, all "pattern variables" like argument0 must appear under a constructor like operation, so we can search the database for that constructor.
We could fix this by trying all the outputs of functions in the database, but this raises semantic questions- do we also search functions defined after this rewrite? If so, the rewrite can refer to types that are not defined yet. Also it raises typechecking questions.

Great issue, something we've been thinking about. For now a hack that works is to define a Universe relation and throw everything you care about in there. Then you can match on (Universe argument 0)

[RafaeNoor]

I think I understand somewhat what you're describing, I'm guessing it would also impact the performance of egglog drastically to support something like that? I think the universe relation you described seems like a quick enough work around for my use-case. Hopefully I can change it back if this get's supported later :)

Thanks!

[oflatt]

I don't think performance is a big question for me- mainly I don't know what the rule would mean in particular. We could use this thread to solve that semantic problem if anyone has ideas. Thanks for bringing up the issue!