{-# OPTIONS_GHC -Wunused-imports #-}

-- | Collect statistics.

module Agda.TypeChecking.Monad.Statistics
  ( MonadStatistics(..), tick, getStatistics, modifyStatistics, printStatistics
  ) where

import Control.DeepSeq ( NFData(rnf) )
import Control.Monad.Except ( ExceptT )
import Control.Monad.Reader ( ReaderT )
import Control.Monad.State ( StateT )
import Control.Monad.Writer ( WriterT )
import Control.Monad.Trans.Class ( MonadTrans(lift) )
import Control.Monad.Trans.Maybe ( MaybeT )

import qualified Data.HashMap.Strict as HMap
import Data.Semigroup ( Max(..), Sum(..) )
import Data.Coerce ( coerce )

import Data.List ( sortOn )
import Data.Word ( Word64 )

import qualified Text.PrettyPrint.Boxes as Boxes

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug ( MonadDebug, alwaysReportSLn )

import Agda.Syntax.Common.Pretty ( prettyShow )
import Agda.Utils.String ( showThousandSep )
import Agda.Utils.Maybe ( caseMaybe )
import Agda.Utils.Null ( unlessNull )

class ReadTCState m => MonadStatistics m where
  tickN   :: String -> Word64 -> m ()
  tickMax :: String -> Word64 -> m ()

  default tickN :: (MonadStatistics n, MonadTrans t, t n ~ m) => String -> Word64 -> m ()
  tickN 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 ()) -> (Word64 -> n ()) -> Word64 -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Word64 -> n ()
forall (m :: * -> *). MonadStatistics m => String -> Word64 -> m ()
tickN String
x

  default tickMax :: (MonadStatistics n, MonadTrans t, t n ~ m) => String -> Word64 -> m ()
  tickMax 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 ()) -> (Word64 -> n ()) -> Word64 -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Word64 -> n ()
forall (m :: * -> *). MonadStatistics m => String -> Word64 -> m ()
tickMax 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
  tickN :: String -> Word64 -> TCM ()
tickN String
x Word64
n = (Statistics -> Statistics) -> TCM ()
modifyStatistics \case
    Statistics HashMap String (Sum Word64)
a HashMap String (Max Word64)
b ->
      let a' :: HashMap String (Sum Word64)
a' = (Sum Word64 -> Sum Word64 -> Sum Word64)
-> String
-> Sum Word64
-> HashMap String (Sum Word64)
-> HashMap String (Sum Word64)
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HMap.insertWith Sum Word64 -> Sum Word64 -> Sum Word64
forall a. Semigroup a => a -> a -> a
(<>) String
x (Word64 -> Sum Word64
forall a. a -> Sum a
Sum Word64
n) HashMap String (Sum Word64)
a
      -- 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.
      in HashMap String (Sum Word64) -> ()
forall a. NFData a => a -> ()
rnf HashMap String (Sum Word64)
a' () -> Statistics -> Statistics
forall a b. a -> b -> b
`seq` HashMap String (Sum Word64)
-> HashMap String (Max Word64) -> Statistics
Statistics HashMap String (Sum Word64)
a' HashMap String (Max Word64)
b

  tickMax :: String -> Word64 -> TCM ()
tickMax String
x Word64
n = (Statistics -> Statistics) -> TCM ()
modifyStatistics \case
    Statistics HashMap String (Sum Word64)
a HashMap String (Max Word64)
b ->
      let b' :: HashMap String (Max Word64)
b' = (Max Word64 -> Max Word64 -> Max Word64)
-> String
-> Max Word64
-> HashMap String (Max Word64)
-> HashMap String (Max Word64)
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HMap.insertWith Max Word64 -> Max Word64 -> Max Word64
forall a. Semigroup a => a -> a -> a
(<>) String
x (Word64 -> Max Word64
forall a. a -> Max a
Max Word64
n) HashMap String (Max Word64)
b
       in HashMap String (Max Word64) -> ()
forall a. NFData a => a -> ()
rnf HashMap String (Max Word64)
b' () -> Statistics -> Statistics
forall a b. a -> b -> b
`seq` HashMap String (Sum Word64)
-> HashMap String (Max Word64) -> Statistics
Statistics HashMap String (Sum Word64)
a HashMap String (Max Word64)
b'

-- | 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 -> Word64 -> m ()
forall (m :: * -> *). MonadStatistics m => String -> Word64 -> m ()
tickN String
x Word64
1

-- | 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 HashMap String (Sum Word64)
tick HashMap String (Max Word64)
max) = do
  let
    counters :: [(String, Word64)]
    counters :: [(String, Word64)]
counters = ((String, Word64) -> String)
-> [(String, Word64)] -> [(String, Word64)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (String, Word64) -> String
forall a b. (a, b) -> a
fst ([(String, Word64)] -> [(String, Word64)])
-> [(String, Word64)] -> [(String, Word64)]
forall a b. (a -> b) -> a -> b
$ HashMap String Word64 -> [(String, Word64)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList (HashMap String (Sum Word64) -> HashMap String Word64
forall a b. Coercible a b => a -> b
coerce HashMap String (Sum Word64)
tick) [(String, Word64)] -> [(String, Word64)] -> [(String, Word64)]
forall a. Semigroup a => a -> a -> a
<> HashMap String Word64 -> [(String, Word64)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList (HashMap String (Max Word64) -> HashMap String Word64
forall a b. Coercible a b => a -> b
coerce HashMap String (Max Word64)
max)

  [(String, Word64)] -> ([(String, Word64)] -> m ()) -> m ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [(String, Word64)]
counters (([(String, Word64)] -> m ()) -> m ())
-> ([(String, Word64)] -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ [(String, Word64)]
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, Word64) -> Box) -> [(String, Word64)] -> [Box]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Box
Boxes.text (String -> Box)
-> ((String, Word64) -> String) -> (String, Word64) -> Box
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Word64) -> String
forall a b. (a, b) -> a
fst) [(String, Word64)]
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, Word64) -> Box) -> [(String, Word64)] -> [Box]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Box
Boxes.text (String -> Box)
-> ((String, Word64) -> String) -> (String, Word64) -> Box
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> String
forall a. Show a => a -> String
showThousandSep (Word64 -> String)
-> ((String, Word64) -> Word64) -> (String, Word64) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Word64) -> Word64
forall a b. (a, b) -> b
snd) [(String, Word64)]
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 ()
alwaysReportSLn 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 ()
alwaysReportSLn String
"" Int
1 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ Box -> String
Boxes.render Box
table