ghc-9.0.1: The GHC API
Safe HaskellNone
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.