Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Termination.Monad

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

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

Instances

Instances details
HasOptions TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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

ReadTCState TerM Source # 
Instance details

Defined in Agda.Termination.Monad

HasBuiltins TerM Source # 
Instance details

Defined in Agda.Termination.Monad

MonadAddContext TerM Source # 
Instance details

Defined in Agda.Termination.Monad

MonadDebug TerM Source # 
Instance details

Defined in Agda.Termination.Monad

PureTCM TerM Source # 
Instance details

Defined in Agda.Termination.Monad

HasConstInfo TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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 #

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

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.

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

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

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

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

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

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

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 #

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

Monoid CallPath Source # 
Instance details

Defined in Agda.Termination.Monad

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