Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- data PmLit
- 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
Lifted expressions for pattern match checking.
Literals (simple and overloaded ones) for pattern match checking.
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
.
A term constraint. TVC x e
encodes that x
is equal to e
.
type TmVarCtEnv = NameEnv PmExpr Source #
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.
isNotPmExprOther :: PmExpr -> Bool #
Check if an expression is lifted or not
lhsExprToPmExpr :: LHsExpr GhcTc -> PmExpr #
hsExprToPmExpr :: HsExpr GhcTc -> PmExpr #
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].
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
.
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
.
exprDeepLookup :: TmVarCtEnv -> PmExpr -> PmExpr Source #
Apply an (un-flattened) substitution to an expression.