Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Monad.Trace

Contents

Trace
Warnings in the parser

Synopsis

interestingCall :: Call -> Bool
class (MonadTCEnv m, ReadTCState m) => MonadTrace (m :: Type -> Type) 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 ()
traceCallCPS' :: MonadTrace m => Call -> (m b -> m b) -> m b -> m b
getCurrentRange :: MonadTCEnv m => m Range
setCurrentRange :: (MonadTrace m, HasRange x) => x -> m a -> m a
highlightAsTypeChecked :: MonadTrace m => Range -> Range -> m a -> m a
runPM :: PM a -> TCM a
runPMDropWarnings :: PM a -> TCM a

Trace

interestingCall :: Call -> Bool Source #

class (MonadTCEnv m, ReadTCState m) => MonadTrace (m :: Type -> Type) 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 :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (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 (MaybeT m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Trace Methods traceCall :: Call -> MaybeT m a -> MaybeT m a Source # traceCallM :: MaybeT m Call -> MaybeT m a -> MaybeT m a Source # traceCallCPS :: Call -> ((a -> MaybeT m b) -> MaybeT m b) -> (a -> MaybeT m b) -> MaybeT m b Source # traceClosureCall :: Closure Call -> MaybeT m a -> MaybeT m a Source # printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> MaybeT m () 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 #

traceCallCPS' :: MonadTrace m => Call -> (m b -> m b) -> m b -> m b 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.

Warnings in the parser

runPM :: PM a -> TCM a Source #

Running the Parse monad, raising parser warnings.

runPMDropWarnings :: PM a -> TCM a Source #

Running the Parse monad, dropping parser warnings.