Mikan
Safe HaskellNone
LanguageHaskell2010

Mikan.Termination.Monad

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

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 Mikan.Termination.Monad

Methods

showsPrec :: Int -> Target -> ShowS #

show :: Target -> String #

showList :: [Target] -> ShowS #

Eq Target Source # 
Instance details

Defined in Mikan.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

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

  • terMaskResult :: !Bool

    Only consider guardedness if False (not masked).

  • terPatterns :: [DeBruijnPattern]

    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.

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 :: Type -> Type) 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 Mikan.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 Mikan.Termination.Monad

Methods

pragmaOptions :: TerM PragmaOptions Source #

commandLineOptions :: TerM CommandLineOptions Source #

MonadTer TerM Source # 
Instance details

Defined in Mikan.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 Mikan.Termination.Monad

Methods

liftReduce :: ReduceM a -> TerM a Source #

MonadTCEnv TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

askTC :: TerM TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> TerM a -> TerM a Source #

MonadTCM TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

liftTCM :: TCM a -> TerM a Source #

MonadTCState TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

getTC :: TerM TCState Source #

putTC :: TCState -> TerM () Source #

modifyTC :: (TCState -> TCState) -> TerM () Source #

ReadTCState TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

getTCState :: TerM TCState Source #

locallyTCState :: Lens' TCState a -> (a -> a) -> TerM b -> TerM b Source #

getSessionState :: TerM SessionState Source #

withTCState :: (TCState -> TCState) -> TerM a -> TerM a Source #

HasBuiltins TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

getBuiltinThing :: SomeBuiltin -> TerM (Maybe (Builtin PrimFun)) Source #

MonadAddContext TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

addCtx :: Name -> Dom Type -> TerM a -> TerM a Source #

addLetBinding' :: IsAxiom -> Origin -> 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 Mikan.Termination.Monad

Methods

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

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

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

getVerbosity :: TerM Verbosity Source #

getProfileOptions :: TerM ProfileOptions Source #

isDebugPrinting :: TerM Bool Source #

nowDebugPrinting :: TerM a -> TerM a Source #

PureTCM TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

HasConstInfo TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

getConstInfo :: QName -> TerM Definition Source #

getConstInfo' :: QName -> TerM (Either SigError Definition) Source #

MonadStatistics TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

tickN :: String -> Word64 -> TerM () Source #

tickMax :: String -> Word64 -> TerM () Source #

MonadBench TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Associated Types

type BenchPhase TerM 
Instance details

Defined in Mikan.Termination.Monad

type BenchPhase TerM = Phase

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 #

MonadFileId TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

fileFromId :: FileId -> TerM File Source #

idFromFile :: File -> TerM FileId Source #

Applicative TerM Source # 
Instance details

Defined in Mikan.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 Mikan.Termination.Monad

Methods

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

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

Monad TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

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

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

return :: a -> TerM a #

MonadIO TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

liftIO :: IO a -> TerM a #

MonadError TCErr TerM Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

throwError :: TCErr -> TerM a #

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

Monoid m => Monoid (TerM m) Source # 
Instance details

Defined in Mikan.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 Mikan.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 Mikan.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.

terGetCurrent :: TerM QName Source #

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

terGetCutOff :: TerM CutOff Source #

terGetMutual :: TerM MutualNames Source #

terGetUserNames :: TerM (Set QName) Source #

terGetTarget :: TerM Target Source #

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

terGetHaveInlinedWith :: TerM Bool Source #

terSetHaveInlinedWith :: TerM a -> TerM a Source #

terGetMaskResult :: TerM Bool Source #

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

terGetPatterns :: TerM [DeBruijnPattern] Source #

terSetPatterns :: [DeBruijnPattern] -> 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 #

isProjectionButNotCoinductive :: MonadTCM tcm => QName -> tcm Bool Source #

elimNotCoinductive :: MonadTCM tcm => Elim' t -> tcm Bool Source #

Is the given elimination anything but a coinductive projection?

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

Call paths

data CallPath Source #

Call paths.

Constructors

CallPath 

Fields

Instances

Instances details
Pretty CallPath Source #

Only show intermediate nodes. (Drop last CallInfo).

Instance details

Defined in Mikan.Termination.Monad

Methods

pretty :: CallPath -> Doc Source #

prettyPrec :: Int -> CallPath -> Doc Source #

prettyList :: [CallPath] -> Doc Source #

PrettyTCM CallPath Source #

Show all nodes.

Instance details

Defined in Mikan.Termination.Monad

Methods

prettyTCM :: MonadPretty m => CallPath -> m Doc Source #

Monoid CallPath Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

mempty :: CallPath #

mappend :: CallPath -> CallPath -> CallPath #

mconcat :: [CallPath] -> CallPath #

Semigroup CallPath Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

(<>) :: CallPath -> CallPath -> CallPath #

sconcat :: NonEmpty CallPath -> CallPath #

stimes :: Integral b => b -> CallPath -> CallPath #

Show CallPath Source # 
Instance details

Defined in Mikan.Termination.Monad

Methods

showsPrec :: Int -> CallPath -> ShowS #

show :: CallPath -> String #

showList :: [CallPath] -> ShowS #

callInfos :: CallPath -> [CallInfo] Source #

The calls making up the call path.

PrettyTCM

Orphan instances

PrettyTCM CallMatrix Source # 
Instance details

Methods

prettyTCM :: MonadPretty m => CallMatrix -> m Doc Source #

PrettyTCM cinfo => PrettyTCM (Call cinfo) Source # 
Instance details

Methods

prettyTCM :: MonadPretty m => Call cinfo -> m Doc Source #

PrettyTCM cinfo => PrettyTCM (CallGraph cinfo) Source # 
Instance details

Methods

prettyTCM :: MonadPretty m => CallGraph cinfo -> m Doc Source #

PrettyTCM cinfo => PrettyTCM (CMSet cinfo) Source # 
Instance details

Methods

prettyTCM :: MonadPretty m => CMSet cinfo -> m Doc Source #

PrettyTCM cinfo => PrettyTCM (CallMatrixAug cinfo) Source # 
Instance details

Methods

prettyTCM :: MonadPretty m => CallMatrixAug cinfo -> m Doc Source #