Agda-2.8.0: A dependently typed functional programming language and proof assistant

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.