Safe Haskell | None |
---|
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.
- type MutualNames = [QName]
- type Target = QName
- type Guarded = Order
- data TerEnv = TerEnv {
- terUseDotPatterns :: Bool
- terGuardingTypeConstructors :: Bool
- terInlineWithFunctions :: Bool
- terSizeSuc :: Maybe QName
- terSharp :: Maybe QName
- terCutOff :: CutOff
- terCurrent :: QName
- terMutual :: MutualNames
- terUserNames :: [QName]
- terTarget :: Maybe Target
- terDelayed :: Delayed
- terMaskArgs :: [Bool]
- terMaskResult :: Bool
- terPatterns :: [DeBruijnPat]
- terPatternsRaise :: !Int
- terGuarded :: !Guarded
- terUseSizeLt :: Bool
- terUsableVars :: VarSet
- defaultTerEnv :: TerEnv
- class (Functor m, Monad m) => MonadTer m where
- newtype TerM a = TerM {}
- runTerm :: TerEnv -> TerM a -> TCM a
- terGetGuardingTypeConstructors :: TerM Bool
- terGetInlineWithFunctions :: TerM Bool
- 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
- 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 DeBruijnPats
- terSetPatterns :: DeBruijnPats -> 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
- terPiGuarded :: TerM a -> TerM a
- 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 => QName -> tcm Bool
- type DeBruijnPats = [DeBruijnPat]
- type DeBruijnPat = DeBruijnPat' Int
- data DeBruijnPat' a
- unusedVar :: DeBruijnPat
- raiseDBP :: Int -> DeBruijnPats -> DeBruijnPats
- class UsableSizeVars a where
- usableSizeVars :: a -> TerM VarSet
- newtype CallPath = CallPath {}
Documentation
type MutualNames = [QName]Source
The mutual block we are checking.
The functions are numbered according to their order of appearance in this list.
The termination environment.
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 whereSource
Termination monad service class.
Termination monad.
Termination monad is a MonadTCM
.
Modifiers and accessors for the termination environment in the monad.
terGetInlineWithFunctions :: TerM BoolSource
terGetUseDotPatterns :: TerM BoolSource
terSetUseDotPatterns :: Bool -> TerM a -> TerM aSource
terGetSizeSuc :: TerM (Maybe QName)Source
terSetCurrent :: QName -> TerM a -> TerM aSource
terGetSharp :: TerM (Maybe QName)Source
terGetTarget :: TerM (Maybe Target)Source
terSetTarget :: Maybe Target -> TerM a -> TerM aSource
terSetDelayed :: Delayed -> TerM a -> TerM aSource
terGetMaskArgs :: TerM [Bool]Source
terSetMaskArgs :: [Bool] -> TerM a -> TerM aSource
terGetMaskResult :: TerM BoolSource
terSetMaskResult :: Bool -> TerM a -> TerM aSource
terSetPatterns :: DeBruijnPats -> TerM a -> TerM aSource
terSetGuarded :: Order -> TerM a -> TerM aSource
terUnguarded :: TerM a -> TerM aSource
terPiGuarded :: TerM a -> TerM aSource
Should the codomain part of a function type preserve guardedness?
terGetUsableVars :: TerM VarSetSource
Lens for terUsableVars
.
terSetUsableVars :: VarSet -> TerM a -> TerM aSource
terGetUseSizeLt :: TerM BoolSource
Lens for terUseSizeLt
.
terModifyUseSizeLt :: (Bool -> Bool) -> TerM a -> TerM aSource
terSetUseSizeLt :: Bool -> TerM a -> TerM aSource
withUsableVars :: UsableSizeVars a => a -> TerM b -> TerM bSource
Compute usable vars from patterns and run subcomputation.
conUseSizeLt :: QName -> TerM a -> TerM aSource
Set terUseSizeLt
when going under constructor c
.
projUseSizeLt :: QName -> TerM a -> TerM aSource
Set terUseSizeLt
for arguments following projection q
.
isProjectionButNotCoinductive :: MonadTCM tcm => QName -> tcm BoolSource
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 => QName -> tcm BoolSource
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 DeBruijnPats = [DeBruijnPat]Source
type DeBruijnPat = DeBruijnPat' IntSource
Patterns with variables as de Bruijn indices.
data DeBruijnPat' a Source
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 | |
ProjDBP QName |
Functor DeBruijnPat' | |
PrettyTCM DeBruijnPat | |
UsableSizeVars DeBruijnPat | |
Show a => Show (DeBruijnPat' a) | |
IsProjP (DeBruijnPat' a) | |
UsableSizeVars [DeBruijnPat] |
unusedVar :: DeBruijnPatSource
A dummy pattern used to mask a pattern that cannot be used for structural descent.
raiseDBP :: Int -> DeBruijnPats -> DeBruijnPatsSource
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 whereSource
Extract variables from DeBruijnPat
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).
usableSizeVars :: a -> TerM VarSetSource
Call pathes
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.