| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Termination.Monad
Description
The monad for the termination checker.
The termination monad TerM is an extension of
the type checking monad TCM by an environment
with information needed by the termination checker.
Synopsis
- data Target
- type Guarded = Order
- data TerEnv = TerEnv {
- terUseDotPatterns :: Bool
- terSizeSuc :: Maybe QName
- terSharp :: Maybe QName
- terCutOff :: CutOff
- terCurrent :: QName
- terMutual :: MutualNames
- terUserNames :: Set QName
- terHaveInlinedWith :: Bool
- terTarget :: Target
- terMaskArgs :: [Bool]
- terMaskResult :: Bool
- _terSizeDepth :: Int
- terPatterns :: MaskedDeBruijnPatterns
- terPatternsRaise :: !Int
- terGuarded :: !Guarded
- terUseSizeLt :: Bool
- terUsableVars :: VarSet
- defaultTerEnv :: TerEnv
- class (Functor m, Monad m) => MonadTer (m :: Type -> Type) where
- newtype TerM a = TerM {}
- runTer :: TerEnv -> TerM a -> TCM a
- runTerDefault :: TerM a -> TCM a
- terGetUseDotPatterns :: TerM Bool
- terSetUseDotPatterns :: Bool -> TerM a -> TerM a
- terGetSizeSuc :: TerM (Maybe QName)
- terGetCurrent :: TerM QName
- terSetCurrent :: QName -> TerM a -> TerM a
- terGetSharp :: TerM (Maybe QName)
- terGetCutOff :: TerM CutOff
- terGetMutual :: TerM MutualNames
- terGetUserNames :: TerM (Set QName)
- terGetTarget :: TerM Target
- terSetTarget :: Target -> TerM a -> TerM a
- terGetHaveInlinedWith :: TerM Bool
- terSetHaveInlinedWith :: TerM a -> TerM a
- terGetMaskArgs :: TerM [Bool]
- terSetMaskArgs :: [Bool] -> TerM a -> TerM a
- terGetMaskResult :: TerM Bool
- terSetMaskResult :: Bool -> TerM a -> TerM a
- terGetPatterns :: TerM MaskedDeBruijnPatterns
- terSetPatterns :: MaskedDeBruijnPatterns -> TerM a -> TerM a
- terRaise :: TerM a -> TerM a
- terGetGuarded :: TerM Guarded
- terModifyGuarded :: (Order -> Order) -> TerM a -> TerM a
- terSetGuarded :: Order -> TerM a -> TerM a
- terUnguarded :: TerM a -> TerM a
- terSizeDepth :: Lens' TerEnv Int
- terGetUsableVars :: TerM VarSet
- terModifyUsableVars :: (VarSet -> VarSet) -> TerM a -> TerM a
- terSetUsableVars :: VarSet -> TerM a -> TerM a
- terGetUseSizeLt :: TerM Bool
- terModifyUseSizeLt :: (Bool -> Bool) -> TerM a -> TerM a
- terSetUseSizeLt :: Bool -> TerM a -> TerM a
- withUsableVars :: UsableSizeVars a => a -> TerM b -> TerM b
- conUseSizeLt :: QName -> TerM a -> TerM a
- projUseSizeLt :: QName -> TerM a -> TerM a
- isProjectionButNotCoinductive :: MonadTCM tcm => QName -> tcm Bool
- isCoinductiveProjection :: MonadTCM tcm => Bool -> QName -> tcm Bool
- patternDepth :: Pattern' a -> Int
- unusedVar :: DeBruijnPattern
- class UsableSizeVars a where
- usableSizeVars :: a -> TerM VarSet
- type MaskedDeBruijnPatterns = [Masked DeBruijnPattern]
- data Masked a = Masked {}
- masked :: a -> Masked a
- notMasked :: a -> Masked a
- newtype CallPath = CallPath (DList CallInfo)
- callInfos :: CallPath -> [CallInfo]
- class TerSetSizeDepth b where
- terSetSizeDepth :: b -> TerM a -> TerM a
Documentation
The target of the function we are checking.
Constructors
| TargetDef QName | The target of recursion is a |
| TargetRecord | We are termination-checking a record. |
| TargetOther | None of the above two or unknown. |
The termination environment.
Constructors
| TerEnv | |
Fields
| |
defaultTerEnv :: TerEnv Source #
An empty termination environment.
Values are set to a safe default meaning that with these initial values the termination checker will not miss termination errors it would have seen with better settings of these values.
Values that do not have a safe default are set to
IMPOSSIBLE.
class (Functor m, Monad m) => MonadTer (m :: Type -> Type) where Source #
Termination monad service class.
Termination monad.
Instances
runTerDefault :: TerM a -> TCM a Source #
Run TerM computation in default environment (created from options).
Modifiers and accessors for the termination environment in the monad.
terSetHaveInlinedWith :: TerM a -> TerM a Source #
terGetMaskArgs :: TerM [Bool] Source #
terSetPatterns :: MaskedDeBruijnPatterns -> TerM a -> TerM a Source #
terUnguarded :: TerM a -> TerM a Source #
terSizeDepth :: Lens' TerEnv Int Source #
Lens for _terSizeDepth.
terGetUsableVars :: TerM VarSet Source #
Lens for terUsableVars.
terGetUseSizeLt :: TerM Bool Source #
Lens for terUseSizeLt.
withUsableVars :: UsableSizeVars a => a -> TerM b -> TerM b Source #
Compute usable vars from patterns and run subcomputation.
conUseSizeLt :: QName -> TerM a -> TerM a Source #
Set terUseSizeLt when going under constructor c.
projUseSizeLt :: QName -> TerM a -> TerM a Source #
Set terUseSizeLt for arguments following projection q.
We disregard j<i after a non-coinductive projection.
However, the projection need not be recursive (Issue 1470).
isProjectionButNotCoinductive :: MonadTCM tcm => QName -> tcm Bool Source #
For termination checking purposes flat should not be considered a projection. That is, it flat doesn't preserve either structural order or guardedness like other projections do. Andreas, 2012-06-09: the same applies to projections of recursive records.
isCoinductiveProjection :: MonadTCM tcm => Bool -> QName -> tcm Bool Source #
Check whether a projection belongs to a coinductive record and is actually recursive. E.g. @ isCoinductiveProjection (Stream.head) = return False
isCoinductiveProjection (Stream.tail) = return True @
De Bruijn pattern stuff
patternDepth :: Pattern' a -> Int Source #
How long is the path to the deepest atomic pattern?
unusedVar :: DeBruijnPattern Source #
A dummy pattern used to mask a pattern that cannot be used for structural descent.
class UsableSizeVars a where Source #
Extract variables from DeBruijnPatterns that could witness a decrease
via a SIZELT constraint.
These variables must be under an inductive constructor (with no record constructor in the way), or after a coinductive projection (with no inductive one in the way).
Methods
usableSizeVars :: a -> TerM VarSet Source #
Instances
| UsableSizeVars DeBruijnPattern Source # | |
Defined in Agda.Termination.Monad Methods | |
| UsableSizeVars MaskedDeBruijnPatterns Source # | |
Defined in Agda.Termination.Monad Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source # | |
| UsableSizeVars (Masked DeBruijnPattern) Source # | |
Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source # | |
| UsableSizeVars [DeBruijnPattern] Source # | |
Defined in Agda.Termination.Monad Methods usableSizeVars :: [DeBruijnPattern] -> TerM VarSet Source # | |
Masked patterns (which are not eligible for structural descent, only for size descent)
type MaskedDeBruijnPatterns = [Masked DeBruijnPattern] Source #
Constructors
| Masked | |
Instances
| UsableSizeVars MaskedDeBruijnPatterns Source # | |
Defined in Agda.Termination.Monad Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source # | |
| Decoration Masked Source # | |
| Foldable Masked Source # | |
Defined in Agda.Termination.Monad Methods fold :: Monoid m => Masked m -> m # foldMap :: Monoid m => (a -> m) -> Masked a -> m # foldMap' :: Monoid m => (a -> m) -> Masked a -> m # foldr :: (a -> b -> b) -> b -> Masked a -> b # foldr' :: (a -> b -> b) -> b -> Masked a -> b # foldl :: (b -> a -> b) -> b -> Masked a -> b # foldl' :: (b -> a -> b) -> b -> Masked a -> b # foldr1 :: (a -> a -> a) -> Masked a -> a # foldl1 :: (a -> a -> a) -> Masked a -> a # elem :: Eq a => a -> Masked a -> Bool # maximum :: Ord a => Masked a -> a # minimum :: Ord a => Masked a -> a # | |
| Traversable Masked Source # | |
| Functor Masked Source # | |
| UsableSizeVars (Masked DeBruijnPattern) Source # | |
Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source # | |
| PrettyTCM a => PrettyTCM (Masked a) Source # | Print masked things in double parentheses. |
Defined in Agda.Termination.Monad | |
| Show a => Show (Masked a) Source # | |
| Eq a => Eq (Masked a) Source # | |
| Ord a => Ord (Masked a) Source # | |
Defined in Agda.Termination.Monad | |
Call pathes
Call paths.
Size depth estimation
class TerSetSizeDepth b where Source #
A very crude way of estimating the SIZELT chains
i > j > k in context. Returns 3 in this case.
Overapproximates.
Methods
terSetSizeDepth :: b -> TerM a -> TerM a Source #
Instances
| TerSetSizeDepth ListTel Source # | |
Defined in Agda.Termination.Monad | |
| TerSetSizeDepth Telescope Source # | |
Defined in Agda.Termination.Monad | |