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

Safe HaskellNone
LanguageHaskell2010

Agda.Termination.Monad

Contents

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 

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?

  • terInlineWithFunctions :: Bool

    Do we inline with functions to enhance termination checking of with?

  • 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?

  • 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 :: MaskedDeBruijnPats

    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

newtype TerM a Source #

Termination monad.

Constructors

TerM 

Fields

Instances

Monad TerM Source # 

Methods

(>>=) :: TerM a -> (a -> TerM b) -> TerM b #

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

return :: a -> TerM a #

fail :: String -> TerM a #

Functor TerM Source # 

Methods

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

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

Applicative TerM Source # 

Methods

pure :: a -> TerM a #

(<*>) :: TerM (a -> b) -> TerM a -> TerM b #

(*>) :: TerM a -> TerM b -> TerM b #

(<*) :: TerM a -> TerM b -> TerM a #

MonadIO TerM Source # 

Methods

liftIO :: IO a -> TerM a #

MonadTCM TerM Source # 

Methods

liftTCM :: TCM a -> TerM a Source #

HasConstInfo TerM Source # 
MonadTer TerM Source # 

Methods

terAsk :: TerM TerEnv Source #

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

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

MonadError TCErr TerM Source # 

Methods

throwError :: TCErr -> TerM a #

catchError :: TerM a -> (TCErr -> TerM a) -> TerM a #

MonadReader TCEnv TerM Source # 

Methods

ask :: TerM TCEnv #

local :: (TCEnv -> TCEnv) -> TerM a -> TerM a #

reader :: (TCEnv -> a) -> TerM a #

MonadState TCState TerM Source # 

Methods

get :: TerM TCState #

put :: TCState -> TerM () #

state :: (TCState -> (a, TCState)) -> TerM a #

MonadBench Phase TerM 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?

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.

type DeBruijnPat = DeBruijnPat' Int Source #

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 ProjOrigin QName

Projection pattern.

patternDepth :: DeBruijnPat' a -> Int Source #

How long is the path to the deepest variable?

unusedVar :: DeBruijnPat Source #

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

raiseDBP :: Int -> DeBruijnPats -> DeBruijnPats Source #

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

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

data Masked a Source #

Constructors

Masked 

Fields

Instances

Functor Masked Source # 

Methods

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

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

Foldable Masked Source # 

Methods

fold :: Monoid m => Masked m -> 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 # 

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

Decoration Masked Source # 

Methods

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

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

UsableSizeVars MaskedDeBruijnPats Source # 
Eq a => Eq (Masked a) Source # 

Methods

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

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

Ord a => Ord (Masked a) Source # 

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 #

Show a => Show (Masked a) Source # 

Methods

showsPrec :: Int -> Masked a -> ShowS #

show :: Masked a -> String #

showList :: [Masked a] -> ShowS #

PrettyTCM a => PrettyTCM (Masked a) Source #

Print masked things in double parentheses.

Methods

prettyTCM :: Masked a -> TCM Doc Source #

UsableSizeVars (Masked DeBruijnPat) Source # 

masked :: a -> Masked a Source #

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 

Fields

Size depth estimation

terSetSizeDepth :: Telescope -> TerM a -> TerM a Source #

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