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

module Agda.TypeChecking.Monad.Benchmark
  ( module Agda.Benchmarking
  , B.MonadBench
  , 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{-# SOURCE #-} Agda.TypeChecking.Monad.Options

import qualified Agda.Utils.Benchmark as B

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

benchmarkKey :: String
benchmarkKey = "profile"

benchmarkLevel :: Int
benchmarkLevel = 7

benchmarkModulesKey :: String
benchmarkModulesKey = "profile.modules"

benchmarkModulesLevel :: Int
benchmarkModulesLevel = 10

benchmarkDefsKey :: String
benchmarkDefsKey = "profile.definitions"

benchmarkDefsLevel :: Int
benchmarkDefsLevel = 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 =
  B.setBenchmarking =<< benchmarking

-- | Check whether benchmarking is activated.
{-# SPECIALIZE benchmarking :: TCM (B.BenchmarkOn Phase) #-}
benchmarking :: MonadTCM tcm => tcm (B.BenchmarkOn Phase)
benchmarking = liftTCM $ 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.
  internal <- hasVerbosity benchmarkKey benchmarkLevel
  defs     <- hasVerbosity benchmarkDefsKey benchmarkDefsLevel
  modules  <- hasVerbosity benchmarkModulesKey benchmarkModulesLevel
  return $ case (internal, defs, modules) of
    (True, _, _) -> B.BenchmarkSome isInternalAccount
    (_, True, _) -> B.BenchmarkSome isDefAccount
    (_, _, True) -> B.BenchmarkSome isModuleAccount
    _            -> B.BenchmarkOff

-- | Prints the accumulated benchmark results. Does nothing if
-- profiling is not activated at level 7.
print :: MonadTCM tcm => tcm ()
print = liftTCM $ whenM (B.isBenchmarkOn [] <$> benchmarking) $ do
  b <- 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
  reportSLn benchmarkKey benchmarkLevel $ 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