Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- 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
- type CompleteMatch = UniqDSet ConLike
- data ResidualCompleteMatches = RCM {
- rcm_vanilla :: !(Maybe CompleteMatch)
- rcm_pragmas :: !(Maybe [CompleteMatch])
- getRcm :: ResidualCompleteMatches -> [CompleteMatch]
- isRcmInitialised :: ResidualCompleteMatches -> Bool
- data PmLit = PmLit {}
- data PmLitValue
- = PmLitInt Integer
- | PmLitRat Rational
- | PmLitChar Char
- | PmLitString FastString
- | PmLitOverInt Int Integer
- | PmLitOverRat Int Rational
- | 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
- 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 |
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 | |
|
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 | |
|
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 | |
|
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 | |
|
A disjunctive bag of Nabla
s, representing a refinement type.
initNablas :: Nablas Source #
Caching residual COMPLETE sets
type CompleteMatch = UniqDSet ConLike #
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
Outputable ResidualCompleteMatches Source # | |
Defined in GHC.HsToCore.Pmc.Solver.Types ppr :: ResidualCompleteMatches -> SDoc |
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 Rational | |
PmLitOverString FastString |
Instances
Outputable PmLitValue Source # | |
Defined in GHC.HsToCore.Pmc.Solver.Types ppr :: PmLitValue -> SDoc |
Represents the head of a match against a ConLike
or literal.
Really similar to AltCon
.
PmAltConLike ConLike | |
PmAltLit 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.
pmAltConImplBangs :: PmAltCon -> [HsImplBang] Source #
PmAltConSet
data PmAltConSet Source #
Instances
Outputable PmAltConSet Source # | |
Defined in GHC.HsToCore.Pmc.Solver.Types ppr :: PmAltConSet -> SDoc |
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
Eq PmEquality Source # | |
Defined in GHC.HsToCore.Pmc.Solver.Types (==) :: PmEquality -> PmEquality -> Bool # (/=) :: PmEquality -> PmEquality -> Bool # | |
Show PmEquality Source # | |
Defined in GHC.HsToCore.Pmc.Solver.Types showsPrec :: Int -> PmEquality -> ShowS # show :: PmEquality -> String # showList :: [PmEquality] -> ShowS # | |
Outputable PmEquality Source # | |
Defined in GHC.HsToCore.Pmc.Solver.Types ppr :: PmEquality -> SDoc |
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 (non-overlapping, 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 #
coreExprAsPmLit :: CoreExpr -> Maybe PmLit Source #