ghc-8.10.2: The GHC API
Safe HaskellNone
LanguageHaskell2010

GHC.HsToCore.PmCheck.Types

Description

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

Synopsis

Representations for Literals and AltCons

data PmLit Source #

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

See Note [Undecidable Equality for PmAltCons]

Constructors

PmLit 

Instances

Instances details
Eq PmLit Source #

Syntactic equality.

Instance details

Defined in GHC.HsToCore.PmCheck.Types

Methods

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

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

Outputable PmLit Source # 
Instance details

Defined in GHC.HsToCore.PmCheck.Types

data PmAltCon Source #

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

Instances

Instances details
Eq PmAltCon Source #

Syntactic equality.

Instance details

Defined in GHC.HsToCore.PmCheck.Types

Outputable PmAltCon Source # 
Instance details

Defined in GHC.HsToCore.PmCheck.Types

pmLitType :: PmLit -> Type Source #

Type of a PmLit

Equality on PmAltCons

data PmEquality Source #

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

Instances

Instances details
Eq PmEquality Source # 
Instance details

Defined in GHC.HsToCore.PmCheck.Types

Show PmEquality Source # 
Instance details

Defined in GHC.HsToCore.PmCheck.Types

Outputable PmEquality Source # 
Instance details

Defined in GHC.HsToCore.PmCheck.Types

eqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality Source #

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

Caching partially matched COMPLETE sets

data PossibleMatches Source #

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

Instances details
Outputable PossibleMatches Source # 
Instance details

Defined in GHC.HsToCore.PmCheck.Types

A DIdEnv where entries may be shared

data Shared a Source #

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

Instances details
Outputable a => Outputable (Shared a) Source # 
Instance details

Defined in GHC.HsToCore.PmCheck.Types

Methods

ppr :: Shared a -> SDoc Source #

pprPrec :: Rational -> Shared a -> SDoc Source #

newtype SharedDIdEnv a Source #

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

Instances

Instances details
Outputable a => Outputable (SharedDIdEnv a) Source # 
Instance details

Defined in GHC.HsToCore.PmCheck.Types

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

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 Source #

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

setIndirectSDIE :: SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a Source #

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 Source #

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

traverseSDIE :: Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b) Source #

The pattern match oracle

data VarInfo Source #

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 PmOracle.

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, [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 :: ![PmAltCon]

    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

Instances details
Outputable VarInfo Source #

Not user-facing.

Instance details

Defined in GHC.HsToCore.PmCheck.Types

data TmState Source #

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 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

Instances details
Outputable TmState Source #

Not user-facing.

Instance details

Defined in GHC.HsToCore.PmCheck.Types

newtype TyState Source #

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

Instances details
Outputable TyState Source #

Not user-facing.

Instance details

Defined in GHC.HsToCore.PmCheck.Types

data Delta Source #

Term and type constraints to accompany each value vector abstraction. For efficiency, we store the term oracle state instead of the term constraints.

Constructors

MkDelta 

Instances

Instances details
Outputable Delta Source # 
Instance details

Defined in GHC.HsToCore.PmCheck.Types

initDelta :: Delta Source #

An initial delta that is always satisfiable