-- | Collect statistics.

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.TopLevelModuleName (TopLevelModuleName)

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
      -- We need to be strict in the map.
      -- Andreas, 2014-03-22:  Could we take Data.Map.Strict instead of this hack?
      -- Or force the map by looking up the very element we inserted?
      -- force m = Map.lookup x m `seq` m
      -- Or use insertLookupWithKey?
      -- update m = old `seq` m' where
      --   (old, m') = Map.insertLookupWithKey (\ _ new old -> f old) x dummy m
      -- Ulf, 2018-04-10: Neither of these approaches are strict enough in the
      -- map (nor are they less hacky). It's not enough to be strict in the
      -- values stored in the map, we also need to be strict in the *structure*
      -- of the map. A less hacky solution is to deepseq the map.
      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

-- | Get the statistics.
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

-- | Modify the statistics via given function.
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

-- | Increase specified counter by @1@.
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

-- | Increase specified counter by @n@.
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
+)

-- | Set the specified counter to the maximum of its current value and @n@.
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)

-- | Print the given statistics.
printStatistics
  :: (MonadDebug m, MonadTCEnv m, HasOptions m)
  => Maybe TopLevelModuleName -> Statistics -> m ()
printStatistics :: forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, HasOptions m) =>
Maybe TopLevelModuleName -> Statistics -> m ()
printStatistics Maybe TopLevelModuleName
mmname Statistics
stats = 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 -- First column (left aligned) is accounts.
        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
        -- Second column (right aligned) is numbers.
        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
"" 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
"" Int
1 forall a b. (a -> b) -> a -> b
$ Box -> String
Boxes.render Box
table