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.Utils.Pretty (prettyShow)

---------------------------------------------------------------------------
-- * Trace
---------------------------------------------------------------------------

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
    -- Andreas, 2019-08-07, expanded catch-all pattern.
    -- The previous presence of a catch-all raises the following question:
    -- are all of the following really interesting?
    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
    CheckConstructorFitsIn{}  -> Bool
True
    CheckFunDefCall{}         -> Bool
True
    CheckPragma{}             -> Bool
True
    CheckPrimitive{}          -> Bool
True
    CheckIsEmpty{}            -> Bool
True
    CheckConfluence{}         -> 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

  -- | Record a function call in the trace.
  traceCall :: Call -> m a -> m a
  traceCall Call
call m a
m = do
    Closure Call
cl <- forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Call
call
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Closure Call
cl m a
m

  traceCallM :: m Call -> m a -> m a
  traceCallM m Call
call m a
m = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall m a
m forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Call
call

  -- | Reset 'envCall' to previous value in the continuation.
  --
  -- Caveat: if the last 'traceCall' did not set an 'interestingCall',
  -- for example, only set the 'Range' with 'SetRange',
  -- we will revert to the last interesting 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
    Maybe (Closure Call)
mcall <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe (Closure Call)
envCall
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall Call
call forall a b. (a -> b) -> a -> b
$ (a -> m b) -> m b
k forall a b. (a -> b) -> a -> b
$ \ a
a -> do
      forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Maybe (Closure Call)
mcall forall a b. (a -> b) -> a -> b
$ a -> m b
ret a
a

  traceClosureCall :: Closure Call -> m a -> m a

  -- | Lispify and print the given highlighting information.
  printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()

  default printHighlightingInfo
    :: (MonadTrans t, MonadTrace n, t n ~ m)
    => RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
  printHighlightingInfo RemoveTokenBasedHighlighting
r HighlightingInfo
i = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 = forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Closure Call
c forall a b. (a -> b) -> a -> b
$ 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 = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ \r
r -> forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Closure Call
c forall a b. (a -> b) -> a -> b
$ 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 = forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT (forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Closure Call
c forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Closure Call
c forall a b. (a -> b) -> a -> b
$ 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 = forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Closure Call
c forall a b. (a -> b) -> a -> b
$ 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
    -- Andreas, 2016-09-13 issue #2177
    -- Since the fix of #2092 we may report an error outside the current file.
    -- (For instance, if we import a module which then happens to have the
    -- wrong name.)
    -- Thus, we no longer crash, but just report the alien range.
    -- -- Andreas, 2015-02-09 Make sure we do not set a range
    -- -- outside the current file
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> m () -> m ()
verboseS [Char]
"check.ranges" VerboseLevel
90 forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
Strict.whenJust (Range -> Maybe RangeFile
rangeFile Range
callRange) forall a b. (a -> b) -> a -> b
$ \RangeFile
f -> do
        Maybe AbsolutePath
currentFile <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe AbsolutePath
envCurrentPath
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe AbsolutePath
currentFile forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just (RangeFile -> AbsolutePath
rangeFilePath RangeFile
f)) forall a b. (a -> b) -> a -> b
$ do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"check.ranges" VerboseLevel
90 forall a b. (a -> b) -> a -> b
$
            forall a. Pretty a => a -> [Char]
prettyShow Call
call forall a. [a] -> [a] -> [a]
++
            [Char]
" is setting the current range to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Range
callRange forall a. [a] -> [a] -> [a]
++
            [Char]
" which is outside of the current file " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Maybe AbsolutePath
currentFile

    -- Compute update to 'Range' and 'Call' components of 'TCEnv'.
    let withCall :: TCM a -> TCM a
withCall = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
          [ [ \TCEnv
e -> TCEnv
e { envCall :: Maybe (Closure Call)
envCall = forall a. a -> Maybe a
Just Closure Call
cl } | Call -> Bool
interestingCall Call
call ]
          , [ \TCEnv
e -> TCEnv
e { envHighlightingRange :: Range
envHighlightingRange = Range
callRange }
            | Bool
callHasRange Bool -> Bool -> Bool
&& Bool
highlightCall
              Bool -> Bool -> Bool
|| Bool
isNoHighlighting
            ]
          , [ \TCEnv
e -> TCEnv
e { envRange :: Range
envRange = Range
callRange } | Bool
callHasRange ]
          ]

    -- For interactive highlighting, also wrap computation @m@ in 'highlightAsTypeChecked':
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
highlightCall forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` do (HighlightingLevel
Interactive forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> HighlightingLevel
envHighlightingLevel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC)
      {-then-} (TCM a -> TCM a
withCall TCM a
m)
      {-else-} forall a b. (a -> b) -> a -> b
$ do
        Range
oldRange <- TCEnv -> Range
envHighlightingRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
        forall (m :: * -> *) a.
MonadTrace m =>
Range -> Range -> m a -> m a
highlightAsTypeChecked Range
oldRange Range
callRange forall a b. (a -> b) -> a -> b
$
          TCM a -> TCM a
withCall TCM a
m
    where
    call :: Call
call = forall a. Closure a -> a
clValue Closure Call
cl
    callRange :: Range
callRange = forall a. HasRange a => a -> Range
getRange Call
call
    callHasRange :: Bool
callHasRange = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null Range
callRange

    -- Should the given call trigger interactive highlighting?
    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
      CheckConstructorFitsIn{}  -> 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
      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
    Map TopLevelModuleName AbsolutePath
modToSrc <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map TopLevelModuleName AbsolutePath) TCState
stModuleToSource
    HighlightingMethod
method   <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' HighlightingMethod TCEnv
eHighlightingMethod
    forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> VerboseLevel -> a -> m ()
reportS [Char]
"highlighting" VerboseLevel
50
      [ [Char]
"Printing highlighting info:"
      , forall a. Show a => a -> [Char]
show HighlightingInfo
info
      , [Char]
"  modToSrc = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Map TopLevelModuleName AbsolutePath
modToSrc
      ]
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null HighlightingInfo
info) forall a b. (a -> b) -> a -> b
$ do
      Response -> TCM ()
appInteractionOutputCallback forall a b. (a -> b) -> a -> b
$
          HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> Map TopLevelModuleName AbsolutePath
-> Response
Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method Map TopLevelModuleName AbsolutePath
modToSrc


getCurrentRange :: MonadTCEnv m => m Range
getCurrentRange :: forall (m :: * -> *). MonadTCEnv m => m Range
getCurrentRange = forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Range
envRange

-- | Sets the current range (for error messages etc.) to the range
--   of the given object, if it has a range (i.e., its range is not 'noRange').
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 = forall a. Bool -> (a -> a) -> a -> a
applyUnless (forall a. Null a => a -> Bool
null Range
r) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall forall a b. (a -> b) -> a -> b
$ Range -> Call
SetRange Range
r
  where r :: Range
r = forall a. HasRange a => a -> Range
getRange x
x

-- | @highlightAsTypeChecked rPre r m@ runs @m@ and returns its
--   result. Additionally, some code may be highlighted:
--
-- * If @r@ is non-empty and not a sub-range of @rPre@ (after
--   'P.continuousPerLine' has been applied to both): @r@ is
--   highlighted as being type-checked while @m@ is running (this
--   highlighting is removed if @m@ completes /successfully/).
--
-- * Otherwise: Highlighting is removed for @rPre - r@ before @m@
--   runs, and if @m@ completes successfully, then @rPre - r@ is
--   highlighted as being type-checked.

highlightAsTypeChecked
  :: (MonadTrace m)
  => Range   -- ^ @rPre@
  -> Range   -- ^ @r@
  -> 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 forall a. Eq a => a -> a -> Bool
/= forall a. Range' a
noRange Bool -> Bool -> Bool
&& Ranges
delta 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 (forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
rPre)
  r' :: Ranges
r'        = Range -> Ranges
rToR (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     = forall a. Monoid a => a
mempty
  highlight :: Aspects
highlight = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = forall a. a -> Set a
Set.singleton OtherAspect
TypeChecks }

  wrap :: Ranges -> Aspects -> Aspects -> m a
wrap Ranges
rs Aspects
x Aspects
y = do
    forall {m :: * -> *}. MonadTrace m => Ranges -> Aspects -> m ()
p Ranges
rs Aspects
x
    a
v <- m a
m
    forall {m :: * -> *}. MonadTrace m => Ranges -> Aspects -> m ()
p Ranges
rs Aspects
y
    forall (m :: * -> *) a. Monad m => a -> m a
return a
v
    where
    p :: Ranges -> Aspects -> m ()
p Ranges
rs Aspects
x = forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (forall a m. IsBasicRangeMap a m => Ranges -> a -> m
singleton Ranges
rs Aspects
x)