{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.TypeChecking.Monad.Trace where
import Prelude hiding (null)
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Identity
import Control.Monad.Writer
import qualified Data.Set as Set
import Agda.Syntax.Position
import qualified Agda.Syntax.Position as P
import Agda.Interaction.Response
import Agda.Interaction.Highlighting.Precise
import Agda.Interaction.Highlighting.Range (rToR, minus)
import Agda.TypeChecking.Monad.Base
hiding (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype)
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.State
import Agda.Utils.Function
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty (prettyShow)
interestingCall :: Call -> Bool
interestingCall :: Call -> Bool
interestingCall = \case
InferVar{} -> Bool
False
InferDef{} -> Bool
False
CheckArguments Range
_ [] Type
_ Maybe Type
_ -> Bool
False
SetRange{} -> Bool
False
NoHighlighting{} -> Bool
False
CheckClause{} -> Bool
True
CheckLHS{} -> Bool
True
CheckPattern{} -> Bool
True
CheckPatternLinearityType{} -> Bool
True
CheckPatternLinearityValue{} -> Bool
True
CheckLetBinding{} -> Bool
True
InferExpr{} -> Bool
True
CheckExprCall{} -> Bool
True
CheckDotPattern{} -> Bool
True
IsTypeCall{} -> Bool
True
IsType_{} -> Bool
True
CheckArguments{} -> Bool
True
CheckMetaSolution{} -> Bool
True
CheckTargetType{} -> Bool
True
CheckDataDef{} -> Bool
True
CheckRecDef{} -> Bool
True
CheckConstructor{} -> Bool
True
CheckIApplyConfluence{} -> Bool
True
CheckConArgFitsIn{} -> Bool
True
CheckFunDefCall{} -> Bool
True
CheckPragma{} -> Bool
True
CheckPrimitive{} -> Bool
True
CheckIsEmpty{} -> Bool
True
CheckConfluence{} -> Bool
True
CheckModuleParameters{} -> Bool
True
CheckWithFunctionType{} -> Bool
True
CheckSectionApplication{} -> Bool
True
CheckNamedWhere{} -> Bool
True
ScopeCheckExpr{} -> Bool
True
ScopeCheckDeclaration{} -> Bool
True
ScopeCheckLHS{} -> Bool
True
CheckProjection{} -> Bool
True
ModuleContents{} -> Bool
True
class (MonadTCEnv m, ReadTCState m) => MonadTrace m where
traceCall :: Call -> m a -> m a
traceCall Call
call m a
m = do
cl <- Call -> m (Closure Call)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Call
call
traceClosureCall cl m
traceCallM :: m Call -> m a -> m a
traceCallM m Call
call m a
m = (Call -> m a -> m a) -> m a -> Call -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Call -> m a -> m a
forall a. Call -> m a -> m a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall m a
m (Call -> m a) -> m Call -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Call
call
traceCallCPS :: Call -> ((a -> m b) -> m b) -> ((a -> m b) -> m b)
traceCallCPS Call
call (a -> m b) -> m b
k a -> m b
ret = do
TCEnv{ envCall = mcall, envRange = r, envHighlightingRange = hr } <- m TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
traceCall call $ k $ \ a
a -> do
(TCEnv -> TCEnv) -> m b -> m b
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e{ envCall = mcall, envRange = r, envHighlightingRange = hr }) (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$
a -> m b
ret a
a
traceClosureCall :: Closure Call -> m a -> m a
printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
default printHighlightingInfo
:: (MonadTrans t, MonadTrace n, t n ~ m)
=> RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
r HighlightingInfo
i = n () -> t n ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n () -> t n ()) -> n () -> t n ()
forall a b. (a -> b) -> a -> b
$ RemoveTokenBasedHighlighting -> HighlightingInfo -> n ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
r HighlightingInfo
i
instance MonadTrace m => MonadTrace (IdentityT m) where
traceClosureCall :: forall a. Closure Call -> IdentityT m a -> IdentityT m a
traceClosureCall Closure Call
c IdentityT m a
f = m a -> IdentityT m a
forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (m a -> IdentityT m a) -> m a -> IdentityT m a
forall a b. (a -> b) -> a -> b
$ Closure Call -> m a -> m a
forall a. Closure Call -> m a -> m a
forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Closure Call
c (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ IdentityT m a -> m a
forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT IdentityT m a
f
instance MonadTrace m => MonadTrace (ReaderT r m) where
traceClosureCall :: forall a. Closure Call -> ReaderT r m a -> ReaderT r m a
traceClosureCall Closure Call
c ReaderT r m a
f = (r -> m a) -> ReaderT r m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((r -> m a) -> ReaderT r m a) -> (r -> m a) -> ReaderT r m a
forall a b. (a -> b) -> a -> b
$ \r
r -> Closure Call -> m a -> m a
forall a. Closure Call -> m a -> m a
forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Closure Call
c (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ ReaderT r m a -> r -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT r m a
f r
r
instance MonadTrace m => MonadTrace (StateT s m) where
traceClosureCall :: forall a. Closure Call -> StateT s m a -> StateT s m a
traceClosureCall Closure Call
c StateT s m a
f = (s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT (Closure Call -> m (a, s) -> m (a, s)
forall a. Closure Call -> m a -> m a
forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Closure Call
c (m (a, s) -> m (a, s)) -> (s -> m (a, s)) -> s -> m (a, s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT s m a
f)
instance (MonadTrace m, Monoid w) => MonadTrace (WriterT w m) where
traceClosureCall :: forall a. Closure Call -> WriterT w m a -> WriterT w m a
traceClosureCall Closure Call
c WriterT w m a
f = m (a, w) -> WriterT w m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (m (a, w) -> WriterT w m a) -> m (a, w) -> WriterT w m a
forall a b. (a -> b) -> a -> b
$ Closure Call -> m (a, w) -> m (a, w)
forall a. Closure Call -> m a -> m a
forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Closure Call
c (m (a, w) -> m (a, w)) -> m (a, w) -> m (a, w)
forall a b. (a -> b) -> a -> b
$ WriterT w m a -> m (a, w)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT WriterT w m a
f
instance MonadTrace m => MonadTrace (ExceptT e m) where
traceClosureCall :: forall a. Closure Call -> ExceptT e m a -> ExceptT e m a
traceClosureCall Closure Call
c ExceptT e m a
f = m (Either e a) -> ExceptT e m a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (m (Either e a) -> ExceptT e m a)
-> m (Either e a) -> ExceptT e m a
forall a b. (a -> b) -> a -> b
$ Closure Call -> m (Either e a) -> m (Either e a)
forall a. Closure Call -> m a -> m a
forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Closure Call
c (m (Either e a) -> m (Either e a))
-> m (Either e a) -> m (Either e a)
forall a b. (a -> b) -> a -> b
$ ExceptT e m a -> m (Either e a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT e m a
f
instance MonadTrace TCM where
traceClosureCall :: forall a. Closure Call -> TCM a -> TCM a
traceClosureCall Closure Call
cl TCM a
m = do
[Char] -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> m () -> m ()
verboseS [Char]
"check.ranges" VerboseLevel
90 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
Maybe RangeFile -> (RangeFile -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
Strict.whenJust (Range -> Maybe RangeFile
rangeFile Range
callRange) ((RangeFile -> TCM ()) -> TCM ())
-> (RangeFile -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \RangeFile
f -> do
currentFile <- (TCEnv -> Maybe AbsolutePath) -> TCMT IO (Maybe AbsolutePath)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe AbsolutePath
envCurrentPath
when (currentFile /= Just (rangeFilePath 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 :: TCM a -> TCM a
withCall = (TCEnv -> TCEnv) -> TCM a -> TCM a
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCM a -> TCM a)
-> (TCEnv -> TCEnv) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ ((TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv)
-> (TCEnv -> TCEnv) -> [TCEnv -> TCEnv] -> TCEnv -> TCEnv
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) TCEnv -> TCEnv
forall a. a -> a
id ([TCEnv -> TCEnv] -> TCEnv -> TCEnv)
-> [TCEnv -> TCEnv] -> TCEnv -> TCEnv
forall a b. (a -> b) -> a -> b
$ [[TCEnv -> TCEnv]] -> [TCEnv -> TCEnv]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[TCEnv -> TCEnv]] -> [TCEnv -> TCEnv])
-> [[TCEnv -> TCEnv]] -> [TCEnv -> TCEnv]
forall a b. (a -> b) -> a -> b
$
[ [ \TCEnv
e -> TCEnv
e { envCall = Just cl } | Call -> Bool
interestingCall Call
call ]
, [ \TCEnv
e -> TCEnv
e { envHighlightingRange = callRange }
| Bool
callHasRange Bool -> Bool -> Bool
&& Bool
highlightCall
Bool -> Bool -> Bool
|| Bool
isNoHighlighting
]
, [ \TCEnv
e -> TCEnv
e { envRange = callRange } | Bool
callHasRange ]
]
TCMT IO Bool -> TCM a -> TCM a -> TCM a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
highlightCall TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` do (HighlightingLevel
Interactive HighlightingLevel -> HighlightingLevel -> Bool
forall a. Eq a => a -> a -> Bool
==) (HighlightingLevel -> Bool)
-> (TCEnv -> HighlightingLevel) -> TCEnv -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> HighlightingLevel
envHighlightingLevel (TCEnv -> Bool) -> TCMT IO TCEnv -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC)
(TCM a -> TCM a
withCall TCM a
m)
(TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
oldRange <- TCEnv -> Range
envHighlightingRange (TCEnv -> Range) -> TCMT IO TCEnv -> TCMT IO Range
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
highlightAsTypeChecked oldRange callRange $
withCall m
where
call :: Call
call = Closure Call -> Call
forall a. Closure a -> a
clValue Closure Call
cl
callRange :: Range
callRange = Call -> Range
forall a. HasRange a => a -> Range
getRange Call
call
callHasRange :: Bool
callHasRange = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Range -> Bool
forall a. Null a => a -> Bool
null Range
callRange
highlightCall :: Bool
highlightCall = case Call
call of
CheckClause{} -> Bool
True
CheckLHS{} -> Bool
True
CheckPattern{} -> Bool
True
CheckPatternLinearityType{} -> Bool
False
CheckPatternLinearityValue{} -> Bool
False
CheckLetBinding{} -> Bool
True
InferExpr{} -> Bool
True
CheckExprCall{} -> Bool
True
CheckDotPattern{} -> Bool
True
IsTypeCall{} -> Bool
True
IsType_{} -> Bool
True
InferVar{} -> Bool
True
InferDef{} -> Bool
True
CheckArguments{} -> Bool
True
CheckMetaSolution{} -> Bool
False
CheckTargetType{} -> Bool
False
CheckDataDef{} -> Bool
True
CheckRecDef{} -> Bool
True
CheckConstructor{} -> Bool
True
CheckConArgFitsIn{} -> Bool
False
CheckFunDefCall Range
_ QName
_ [Clause]
_ Bool
h -> Bool
h
CheckPragma{} -> Bool
True
CheckPrimitive{} -> Bool
True
CheckIsEmpty{} -> Bool
True
CheckConfluence{} -> Bool
False
CheckIApplyConfluence{} -> Bool
False
CheckModuleParameters{} -> Bool
False
CheckWithFunctionType{} -> Bool
True
CheckSectionApplication{} -> Bool
True
CheckNamedWhere{} -> Bool
False
ScopeCheckExpr{} -> Bool
False
ScopeCheckDeclaration{} -> Bool
False
ScopeCheckLHS{} -> Bool
False
NoHighlighting{} -> Bool
True
CheckProjection{} -> Bool
False
SetRange{} -> Bool
False
ModuleContents{} -> Bool
False
isNoHighlighting :: Bool
isNoHighlighting = case Call
call of
NoHighlighting{} -> Bool
True
Call
_ -> Bool
False
printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
printHighlightingInfo RemoveTokenBasedHighlighting
remove HighlightingInfo
info = do
modToSrc <- Lens' TCState (Map TopLevelModuleName AbsolutePath)
-> TCMT IO (Map TopLevelModuleName AbsolutePath)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map TopLevelModuleName AbsolutePath
-> f (Map TopLevelModuleName AbsolutePath))
-> TCState -> f TCState
Lens' TCState (Map TopLevelModuleName AbsolutePath)
stModuleToSource
method <- viewTC eHighlightingMethod
reportS "highlighting" 50
[ "Printing highlighting info:"
, show info
, " modToSrc = " ++ show modToSrc
]
unless (null info) $ do
appInteractionOutputCallback $
Resp_HighlightingInfo info remove method modToSrc
getCurrentRange :: MonadTCEnv m => m Range
getCurrentRange :: forall (m :: * -> *). MonadTCEnv m => m Range
getCurrentRange = (TCEnv -> Range) -> m Range
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Range
envRange
setCurrentRange :: (MonadTrace m, HasRange x) => x -> m a -> m a
setCurrentRange :: forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange x
x = Bool -> (m a -> m a) -> m a -> m a
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (Range -> Bool
forall a. Null a => a -> Bool
null Range
r) ((m a -> m a) -> m a -> m a) -> (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Call -> m a -> m a
forall a. Call -> m a -> m a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Call -> m a -> m a) -> Call -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Range -> Call
SetRange Range
r
where r :: Range
r = x -> Range
forall a. HasRange a => a -> Range
getRange x
x
highlightAsTypeChecked
:: (MonadTrace m)
=> Range
-> Range
-> m a
-> m a
highlightAsTypeChecked :: forall (m :: * -> *) a.
MonadTrace m =>
Range -> Range -> m a -> m a
highlightAsTypeChecked Range
rPre Range
r m a
m
| Range
r Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
/= Range
forall a. Range' a
noRange Bool -> Bool -> Bool
&& Ranges
delta Ranges -> Ranges -> Bool
forall a. Eq a => a -> a -> Bool
== Ranges
rPre' = Ranges -> Aspects -> Aspects -> m a
wrap Ranges
r' Aspects
highlight Aspects
clear
| Bool
otherwise = Ranges -> Aspects -> Aspects -> m a
wrap Ranges
delta Aspects
clear Aspects
highlight
where
rPre' :: Ranges
rPre' = Range -> Ranges
rToR (Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
rPre)
r' :: Ranges
r' = Range -> Ranges
rToR (Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
r)
delta :: Ranges
delta = Ranges
rPre' Ranges -> Ranges -> Ranges
`minus` Ranges
r'
clear :: Aspects
clear = Aspects
forall a. Monoid a => a
mempty
highlight :: Aspects
highlight = Aspects
parserBased { otherAspects = Set.singleton TypeChecks }
wrap :: Ranges -> Aspects -> Aspects -> m a
wrap Ranges
rs Aspects
x Aspects
y = do
Ranges -> Aspects -> m ()
forall {m :: * -> *}. MonadTrace m => Ranges -> Aspects -> m ()
p Ranges
rs Aspects
x
v <- m a
m
p rs y
return v
where
p :: Ranges -> Aspects -> m ()
p Ranges
rs Aspects
x = RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (Ranges -> Aspects -> HighlightingInfo
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
singleton Ranges
rs Aspects
x)