module Agda.TypeChecking.Monad.Trace where
import Prelude hiding (null)
import Control.Monad.Reader
import Agda.Interaction.Highlighting.Generate
(highlightAsTypeChecked)
import Agda.Syntax.Position
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Options
import Agda.Utils.Function
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
#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 => tcm (Maybe r -> Call) -> tcm a -> tcm a
traceCallM mkCall m = flip traceCall m =<< mkCall
traceCall :: MonadTCM tcm => (Maybe r -> Call) -> tcm a -> tcm a
traceCall mkCall m = do
let call = mkCall Nothing
callRange = getRange call
unlessNull callRange $ \ (Range is) ->
unlessNull (mapMaybe srcFile $ map iStart is ++ map iEnd is) $ \ files -> do
whenJustM (asks envCurrentPath) $ \ currentFile -> do
unlessNull (filter (/= currentFile) files) $ \ wrongFiles -> do
reportSLn "impossible" 10 $
"Someone is trying to set the current range to " ++ show callRange ++
" which is outside of the current file " ++ show currentFile
__IMPOSSIBLE__
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
CheckDataDef _ _ _ _ _ -> True
CheckRecDef _ _ _ _ _ -> True
CheckConstructor _ _ _ _ _ -> True
CheckFunDef _ _ _ _ -> True
CheckPragma _ _ _ -> True
CheckPrimitive _ _ _ _ -> True
CheckIsEmpty _ _ _ -> True
CheckWithFunctionType _ _ -> True
CheckSectionApplication _ _ _ _ -> True
ScopeCheckExpr _ _ -> False
ScopeCheckDeclaration _ _ -> False
ScopeCheckLHS _ _ _ -> False
NoHighlighting _ -> True
SetRange _ _ -> False
isNoHighlighting (NoHighlighting {}) = True
isNoHighlighting _ = False
traceCall_ :: MonadTCM tcm => (Maybe () -> Call) -> tcm r -> tcm r
traceCall_ mkCall = traceCall (mkCall . fmap (const ()))
traceCallCPS :: MonadTCM tcm => (Maybe r -> Call) -> (r -> tcm a) -> ((r -> tcm a) -> tcm b) -> tcm b
traceCallCPS mkCall ret cc = traceCall mkCall (cc ret)
traceCallCPS_ :: MonadTCM tcm => (Maybe () -> Call) -> tcm a -> (tcm a -> tcm b) -> tcm b
traceCallCPS_ mkCall ret cc =
traceCallCPS mkCall (const ret) (\k -> cc $ k ())
getCurrentRange :: TCM Range
getCurrentRange = asks envRange
setCurrentRange :: HasRange x => x -> TCM a -> TCM a
setCurrentRange x = applyUnless (null r) $ traceCall $ SetRange r
where r = getRange x