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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Termination.Monad

Contents

- Modifiers and accessors for the termination environment in the monad.
- De Bruijn pattern stuff
- Masked patterns (which are not eligible for structural descent, only for size descent)
- Call pathes
- Size depth estimation

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

- type MutualNames = [QName]
- type Target = QName
- type Guarded = Order
- data TerEnv = TerEnv {
  - terUseDotPatterns :: Bool
  - terSizeSuc :: Maybe QName
  - terSharp :: Maybe QName
  - terCutOff :: CutOff
  - terCurrent :: QName
  - terMutual :: MutualNames
  - terUserNames :: [QName]
  - terHaveInlinedWith :: Bool
  - terTarget :: Maybe Target
  - terDelayed :: Delayed
  - terMaskArgs :: [Bool]
  - terMaskResult :: Bool
  - _terSizeDepth :: Int
  - terPatterns :: MaskedDeBruijnPatterns
  - terPatternsRaise :: !Int
  - terGuarded :: !Guarded
  - terUseSizeLt :: Bool
  - terUsableVars :: VarSet
  }
- defaultTerEnv :: TerEnv
- class (Functor m, Monad m) => MonadTer m where
  - terAsk :: m TerEnv
  - terLocal :: (TerEnv -> TerEnv) -> m a -> m a
  - terAsks :: (TerEnv -> a) -> m a
- newtype TerM a = TerM {
  - terM :: ReaderT TerEnv TCM a
  }
- runTer :: TerEnv -> TerM a -> TCM a
- runTerDefault :: TerM a -> TCM a
- 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
- terGetHaveInlinedWith :: TerM Bool
- terSetHaveInlinedWith :: TerM a -> TerM a
- terGetDelayed :: TerM Delayed
- terSetDelayed :: Delayed -> 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' Int TerEnv
- terGetUsableVars :: TerM VarSet
- terModifyUsableVars :: (VarSet -> VarSet) -> TerM a -> TerM a
- terSetUsableVars :: VarSet -> TerM a -> TerM a
- terGetUseSizeLt :: TerM Bool
- terModifyUseSizeLt :: (Bool -> Bool) -> TerM a -> TerM a
- terSetUseSizeLt :: Bool -> TerM a -> TerM a
- withUsableVars :: UsableSizeVars a => a -> TerM b -> TerM b
- conUseSizeLt :: QName -> TerM a -> TerM a
- projUseSizeLt :: QName -> TerM a -> TerM a
- isProjectionButNotCoinductive :: MonadTCM tcm => QName -> tcm Bool
- isCoinductiveProjection :: MonadTCM tcm => Bool -> QName -> tcm Bool
- patternDepth :: forall a. Pattern' a -> Int
- unusedVar :: DeBruijnPattern
- class UsableSizeVars a where
  - usableSizeVars :: a -> TerM VarSet
- type MaskedDeBruijnPatterns = [Masked DeBruijnPattern]
- data Masked a = Masked {
  - getMask :: Bool
  - getMasked :: a
  }
- masked :: a -> Masked a
- notMasked :: a -> Masked a
- newtype CallPath = CallPath {
  - callInfos :: [CallInfo]
  }
- terSetSizeDepth :: Telescope -> TerM a -> TerM a

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

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

- terHaveInlinedWith :: Bool

  Does the actual clause result from with-inlining? (If yes, it may be ill-typed.)

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

- terM :: ReaderT TerEnv TCM a

#### Instances

Instances details

HasOptions TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods pragmaOptions :: TerM PragmaOptions Source # commandLineOptions :: TerM CommandLineOptions Source #
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 Methods getTC :: TerM TCState Source # putTC :: TCState -> TerM () Source # modifyTC :: (TCState -> TCState) -> TerM () Source #
ReadTCState TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods getTCState :: TerM TCState Source # locallyTCState :: Lens' a TCState -> (a -> a) -> TerM b -> TerM b Source # withTCState :: (TCState -> TCState) -> TerM a -> TerM a Source #
HasBuiltins TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods getBuiltinThing :: String -> TerM (Maybe (Builtin PrimFun)) Source #
MonadAddContext TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods addCtx :: Name -> Dom Type -> TerM a -> TerM a Source # addLetBinding' :: Name -> Term -> Dom Type -> TerM a -> TerM a Source # updateContext :: Substitution -> (Context -> Context) -> TerM a -> TerM a Source # withFreshName :: Range -> ArgName -> (Name -> TerM a) -> TerM a Source #
MonadDebug TerM Source # |

Instance details

Defined in Agda.Termination.Monad

Methods

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

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

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

getVerbosity :: TerM Verbosity Source #

isDebugPrinting :: TerM Bool Source #

nowDebugPrinting :: TerM a -> TerM a Source #

PureTCM TerM Source # |
Instance details Defined in Agda.Termination.Monad
HasConstInfo TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods getConstInfo :: QName -> TerM Definition Source # getConstInfo' :: QName -> TerM (Either SigError Definition) Source # getRewriteRulesFor :: QName -> TerM RewriteRules Source #
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 # Methods getBenchmark :: TerM (Benchmark (BenchPhase TerM)) Source # putBenchmark :: Benchmark (BenchPhase TerM) -> TerM () Source # modifyBenchmark :: (Benchmark (BenchPhase TerM) -> Benchmark (BenchPhase TerM)) -> TerM () Source # finally :: TerM b -> TerM c -> TerM b Source #
MonadFail TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods fail :: String -> TerM a Source #
MonadIO TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods liftIO :: IO a -> TerM a Source #
Applicative TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods pure :: a -> TerM a Source # (<*>) :: TerM (a -> b) -> TerM a -> TerM b Source # liftA2 :: (a -> b -> c) -> TerM a -> TerM b -> TerM c Source # (*>) :: TerM a -> TerM b -> TerM b Source # (<*) :: TerM a -> TerM b -> TerM a Source #
Functor TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods fmap :: (a -> b) -> TerM a -> TerM b Source # (<$) :: a -> TerM b -> TerM a Source #
Monad TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods (>>=) :: TerM a -> (a -> TerM b) -> TerM b Source # (>>) :: TerM a -> TerM b -> TerM b Source # return :: a -> TerM a Source #
MonadError TCErr TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods throwError :: TCErr -> TerM a Source # catchError :: TerM a -> (TCErr -> TerM a) -> TerM a Source #
(Semigroup m, Monoid m) => Monoid (TerM m) Source # |
Instance details Defined in Agda.Termination.Monad Methods mempty :: TerM m Source # mappend :: TerM m -> TerM m -> TerM m Source # mconcat :: [TerM m] -> TerM m Source #
Semigroup m => Semigroup (TerM m) Source # |
Instance details Defined in Agda.Termination.Monad Methods (<>) :: TerM m -> TerM m -> TerM m Source # sconcat :: NonEmpty (TerM m) -> TerM m Source # stimes :: Integral b => b -> TerM m -> TerM m Source #
type BenchPhase TerM Source # |
Instance details Defined in Agda.Termination.Monad type BenchPhase TerM = Phase

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.

terGetUseDotPatterns :: TerM Bool Source #

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

terGetSizeSuc :: TerM (Maybe QName) Source #

terGetCurrent :: TerM QName Source #

terSetCurrent :: QName -> TerM a -> TerM a Source #

terGetSharp :: TerM (Maybe QName) Source #

terGetCutOff :: TerM CutOff Source #

terGetMutual :: TerM MutualNames Source #

terGetUserNames :: TerM [QName] Source #

terGetTarget :: TerM (Maybe Target) Source #

terSetTarget :: Maybe Target -> TerM a -> TerM a Source #

terGetHaveInlinedWith :: TerM Bool Source #

terSetHaveInlinedWith :: TerM a -> TerM a Source #

terGetDelayed :: TerM Delayed Source #

terSetDelayed :: Delayed -> TerM a -> TerM a Source #

terGetMaskArgs :: TerM [Bool] Source #

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

terGetMaskResult :: TerM Bool Source #

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

terGetPatterns :: TerM MaskedDeBruijnPatterns Source #

terSetPatterns :: MaskedDeBruijnPatterns -> TerM a -> TerM a Source #

terRaise :: TerM a -> TerM a Source #

terGetGuarded :: TerM Guarded Source #

terModifyGuarded :: (Order -> Order) -> TerM a -> TerM a Source #

terSetGuarded :: Order -> TerM a -> TerM a Source #

terUnguarded :: TerM a -> TerM a Source #

terSizeDepth :: Lens' Int TerEnv Source #

Lens for `_terSizeDepth`.

terGetUsableVars :: TerM VarSet Source #

Lens for `terUsableVars`.

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

terSetUsableVars :: VarSet -> TerM a -> TerM a Source #

terGetUseSizeLt :: TerM Bool Source #

Lens for `terUseSizeLt`.

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 `DeBruijnPattern`s 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 Source #

#### Instances

Instances details

UsableSizeVars DeBruijnPattern Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: DeBruijnPattern -> TerM VarSet Source #
UsableSizeVars MaskedDeBruijnPatterns Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source #
UsableSizeVars (Masked DeBruijnPattern) Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source #
UsableSizeVars [DeBruijnPattern] Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: [DeBruijnPattern] -> TerM VarSet Source #

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

type MaskedDeBruijnPatterns = [Masked DeBruijnPattern] Source #

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 Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source #
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 Source #

foldMap :: Monoid m => (a -> m) -> Masked a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Masked a -> m Source #

foldr :: (a -> b -> b) -> b -> Masked a -> b Source #

foldr' :: (a -> b -> b) -> b -> Masked a -> b Source #

foldl :: (b -> a -> b) -> b -> Masked a -> b Source #

foldl' :: (b -> a -> b) -> b -> Masked a -> b Source #

foldr1 :: (a -> a -> a) -> Masked a -> a Source #

foldl1 :: (a -> a -> a) -> Masked a -> a Source #

toList :: Masked a -> [a] Source #

null :: Masked a -> Bool Source #

length :: Masked a -> Int Source #

elem :: Eq a => a -> Masked a -> Bool Source #

maximum :: Ord a => Masked a -> a Source #

minimum :: Ord a => Masked a -> a Source #

sum :: Num a => Masked a -> a Source #

product :: Num a => Masked a -> a Source #

Traversable Masked Source # |
Instance details Defined in Agda.Termination.Monad Methods traverse :: Applicative f => (a -> f b) -> Masked a -> f (Masked b) Source # sequenceA :: Applicative f => Masked (f a) -> f (Masked a) Source # mapM :: Monad m => (a -> m b) -> Masked a -> m (Masked b) Source # sequence :: Monad m => Masked (m a) -> m (Masked a) Source #
Functor Masked Source # |
Instance details Defined in Agda.Termination.Monad Methods fmap :: (a -> b) -> Masked a -> Masked b Source # (<$) :: a -> Masked b -> Masked a Source #
UsableSizeVars (Masked DeBruijnPattern) Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source #
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 Source # show :: Masked a -> String Source # showList :: [Masked a] -> ShowS Source #
Eq a => Eq (Masked a) Source # |
Instance details Defined in Agda.Termination.Monad Methods (==) :: Masked a -> Masked a -> Bool Source # (/=) :: Masked a -> Masked a -> Bool Source #
Ord a => Ord (Masked a) Source # |
Instance details Defined in Agda.Termination.Monad Methods compare :: Masked a -> Masked a -> Ordering Source # (<) :: Masked a -> Masked a -> Bool Source # (<=) :: Masked a -> Masked a -> Bool Source # (>) :: Masked a -> Masked a -> Bool Source # (>=) :: Masked a -> Masked a -> Bool Source # max :: Masked a -> Masked a -> Masked a Source # min :: Masked a -> Masked a -> Masked a Source #

masked :: a -> Masked a Source #

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

- callInfos :: [CallInfo]

#### Instances

Instances details

Pretty CallPath Source # | Only show intermediate nodes. (Drop last `CallInfo`).
Instance details Defined in Agda.Termination.Monad Methods pretty :: CallPath -> Doc Source # prettyPrec :: Int -> CallPath -> Doc Source # prettyList :: [CallPath] -> Doc Source #
Monoid CallPath Source # |
Instance details Defined in Agda.Termination.Monad Methods mempty :: CallPath Source # mappend :: CallPath -> CallPath -> CallPath Source # mconcat :: [CallPath] -> CallPath Source #
Semigroup CallPath Source # |
Instance details Defined in Agda.Termination.Monad Methods (<>) :: CallPath -> CallPath -> CallPath Source # sconcat :: NonEmpty CallPath -> CallPath Source # stimes :: Integral b => b -> CallPath -> CallPath Source #
Show CallPath Source # |
Instance details Defined in Agda.Termination.Monad Methods showsPrec :: Int -> CallPath -> ShowS Source # show :: CallPath -> String Source # showList :: [CallPath] -> ShowS Source #

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