Language.Haskell.Liquid.Constraint.Termination

This module defines code for generating termination constraints.

Documentation

data TCheck

Constructors

TerminationCheck

StrataCheck

NoCheck

mkTCheck :: Bool -> Bool -> TCheck

doTermCheck :: Config -> Bind Var -> CG Bool

makeTermEnvs :: CGEnv -> [(Var, [Located Expr])] -> [(Var, CoreExpr)] -> [SpecType] -> [SpecType] -> [CGEnv]

makeDecrIndex :: (Var, Template SpecType, [Var]) -> CG (Maybe Int)

TERMINATION TYPE ----------------------------------------------------------

checkIndex :: (NamedThing t, PPrint t, PPrint a) => (t, [a], Template (RType c tv r), Maybe Int) -> CG (Maybe (RType c tv r))

recType :: Symbolic a => HashSet TyCon -> (([a], Maybe Int), (t, Maybe Int, SpecType)) -> SpecType

unOCons :: RType c tv r -> RType c tv r

consCBSizedTys :: (Bool -> CGEnv -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType)) -> CGEnv -> [(Var, CoreExpr)] -> CG CGEnv

consCBWithExprs :: (Bool -> CGEnv -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType)) -> CGEnv -> [(Var, CoreExpr)] -> CG CGEnv