{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Agda.TypeChecking.Monad.Statistics
( MonadStatistics(..), tick, tickN, tickMax, getStatistics, modifyStatistics, printStatistics
) where
import Control.DeepSeq
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer
import Control.Monad.Trans
import Control.Monad.Trans.Maybe
import qualified Data.Map as Map
import qualified Text.PrettyPrint.Boxes as Boxes
import Agda.Syntax.Concrete.Name as C
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.String
class ReadTCState m => MonadStatistics m where
modifyCounter :: String -> (Integer -> Integer) -> m ()
default modifyCounter
:: (MonadStatistics n, MonadTrans t, t n ~ m)
=> String -> (Integer -> Integer) -> m ()
modifyCounter x = lift . modifyCounter x
instance MonadStatistics m => MonadStatistics (ExceptT e m)
instance MonadStatistics m => MonadStatistics (MaybeT m)
instance MonadStatistics m => MonadStatistics (ReaderT r m)
instance MonadStatistics m => MonadStatistics (StateT s m)
instance (MonadStatistics m, Monoid w) => MonadStatistics (WriterT w m)
instance MonadStatistics TCM where
modifyCounter x f = modifyStatistics $ force . update
where
force m = rnf m `seq` m
update = Map.insertWith (\ new old -> f old) x dummy
dummy = f 0
getStatistics :: ReadTCState m => m Statistics
getStatistics = useR stStatistics
modifyStatistics :: (Statistics -> Statistics) -> TCM ()
modifyStatistics f = stStatistics `modifyTCLens` f
tick :: MonadStatistics m => String -> m ()
tick x = tickN x 1
tickN :: MonadStatistics m => String -> Integer -> m ()
tickN s n = modifyCounter s (n +)
tickMax :: MonadStatistics m => String -> Integer -> m ()
tickMax s n = modifyCounter s (max n)
printStatistics
:: (MonadDebug m, MonadTCEnv m, HasOptions m)
=> Int -> Maybe C.TopLevelModuleName -> Statistics -> m ()
printStatistics vl mmname stats = verboseS "profile.ticks" vl $ do
unlessNull (Map.toList stats) $ \ stats -> do
let
col1 = Boxes.vcat Boxes.left $ map (Boxes.text . fst) stats
col2 = Boxes.vcat Boxes.right $ map (Boxes.text . showThousandSep . snd) stats
table = Boxes.hsep 1 Boxes.left [col1, col2]
reportSLn "profile" 1 $ caseMaybe mmname "Accumulated statistics" $ \ mname ->
"Statistics for " ++ prettyShow mname
reportSLn "profile" 1 $ Boxes.render table