TmOracle: Replace negative term equalities by refutable PmAltCons

Closed Sebastian Graf requested to merge wip/pmcheck-refuts into master

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.

Edited by Sebastian Graf

Merge request reports