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

import GHC.Stack (HasCallStack, freezeCallStack, callStack)

import qualified Control.Exception as E
import qualified Control.DeepSeq as DeepSeq (force)
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Maybe
import Control.Monad.Trans.Identity
import Control.Monad.Writer

import Data.Maybe
import Data.Monoid ( Monoid)

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

import Agda.Interaction.Options
import {-# SOURCE #-} Agda.Interaction.Response (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
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
  displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> 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 ()

  traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> m a -> m a
  traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s m a
cont = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s m () -> m a -> m a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m a
cont

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

  getVerbosity :: m Verbosity

  default getVerbosity :: HasOptions m => m Verbosity
  getVerbosity = 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

  isDebugPrinting :: m Bool

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

  nowDebugPrinting :: m a -> m a

  default nowDebugPrinting :: MonadTCEnv m => m a -> m a
  nowDebugPrinting = 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 brackets around debug messages issued by a computation.
  verboseBracket :: VerboseKey -> VerboseLevel -> String -> m a -> m a

-- | During printing, catch internal errors of kind 'Impossible' and print them.
catchAndPrintImpossible
  :: (CatchImpossible m, Monad m)
  => VerboseKey -> VerboseLevel -> m String -> m String
catchAndPrintImpossible :: 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
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
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

  displayDebugMessage :: VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = 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)

  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
vcat
        [ [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 :: VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = VerboseKey -> VerboseLevel -> (TCM a -> TCM a) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n ((TCM a -> TCM a) -> TCM a -> TCM a)
-> (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ \ TCM a
m -> do
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
openVerboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s
    TCM a
m TCM a -> TCM () -> TCM a
forall e (m :: * -> *) a. MonadError e m => m a -> m () -> m a
`finally` VerboseKey -> VerboseLevel -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracket VerboseKey
k VerboseLevel
n

instance MonadDebug m => MonadDebug (ExceptT e m) where
  displayDebugMessage :: VerboseKey -> VerboseLevel -> VerboseKey -> ExceptT e m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = m () -> ExceptT e m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT e m ()) -> m () -> ExceptT e 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
s
  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ExceptT e m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d = m VerboseKey -> ExceptT e m VerboseKey
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VerboseKey -> ExceptT e m VerboseKey)
-> m VerboseKey -> ExceptT e m VerboseKey
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d
  getVerbosity :: ExceptT e m Verbosity
getVerbosity = m Verbosity -> ExceptT e m Verbosity
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  isDebugPrinting :: ExceptT e m Bool
isDebugPrinting = m Bool -> ExceptT e m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Bool
forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting
  nowDebugPrinting :: ExceptT e m a -> ExceptT e m a
nowDebugPrinting = (m (Either e a) -> m (Either e a))
-> ExceptT e m a -> ExceptT e m a
forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> ExceptT e m a -> ExceptT e' n b
mapExceptT m (Either e a) -> m (Either e a)
forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting
  verboseBracket :: VerboseKey
-> VerboseLevel -> VerboseKey -> ExceptT e m a -> ExceptT e m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = (m (Either e a) -> m (Either e a))
-> ExceptT e m a -> ExceptT e m a
forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> ExceptT e m a -> ExceptT e' n b
mapExceptT (VerboseKey
-> VerboseLevel -> VerboseKey -> m (Either e a) -> m (Either e a)
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s)

instance MonadDebug m => MonadDebug (ListT m) where
  displayDebugMessage :: VerboseKey -> VerboseLevel -> VerboseKey -> ListT m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = m () -> ListT m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ListT m ()) -> m () -> ListT 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
s
  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ListT m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d = m VerboseKey -> ListT m VerboseKey
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VerboseKey -> ListT m VerboseKey)
-> m VerboseKey -> ListT m VerboseKey
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d
  getVerbosity :: ListT m Verbosity
getVerbosity = m Verbosity -> ListT m Verbosity
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  isDebugPrinting :: ListT m Bool
isDebugPrinting = m Bool -> ListT m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Bool
forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting
  nowDebugPrinting :: 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
  verboseBracket :: 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

instance MonadDebug m => MonadDebug (MaybeT m) where
  displayDebugMessage :: VerboseKey -> VerboseLevel -> VerboseKey -> MaybeT m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = m () -> MaybeT m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> MaybeT m ()) -> m () -> MaybeT 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
s
  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> MaybeT m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d = m VerboseKey -> MaybeT m VerboseKey
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VerboseKey -> MaybeT m VerboseKey)
-> m VerboseKey -> MaybeT m VerboseKey
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d
  getVerbosity :: MaybeT m Verbosity
getVerbosity = m Verbosity -> MaybeT m Verbosity
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  isDebugPrinting :: MaybeT m Bool
isDebugPrinting = m Bool -> MaybeT m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Bool
forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting
  nowDebugPrinting :: MaybeT m a -> MaybeT m a
nowDebugPrinting = (m (Maybe a) -> m (Maybe a)) -> MaybeT m a -> MaybeT m a
forall (m :: * -> *) a (n :: * -> *) b.
(m (Maybe a) -> n (Maybe b)) -> MaybeT m a -> MaybeT n b
mapMaybeT m (Maybe a) -> m (Maybe a)
forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting
  verboseBracket :: VerboseKey
-> VerboseLevel -> VerboseKey -> MaybeT m a -> MaybeT m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe a) -> MaybeT m a)
-> (MaybeT m a -> m (Maybe a)) -> MaybeT m a -> MaybeT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey
-> VerboseLevel -> VerboseKey -> m (Maybe a) -> m (Maybe a)
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s (m (Maybe a) -> m (Maybe a))
-> (MaybeT m a -> m (Maybe a)) -> MaybeT m a -> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeT m a -> m (Maybe a)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT

instance MonadDebug m => MonadDebug (ReaderT r m) where
  displayDebugMessage :: VerboseKey -> VerboseLevel -> VerboseKey -> ReaderT r m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = m () -> ReaderT r m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ()) -> m () -> ReaderT r 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
s
  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ReaderT r m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d = m VerboseKey -> ReaderT r m VerboseKey
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VerboseKey -> ReaderT r m VerboseKey)
-> m VerboseKey -> ReaderT r m VerboseKey
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d
  getVerbosity :: ReaderT r m Verbosity
getVerbosity = m Verbosity -> ReaderT r m Verbosity
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  isDebugPrinting :: ReaderT r m Bool
isDebugPrinting = m Bool -> ReaderT r m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Bool
forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting
  nowDebugPrinting :: ReaderT r m a -> ReaderT r m a
nowDebugPrinting = (m a -> m a) -> ReaderT r m a -> ReaderT r m a
forall (m :: * -> *) a (n :: * -> *) b r.
(m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT m a -> m a
forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting
  verboseBracket :: VerboseKey
-> VerboseLevel -> VerboseKey -> ReaderT r m a -> ReaderT r m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = (m a -> m a) -> ReaderT r m a -> ReaderT r m a
forall (m :: * -> *) a (n :: * -> *) b r.
(m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT ((m a -> m a) -> ReaderT r m a -> ReaderT r m a)
-> (m a -> m a) -> ReaderT r m a -> ReaderT r 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
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s

instance MonadDebug m => MonadDebug (StateT s m) where
  displayDebugMessage :: VerboseKey -> VerboseLevel -> VerboseKey -> StateT s m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = m () -> StateT s m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT s m ()) -> m () -> StateT s 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
s
  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> StateT s m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d = m VerboseKey -> StateT s m VerboseKey
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VerboseKey -> StateT s m VerboseKey)
-> m VerboseKey -> StateT s m VerboseKey
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d
  getVerbosity :: StateT s m Verbosity
getVerbosity = m Verbosity -> StateT s m Verbosity
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  isDebugPrinting :: StateT s m Bool
isDebugPrinting = m Bool -> StateT s m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Bool
forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting
  nowDebugPrinting :: StateT s m a -> StateT s m a
nowDebugPrinting = (m (a, s) -> m (a, s)) -> StateT s m a -> StateT s m a
forall (m :: * -> *) a s (n :: * -> *) b.
(m (a, s) -> n (b, s)) -> StateT s m a -> StateT s n b
mapStateT m (a, s) -> m (a, s)
forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting
  verboseBracket :: VerboseKey
-> VerboseLevel -> VerboseKey -> StateT s m a -> StateT s m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = (m (a, s) -> m (a, s)) -> StateT s m a -> StateT s m a
forall (m :: * -> *) a s (n :: * -> *) b.
(m (a, s) -> n (b, s)) -> StateT s m a -> StateT s n b
mapStateT ((m (a, s) -> m (a, s)) -> StateT s m a -> StateT s m a)
-> (m (a, s) -> m (a, s)) -> StateT s m a -> StateT s m a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> m (a, s) -> m (a, s)
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s

instance (MonadDebug m, Monoid w) => MonadDebug (WriterT w m) where
  displayDebugMessage :: VerboseKey -> VerboseLevel -> VerboseKey -> WriterT w m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = m () -> WriterT w m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT w m ()) -> m () -> WriterT w 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
s
  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> WriterT w m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d = m VerboseKey -> WriterT w m VerboseKey
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VerboseKey -> WriterT w m VerboseKey)
-> m VerboseKey -> WriterT w m VerboseKey
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d
  getVerbosity :: WriterT w m Verbosity
getVerbosity = m Verbosity -> WriterT w m Verbosity
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  isDebugPrinting :: WriterT w m Bool
isDebugPrinting = m Bool -> WriterT w m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Bool
forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting
  nowDebugPrinting :: WriterT w m a -> WriterT w m a
nowDebugPrinting = (m (a, w) -> m (a, w)) -> WriterT w m a -> WriterT w m a
forall (m :: * -> *) a w (n :: * -> *) b w'.
(m (a, w) -> n (b, w')) -> WriterT w m a -> WriterT w' n b
mapWriterT m (a, w) -> m (a, w)
forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting
  verboseBracket :: VerboseKey
-> VerboseLevel -> VerboseKey -> WriterT w m a -> WriterT w m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = (m (a, w) -> m (a, w)) -> WriterT w m a -> WriterT w m a
forall (m :: * -> *) a w (n :: * -> *) b w'.
(m (a, w) -> n (b, w')) -> WriterT w m a -> WriterT w' n b
mapWriterT ((m (a, w) -> m (a, w)) -> WriterT w m a -> WriterT w m a)
-> (m (a, w) -> m (a, w)) -> WriterT w m a -> WriterT w m a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> m (a, w) -> m (a, w)
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s

instance MonadDebug m => MonadDebug (ChangeT m) where
  displayDebugMessage :: VerboseKey -> VerboseLevel -> VerboseKey -> ChangeT m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = m () -> ChangeT m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ChangeT m ()) -> m () -> ChangeT 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
s
  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ChangeT m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d  = m VerboseKey -> ChangeT m VerboseKey
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VerboseKey -> ChangeT m VerboseKey)
-> m VerboseKey -> ChangeT m VerboseKey
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d
  getVerbosity :: ChangeT m Verbosity
getVerbosity              = m Verbosity -> ChangeT m Verbosity
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Verbosity -> ChangeT m Verbosity)
-> m Verbosity -> ChangeT m Verbosity
forall a b. (a -> b) -> a -> b
$ m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  isDebugPrinting :: ChangeT m Bool
isDebugPrinting           = m Bool -> ChangeT m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> ChangeT m Bool) -> m Bool -> ChangeT m Bool
forall a b. (a -> b) -> a -> b
$ m Bool
forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting
  nowDebugPrinting :: ChangeT m a -> ChangeT m a
nowDebugPrinting          = (m (a, Any) -> m (a, Any)) -> ChangeT m a -> ChangeT m a
forall (m :: * -> *) a (n :: * -> *) b.
(m (a, Any) -> n (b, Any)) -> ChangeT m a -> ChangeT n b
mapChangeT ((m (a, Any) -> m (a, Any)) -> ChangeT m a -> ChangeT m a)
-> (m (a, Any) -> m (a, Any)) -> ChangeT m a -> ChangeT m a
forall a b. (a -> b) -> a -> b
$ m (a, Any) -> m (a, Any)
forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting
  verboseBracket :: VerboseKey
-> VerboseLevel -> VerboseKey -> ChangeT m a -> ChangeT m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s      = (m (a, Any) -> m (a, Any)) -> ChangeT m a -> ChangeT m a
forall (m :: * -> *) a (n :: * -> *) b.
(m (a, Any) -> n (b, Any)) -> ChangeT m a -> ChangeT n b
mapChangeT ((m (a, Any) -> m (a, Any)) -> ChangeT m a -> ChangeT m a)
-> (m (a, Any) -> m (a, Any)) -> ChangeT m a -> ChangeT m a
forall a b. (a -> b) -> a -> b
$ VerboseKey
-> VerboseLevel -> VerboseKey -> m (a, Any) -> m (a, Any)
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s

instance MonadDebug m => MonadDebug (IdentityT m) where
  displayDebugMessage :: VerboseKey -> VerboseLevel -> VerboseKey -> IdentityT m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = m () -> IdentityT m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> IdentityT m ()) -> m () -> IdentityT 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
s
  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> IdentityT m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d  = m VerboseKey -> IdentityT m VerboseKey
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VerboseKey -> IdentityT m VerboseKey)
-> m VerboseKey -> IdentityT m VerboseKey
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d
  getVerbosity :: IdentityT m Verbosity
getVerbosity              = m Verbosity -> IdentityT m Verbosity
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Verbosity -> IdentityT m Verbosity)
-> m Verbosity -> IdentityT m Verbosity
forall a b. (a -> b) -> a -> b
$ m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  isDebugPrinting :: IdentityT m Bool
isDebugPrinting           = m Bool -> IdentityT m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> IdentityT m Bool) -> m Bool -> IdentityT m Bool
forall a b. (a -> b) -> a -> b
$ m Bool
forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting
  nowDebugPrinting :: IdentityT m a -> IdentityT m a
nowDebugPrinting          = (m a -> m a) -> IdentityT m a -> IdentityT m a
forall k1 k2 (m :: k1 -> *) (a :: k1) (n :: k2 -> *) (b :: k2).
(m a -> n b) -> IdentityT m a -> IdentityT n b
mapIdentityT ((m a -> m a) -> IdentityT m a -> IdentityT m a)
-> (m a -> m a) -> IdentityT m a -> IdentityT m a
forall a b. (a -> b) -> a -> b
$ m a -> m a
forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting
  verboseBracket :: VerboseKey
-> VerboseLevel -> VerboseKey -> IdentityT m a -> IdentityT m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s      = (m a -> m a) -> IdentityT m a -> IdentityT m a
forall k1 k2 (m :: k1 -> *) (a :: k1) (n :: k2 -> *) (b :: k2).
(m a -> n b) -> IdentityT m a -> IdentityT n b
mapIdentityT ((m a -> m a) -> IdentityT m a -> IdentityT m a)
-> (m a -> m a) -> IdentityT m a -> IdentityT 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
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s

-- | 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 :: 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 :: VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportS = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn

instance ReportS [TCM Doc] where reportS :: 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
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 :: 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 :: 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
vcat
instance ReportS Doc       where reportS :: 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 :: 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__ :: 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 -> (VerboseKey -> Integer -> Impossible) -> Impossible
forall a b. Integral a => CallStack -> (VerboseKey -> a -> b) -> b
withFileAndLine' (CallStack -> CallStack
freezeCallStack CallStack
HasCallStack => CallStack
callStack) VerboseKey -> Integer -> 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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
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 :: 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 :: 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
vcat
instance TraceS Doc       where traceS :: 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 :: VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
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 :: VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
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 :: 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 :: 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"


------------------------------------------------------------------------
-- 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 :: 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
forall a. [a] -> a
last ([VerboseLevel] -> VerboseLevel) -> [VerboseLevel] -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ VerboseLevel
0 VerboseLevel -> [VerboseLevel] -> [VerboseLevel]
forall a. a -> [a] -> [a]
: [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 :: 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 :: 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__ :: 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 -> (VerboseKey -> Integer -> Impossible) -> Impossible
forall a b. Integral a => CallStack -> (VerboseKey -> a -> b) -> b
withFileAndLine' (CallStack -> CallStack
freezeCallStack CallStack
HasCallStack => CallStack
callStack) VerboseKey -> Integer -> 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 :: 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 :: 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 :: (Verbosity -> f Verbosity) -> PragmaOptions -> f 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 :: 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)