HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

ModuleAgda-2.7.0.1Haskell2010

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.

  • 7 types
  • 3 classes
  • 44 values
  • PackageAgda-2.7.0.1
  • Exports54
  • LanguageHaskell2010
  • LicenceMIT
  • SourceMonad.hs
datadata Target
#

The target of the function we are checking.

Constructors

Instances2Eq, Show
  • Eq TargetDefined in Agda-2.7.0.1 · Agda.Termination.Monad
  • Show TargetDefined in Agda-2.7.0.1 · Agda.Termination.Monad
datadata TerEnv
#

The termination environment.

Constructors

  • TerEnv
    • 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.

valuedefaultTerEnv :: 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.

newtypenewtype TerM a
#

Termination monad.

Constructors

Instances23Monad, Functor, MonadFail, Applicative, MonadIO, MonadBench, …
valuerunTerDefault :: TerM a -> TCM a
#

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

Modifiers and accessors for the termination environment in the monad.

36 declarations
valueprojUseSizeLt :: 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).

valueisProjectionButNotCoinductive :: 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.

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

3 declarations
classclass 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

Instances4UsableSizeVars

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

4 declarations
datadata Masked a
#

Constructors

Instances10Functor, Foldable, Traversable, Decoration, Eq, Ord, …

Call pathes

2 declarations

Size depth estimation

1 declaration