liquidhaskell-0.8.0.2: Liquid Types for Haskell

Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Desugar.TmOracle

Synopsis

Documentation

data PmExpr :: * #

Lifted expressions for pattern match checking.

Instances

data PmLit :: * #

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

Constructors

PmSLit HsLit 
PmOLit Bool (HsOverLit Id) 

Instances

type SimpleEq = (Id, PmExpr) #

Term equalities

type PmVarEnv = Map Name PmExpr Source #

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])]) #

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

External interface to the term oracle.

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.

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

Solve a complex 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.

exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr Source #

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

pmLitType :: PmLit -> Type Source #

Type of a PmLit

flattenPmVarEnv :: PmVarEnv -> PmVarEnv Source #

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