{-# OPTIONS_GHC -Wunused-imports #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | Agda-specific benchmarking structure.

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 () --instance only
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

-- | Phases to allocate CPU time to.
data Phase
  = Parsing
    -- ^ Happy parsing and operator parsing.
  | Import
    -- ^ Import chasing.
  | Deserialization
    -- ^ Reading interface files.
  | Scoping
    -- ^ Scope checking and translation to abstract syntax.
  | Typing
    -- ^ Type checking and translation to internal syntax.
  | Termination
    -- ^ Termination checking.
  | Positivity
    -- ^ Positivity checking and polarity computation.
  | Injectivity
    -- ^ Injectivity checking.
  | ProjectionLikeness
    -- ^ Checking for projection likeness.
  | Coverage
    -- ^ Coverage checking and compilation to case trees.
  | Highlighting
    -- ^ Generating highlighting info.
  | Serialization
    -- ^ Writing interface files.
  | DeadCode
    -- ^ Dead code elimination.
  | InterfaceInstantiateFull
    -- ^ Unfolding all metas before serialization.
  | DeadCodeReachable
    -- ^ Dead code reachable definitions subphase.
  | Graph
    -- ^ Subphase for 'Termination'.
  | RecCheck
    -- ^ Subphase for 'Termination'.
  | Reduce
    -- ^ Subphase for 'Termination'.
  | Level
    -- ^ Subphase for 'Termination'.
  | Compare
    -- ^ Subphase for 'Termination'.
  | With
    -- ^ Subphase for 'Termination'.
  | ModuleName
    -- ^ Subphase for 'Import'.
  | Compaction
    -- ^ Subphase for 'Deserialization': compacting interfaces.
  | BuildInterface
    -- ^ Subphase for 'Serialization'.
  | Sort
    -- ^ Subphase for 'Serialization'.
  | BinaryEncode
    -- ^ Subphase for 'Serialization'.
  | Compress
    -- ^ Subphase for 'Serialization'.
  | OperatorsExpr
    -- ^ Subphase for 'Parsing'.
  | OperatorsPattern
    -- ^ Subphase for 'Parsing'.
  | Free
    -- ^ Subphase for 'Typing': free variable computation.
  | OccursCheck
    -- ^ Subphase for 'Typing': occurs check for solving metas.
  | CheckLHS
    -- ^ Subphase for 'Typing': checking the LHS
  | CheckRHS
    -- ^ Subphase for 'Typing': checking the RHS
  | TypeSig
    -- ^ Subphase for 'Typing': checking a type signature
  | Generalize
    -- ^ Subphase for 'Typing': generalizing over `variable`s
  | InstanceSearch
    -- ^ Subphase for 'Typing': solving instance goals
  | Reflection
    -- ^ Subphase for 'Typing': evaluating elaborator reflection
  | InitialCandidates
    -- ^ Subphase for 'InstanceSearch': collecting initial candidates
  | FilterCandidates
    -- ^ Subphase for 'InstanceSearch': checking candidates for validity
  | OrderCandidates
    -- ^ Subphase for 'InstanceSearch': ordering candidates for specificity
  | CheckOverlap
    -- ^ Subphase for 'InstanceSearch': reducing overlapping instances
  | UnifyIndices
    -- ^ Subphase for 'CheckLHS': unification of the indices
  | InverseScopeLookup
    -- ^ Pretty printing names.
  | 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

-- * Benchmarking in the IO monad.

-- | Global variable to store benchmark statistics.
{-# 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

-- | Benchmark an IO computation and bill it to the given account.
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

-- | Benchmark a pure computation and bill it to the given account.
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 #-}