ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Monad.Trace

Contents

Synopsis

Trace

valueinterestingCall :: Call -> Bool

classclass (MonadTCEnv m, ReadTCState m) => MonadTrace (m :: Type -> Type) where

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
Like traceCall, but resets envCall and the current ranges to the previous values in the continuation.
traceClosureCall :: Closure Call -> m a -> m a
printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
Lispify and print the given highlighting information.

Instances7MonadTrace, …

MonadTrace TCMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Trace
MonadTrace m => MonadTrace (MaybeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Trace
MonadTrace m => MonadTrace (ExceptT e m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Trace
MonadTrace m => MonadTrace (IdentityT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Trace
MonadTrace m => MonadTrace (ReaderT r m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Trace
MonadTrace m => MonadTrace (StateT s m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Trace
(MonadTrace m, Monoid w) => MonadTrace (WriterT w m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Trace

valuetraceCallCPS' :: MonadTrace m => Call -> (m b -> m b) -> m b -> m b

valuegetCurrentRange :: MonadTCEnv m => m Range

valuesetCurrentRange :: (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).

valuehighlightAsTypeChecked

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.

valuerunPM :: PM a -> TCM a

Running the Parse monad, raising parser warnings.

valuerunPMDropWarnings :: PM a -> TCM a

Running the Parse monad, dropping parser warnings.