Agda-2.5.1.2: A dependently typed functional programming language and proof assistant

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

# Documentation

type MutualNames = [QName] Source #

The mutual block we are checking.

The functions are numbered according to their order of appearance in this list.

type Target = QName Source #

The target of the function we are checking.

type Guarded = Order Source #

The current guardedness level.

data TerEnv Source #

The termination environment.

Constructors

 TerEnv FieldsterUseDotPatterns :: BoolAre we mining dot patterns to find evindence of structal descent?terGuardingTypeConstructors :: BoolDo we assume that record and data type constructors preserve guardedness?terInlineWithFunctions :: BoolDo we inline with functions to enhance termination checking of with?terSizeSuc :: Maybe QNameThe name of size successor, if any.terSharp :: Maybe QNameThe name of the delay constructor (sharp), if any.terCutOff :: CutOffDepth at which to cut off the structural order.terCurrent :: QNameThe name of the function we are currently checking.terMutual :: MutualNamesThe names of the functions in the mutual block we are checking. This includes the internally generated functions (with, extendedlambda, coinduction).terUserNames :: [QName]The list of name actually appearing in the file (abstract syntax). Excludes the internally generated functions.terTarget :: Maybe TargetTarget type of the function we are currently termination checking. Only the constructors of Target are considered guarding.terDelayed :: DelayedAre we checking a delayed definition?terMaskArgs :: [Bool]Only consider the notMasked False arguments for establishing termination.terMaskResult :: BoolOnly consider guardedness if False (not masked)._terSizeDepth :: IntHow many SIZELT relations do we have in the context (= clause telescope). Used to approximate termination for metas in call args.terPatterns :: MaskedDeBruijnPatsThe patterns of the clause we are checking.terPatternsRaise :: !IntNumber 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 :: !GuardedThe current guardedness status. Changes as we go deeper into the term. Updated during call graph extraction, hence strict.terUseSizeLt :: BoolWhen 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.terUsableVars :: VarSetPattern variables that can be compared to argument variables using SIZELT.

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.

Minimal complete definition

Methods

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

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

Instances

 Source # MethodsterLocal :: (TerEnv -> TerEnv) -> TerM a -> TerM a Source #terAsks :: (TerEnv -> a) -> TerM a Source #

newtype TerM a Source #

Constructors

 TerM FieldsterM :: ReaderT TerEnv TCM a

Instances

 Source # Methods(>>=) :: TerM a -> (a -> TerM b) -> TerM b #(>>) :: TerM a -> TerM b -> TerM b #return :: a -> TerM a #fail :: String -> TerM a # Source # Methodsfmap :: (a -> b) -> TerM a -> TerM b #(<$) :: a -> TerM b -> TerM a # Source # Methodspure :: a -> TerM a #(<*>) :: TerM (a -> b) -> TerM a -> TerM b #(*>) :: TerM a -> TerM b -> TerM b #(<*) :: TerM a -> TerM b -> TerM a # Source # MethodsliftIO :: IO a -> TerM a # Source # MethodsliftTCM :: TCM a -> TerM a Source # Source # MethodsterLocal :: (TerEnv -> TerEnv) -> TerM a -> TerM a Source #terAsks :: (TerEnv -> a) -> TerM a Source # Source # MethodsthrowError :: TCErr -> TerM a #catchError :: TerM a -> (TCErr -> TerM a) -> TerM a # Source # Methodslocal :: (TCEnv -> TCEnv) -> TerM a -> TerM a #reader :: (TCEnv -> a) -> TerM a # Source # Methodsput :: TCState -> TerM () #state :: (TCState -> (a, TCState)) -> TerM a # Source # MethodsgetsBenchmark :: (Benchmark Phase -> c) -> TerM c Source #finally :: TerM b -> TerM c -> TerM b Source # 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). # Termination monad is a MonadTCM. # Modifiers and accessors for the termination environment in the monad. terPiGuarded :: TerM a -> TerM a Source # Should the codomain part of a function type preserve guardedness? Lens for _terSizeDepth. Lens for terUsableVars. 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 patterns. Patterns with variables as de Bruijn indices. data DeBruijnPat' a Source # Constructors  VarDBP a De Bruijn Index. ConDBP QName [DeBruijnPat' a] The name refers to either an ordinary constructor or the successor function on sized types. LitDBP Literal Literal. Also abused to censor part of a pattern. TermDBP Term Part of dot pattern that cannot be converted into a pattern. ProjDBP QName Projection pattern. Instances  Source # Methodsfmap :: (a -> b) -> DeBruijnPat' a -> DeBruijnPat' b #(<$) :: a -> DeBruijnPat' b -> DeBruijnPat' a # Source # Methods Source # Methods Source # Methods Source # Methods Show a => Show (DeBruijnPat' a) Source # MethodsshowsPrec :: Int -> DeBruijnPat' a -> ShowS #show :: DeBruijnPat' a -> String #showList :: [DeBruijnPat' a] -> ShowS # Source # Methods Source # Methods

How long is the path to the deepest variable?

A dummy pattern used to mask a pattern that cannot be used for structural descent.

raiseDBP n ps increases each de Bruijn index in ps by n. Needed when going under a binder during analysis of a term.

class UsableSizeVars a where Source #

Extract variables from DeBruijnPats 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

usableSizeVars

Methods

Instances

 Source # Methods Source # Methods Source # Methods Source # Methods

Constructors

Instances

# Call pathes

newtype CallPath Source #

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.

Constructors

 CallPath FieldscallInfos :: [CallInfo]

Instances

 Source # MethodsshowList :: [CallPath] -> ShowS # Source # Methodsmconcat :: [CallPath] -> CallPath # Source # Only show intermediate nodes. (Drop last CallInfo). Methods Source # Methods

# Size depth estimation

A very crude way of estimating the SIZELT chains i > j > k in context. Returns 3 in this case. Overapproximates.