-- | 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