module Agda.Utils.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
  deriving (Int -> ProfileOption -> ShowS
[ProfileOption] -> ShowS
ProfileOption -> String
(Int -> ProfileOption -> ShowS)
-> (ProfileOption -> String)
-> ([ProfileOption] -> ShowS)
-> Show ProfileOption
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProfileOption -> ShowS
showsPrec :: Int -> ProfileOption -> ShowS
$cshow :: ProfileOption -> String
show :: ProfileOption -> String
$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 -> String
(Int -> ProfileOptions -> ShowS)
-> (ProfileOptions -> String)
-> ([ProfileOptions] -> ShowS)
-> Show ProfileOptions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProfileOptions -> ShowS
showsPrec :: Int -> ProfileOptions -> ShowS
$cshow :: ProfileOptions -> String
show :: ProfileOptions -> String
$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 :: [String]
validProfileOptionStrings = String
"all" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (ProfileOption -> String) -> [ProfileOption] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ProfileOption -> String
optName [ProfileOption
forall a. Bounded a => a
minBound .. ProfileOption
forall a. Bounded a => a
maxBound :: ProfileOption]

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

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

optName :: ProfileOption -> String
optName :: ProfileOption -> String
optName = (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ShowS -> (ProfileOption -> String) -> ProfileOption -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProfileOption -> String
forall a. Show a => a -> String
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 :: String -> ProfileOptions -> Either String ProfileOptions
addProfileOption String
"all" ProfileOptions
opts = ProfileOptions -> Either String ProfileOptions
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ProfileOptions -> Either String ProfileOptions)
-> ProfileOptions -> Either String ProfileOptions
forall a b. (a -> b) -> a -> b
$ ProfileOptions -> ProfileOptions
addAllProfileOptions ProfileOptions
opts
addProfileOption String
s (ProfileOpts Set ProfileOption
opts) = do
  ProfileOption
o <- String -> Either String ProfileOption
parseOpt String
s
  [ProfileOption]
-> Either String ProfileOptions
-> (List1 ProfileOption -> Either String ProfileOptions)
-> Either String ProfileOptions
forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull ((ProfileOption -> Bool) -> [ProfileOption] -> [ProfileOption]
forall a. (a -> Bool) -> [a] -> [a]
filter (ProfileOption -> ProfileOption -> Bool
incompatible ProfileOption
o) ([ProfileOption] -> [ProfileOption])
-> [ProfileOption] -> [ProfileOption]
forall a b. (a -> b) -> a -> b
$ Set ProfileOption -> [ProfileOption]
forall a. Set a -> [a]
Set.toList Set ProfileOption
opts)
    {-then-}
    (ProfileOptions -> Either String ProfileOptions
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProfileOptions -> Either String ProfileOptions)
-> ProfileOptions -> Either String ProfileOptions
forall a b. (a -> b) -> a -> b
$ Set ProfileOption -> ProfileOptions
ProfileOpts (Set ProfileOption -> ProfileOptions)
-> Set ProfileOption -> ProfileOptions
forall a b. (a -> b) -> a -> b
$ ProfileOption -> Set ProfileOption -> Set ProfileOption
forall a. Ord a => a -> Set a -> Set a
Set.insert ProfileOption
o Set ProfileOption
opts)
    {-else-} ((List1 ProfileOption -> Either String ProfileOptions)
 -> Either String ProfileOptions)
-> (List1 ProfileOption -> Either String ProfileOptions)
-> Either String ProfileOptions
forall a b. (a -> b) -> a -> b
$ \ List1 ProfileOption
conflicts ->
    String -> Either String ProfileOptions
forall a b. a -> Either a b
Left (String -> Either String ProfileOptions)
-> String -> Either String ProfileOptions
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"Cannot use profiling option '", String
s, String
"' with '", ProfileOption -> String
optName (ProfileOption -> String) -> ProfileOption -> String
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, String
"'"]

-- | 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