Safe Haskell  None 

Language  GHC2021 
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 PatternMatch Coverage Checker".
Synopsis
 data BotInfo
 data PmAltConApp = PACA {}
 data VarInfo = VI {
 vi_id :: !Id
 vi_pos :: ![PmAltConApp]
 vi_neg :: !PmAltConSet
 vi_bot :: BotInfo
 vi_rcm :: !ResidualCompleteMatches
 data TmState = TmSt {}
 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)
 type CompleteMatch = CompleteMatchX Name
 data ResidualCompleteMatches = RCM {
 rcm_vanilla :: !(Maybe DsCompleteMatch)
 rcm_pragmas :: !(Maybe DsCompleteMatches)
 getRcm :: ResidualCompleteMatches > DsCompleteMatches
 isRcmInitialised :: ResidualCompleteMatches > Bool
 data PmLit = PmLit {}
 data PmLitValue
 data PmAltCon
 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
 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
See vi_bot
.
data PmAltConApp Source #
Instances
Outputable PmAltConApp Source #  
Defined in GHC.HsToCore.Pmc.Solver.Types ppr :: PmAltConApp > SDoc 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.
VI  

Instances
Outputable VarInfo Source #  Not userfacing. 
The term oracle state. Stores VarInfo
for encountered Id
s. 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.
TmSt  

Instances
Outputable TmState Source #  Not userfacing. 
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.
TySt  

Instances
Outputable TyState Source #  Not userfacing. 
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.
MkNabla  

Instances
A disjunctive bag of Nabla
s, representing a refinement type.
initNablas :: Nablas Source #
lookupSolution :: Nabla > Id > Maybe PmAltConApp 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.
Caching residual COMPLETE sets
type CompleteMatch = CompleteMatchX Name 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]
RCM  

Instances
Representations for Literals and AltCons
Literals (simple and overloaded ones) for pattern match checking.
See Note [Undecidable Equality for PmAltCons]
PmLit  

data PmLitValue Source #
PmLitInt Integer  
PmLitRat Rational  
PmLitChar Char  
PmLitString FastString  
PmLitOverInt Int Integer  
PmLitOverRat Int FractionalLit  
PmLitOverString FastString 
Instances
Outputable PmLitValue Source #  
Defined in GHC.HsToCore.Pmc.Solver.Types ppr :: PmLitValue > SDoc Source # 
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
Outputable PmAltConSet Source #  
Defined in GHC.HsToCore.Pmc.Solver.Types ppr :: PmAltConSet > SDoc 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]
Instances
Outputable PmEquality Source #  
Defined in GHC.HsToCore.Pmc.Solver.Types ppr :: PmEquality > SDoc Source #  
Show PmEquality Source #  
Defined in GHC.HsToCore.Pmc.Solver.Types showsPrec :: Int > PmEquality > ShowS # show :: PmEquality > String # showList :: [PmEquality] > ShowS #  
Eq PmEquality Source #  
Defined in GHC.HsToCore.Pmc.Solver.Types (==) :: PmEquality > PmEquality > Bool # (/=) :: PmEquality > PmEquality > Bool # 
eqPmAltCon :: PmAltCon > PmAltCon > PmEquality Source #
We can't in general decide whether two PmAltCon
s 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 equalJust False
==> Surely different (nonoverlapping, even!)Nothing
==> Equality relation undecidable
Examples (omitting some constructor wrapping):
eqPmAltCon (LitInt 42) (LitInt 1) == Just False
: Lit equality is decidableeqPmAltCon (DataCon A) (DataCon B) == Just False
: DataCon equality is decidableeqPmAltCon (LitOverInt 42) (LitOverInt 1) == Nothing
: OverLit equality is undecidableeqPmAltCon (PatSyn PA) (PatSyn PB) == Nothing
: PatSyn equality is undecidableeqPmAltCon (DataCon I#) (LitInt 1) == Nothing
: DataCon to Lit comparisons are undecidable without reasoning about the wrappedInt#
eqPmAltCon (LitOverInt 1) (LitOverInt 1) == Just True
: We assume reflexivity for overloaded literalseqPmAltCon (PatSyn PA) (PatSyn PA) == Just True
: We assume reflexivity for Pattern Synonyms
Operations on PmLit
pmLitAsStringLit :: PmLit > Maybe FastString Source #