Skip to content

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
    • Help
    • Support
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project
    • Project
    • Details
    • Activity
    • Releases
    • Cycle Analytics
    • Insights
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Charts
    • Locked Files
  • Issues 3,734
    • Issues 3,734
    • List
    • Boards
    • Labels
    • Milestones
  • Merge Requests 258
    • Merge Requests 258
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Charts
  • Security & Compliance
    • Security & Compliance
    • Dependency List
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Charts
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Merge Requests
  • !2192

Closed
Opened Nov 18, 2019 by Sebastian Graf@sgraf812
  • Report abuse
Report abuse

PmCheck: Formulate as translation between Clause Trees

We used to check GrdVecs arising from multiple clauses and guards in isolation. That resulted in a split between pmCheck and pmCheckGuards, the implementations of which were similar, but subtly different in detail. Also the throttling mechanism described in Note [Countering exponential blowup] ultimately got quite complicated because it had to cater for both checking functions.

This patch realises that pattern match checking doesn't just consider single guarded RHSs, but that it's always a whole set of clauses, each of which can have multiple guarded RHSs in turn. We do so by translating a list of Matches to a GrdTree:

data GrdTree
  = Rhs !RhsInfo
  | Sequence !GrdTree !GrdTree -- captures top-to-bottom match semantics
  | Guard !PmGrd !GrdTree      -- captures lef-to-right  match semantics
  | Empty                      -- For -XEmptyCase, neutral element of Sequence

Then we have a function checkGrdTree that matches a given GrdTree against an incoming set of values, represented by Deltas:

checkGrdTree :: GrdTree -> Deltas -> CheckResult
...

Throttling is isolated to the Sequence case and becomes as easy as one would expect: When the union of uncovered values becomes too big, just return the original incoming Deltas instead (which is always a superset of the union, thus a sound approximation).

The returned CheckResult contains two things:

  1. The set of values that were not covered by any of the clauses, for exhaustivity warnings.
  2. The AnnotatedTree that enriches the syntactic structure of the input program with divergence and inaccessibility information.

This is AnnotatedTree:

data AnnotatedTree
  = AccessibleRhs !RhsInfo
  | InaccessibleRhs !RhsInfo
  | MayDiverge !AnnotatedTree
  | SequenceAnn !AnnotatedTree !AnnotatedTree
  | EmptyAnn

Crucially, MayDiverge asserts that the tree may force diverging values, so not all of its wrapped clauses can be redundant.

While the set of uncovered values can be used to generate the missing equations for warning messages, redundant and proper inaccessible equations can be extracted from AnnotatedTree by redundantAndInaccessibleRhss.

For this to work properly, the interface to the Oracle had to change. There's only addPmCts now, which takes a bag of PmCts. There's a whole bunch of PmCt variants to replace the different oracle functions from before.

The new AnnotatedTree structure allows for more accurate warning reporting (as evidenced by a number of changes spread throughout GHC's code base), thus we fix #17465 (closed).

Fixes #17646 (closed) on the go.

Edited Jan 07, 2020 by Sebastian Graf

Check out, review, and merge locally

Step 1. Fetch and check out the branch for this merge request

git fetch origin
git checkout -b "wip/pmcheck-clausetree" "origin/wip/pmcheck-clausetree"

Step 2. Review the changes locally

Step 3. Merge the branch and fix any conflicts that come up

git fetch origin
git checkout "origin/master"
git merge --no-ff "wip/pmcheck-clausetree"

Step 4. Push the result of the merge to GitLab

git push origin "master"

Note that pushing to GitLab requires write access to this repository.

Tip: You can also checkout merge requests locally by following these guidelines.

  • Discussion 91
  • Commits 2
  • Pipelines 30
  • Changes 38
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
1
Labels
pattern match warnings
Assign labels
  • View project labels
Reference: ghc/ghc!2192