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

Safe Haskell | None

Agda.TypeChecking.Monad.Trace

Contents

- Trace

Synopsis

- interestingCall :: Closure Call -> Bool
- traceCallM :: MonadTCM tcm => tcm (Maybe r -> Call) -> tcm a -> tcm a
- traceCall :: MonadTCM tcm => (Maybe r -> Call) -> tcm a -> tcm a
- traceCall_ :: MonadTCM tcm => (Maybe () -> Call) -> tcm r -> tcm r
- traceCallCPS :: MonadTCM tcm => (Maybe r -> Call) -> (r -> tcm a) -> ((r -> tcm a) -> tcm b) -> tcm b
- traceCallCPS_ :: MonadTCM tcm => (Maybe () -> Call) -> tcm a -> (tcm a -> tcm b) -> tcm b
- getCurrentRange :: TCM Range
- setCurrentRange :: Range -> TCM a -> TCM a

# Trace

interestingCall :: Closure Call -> Bool

traceCallM :: MonadTCM tcm => tcm (Maybe r -> Call) -> tcm a -> tcm a

traceCall :: MonadTCM tcm => (Maybe r -> Call) -> tcm a -> tcm a

Record a function call in the trace.

traceCall_ :: MonadTCM tcm => (Maybe () -> Call) -> tcm r -> tcm r

traceCallCPS :: MonadTCM tcm => (Maybe r -> Call) -> (r -> tcm a) -> ((r -> tcm a) -> tcm b) -> tcm b

traceCallCPS_ :: MonadTCM tcm => (Maybe () -> Call) -> tcm a -> (tcm a -> tcm b) -> tcm b

getCurrentRange :: TCM Range

setCurrentRange :: Range -> TCM a -> TCM a