Alessandro Cheli

For proofs https://www.cs.upc.edu/~oliveras/espai/papers/rta05.pdf

For the ematch thing, I have a branch https://github.com/0x0f0f0f/Metatheory.jl/tree/staged_ematch where I implement @philzook58 staged ematcher http://www.philipzucker.com/staging-patterns/

Got some improvements by splitting `ENode` into `ENodeTerm` and `ENodeLiteral`. Got also some improvements by avoiding storing the matched e-nodes if not strictly needed, only storing ids.

good catch! updated parents have to go directly into `repair!` since parents are now stored per-enode and not globally in the egraph! would you suggest me any package for defining...

@dalejordan still interested ?

I got stuck there and never got the cache to work. Have to revisit it completely. It should improve search performance significantly

@MrVPlusOne this is a very stupid optimization that I didn't consider. If the pattern to be searched is a literal, we just know where it is due to the egraph...

```julia function cached_ids(g::EGraph, p::Pattern)# ::Vector{Int64} collect(keys(g.classes)) end function cached_ids(g::EGraph, p) # p is a literal [lookup(g, ENodeLiteral(p))] end ```

Same happens if the pattern is a ground term (no variables). So it can only reside in a single eclass.

cc @shashi