module Agda.Interaction.Options.ProfileOptions
  ( ProfileOption(..)
  , ProfileOptions
  , noProfileOptions
  , addProfileOption
  , containsProfileOption
  , profileOptionsToList
  , profileOptionsFromList
  , validProfileOptionStrings
  ) where

import Control.DeepSeq
import Control.Monad
import Data.List (intercalate)
import Data.Char (toLower)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import GHC.Generics (Generic)
import Text.EditDistance (restrictedDamerauLevenshteinDistance, defaultEditCosts)

import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null (Null, empty)

-- | Various things that can be measured when checking an Agda development. Turned on with
--   the `--profile` flag, for instance `--profile=sharing` to turn on the 'Sharing' option.
--   'Internal', 'Modules', and 'Definitions' are mutually exclusive.
--
--   NOTE: Changing this data type requires bumping the interface version number in
--   'Agda.TypeChecking.Serialise.currentInterfaceVersion'.
data ProfileOption
  = Internal     -- ^ Measure time taken by various parts of the system (type checking, serialization, etc)
  | Modules      -- ^ Measure time spent on individual (Agda) modules
  | Definitions  -- ^ Measure time spent on individual (Agda) definitions
  | Sharing      -- ^ Measure things related to sharing
  | Serialize    -- ^ Collect detailed statistics about serialization
  | Constraints  -- ^ Collect statistics about constraint solving
  | Metas        -- ^ Count number of created metavariables
  | Interactive  -- ^ Measure time of interactive commands
  | Conversion   -- ^ Collect statistics about conversion checking
  | Instances    -- ^ Collect statistics about instance search
  | Sections     -- ^ Collect statistics about section applications
  deriving (Int -> ProfileOption -> ShowS
[ProfileOption] -> ShowS
ProfileOption -> [Char]
(Int -> ProfileOption -> ShowS)
-> (ProfileOption -> [Char])
-> ([ProfileOption] -> ShowS)
-> Show ProfileOption
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProfileOption -> ShowS
showsPrec :: Int -> ProfileOption -> ShowS
$cshow :: ProfileOption -> [Char]
show :: ProfileOption -> [Char]
$cshowList :: [ProfileOption] -> ShowS
showList :: [ProfileOption] -> ShowS
Show, ProfileOption -> ProfileOption -> Bool
(ProfileOption -> ProfileOption -> Bool)
-> (ProfileOption -> ProfileOption -> Bool) -> Eq ProfileOption
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ProfileOption -> ProfileOption -> Bool
== :: ProfileOption -> ProfileOption -> Bool
$c/= :: ProfileOption -> ProfileOption -> Bool
/= :: ProfileOption -> ProfileOption -> Bool
Eq, Eq ProfileOption
Eq ProfileOption =>
(ProfileOption -> ProfileOption -> Ordering)
-> (ProfileOption -> ProfileOption -> Bool)
-> (ProfileOption -> ProfileOption -> Bool)
-> (ProfileOption -> ProfileOption -> Bool)
-> (ProfileOption -> ProfileOption -> Bool)
-> (ProfileOption -> ProfileOption -> ProfileOption)
-> (ProfileOption -> ProfileOption -> ProfileOption)
-> Ord ProfileOption
ProfileOption -> ProfileOption -> Bool
ProfileOption -> ProfileOption -> Ordering
ProfileOption -> ProfileOption -> ProfileOption
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 :: ProfileOption -> ProfileOption -> Ordering
compare :: ProfileOption -> ProfileOption -> Ordering
$c< :: ProfileOption -> ProfileOption -> Bool
< :: ProfileOption -> ProfileOption -> Bool
$c<= :: ProfileOption -> ProfileOption -> Bool
<= :: ProfileOption -> ProfileOption -> Bool
$c> :: ProfileOption -> ProfileOption -> Bool
> :: ProfileOption -> ProfileOption -> Bool
$c>= :: ProfileOption -> ProfileOption -> Bool
>= :: ProfileOption -> ProfileOption -> Bool
$cmax :: ProfileOption -> ProfileOption -> ProfileOption
max :: ProfileOption -> ProfileOption -> ProfileOption
$cmin :: ProfileOption -> ProfileOption -> ProfileOption
min :: ProfileOption -> ProfileOption -> ProfileOption
Ord, Int -> ProfileOption
ProfileOption -> Int
ProfileOption -> [ProfileOption]
ProfileOption -> ProfileOption
ProfileOption -> ProfileOption -> [ProfileOption]
ProfileOption -> ProfileOption -> ProfileOption -> [ProfileOption]
(ProfileOption -> ProfileOption)
-> (ProfileOption -> ProfileOption)
-> (Int -> ProfileOption)
-> (ProfileOption -> Int)
-> (ProfileOption -> [ProfileOption])
-> (ProfileOption -> ProfileOption -> [ProfileOption])
-> (ProfileOption -> ProfileOption -> [ProfileOption])
-> (ProfileOption
    -> ProfileOption -> ProfileOption -> [ProfileOption])
-> Enum ProfileOption
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: ProfileOption -> ProfileOption
succ :: ProfileOption -> ProfileOption
$cpred :: ProfileOption -> ProfileOption
pred :: ProfileOption -> ProfileOption
$ctoEnum :: Int -> ProfileOption
toEnum :: Int -> ProfileOption
$cfromEnum :: ProfileOption -> Int
fromEnum :: ProfileOption -> Int
$cenumFrom :: ProfileOption -> [ProfileOption]
enumFrom :: ProfileOption -> [ProfileOption]
$cenumFromThen :: ProfileOption -> ProfileOption -> [ProfileOption]
enumFromThen :: ProfileOption -> ProfileOption -> [ProfileOption]
$cenumFromTo :: ProfileOption -> ProfileOption -> [ProfileOption]
enumFromTo :: ProfileOption -> ProfileOption -> [ProfileOption]
$cenumFromThenTo :: ProfileOption -> ProfileOption -> ProfileOption -> [ProfileOption]
enumFromThenTo :: ProfileOption -> ProfileOption -> ProfileOption -> [ProfileOption]
Enum, ProfileOption
ProfileOption -> ProfileOption -> Bounded ProfileOption
forall a. a -> a -> Bounded a
$cminBound :: ProfileOption
minBound :: ProfileOption
$cmaxBound :: ProfileOption
maxBound :: ProfileOption
Bounded, (forall x. ProfileOption -> Rep ProfileOption x)
-> (forall x. Rep ProfileOption x -> ProfileOption)
-> Generic ProfileOption
forall x. Rep ProfileOption x -> ProfileOption
forall x. ProfileOption -> Rep ProfileOption x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ProfileOption -> Rep ProfileOption x
from :: forall x. ProfileOption -> Rep ProfileOption x
$cto :: forall x. Rep ProfileOption x -> ProfileOption
to :: forall x. Rep ProfileOption x -> ProfileOption
Generic)

instance NFData ProfileOption

-- | A set of 'ProfileOption's
newtype ProfileOptions = ProfileOpts { ProfileOptions -> Set ProfileOption
unProfileOpts :: Set ProfileOption }
  deriving (Int -> ProfileOptions -> ShowS
[ProfileOptions] -> ShowS
ProfileOptions -> [Char]
(Int -> ProfileOptions -> ShowS)
-> (ProfileOptions -> [Char])
-> ([ProfileOptions] -> ShowS)
-> Show ProfileOptions
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProfileOptions -> ShowS
showsPrec :: Int -> ProfileOptions -> ShowS
$cshow :: ProfileOptions -> [Char]
show :: ProfileOptions -> [Char]
$cshowList :: [ProfileOptions] -> ShowS
showList :: [ProfileOptions] -> ShowS
Show, ProfileOptions -> ProfileOptions -> Bool
(ProfileOptions -> ProfileOptions -> Bool)
-> (ProfileOptions -> ProfileOptions -> Bool) -> Eq ProfileOptions
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ProfileOptions -> ProfileOptions -> Bool
== :: ProfileOptions -> ProfileOptions -> Bool
$c/= :: ProfileOptions -> ProfileOptions -> Bool
/= :: ProfileOptions -> ProfileOptions -> Bool
Eq, ProfileOptions -> ()
(ProfileOptions -> ()) -> NFData ProfileOptions
forall a. (a -> ()) -> NFData a
$crnf :: ProfileOptions -> ()
rnf :: ProfileOptions -> ()
NFData, ProfileOptions
ProfileOptions -> Bool
ProfileOptions -> (ProfileOptions -> Bool) -> Null ProfileOptions
forall a. a -> (a -> Bool) -> Null a
$cempty :: ProfileOptions
empty :: ProfileOptions
$cnull :: ProfileOptions -> Bool
null :: ProfileOptions -> Bool
Null)

-- | The empty set of profiling options.
noProfileOptions :: ProfileOptions
noProfileOptions :: ProfileOptions
noProfileOptions = ProfileOptions
forall a. Null a => a
empty

addAllProfileOptions :: ProfileOptions -> ProfileOptions
addAllProfileOptions :: ProfileOptions -> ProfileOptions
addAllProfileOptions (ProfileOpts Set ProfileOption
opts) = Set ProfileOption -> ProfileOptions
ProfileOpts (Set ProfileOption -> ProfileOptions)
-> Set ProfileOption -> ProfileOptions
forall a b. (a -> b) -> a -> b
$ (Set ProfileOption -> ProfileOption -> Set ProfileOption)
-> Set ProfileOption -> [ProfileOption] -> Set ProfileOption
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Set ProfileOption -> ProfileOption -> Set ProfileOption
ins Set ProfileOption
opts [ProfileOption
forall a. Bounded a => a
minBound..ProfileOption
forall a. Bounded a => a
maxBound]
  where
    ins :: Set ProfileOption -> ProfileOption -> Set ProfileOption
ins Set ProfileOption
os ProfileOption
o | (ProfileOption -> Bool) -> Set ProfileOption -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (ProfileOption -> ProfileOption -> Bool
incompatible ProfileOption
o) Set ProfileOption
os = Set ProfileOption
os
             | Bool
otherwise               = ProfileOption -> Set ProfileOption -> Set ProfileOption
forall a. Ord a => a -> Set a -> Set a
Set.insert ProfileOption
o Set ProfileOption
os

-- | Strings accepted by 'addProfileOption'
validProfileOptionStrings :: [String]
validProfileOptionStrings :: [[Char]]
validProfileOptionStrings = [Char]
"all" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (ProfileOption -> [Char]) -> [ProfileOption] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ProfileOption -> [Char]
optName [ProfileOption
forall a. Bounded a => a
minBound .. ProfileOption
forall a. Bounded a => a
maxBound :: ProfileOption]

parseOpt :: String -> Either String ProfileOption
parseOpt :: [Char] -> Either [Char] ProfileOption
parseOpt = \ [Char]
s -> case [Char] -> Map [Char] ProfileOption -> Maybe ProfileOption
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup [Char]
s Map [Char] ProfileOption
names of
    Maybe ProfileOption
Nothing -> [Char] -> Either [Char] ProfileOption
forall a b. a -> Either a b
Left ([Char] -> Either [Char] ProfileOption)
-> [Char] -> Either [Char] ProfileOption
forall a b. (a -> b) -> a -> b
$ ShowS
err [Char]
s
    Just ProfileOption
o  -> ProfileOption -> Either [Char] ProfileOption
forall a b. b -> Either a b
Right ProfileOption
o
  where
    names :: Map [Char] ProfileOption
names = [([Char], ProfileOption)] -> Map [Char] ProfileOption
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (ProfileOption -> [Char]
optName ProfileOption
o, ProfileOption
o) | ProfileOption
o <- [ProfileOption
forall a. Bounded a => a
minBound .. ProfileOption
forall a. Bounded a => a
maxBound] ]

    close :: [Char] -> [Char] -> Bool
close [Char]
s [Char]
t = EditCosts -> [Char] -> [Char] -> Int
restrictedDamerauLevenshteinDistance EditCosts
defaultEditCosts [Char]
s [Char]
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
3
    err :: ShowS
err  [Char]
s = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
"Not a valid profiling option: '", [Char]
s, [Char]
"'. ", ShowS
hint [Char]
s]
    hint :: ShowS
hint [Char]
s = case ([Char] -> Bool) -> [[Char]] -> [[Char]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Char] -> [Char] -> Bool
close [Char]
s) (Map [Char] ProfileOption -> [[Char]]
forall k a. Map k a -> [k]
Map.keys Map [Char] ProfileOption
names) of
               [] -> [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"Valid options are ", [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ Map [Char] ProfileOption -> [[Char]]
forall k a. Map k a -> [k]
Map.keys Map [Char] ProfileOption
names, [Char]
", or all." ]
               [[Char]]
ss -> [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"Did you mean ", [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" or " [[Char]]
ss, [Char]
"?" ]

optName :: ProfileOption -> String
optName :: ProfileOption -> [Char]
optName = (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ShowS -> (ProfileOption -> [Char]) -> ProfileOption -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProfileOption -> [Char]
forall a. Show a => a -> [Char]
show

incompatible :: ProfileOption -> ProfileOption -> Bool
incompatible :: ProfileOption -> ProfileOption -> Bool
incompatible ProfileOption
o1 ProfileOption
o2
  | ProfileOption
o1 ProfileOption -> ProfileOption -> Bool
forall a. Eq a => a -> a -> Bool
== ProfileOption
o2  = Bool
False
  | Bool
otherwise = ([ProfileOption] -> Bool) -> [[ProfileOption]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ [ProfileOption]
set -> ProfileOption -> [ProfileOption] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ProfileOption
o1 [ProfileOption]
set Bool -> Bool -> Bool
&& ProfileOption -> [ProfileOption] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ProfileOption
o2 [ProfileOption]
set) [[ProfileOption]]
sets
  where
    sets :: [[ProfileOption]]
sets = [[ProfileOption
Internal, ProfileOption
Modules, ProfileOption
Definitions]]

-- | Parse and add a profiling option to a set of profiling options. Returns `Left` with a helpful
--   error message if the option doesn't parse or if it's incompatible with existing options.
--   The special string "all" adds all options compatible with the given set and prefering the first
--   of incompatible options. So `--profile=all` sets 'Internal' over 'Modules' and 'Definitions',
--   but `--profile=modules --profile=all` sets 'Modules' and not 'Internal'.
addProfileOption :: String -> ProfileOptions -> Either String ProfileOptions
addProfileOption :: [Char] -> ProfileOptions -> Either [Char] ProfileOptions
addProfileOption [Char]
"all" ProfileOptions
opts = ProfileOptions -> Either [Char] ProfileOptions
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ProfileOptions -> Either [Char] ProfileOptions)
-> ProfileOptions -> Either [Char] ProfileOptions
forall a b. (a -> b) -> a -> b
$ ProfileOptions -> ProfileOptions
addAllProfileOptions ProfileOptions
opts
addProfileOption [Char]
s (ProfileOpts Set ProfileOption
opts) = do
  o <- [Char] -> Either [Char] ProfileOption
parseOpt [Char]
s
  List1.ifNull (filter (incompatible o) $ Set.toList opts)
    {-then-}
    (return $ ProfileOpts $ Set.insert o opts)
    {-else-} $ \ List1 ProfileOption
conflicts ->
    [Char] -> Either [Char] ProfileOptions
forall a b. a -> Either a b
Left ([Char] -> Either [Char] ProfileOptions)
-> [Char] -> Either [Char] ProfileOptions
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
"Cannot use profiling option '", [Char]
s, [Char]
"' with '", ProfileOption -> [Char]
optName (ProfileOption -> [Char]) -> ProfileOption -> [Char]
forall a b. (a -> b) -> a -> b
$ List1 ProfileOption -> ProfileOption
forall a. NonEmpty a -> a
List1.head (List1 ProfileOption -> ProfileOption)
-> List1 ProfileOption -> ProfileOption
forall a b. (a -> b) -> a -> b
$ List1 ProfileOption
conflicts, [Char]
"'"]

-- | Check if a given profiling option is present in a set of profiling options.
containsProfileOption :: ProfileOption -> ProfileOptions -> Bool
containsProfileOption :: ProfileOption -> ProfileOptions -> Bool
containsProfileOption ProfileOption
o (ProfileOpts Set ProfileOption
opts) = ProfileOption -> Set ProfileOption -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ProfileOption
o Set ProfileOption
opts

-- | Use only for serialization.
profileOptionsToList :: ProfileOptions -> [ProfileOption]
profileOptionsToList :: ProfileOptions -> [ProfileOption]
profileOptionsToList (ProfileOpts Set ProfileOption
opts) = Set ProfileOption -> [ProfileOption]
forall a. Set a -> [a]
Set.toList Set ProfileOption
opts

-- | Use only for serialization.
profileOptionsFromList :: [ProfileOption] -> ProfileOptions
profileOptionsFromList :: [ProfileOption] -> ProfileOptions
profileOptionsFromList [ProfileOption]
opts = Set ProfileOption -> ProfileOptions
ProfileOpts (Set ProfileOption -> ProfileOptions)
-> Set ProfileOption -> ProfileOptions
forall a b. (a -> b) -> a -> b
$ [ProfileOption] -> Set ProfileOption
forall a. Ord a => [a] -> Set a
Set.fromList [ProfileOption]
opts