module Agda.TypeChecking.Monad.Statistics
( tick, tickN, tickMax, getStatistics
) where
import Control.Monad.State
import Data.Map as Map
import Agda.TypeChecking.Monad.Base
tick :: String -> TCM ()
tick x = tickN x 1
tickN :: String -> Integer -> TCM ()
tickN s n = tick' s (n +)
tick' :: String -> (Integer -> Integer) -> TCM ()
tick' x f = modify $ \s ->
let st' = upd $ stStatistics s in
force st' `seq` s { stStatistics = st' }
where
force m = sum (Map.elems m)
upd = Map.insertWith (\_ m -> f m) x (f 0)
tickMax :: String -> Integer -> TCM ()
tickMax s n = tick' s (max n)
getStatistics :: TCM Statistics
getStatistics = gets stStatistics