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
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 => tcm Call -> tcm a -> tcm a
traceCallM mkCall m = flip traceCall m =<< mkCall
traceCall :: MonadTCM tcm => Call -> tcm a -> tcm a
traceCall mkCall m = do
let call = mkCall
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 $
prettyShow call ++
" 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
traceCallCPS :: MonadTCM tcm => Call -> (r -> tcm a) -> ((r -> tcm a) -> tcm b) -> tcm b
traceCallCPS mkCall ret cc = traceCall mkCall (cc ret)
traceCallCPS_ :: MonadTCM tcm => 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