    -- | Measure CPU time for individual phases of the Agda pipeline.

    module Agda.TypeChecking.Monad.Benchmark
      ( module Agda.Benchmarking
      , B.MonadBench
      , B.BenchPhase
      , B.getBenchmark
      , updateBenchmarkingStatus
      , B.billTo, B.billPureTo, B.billToCPS
      , B.reset
      , print
      ) where

    import Prelude hiding (print)

    import Agda.Benchmarking

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Debug

    import qualified Agda.Utils.Benchmark as B

    import Agda.Utils.Monad
    import Agda.Utils.Pretty (prettyShow)

    benchmarkKey :: String
    benchmarkKey :: String
    benchmarkKey = String
    "profile"

    benchmarkLevel :: Int
    benchmarkLevel :: Int
    benchmarkLevel = Int
    7

    benchmarkModulesKey :: String
    benchmarkModulesKey :: String
    benchmarkModulesKey = String
    "profile.modules"

    benchmarkModulesLevel :: Int
    benchmarkModulesLevel :: Int
    benchmarkModulesLevel = Int
    10

    benchmarkDefsKey :: String
    benchmarkDefsKey :: String
    benchmarkDefsKey = String
    "profile.definitions"

    benchmarkDefsLevel :: Int
    benchmarkDefsLevel :: Int
    benchmarkDefsLevel = Int
    10

    -- | When verbosity is set or changes, we need to turn benchmarking on or off.
    updateBenchmarkingStatus :: TCM ()
    -- {-# SPECIALIZE updateBenchmarkingStatus :: TCM () #-}
    -- updateBenchmarkingStatus :: (HasOptions m, MonadBench a m) => m ()
    updateBenchmarkingStatus :: TCM ()
    updateBenchmarkingStatus =
      BenchmarkOn Phase -> TCM ()
    forall (m :: * -> *).
    MonadBench m =>
    BenchmarkOn (BenchPhase m) -> m ()
    B.setBenchmarking (BenchmarkOn Phase -> TCM ())
    -> TCMT IO (BenchmarkOn Phase) -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO (BenchmarkOn Phase)
    forall (tcm :: * -> *). MonadTCM tcm => tcm (BenchmarkOn Phase)
    benchmarking

    -- | Check whether benchmarking is activated.
    {-# SPECIALIZE benchmarking :: TCM (B.BenchmarkOn Phase) #-}
    benchmarking :: MonadTCM tcm => tcm (B.BenchmarkOn Phase)
    benchmarking :: forall (tcm :: * -> *). MonadTCM tcm => tcm (BenchmarkOn Phase)
    benchmarking = TCMT IO (BenchmarkOn Phase) -> tcm (BenchmarkOn Phase)
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO (BenchmarkOn Phase) -> tcm (BenchmarkOn Phase))
    -> TCMT IO (BenchmarkOn Phase) -> tcm (BenchmarkOn Phase)
    forall a b. (a -> b) -> a -> b
    $ do
      -- Ulf, 2016-12-13: Using verbosity levels to control the type of
      -- benchmarking isn't ideal, but let's stick with it for now.
      Bool
    internal <- String -> Int -> TCMT IO Bool
    forall (m :: * -> *). MonadDebug m => String -> Int -> m Bool
    hasVerbosity String
    benchmarkKey Int
    benchmarkLevel
      Bool
    defs     <- String -> Int -> TCMT IO Bool
    forall (m :: * -> *). MonadDebug m => String -> Int -> m Bool
    hasVerbosity String
    benchmarkDefsKey Int
    benchmarkDefsLevel
      Bool
    modules  <- String -> Int -> TCMT IO Bool
    forall (m :: * -> *). MonadDebug m => String -> Int -> m Bool
    hasVerbosity String
    benchmarkModulesKey Int
    benchmarkModulesLevel
      BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase))
    -> BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
    forall a b. (a -> b) -> a -> b
    $ case (Bool
    internal, Bool
    defs, Bool
    modules) of
        (Bool
    True, Bool
    _, Bool
    _) -> (Account Phase -> Bool) -> BenchmarkOn Phase
    forall a. (Account a -> Bool) -> BenchmarkOn a
    B.BenchmarkSome Account Phase -> Bool
    isInternalAccount
        (Bool
    _, Bool
    True, Bool
    _) -> (Account Phase -> Bool) -> BenchmarkOn Phase
    forall a. (Account a -> Bool) -> BenchmarkOn a
    B.BenchmarkSome Account Phase -> Bool
    isDefAccount
        (Bool
    _, Bool
    _, Bool
    True) -> (Account Phase -> Bool) -> BenchmarkOn Phase
    forall a. (Account a -> Bool) -> BenchmarkOn a
    B.BenchmarkSome Account Phase -> Bool
    isModuleAccount
        (Bool, Bool, Bool)
    _            -> BenchmarkOn Phase
    forall a. BenchmarkOn a
    B.BenchmarkOff

    -- | Prints the accumulated benchmark results. Does nothing if
    -- profiling is not activated at level 2.
    print :: MonadTCM tcm => tcm ()
    print :: forall (tcm :: * -> *). MonadTCM tcm => tcm ()
    print = TCM () -> tcm ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> tcm ()) -> TCM () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (Account Phase -> BenchmarkOn Phase -> Bool
    forall a. Account a -> BenchmarkOn a -> Bool
    B.isBenchmarkOn [] (BenchmarkOn Phase -> Bool)
    -> TCMT IO (BenchmarkOn Phase) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (BenchmarkOn Phase)
    forall (tcm :: * -> *). MonadTCM tcm => tcm (BenchmarkOn Phase)
    benchmarking) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      Benchmark Phase
    b <- TCMT IO (Benchmark Phase)
    forall (m :: * -> *). MonadBench m => m (Benchmark (BenchPhase m))
    B.getBenchmark
      -- Andreas, 2017-07-29, issue #2602:
      -- The following line messes up the AgdaInfo buffer,
      -- thus, as Fredrik Forsberg suggest, I restore the original
      -- line for release 2.5.3 until a fix is found.
      -- reportSLn "" 0 $ prettyShow b
      -- Ulf, 2020-03-04: Using benchmarkLevel here means that it only prints if internal benchmarking
      -- is turned on, effectively making module/definition benchmarking impossible (since internal
      -- takes precedence). It needs to be > 1 to avoid triggering #2602 though. Also use
      -- displayDebugMessage instead of reportSLn to avoid requiring -v profile:2 in addition to the
      -- specific profile levels.
      String -> Int -> String -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    displayDebugMessage String
    benchmarkKey Int
    2 (String -> TCM ()) -> String -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Benchmark Phase -> String
    forall a. Pretty a => a -> String
    prettyShow Benchmark Phase
    b

    -- -- | Bill a computation to a specific account.
    -- {-# SPECIALIZE billTo :: Account -> TCM a -> TCM a #-}
    -- billTo :: MonadTCM tcm => Account -> tcm a -> tcm a
    -- billTo account = lift1TCM $ B.billTo account
       -- Andreas, 2015-05-23
       -- FAILS as lift1TCM :: (TCM a -> TCM b) -> tcm a -> tcm b
       -- cannot be implemented lazily in general.
       -- With `lazily` I mean that embedded IO computations in @tcm a@ are
       -- not executed, but passed on to @TCM a -> TCM b@ unevaluated.
       -- If they are treated strictly, then the whole benchmarking is inaccurate
       -- of course, as the computation is done before the clock is started.

    -- -- | Bill a pure computation to a specific account.
    -- {-# SPECIALIZE billPureTo :: Account -> a -> TCM a #-}
    -- billPureTo :: MonadTCM tcm => Account -> a -> tcm a
    -- billPureTo k a = billTo k $ return a