Safe Haskell	None
Language	GHC2021

GHC.HsToCore.Pmc.Solver.Types

Contents

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

data BotInfo
- = IsBot
- | IsNotBot
- | MaybeBot
data PmAltConApp = PACA {
- paca_con :: !PmAltCon
- paca_tvs :: ![TyVar]
- paca_ids :: ![Id]
}
data VarInfo = VI {
- vi_id :: !Id
- vi_pos :: ![PmAltConApp]
- vi_neg :: !PmAltConSet
- vi_bot :: BotInfo
- vi_rcm :: !ResidualCompleteMatches
}
data TmState = TmSt {
- ts_facts :: !(UniqSDFM Id VarInfo)
- ts_reps :: !(CoreMap Id)
- ts_dirty :: !DIdSet
}
data TyState = TySt {
- ty_st_n :: !Int
- ty_st_inert :: !InertSet
}
data Nabla = MkNabla {
- nabla_ty_st :: !TyState
- nabla_tm_st :: !TmState
}
newtype Nablas = MkNablas (Bag Nabla)
initNablas :: Nablas
lookupRefuts :: Nabla -> Id -> [PmAltCon]
lookupSolution :: Nabla -> Id -> Maybe PmAltConApp
lookupVarInfo :: TmState -> Id -> VarInfo
lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)
trvVarInfo :: Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
data CompleteMatch
data ResidualCompleteMatches = RCM {
- rcm_vanilla :: !(Maybe CompleteMatch)
- rcm_pragmas :: !(Maybe [CompleteMatch])
}
getRcm :: ResidualCompleteMatches -> [CompleteMatch]
isRcmInitialised :: ResidualCompleteMatches -> Bool
data PmLit = PmLit {
- pm_lit_ty :: Type
- pm_lit_val :: PmLitValue
}
data PmLitValue
- = PmLitInt Integer
- | PmLitRat Rational
- | PmLitChar Char
- | PmLitString FastString
- | PmLitOverInt Int Integer
- | PmLitOverRat Int FractionalLit
- | PmLitOverString FastString
data PmAltCon
- = PmAltConLike ConLike
- | PmAltLit PmLit
pmLitType :: PmLit -> Type
pmAltConType :: PmAltCon -> [Type] -> Type
isPmAltConMatchStrict :: PmAltCon -> Bool
pmAltConImplBangs :: PmAltCon -> [HsImplBang]
data PmAltConSet
emptyPmAltConSet :: PmAltConSet
isEmptyPmAltConSet :: PmAltConSet -> Bool
elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool
extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet
pmAltConSetElems :: PmAltConSet -> [PmAltCon]
data PmEquality
- = Equal
- | Disjoint
- | PossiblyOverlap
eqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality
literalToPmLit :: Type -> Literal -> Maybe PmLit
negatePmLit :: PmLit -> Maybe PmLit
overloadPmLit :: Type -> PmLit -> Maybe PmLit
pmLitAsStringLit :: PmLit -> Maybe FastString
coreExprAsPmLit :: CoreExpr -> Maybe PmLit

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 paca_con :: !PmAltCon paca_tvs :: ![TyVar] paca_ids :: ![Id]

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 ty_st_n :: !Int ty_st_inert :: !InertSet

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 nabla_ty_st :: !TyState Type oracle; things like a~Int nabla_tm_st :: !TmState Term oracle; things like x~Nothing

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

Outputable Nablas Source #
Instance details Defined in GHC.HsToCore.Pmc.Solver.Types Methods ppr :: Nablas -> SDoc Source #
Monoid Nablas Source #
Instance details Defined in GHC.HsToCore.Pmc.Solver.Types Methods mempty :: Nablas # mappend :: Nablas -> Nablas -> Nablas # mconcat :: [Nablas] -> Nablas #
Semigroup Nablas Source #
Instance details Defined in GHC.HsToCore.Pmc.Solver.Types Methods (<>) :: Nablas -> Nablas -> Nablas # sconcat :: NonEmpty Nablas -> Nablas # stimes :: Integral b => b -> Nablas -> Nablas #

initNablas :: Nablas Source #

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

lookupSolution :: Nabla -> Id -> Maybe PmAltConApp Source #

Looking up `VarInfo`

lookupVarInfo :: TmState -> Id -> VarInfo Source #

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 Methods ppr :: CompleteMatch -> SDoc Source #

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 Methods ppr :: ResidualCompleteMatches -> SDoc Source #

getRcm :: ResidualCompleteMatches -> [CompleteMatch] Source #

isRcmInitialised :: ResidualCompleteMatches -> Bool Source #

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
Fields pm_lit_ty :: Type pm_lit_val :: PmLitValue

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

Constructors

PmLitInt Integer
PmLitRat Rational
PmLitChar Char
PmLitString FastString
PmLitOverInt Int Integer
PmLitOverRat Int FractionalLit
PmLitOverString FastString

Instances

Instances details

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

data PmAltCon Source #

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

Constructors

PmAltConLike ConLike
PmAltLit PmLit

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 Methods (==) :: PmAltCon -> PmAltCon -> Bool # (/=) :: PmAltCon -> PmAltCon -> Bool #

pmLitType :: PmLit -> Type Source #

Type of a PmLit

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

Type of a PmAltCon

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.

pmAltConImplBangs :: PmAltCon -> [HsImplBang] Source #

PmAltConSet

data PmAltConSet Source #

Instances

Instances details

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

emptyPmAltConSet :: PmAltConSet Source #

isEmptyPmAltConSet :: PmAltConSet -> Bool Source #

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

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

extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet Source #

pmAltConSetElems :: PmAltConSet -> [PmAltCon] Source #

Equality on `PmAltCon`s

data PmEquality Source #

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

Constructors

Equal
Disjoint
PossiblyOverlap

Instances

Instances details

Outputable PmEquality Source #
Instance details Defined in GHC.HsToCore.Pmc.Solver.Types Methods ppr :: PmEquality -> SDoc Source #
Show PmEquality Source #
Instance details Defined in GHC.HsToCore.Pmc.Solver.Types Methods showsPrec :: Int -> PmEquality -> ShowS # show :: PmEquality -> String # showList :: [PmEquality] -> ShowS #
Eq PmEquality Source #
Instance details Defined in GHC.HsToCore.Pmc.Solver.Types Methods (==) :: PmEquality -> PmEquality -> Bool # (/=) :: PmEquality -> PmEquality -> Bool #

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