module Agda.TypeChecking.Monad.Statistics
( tick, tickN, tickMax, getStatistics, modifyStatistics, printStatistics
) where
import qualified Data.Map as Map
import Control.DeepSeq
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.TypeChecking.Monad.Options
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.String
getStatistics :: TCM Statistics
getStatistics = use stStatistics
modifyStatistics :: (Statistics -> Statistics) -> TCM ()
modifyStatistics f = stStatistics %= f
tick :: String -> TCM ()
tick x = tickN x 1
tickN :: String -> Integer -> TCM ()
tickN s n = modifyCounter s (n +)
tickMax :: String -> Integer -> TCM ()
tickMax s n = modifyCounter s (max n)
modifyCounter :: String -> (Integer -> Integer) -> TCM ()
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
printStatistics :: Int -> Maybe C.TopLevelModuleName -> Statistics -> TCM ()
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