module Agda.TypeChecking.Monad.Trace where
import Prelude hiding (null)
import Control.Monad.Reader
import {-# SOURCE #-} Agda.Interaction.Highlighting.Generate
(highlightAsTypeChecked)
import Agda.Syntax.Position
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug
import Agda.Utils.Function
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
interestingCall :: Call -> Bool
interestingCall = \case
InferVar{} -> False
InferDef{} -> False
CheckArguments _ [] _ _ -> False
SetRange{} -> False
NoHighlighting{} -> False
CheckClause{} -> True
CheckLHS{} -> True
CheckPattern{} -> True
CheckLetBinding{} -> True
InferExpr{} -> True
CheckExprCall{} -> True
CheckDotPattern{} -> True
IsTypeCall{} -> True
IsType_{} -> True
CheckArguments{} -> True
CheckMetaSolution{} -> True
CheckTargetType{} -> True
CheckDataDef{} -> True
CheckRecDef{} -> True
CheckConstructor{} -> True
CheckConstructorFitsIn{} -> True
CheckFunDefCall{} -> True
CheckPragma{} -> True
CheckPrimitive{} -> True
CheckIsEmpty{} -> True
CheckConfluence{} -> True
CheckWithFunctionType{} -> True
CheckSectionApplication{} -> True
CheckNamedWhere{} -> True
ScopeCheckExpr{} -> True
ScopeCheckDeclaration{} -> True
ScopeCheckLHS{} -> True
CheckProjection{} -> True
ModuleContents{} -> True
traceCallM :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => tcm Call -> tcm a -> tcm a
traceCallM call m = flip traceCall m =<< call
traceCallCPS :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm)
=> Call
-> ((a -> tcm b) -> tcm b)
-> ((a -> tcm b) -> tcm b)
traceCallCPS call k ret = do
mcall <- asksTC envCall
traceCall call $ k $ \ a -> do
maybe id traceClosureCall mcall $ ret a
traceCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> tcm a -> tcm a
traceCall call m = do
cl <- liftTCM $ buildClosure call
traceClosureCall cl m
traceClosureCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Closure Call -> tcm a -> tcm a
traceClosureCall cl m = do
verboseS "check.ranges" 90 $
Strict.whenJust (rangeFile callRange) $ \f -> do
currentFile <- asksTC envCurrentPath
when (currentFile /= Just f) $ do
reportSLn "check.ranges" 90 $
prettyShow call ++
" is setting the current range to " ++ show callRange ++
" which is outside of the current file " ++ show currentFile
let withCall = localTC $ foldr (.) id $ concat $
[ [ \e -> e { envCall = Just cl } | interestingCall call ]
, [ \e -> e { envHighlightingRange = callRange }
| callHasRange && highlightCall
|| isNoHighlighting
]
, [ \e -> e { envRange = callRange } | callHasRange ]
]
ifNotM (pure highlightCall `and2M` do (Interactive ==) . envHighlightingLevel <$> askTC)
(withCall m)
$ do
oldRange <- envHighlightingRange <$> askTC
highlightAsTypeChecked oldRange callRange $
withCall m
where
call = clValue cl
callRange = getRange call
callHasRange = not $ null callRange
highlightCall = case call of
CheckClause{} -> True
CheckLHS{} -> True
CheckPattern{} -> True
CheckLetBinding{} -> True
InferExpr{} -> True
CheckExprCall{} -> True
CheckDotPattern{} -> True
IsTypeCall{} -> True
IsType_{} -> True
InferVar{} -> True
InferDef{} -> True
CheckArguments{} -> True
CheckMetaSolution{} -> False
CheckTargetType{} -> False
CheckDataDef{} -> True
CheckRecDef{} -> True
CheckConstructor{} -> True
CheckConstructorFitsIn{} -> False
CheckFunDefCall{} -> True
CheckPragma{} -> True
CheckPrimitive{} -> True
CheckIsEmpty{} -> True
CheckConfluence{} -> False
CheckWithFunctionType{} -> True
CheckSectionApplication{} -> True
CheckNamedWhere{} -> False
ScopeCheckExpr{} -> False
ScopeCheckDeclaration{} -> False
ScopeCheckLHS{} -> False
NoHighlighting{} -> True
CheckProjection{} -> False
SetRange{} -> False
ModuleContents{} -> False
isNoHighlighting = case call of
NoHighlighting{} -> True
_ -> False
getCurrentRange :: MonadTCEnv m => m Range
getCurrentRange = asksTC envRange
setCurrentRange :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x)
=> x -> tcm a -> tcm a
setCurrentRange x = applyUnless (null r) $ traceCall $ SetRange r
where r = getRange x