GHC.HsToCore.PmCheck.Types

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

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.PmCheck.Types

Methods

ppr :: PmLit -> SDoc

pprPrec :: Rational -> PmLit -> SDoc

Eq PmLit

Syntactic equality.

Defined in GHC.HsToCore.PmCheck.Types

Methods

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

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

data PmLitValue

Constructors

PmLitInt Integer

PmLitRat Rational

PmLitChar Char

PmLitString FastString

PmLitOverInt Int Integer

PmLitOverRat Int Rational

PmLitOverString FastString

Instances

Outputable PmLitValue

Defined in GHC.HsToCore.PmCheck.Types

Methods

ppr :: PmLitValue -> SDoc

pprPrec :: Rational -> 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.PmCheck.Types

Methods

ppr :: PmAltCon -> SDoc

pprPrec :: Rational -> PmAltCon -> SDoc

Eq PmAltCon

Syntactic equality.

Defined in GHC.HsToCore.PmCheck.Types

Methods

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

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

pmLitType :: PmLit -> Type

Type of a PmLit

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

Type of a 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.PmCheck.Types

Methods

showsPrec :: Int -> PmEquality -> ShowS

show :: PmEquality -> String

showList :: [PmEquality] -> ShowS

Outputable PmEquality

Defined in GHC.HsToCore.PmCheck.Types

Methods

ppr :: PmEquality -> SDoc

pprPrec :: Rational -> PmEquality -> SDoc

Eq PmEquality

Defined in GHC.HsToCore.PmCheck.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

Caching partially matched COMPLETE sets

type ConLikeSet = UniqDSet ConLike

data PossibleMatches

A data type caching the results of completeMatchConLikes with support for deletion of constructors that were already matched on.

Constructors

PM (NonEmpty ConLikeSet)

Each ConLikeSet is a (subset of) the constructors in a COMPLETE set NonEmpty because the empty case would mean that the type has no COMPLETE set at all, for which we have NoPM.

NoPM

No COMPLETE set for this type (yet). Think of overloaded literals.

Instances

Outputable PossibleMatches

Defined in GHC.HsToCore.PmCheck.Types

Methods

ppr :: PossibleMatches -> SDoc

pprPrec :: Rational -> PossibleMatches -> SDoc

PmAltConSet

data PmAltConSet

Instances

Outputable PmAltConSet

Defined in GHC.HsToCore.PmCheck.Types

Methods

ppr :: PmAltConSet -> SDoc

pprPrec :: Rational -> 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]

A DIdEnv where entries may be shared

data Shared a

Either Indirect x, meaning the value is represented by that of x, or an Entry containing containing the actual value it represents.

Constructors

Indirect Id

Entry a

Instances

Outputable a => Outputable (Shared a)

Defined in GHC.HsToCore.PmCheck.Types

Methods

ppr :: Shared a -> SDoc

pprPrec :: Rational -> Shared a -> SDoc

newtype SharedDIdEnv a

A DIdEnv in which entries can be shared by multiple Ids. Merge equivalence classes of two Ids by setIndirectSDIE and set the entry of an Id with setEntrySDIE.

Constructors

SDIE

Fields

• unSDIE :: DIdEnv (Shared a)

Instances

Outputable a => Outputable (SharedDIdEnv a)

Defined in GHC.HsToCore.PmCheck.Types

Methods

ppr :: SharedDIdEnv a -> SDoc

pprPrec :: Rational -> SharedDIdEnv a -> SDoc

emptySDIE :: SharedDIdEnv a

lookupSDIE :: SharedDIdEnv a -> Id -> Maybe a

lookupSDIE env x looks up an entry for x, looking through all Indirects until it finds a shared Entry.

sameRepresentativeSDIE :: SharedDIdEnv a -> Id -> Id -> Bool

Check if two variables are part of the same equivalence class.

setIndirectSDIE :: SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a

setIndirectSDIE env x y sets x's Entry to Indirect y, thereby merging x's equivalence class into y's. This will discard all info on x!

setEntrySDIE :: SharedDIdEnv a -> Id -> a -> SharedDIdEnv a

setEntrySDIE env x a sets the Entry x is associated with to a, thereby modifying its whole equivalence class.

traverseSDIE :: forall a b f. Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b)

The pattern match oracle

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 PossibleMatches of a COMPLETE set (vi_cache).

Subject to Note [The Pos/Neg invariant] in GHC.HsToCore.PmCheck.Oracle.

Constructors

VI

Fields

• vi_ty :: !Type

  The type of the variable. Important for rejecting possible GADT constructors or incompatible pattern synonyms (Just42 :: Maybe Int).

• vi_pos :: ![(PmAltCon, [TyVar], [Id])]

  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_cache :: !PossibleMatches

  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.PmCheck.Types

Methods

ppr :: VarInfo -> SDoc

pprPrec :: Rational -> 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.PmCheck.Oracle.

Constructors

TmSt

Fields

• ts_facts :: !(SharedDIdEnv 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.

Instances

Outputable TmState

Not user-facing.

Defined in GHC.HsToCore.PmCheck.Types

Methods

ppr :: TmState -> SDoc

pprPrec :: Rational -> TmState -> SDoc

newtype TyState

The type oracle state. A poor man's InsertSet: The invariant is that all constraints in there are mutually compatible.

Constructors

TySt (Bag EvVar)

Instances

Outputable TyState

Not user-facing.

Defined in GHC.HsToCore.PmCheck.Types

Methods

ppr :: TyState -> SDoc

pprPrec :: Rational -> TyState -> SDoc

data Delta

An inert set of canonical (i.e. mutually compatible) term and type constraints.

Constructors

MkDelta

Fields

• delta_ty_st :: TyState
• delta_tm_st :: TmState

Instances

Outputable Delta

Defined in GHC.HsToCore.PmCheck.Types

Methods

ppr :: Delta -> SDoc

pprPrec :: Rational -> Delta -> SDoc

newtype Deltas

A disjunctive bag of Deltas, representing a refinement type.

Constructors

MkDeltas (Bag Delta)

Instances

Semigroup Deltas

Defined in GHC.HsToCore.PmCheck.Types

Methods

(<>) :: Deltas -> Deltas -> Deltas

sconcat :: NonEmpty Deltas -> Deltas

stimes :: Integral b => b -> Deltas -> Deltas

Outputable Deltas

Defined in GHC.HsToCore.PmCheck.Types

Methods

ppr :: Deltas -> SDoc

pprPrec :: Rational -> Deltas -> SDoc

initDeltas :: Deltas

liftDeltasM :: Monad m => (Delta -> m (Maybe Delta)) -> Deltas -> m Deltas