TmOracle: Replace negative term equalities by refutable PmAltCons
This is the change I was alluding to in !994 (comment 199787). Is this enough commentary? Does this need a Note?
In preparation for the PmNCons idea from !963 (closed), I introduced the PmAltConLike constructor which is kind-of dead right now. Note that the old model allowed for much more complicated negative constraints that we never used, so I hope this is OK for the time being. I'll refactor if you disagree.
Here's the commit message:
The PmExprEq business was a huge hack and was at the same time vastly
too powerful and not powerful enough to encode negative term equalities,
i.e. facts of the form "forall y. x ≁ Just y".
This patch introduces the concept of 'refutable shapes': What matters
for the pattern match checker is being able to encode knowledge of the
kind "x can no longer be the literal 5". We encode this knowledge in a
PmRefutEnv, mapping a set of newly introduced PmAltCons (which are
just PmLits at the moment) to each variable denoting above
inequalities.
So, say we have x ≁ 42 ∈ refuts in the term oracle context and
try to solve an equality like x ~ 42. The entry in the refutable
environment will immediately lead to a contradiction.
This machinery renders the whole PmExprEq and ComplexEq business
unnecessary, getting rid of a lot of (mostly dead) code.
See the Note [Refutable shapes] in TmOracle for a place to start.