{-# OPTIONS_GHC -Wunused-imports #-}
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
updateBenchmarkingStatus :: TCM ()
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
{-# 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
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
displayDebugMessage "profile" 2 $ prettyShow b