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 = n VerboseKey -> t n VerboseKey
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n VerboseKey -> t n VerboseKey) -> n VerboseKey -> t n VerboseKey
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> n VerboseKey
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 = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
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 ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
-> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall a b. (a -> b) -> a -> b
$ VerboseKey
-> VerboseLevel -> VerboseKey -> n (StT t a) -> n (StT t a)
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 = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
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 ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
-> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall a b. (a -> b) -> a -> b
$ VerboseKey
-> VerboseLevel -> VerboseKey -> n (StT t a) -> n (StT t a)
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 = n Verbosity -> t n Verbosity
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift n Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity

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

  default nowDebugPrinting
    :: (MonadTransControl t, MonadDebug n, m ~ t n)
    => m a -> m a
  nowDebugPrinting = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
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 n (StT t a) -> n (StT t a)
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 (PragmaOptions -> Verbosity) -> m PragmaOptions -> m Verbosity
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

defaultIsDebugPrinting :: MonadTCEnv m => m Bool
defaultIsDebugPrinting :: forall (m :: * -> *). MonadTCEnv m => m Bool
defaultIsDebugPrinting = (TCEnv -> Bool) -> m Bool
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 = Lens' Bool TCEnv -> (Bool -> Bool) -> m a -> m a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eIsDebugPrinting ((Bool -> Bool) -> m a -> m a) -> (Bool -> Bool) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
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 = VerboseKey -> VerboseLevel -> VerboseKey -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ () -> m ()
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 = (Impossible -> Maybe Impossible)
-> m VerboseKey -> (Impossible -> m VerboseKey) -> m VerboseKey
forall (m :: * -> *) b a.
CatchImpossible m =>
(Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
catchImpossibleJust Impossible -> Maybe Impossible
catchMe m VerboseKey
m ((Impossible -> m VerboseKey) -> m VerboseKey)
-> (Impossible -> m VerboseKey) -> m VerboseKey
forall a b. (a -> b) -> a -> b
$ \ Impossible
imposs -> do
  VerboseKey -> m VerboseKey
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseKey -> m VerboseKey) -> VerboseKey -> m VerboseKey
forall a b. (a -> b) -> a -> b
$ Doc -> VerboseKey
render (Doc -> VerboseKey) -> Doc -> VerboseKey
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
    [ VerboseKey -> Doc
text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Debug printing " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
k VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
":" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
n VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" failed due to exception:"
    , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (VerboseKey -> Doc) -> [VerboseKey] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 (Doc -> Doc) -> (VerboseKey -> Doc) -> VerboseKey -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> Doc
text) ([VerboseKey] -> [Doc]) -> [VerboseKey] -> [Doc]
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [VerboseKey]
lines (VerboseKey -> [VerboseKey]) -> VerboseKey -> [VerboseKey]
forall a b. (a -> b) -> a -> b
$ Impossible -> VerboseKey
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 = (Impossible -> Bool) -> Impossible -> Maybe Impossible
forall a. (a -> Bool) -> a -> Maybe a
filterMaybe ((Impossible -> Bool) -> Impossible -> Maybe Impossible)
-> (Impossible -> Bool) -> Impossible -> Maybe Impossible
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  <- IO VerboseKey -> TCM VerboseKey
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO VerboseKey -> TCM VerboseKey)
-> (VerboseKey -> IO VerboseKey) -> VerboseKey -> TCM VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> VerboseLevel -> IO VerboseKey -> IO VerboseKey
forall (m :: * -> *).
(CatchImpossible m, Monad m) =>
VerboseKey -> VerboseLevel -> m VerboseKey -> m VerboseKey
catchAndPrintImpossible VerboseKey
k VerboseLevel
n (IO VerboseKey -> IO VerboseKey)
-> (VerboseKey -> IO VerboseKey) -> VerboseKey -> IO VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> IO VerboseKey
forall a. a -> IO a
E.evaluate (VerboseKey -> IO VerboseKey)
-> (VerboseKey -> VerboseKey) -> VerboseKey -> IO VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> VerboseKey
forall a. NFData a => a -> a
DeepSeq.force (VerboseKey -> TCM VerboseKey) -> VerboseKey -> TCM VerboseKey
forall a b. (a -> b) -> a -> b
$ VerboseKey
s
    InteractionOutputCallback
cb <- (TCState -> InteractionOutputCallback)
-> TCMT IO InteractionOutputCallback
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC ((TCState -> InteractionOutputCallback)
 -> TCMT IO InteractionOutputCallback)
-> (TCState -> InteractionOutputCallback)
-> TCMT IO InteractionOutputCallback
forall a b. (a -> b) -> a -> b
$ PersistentTCState -> InteractionOutputCallback
stInteractionOutputCallback (PersistentTCState -> InteractionOutputCallback)
-> (TCState -> PersistentTCState)
-> TCState
-> InteractionOutputCallback
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 = VerboseKey -> VerboseLevel -> TCM VerboseKey -> TCM VerboseKey
forall (m :: * -> *).
(CatchImpossible m, Monad m) =>
VerboseKey -> VerboseLevel -> m VerboseKey -> m VerboseKey
catchAndPrintImpossible VerboseKey
k VerboseLevel
n (TCM VerboseKey -> TCM VerboseKey)
-> TCM VerboseKey -> TCM VerboseKey
forall a b. (a -> b) -> a -> b
$ do
    Doc -> VerboseKey
render (Doc -> VerboseKey) -> TCM Doc -> TCM VerboseKey
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Doc
d TCM Doc -> (TCErr -> TCM Doc) -> TCM Doc
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err -> do
      TCErr -> TCM VerboseKey
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm VerboseKey
prettyError TCErr
err TCM VerboseKey -> (VerboseKey -> Doc) -> TCM Doc
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ VerboseKey
s -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
        [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (VerboseKey -> Doc) -> [VerboseKey] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map VerboseKey -> Doc
text
          [ VerboseKey
"Printing debug message"
          , VerboseKey
k  VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
":" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
n
          , VerboseKey
"failed due to error:"
          ]
        , VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
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 = VerboseKey
-> VerboseLevel
-> (TCMT IO a -> TCMT IO a)
-> TCMT IO a
-> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n ((TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a)
-> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ \ TCMT IO a
m -> do
    VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
openVerboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s
    (TCMT IO a
m TCMT IO a -> TCMT IO () -> TCMT IO a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* VerboseKey -> VerboseLevel -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracket VerboseKey
k VerboseLevel
n) TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
e -> do
      VerboseKey -> VerboseLevel -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracketException VerboseKey
k VerboseLevel
n
      TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
e

  getVerbosity :: TCM Verbosity
getVerbosity     = TCM Verbosity
forall (m :: * -> *). HasOptions m => m Verbosity
defaultGetVerbosity
  isDebugPrinting :: TCM Bool
isDebugPrinting  = TCM Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
defaultIsDebugPrinting
  nowDebugPrinting :: forall a. TCM a -> TCM a
nowDebugPrinting = TCMT IO a -> TCMT IO a
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 a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT ((forall a1. m a1 -> m a1) -> ListT m a -> ListT m a)
-> (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> m a1 -> m a1
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 a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT ((forall a1. m a1 -> m a1) -> ListT m a -> ListT m a)
-> (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> m a1 -> m a1
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 a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT forall a1. m a1 -> m a1
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 = VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc
instance ReportS String    where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportS = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
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 = VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
k VerboseLevel
n (TCM Doc -> m ()) -> ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Doc] -> Doc) -> TCMT IO [Doc] -> TCM Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (TCMT IO [Doc] -> TCM Doc)
-> ([TCM Doc] -> TCMT IO [Doc]) -> [TCM Doc] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCM Doc] -> TCMT IO [Doc]
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 = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
k VerboseLevel
n (VerboseKey -> m ())
-> ([VerboseKey] -> VerboseKey) -> [VerboseKey] -> m ()
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 = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
k VerboseLevel
n (VerboseKey -> m ()) -> ([Doc] -> VerboseKey) -> [Doc] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> VerboseKey
render (Doc -> VerboseKey) -> ([Doc] -> Doc) -> [Doc] -> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
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 = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
k VerboseLevel
n (VerboseKey -> m ()) -> (Doc -> VerboseKey) -> Doc -> m ()
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 = VerboseKey -> VerboseLevel -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
k VerboseLevel
n (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
s VerboseKey -> VerboseKey -> VerboseKey
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 { VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"impossible" VerboseLevel
10 VerboseKey
s ; Impossible -> m a
forall a. Impossible -> a
throwImpossible Impossible
err }
  where
    -- Create the "Impossible" error using *our* caller as the call site.
    err :: Impossible
err = (CallStack -> Impossible) -> Impossible
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 = VerboseKey -> VerboseLevel -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
k VerboseLevel
n (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey -> m ())
-> (VerboseKey -> VerboseKey) -> VerboseKey -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n") (VerboseKey -> m ()) -> m VerboseKey -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n (Lens' Bool TCEnv -> (Bool -> Bool) -> TCM Doc -> TCM Doc
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eIsDebugPrinting (Bool -> Bool -> Bool
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 a -> m () -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ VerboseKey -> VerboseLevel -> TCM Doc -> m ()
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 = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM m Bool
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 = VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
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 = VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
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 = VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
traceSDoc VerboseKey
k VerboseLevel
n (TCM Doc -> m c -> m c)
-> ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> m c -> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Doc] -> Doc) -> TCMT IO [Doc] -> TCM Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (TCMT IO [Doc] -> TCM Doc)
-> ([TCM Doc] -> TCMT IO [Doc]) -> [TCM Doc] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCM Doc] -> TCMT IO [Doc]
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 = VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn  VerboseKey
k VerboseLevel
n (VerboseKey -> m c -> m c)
-> ([VerboseKey] -> VerboseKey) -> [VerboseKey] -> m c -> m c
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 = VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn  VerboseKey
k VerboseLevel
n (VerboseKey -> m c -> m c)
-> ([Doc] -> VerboseKey) -> [Doc] -> m c -> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> VerboseKey
render (Doc -> VerboseKey) -> ([Doc] -> Doc) -> [Doc] -> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
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 = VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn  VerboseKey
k VerboseLevel
n (VerboseKey -> m c -> m c)
-> (Doc -> VerboseKey) -> Doc -> m c -> m c
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 = VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n ((m a -> m a) -> m a -> m a) -> (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey -> m a -> m a) -> VerboseKey -> m a -> m a
forall a b. (a -> b) -> a -> b
$ VerboseKey
s VerboseKey -> VerboseKey -> VerboseKey
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 = VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n ((m a -> m a) -> m a -> m a) -> (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \m a
cont -> do
  VerboseKey
s <- VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n (TCM Doc -> m VerboseKey) -> TCM Doc -> m VerboseKey
forall a b. (a -> b) -> a -> b
$ Lens' Bool TCEnv -> (Bool -> Bool) -> TCM Doc -> TCM Doc
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eIsDebugPrinting (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) TCM Doc
d
  VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey
s VerboseKey -> VerboseKey -> VerboseKey
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 = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"{ " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
s VerboseKey -> VerboseKey -> VerboseKey
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 = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
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 = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
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 = (Char -> Bool) -> VerboseKey -> [VerboseKey]
forall a. (a -> Bool) -> [a] -> [[a]]
wordsBy (Char -> VerboseKey -> Bool
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 VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< VerboseLevel
0     = m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
                 | Bool
otherwise = do
    Verbosity
t <- m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
    let ks :: [VerboseKey]
ks = VerboseKey -> [VerboseKey]
parseVerboseKey VerboseKey
k
        m :: VerboseLevel
m  = VerboseLevel -> [VerboseLevel] -> VerboseLevel
forall a. a -> [a] -> a
lastWithDefault VerboseLevel
0 ([VerboseLevel] -> VerboseLevel) -> [VerboseLevel] -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ [VerboseKey] -> Verbosity -> [VerboseLevel]
forall k v. Ord k => [k] -> Trie k v -> [v]
Trie.lookupPath [VerboseKey]
ks Verbosity
t
    Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
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 =
  (VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
n Maybe VerboseLevel -> Maybe VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe VerboseLevel -> Bool)
-> (Verbosity -> Maybe VerboseLevel) -> Verbosity -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VerboseKey] -> Verbosity -> Maybe VerboseLevel
forall k v. Ord k => [k] -> Trie k v -> Maybe v
Trie.lookup (VerboseKey -> [VerboseKey]
parseVerboseKey VerboseKey
k) (Verbosity -> Bool) -> m Verbosity -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Verbosity
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 = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (m Bool -> m () -> m ()) -> m Bool -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> m Bool
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 = VerboseKey -> VerboseLevel -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
whenExactVerbosity VerboseKey
k VerboseLevel
n (Impossible -> m ()
forall a. Impossible -> a
throwImpossible Impossible
err)
  where
    -- Create the "Unreachable" error using *our* caller as the call site.
    err :: Impossible
err = (CallStack -> Impossible) -> Impossible
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 = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (VerboseKey -> VerboseLevel -> m Bool
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
k VerboseLevel
n) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ m () -> m ()
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 = m Bool -> m a -> m a -> m a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (VerboseKey -> VerboseLevel -> m Bool
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 = (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' PragmaOptions TCState
stPragmaOptions ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState)
-> ((VerboseLevel -> f VerboseLevel)
    -> PragmaOptions -> f PragmaOptions)
-> (VerboseLevel -> f VerboseLevel)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Verbosity -> f Verbosity) -> PragmaOptions -> f PragmaOptions
Lens' Verbosity PragmaOptions
verbOpt ((Verbosity -> f Verbosity) -> PragmaOptions -> f PragmaOptions)
-> ((VerboseLevel -> f VerboseLevel) -> Verbosity -> f Verbosity)
-> (VerboseLevel -> f VerboseLevel)
-> PragmaOptions
-> f PragmaOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VerboseKey] -> Lens' (Maybe VerboseLevel) Verbosity
forall k v. Ord k => [k] -> Lens' (Maybe v) (Trie k v)
Trie.valueAt (VerboseKey -> [VerboseKey]
parseVerboseKey VerboseKey
k) ((Maybe VerboseLevel -> f (Maybe VerboseLevel))
 -> Verbosity -> f Verbosity)
-> ((VerboseLevel -> f VerboseLevel)
    -> Maybe VerboseLevel -> f (Maybe VerboseLevel))
-> (VerboseLevel -> f VerboseLevel)
-> Verbosity
-> f Verbosity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Lens' VerboseLevel (Maybe VerboseLevel)
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) f Verbosity -> (Verbosity -> PragmaOptions) -> f PragmaOptions
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 = (a -> Bool) -> a -> Maybe a
forall a. (a -> Bool) -> a -> Maybe a
filterMaybe (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x) (a -> Maybe a) -> f a -> f (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f (a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
x Maybe a
m)