module Agda.TypeChecking.Monad.Debug
  ( module Agda.TypeChecking.Monad.Debug
  , Verbosity, VerboseKey, VerboseLevel
  ) where

import qualified Control.Exception as E
import qualified Control.DeepSeq as DeepSeq (force)

import Control.Monad.IO.Class       ( MonadIO(..) )
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Control  ( MonadTransControl(..), liftThrough )
import Control.Monad.Trans.Maybe
import Control.Monad.Trans.Identity
import Control.Monad.Writer

import Data.Maybe

import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.Base

import Agda.Interaction.Options
import {-# SOURCE #-} Agda.Interaction.Response (Response(..))

import Agda.Utils.CallStack ( HasCallStack, withCallerCallStack )
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty
import Agda.Utils.Update
import qualified Agda.Utils.Trie as Trie

import Agda.Utils.Impossible

class (Functor m, Applicative m, Monad m) => MonadDebug m where

  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> m String
  traceDebugMessage  :: VerboseKey -> VerboseLevel -> String -> m a -> m a

  -- | Print brackets around debug messages issued by a computation.
  verboseBracket     :: VerboseKey -> VerboseLevel -> String -> m a -> m a

  getVerbosity       :: m Verbosity

  -- | Check whether we are currently debug printing.
  isDebugPrinting    :: m Bool

  -- | Flag in a computation that we are currently debug printing.
  nowDebugPrinting   :: m a -> m a

  -- default implementation of transformed debug monad

  default formatDebugMessage
    :: (MonadTrans t, MonadDebug n, m ~ t n)
    => VerboseKey -> VerboseLevel -> TCM Doc -> m String
  formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d

  default traceDebugMessage
    :: (MonadTransControl t, MonadDebug n, m ~ t n)
    => VerboseKey -> VerboseLevel -> String -> m a -> m a
  traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTransControl t, Monad (t m), Monad m) =>
(m (StT t a) -> m (StT t b)) -> t m a -> t m b
liftThrough forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s

  default verboseBracket
    :: (MonadTransControl t, MonadDebug n, m ~ t n)
    => VerboseKey -> VerboseLevel -> String -> m a -> m a
  verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTransControl t, Monad (t m), Monad m) =>
(m (StT t a) -> m (StT t b)) -> t m a -> t m b
liftThrough forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s

  default getVerbosity
    :: (MonadTrans t, MonadDebug n, m ~ t n)
    => m Verbosity
  getVerbosity = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity

  default isDebugPrinting
    :: (MonadTrans t, MonadDebug n, m ~ t n)
    => m Bool
  isDebugPrinting = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting

  default nowDebugPrinting
    :: (MonadTransControl t, MonadDebug n, m ~ t n)
    => m a -> m a
  nowDebugPrinting = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTransControl t, Monad (t m), Monad m) =>
(m (StT t a) -> m (StT t b)) -> t m a -> t m b
liftThrough forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting

-- Default implementations (working around the restriction to only
-- have one default signature).

defaultGetVerbosity :: HasOptions m => m Verbosity
defaultGetVerbosity :: forall (m :: * -> *). HasOptions m => m Verbosity
defaultGetVerbosity = PragmaOptions -> Verbosity
optVerbose forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

defaultIsDebugPrinting :: MonadTCEnv m => m Bool
defaultIsDebugPrinting :: forall (m :: * -> *). MonadTCEnv m => m Bool
defaultIsDebugPrinting = forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envIsDebugPrinting

defaultNowDebugPrinting :: MonadTCEnv m => m a -> m a
defaultNowDebugPrinting :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
defaultNowDebugPrinting = forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eIsDebugPrinting forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Bool
True

-- | Print a debug message if switched on.
displayDebugMessage :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
displayDebugMessage :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | During printing, catch internal errors of kind 'Impossible' and print them.
catchAndPrintImpossible
  :: (CatchImpossible m, Monad m)
  => VerboseKey -> VerboseLevel -> m String -> m String
catchAndPrintImpossible :: forall (m :: * -> *).
(CatchImpossible m, Monad m) =>
VerboseKey -> VerboseLevel -> m VerboseKey -> m VerboseKey
catchAndPrintImpossible VerboseKey
k VerboseLevel
n m VerboseKey
m = forall (m :: * -> *) b a.
CatchImpossible m =>
(Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
catchImpossibleJust Impossible -> Maybe Impossible
catchMe m VerboseKey
m forall a b. (a -> b) -> a -> b
$ \ Impossible
imposs -> do
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Doc -> VerboseKey
render forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
    [ VerboseKey -> Doc
text forall a b. (a -> b) -> a -> b
$ VerboseKey
"Debug printing " forall a. [a] -> [a] -> [a]
++ VerboseKey
k forall a. [a] -> [a] -> [a]
++ VerboseKey
":" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> VerboseKey
show VerboseLevel
n forall a. [a] -> [a] -> [a]
++ VerboseKey
" failed due to exception:"
    , forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> Doc
text) forall a b. (a -> b) -> a -> b
$ VerboseKey -> [VerboseKey]
lines forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> VerboseKey
show Impossible
imposs
    ]
  where
  -- Exception filter: Catch only the 'Impossible' exception during debug printing.
  catchMe :: Impossible -> Maybe Impossible
  catchMe :: Impossible -> Maybe Impossible
catchMe = forall a. (a -> Bool) -> a -> Maybe a
filterMaybe forall a b. (a -> b) -> a -> b
$ \case
    Impossible{}            -> Bool
True
    Unreachable{}           -> Bool
False
    ImpMissingDefinitions{} -> Bool
False

instance MonadDebug TCM where

  traceDebugMessage :: forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s TCM a
cont = do
    -- Andreas, 2019-08-20, issue #4016:
    -- Force any lazy 'Impossible' exceptions to the surface and handle them.
    VerboseKey
s  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
(CatchImpossible m, Monad m) =>
VerboseKey -> VerboseLevel -> m VerboseKey -> m VerboseKey
catchAndPrintImpossible VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> IO a
E.evaluate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NFData a => a -> a
DeepSeq.force forall a b. (a -> b) -> a -> b
$ VerboseKey
s
    InteractionOutputCallback
cb <- forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC forall a b. (a -> b) -> a -> b
$ PersistentTCState -> InteractionOutputCallback
stInteractionOutputCallback forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState
    InteractionOutputCallback
cb (VerboseLevel -> VerboseKey -> Response
Resp_RunningInfo VerboseLevel
n VerboseKey
s)
    TCM a
cont

  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d = forall (m :: * -> *).
(CatchImpossible m, Monad m) =>
VerboseKey -> VerboseLevel -> m VerboseKey -> m VerboseKey
catchAndPrintImpossible VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ do
    Doc -> VerboseKey
render forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Doc
d forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err -> do
      forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm VerboseKey
prettyError TCErr
err forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ VerboseKey
s -> forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
        [ forall (t :: * -> *). Foldable t => t Doc -> Doc
sep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map VerboseKey -> Doc
text
          [ VerboseKey
"Printing debug message"
          , VerboseKey
k  forall a. [a] -> [a] -> [a]
++ VerboseKey
":" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> VerboseKey
show VerboseLevel
n
          , VerboseKey
"failed due to error:"
          ]
        , VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ VerboseKey -> Doc
text VerboseKey
s
        ]

  verboseBracket :: forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ \ TCMT IO a
m -> do
    forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
openVerboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s
    (TCMT IO a
m forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracket VerboseKey
k VerboseLevel
n) forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
e -> do
      forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracketException VerboseKey
k VerboseLevel
n
      forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
e

  getVerbosity :: TCM Verbosity
getVerbosity     = forall (m :: * -> *). HasOptions m => m Verbosity
defaultGetVerbosity
  isDebugPrinting :: TCM Bool
isDebugPrinting  = forall (m :: * -> *). MonadTCEnv m => m Bool
defaultIsDebugPrinting
  nowDebugPrinting :: forall a. TCM a -> TCM a
nowDebugPrinting = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
defaultNowDebugPrinting

-- MonadTrans default instances

deriving instance MonadDebug m => MonadDebug (BlockT m)  -- ghc <= 8.0, GeneralizedNewtypeDeriving
instance MonadDebug m => MonadDebug (ChangeT m)
instance MonadDebug m => MonadDebug (ExceptT e m)
instance MonadDebug m => MonadDebug (MaybeT m)
instance MonadDebug m => MonadDebug (ReaderT r m)
instance MonadDebug m => MonadDebug (StateT s m)
instance (MonadDebug m, Monoid w) => MonadDebug (WriterT w m)
instance MonadDebug m => MonadDebug (IdentityT m)

-- We are lacking MonadTransControl ListT

instance MonadDebug m => MonadDebug (ListT m) where
  traceDebugMessage :: forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> ListT m a -> ListT m a
traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s
  verboseBracket :: forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> ListT m a -> ListT m a
verboseBracket    VerboseKey
k VerboseLevel
n VerboseKey
s = forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s
  nowDebugPrinting :: forall a. ListT m a -> ListT m a
nowDebugPrinting        = forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting

-- | Debug print some lines if the verbosity level for the given
--   'VerboseKey' is at least 'VerboseLevel'.
--
-- Note: In the presence of @OverloadedStrings@, just
-- @@
--   reportS key level "Literate string"
-- @@
-- gives an @Ambiguous type variable@ error in @GHC@.
-- Use the legacy functions 'reportSLn' and 'reportSDoc' instead then.
--
class ReportS a where
  reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m ()

instance ReportS (TCM Doc) where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportS = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc
instance ReportS String    where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportS = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn

instance ReportS [TCM Doc] where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> [TCM Doc] -> m ()
reportS VerboseKey
k VerboseLevel
n = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
instance ReportS [String]  where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> [VerboseKey] -> m ()
reportS VerboseKey
k VerboseLevel
n = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VerboseKey] -> VerboseKey
unlines
instance ReportS [Doc]     where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> [Doc] -> m ()
reportS VerboseKey
k VerboseLevel
n = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> VerboseKey
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
instance ReportS Doc       where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> m ()
reportS VerboseKey
k VerboseLevel
n = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> VerboseKey
render

-- | Conditionally println debug string.
{-# SPECIALIZE reportSLn :: VerboseKey -> VerboseLevel -> String -> TCM () #-}
reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
reportSLn :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
k VerboseLevel
n VerboseKey
s = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ VerboseKey
s forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n"

__IMPOSSIBLE_VERBOSE__ :: (HasCallStack, MonadDebug m) => String -> m a
__IMPOSSIBLE_VERBOSE__ :: forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ VerboseKey
s = do { forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"impossible" VerboseLevel
10 VerboseKey
s ; forall a. Impossible -> a
throwImpossible Impossible
err }
  where
    -- Create the "Impossible" error using *our* caller as the call site.
    err :: Impossible
err = forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Impossible
Impossible

-- | Conditionally render debug 'Doc' and print it.
{-# SPECIALIZE reportSDoc :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM () #-}
reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
k VerboseLevel
n TCM Doc
d = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n") forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n (forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eIsDebugPrinting (forall a b. a -> b -> a
const Bool
True) TCM Doc
d)

-- | Debug print the result of a computation.
reportResult :: MonadDebug m => VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
reportResult :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
reportResult VerboseKey
k VerboseLevel
n a -> TCM Doc
debug m a
action = do
  a
x <- m a
action
  a
x forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
k VerboseLevel
n (a -> TCM Doc
debug a
x)

unlessDebugPrinting :: MonadDebug m => m () -> m ()
unlessDebugPrinting :: forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting

-- | Debug print some lines if the verbosity level for the given
--   'VerboseKey' is at least 'VerboseLevel'.
--
-- Note: In the presence of @OverloadedStrings@, just
-- @@
--   traceS key level "Literate string"
-- @@
-- gives an @Ambiguous type variable@ error in @GHC@.
-- Use the legacy functions 'traceSLn' and 'traceSDoc' instead then.
--
class TraceS a where
  traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m c -> m c

instance TraceS (TCM Doc) where traceS :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
traceS = forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
traceSDoc
instance TraceS String    where traceS :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceS = forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn

instance TraceS [TCM Doc] where traceS :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c
traceS VerboseKey
k VerboseLevel
n = forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
traceSDoc VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
instance TraceS [String]  where traceS :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> [VerboseKey] -> m c -> m c
traceS VerboseKey
k VerboseLevel
n = forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn  VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VerboseKey] -> VerboseKey
unlines
instance TraceS [Doc]     where traceS :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c
traceS VerboseKey
k VerboseLevel
n = forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn  VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> VerboseKey
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
instance TraceS Doc       where traceS :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> m c -> m c
traceS VerboseKey
k VerboseLevel
n = forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn  VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> VerboseKey
render

traceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a
traceSLn :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn VerboseKey
k VerboseLevel
n VerboseKey
s = forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ VerboseKey
s forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n"

-- | Conditionally render debug 'Doc', print it, and then continue.
traceSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
traceSDoc VerboseKey
k VerboseLevel
n TCM Doc
d = forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ \m a
cont -> do
  VerboseKey
s <- forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eIsDebugPrinting (forall a b. a -> b -> a
const Bool
True) TCM Doc
d
  forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey
s forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n") m a
cont

openVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
openVerboseBracket :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
openVerboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ VerboseKey
"{ " forall a. [a] -> [a] -> [a]
++ VerboseKey
s forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n"

closeVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> m ()
closeVerboseBracket :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracket VerboseKey
k VerboseLevel
n = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
"}\n"

closeVerboseBracketException :: MonadDebug m => VerboseKey -> VerboseLevel -> m ()
closeVerboseBracketException :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracketException VerboseKey
k VerboseLevel
n = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
"} (exception)\n"


------------------------------------------------------------------------
-- Verbosity

-- Invariant (which we may or may not currently break): Debug
-- printouts use one of the following functions:
--
--   reportS
--   reportSLn
--   reportSDoc

parseVerboseKey :: VerboseKey -> [String]
parseVerboseKey :: VerboseKey -> [VerboseKey]
parseVerboseKey = forall a. (a -> Bool) -> [a] -> [[a]]
wordsBy (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (VerboseKey
".:" :: String))

-- | Check whether a certain verbosity level is activated.
--
--   Precondition: The level must be non-negative.
{-# SPECIALIZE hasVerbosity :: VerboseKey -> VerboseLevel -> TCM Bool #-}
hasVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
hasVerbosity :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
k VerboseLevel
n | VerboseLevel
n forall a. Ord a => a -> a -> Bool
< VerboseLevel
0     = forall a. HasCallStack => a
__IMPOSSIBLE__
                 | Bool
otherwise = do
    Verbosity
t <- forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
    let ks :: [VerboseKey]
ks = VerboseKey -> [VerboseKey]
parseVerboseKey VerboseKey
k
        m :: VerboseLevel
m  = forall a. a -> [a] -> a
lastWithDefault VerboseLevel
0 forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => [k] -> Trie k v -> [v]
Trie.lookupPath [VerboseKey]
ks Verbosity
t
    forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseLevel
n forall a. Ord a => a -> a -> Bool
<= VerboseLevel
m)

-- | Check whether a certain verbosity level is activated (exact match).

{-# SPECIALIZE hasExactVerbosity :: VerboseKey -> VerboseLevel -> TCM Bool #-}
hasExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
hasExactVerbosity :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasExactVerbosity VerboseKey
k VerboseLevel
n =
  (forall a. a -> Maybe a
Just VerboseLevel
n forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => [k] -> Trie k v -> Maybe v
Trie.lookup (VerboseKey -> [VerboseKey]
parseVerboseKey VerboseKey
k) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity

-- | Run a computation if a certain verbosity level is activated (exact match).

{-# SPECIALIZE whenExactVerbosity :: VerboseKey -> VerboseLevel -> TCM () -> TCM () #-}
whenExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
whenExactVerbosity :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
whenExactVerbosity VerboseKey
k VerboseLevel
n = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasExactVerbosity VerboseKey
k VerboseLevel
n

__CRASH_WHEN__ :: (HasCallStack, MonadTCM m, MonadDebug m) => VerboseKey -> VerboseLevel -> m ()
__CRASH_WHEN__ :: forall (m :: * -> *).
(HasCallStack, MonadTCM m, MonadDebug m) =>
VerboseKey -> VerboseLevel -> m ()
__CRASH_WHEN__ VerboseKey
k VerboseLevel
n = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
whenExactVerbosity VerboseKey
k VerboseLevel
n (forall a. Impossible -> a
throwImpossible Impossible
err)
  where
    -- Create the "Unreachable" error using *our* caller as the call site.
    err :: Impossible
err = forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Impossible
Unreachable

-- | Run a computation if a certain verbosity level is activated.
--
--   Precondition: The level must be non-negative.
{-# SPECIALIZE verboseS :: VerboseKey -> VerboseLevel -> TCM () -> TCM () #-}
-- {-# SPECIALIZE verboseS :: MonadIO m => VerboseKey -> VerboseLevel -> TCMT m () -> TCMT m () #-} -- RULE left-hand side too complicated to desugar
-- {-# SPECIALIZE verboseS :: MonadTCM tcm => VerboseKey -> VerboseLevel -> tcm () -> tcm () #-}
verboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
verboseS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
k VerboseLevel
n m ()
action = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
k VerboseLevel
n) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting m ()
action

-- | Apply a function if a certain verbosity level is activated.
--
--   Precondition: The level must be non-negative.
applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n m a -> m a
f m a
a = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
k VerboseLevel
n) (m a -> m a
f m a
a) m a
a

-- | Verbosity lens.
verbosity :: VerboseKey -> Lens' VerboseLevel TCState
verbosity :: VerboseKey -> Lens' VerboseLevel TCState
verbosity VerboseKey
k = Lens' PragmaOptions TCState
stPragmaOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Verbosity PragmaOptions
verbOpt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => [k] -> Lens' (Maybe v) (Trie k v)
Trie.valueAt (VerboseKey -> [VerboseKey]
parseVerboseKey VerboseKey
k) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => a -> Lens' a (Maybe a)
defaultTo VerboseLevel
0
  where
    verbOpt :: Lens' Verbosity PragmaOptions
    verbOpt :: Lens' Verbosity PragmaOptions
verbOpt Verbosity -> f Verbosity
f PragmaOptions
opts = Verbosity -> f Verbosity
f (PragmaOptions -> Verbosity
optVerbose PragmaOptions
opts) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Verbosity
v -> PragmaOptions
opts { optVerbose :: Verbosity
optVerbose = Verbosity
v }
    -- Andreas, 2019-08-20: this lens should go into Interaction.Option.Lenses!

    defaultTo :: Eq a => a -> Lens' a (Maybe a)
    defaultTo :: forall a. Eq a => a -> Lens' a (Maybe a)
defaultTo a
x a -> f a
f Maybe a
m = forall a. (a -> Bool) -> a -> Maybe a
filterMaybe (forall a. Eq a => a -> a -> Bool
== a
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f (forall a. a -> Maybe a -> a
fromMaybe a
x Maybe a
m)