ghc-9.0.2: The GHC API
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

Documentation

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

mkPmId :: Type -> DsM Id #

Generate a fresh Id of a given type

data Delta #

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 #

pprPrec :: Rational -> Delta -> SDoc #

data PmCt #

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 #

pprPrec :: Rational -> PmCt -> SDoc #

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) #

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

canDiverge :: Delta -> Id -> Bool #

Check whether adding a constraint x ~ BOT to Delta succeeds.

provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta] #

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.