Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Trace

Contents

Synopsis

Trace

interestingCall :: Call -> Bool Source #

traceCallM :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => tcm Call -> tcm a -> tcm a Source #

traceCallCPS :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> ((a -> tcm b) -> tcm b) -> (a -> tcm b) -> tcm b Source #

Reset envCall to previous value in the continuation.

Caveat: if the last traceCall did not set an interestingCall, for example, only set the Range with SetRange, we will revert to the last interesting call.

traceCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> tcm a -> tcm a Source #

Record a function call in the trace.

traceClosureCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Closure Call -> tcm a -> tcm a Source #

getCurrentRange :: MonadTCEnv m => m Range Source #

setCurrentRange :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) => x -> tcm a -> tcm 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

:: (MonadTCM tcm, ReadTCState tcm) 
=> Range
rPre
-> Range
r
-> tcm a 
-> tcm 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.

printHighlightingInfo :: (MonadTCM tcm, ReadTCState tcm) => RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm () Source #

Lispify and print the given highlighting information.