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
updateBenchmarkingStatus :: TCM ()
updateBenchmarkingStatus =
B.setBenchmarking =<< benchmarking
{-# SPECIALIZE benchmarking :: TCM (B.BenchmarkOn Phase) #-}
benchmarking :: MonadTCM tcm => tcm (B.BenchmarkOn Phase)
benchmarking = liftTCM $ do
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
print :: MonadTCM tcm => tcm ()
print = liftTCM $ whenM (B.isBenchmarkOn [] <$> benchmarking) $ do
b <- B.getBenchmark
reportSLn benchmarkKey benchmarkLevel $ prettyShow b