ghc-9.6.0.20230128: The GHC API
Safe HaskellSafe-Inferred
LanguageHaskell2010

GHC.HsToCore.Pmc.Solver.Types

Description

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

Synopsis

Normalised refinement types

data BotInfo Source #

See vi_bot.

Constructors

IsBot 
IsNotBot 
MaybeBot 

Instances

Instances details
Outputable BotInfo Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: BotInfo -> SDoc Source #

Eq BotInfo Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

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

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

data PmAltConApp Source #

Constructors

PACA 

Fields

Instances

Instances details
Outputable PmAltConApp Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: PmAltConApp -> SDoc Source #

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

Instances details
Outputable VarInfo Source #

Not user-facing.

Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: VarInfo -> SDoc Source #

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

Instances details
Outputable TmState Source #

Not user-facing.

Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: TmState -> SDoc Source #

data TyState Source #

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

Instances

Instances details
Outputable TyState Source #

Not user-facing.

Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: TyState -> SDoc Source #

data Nabla Source #

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

Instances

Instances details
Outputable Nabla Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: Nabla -> SDoc Source #

newtype Nablas Source #

A disjunctive bag of Nablas, representing a refinement type.

Constructors

MkNablas (Bag Nabla) 

Instances

Instances details
Monoid Nablas Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Semigroup Nablas Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Outputable Nablas Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: Nablas -> SDoc Source #

Looking up VarInfo

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

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

Caching residual COMPLETE sets

data CompleteMatch Source #

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

Instances

Instances details
Outputable CompleteMatch Source # 
Instance details

Defined in GHC.Types.CompleteMatch

data ResidualCompleteMatches Source #

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

Instances details
Outputable ResidualCompleteMatches Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

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
Outputable PmLit Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: PmLit -> SDoc Source #

Eq PmLit Source #

Syntactic equality.

Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

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

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

data PmAltCon Source #

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

Instances

Instances details
Outputable PmAltCon Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: PmAltCon -> SDoc Source #

Eq PmAltCon Source #

Syntactic equality.

Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

pmLitType :: PmLit -> Type Source #

Type of a PmLit

isPmAltConMatchStrict :: PmAltCon -> Bool Source #

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.

PmAltConSet

data PmAltConSet Source #

Instances

Instances details
Outputable PmAltConSet Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: PmAltConSet -> SDoc Source #

elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool Source #

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

Equality on PmAltCons

data PmEquality Source #

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

Instances

Instances details
Show PmEquality Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Outputable PmEquality Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: PmEquality -> SDoc Source #

Eq PmEquality Source # 
Instance details

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