This is a nice literate walkthrough. If one wants to know specifically how to implement egg, I apparently hacked up a literate Monte module explaining that in detail. The paper to read is de Moura & Bjørner 2007 which introduces a virtual machine that can efficiently search e-classes.
Very nice, my previous implementation turned out to be incredibly messy, and you seem to have put some thought into making it non-messy: I especially like the idea of sealing the batching directly into the API. Super, will reimplement this and let you know how it goes!
Monte is easily transliterable to Python; each object literal needs its own class, and the pattern-matching one-liners have to be expanded into two or three lines of imperative actions. The resulting code will be missing most of the safety checks we built into the language, though.
This is a nice literate walkthrough. If one wants to know specifically how to implement
egg, I apparently hacked up a literate Monte module explaining that in detail. The paper to read is de Moura & Bjørner 2007 which introduces a virtual machine that can efficiently search e-classes.De Moura & Bjorner of Z3 fame?
Very nice, my previous implementation turned out to be incredibly messy, and you seem to have put some thought into making it non-messy: I especially like the idea of sealing the batching directly into the API. Super, will reimplement this and let you know how it goes!
In what language are you implementing this? Would you be open to sharing?
Sure, I’ll probably do it in lean4 and C++ : https://github.com/bollu/lean.egraphs
The repo contains two implementations, one in C++, and the other in Lean :)
Sweet!
Have you poked at this at all? The reimplementation?
Oh very cool!! I wonder if this helps with the built-in matching DSL that I didn’t bother to implement. How close is Monte to Python?
Monte is easily transliterable to Python; each
objectliteral needs its ownclass, and the pattern-matching one-liners have to be expanded into two or three lines of imperative actions. The resulting code will be missing most of the safety checks we built into the language, though.Very cool. Thank you
Sorry, if I wrote compilers I guess I would know, but what is an IR?
Intermediate representation - any compiler internal way to store a program for transformations and analysis