{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.Benchmarking where
import Control.DeepSeq
import qualified Control.Exception as E
import Data.IORef
import GHC.Generics (Generic)
import System.IO.Unsafe
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Abstract.Name
import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)
import Agda.Utils.Benchmark (MonadBench(..))
import qualified Agda.Utils.Benchmark as B
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty
data Phase
= Parsing
| Import
| Deserialization
| Scoping
| Typing
| Termination
| Positivity
| Injectivity
| ProjectionLikeness
| Coverage
| Highlighting
| Serialization
| DeadCode
| InterfaceInstantiateFull
| DeadCodeReachable
| Graph
| RecCheck
| Reduce
| Level
| Compare
| With
| ModuleName
| Compaction
| BuildInterface
| Sort
| BinaryEncode
| Compress
| OperatorsExpr
| OperatorsPattern
| Free
| OccursCheck
| CheckLHS
| CheckRHS
| TypeSig
| Generalize
| InstanceSearch
| Reflection
| InitialCandidates
| FilterCandidates
| OrderCandidates
| CheckOverlap
| UnifyIndices
| InverseScopeLookup
| TopModule TopLevelModuleName
| Typeclass QName
| Definition QName
deriving (Phase -> Phase -> Bool
(Phase -> Phase -> Bool) -> (Phase -> Phase -> Bool) -> Eq Phase
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Phase -> Phase -> Bool
== :: Phase -> Phase -> Bool
$c/= :: Phase -> Phase -> Bool
/= :: Phase -> Phase -> Bool
Eq, Eq Phase
Eq Phase =>
(Phase -> Phase -> Ordering)
-> (Phase -> Phase -> Bool)
-> (Phase -> Phase -> Bool)
-> (Phase -> Phase -> Bool)
-> (Phase -> Phase -> Bool)
-> (Phase -> Phase -> Phase)
-> (Phase -> Phase -> Phase)
-> Ord Phase
Phase -> Phase -> Bool
Phase -> Phase -> Ordering
Phase -> Phase -> Phase
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Phase -> Phase -> Ordering
compare :: Phase -> Phase -> Ordering
$c< :: Phase -> Phase -> Bool
< :: Phase -> Phase -> Bool
$c<= :: Phase -> Phase -> Bool
<= :: Phase -> Phase -> Bool
$c> :: Phase -> Phase -> Bool
> :: Phase -> Phase -> Bool
$c>= :: Phase -> Phase -> Bool
>= :: Phase -> Phase -> Bool
$cmax :: Phase -> Phase -> Phase
max :: Phase -> Phase -> Phase
$cmin :: Phase -> Phase -> Phase
min :: Phase -> Phase -> Phase
Ord, Int -> Phase -> ShowS
[Phase] -> ShowS
Phase -> String
(Int -> Phase -> ShowS)
-> (Phase -> String) -> ([Phase] -> ShowS) -> Show Phase
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Phase -> ShowS
showsPrec :: Int -> Phase -> ShowS
$cshow :: Phase -> String
show :: Phase -> String
$cshowList :: [Phase] -> ShowS
showList :: [Phase] -> ShowS
Show, (forall x. Phase -> Rep Phase x)
-> (forall x. Rep Phase x -> Phase) -> Generic Phase
forall x. Rep Phase x -> Phase
forall x. Phase -> Rep Phase x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Phase -> Rep Phase x
from :: forall x. Phase -> Rep Phase x
$cto :: forall x. Rep Phase x -> Phase
to :: forall x. Rep Phase x -> Phase
Generic)
instance Pretty Phase where
pretty :: Phase -> Doc
pretty (TopModule TopLevelModuleName
m) = TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty TopLevelModuleName
m
pretty (Definition QName
q) = QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q
pretty Phase
a = String -> Doc
forall a. String -> Doc a
text (Phase -> String
forall a. Show a => a -> String
show Phase
a)
instance NFData Phase
type Benchmark = B.Benchmark Phase
type Account = B.Account Phase
isModuleAccount :: Account -> Bool
isModuleAccount :: [Phase] -> Bool
isModuleAccount [] = Bool
True
isModuleAccount (TopModule{} : [Phase]
_) = Bool
True
isModuleAccount [Phase]
_ = Bool
False
isDefAccount :: Account -> Bool
isDefAccount :: [Phase] -> Bool
isDefAccount [] = Bool
True
isDefAccount (Definition{} : [Phase]
_) = Bool
True
isDefAccount [Phase]
_ = Bool
False
isInternalAccount :: Account -> Bool
isInternalAccount :: [Phase] -> Bool
isInternalAccount (TopModule{} : [Phase]
_) = Bool
False
isInternalAccount (Definition{} : [Phase]
_) = Bool
False
isInternalAccount [Phase]
_ = Bool
True
{-# NOINLINE benchmarks #-}
benchmarks :: IORef Benchmark
benchmarks :: IORef Benchmark
benchmarks = IO (IORef Benchmark) -> IORef Benchmark
forall a. IO a -> a
unsafePerformIO (IO (IORef Benchmark) -> IORef Benchmark)
-> IO (IORef Benchmark) -> IORef Benchmark
forall a b. (a -> b) -> a -> b
$ Benchmark -> IO (IORef Benchmark)
forall a. a -> IO (IORef a)
newIORef Benchmark
forall a. Null a => a
empty
instance MonadBench IO where
type BenchPhase IO = Phase
getBenchmark :: IO (Benchmark (BenchPhase IO))
getBenchmark = IORef Benchmark -> IO Benchmark
forall a. IORef a -> IO a
readIORef IORef Benchmark
benchmarks
putBenchmark :: Benchmark (BenchPhase IO) -> IO ()
putBenchmark = IORef Benchmark -> Benchmark -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Benchmark
benchmarks
finally :: forall b c. IO b -> IO c -> IO b
finally = IO b -> IO c -> IO b
forall b c. IO b -> IO c -> IO b
E.finally
billToIO :: Account -> IO a -> IO a
billToIO :: forall a. [Phase] -> IO a -> IO a
billToIO = Account (BenchPhase IO) -> IO a -> IO a
[Phase] -> IO a -> IO a
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
B.billTo
billToPure :: Account -> a -> a
billToPure :: forall a. [Phase] -> a -> a
billToPure [Phase]
acc a
a = IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> IO a -> a
forall a b. (a -> b) -> a -> b
$ [Phase] -> IO a -> IO a
forall a. [Phase] -> IO a -> IO a
billToIO [Phase]
acc (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$ a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
{-# NOINLINE billToPure #-}