Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Termination.Monad

Contents

Modifiers and accessors for the termination environment in the monad.
De Bruijn pattern stuff
Masked patterns (which are not eligible for structural descent, only for size descent)
Call pathes
Size depth estimation

Description

The monad for the termination checker.

The termination monad TerM is an extension of the type checking monad TCMT by an environment with information needed by the termination checker.

Synopsis

data Target
- = TargetDef QName
- | TargetRecord
- | TargetOther
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 where
- terAsk :: m TerEnv
- terLocal :: (TerEnv -> TerEnv) -> m a -> m a
- terAsks :: (TerEnv -> a) -> m a
newtype TerM a = TerM {
- terM :: ReaderT TerEnv TCM a
}
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 :: forall a. Pattern' a -> Int
unusedVar :: DeBruijnPattern
class UsableSizeVars a where
- usableSizeVars :: a -> TerM VarSet
type MaskedDeBruijnPatterns = [Masked DeBruijnPattern]
data Masked a = Masked {
- getMask :: Bool
- getMasked :: a
}
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

data Target Source #

The target of the function we are checking.

Constructors

TargetDef QName	The target of recursion is a `record`, `data`, or unreducible `Def`.
TargetRecord	We are termination-checking a record.
TargetOther	None of the above two or unknown.

Instances

Instances details

Show Target Source #
Instance details Defined in Agda.Termination.Monad Methods showsPrec :: Int -> Target -> ShowS show :: Target -> String showList :: [Target] -> ShowS
Eq Target Source #
Instance details Defined in Agda.Termination.Monad Methods (==) :: Target -> Target -> Bool (/=) :: Target -> Target -> Bool

type Guarded = Order Source #

The current guardedness level.

data TerEnv Source #

The termination environment.

Constructors

TerEnv

Fields

terUseDotPatterns :: Bool
Are we mining dot patterns to find evindence of structal descent?
terSizeSuc :: Maybe QName
The name of size successor, if any.
terSharp :: Maybe QName
The name of the delay constructor (sharp), if any.
terCutOff :: CutOff
Depth at which to cut off the structural order.
terCurrent :: QName
The name of the function we are currently checking.
terMutual :: MutualNames
The names of the functions in the mutual block we are checking. This includes the internally generated functions (with, extendedlambda, coinduction).
terUserNames :: Set QName
The list of name actually appearing in the file (abstract syntax). Excludes the internally generated functions.
terHaveInlinedWith :: Bool
Does the actual clause result from with-inlining? (If yes, it may be ill-typed.)
terTarget :: Target
Target type of the function we are currently termination checking. Only the constructors of Target are considered guarding.
terMaskArgs :: [Bool]
Only consider the notMasked False arguments for establishing termination. See issue #1023.
terMaskResult :: Bool
Only consider guardedness if False (not masked).
_terSizeDepth :: Int
How many SIZELT relations do we have in the context (= clause telescope). Used to approximate termination for metas in call args.
terPatterns :: MaskedDeBruijnPatterns
The patterns of the clause we are checking.
terPatternsRaise :: !Int
Number of additional binders we have gone under (and consequently need to raise the patterns to compare to terms). Updated during call graph extraction, hence strict.
terGuarded :: !Guarded
The current guardedness status. Changes as we go deeper into the term. Updated during call graph extraction, hence strict.
terUseSizeLt :: Bool
When extracting usable size variables during construction of the call matrix, can we take the variable for use with SIZELT constraints from the context? Yes, if we are under an inductive constructor. No, if we are under a record constructor. (See issue #1015).
terUsableVars :: VarSet
Pattern variables that can be compared to argument variables using SIZELT.

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 where Source #

Termination monad service class.

Minimal complete definition

terAsk, terLocal

Methods

terAsk :: m TerEnv Source #

terLocal :: (TerEnv -> TerEnv) -> m a -> m a Source #

terAsks :: (TerEnv -> a) -> m a Source #

Instances

Instances details

MonadTer TerM Source #
Instance details Defined in Agda.Termination.Monad Methods terAsk :: TerM TerEnv Source # terLocal :: (TerEnv -> TerEnv) -> TerM a -> TerM a Source # terAsks :: (TerEnv -> a) -> TerM a Source #

newtype TerM a Source #

Termination monad.

Constructors

TerM
Fields terM :: ReaderT TerEnv TCM a

Instances

Instances details

HasOptions TerM Source #
Instance details Defined in Agda.Termination.Monad Methods pragmaOptions :: TerM PragmaOptions Source # commandLineOptions :: TerM CommandLineOptions Source #
MonadTer TerM Source #
Instance details Defined in Agda.Termination.Monad Methods terAsk :: TerM TerEnv Source # terLocal :: (TerEnv -> TerEnv) -> TerM a -> TerM a Source # terAsks :: (TerEnv -> a) -> TerM a Source #
MonadReduce TerM Source #
Instance details Defined in Agda.Termination.Monad Methods liftReduce :: ReduceM a -> TerM a Source #
MonadTCEnv TerM Source #
Instance details Defined in Agda.Termination.Monad Methods askTC :: TerM TCEnv Source # localTC :: (TCEnv -> TCEnv) -> TerM a -> TerM a Source #
MonadTCM TerM Source #
Instance details Defined in Agda.Termination.Monad Methods liftTCM :: TCM a -> TerM a Source #
MonadTCState TerM Source #
Instance details Defined in Agda.Termination.Monad Methods getTC :: TerM TCState Source # putTC :: TCState -> TerM () Source # modifyTC :: (TCState -> TCState) -> TerM () Source #
ReadTCState TerM Source #
Instance details Defined in Agda.Termination.Monad Methods getTCState :: TerM TCState Source # locallyTCState :: Lens' TCState a -> (a -> a) -> TerM b -> TerM b Source # withTCState :: (TCState -> TCState) -> TerM a -> TerM a Source #
HasBuiltins TerM Source #
Instance details Defined in Agda.Termination.Monad Methods getBuiltinThing :: SomeBuiltin -> TerM (Maybe (Builtin PrimFun)) Source #
MonadAddContext TerM Source #
Instance details Defined in Agda.Termination.Monad Methods addCtx :: Name -> Dom Type -> TerM a -> TerM a Source # addLetBinding' :: Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a Source # updateContext :: Substitution -> (Context -> Context) -> TerM a -> TerM a Source # withFreshName :: Range -> ArgName -> (Name -> TerM a) -> TerM a Source #
MonadDebug TerM Source #
Instance details Defined in Agda.Termination.Monad Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> TerM String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> TerM a -> TerM a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> TerM a -> TerM a Source # getVerbosity :: TerM Verbosity Source # getProfileOptions :: TerM ProfileOptions Source # isDebugPrinting :: TerM Bool Source # nowDebugPrinting :: TerM a -> TerM a Source #
PureTCM TerM Source #
Instance details Defined in Agda.Termination.Monad
HasConstInfo TerM Source #
Instance details Defined in Agda.Termination.Monad Methods getConstInfo :: QName -> TerM Definition Source # getConstInfo' :: QName -> TerM (Either SigError Definition) Source # getRewriteRulesFor :: QName -> TerM RewriteRules Source #
MonadStatistics TerM Source #
Instance details Defined in Agda.Termination.Monad Methods modifyCounter :: String -> (Integer -> Integer) -> TerM () Source #
MonadBench TerM Source #
Instance details Defined in Agda.Termination.Monad Associated Types type BenchPhase TerM Source # Methods getBenchmark :: TerM (Benchmark (BenchPhase TerM)) Source # putBenchmark :: Benchmark (BenchPhase TerM) -> TerM () Source # modifyBenchmark :: (Benchmark (BenchPhase TerM) -> Benchmark (BenchPhase TerM)) -> TerM () Source # finally :: TerM b -> TerM c -> TerM b Source #
MonadFail TerM Source #
Instance details Defined in Agda.Termination.Monad Methods fail :: String -> TerM a
MonadIO TerM Source #
Instance details Defined in Agda.Termination.Monad Methods liftIO :: IO a -> TerM a
Applicative TerM Source #
Instance details Defined in Agda.Termination.Monad Methods pure :: a -> TerM a (<>) :: TerM (a -> b) -> TerM a -> TerM b # liftA2 :: (a -> b -> c) -> TerM a -> TerM b -> TerM c (>) :: TerM a -> TerM b -> TerM b (<*) :: TerM a -> TerM b -> TerM a
Functor TerM Source #
Instance details Defined in Agda.Termination.Monad Methods fmap :: (a -> b) -> TerM a -> TerM b (<$) :: a -> TerM b -> TerM a #
Monad TerM Source #
Instance details Defined in Agda.Termination.Monad Methods (>>=) :: TerM a -> (a -> TerM b) -> TerM b (>>) :: TerM a -> TerM b -> TerM b return :: a -> TerM a
MonadError TCErr TerM Source #
Instance details Defined in Agda.Termination.Monad Methods throwError :: TCErr -> TerM a catchError :: TerM a -> (TCErr -> TerM a) -> TerM a
(Semigroup m, Monoid m) => Monoid (TerM m) Source #
Instance details Defined in Agda.Termination.Monad Methods mempty :: TerM m mappend :: TerM m -> TerM m -> TerM m mconcat :: [TerM m] -> TerM m
Semigroup m => Semigroup (TerM m) Source #
Instance details Defined in Agda.Termination.Monad Methods (<>) :: TerM m -> TerM m -> TerM m # sconcat :: NonEmpty (TerM m) -> TerM m stimes :: Integral b => b -> TerM m -> TerM m
type BenchPhase TerM Source #
Instance details Defined in Agda.Termination.Monad type BenchPhase TerM = Phase

runTer :: TerEnv -> TerM a -> TCM a Source #

Generic run method for termination monad.

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.

terGetUseDotPatterns :: TerM Bool Source #

terSetUseDotPatterns :: Bool -> TerM a -> TerM a Source #

terGetSizeSuc :: TerM (Maybe QName) Source #

terGetCurrent :: TerM QName Source #

terSetCurrent :: QName -> TerM a -> TerM a Source #

terGetSharp :: TerM (Maybe QName) Source #

terGetCutOff :: TerM CutOff Source #

terGetMutual :: TerM MutualNames Source #

terGetUserNames :: TerM (Set QName) Source #

terGetTarget :: TerM Target Source #

terSetTarget :: Target -> TerM a -> TerM a Source #

terGetHaveInlinedWith :: TerM Bool Source #

terSetHaveInlinedWith :: TerM a -> TerM a Source #

terGetMaskArgs :: TerM [Bool] Source #

terSetMaskArgs :: [Bool] -> TerM a -> TerM a Source #

terGetMaskResult :: TerM Bool Source #

terSetMaskResult :: Bool -> TerM a -> TerM a Source #

terGetPatterns :: TerM MaskedDeBruijnPatterns Source #

terSetPatterns :: MaskedDeBruijnPatterns -> TerM a -> TerM a Source #

terRaise :: TerM a -> TerM a Source #

terGetGuarded :: TerM Guarded Source #

terModifyGuarded :: (Order -> Order) -> TerM a -> TerM a Source #

terSetGuarded :: Order -> 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.

terModifyUsableVars :: (VarSet -> VarSet) -> TerM a -> TerM a Source #

terSetUsableVars :: VarSet -> TerM a -> TerM a Source #

terGetUseSizeLt :: TerM Bool Source #

Lens for terUseSizeLt.

terModifyUseSizeLt :: (Bool -> Bool) -> TerM a -> TerM a Source #

terSetUseSizeLt :: Bool -> TerM a -> TerM a Source #

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 :: forall a. 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

Instances details

UsableSizeVars DeBruijnPattern Source #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: DeBruijnPattern -> TerM VarSet Source #
UsableSizeVars MaskedDeBruijnPatterns Source #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source #
UsableSizeVars (Masked DeBruijnPattern) Source #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source #
UsableSizeVars [DeBruijnPattern] Source #
Instance details 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 #

data Masked a Source #

Constructors

Masked
Fields getMask :: Bool True if thing not eligible for structural descent. getMasked :: a Thing.

Instances

Instances details

UsableSizeVars MaskedDeBruijnPatterns Source #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source #
Decoration Masked Source #
Instance details Defined in Agda.Termination.Monad Methods traverseF :: Functor m => (a -> m b) -> Masked a -> m (Masked b) Source # distributeF :: Functor m => Masked (m a) -> m (Masked a) Source #
Foldable Masked Source #
Instance details 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 toList :: Masked a -> [a] null :: Masked a -> Bool length :: Masked a -> Int elem :: Eq a => a -> Masked a -> Bool maximum :: Ord a => Masked a -> a minimum :: Ord a => Masked a -> a sum :: Num a => Masked a -> a product :: Num a => Masked a -> a
Traversable Masked Source #
Instance details Defined in Agda.Termination.Monad Methods traverse :: Applicative f => (a -> f b) -> Masked a -> f (Masked b) sequenceA :: Applicative f => Masked (f a) -> f (Masked a) mapM :: Monad m => (a -> m b) -> Masked a -> m (Masked b) sequence :: Monad m => Masked (m a) -> m (Masked a)
Functor Masked Source #
Instance details Defined in Agda.Termination.Monad Methods fmap :: (a -> b) -> Masked a -> Masked b (<$) :: a -> Masked b -> Masked a #
UsableSizeVars (Masked DeBruijnPattern) Source #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source #
PrettyTCM a => PrettyTCM (Masked a) Source #	Print masked things in double parentheses.
Instance details Defined in Agda.Termination.Monad Methods prettyTCM :: MonadPretty m => Masked a -> m Doc Source #
Show a => Show (Masked a) Source #
Instance details Defined in Agda.Termination.Monad Methods showsPrec :: Int -> Masked a -> ShowS show :: Masked a -> String showList :: [Masked a] -> ShowS
Eq a => Eq (Masked a) Source #
Instance details Defined in Agda.Termination.Monad Methods (==) :: Masked a -> Masked a -> Bool (/=) :: Masked a -> Masked a -> Bool
Ord a => Ord (Masked a) Source #
Instance details Defined in Agda.Termination.Monad Methods compare :: Masked a -> Masked a -> Ordering (<) :: Masked a -> Masked a -> Bool (<=) :: Masked a -> Masked a -> Bool (>) :: Masked a -> Masked a -> Bool (>=) :: Masked a -> Masked a -> Bool max :: Masked a -> Masked a -> Masked a min :: Masked a -> Masked a -> Masked a

masked :: a -> Masked a Source #

notMasked :: a -> Masked a Source #

Call pathes

newtype CallPath Source #

Call paths.

Constructors

CallPath (DList CallInfo)

Instances

Instances details

Pretty CallPath Source #	Only show intermediate nodes. (Drop last `CallInfo`).
Instance details Defined in Agda.Termination.Monad Methods pretty :: CallPath -> Doc Source # prettyPrec :: Int -> CallPath -> Doc Source # prettyList :: [CallPath] -> Doc Source #
Monoid CallPath Source #
Instance details Defined in Agda.Termination.Monad Methods mempty :: CallPath mappend :: CallPath -> CallPath -> CallPath mconcat :: [CallPath] -> CallPath
Semigroup CallPath Source #
Instance details Defined in Agda.Termination.Monad Methods (<>) :: CallPath -> CallPath -> CallPath # sconcat :: NonEmpty CallPath -> CallPath stimes :: Integral b => b -> CallPath -> CallPath
Show CallPath Source #
Instance details Defined in Agda.Termination.Monad Methods showsPrec :: Int -> CallPath -> ShowS show :: CallPath -> String showList :: [CallPath] -> ShowS

callInfos :: CallPath -> [CallInfo] Source #

The calls making up the call path.

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

Instances details

TerSetSizeDepth ListTel Source #
Instance details Defined in Agda.Termination.Monad Methods terSetSizeDepth :: ListTel -> TerM a -> TerM a Source #
TerSetSizeDepth Telescope Source #
Instance details Defined in Agda.Termination.Monad Methods terSetSizeDepth :: Telescope -> TerM a -> TerM a Source #