| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Desugar.TmOracle
- data PmExpr :: *
- data PmLit :: *
- type SimpleEq = (Id, PmExpr)
- type ComplexEq = (PmExpr, PmExpr)
- type PmVarEnv = Map Name PmExpr
- falsePmExpr :: PmExpr
- eqPmLit :: PmLit -> PmLit -> Bool
- filterComplex :: [ComplexEq] -> [PmNegLitCt]
- isNotPmExprOther :: PmExpr -> Bool
- runPmPprM :: PmPprM a -> [PmNegLitCt] -> (a, [(SDoc, [PmLit])])
- lhsExprToPmExpr :: LHsExpr Id -> PmExpr
- hsExprToPmExpr :: HsExpr Id -> PmExpr
- pprPmExprWithParens :: PmExpr -> PmPprM SDoc
- tmOracle :: TmState -> [ComplexEq] -> Maybe TmState
- type TmState = ([ComplexEq], TmOracleEnv)
- initialTmState :: TmState
- solveOneEq :: TmState -> ComplexEq -> Maybe TmState
- extendSubst :: Id -> PmExpr -> TmState -> TmState
- canDiverge :: Name -> TmState -> Bool
- toComplex :: SimpleEq -> ComplexEq
- exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
- pmLitType :: PmLit -> Type
- flattenPmVarEnv :: PmVarEnv -> PmVarEnv
Documentation
Lifted expressions for pattern match checking.
Constructors
| PmExprVar Name | |
| PmExprCon DataCon [PmExpr] | |
| PmExprLit PmLit | |
| PmExprEq PmExpr PmExpr | |
| PmExprOther (HsExpr Id) |
Instances
Literals (simple and overloaded ones) for pattern match checking.
Instances
falsePmExpr :: PmExpr #
Expression False
filterComplex :: [ComplexEq] -> [PmNegLitCt] #
isNotPmExprOther :: PmExpr -> Bool #
Check if an expression is lifted or not
lhsExprToPmExpr :: LHsExpr Id -> PmExpr #
hsExprToPmExpr :: HsExpr Id -> PmExpr #
pprPmExprWithParens :: PmExpr -> PmPprM SDoc #
type TmState = ([ComplexEq], TmOracleEnv) Source #
The state of the term oracle (includes complex constraints that cannot progress unless we get more information).
initialTmState :: TmState Source #
Initial state of the oracle.
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.
exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr Source #
Apply an (un-flattened) substitution to an expression.
flattenPmVarEnv :: PmVarEnv -> PmVarEnv Source #
Flatten the DAG (Could be improved in terms of performance.).