summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Monad/Benchmark.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Monad/Benchmark.hs')
-rw-r--r--src/full/Agda/TypeChecking/Monad/Benchmark.hs102
1 files changed, 57 insertions, 45 deletions
diff --git a/src/full/Agda/TypeChecking/Monad/Benchmark.hs b/src/full/Agda/TypeChecking/Monad/Benchmark.hs
index 3c93221..9177303 100644
--- a/src/full/Agda/TypeChecking/Monad/Benchmark.hs
+++ b/src/full/Agda/TypeChecking/Monad/Benchmark.hs
@@ -5,75 +5,87 @@
module Agda.TypeChecking.Monad.Benchmark
( module Agda.TypeChecking.Monad.Base.Benchmark
, getBenchmark
- , benchmarking, reportBenchmarkingLn, reportBenchmarkingDoc
- , billTo, billTop, billPureTo, billSub
- , reimburse, reimburseTop
+ , benchmarking
+ , billTo, billPureTo
+ , print
) where
import qualified Control.Exception as E (evaluate)
import Control.Monad.State
+import Data.List
+import Prelude hiding (print)
+import qualified Text.PrettyPrint.Boxes as Boxes
import Agda.TypeChecking.Monad.Base.Benchmark
import Agda.TypeChecking.Monad.Base
import{-# SOURCE #-} Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.State
+import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
-import Agda.Utils.Pretty (Doc)
+import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Time
+import qualified Agda.Utils.Trie as Trie
#include "undefined.h"
import Agda.Utils.Impossible
+benchmarkKey :: String
+benchmarkKey = "profile"
+
+benchmarkLevel :: Int
+benchmarkLevel = 7
+
-- | Check whether benchmarking is activated.
{-# SPECIALIZE benchmarking :: TCM Bool #-}
benchmarking :: MonadTCM tcm => tcm Bool
-benchmarking = liftTCM $ hasVerbosity "profile" 7
-
--- | Report benchmarking results.
-reportBenchmarkingLn :: String -> TCM ()
-reportBenchmarkingLn = reportSLn "profile" 7
-
--- | Report benchmarking results.
-reportBenchmarkingDoc :: TCM Doc -> TCM ()
-reportBenchmarkingDoc = reportSDoc "profile" 7
+benchmarking = liftTCM $ hasVerbosity benchmarkKey benchmarkLevel
+
+-- | Prints the accumulated benchmark results. Does nothing if
+-- profiling is not activated at level 7.
+print :: MonadTCM tcm => tcm ()
+print = liftTCM $ whenM benchmarking $ do
+
+ (accounts, times) <- unzip . Trie.toList . timings <$> getBenchmark
+
+ -- Generate a table.
+ let -- First column: Accounts.
+ col1 = Boxes.vcat Boxes.left $
+ map Boxes.text $
+ "Total" : map showAccount accounts
+ -- Second column: Times.
+ col2 = Boxes.vcat Boxes.right $
+ map (Boxes.text . prettyShow) $
+ sum times : times
+ table = Boxes.hsep 1 Boxes.left [col1, col2]
+ reportSLn benchmarkKey benchmarkLevel $
+ Boxes.render table
+
+ where
+ showAccount [] = "Miscellaneous"
+ showAccount ks = intercalate "." (map show ks)
--- | Bill a computation to a specific account (True) or reimburse (False).
-billTo' :: MonadTCM tcm => Bool -> Account -> tcm a -> tcm a
-billTo' add k m = ifNotM benchmarking m {- else -} $ do
- (res, time) <- measureTime $ liftIO . E.evaluate =<< m
- addToAccount k $ if add then time else -time
- return res
+-- | Add CPU time to specified account.
+addToAccount :: Account -> CPUTime -> TCM ()
+addToAccount k v = modifyBenchmark $ addCPUTime k v
-- | Bill a computation to a specific account.
billTo :: MonadTCM tcm => Account -> tcm a -> tcm a
-billTo = billTo' True
-
--- | Bill a top account.
-billTop :: MonadTCM tcm => Phase -> tcm a -> tcm a
-billTop k = billTo [k]
-
--- | Bill a sub account.
-billSub :: MonadTCM tcm => Account -> tcm a -> tcm a
-billSub [] = __IMPOSSIBLE__
-billSub k = reimburse (init k) . billTo k
+billTo account m = ifNotM benchmarking m {- else -} $ do
+ oldAccount <- liftTCM $ do
+ oldAccount <- currentAccount <$> liftTCM getBenchmark
+ modifyBenchmark $ modifyCurrentAccount $ const (Strict.Just account)
+ return oldAccount
+ (res, time) <- measureTime $ liftIO . E.evaluate =<< m
+ liftTCM $ do
+ addToAccount account time
+ case oldAccount of
+ Strict.Just acc -> addToAccount acc (- time)
+ Strict.Nothing -> return ()
+ modifyBenchmark $ modifyCurrentAccount $ const oldAccount
+ return res
-- | Bill a pure computation to a specific account.
{-# SPECIALIZE billPureTo :: Account -> a -> TCM a #-}
billPureTo :: MonadTCM tcm => Account -> a -> tcm a
-billPureTo k a = liftTCM $ billTo k $ return a
--- billPureTo k a = liftTCM $ billTo k $ liftIO $ E.evaluate a
-
--- | Reimburse a specific account for computation costs.
-reimburse :: MonadTCM tcm => Account -> tcm a -> tcm a
-reimburse = billTo' False
-
--- | Reimburse a top account.
-reimburseTop :: MonadTCM tcm => Phase -> tcm a -> tcm a
-reimburseTop k = reimburse [k]
-
--- * Auxiliary functions
-
--- | Add CPU time to specified account.
-addToAccount :: MonadTCM tcm => Account -> CPUTime -> tcm ()
-addToAccount k v = liftTCM $ modifyBenchmark $ addCPUTime k v
+billPureTo k a = billTo k $ return a