-- | 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.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 = n () -> m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n () -> m ())
-> ((Integer -> Integer) -> n ()) -> (Integer -> Integer) -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> (Integer -> Integer) -> n ()
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 ((Statistics -> Statistics) -> TCM ())
-> (Statistics -> Statistics) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Statistics -> Statistics
forall {b}. NFData b => b -> b
force (Statistics -> Statistics)
-> (Statistics -> Statistics) -> Statistics -> Statistics
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 = b -> ()
forall a. NFData a => a -> ()
rnf b
m () -> b -> b
`seq` b
m
      update :: Statistics -> Statistics
update  = (Integer -> Integer -> Integer)
-> String -> Integer -> Statistics -> Statistics
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 = Lens' Statistics TCState -> m Statistics
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 Lens' Statistics TCState -> (Statistics -> Statistics) -> TCM ()
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 = String -> Integer -> m ()
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 = String -> (Integer -> Integer) -> m ()
forall (m :: * -> *).
MonadStatistics m =>
String -> (Integer -> Integer) -> m ()
modifyCounter String
s (Integer
n Integer -> Integer -> Integer
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 = String -> (Integer -> Integer) -> m ()
forall (m :: * -> *).
MonadStatistics m =>
String -> (Integer -> Integer) -> m ()
modifyCounter String
s (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
n)

-- | Print the given statistics if verbosity "profile.ticks" is given.
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 = String -> Int -> m () -> m ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS String
"profile.ticks" Int
vl (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  [(String, Integer)] -> ([(String, Integer)] -> m ()) -> m ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (Statistics -> [(String, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList Statistics
stats) (([(String, Integer)] -> m ()) -> m ())
-> ([(String, Integer)] -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ [(String, Integer)]
stats -> do
    let -- First column (left aligned) is accounts.
        col1 :: Box
col1 = Alignment -> [Box] -> Box
forall (f :: * -> *). Foldable f => Alignment -> f Box -> Box
Boxes.vcat Alignment
Boxes.left  ([Box] -> Box) -> [Box] -> Box
forall a b. (a -> b) -> a -> b
$ ((String, Integer) -> Box) -> [(String, Integer)] -> [Box]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Box
Boxes.text (String -> Box)
-> ((String, Integer) -> String) -> (String, Integer) -> Box
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Integer) -> String
forall a b. (a, b) -> a
fst) [(String, Integer)]
stats
        -- Second column (right aligned) is numbers.
        col2 :: Box
col2 = Alignment -> [Box] -> Box
forall (f :: * -> *). Foldable f => Alignment -> f Box -> Box
Boxes.vcat Alignment
Boxes.right ([Box] -> Box) -> [Box] -> Box
forall a b. (a -> b) -> a -> b
$ ((String, Integer) -> Box) -> [(String, Integer)] -> [Box]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Box
Boxes.text (String -> Box)
-> ((String, Integer) -> String) -> (String, Integer) -> Box
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
showThousandSep (Integer -> String)
-> ((String, Integer) -> Integer) -> (String, Integer) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Integer) -> Integer
forall a b. (a, b) -> b
snd) [(String, Integer)]
stats
        table :: Box
table = Int -> Alignment -> [Box] -> Box
forall (f :: * -> *).
Foldable f =>
Int -> Alignment -> f Box -> Box
Boxes.hsep Int
1 Alignment
Boxes.left [Box
col1, Box
col2]
    String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"profile" Int
1 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ Maybe TopLevelModuleName
-> String -> (TopLevelModuleName -> String) -> String
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe TopLevelModuleName
mmname String
"Accumulated statistics" ((TopLevelModuleName -> String) -> String)
-> (TopLevelModuleName -> String) -> String
forall a b. (a -> b) -> a -> b
$ \ TopLevelModuleName
mname ->
      String
"Statistics for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
mname
    String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"profile" Int
1 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ Box -> String
Boxes.render Box
table