GHC.HsToCore.Pmc.Solver.Types

Domain types used in GHC.HsToCore.Pmc.Solver. The ultimate goal is to define Nabla, which models normalised refinement types from the paper Lower Your Guards: A Compositional Pattern-Match Coverage Checker".

Normalised refinement types

data BotInfo

See vi_bot.

Constructors

IsBot

IsNotBot

MaybeBot

Instances

Outputable BotInfo

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: BotInfo -> SDoc

Eq BotInfo

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

(==) :: BotInfo -> BotInfo -> Bool

(/=) :: BotInfo -> BotInfo -> Bool

data PmAltConApp

Constructors

PACA

Fields

• paca_con :: !PmAltCon
• paca_tvs :: ![TyVar]
• paca_ids :: ![Id]

Instances

Outputable PmAltConApp

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: PmAltConApp -> SDoc

data VarInfo

Information about an Id. Stores positive (vi_pos) facts, like x ~ Just 42, and negative (vi_neg) facts, like "x is not (:)". Also caches the type (vi_ty), the ResidualCompleteMatches of a COMPLETE set (vi_rcm).

Subject to Note [The Pos/Neg invariant] in GHC.HsToCore.Pmc.Solver.

Constructors

VI

Fields

• vi_id :: !Id

  The Id in question. Important for adding new constraints relative to this VarInfo when we don't easily have the Id available.

• vi_pos :: ![PmAltConApp]

  Positive info: PmAltCon apps it is (i.e. x ~ [Just y, PatSyn z]), all at the same time (i.e. conjunctive). We need a list because of nested pattern matches involving pattern synonym case x of { Just y -> case x of PatSyn z -> ... } However, no more than one RealDataCon in the list, otherwise contradiction because of generativity.

• vi_neg :: !PmAltConSet

  Negative info: A list of PmAltCons that it cannot match. Example, assuming

      data T = Leaf Int | Branch T T | Node Int T
  

  then x ≁ [Leaf, Node] means that x cannot match a Leaf or Node, and hence can only match Branch. Is orthogonal to anything from vi_pos, in the sense that eqPmAltCon returns PossiblyOverlap for any pairing between vi_pos and vi_neg.

• vi_bot :: BotInfo

  Can this variable be ⊥? Models (mutually contradicting) x ~ ⊥ and x ≁ ⊥ constraints. E.g. * MaybeBot: Don't know; Neither x ~ ⊥ nor x ≁ ⊥. * IsBot: x ~ ⊥ * IsNotBot: x ≁ ⊥

• vi_rcm :: !ResidualCompleteMatches

  A cache of the associated COMPLETE sets. At any time a superset of possible constructors of each COMPLETE set. So, if it's not in here, we can't possibly match on it. Complementary to vi_neg. We still need it to recognise completion of a COMPLETE set efficiently for large enums.

Instances

Outputable VarInfo

Not user-facing.

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: VarInfo -> SDoc

data TmState

The term oracle state. Stores VarInfo for encountered Ids. These entries are possibly shared when we figure out that two variables must be equal, thus represent the same set of values.

See Note [TmState invariants] in GHC.HsToCore.Pmc.Solver.

Constructors

TmSt

Fields

• ts_facts :: !(UniqSDFM Id VarInfo)

  Facts about term variables. Deterministic env, so that we generate deterministic error messages.

• ts_reps :: !(CoreMap Id)

  An environment for looking up whether we already encountered semantically equivalent expressions that we want to represent by the same Id representative.

• ts_dirty :: !DIdSet

  Which VarInfo needs to be checked for inhabitants because of new negative constraints (e.g. x ≁ ⊥ or x ≁ K).

Instances

Outputable TmState

Not user-facing.

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: TmState -> SDoc

data TyState

The type oracle state. An InertSet that we incrementally add local type constraints to, together with a sequence number that counts the number of times we extended it with new facts.

Constructors

TySt

Fields

• ty_st_n :: !Int
• ty_st_inert :: !InertSet

Instances

Outputable TyState

Not user-facing.

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: TyState -> SDoc

data Nabla

A normalised refinement type ∇ ("nabla"), comprised of an inert set of canonical (i.e. mutually compatible) term and type constraints that form the refinement type's predicate.

Constructors

MkNabla

Fields

• nabla_ty_st :: !TyState

  Type oracle; things like a~Int

• nabla_tm_st :: !TmState

  Term oracle; things like x~Nothing

Instances

Outputable Nabla

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: Nabla -> SDoc

newtype Nablas

A disjunctive bag of Nablas, representing a refinement type.

Constructors

MkNablas (Bag Nabla)

Instances

Monoid Nablas

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

mempty :: Nablas

mappend :: Nablas -> Nablas -> Nablas

mconcat :: [Nablas] -> Nablas

Semigroup Nablas

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

(<>) :: Nablas -> Nablas -> Nablas

sconcat :: NonEmpty Nablas -> Nablas

stimes :: Integral b => b -> Nablas -> Nablas

Outputable Nablas

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: Nablas -> SDoc

initNablas :: Nablas

lookupRefuts :: Nabla -> Id -> [PmAltCon]

lookupSolution :: Nabla -> Id -> Maybe PmAltConApp

Looking up VarInfo

lookupVarInfo :: TmState -> Id -> VarInfo

lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)

Like lookupVarInfo ts x, but lookupVarInfo ts x = (y, vi) also looks through newtype constructors. We have x ~ N1 (... (Nk y)) such that the returned y doesn't have a positive newtype constructor constraint associated with it (yet). The VarInfo returned is that of y's representative.

Careful, this means that idType x might be different to idType y, even modulo type normalisation!

See also Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.

trvVarInfo :: Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)

Caching residual COMPLETE sets

data CompleteMatch

A list of conlikes which represents a complete pattern match. These arise from COMPLETE signatures. See also Note [Implementation of COMPLETE pragmas].

Instances

Outputable CompleteMatch

Defined in GHC.Types.CompleteMatch

Methods

ppr :: CompleteMatch -> SDoc

data ResidualCompleteMatches

A data type that caches for the VarInfo of x the results of querying dsGetCompleteMatches and then striking out all occurrences of K for which we already know x ≁ K from these sets.

For motivation, see Section 5.3 in Lower Your Guards. See also Note [Implementation of COMPLETE pragmas]

Constructors

RCM

Fields

• rcm_vanilla :: !(Maybe CompleteMatch)

  The residual set for the vanilla COMPLETE set from the data defn. Tracked separately from rcm_pragmas, because it might only be known much later (when we have enough type information to see the TyCon of the match), or not at all even. Until that happens, it is Nothing.

• rcm_pragmas :: !(Maybe [CompleteMatch])

  The residual sets for all COMPLETE sets from pragmas that are visible when compiling this module. Querying that set with dsGetCompleteMatches requires DsM, so we initialise it with Nothing until first needed in a DsM context.

Instances

Outputable ResidualCompleteMatches

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: ResidualCompleteMatches -> SDoc

getRcm :: ResidualCompleteMatches -> [CompleteMatch]

isRcmInitialised :: ResidualCompleteMatches -> Bool

Representations for Literals and AltCons

data PmLit

Literals (simple and overloaded ones) for pattern match checking.

See Note [Undecidable Equality for PmAltCons]

Constructors

PmLit

Fields

• pm_lit_ty :: Type
• pm_lit_val :: PmLitValue

Instances

Outputable PmLit

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: PmLit -> SDoc

Eq PmLit

Syntactic equality.

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

(==) :: PmLit -> PmLit -> Bool

(/=) :: PmLit -> PmLit -> Bool

data PmLitValue

Constructors

PmLitInt Integer

PmLitRat Rational

PmLitChar Char

PmLitString FastString

PmLitOverInt Int Integer

PmLitOverRat Int FractionalLit

PmLitOverString FastString

Instances

Outputable PmLitValue

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: PmLitValue -> SDoc

data PmAltCon

Represents the head of a match against a ConLike or literal. Really similar to AltCon.

Constructors

PmAltConLike ConLike

PmAltLit PmLit

Instances

Outputable PmAltCon

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: PmAltCon -> SDoc

Eq PmAltCon

Syntactic equality.

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

(==) :: PmAltCon -> PmAltCon -> Bool

(/=) :: PmAltCon -> PmAltCon -> Bool

pmLitType :: PmLit -> Type

Type of a PmLit

pmAltConType :: PmAltCon -> [Type] -> Type

Type of a PmAltCon

isPmAltConMatchStrict :: PmAltCon -> Bool

Is a match on this constructor forcing the match variable? True of data constructors, literals and pattern synonyms (#17357), but not of newtypes. See Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.

pmAltConImplBangs :: PmAltCon -> [HsImplBang]

PmAltConSet

data PmAltConSet

Instances

Outputable PmAltConSet

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: PmAltConSet -> SDoc

emptyPmAltConSet :: PmAltConSet

isEmptyPmAltConSet :: PmAltConSet -> Bool

elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool

Whether there is a PmAltCon in the PmAltConSet that compares Equal to the given PmAltCon according to eqPmAltCon.

extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet

pmAltConSetElems :: PmAltConSet -> [PmAltCon]

Equality on PmAltCons

data PmEquality

Undecidable semantic equality result. See Note [Undecidable Equality for PmAltCons]

Constructors

Equal

Disjoint

PossiblyOverlap

Instances

Show PmEquality

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

showsPrec :: Int -> PmEquality -> ShowS

show :: PmEquality -> String

showList :: [PmEquality] -> ShowS

Outputable PmEquality

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: PmEquality -> SDoc

Eq PmEquality

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

(==) :: PmEquality -> PmEquality -> Bool

(/=) :: PmEquality -> PmEquality -> Bool

eqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality

We can't in general decide whether two PmAltCons match the same set of values. In addition to the reasons in eqPmLit and eqConLike, a PmAltConLike might or might not represent the same value as a PmAltLit. See Note [Undecidable Equality for PmAltCons].

• Just True ==> Surely equal
• Just False ==> Surely different (non-overlapping, even!)
• Nothing ==> Equality relation undecidable

Examples (omitting some constructor wrapping):

• eqPmAltCon (LitInt 42) (LitInt 1) == Just False: Lit equality is decidable
• eqPmAltCon (DataCon A) (DataCon B) == Just False: DataCon equality is decidable
• eqPmAltCon (LitOverInt 42) (LitOverInt 1) == Nothing: OverLit equality is undecidable
• eqPmAltCon (PatSyn PA) (PatSyn PB) == Nothing: PatSyn equality is undecidable
• eqPmAltCon (DataCon I#) (LitInt 1) == Nothing: DataCon to Lit comparisons are undecidable without reasoning about the wrapped Int#
• eqPmAltCon (LitOverInt 1) (LitOverInt 1) == Just True: We assume reflexivity for overloaded literals
• eqPmAltCon (PatSyn PA) (PatSyn PA) == Just True: We assume reflexivity for Pattern Synonyms

Operations on PmLit

literalToPmLit :: Type -> Literal -> Maybe PmLit

negatePmLit :: PmLit -> Maybe PmLit

overloadPmLit :: Type -> PmLit -> Maybe PmLit

pmLitAsStringLit :: PmLit -> Maybe FastString

coreExprAsPmLit :: CoreExpr -> Maybe PmLit