module Agda.TypeChecking.Monad.Benchmark
( module Agda.TypeChecking.Monad.Base.Benchmark
, getBenchmark
, benchmarking, reportBenchmarkingLn, reportBenchmarkingDoc
, billTo, billTop, billPureTo, billSub
, reimburse, reimburseTop
) where
import qualified Control.Exception as E (evaluate)
import Control.Monad.State
import Agda.TypeChecking.Monad.Base.Benchmark
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.State
import Agda.Utils.Monad
import Agda.Utils.Pretty (Doc)
import Agda.Utils.Time
#include "undefined.h"
import Agda.Utils.Impossible
benchmarking :: MonadTCM tcm => tcm Bool
benchmarking = liftTCM $ hasVerbosity "profile" 7
reportBenchmarkingLn :: String -> TCM ()
reportBenchmarkingLn = reportSLn "profile" 7
reportBenchmarkingDoc :: TCM Doc -> TCM ()
reportBenchmarkingDoc = reportSDoc "profile" 7
billTo' :: MonadTCM tcm => Bool -> Account -> tcm a -> tcm a
billTo' add k m = ifNotM benchmarking m $ do
(res, time) <- measureTime $ liftIO . E.evaluate =<< m
addToAccount k $ if add then time else time
return res
billTo :: MonadTCM tcm => Account -> tcm a -> tcm a
billTo = billTo' True
billTop :: MonadTCM tcm => Phase -> tcm a -> tcm a
billTop k = billTo [k]
billSub :: MonadTCM tcm => Account -> tcm a -> tcm a
billSub [] = __IMPOSSIBLE__
billSub k = reimburse (init k) . billTo k
billPureTo :: MonadTCM tcm => Account -> a -> tcm a
billPureTo k a = liftTCM $ billTo k $ return a
reimburse :: MonadTCM tcm => Account -> tcm a -> tcm a
reimburse = billTo' False
reimburseTop :: MonadTCM tcm => Phase -> tcm a -> tcm a
reimburseTop k = reimburse [k]
addToAccount :: MonadTCM tcm => Account -> CPUTime -> tcm ()
addToAccount k v = liftTCM $ modifyBenchmark $ addCPUTime k v