• Sebastian Graf's avatar
    Encode shape information in `PmOracle` · 7915afc6
    Sebastian Graf authored
    Previously, we had an elaborate mechanism for selecting the warnings to
    generate in the presence of different `COMPLETE` matching groups that,
    albeit finely-tuned, produced wrong results from an end user's
    perspective in some cases (#13363).
    
    The underlying issue is that at the point where the `ConVar` case has to
    commit to a particular `COMPLETE` group, there's not enough information
    to do so and the status quo was to just enumerate all possible complete
    sets nondeterministically.  The `getResult` function would then pick the
    outcome according to metrics defined in accordance to the user's guide.
    But crucially, it lacked knowledge about the order in which affected
    clauses appear, leading to the surprising behavior in #13363.
    
    In !1010 we taught the term oracle to reason about literal values a
    variable can certainly not take on. This MR extends that idea to
    `ConLike`s and thereby fixes #13363: Instead of committing to a
    particular `COMPLETE` group in the `ConVar` case, we now split off the
    matching constructor incrementally and record the newly covered case as
    a refutable shape in the oracle. Whenever the set of refutable shapes
    covers any `COMPLETE` set, the oracle recognises vacuosity of the
    uncovered set.
    
    This patch goes a step further: Since at this point the information
    in value abstractions is merely a cut down representation of what the
    oracle knows, value abstractions degenerate to a single `Id`, the
    semantics of which is determined by the oracle state `Delta`.
    Value vectors become lists of `[Id]` given meaning to by a single
    `Delta`, value set abstractions (of which the uncovered set is an
    instance) correspond to a union of `Delta`s which instantiate the
    same `[Id]` (akin to models of formula).
    
    Fixes #11528 #13021, #13363, #13965, #14059, #14253, #14851, #15753, #17096, #17149
    
    -------------------------
    Metric Decrease:
        ManyAlternatives
        T11195
    -------------------------
    7915afc6
Code owners : Ben Gamari
PatSyn.hs 16.6 KB