{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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.Syntax.Common.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 ()
n () -> t n ()
forall (m :: * -> *) a. Monad m => m a -> t m a
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
forall a b. a -> 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' TCState Statistics -> m Statistics
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Statistics -> f Statistics) -> TCState -> f TCState
Lens' TCState Statistics
stStatistics

-- | Modify the statistics via given function.
modifyStatistics :: (Statistics -> Statistics) -> TCM ()
modifyStatistics :: (Statistics -> Statistics) -> TCM ()
modifyStatistics Statistics -> Statistics
f = (Statistics -> f Statistics) -> TCState -> f TCState
Lens' TCState Statistics
stStatistics Lens' TCState Statistics -> (Statistics -> Statistics) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (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.
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
  [(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
"" 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
"" Int
1 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ Box -> String
Boxes.render Box
table