TmOracle: Replace negative term equalities by refutable PmAltCons

Authored by sgraf on May 22 2019, 11:46 AM.

Description

TmOracle: Replace negative term equalities by refutable PmAltCons

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.

Metric Decrease:

T11195

Details

Committed
Marge Bot <ben+marge-bot@smart-cactus.org>Jun 7 2019, 9:21 AM
Parents
rGHCd3915b304f29: [skip ci] Improve the documentation of the CNF primops. In this context, the…
Branches
Unknown
Tags
Unknown