Agda.Termination.Monad

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.

Documentation

type MutualNames = [QName]

The mutual block we are checking.

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

type Target = QName

The target of the function we are checking.

type Guarded = Order

The current guardedness level.

data TerEnv

The termination environment.

Constructors

TerEnv

Fields

terUseDotPatterns :: Bool

Are we mining dot patterns to find evindence of structal descent?

terGuardingTypeConstructors :: Bool

Do we assume that record and data type constructors preserve guardedness?

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 :: [QName]

The list of name actually appearing in the file (abstract syntax). Excludes the internally generated functions.

terTarget :: Maybe Target

Target type of the function we are currently termination checking. Only the constructors of Target are considered guarding.

terDelayed :: Delayed

Are we checking a delayed definition?

terPatterns :: [DeBruijnPat]

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.

terUsableVars :: VarSet

Pattern variables that can be compared to argument variables using SIZELT.

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.

Methods

terAsk :: m TerEnv

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

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

Instances

MonadTer TerM

newtype TerM a

Termination monad.

Constructors

TerM

Fields

terM :: ReaderT TerEnv TCM a

Instances

Monad TerM

Functor TerM

Applicative TerM

MonadIO TerM

MonadTCM TerM

MonadTer TerM

MonadError TCErr TerM

MonadReader TCEnv TerM

MonadState TCState TerM

runTerm :: TerEnv -> TerM a -> TCM a

Termination monad is a MonadTCM.

Modifiers and accessors for the termination environment in the monad.

terGetGuardingTypeConstructors :: 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

terGetDelayed :: TerM Delayed

terSetDelayed :: Delayed -> TerM a -> TerM a

terGetPatterns :: TerM DeBruijnPats

terSetPatterns :: DeBruijnPats -> 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

Should the codomain part of a function type preserve guardedness?

terGetUsableVars :: TerM VarSet

Lens for terUsableVars.

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

terSetUsableVars :: VarSet -> TerM a -> TerM a

terGetUseSizeLt :: TerM Bool

Lens for terUseSizeLt.

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

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.

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.

De Bruijn patterns.

type DeBruijnPats = [DeBruijnPat]

type DeBruijnPat = DeBruijnPat' Int

Patterns with variables as de Bruijn indices.

data DeBruijnPat' a

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

ProjDBP QName

Instances

Functor DeBruijnPat'

PrettyTCM DeBruijnPat

UsableSizeVars DeBruijnPat

Show a => Show (DeBruijnPat' a)

IsProjP (DeBruijnPat' a)

UsableSizeVars [DeBruijnPat]

unusedVar :: DeBruijnPat

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

raiseDBP :: Int -> DeBruijnPats -> DeBruijnPats

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

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).

Methods

usableSizeVars :: a -> TerM VarSet

Instances

UsableSizeVars DeBruijnPat

UsableSizeVars [DeBruijnPat]

Call pathes

newtype CallPath

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

Fields

callInfos :: [CallInfo]

Instances

Show CallPath

Monoid CallPath

Pretty CallPath

Only show intermediate nodes. (Drop last CallInfo).