    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | 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.Syntax.Common.Pretty (prettyShow)
    import qualified Agda.Utils.ProfileOptions as Profile

    -- | When profile options are set or changed, we need to turn benchmarking on or off.
    updateBenchmarkingStatus :: TCM ()
    -- {-# SPECIALIZE updateBenchmarkingStatus :: TCM () #-}
    -- updateBenchmarkingStatus :: (HasOptions m, MonadBench a m) => m ()
    updateBenchmarkingStatus :: TCM ()
    updateBenchmarkingStatus =
      BenchmarkOn (BenchPhase (TCMT IO)) -> TCM ()
    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 a. TCM a -> tcm a
    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
    $
      TCMT IO Bool
    -> TCMT IO (BenchmarkOn Phase)
    -> TCMT IO (BenchmarkOn Phase)
    -> TCMT IO (BenchmarkOn Phase)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (ProfileOption -> TCMT IO Bool
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
    hasProfileOption ProfileOption
    Profile.Internal)    (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase))
    -> BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
    forall a b. (a -> b) -> a -> b
    $ (Account Phase -> Bool) -> BenchmarkOn Phase
    forall a. (Account a -> Bool) -> BenchmarkOn a
    B.BenchmarkSome Account Phase -> Bool
    isInternalAccount) (TCMT IO (BenchmarkOn Phase) -> TCMT IO (BenchmarkOn Phase))
    -> TCMT IO (BenchmarkOn Phase) -> TCMT IO (BenchmarkOn Phase)
    forall a b. (a -> b) -> a -> b
    $
      TCMT IO Bool
    -> TCMT IO (BenchmarkOn Phase)
    -> TCMT IO (BenchmarkOn Phase)
    -> TCMT IO (BenchmarkOn Phase)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (ProfileOption -> TCMT IO Bool
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
    hasProfileOption ProfileOption
    Profile.Definitions) (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase))
    -> BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
    forall a b. (a -> b) -> a -> b
    $ (Account Phase -> Bool) -> BenchmarkOn Phase
    forall a. (Account a -> Bool) -> BenchmarkOn a
    B.BenchmarkSome Account Phase -> Bool
    isDefAccount) (TCMT IO (BenchmarkOn Phase) -> TCMT IO (BenchmarkOn Phase))
    -> TCMT IO (BenchmarkOn Phase) -> TCMT IO (BenchmarkOn Phase)
    forall a b. (a -> b) -> a -> b
    $
      TCMT IO Bool
    -> TCMT IO (BenchmarkOn Phase)
    -> TCMT IO (BenchmarkOn Phase)
    -> TCMT IO (BenchmarkOn Phase)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (ProfileOption -> TCMT IO Bool
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
    hasProfileOption ProfileOption
    Profile.Modules)     (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase))
    -> BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
    forall a b. (a -> b) -> a -> b
    $ (Account Phase -> Bool) -> BenchmarkOn Phase
    forall a. (Account a -> Bool) -> BenchmarkOn a
    B.BenchmarkSome Account Phase -> Bool
    isModuleAccount) (TCMT IO (BenchmarkOn Phase) -> TCMT IO (BenchmarkOn Phase))
    -> TCMT IO (BenchmarkOn Phase) -> TCMT IO (BenchmarkOn Phase)
    forall a b. (a -> b) -> a -> b
    $
      BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure BenchmarkOn Phase
    forall a. BenchmarkOn a
    B.BenchmarkOff

    -- | Prints the accumulated benchmark results. Does nothing if
    --   no benchmark profiling is enabled.
    print :: MonadTCM tcm => tcm ()
    print :: forall (tcm :: * -> *). MonadTCM tcm => tcm ()
    print = TCM () -> tcm ()
    forall a. TCM a -> tcm a
    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
      b <- TCMT IO (Benchmark (BenchPhase (TCMT IO)))
    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.
      displayDebugMessage "profile" 2 $ prettyShow 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