{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE NumDecimals #-}
module Agda.TypeChecking.Monad.Benchmark
( module Agda.Benchmarking
, B.MonadBench
, B.BenchPhase
, B.getBenchmark
, updateBenchmarkingStatus
, B.billTo, B.billPureTo, B.billToCPS
, B.reset
, print
) where
import Prelude hiding (print)
import Data.Foldable (foldMap')
import Data.Function (on)
import Data.Maybe (fromMaybe, mapMaybe)
import Data.Monoid (Sum(..), getSum)
import qualified Data.Text.Lazy as TL
import Agda.Benchmarking
import Agda.Interaction.Options.Types( optParallelChecking, Parallelism(..) )
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Imports (getVisitedModule)
import qualified Agda.Utils.Benchmark as B
import qualified Agda.Utils.Trie as Trie
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.Monad
import Agda.Utils.Time (CPUTime(..), fromMilliseconds)
import Agda.Syntax.Common.Pretty
( Doc, Pretty, comma, hsep, nest, parens, pretty, prettyShow
, text, vcat, (<+>), ($+$)
)
import qualified Agda.Interaction.Options.ProfileOptions as Profile
updateBenchmarkingStatus :: TCM ()
updateBenchmarkingStatus :: TCM ()
updateBenchmarkingStatus =
BenchmarkOn (BenchPhase (TCMT IO)) -> TCM ()
BenchmarkOn Phase -> TCM ()
forall (m :: * -> *).
MonadBench m =>
BenchmarkOn (BenchPhase m) -> m ()
B.setBenchmarking (BenchmarkOn Phase -> TCM ())
-> TCMT IO (BenchmarkOn Phase) -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (BenchmarkOn Phase)
forall (tcm :: * -> *). MonadTCM tcm => tcm (BenchmarkOn Phase)
benchmarking
{-# SPECIALIZE benchmarking :: TCM (B.BenchmarkOn Phase) #-}
benchmarking :: MonadTCM tcm => tcm (B.BenchmarkOn Phase)
benchmarking :: forall (tcm :: * -> *). MonadTCM tcm => tcm (BenchmarkOn Phase)
benchmarking = TCMT IO (BenchmarkOn Phase) -> tcm (BenchmarkOn Phase)
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (BenchmarkOn Phase) -> tcm (BenchmarkOn Phase))
-> TCMT IO (BenchmarkOn Phase) -> tcm (BenchmarkOn Phase)
forall a b. (a -> b) -> a -> b
$
TCMT IO Bool
-> TCMT IO (BenchmarkOn Phase)
-> TCMT IO (BenchmarkOn Phase)
-> TCMT IO (BenchmarkOn Phase)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (ProfileOption -> TCMT IO Bool
forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
hasProfileOption ProfileOption
Profile.Internal) (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase))
-> BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
forall a b. (a -> b) -> a -> b
$ (Account Phase -> Bool) -> BenchmarkOn Phase
forall a. (Account a -> Bool) -> BenchmarkOn a
B.BenchmarkSome Account Phase -> Bool
isInternalAccount) (TCMT IO (BenchmarkOn Phase) -> TCMT IO (BenchmarkOn Phase))
-> TCMT IO (BenchmarkOn Phase) -> TCMT IO (BenchmarkOn Phase)
forall a b. (a -> b) -> a -> b
$
TCMT IO Bool
-> TCMT IO (BenchmarkOn Phase)
-> TCMT IO (BenchmarkOn Phase)
-> TCMT IO (BenchmarkOn Phase)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (ProfileOption -> TCMT IO Bool
forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
hasProfileOption ProfileOption
Profile.Definitions) (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase))
-> BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
forall a b. (a -> b) -> a -> b
$ (Account Phase -> Bool) -> BenchmarkOn Phase
forall a. (Account a -> Bool) -> BenchmarkOn a
B.BenchmarkSome Account Phase -> Bool
isDefAccount) (TCMT IO (BenchmarkOn Phase) -> TCMT IO (BenchmarkOn Phase))
-> TCMT IO (BenchmarkOn Phase) -> TCMT IO (BenchmarkOn Phase)
forall a b. (a -> b) -> a -> b
$
TCMT IO Bool
-> TCMT IO (BenchmarkOn Phase)
-> TCMT IO (BenchmarkOn Phase)
-> TCMT IO (BenchmarkOn Phase)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (ProfileOption -> TCMT IO Bool
forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
hasProfileOption ProfileOption
Profile.Modules) (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase))
-> BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
forall a b. (a -> b) -> a -> b
$ (Account Phase -> Bool) -> BenchmarkOn Phase
forall a. (Account a -> Bool) -> BenchmarkOn a
B.BenchmarkSome Account Phase -> Bool
isModuleAccount) (TCMT IO (BenchmarkOn Phase) -> TCMT IO (BenchmarkOn Phase))
-> TCMT IO (BenchmarkOn Phase) -> TCMT IO (BenchmarkOn Phase)
forall a b. (a -> b) -> a -> b
$
BenchmarkOn Phase -> TCMT IO (BenchmarkOn Phase)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BenchmarkOn Phase
forall a. BenchmarkOn a
B.BenchmarkOff
print :: MonadTCM tcm => tcm ()
print :: forall (tcm :: * -> *). MonadTCM tcm => tcm ()
print = TCM () -> tcm ()
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> tcm ()) -> TCM () -> tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Account Phase -> BenchmarkOn Phase -> Bool
forall a. Account a -> BenchmarkOn a -> Bool
B.isBenchmarkOn [] (BenchmarkOn Phase -> Bool)
-> TCMT IO (BenchmarkOn Phase) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (BenchmarkOn Phase)
forall (tcm :: * -> *). MonadTCM tcm => tcm (BenchmarkOn Phase)
benchmarking) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
b <- TCMT IO (Benchmark (BenchPhase (TCMT IO)))
TCMT IO (Benchmark Phase)
forall (m :: * -> *). MonadBench m => m (Benchmark (BenchPhase m))
B.getBenchmark
extra <- ifM moduleThroughputEnabled
(moduleThroughputDoc b)
(pure mempty)
displayDebugMessage "profile" 2 $ pretty b $+$ extra
moduleThroughputEnabled :: TCM Bool
moduleThroughputEnabled :: TCMT IO Bool
moduleThroughputEnabled = do
modulesProfiling <- ProfileOption -> TCMT IO Bool
forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
hasProfileOption ProfileOption
Profile.Modules
sequential <- sequentialTypeChecking
pure $ modulesProfiling && sequential
sequentialTypeChecking :: TCM Bool
sequentialTypeChecking :: TCMT IO Bool
sequentialTypeChecking = do
opts <- TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
pure $ case optParallelChecking opts of
Parallelism
Sequential -> Bool
True
Parallel{} -> Bool
False
data ModuleThroughput = ModuleThroughput
{ ModuleThroughput -> TopLevelModuleName
mtModuleName :: TopLevelModuleName
, ModuleThroughput -> Int
mtLineCount :: Int
, ModuleThroughput -> CPUTime
mtTime :: CPUTime
}
instance Pretty ModuleThroughput where
pretty :: ModuleThroughput -> Doc Aspects
pretty ModuleThroughput
mt =
VerboseKey -> Doc Aspects
forall a. VerboseKey -> Doc a
text (TopLevelModuleName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (TopLevelModuleName -> VerboseKey)
-> TopLevelModuleName -> VerboseKey
forall a b. (a -> b) -> a -> b
$ ModuleThroughput -> TopLevelModuleName
mtModuleName ModuleThroughput
mt) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+>
Doc Aspects -> Doc Aspects
parens
([Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
hsep
[ (VerboseKey -> Doc Aspects
forall a. VerboseKey -> Doc a
text (Int -> VerboseKey
forall a. Show a => a -> VerboseKey
show (ModuleThroughput -> Int
mtLineCount ModuleThroughput
mt)) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"lines") Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Semigroup a => a -> a -> a
<> Doc Aspects
comma
, VerboseKey -> Doc Aspects
forall a. VerboseKey -> Doc a
text (Integer -> VerboseKey
forall a. Show a => a -> VerboseKey
show (ModuleThroughput -> Integer
linesPerSecond ModuleThroughput
mt)) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"lines/s"
])
moduleThroughputDoc :: Benchmark -> TCM Doc
moduleThroughputDoc :: Benchmark Phase -> TCMT IO (Doc Aspects)
moduleThroughputDoc Benchmark Phase
b = do
stats <- ((TopLevelModuleName, CPUTime) -> TCMT IO ModuleThroughput)
-> [(TopLevelModuleName, CPUTime)] -> TCMT IO [ModuleThroughput]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (TopLevelModuleName, CPUTime) -> TCMT IO ModuleThroughput
loadModuleThroughput (Benchmark Phase -> [(TopLevelModuleName, CPUTime)]
moduleRows Benchmark Phase
b)
pure $ renderModuleThroughput stats
renderModuleThroughput :: [ModuleThroughput] -> Doc
renderModuleThroughput :: [ModuleThroughput] -> Doc Aspects
renderModuleThroughput [] = Doc Aspects
forall a. Monoid a => a
mempty
renderModuleThroughput [ModuleThroughput]
stats =
[Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat
[ Doc Aspects
forall a. Monoid a => a
mempty
, Doc Aspects
forall a. Monoid a => a
mempty
, VerboseKey -> Doc Aspects
forall a. VerboseKey -> Doc a
text VerboseKey
"Module throughput:"
, [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat ([Doc Aspects] -> Doc Aspects) -> [Doc Aspects] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ (ModuleThroughput -> Doc Aspects)
-> [ModuleThroughput] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc Aspects -> Doc Aspects
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc Aspects -> Doc Aspects)
-> (ModuleThroughput -> Doc Aspects)
-> ModuleThroughput
-> Doc Aspects
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleThroughput -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty) [ModuleThroughput]
stats
]
moduleRows :: Benchmark -> [(TopLevelModuleName, CPUTime)]
moduleRows :: Benchmark Phase -> [(TopLevelModuleName, CPUTime)]
moduleRows =
((Account Phase, (CPUTime, CPUTime))
-> Maybe (TopLevelModuleName, CPUTime))
-> [(Account Phase, (CPUTime, CPUTime))]
-> [(TopLevelModuleName, CPUTime)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Account Phase, (CPUTime, CPUTime))
-> Maybe (TopLevelModuleName, CPUTime)
forall {a} {b}.
(Account Phase, (a, b)) -> Maybe (TopLevelModuleName, b)
moduleRow ([(Account Phase, (CPUTime, CPUTime))]
-> [(TopLevelModuleName, CPUTime)])
-> (Benchmark Phase -> [(Account Phase, (CPUTime, CPUTime))])
-> Benchmark Phase
-> [(TopLevelModuleName, CPUTime)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Benchmark Phase -> [(Account Phase, (CPUTime, CPUTime))]
orderedBenchmarkEntries
where
moduleRow :: (Account Phase, (a, b)) -> Maybe (TopLevelModuleName, b)
moduleRow (Account Phase
acc, (a
_selfTime, b
totalTime)) =
case Account Phase
acc of
[TopModule TopLevelModuleName
m] -> (TopLevelModuleName, b) -> Maybe (TopLevelModuleName, b)
forall a. a -> Maybe a
Just (TopLevelModuleName
m, b
totalTime)
Account Phase
_ -> Maybe (TopLevelModuleName, b)
forall a. Maybe a
Nothing
orderedBenchmarkEntries :: Benchmark -> [(Account, (CPUTime, CPUTime))]
orderedBenchmarkEntries :: Benchmark Phase -> [(Account Phase, (CPUTime, CPUTime))]
orderedBenchmarkEntries =
((CPUTime, CPUTime) -> (CPUTime, CPUTime) -> Ordering)
-> Trie Phase (CPUTime, CPUTime)
-> [(Account Phase, (CPUTime, CPUTime))]
forall k v. Ord k => (v -> v -> Ordering) -> Trie k v -> [([k], v)]
Trie.toListOrderedBy ((CPUTime -> CPUTime -> Ordering) -> CPUTime -> CPUTime -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip CPUTime -> CPUTime -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (CPUTime -> CPUTime -> Ordering)
-> ((CPUTime, CPUTime) -> CPUTime)
-> (CPUTime, CPUTime)
-> (CPUTime, CPUTime)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (CPUTime, CPUTime) -> CPUTime
forall a b. (a, b) -> b
snd)
(Trie Phase (CPUTime, CPUTime)
-> [(Account Phase, (CPUTime, CPUTime))])
-> (Benchmark Phase -> Trie Phase (CPUTime, CPUTime))
-> Benchmark Phase
-> [(Account Phase, (CPUTime, CPUTime))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((CPUTime, CPUTime) -> Bool)
-> Trie Phase (CPUTime, CPUTime) -> Trie Phase (CPUTime, CPUTime)
forall k v. Ord k => (v -> Bool) -> Trie k v -> Trie k v
Trie.filter ((CPUTime -> CPUTime -> Bool
forall a. Ord a => a -> a -> Bool
> Integer -> CPUTime
fromMilliseconds Integer
10) (CPUTime -> Bool)
-> ((CPUTime, CPUTime) -> CPUTime) -> (CPUTime, CPUTime) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CPUTime, CPUTime) -> CPUTime
forall a b. (a, b) -> b
snd)
(Trie Phase (CPUTime, CPUTime) -> Trie Phase (CPUTime, CPUTime))
-> (Benchmark Phase -> Trie Phase (CPUTime, CPUTime))
-> Benchmark Phase
-> Trie Phase (CPUTime, CPUTime)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Trie Phase CPUTime -> Maybe (CPUTime, CPUTime))
-> Trie Phase CPUTime -> Trie Phase (CPUTime, CPUTime)
forall k u v.
Ord k =>
(Trie k u -> Maybe v) -> Trie k u -> Trie k v
Trie.mapSubTries ((CPUTime, CPUTime) -> Maybe (CPUTime, CPUTime)
forall a. a -> Maybe a
Just ((CPUTime, CPUTime) -> Maybe (CPUTime, CPUTime))
-> (Trie Phase CPUTime -> (CPUTime, CPUTime))
-> Trie Phase CPUTime
-> Maybe (CPUTime, CPUTime)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trie Phase CPUTime -> (CPUTime, CPUTime)
forall a. Ord a => Trie a CPUTime -> (CPUTime, CPUTime)
aggregateNode)
(Trie Phase CPUTime -> Trie Phase (CPUTime, CPUTime))
-> (Benchmark Phase -> Trie Phase CPUTime)
-> Benchmark Phase
-> Trie Phase (CPUTime, CPUTime)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Benchmark Phase -> Trie Phase CPUTime
forall a. Benchmark a -> Timings a
B.timings
aggregateNode :: Ord a => Trie.Trie a CPUTime -> (CPUTime, CPUTime)
aggregateNode :: forall a. Ord a => Trie a CPUTime -> (CPUTime, CPUTime)
aggregateNode Trie a CPUTime
t =
( CPUTime -> Maybe CPUTime -> CPUTime
forall a. a -> Maybe a -> a
fromMaybe CPUTime
0 (Maybe CPUTime -> CPUTime) -> Maybe CPUTime -> CPUTime
forall a b. (a -> b) -> a -> b
$ [a] -> Trie a CPUTime -> Maybe CPUTime
forall k v. Ord k => [k] -> Trie k v -> Maybe v
Trie.lookup [] Trie a CPUTime
t
, Sum CPUTime -> CPUTime
forall a. Sum a -> a
getSum (Sum CPUTime -> CPUTime) -> Sum CPUTime -> CPUTime
forall a b. (a -> b) -> a -> b
$ (CPUTime -> Sum CPUTime) -> Trie a CPUTime -> Sum CPUTime
forall m a. Monoid m => (a -> m) -> Trie a a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap' CPUTime -> Sum CPUTime
forall a. a -> Sum a
Sum Trie a CPUTime
t
)
loadModuleThroughput
:: (TopLevelModuleName, CPUTime)
-> TCM ModuleThroughput
loadModuleThroughput :: (TopLevelModuleName, CPUTime) -> TCMT IO ModuleThroughput
loadModuleThroughput (TopLevelModuleName
mName, CPUTime
totalTime) = do
mi <- TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule TopLevelModuleName
mName TCMT IO (Maybe ModuleInfo)
-> (Maybe ModuleInfo -> TCMT IO ModuleInfo) -> TCMT IO ModuleInfo
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just ModuleInfo
mi -> ModuleInfo -> TCMT IO ModuleInfo
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleInfo
mi
Maybe ModuleInfo
Nothing -> TCMT IO ModuleInfo
forall a. HasCallStack => a
__IMPOSSIBLE__
let lineCount = [VerboseKey] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (VerboseKey -> [VerboseKey]
lines (Text -> VerboseKey
TL.unpack (Interface -> Text
iSource (ModuleInfo -> Interface
miInterface ModuleInfo
mi))))
pure ModuleThroughput
{ mtModuleName = mName
, mtTime = totalTime
, mtLineCount = lineCount
}
picosecondsPerSecond :: Integer
picosecondsPerSecond :: Integer
picosecondsPerSecond = Integer
1e12
linesPerSecond :: ModuleThroughput -> Integer
linesPerSecond :: ModuleThroughput -> Integer
linesPerSecond ModuleThroughput{ Int
mtLineCount :: ModuleThroughput -> Int
mtLineCount :: Int
mtLineCount, mtTime :: ModuleThroughput -> CPUTime
mtTime = CPUTime Integer
ps }
| Integer
ps Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer
0
| Bool
otherwise = Double -> Integer
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
round Double
throughput
where
elapsedSeconds :: Double
elapsedSeconds =
Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
ps Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
picosecondsPerSecond
throughput :: Double
throughput =
Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
mtLineCount Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
elapsedSeconds