{-# LANGUAGE CPP                       #-}
{-# LANGUAGE IncoherentInstances       #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

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

-- | Agda-specific benchmarking structure.

module Agda.Benchmarking where

import qualified Control.Exception as E

import Data.IORef

import System.IO.Unsafe

import Agda.Syntax.Concrete.Name (TopLevelModuleName)
import Agda.Syntax.Concrete.Pretty
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'.
  | 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 (Eq, Ord, Show)

instance Pretty Phase where
  pretty (TopModule m)  = pretty m
  pretty (Definition q) = pretty q
  pretty a = text (show a)

type Benchmark = B.Benchmark Phase
type Account   = B.Account Phase

isModuleAccount :: Account -> Bool
isModuleAccount []                = True
isModuleAccount (TopModule{} : _) = True
isModuleAccount _                 = False

isDefAccount :: Account -> Bool
isDefAccount []                 = True
isDefAccount (Definition{} : _) = True
isDefAccount _                  = False

isInternalAccount :: Account -> Bool
isInternalAccount (TopModule{}  : _) = False
isInternalAccount (Definition{} : _) = False
isInternalAccount _                  = True

-- * Benchmarking in the IO monad.

-- | Global variable to store benchmark statistics.
{-# NOINLINE benchmarks #-}
benchmarks :: IORef Benchmark
benchmarks = unsafePerformIO $ newIORef empty

instance MonadBench Phase IO where
  getBenchmark = readIORef benchmarks
  putBenchmark = writeIORef benchmarks
  finally = E.finally

-- | Benchmark an IO computation and bill it to the given account.
billToIO :: Account -> IO a -> IO a
billToIO = B.billTo

-- | Benchmark a pure computation and bill it to the given account.
billToPure :: Account -> a -> a
billToPure acc a = unsafePerformIO $ billToIO acc $ return a