Agda.TypeChecking.Monad.Trace

Trace

interestingCall :: Call -> Bool

class (MonadTCEnv m, ReadTCState m) => MonadTrace m where

Minimal complete definition

traceClosureCall

Methods

traceCall :: Call -> m a -> m a

Record a function call in the trace.

traceCallM :: m Call -> m a -> m a

traceCallCPS :: Call -> ((a -> m b) -> m b) -> (a -> m b) -> m b

Reset envCall to previous value in the continuation.

Caveat: if the last traceCall did not set an interestingCall, for example, only set the Range' with Call, we will revert to the last interesting call.

traceClosureCall :: Closure Call -> m a -> m a

printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()

Lispify and print the given highlighting information.

default printHighlightingInfo :: (MonadTrans t, MonadTrace n, t n ~ m) => RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()

Instances

MonadTrace TCM

Defined in Agda.TypeChecking.Monad.Trace

Methods

traceCall :: Call -> TCM a -> TCM a

traceCallM :: TCM Call -> TCM a -> TCM a

traceCallCPS :: Call -> ((a -> TCM b) -> TCM b) -> (a -> TCM b) -> TCM b

traceClosureCall :: Closure Call -> TCM a -> TCM a

printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()

MonadTrace m => MonadTrace (ExceptT e m)

Defined in Agda.TypeChecking.Monad.Trace

Methods

traceCall :: Call -> ExceptT e m a -> ExceptT e m a

traceCallM :: ExceptT e m Call -> ExceptT e m a -> ExceptT e m a

traceCallCPS :: Call -> ((a -> ExceptT e m b) -> ExceptT e m b) -> (a -> ExceptT e m b) -> ExceptT e m b

traceClosureCall :: Closure Call -> ExceptT e m a -> ExceptT e m a

printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> ExceptT e m ()

MonadTrace m => MonadTrace (IdentityT m)

Defined in Agda.TypeChecking.Monad.Trace

Methods

traceCall :: Call -> IdentityT m a -> IdentityT m a

traceCallM :: IdentityT m Call -> IdentityT m a -> IdentityT m a

traceCallCPS :: Call -> ((a -> IdentityT m b) -> IdentityT m b) -> (a -> IdentityT m b) -> IdentityT m b

traceClosureCall :: Closure Call -> IdentityT m a -> IdentityT m a

printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> IdentityT m ()

MonadTrace m => MonadTrace (ReaderT r m)

Defined in Agda.TypeChecking.Monad.Trace

Methods

traceCall :: Call -> ReaderT r m a -> ReaderT r m a

traceCallM :: ReaderT r m Call -> ReaderT r m a -> ReaderT r m a

traceCallCPS :: Call -> ((a -> ReaderT r m b) -> ReaderT r m b) -> (a -> ReaderT r m b) -> ReaderT r m b

traceClosureCall :: Closure Call -> ReaderT r m a -> ReaderT r m a

printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> ReaderT r m ()

MonadTrace m => MonadTrace (StateT s m)

Defined in Agda.TypeChecking.Monad.Trace

Methods

traceCall :: Call -> StateT s m a -> StateT s m a

traceCallM :: StateT s m Call -> StateT s m a -> StateT s m a

traceCallCPS :: Call -> ((a -> StateT s m b) -> StateT s m b) -> (a -> StateT s m b) -> StateT s m b

traceClosureCall :: Closure Call -> StateT s m a -> StateT s m a

printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> StateT s m ()

(MonadTrace m, Monoid w) => MonadTrace (WriterT w m)

Defined in Agda.TypeChecking.Monad.Trace

Methods

traceCall :: Call -> WriterT w m a -> WriterT w m a

traceCallM :: WriterT w m Call -> WriterT w m a -> WriterT w m a

traceCallCPS :: Call -> ((a -> WriterT w m b) -> WriterT w m b) -> (a -> WriterT w m b) -> WriterT w m b

traceClosureCall :: Closure Call -> WriterT w m a -> WriterT w m a

printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> WriterT w m ()

getCurrentRange :: MonadTCEnv m => m Range

setCurrentRange :: (MonadTrace m, HasRange x) => x -> m a -> m a

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

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 r is non-empty and not a sub-range of rPre (after continuousPerLine has been applied to both): r is highlighted as being type-checked while m is running (this highlighting is removed if m completes successfully).
• Otherwise: Highlighting is removed for rPre - r before m runs, and if m completes successfully, then rPre - r is highlighted as being type-checked.