{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UndecidableInstances #-}
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.Foldable (foldMap)
import Data.Functor
import Data.Function
import qualified Data.List as List
import Data.Monoid
import Data.Maybe
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 BenchmarkOn a = BenchmarkOff | BenchmarkOn | BenchmarkSome (Account a -> Bool)
isBenchmarkOn :: Account a -> BenchmarkOn a -> Bool
isBenchmarkOn _ BenchmarkOff = False
isBenchmarkOn _ BenchmarkOn = True
isBenchmarkOn a (BenchmarkSome p) = p a
data Benchmark a = Benchmark
{ benchmarkOn :: !(BenchmarkOn a)
, currentAccount :: !(CurrentAccount a)
, timings :: !(Timings a)
}
instance Null (Benchmark a) where
empty = Benchmark
{ benchmarkOn = BenchmarkOff
, currentAccount = Strict.Nothing
, timings = empty
}
null = null . timings
mapBenchmarkOn :: (BenchmarkOn a -> BenchmarkOn a) -> 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
trie = timings b
(accounts, times0) = unzip $ Trie.toListOrderedBy (flip compare `on` snd)
$ Trie.filter ((> fromMilliseconds 10) . snd)
$ Trie.mapSubTries (Just . aggr) trie
times = map fst times0
aggr t = (fromMaybe 0 $ Trie.lookup [] t, getSum $ foldMap Sum t)
aggrTimes = do
(a, (t, aggrT)) <- zip accounts times0
return $ if t == aggrT || null a
then Boxes.text ""
else Boxes.text $ "(" ++ prettyShow aggrT ++ ")"
table = Boxes.hsep 1 Boxes.left [col1, col2, col3]
col1 = Boxes.vcat Boxes.left $
map Boxes.text $
"Total" : map showAccount accounts
col2 = Boxes.vcat Boxes.right $
map (Boxes.text . prettyShow) $
sum times : times
col3 = Boxes.vcat Boxes.right $
Boxes.text "" : aggrTimes
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 => BenchmarkOn a -> 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 (isBenchmarkOn account <$> getsBenchmark benchmarkOn) m $ do
old <- switchBenchmarking $ Strict.Just account
(liftIO . E.evaluate =<< m) `finally` switchBenchmarking old
billToCPS :: MonadBench a m => Account a -> ((b -> m c) -> m c) -> (b -> m c) -> m c
billToCPS account f k = ifNotM (isBenchmarkOn account <$> getsBenchmark benchmarkOn) (f k) $ do
old <- switchBenchmarking $ Strict.Just account
f $ \ x -> x `seq` do
_ <- switchBenchmarking old
k x
billPureTo :: MonadBench a m => Account a -> c -> m c
billPureTo account = billTo account . return