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.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 String
x = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
MonadStatistics m =>
String -> (Integer -> Integer) -> m ()
modifyCounter String
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 :: String -> (Integer -> Integer) -> TCM ()
modifyCounter String
x Integer -> Integer
f = (Statistics -> Statistics) -> TCM ()
modifyStatistics forall a b. (a -> b) -> a -> b
$ forall {b}. NFData b => b -> b
force forall b c a. (b -> c) -> (a -> b) -> a -> c
. Statistics -> Statistics
update
where
force :: b -> b
force b
m = forall a. NFData a => a -> ()
rnf b
m seq :: forall a b. a -> b -> b
`seq` b
m
update :: Statistics -> Statistics
update = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (\ Integer
new Integer
old -> Integer -> Integer
f Integer
old) String
x Integer
dummy
dummy :: Integer
dummy = Integer -> Integer
f Integer
0
getStatistics :: ReadTCState m => m Statistics
getStatistics :: forall (m :: * -> *). ReadTCState m => m Statistics
getStatistics = forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' Statistics TCState
stStatistics
modifyStatistics :: (Statistics -> Statistics) -> TCM ()
modifyStatistics :: (Statistics -> Statistics) -> TCM ()
modifyStatistics Statistics -> Statistics
f = Lens' Statistics TCState
stStatistics forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` Statistics -> Statistics
f
tick :: MonadStatistics m => String -> m ()
tick :: forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
x = forall (m :: * -> *).
MonadStatistics m =>
String -> Integer -> m ()
tickN String
x Integer
1
tickN :: MonadStatistics m => String -> Integer -> m ()
tickN :: forall (m :: * -> *).
MonadStatistics m =>
String -> Integer -> m ()
tickN String
s Integer
n = forall (m :: * -> *).
MonadStatistics m =>
String -> (Integer -> Integer) -> m ()
modifyCounter String
s (Integer
n forall a. Num a => a -> a -> a
+)
tickMax :: MonadStatistics m => String -> Integer -> m ()
tickMax :: forall (m :: * -> *).
MonadStatistics m =>
String -> Integer -> m ()
tickMax String
s Integer
n = forall (m :: * -> *).
MonadStatistics m =>
String -> (Integer -> Integer) -> m ()
modifyCounter String
s (forall a. Ord a => a -> a -> a
max Integer
n)
printStatistics
:: (MonadDebug m, MonadTCEnv m, HasOptions m)
=> Int -> Maybe C.TopLevelModuleName -> Statistics -> m ()
printStatistics :: forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, HasOptions m) =>
Int -> Maybe TopLevelModuleName -> Statistics -> m ()
printStatistics Int
vl Maybe TopLevelModuleName
mmname Statistics
stats = forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS String
"profile.ticks" Int
vl forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (forall k a. Map k a -> [(k, a)]
Map.toList Statistics
stats) forall a b. (a -> b) -> a -> b
$ \ [(String, Integer)]
stats -> do
let
col1 :: Box
col1 = forall (f :: * -> *). Foldable f => Alignment -> f Box -> Box
Boxes.vcat Alignment
Boxes.left forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (String -> Box
Boxes.text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(String, Integer)]
stats
col2 :: Box
col2 = forall (f :: * -> *). Foldable f => Alignment -> f Box -> Box
Boxes.vcat Alignment
Boxes.right forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (String -> Box
Boxes.text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
showThousandSep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(String, Integer)]
stats
table :: Box
table = forall (f :: * -> *).
Foldable f =>
Int -> Alignment -> f Box -> Box
Boxes.hsep Int
1 Alignment
Boxes.left [Box
col1, Box
col2]
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"profile" Int
1 forall a b. (a -> b) -> a -> b
$ forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe TopLevelModuleName
mmname String
"Accumulated statistics" forall a b. (a -> b) -> a -> b
$ \ TopLevelModuleName
mname ->
String
"Statistics for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
mname
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"profile" Int
1 forall a b. (a -> b) -> a -> b
$ Box -> String
Boxes.render Box
table