| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Termination.Monad
Contents
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
- type MutualNames = [QName]
- type Target = QName
- type Guarded = Order
- data TerEnv = TerEnv {
- terUseDotPatterns :: Bool
- terGuardingTypeConstructors :: Bool
- terInlineWithFunctions :: Bool
- terSizeSuc :: Maybe QName
- terSharp :: Maybe QName
- terCutOff :: CutOff
- terCurrent :: QName
- terMutual :: MutualNames
- terUserNames :: [QName]
- terHaveInlinedWith :: Bool
- terTarget :: Maybe Target
- terDelayed :: Delayed
- 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 where
- newtype TerM a = TerM {}
- runTer :: TerEnv -> TerM a -> TCM a
- runTerDefault :: TerM a -> TCM a
- terGetGuardingTypeConstructors :: TerM Bool
- terGetInlineWithFunctions :: TerM Bool
- 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 [QName]
- terGetTarget :: TerM (Maybe Target)
- terSetTarget :: Maybe Target -> TerM a -> TerM a
- terGetHaveInlinedWith :: TerM Bool
- terSetHaveInlinedWith :: TerM a -> TerM a
- terGetDelayed :: TerM Delayed
- terSetDelayed :: Delayed -> 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
- terPiGuarded :: TerM a -> TerM a
- terSizeDepth :: Lens' Int TerEnv
- 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 :: forall a. Pattern' a -> Int
- unusedVar :: DeBruijnPattern
- class UsableSizeVars a where
- type MaskedDeBruijnPatterns = [Masked DeBruijnPattern]
- data Masked a = Masked {}
- masked :: a -> Masked a
- notMasked :: a -> Masked a
- newtype CallPath = CallPath {}
- terSetSizeDepth :: Telescope -> TerM a -> TerM a
Documentation
type MutualNames = [QName] #
The mutual block we are checking.
The functions are numbered according to their order of appearance in this list.
The termination environment.
Constructors
| TerEnv | |
Fields
| |
defaultTerEnv :: TerEnv #
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 where #
Termination monad service class.
Termination monad.
Instances
| Monad TerM # | |
| Functor TerM # | |
| Applicative TerM # | |
| MonadIO TerM # | |
Defined in Agda.Termination.Monad | |
| MonadTCM TerM # | |
Defined in Agda.Termination.Monad | |
| HasOptions TerM # | |
Defined in Agda.Termination.Monad | |
| MonadDebug TerM # | |
Defined in Agda.Termination.Monad Methods displayDebugMessage :: Int -> String -> TerM () # traceDebugMessage :: Int -> String -> TerM a -> TerM a # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> TerM String # | |
| HasConstInfo TerM # | |
Defined in Agda.Termination.Monad Methods getConstInfo :: QName -> TerM Definition # getConstInfo' :: QName -> TerM (Either SigError Definition) # getRewriteRulesFor :: QName -> TerM RewriteRules # | |
| MonadTer TerM # | |
| MonadState TCState TerM # | |
| MonadReader TCEnv TerM # | |
| MonadError TCErr TerM # | |
Defined in Agda.Termination.Monad | |
| MonadBench Phase TerM # | |
| Semigroup m => Semigroup (TerM m) # | |
| (Semigroup m, Monoid m) => Monoid (TerM m) # | |
runTerDefault :: TerM a -> TCM a #
Run TerM computation in default environment (created from options).
Termination monad is a MonadTCM.
Modifiers and accessors for the termination environment in the monad.
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 #
terGetUserNames :: TerM [QName] #
terGetTarget :: TerM (Maybe Target) #
terSetHaveInlinedWith :: TerM a -> TerM a #
terSetDelayed :: Delayed -> TerM a -> TerM a #
terGetMaskArgs :: TerM [Bool] #
terSetMaskArgs :: [Bool] -> TerM a -> TerM a #
terSetMaskResult :: Bool -> TerM a -> TerM a #
terSetPatterns :: MaskedDeBruijnPatterns -> TerM a -> TerM a #
terSetGuarded :: Order -> TerM a -> TerM a #
terUnguarded :: TerM a -> TerM a #
terPiGuarded :: TerM a -> TerM a #
Should the codomain part of a function type preserve guardedness?
terSizeDepth :: Lens' Int TerEnv #
Lens for _terSizeDepth.
terGetUsableVars :: TerM VarSet #
Lens for terUsableVars.
terSetUsableVars :: VarSet -> TerM a -> TerM a #
terGetUseSizeLt :: TerM Bool #
Lens for terUseSizeLt.
terSetUseSizeLt :: Bool -> TerM a -> TerM a #
withUsableVars :: UsableSizeVars a => a -> TerM b -> TerM b #
Compute usable vars from patterns and run subcomputation.
conUseSizeLt :: QName -> TerM a -> TerM a #
Set terUseSizeLt when going under constructor c.
projUseSizeLt :: QName -> TerM a -> TerM a #
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 #
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 #
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 :: forall a. Pattern' a -> Int #
How long is the path to the deepest atomic pattern?
unusedVar :: DeBruijnPattern #
A dummy pattern used to mask a pattern that cannot be used for structural descent.
class UsableSizeVars a where #
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).
Minimal complete definition
Methods
usableSizeVars :: a -> TerM VarSet #
Instances
| UsableSizeVars DeBruijnPattern # | |
Defined in Agda.Termination.Monad Methods usableSizeVars :: DeBruijnPattern -> TerM VarSet # | |
| UsableSizeVars MaskedDeBruijnPatterns # | |
Defined in Agda.Termination.Monad Methods | |
| UsableSizeVars [DeBruijnPattern] # | |
Defined in Agda.Termination.Monad Methods usableSizeVars :: [DeBruijnPattern] -> TerM VarSet # | |
| UsableSizeVars (Masked DeBruijnPattern) # | |
Defined in Agda.Termination.Monad Methods | |
Masked patterns (which are not eligible for structural descent, only for size descent)
type MaskedDeBruijnPatterns = [Masked DeBruijnPattern] #
Constructors
| Masked | |
Instances
| Functor Masked # | |
| Foldable Masked # | |
Defined in Agda.Termination.Monad Methods fold :: Monoid m => Masked m -> 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 # | |
| Decoration Masked # | |
| UsableSizeVars MaskedDeBruijnPatterns # | |
Defined in Agda.Termination.Monad Methods | |
| Eq a => Eq (Masked a) # | |
| Ord a => Ord (Masked a) # | |
Defined in Agda.Termination.Monad | |
| Show a => Show (Masked a) # | |
| PrettyTCM a => PrettyTCM (Masked a) # | Print masked things in double parentheses. |
| UsableSizeVars (Masked DeBruijnPattern) # | |
Defined in Agda.Termination.Monad Methods | |
Call pathes
The call information is stored as free monoid
over CallInfo. As long as we never look at it,
only accumulate it, it does not matter whether we use
Set, (nub) list, or Tree.
Internally, due to lazyness, it is anyway a binary tree of
mappend nodes and singleton leafs.
Since we define no order on CallInfo (expensive),
we cannot use a Set or nub list.
Performance-wise, I could not see a difference between Set and list.
Size depth estimation
terSetSizeDepth :: Telescope -> TerM a -> TerM a #
A very crude way of estimating the SIZELT chains
i > j > k in context. Returns 3 in this case.
Overapproximates.