Agda-2.7.0.1: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Monad.Trace

Contents

Synopsis

Trace

interestingCall :: Call -> Bool Source #

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

Minimal complete definition

traceClosureCall

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

Instances details
MonadTrace TCM Source # 
Instance details

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 # 
Instance details

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 # 
Instance details

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 # 
Instance details

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 # 
Instance details

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 # 
Instance details

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