module Agda.TypeChecking.Monad.Statistics
( tick, tickN, tickMax, getStatistics
) where
import Control.Monad.State
import Data.Map as Map
import Agda.TypeChecking.Monad.Base
getStatistics :: TCM Statistics
getStatistics = gets stStatistics
modifyStatistics :: (Statistics -> Statistics) -> TCM ()
modifyStatistics f = modify $ \ s -> s { stStatistics = f (stStatistics s) }
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 = sum (Map.elems m) `seq` m
update = Map.insertWith (\ new old -> f old) x dummy
dummy = f 0