Safe Haskell	None
Language	GHC2021

GHC.HsToCore.Pmc.Types

Contents

LYG syntax
- Guard language
- Guard tree language
Coverage Checking types
Pre and post coverage checking synonyms
Normalised refinement types

Description

Types used through-out pattern match checking. This module is mostly there to be imported from GHC.HsToCore.Types. The exposed API is that of GHC.HsToCore.Pmc.

These types model the paper Lower Your Guards: A Compositional Pattern-Match Coverage Checker".

Synopsis

newtype SrcInfo = SrcInfo (Located SDoc)
data PmGrd
- = PmCon {
  - pm_id :: !Id
  - pm_con_con :: !PmAltCon
  - pm_con_tvs :: ![TyVar]
  - pm_con_dicts :: ![EvVar]
  - pm_con_args :: ![Id]
  }
- | PmBang {
  - pm_id :: !Id
  - _pm_loc :: !(Maybe SrcInfo)
  }
- | PmLet {
  - pm_id :: !Id
  - _pm_let_expr :: !CoreExpr
  }
data GrdDag
- = GdEnd
- | GdOne !PmGrd
- | GdSeq !GrdDag !GrdDag
- | GdAlt !GrdDag !GrdDag
consGrdDag :: PmGrd -> GrdDag -> GrdDag
gdSeq :: GrdDag -> GrdDag -> GrdDag
sequencePmGrds :: [PmGrd] -> GrdDag
sequenceGrdDags :: [GrdDag] -> GrdDag
alternativesGrdDags :: NonEmpty GrdDag -> GrdDag
newtype PmMatchGroup p = PmMatchGroup (NonEmpty (PmMatch p))
data PmMatch p = PmMatch {
- pm_pats :: !p
- pm_grhss :: !(PmGRHSs p)
}
data PmGRHSs p = PmGRHSs {
- pgs_lcls :: !p
- pgs_grhss :: !(NonEmpty (PmGRHS p))
}
data PmGRHS p = PmGRHS {
- pg_grds :: !p
- pg_rhs :: !SrcInfo
}
newtype PmPatBind p = PmPatBind (PmGRHS p)
newtype PmEmptyCase = PmEmptyCase {
- pe_var :: Id
}
data PmRecSel v = PmRecSel {
- pr_arg_var :: v
- pr_arg :: CoreExpr
- pr_cons :: [ConLike]
}
data RedSets = RedSets {
- rs_cov :: !Nablas
- rs_div :: !Nablas
- rs_bangs :: !(OrdList (Nablas, SrcInfo))
}
data Precision
- = Approximate
- | Precise
data CheckResult a = CheckResult {
- cr_ret :: !a
- cr_uncov :: !Nablas
- cr_approx :: !Precision
}
type Pre = GrdDag
type Post = RedSets
module GHC.HsToCore.Pmc.Solver.Types

LYG syntax

Guard language

newtype SrcInfo Source #

Means by which we identify a source construct for later pretty-printing in a warning message. SDoc for the equation to show, Located for the location.

Constructors

SrcInfo (Located SDoc)

Instances

Instances details

Outputable SrcInfo Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods ppr :: SrcInfo -> SDoc Source #

data PmGrd Source #

A very simple language for pattern guards. Let bindings, bang patterns, and matching variables against flat constructor patterns. The LYG guard language.

Constructors

PmCon	`PmCon x K dicts args` corresponds to a `K dicts args <- x` guard. The `args` are bound in this construct, the `x` is just a use. For the arguments' meaning see `ConPatOut`.
Fields pm_id :: !Id pm_con_con :: !PmAltCon pm_con_tvs :: ![TyVar] pm_con_dicts :: ![EvVar] pm_con_args :: ![Id]
PmBang	`PmBang x` corresponds to a `seq x True` guard. If the extra `SrcInfo` is present, the bang guard came from a source bang pattern, in which case we might want to report it as redundant. See Note [Dead bang patterns] in GHC.HsToCore.Pmc.Check.
Fields pm_id :: !Id _pm_loc :: !(Maybe SrcInfo)
PmLet	`PmLet x expr` corresponds to a `let x = expr` guard. This actually binds `x`.
Fields pm_id :: !Id _pm_let_expr :: !CoreExpr

Instances

Instances details

Outputable PmGrd Source #	Should not be user-facing.
Instance details Defined in GHC.HsToCore.Pmc.Types Methods ppr :: PmGrd -> SDoc Source #

data GrdDag Source #

A series-parallel graph of PmGrds, so very nearly a guard tree, if it weren't for or-patterns/GdAlt! The implicit "source" corresponds to "before the match" and the implicit "sink" corresponds to "after a successful match".

GdEnd is a GrdDag that always matches.
GdOne is a GrdDag that matches iff its PmGrd matches.
GdSeq g1 g2 corresponds to matching guards g1 and then g2 if matching g1 succeeded. Example: The Haskell guard | x > 1, x < 10 = ... will test x > 1 before x < 10, failing if either test fails.
GdAlt g1 g2 is far less common than GdSeq and corresponds to matching an or-pattern (LT; EQ), succeeding if the match variable matches either LT or EQ. See Note [Implementation of OrPatterns] for a larger example.

Constructors

GdEnd
GdOne !PmGrd
GdSeq !GrdDag !GrdDag
GdAlt !GrdDag !GrdDag

Instances

Instances details

Outputable GrdDag Source #	Format LYG guards as `\| True <- x, let x = 42, !z`
Instance details Defined in GHC.HsToCore.Pmc.Types Methods ppr :: GrdDag -> SDoc Source #

consGrdDag :: PmGrd -> GrdDag -> GrdDag Source #

Sequentially compose a PmGrd in front of a GrdDag.

gdSeq :: GrdDag -> GrdDag -> GrdDag Source #

Sequentially compose two GrdDags. A smart constructor for GdSeq that eliminates GdEnds.

sequencePmGrds :: [PmGrd] -> GrdDag Source #

Sequentially compose a list of PmGrds into a GrdDag.

sequenceGrdDags :: [GrdDag] -> GrdDag Source #

Sequentially compose a list of GrdDags.

alternativesGrdDags :: NonEmpty GrdDag -> GrdDag Source #

Parallel composition of a list of GrdDags. Needs a non-empty list as GdAlt does not have a neutral element.

Guard tree language

newtype PmMatchGroup p Source #

A guard tree denoting MatchGroup.

Constructors

PmMatchGroup (NonEmpty (PmMatch p))

Instances

Instances details

Outputable p => Outputable (PmMatchGroup p) Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods ppr :: PmMatchGroup p -> SDoc Source #

data PmMatch p Source #

A guard tree denoting Match: A payload describing the pats and a bunch of GRHS.

Constructors

PmMatch
Fields pm_pats :: !p pm_grhss :: !(PmGRHSs p)

Instances

Instances details

Outputable p => Outputable (PmMatch p) Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods ppr :: PmMatch p -> SDoc Source #

data PmGRHSs p Source #

A guard tree denoting GRHSs: A bunch of PmLet guards for local bindings from the GRHSss where clauses and the actual list of GRHS. See Note [Long-distance information for HsLocalBinds] in GHC.HsToCore.Pmc.Desugar.

Constructors

PmGRHSs
Fields pgs_lcls :: !p pgs_grhss :: !(NonEmpty (PmGRHS p))

Instances

Instances details

Outputable p => Outputable (PmGRHSs p) Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods ppr :: PmGRHSs p -> SDoc Source #

data PmGRHS p Source #

A guard tree denoting GRHS: A payload describing the grds and a SrcInfo useful for printing out in warnings messages.

Constructors

PmGRHS
Fields pg_grds :: !p pg_rhs :: !SrcInfo

Instances

Instances details

Outputable p => Outputable (PmGRHS p) Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods ppr :: PmGRHS p -> SDoc Source #

newtype PmPatBind p Source #

A guard tree denoting a pattern binding.

Constructors

PmPatBind (PmGRHS p)

Instances

Instances details

Outputable p => Outputable (PmPatBind p) Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods ppr :: PmPatBind p -> SDoc Source #

newtype PmEmptyCase Source #

A guard tree denoting an -XEmptyCase.

Constructors

PmEmptyCase
Fields pe_var :: Id

Instances

Instances details

Outputable PmEmptyCase Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods ppr :: PmEmptyCase -> SDoc Source #

data PmRecSel v Source #

Constructors

PmRecSel
Fields pr_arg_var :: v pr_arg :: CoreExpr pr_cons :: [ConLike]

Coverage Checking types

data RedSets Source #

Redundancy sets, used to determine redundancy of RHSs and bang patterns (later digested into a CIRB).

Constructors

RedSets

Fields

rs_cov :: !Nablas
The Covered set; the set of values reaching a particular program point.
rs_div :: !Nablas
The Diverging set; empty if no match can lead to divergence. If it wasn't empty, we have to turn redundancy warnings into inaccessibility warnings for any subclauses.
rs_bangs :: !(OrdList (Nablas, SrcInfo))
If any of the Nablas is empty, the corresponding SrcInfo pin-points a bang pattern in source that is redundant. See Note [Dead bang patterns].

Instances

Instances details

Outputable RedSets Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods ppr :: RedSets -> SDoc Source #

data Precision Source #

Constructors

Approximate
Precise

Instances

Instances details

Outputable Precision Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods ppr :: Precision -> SDoc Source #
Monoid Precision Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods mempty :: Precision # mappend :: Precision -> Precision -> Precision # mconcat :: [Precision] -> Precision #
Semigroup Precision Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods (<>) :: Precision -> Precision -> Precision # sconcat :: NonEmpty Precision -> Precision # stimes :: Integral b => b -> Precision -> Precision #
Show Precision Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods showsPrec :: Int -> Precision -> ShowS # show :: Precision -> String # showList :: [Precision] -> ShowS #
Eq Precision Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods (==) :: Precision -> Precision -> Bool # (/=) :: Precision -> Precision -> Bool #

data CheckResult a Source #

Pattern-match coverage check result

Constructors

CheckResult
Fields cr_ret :: !a A hole for redundancy info and covered sets. cr_uncov :: !Nablas The set of uncovered values falling out at the bottom. (for -Wincomplete-patterns, but also important state for the algorithm) cr_approx :: !Precision A flag saying whether we ran into the `maxPmCheckModels` limit for the purpose of suggesting to crank it up in the warning message. Writer state.

Instances

Instances details

Functor CheckResult Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods fmap :: (a -> b) -> CheckResult a -> CheckResult b # (<$) :: a -> CheckResult b -> CheckResult a #
Outputable a => Outputable (CheckResult a) Source #
Instance details Defined in GHC.HsToCore.Pmc.Types Methods ppr :: CheckResult a -> SDoc Source #

Pre and post coverage checking synonyms

type Pre = GrdDag Source #

Used as tree payload pre-checking. The LYG guards to check.

type Post = RedSets Source #

Used as tree payload post-checking. The redundancy info we elaborated.

Normalised refinement types

module GHC.HsToCore.Pmc.Solver.Types