Agda.Termination.Monad

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.

Documentation

data Target

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

Show Target

Defined in Agda.Termination.Monad

Methods

showsPrec :: Int -> Target -> ShowS

show :: Target -> String

showList :: [Target] -> ShowS

Eq Target

Defined in Agda.Termination.Monad

Methods

(==) :: Target -> Target -> Bool

(/=) :: Target -> Target -> Bool

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?

• 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

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.

Minimal complete definition

terAsk, terLocal

Methods

terAsk :: m TerEnv

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

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

Instances

MonadTer TerM

Defined in Agda.Termination.Monad

Methods

terAsk :: TerM TerEnv

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

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

newtype TerM a

Termination monad.

Constructors

TerM

Fields

• terM :: ReaderT TerEnv TCM a

Instances

HasOptions TerM

Defined in Agda.Termination.Monad

Methods

pragmaOptions :: TerM PragmaOptions

commandLineOptions :: TerM CommandLineOptions

MonadTer TerM

Defined in Agda.Termination.Monad

Methods

terAsk :: TerM TerEnv

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

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

MonadReduce TerM

Defined in Agda.Termination.Monad

Methods

liftReduce :: ReduceM a -> TerM a

MonadTCEnv TerM

Defined in Agda.Termination.Monad

Methods

askTC :: TerM TCEnv

localTC :: (TCEnv -> TCEnv) -> TerM a -> TerM a

MonadTCM TerM

Defined in Agda.Termination.Monad

Methods

liftTCM :: TCM a -> TerM a

MonadTCState TerM

Defined in Agda.Termination.Monad

Methods

getTC :: TerM TCState

putTC :: TCState -> TerM ()

modifyTC :: (TCState -> TCState) -> TerM ()

ReadTCState TerM

Defined in Agda.Termination.Monad

Methods

getTCState :: TerM TCState

locallyTCState :: Lens' TCState a -> (a -> a) -> TerM b -> TerM b

withTCState :: (TCState -> TCState) -> TerM a -> TerM a

HasBuiltins TerM

Defined in Agda.Termination.Monad

Methods

getBuiltinThing :: SomeBuiltin -> TerM (Maybe (Builtin PrimFun))

MonadAddContext TerM

Defined in Agda.Termination.Monad

Methods

addCtx :: Name -> Dom Type -> TerM a -> TerM a

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a

updateContext :: Substitution -> (Context -> Context) -> TerM a -> TerM a

withFreshName :: Range -> ArgName -> (Name -> TerM a) -> TerM a

MonadDebug TerM

Defined in Agda.Termination.Monad

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> TerM String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> TerM a -> TerM a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> TerM a -> TerM a

getVerbosity :: TerM Verbosity

getProfileOptions :: TerM ProfileOptions

isDebugPrinting :: TerM Bool

nowDebugPrinting :: TerM a -> TerM a

PureTCM TerM

Defined in Agda.Termination.Monad

HasConstInfo TerM

Defined in Agda.Termination.Monad

Methods

getConstInfo :: QName -> TerM Definition

getConstInfo' :: QName -> TerM (Either SigError Definition)

getRewriteRulesFor :: QName -> TerM RewriteRules

MonadStatistics TerM

Defined in Agda.Termination.Monad

Methods

modifyCounter :: String -> (Integer -> Integer) -> TerM ()

MonadBench TerM

Defined in Agda.Termination.Monad

Associated Types

type BenchPhase TerM

Methods

getBenchmark :: TerM (Benchmark (BenchPhase TerM))

putBenchmark :: Benchmark (BenchPhase TerM) -> TerM ()

modifyBenchmark :: (Benchmark (BenchPhase TerM) -> Benchmark (BenchPhase TerM)) -> TerM ()

finally :: TerM b -> TerM c -> TerM b

MonadFail TerM

Defined in Agda.Termination.Monad

Methods

fail :: String -> TerM a

MonadIO TerM

Defined in Agda.Termination.Monad

Methods

liftIO :: IO a -> TerM a

Applicative TerM

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

Defined in Agda.Termination.Monad

Methods

fmap :: (a -> b) -> TerM a -> TerM b

(<$) :: a -> TerM b -> TerM a

Monad TerM

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

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)

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)

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

Defined in Agda.Termination.Monad

type BenchPhase TerM = Phase

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

Generic run method for termination monad.

runTerDefault :: TerM a -> TCM a

Run TerM computation in default environment (created from options).

Modifiers and accessors for the termination environment in the monad.

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

Lens for _terSizeDepth.

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

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 :: MaskedDeBruijnPatterns -> TerM VarSet

UsableSizeVars (Masked DeBruijnPattern)

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet

UsableSizeVars [DeBruijnPattern]

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: [DeBruijnPattern] -> TerM VarSet

Masked patterns (which are not eligible for structural descent, only for size descent)

type MaskedDeBruijnPatterns = [Masked DeBruijnPattern]

data Masked a

Constructors

Masked

Fields

• getMask :: Bool

  True if thing not eligible for structural descent.

• getMasked :: a

  Thing.

Instances

UsableSizeVars MaskedDeBruijnPatterns

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet

Decoration Masked

Defined in Agda.Termination.Monad

Methods

traverseF :: Functor m => (a -> m b) -> Masked a -> m (Masked b)

distributeF :: Functor m => Masked (m a) -> m (Masked a)

Foldable Masked

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

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

Defined in Agda.Termination.Monad

Methods

fmap :: (a -> b) -> Masked a -> Masked b

(<$) :: a -> Masked b -> Masked a

UsableSizeVars (Masked DeBruijnPattern)

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet

PrettyTCM a => PrettyTCM (Masked a)

Print masked things in double parentheses.

Defined in Agda.Termination.Monad

Methods

prettyTCM :: MonadPretty m => Masked a -> m Doc

Show a => Show (Masked a)

Defined in Agda.Termination.Monad

Methods

showsPrec :: Int -> Masked a -> ShowS

show :: Masked a -> String

showList :: [Masked a] -> ShowS

Eq a => Eq (Masked a)

Defined in Agda.Termination.Monad

Methods

(==) :: Masked a -> Masked a -> Bool

(/=) :: Masked a -> Masked a -> Bool

Ord a => Ord (Masked a)

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

notMasked :: a -> Masked a

Call pathes

newtype CallPath

Call paths.

Constructors

CallPath (DList CallInfo)

Instances

Pretty CallPath

Only show intermediate nodes. (Drop last CallInfo).

Defined in Agda.Termination.Monad

Methods

pretty :: CallPath -> Doc

prettyPrec :: Int -> CallPath -> Doc

prettyList :: [CallPath] -> Doc

Monoid CallPath

Defined in Agda.Termination.Monad

Methods

mempty :: CallPath

mappend :: CallPath -> CallPath -> CallPath

mconcat :: [CallPath] -> CallPath

Semigroup CallPath

Defined in Agda.Termination.Monad

Methods

(<>) :: CallPath -> CallPath -> CallPath

sconcat :: NonEmpty CallPath -> CallPath

stimes :: Integral b => b -> CallPath -> CallPath

Show CallPath

Defined in Agda.Termination.Monad

Methods

showsPrec :: Int -> CallPath -> ShowS

show :: CallPath -> String

showList :: [CallPath] -> ShowS

callInfos :: CallPath -> [CallInfo]

The calls making up the call path.

Size depth estimation

class TerSetSizeDepth b where

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

Instances

TerSetSizeDepth ListTel

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: ListTel -> TerM a -> TerM a

TerSetSizeDepth Telescope

Defined in Agda.Termination.Monad

Methods

terSetSizeDepth :: Telescope -> TerM a -> TerM a