Safe Haskell	None
Language	Haskell2010

TmOracle

Description

The term equality oracle. The main export of the module are the functions tmOracle, solveOneEq and addSolveRefutableAltCon.

If you are looking for an oracle that can solve type-level constraints, look at tcCheckSatisfiability.

Synopsis

data PmExpr
- = PmExprVar Name
- | PmExprCon ConLike [PmExpr]
- | PmExprLit PmLit
- | PmExprOther (HsExpr GhcTc)
data PmLit
- = PmSLit (HsLit GhcTc)
- | PmOLit Bool (HsOverLit GhcTc)
newtype PmAltCon = PmAltLit PmLit
data TmVarCt = TVC !Id !PmExpr
type TmVarCtEnv = NameEnv PmExpr
type PmRefutEnv = DNameEnv [PmAltCon]
eqPmLit :: PmLit -> PmLit -> Bool
isNotPmExprOther :: PmExpr -> Bool
lhsExprToPmExpr :: LHsExpr GhcTc -> PmExpr
hsExprToPmExpr :: HsExpr GhcTc -> PmExpr
tmOracle :: TmState -> [TmVarCt] -> Maybe TmState
data TmState
initialTmState :: TmState
wrapUpTmState :: TmState -> (TmVarCtEnv, PmRefutEnv)
solveOneEq :: TmState -> TmVarCt -> Maybe TmState
extendSubst :: Id -> PmExpr -> TmState -> TmState
canDiverge :: Name -> TmState -> Bool
isRigid :: TmState -> Name -> Maybe PmExpr
addSolveRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState
lookupRefutableAltCons :: Id -> TmState -> [PmAltCon]
exprDeepLookup :: TmVarCtEnv -> PmExpr -> PmExpr
pmLitType :: PmLit -> Type

Documentation

data PmExpr #

Lifted expressions for pattern match checking.

Constructors

PmExprVar Name
PmExprCon ConLike [PmExpr]
PmExprLit PmLit
PmExprOther (HsExpr GhcTc)

Instances

Outputable PmExpr
Instance details 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
Instance details Defined in PmExpr Methods ppr :: PmLit -> SDoc # pprPrec :: Rational -> PmLit -> SDoc #

newtype PmAltCon #

Represents a match against a literal. We mostly use it to to encode shapes for a variable that immediately lead to a refutation.

See Note [Refutable shapes] in TmOracle. Really similar to AltCon.

Constructors

PmAltLit PmLit

Instances

Eq PmAltCon
Instance details Defined in PmExpr Methods (==) :: PmAltCon -> PmAltCon -> Bool # (/=) :: PmAltCon -> PmAltCon -> Bool #
Outputable PmAltCon
Instance details Defined in PmExpr Methods ppr :: PmAltCon -> SDoc # pprPrec :: Rational -> PmAltCon -> SDoc #

data TmVarCt #

A term constraint. TVC x e encodes that x is equal to e.

Constructors

TVC !Id !PmExpr

Instances

Outputable TmVarCt
Instance details Defined in PmExpr Methods ppr :: TmVarCt -> SDoc # pprPrec :: Rational -> TmVarCt -> SDoc #

type TmVarCtEnv = NameEnv PmExpr Source #

Pretty much a [TmVarCt] association list where the domain is Name instead of Id. This is the type of tm_pos, where we store solutions for rigid pattern match variables.

type PmRefutEnv = DNameEnv [PmAltCon] Source #

An environment assigning shapes to variables that immediately lead to a refutation. So, if this maps x :-> [3], then trying to solve a TmVarCt like x ~ 3 immediately leads to a contradiction. Determinism is important since we use this for warning messages in pprUncovered. We don't do the same for TmVarCtEnv, so that is a plain NameEnv.

See also Note [Refutable shapes] in TmOracle.

eqPmLit :: PmLit -> PmLit -> Bool #

Equality between literals for pattern match checking.

isNotPmExprOther :: PmExpr -> Bool #

Check if an expression is lifted or not

lhsExprToPmExpr :: LHsExpr GhcTc -> PmExpr #

hsExprToPmExpr :: HsExpr GhcTc -> PmExpr #

tmOracle :: TmState -> [TmVarCt] -> Maybe TmState Source #

External interface to the term oracle.

data TmState Source #

The state of the term oracle. Tracks all term-level facts of the form "x is True" (tm_pos) and "x is not 5" (tm_neg).

Subject to Note [The Pos/Neg invariant].

Instances

Outputable TmState Source #
Instance details Defined in TmOracle Methods ppr :: TmState -> SDoc # pprPrec :: Rational -> TmState -> SDoc #

initialTmState :: TmState Source #

Initial state of the oracle.

wrapUpTmState :: TmState -> (TmVarCtEnv, PmRefutEnv) Source #

Wrap up the term oracle's state once solving is complete. Return the flattened tm_pos and tm_neg.

solveOneEq :: TmState -> TmVarCt -> Maybe TmState Source #

Solve an equality (top-level).

extendSubst :: Id -> PmExpr -> TmState -> TmState Source #

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

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

isRigid :: TmState -> Name -> Maybe PmExpr Source #

Is the given variable rigid (i.e., we have a solution for it) or flexible (i.e., no solution)? Returns the solution if rigid. A semantically helpful alias for lookupNameEnv.

addSolveRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState Source #

Record that a particular Id can't take the shape of a PmAltCon in the TmState and return Nothing if that leads to a contradiction.

lookupRefutableAltCons :: Id -> TmState -> [PmAltCon] Source #

Return all PmAltCon shapes that are impossible for Id to take, i.e. would immediately lead to a refutation by the term oracle.

exprDeepLookup :: TmVarCtEnv -> PmExpr -> PmExpr Source #

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

pmLitType :: PmLit -> Type Source #

Type of a PmLit