| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Constraint.Termination
Description
This module defines code for generating termination constraints.
Synopsis
- data TCheck
- 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)
- 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
Documentation
Constructors
| TerminationCheck | |
| StrataCheck | |
| NoCheck |
makeTermEnvs :: CGEnv -> [(Var, [Located Expr])] -> [(Var, CoreExpr)] -> [SpecType] -> [SpecType] -> [CGEnv] Source #
makeDecrIndex :: (Var, Template SpecType, [Var]) -> CG (Maybe Int) Source #
TERMINATION TYPE ----------------------------------------------------------
checkIndex :: (NamedThing t, PPrint t, PPrint a) => (t, [a], Template (RType c tv r), Maybe Int) -> CG (Maybe (RType c tv r)) Source #
recType :: Symbolic a => HashSet TyCon -> (([a], Maybe Int), (t, Maybe Int, SpecType)) -> SpecType Source #