Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,399
    • Issues 5,399
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 588
    • Merge requests 588
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Merge requests
  • !1010

TmOracle: Replace negative term equalities by refutable PmAltCons

  • Review changes

  • Download
  • Email patches
  • Plain diff
Closed Sebastian Graf requested to merge wip/pmcheck-refuts into master May 22, 2019
  • Overview 105
  • Commits 1
  • Pipelines 29
  • Changes 15

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 Jun 03, 2019 by Sebastian Graf
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: wip/pmcheck-refuts