module Agda.Utils.Benchmark where
import Prelude hiding (null)
import qualified Control.Exception as E (evaluate)
import Control.Monad.Reader
import Control.Monad.State
import Data.Functor
import qualified Data.List as List
import qualified Text.PrettyPrint.Boxes as Boxes
import Agda.Utils.Null
import Agda.Utils.Monad hiding (finally)
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Pretty
import Agda.Utils.Time
import Agda.Utils.Trie (Trie)
import qualified Agda.Utils.Trie as Trie
type Account a = [a]
type CurrentAccount a = Strict.Maybe (Account a, CPUTime)
type Timings a = Trie a CPUTime
data Benchmark a = Benchmark
{ benchmarkOn :: !Bool
, currentAccount :: !(CurrentAccount a)
, timings :: !(Timings a)
}
instance Null (Benchmark a) where
empty = Benchmark
{ benchmarkOn = False
, currentAccount = Strict.Nothing
, timings = empty
}
null = null . timings
mapBenchmarkOn :: (Bool -> Bool) -> Benchmark a -> Benchmark a
mapBenchmarkOn f b = b { benchmarkOn = f $ benchmarkOn b }
mapCurrentAccount ::
(CurrentAccount a -> CurrentAccount a) -> Benchmark a -> Benchmark a
mapCurrentAccount f b = b { currentAccount = f (currentAccount b) }
mapTimings :: (Timings a -> Timings a) -> Benchmark a -> Benchmark a
mapTimings f b = b { timings = f (timings b) }
addCPUTime :: Ord a => Account a -> CPUTime -> Benchmark a -> Benchmark a
addCPUTime acc t = mapTimings (Trie.insertWith (+) acc t)
instance (Ord a, Pretty a) => Pretty (Benchmark a) where
pretty b = text $ Boxes.render table
where
(accounts, times) = unzip $ Trie.toList $ timings b
table = Boxes.hsep 1 Boxes.left [col1, col2]
col1 = Boxes.vcat Boxes.left $
map Boxes.text $
"Total" : map showAccount accounts
col2 = Boxes.vcat Boxes.right $
map (Boxes.text . prettyShow) $
sum times : times
showAccount [] = "Miscellaneous"
showAccount ks = List.intercalate "." $ map prettyShow ks
class (Ord a, Functor m, MonadIO m) => MonadBench a m | m -> a where
getBenchmark :: m (Benchmark a)
getsBenchmark :: (Benchmark a -> c) -> m c
getsBenchmark f = f <$> getBenchmark
putBenchmark :: Benchmark a -> m ()
putBenchmark b = modifyBenchmark $ const b
modifyBenchmark :: (Benchmark a -> Benchmark a) -> m ()
modifyBenchmark f = do
b <- getBenchmark
putBenchmark $! f b
finally :: m b -> m c -> m b
instance MonadBench a m => MonadBench a (ReaderT r m) where
getBenchmark = lift $ getBenchmark
putBenchmark = lift . putBenchmark
modifyBenchmark = lift . modifyBenchmark
finally m f = ReaderT $ \ r ->
finally (m `runReaderT` r) (f `runReaderT` r)
instance MonadBench a m => MonadBench a (StateT r m) where
getBenchmark = lift $ getBenchmark
putBenchmark = lift . putBenchmark
modifyBenchmark = lift . modifyBenchmark
finally m f = StateT $ \s ->
finally (m `runStateT` s) (f `runStateT` s)
setBenchmarking :: MonadBench a m => Bool -> m ()
setBenchmarking b = modifyBenchmark $ mapBenchmarkOn $ const b
switchBenchmarking :: MonadBench a m
=> Strict.Maybe (Account a)
-> m (Strict.Maybe (Account a))
switchBenchmarking newAccount = do
now <- liftIO $ getCPUTime
oldAccount <- getsBenchmark currentAccount
Strict.whenJust oldAccount $ \ (acc, start) ->
modifyBenchmark $ addCPUTime acc $ now start
modifyBenchmark $ mapCurrentAccount $ const $ (, now) <$> newAccount
return $ fst <$> oldAccount
reset :: MonadBench a m => m ()
reset = modifyBenchmark $
mapCurrentAccount (const Strict.Nothing) .
mapTimings (const Trie.empty)
billTo :: MonadBench a m => Account a -> m c -> m c
billTo account m = ifNotM (getsBenchmark benchmarkOn) m $ do
old <- switchBenchmarking $ Strict.Just account
(liftIO . E.evaluate =<< m) `finally` switchBenchmarking old
billPureTo :: MonadBench a m => Account a -> c -> m c
billPureTo account = billTo account . return