Safe Haskell | None |
---|---|
Language | Haskell2010 |
The pattern match oracle. The main export of the module are the functions
addTmCt
, addVarCoreCt
, addRefutableAltCon
and addTypeEvidence
for
adding facts to the oracle, and provideEvidence
to turn a
Delta
into a concrete evidence for an equation.
Synopsis
- type DsM = TcRnIf DsGblEnv DsLclEnv
- tracePm :: String -> SDoc -> DsM ()
- mkPmId :: Type -> DsM Id
- data Delta
- initDelta :: Delta
- lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon]
- lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [Id])
- data TmCt
- addTypeEvidence :: Delta -> Bag EvVar -> DsM (Maybe Delta)
- addRefutableAltCon :: Delta -> Id -> PmAltCon -> DsM (Maybe Delta)
- addTmCt :: Delta -> TmCt -> DsM (Maybe Delta)
- addVarCoreCt :: Delta -> Id -> CoreExpr -> DsM (Maybe Delta)
- canDiverge :: Delta -> Id -> Bool
- provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta]
Documentation
Term and type constraints to accompany each value vector abstraction. For efficiency, we store the term oracle state instead of the term constraints.
A term constraint. Either equates two variables or a variable with a
PmAltCon
application.
addTmCt :: Delta -> TmCt -> DsM (Maybe Delta) Source #
Tries to equate two representatives in Delta
.
See Note [TmState invariants].
addVarCoreCt :: Delta -> Id -> CoreExpr -> DsM (Maybe Delta) Source #
Records that a variable x
is equal to a CoreExpr
e
.
canDiverge :: Delta -> Id -> Bool Source #
Check whether adding a constraint x ~ BOT
to Delta
succeeds.
provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta] Source #
provideEvidence vs n delta
returns a list of
at most n
(but perhaps empty) refinements of delta
that instantiate
vs
to compatible constructor applications or wildcards.
Negative information is only retained if literals are involved or when
for recursive GADTs.