    {-# 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.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 ()
    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