merge a document that describes what the unique id invariant is, and how to maintain it when writing rules
implement ShouldBeValid
Our plan is to implement (relation ShouldBeValid (Expr)) (but call it something more sensible). An expr is in ShouldBeValid if it follows Ryan’s id invariants. All extractable e-classes should be in the relation or something has gone wrong.
On the other hand, we break them when we do deep copying.
As a side-effect, we may be able to make rules cleaner by not including (i64-fresh!) in them. We may also get some deep-copy sharing due to shared inputs. (edited)
oflatt
commented
7 months ago
The goal of this issue is to
ShouldBeValidOur plan is to implement (relation ShouldBeValid (Expr)) (but call it something more sensible). An expr is in ShouldBeValid if it follows Ryan’s id invariants. All extractable e-classes should be in the relation or something has gone wrong.
We think this is necessary because:
As a side-effect, we may be able to make rules cleaner by not including (i64-fresh!) in them. We may also get some deep-copy sharing due to shared inputs. (edited)