TmOracle

Documentation

data PmExpr

Lifted expressions for pattern match checking.

Constructors

PmExprVar Name

PmExprCon ConLike [PmExpr]

PmExprLit PmLit

PmExprEq PmExpr PmExpr

PmExprOther (HsExpr GhcTc)

Instances

Outputable PmExpr

Defined in PmExpr

Methods

ppr :: PmExpr -> SDoc

pprPrec :: Rational -> PmExpr -> SDoc

data PmLit

Literals (simple and overloaded ones) for pattern match checking.

Constructors

PmSLit (HsLit GhcTc)

PmOLit Bool (HsOverLit GhcTc)

Instances

Outputable PmLit

Defined in PmExpr

Methods

ppr :: PmLit -> SDoc

pprPrec :: Rational -> PmLit -> SDoc

type SimpleEq = (Id, PmExpr)

Term equalities

type ComplexEq = (PmExpr, PmExpr)

type PmVarEnv = NameEnv PmExpr

The type of substitutions.

falsePmExpr :: PmExpr

Expression False

eqPmLit :: PmLit -> PmLit -> Bool

Equality between literals for pattern match checking.

filterComplex :: [ComplexEq] -> [PmNegLitCt]

isNotPmExprOther :: PmExpr -> Bool

Check if an expression is lifted or not

runPmPprM :: PmPprM a -> [PmNegLitCt] -> (a, [(SDoc, [PmLit])])

lhsExprToPmExpr :: LHsExpr GhcTc -> PmExpr

hsExprToPmExpr :: HsExpr GhcTc -> PmExpr

pprPmExprWithParens :: PmExpr -> PmPprM SDoc

tmOracle :: TmState -> [ComplexEq] -> Maybe TmState

External interface to the term oracle.

type TmState = ([ComplexEq], TmOracleEnv)

The state of the term oracle (includes complex constraints that cannot progress unless we get more information).

initialTmState :: TmState

Initial state of the oracle.

solveOneEq :: TmState -> ComplexEq -> Maybe TmState

Solve a complex equality (top-level).

extendSubst :: Id -> PmExpr -> TmState -> TmState

When we know that a variable is fresh, we do not actually have to check whether anything changes, we know that nothing does. Hence, extendSubst simply extends the substitution, unlike what extendSubstAndSolve does.

canDiverge :: Name -> TmState -> Bool

Check whether a constraint (x ~ BOT) can succeed, given the resulting state of the term oracle.

toComplex :: SimpleEq -> ComplexEq

Lift a SimpleEq to a ComplexEq

exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr

Apply an (un-flattened) substitution to an expression.

pmLitType :: PmLit -> Type

Type of a PmLit

flattenPmVarEnv :: PmVarEnv -> PmVarEnv

Flatten the DAG (Could be improved in terms of performance.).