| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.Trace
Contents
Synopsis
- interestingCall :: Call -> Bool
- class (MonadTCEnv m, ReadTCState m) => MonadTrace m where
- traceCall :: Call -> m a -> m a
- traceCallM :: m Call -> m a -> m a
- traceCallCPS :: Call -> ((a -> m b) -> m b) -> (a -> m b) -> m b
- traceClosureCall :: Closure Call -> m a -> m a
- printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
- getCurrentRange :: MonadTCEnv m => m Range
- setCurrentRange :: (MonadTrace m, HasRange x) => x -> m a -> m a
- highlightAsTypeChecked :: MonadTrace m => Range -> Range -> m a -> m a
Trace
interestingCall :: Call -> Bool Source #
class (MonadTCEnv m, ReadTCState m) => MonadTrace m where Source #
Minimal complete definition
Methods
traceCall :: Call -> m a -> m a Source #
Record a function call in the trace.
traceCallM :: m Call -> m a -> m a Source #
traceCallCPS :: Call -> ((a -> m b) -> m b) -> (a -> m b) -> m b Source #
Like traceCall, but resets envCall and the current ranges to the
previous values in the continuation.
traceClosureCall :: Closure Call -> m a -> m a Source #
printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> m () Source #
Lispify and print the given highlighting information.
default printHighlightingInfo :: (MonadTrans t, MonadTrace n, t n ~ m) => RemoveTokenBasedHighlighting -> HighlightingInfo -> m () Source #
Instances
| MonadTrace TCM Source # | |
Defined in Agda.TypeChecking.Monad.Trace Methods traceCall :: Call -> TCM a -> TCM a Source # traceCallM :: TCM Call -> TCM a -> TCM a Source # traceCallCPS :: Call -> ((a -> TCM b) -> TCM b) -> (a -> TCM b) -> TCM b Source # traceClosureCall :: Closure Call -> TCM a -> TCM a Source # printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM () Source # | |
| MonadTrace m => MonadTrace (ExceptT e m) Source # | |
Defined in Agda.TypeChecking.Monad.Trace Methods traceCall :: Call -> ExceptT e m a -> ExceptT e m a Source # traceCallM :: ExceptT e m Call -> ExceptT e m a -> ExceptT e m a Source # traceCallCPS :: Call -> ((a -> ExceptT e m b) -> ExceptT e m b) -> (a -> ExceptT e m b) -> ExceptT e m b Source # traceClosureCall :: Closure Call -> ExceptT e m a -> ExceptT e m a Source # printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> ExceptT e m () Source # | |
| MonadTrace m => MonadTrace (IdentityT m) Source # | |
Defined in Agda.TypeChecking.Monad.Trace Methods traceCall :: Call -> IdentityT m a -> IdentityT m a Source # traceCallM :: IdentityT m Call -> IdentityT m a -> IdentityT m a Source # traceCallCPS :: Call -> ((a -> IdentityT m b) -> IdentityT m b) -> (a -> IdentityT m b) -> IdentityT m b Source # traceClosureCall :: Closure Call -> IdentityT m a -> IdentityT m a Source # printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> IdentityT m () Source # | |
| MonadTrace m => MonadTrace (ReaderT r m) Source # | |
Defined in Agda.TypeChecking.Monad.Trace Methods traceCall :: Call -> ReaderT r m a -> ReaderT r m a Source # traceCallM :: ReaderT r m Call -> ReaderT r m a -> ReaderT r m a Source # traceCallCPS :: Call -> ((a -> ReaderT r m b) -> ReaderT r m b) -> (a -> ReaderT r m b) -> ReaderT r m b Source # traceClosureCall :: Closure Call -> ReaderT r m a -> ReaderT r m a Source # printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> ReaderT r m () Source # | |
| MonadTrace m => MonadTrace (StateT s m) Source # | |
Defined in Agda.TypeChecking.Monad.Trace Methods traceCall :: Call -> StateT s m a -> StateT s m a Source # traceCallM :: StateT s m Call -> StateT s m a -> StateT s m a Source # traceCallCPS :: Call -> ((a -> StateT s m b) -> StateT s m b) -> (a -> StateT s m b) -> StateT s m b Source # traceClosureCall :: Closure Call -> StateT s m a -> StateT s m a Source # printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> StateT s m () Source # | |
| (MonadTrace m, Monoid w) => MonadTrace (WriterT w m) Source # | |
Defined in Agda.TypeChecking.Monad.Trace Methods traceCall :: Call -> WriterT w m a -> WriterT w m a Source # traceCallM :: WriterT w m Call -> WriterT w m a -> WriterT w m a Source # traceCallCPS :: Call -> ((a -> WriterT w m b) -> WriterT w m b) -> (a -> WriterT w m b) -> WriterT w m b Source # traceClosureCall :: Closure Call -> WriterT w m a -> WriterT w m a Source # printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> WriterT w m () Source # | |
getCurrentRange :: MonadTCEnv m => m Range Source #
setCurrentRange :: (MonadTrace m, HasRange x) => x -> m a -> m a Source #
Sets the current range (for error messages etc.) to the range
of the given object, if it has a range (i.e., its range is not noRange).
highlightAsTypeChecked Source #
Arguments
| :: MonadTrace m | |
| => Range | rPre |
| -> Range | r |
| -> m a | |
| -> m a |
highlightAsTypeChecked rPre r m runs m and returns its
result. Additionally, some code may be highlighted:
- If
ris non-empty and not a sub-range ofrPre(aftercontinuousPerLinehas been applied to both):ris highlighted as being type-checked whilemis running (this highlighting is removed ifmcompletes successfully). - Otherwise: Highlighting is removed for
rPre - rbeforemruns, and ifmcompletes successfully, thenrPre - ris highlighted as being type-checked.