Safe Haskell	None
Language	Haskell2010

GHC.HsToCore.PmCheck.Oracle

Description

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
- = TmVarVar !Id !Id
- | TmVarCon !Id !PmAltCon ![Id]
- | TmVarNonVoid !Id
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

type DsM = TcRnIf DsGblEnv DsLclEnv Source #

tracePm :: String -> SDoc -> DsM () Source #

mkPmId :: Type -> DsM Id Source #

Generate a fresh Id of a given type

data Delta Source #

Term and type constraints to accompany each value vector abstraction. For efficiency, we store the term oracle state instead of the term constraints.

Instances

Instances details

Outputable Delta Source #
Instance details Defined in GHC.HsToCore.PmCheck.Types Methods ppr :: Delta -> SDoc Source # pprPrec :: Rational -> Delta -> SDoc Source #

initDelta :: Delta Source #

An initial delta that is always satisfiable

lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon] Source #

lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [Id]) Source #

data TmCt Source #

A term constraint. Either equates two variables or a variable with a PmAltCon application.

Constructors

TmVarVar !Id !Id
TmVarCon !Id !PmAltCon ![Id]
TmVarNonVoid !Id

Instances

Instances details

Outputable TmCt Source #
Instance details Defined in GHC.HsToCore.PmCheck.Oracle Methods ppr :: TmCt -> SDoc Source # pprPrec :: Rational -> TmCt -> SDoc Source #

addTypeEvidence :: Delta -> Bag EvVar -> DsM (Maybe Delta) Source #

Add type equalities to Delta.

addRefutableAltCon :: Delta -> Id -> PmAltCon -> DsM (Maybe Delta) Source #

Record that a particular Id can't take the shape of a PmAltCon in the Delta and return Nothing if that leads to a contradiction. See Note [TmState invariants].

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.