Safe Haskell	None
Language	Haskell2010

GHC.HsToCore.PmCheck.Oracle

Description

The pattern match oracle. The main export of the module are the functions addPmCts 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
initDeltas :: Deltas
lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon]
lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [TyVar], [Id])
data PmCt = PmTyCt !TyCt
type PmCts = Bag PmCt
pattern PmVarCt :: Id -> Id -> PmCt
pattern PmCoreCt :: Id -> CoreExpr -> PmCt
pattern PmConCt :: Id -> PmAltCon -> [TyVar] -> [Id] -> PmCt
pattern PmNotConCt :: Id -> PmAltCon -> PmCt
pattern PmBotCt :: Id -> PmCt
pattern PmNotBotCt :: Id -> PmCt
addPmCts :: Delta -> PmCts -> 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 #

An inert set of canonical (i.e. mutually compatible) term and type constraints.

Instances

Instances details

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

initDeltas :: Deltas Source #

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

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

data PmCt Source #

An oracle constraint.

Constructors

PmTyCt !TyCt

PmTy pred_ty carries PredTypes, for example equality constraints.

Instances

Instances details

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

type PmCts = Bag PmCt Source #

pattern PmVarCt :: Id -> Id -> PmCt Source #

pattern PmCoreCt :: Id -> CoreExpr -> PmCt Source #

pattern PmConCt :: Id -> PmAltCon -> [TyVar] -> [Id] -> PmCt Source #

pattern PmNotConCt :: Id -> PmAltCon -> PmCt Source #

pattern PmBotCt :: Id -> PmCt Source #

pattern PmNotBotCt :: Id -> PmCt Source #

addPmCts :: Delta -> PmCts -> DsM (Maybe Delta) Source #

Adds new constraints to Delta and returns Nothing if that leads to a contradiction.

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.