Hi, thank you kindly!

I've given it some thought -- I don't think it is easy to get an exact trace of the rules applied to get an exact trace!

Equality saturation works by representing a term (and necessarily all its sub-terms) in an e-graph and then applying rewrite rules over and over. These will match the terms represented in certain e-classes, and add the rewritten version in the same e-class.

I imagine it might be possible by tracking the origin of each term (e.g. if add was called by eqsat for rule X, or if it was called by the eqsat init, or by recursing inside a larger term?...), and then when extracting (choosing the best term out of each class that the main term depends on) compose this information into a useful trace.

I think there might be a compromise that avoids a pervasive change like that:

It'd be cool if you could elaborate on your use case and possibly provide examples for what you'd like to see happening.

One idea from your mention of debugging bogus rules:
What if we tracked all the rules that fired and printed them out, deduplicated, at the end of equalitySaturationWithTrace? Or just print them out as they fire (for posterior analysis with e.g. grep 😛)?

Though I can see the benefit of a more involved tracing system! We can discuss it further :-)

For example, I had the expression log ( x * (x / x) ) - x that entered an infinite loop because of the rules negate x := 0 - x and 0 - x := negate x. But since I have so many rules, it took me some time to find the culprit. (I'm taking notes of my experiments and going to write some minimal code to reproduce them).

I think printing them out could already help a lot (or enveloping the function with a Writer monad). But, like I said, I'm still studying the code so that I can do some actual contribution 😄

I see! Which means that if all the rules that fire were to be printed out, eventually you'd see the loop printed out.

Let me know of any questions regarding the implementation. I can help you understand the code.

On approaching this: I think we can either have a compile time flag -fdebug or a module Data.Equality.Saturation.Debug in the spirit of Debug.Trace with duplicated code from Data.Equality.Saturation that calls trace here and there.

I think it's a good idea to add something like this!

Perfect! I'll try to implement that (but no promises I can do it quickly 😆 )

You'll want to look around here:

Possibly adding a Debug.Trace.trace there already goes a long way! It would mean that for each match on the e-graph you'd get the rewrite rule printed out.

I can suggest you add your fork of hegg to your cabal.project as follows, and commit this trace change (you might require some additional Show constraints too) and try it out on your use case.

Create a cabal.project file in your project root and add the following incantation:

source-repository-package
     type: git
     location: https://github.com/alt-romes/hegg.git
     tag: the-sha-of-your-commit-with-the-trace

It should override the hackage package and use your fork of hegg with the change.

Let me know how it goes, if the output is useful enough, etc...

Thanks!

Just to let you know, the debug.trace helped a lot to generate a minimal number of rules that leads to some issues. I found a minimal example that seems to create an infinite loop in the current code, but haven't figured it out how and why. I'll create another issue with this code.

Glad to know, then Equality.Saturation.Debug sounds like a good idea.

I'll take a look at the loop asap.

Thanks for your help!