    {-# 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.Name (TopLevelModuleName)
    import Agda.Syntax.Concrete.Pretty () --instance only
    import Agda.Syntax.Abstract.Name
    import Agda.Utils.Benchmark (MonadBench(..))
    import qualified Agda.Utils.Benchmark as B
    import Agda.Utils.Null
    import Agda.Utils.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
        -- ^ Deac code elimination.
      | 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
      | UnifyIndices
        -- ^ Subphase for 'CheckLHS': unification of the indices
      | InverseScopeLookup
        -- ^ Pretty printing names.
      | TopModule TopLevelModuleName
      | Definition QName
      deriving (Phase -> Phase -> Bool
    (Phase -> Phase -> Bool) -> (Phase -> Phase -> Bool) -> Eq Phase
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Phase -> Phase -> Bool
    $c/= :: Phase -> Phase -> Bool
    == :: Phase -> Phase -> Bool
    $c== :: 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
    min :: Phase -> Phase -> Phase
    $cmin :: Phase -> Phase -> Phase
    max :: Phase -> Phase -> Phase
    $cmax :: Phase -> Phase -> Phase
    >= :: Phase -> Phase -> Bool
    $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
    compare :: Phase -> Phase -> Ordering
    $ccompare :: Phase -> Phase -> Ordering
    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
    showList :: [Phase] -> ShowS
    $cshowList :: [Phase] -> ShowS
    show :: Phase -> String
    $cshow :: Phase -> String
    showsPrec :: Int -> Phase -> ShowS
    $cshowsPrec :: Int -> 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
    $cto :: forall x. Rep Phase x -> Phase
    $cfrom :: forall x. Phase -> Rep Phase x
    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
    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 = [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 (m :: * -> *) a. Monad m => a -> m a
    return a
    a