• Sebastian Graf's avatar
    TmOracle: Replace negative term equalities by refutable PmAltCons · e963beb5
    Sebastian Graf authored
    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 `PmAltCon`s (which are
    just `PmLit`s 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
    e963beb5
TmOracle.hs 14.4 KB