{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Monad.Debug where
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Maybe
import Control.Monad.Writer
import Data.Maybe
import Data.Monoid ( Monoid, mempty, mappend )
import Data.Semigroup ( Semigroup, (<>), Any(..) )
import Data.Traversable
import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.Base
import {-# SOURCE #-} Agda.TypeChecking.Monad.Options
import Agda.Interaction.Response
import Agda.Utils.Except
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
class (Functor m, Applicative m, Monad m) => MonadDebug m where
displayDebugMessage :: Int -> String -> m ()
displayDebugMessage n s = traceDebugMessage n s $ return ()
traceDebugMessage :: Int -> String -> m a -> m a
traceDebugMessage n s cont = displayDebugMessage n s >> cont
formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> m String
instance (MonadIO m) => MonadDebug (TCMT m) where
displayDebugMessage n s = liftTCM $ do
cb <- getsTC $ stInteractionOutputCallback . stPersistentState
cb (Resp_RunningInfo n s)
formatDebugMessage k n d = liftTCM $
show <$> d `catchError` \ err ->
(\ s -> (sep $ map text
[ "Printing debug message"
, k ++ ":" ++show n
, "failed due to error:" ]) $$
(nest 2 $ text s)) <$> prettyError err
instance MonadDebug m => MonadDebug (ExceptT e m) where
displayDebugMessage n s = lift $ displayDebugMessage n s
formatDebugMessage k n d = lift $ formatDebugMessage k n d
instance MonadDebug m => MonadDebug (ListT m) where
displayDebugMessage n s = lift $ displayDebugMessage n s
formatDebugMessage k n d = lift $ formatDebugMessage k n d
instance MonadDebug m => MonadDebug (MaybeT m) where
displayDebugMessage n s = lift $ displayDebugMessage n s
formatDebugMessage k n d = lift $ formatDebugMessage k n d
instance MonadDebug m => MonadDebug (ReaderT r m) where
displayDebugMessage n s = lift $ displayDebugMessage n s
formatDebugMessage k n d = lift $ formatDebugMessage k n d
instance MonadDebug m => MonadDebug (StateT s m) where
displayDebugMessage n s = lift $ displayDebugMessage n s
formatDebugMessage k n d = lift $ formatDebugMessage k n d
instance (MonadDebug m, Monoid w) => MonadDebug (WriterT w m) where
displayDebugMessage n s = lift $ displayDebugMessage n s
formatDebugMessage k n d = lift $ formatDebugMessage k n d
{-# SPECIALIZE reportS :: VerboseKey -> Int -> String -> TCM () #-}
reportS :: (HasOptions m, MonadDebug m, MonadTCEnv m)
=> VerboseKey -> Int -> String -> m ()
reportS k n s = verboseS k n $ displayDebugMessage n s
{-# SPECIALIZE reportSLn :: VerboseKey -> Int -> String -> TCM () #-}
reportSLn :: (HasOptions m, MonadDebug m, MonadTCEnv m)
=> VerboseKey -> Int -> String -> m ()
reportSLn k n s = verboseS k n $
displayDebugMessage n (s ++ "\n")
{-# SPECIALIZE reportSDoc :: VerboseKey -> Int -> TCM Doc -> TCM () #-}
reportSDoc :: (HasOptions m, MonadDebug m, MonadTCEnv m)
=> VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc k n d = verboseS k n $ do
displayDebugMessage n . (++ "\n") =<< formatDebugMessage k n (locallyTC eIsDebugPrinting (const True) d)
unlessDebugPrinting :: MonadTCM m => m () -> m ()
unlessDebugPrinting = unlessM (asksTC envIsDebugPrinting)
traceSLn :: (HasOptions m, MonadDebug m)
=> VerboseKey -> Int -> String -> m a -> m a
traceSLn k n s cont = ifNotM (hasVerbosity k n) cont $ do
traceDebugMessage n (s ++ "\n") cont
traceSDoc :: (HasOptions m, MonadDebug m)
=> VerboseKey -> Int -> TCM Doc -> m a -> m a
traceSDoc k n d cont = ifNotM (hasVerbosity k n) cont $ do
s <- formatDebugMessage k n $ locallyTC eIsDebugPrinting (const True) d
traceDebugMessage n (s ++ "\n") cont
{-# SPECIALIZE verboseBracket :: VerboseKey -> Int -> String -> TCM a -> TCM a #-}
verboseBracket :: (HasOptions m, MonadDebug m, MonadError err m)
=> VerboseKey -> Int -> String -> m a -> m a
verboseBracket k n s m = ifNotM (hasVerbosity k n) m $ do
displayDebugMessage n $ "{ " ++ s ++ "\n"
m `finally` displayDebugMessage n "}\n"