{-# LANGUAGE CPP #-}
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.TypeChecking.Monad.Options
import Agda.Utils.Function
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
#include "undefined.h"
import Agda.Utils.Impossible
interestingCall :: Closure Call -> Bool
interestingCall cl = case clValue cl of
InferVar{} -> False
InferDef{} -> False
CheckArguments _ [] _ _ -> False
SetRange{} -> False
NoHighlighting{} -> False
_ -> True
traceCallM :: (MonadTCM tcm, MonadDebug tcm) => tcm Call -> tcm a -> tcm a
traceCallM mkCall m = flip traceCall m =<< mkCall
traceCall :: (MonadTCM tcm, MonadDebug tcm) => Call -> tcm a -> tcm a
traceCall mkCall m = do
let call = mkCall
callRange = getRange call
verboseS "check.ranges" 90 $
Strict.whenJust (rangeFile callRange) $ \f -> do
currentFile <- asks 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
cl <- liftTCM $ buildClosure call
let trace = local $ foldr (.) id $
[ \e -> e { envCall = Just cl } | interestingCall cl ] ++
[ \e -> e { envHighlightingRange = callRange }
| callRange /= noRange && highlightCall call || isNoHighlighting call ] ++
[ \e -> e { envRange = callRange } | callRange /= noRange ]
wrap <- ifM (do l <- envHighlightingLevel <$> ask
return (l == Interactive && highlightCall call))
(do oldRange <- envHighlightingRange <$> ask
return $ highlightAsTypeChecked oldRange callRange)
(return id)
wrap $ trace m
where
highlightCall call = case call of
CheckClause{} -> True
CheckPattern{} -> True
CheckLetBinding{} -> True
InferExpr{} -> True
CheckExprCall{} -> True
CheckDotPattern{} -> True
CheckPatternShadowing{} -> True
IsTypeCall{} -> True
IsType_{} -> True
InferVar{} -> True
InferDef{} -> True
CheckArguments{} -> True
CheckTargetType{} -> False
CheckDataDef{} -> True
CheckRecDef{} -> True
CheckConstructor{} -> True
CheckFunDefCall{} -> True
CheckPragma{} -> True
CheckPrimitive{} -> True
CheckIsEmpty{} -> True
CheckWithFunctionType{} -> True
CheckSectionApplication{} -> True
CheckNamedWhere{} -> False
ScopeCheckExpr{} -> False
ScopeCheckDeclaration{} -> False
ScopeCheckLHS{} -> False
NoHighlighting{} -> True
CheckProjection{} -> False
SetRange{} -> False
ModuleContents{} -> False
isNoHighlighting NoHighlighting{} = True
isNoHighlighting _ = False
getCurrentRange :: (MonadTCM tcm, MonadDebug tcm) => tcm Range
getCurrentRange = asks envRange
setCurrentRange :: (MonadTCM tcm, MonadDebug tcm, HasRange x)
=> x -> tcm a -> tcm a
setCurrentRange x = applyUnless (null r) $ traceCall $ SetRange r
where r = getRange x