    -- | 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 () -> t n ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n () -> t n ())
    -> ((Integer -> Integer) -> n ()) -> (Integer -> Integer) -> t n ()
    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 = (Map String Integer -> Map String Integer) -> TCM ()
    modifyStatistics ((Map String Integer -> Map String Integer) -> TCM ())
    -> (Map String Integer -> Map String Integer) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Map String Integer -> Map String Integer
    forall {b}. NFData b => b -> b
    force (Map String Integer -> Map String Integer)
    -> (Map String Integer -> Map String Integer)
    -> Map String Integer
    -> Map String Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map String Integer -> Map String Integer
    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 :: Map String Integer -> Map String Integer
    update  = (Integer -> Integer -> Integer)
    -> String -> Integer -> Map String Integer -> Map String Integer
    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 (Map String Integer)
    getStatistics = Lens' (Map String Integer) TCState -> m (Map String Integer)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' (Map String Integer) TCState
    stStatistics

    -- | Modify the statistics via given function.
    modifyStatistics :: (Statistics -> Statistics) -> TCM ()
    modifyStatistics :: (Map String Integer -> Map String Integer) -> TCM ()
    modifyStatistics Map String Integer -> Map String Integer
    f = Lens' (Map String Integer) TCState
    stStatistics Lens' (Map String Integer) TCState
    -> (Map String Integer -> Map String Integer) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` Map String Integer -> Map String Integer
    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 -> Map String Integer -> m ()
    printStatistics Int
    vl Maybe TopLevelModuleName
    mmname Map String Integer
    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 (Map String Integer -> [(String, Integer)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map String Integer
    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