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)

-- | 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
  deriving (Int -> ProfileOption -> ShowS
[ProfileOption] -> ShowS
ProfileOption -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProfileOption] -> ShowS
$cshowList :: [ProfileOption] -> ShowS
show :: ProfileOption -> String
$cshow :: ProfileOption -> String
showsPrec :: Int -> ProfileOption -> ShowS
$cshowsPrec :: Int -> ProfileOption -> ShowS
Show, ProfileOption -> ProfileOption -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProfileOption -> ProfileOption -> Bool
$c/= :: ProfileOption -> ProfileOption -> Bool
== :: ProfileOption -> ProfileOption -> Bool
$c== :: ProfileOption -> ProfileOption -> Bool
Eq, Eq 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
min :: ProfileOption -> ProfileOption -> ProfileOption
$cmin :: ProfileOption -> ProfileOption -> ProfileOption
max :: ProfileOption -> ProfileOption -> ProfileOption
$cmax :: ProfileOption -> ProfileOption -> ProfileOption
>= :: ProfileOption -> ProfileOption -> Bool
$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
compare :: ProfileOption -> ProfileOption -> Ordering
$ccompare :: ProfileOption -> ProfileOption -> Ordering
Ord, Int -> ProfileOption
ProfileOption -> Int
ProfileOption -> [ProfileOption]
ProfileOption -> ProfileOption
ProfileOption -> ProfileOption -> [ProfileOption]
ProfileOption -> ProfileOption -> ProfileOption -> [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
enumFromThenTo :: ProfileOption -> ProfileOption -> ProfileOption -> [ProfileOption]
$cenumFromThenTo :: ProfileOption -> ProfileOption -> ProfileOption -> [ProfileOption]
enumFromTo :: ProfileOption -> ProfileOption -> [ProfileOption]
$cenumFromTo :: ProfileOption -> ProfileOption -> [ProfileOption]
enumFromThen :: ProfileOption -> ProfileOption -> [ProfileOption]
$cenumFromThen :: ProfileOption -> ProfileOption -> [ProfileOption]
enumFrom :: ProfileOption -> [ProfileOption]
$cenumFrom :: ProfileOption -> [ProfileOption]
fromEnum :: ProfileOption -> Int
$cfromEnum :: ProfileOption -> Int
toEnum :: Int -> ProfileOption
$ctoEnum :: Int -> ProfileOption
pred :: ProfileOption -> ProfileOption
$cpred :: ProfileOption -> ProfileOption
succ :: ProfileOption -> ProfileOption
$csucc :: ProfileOption -> ProfileOption
Enum, ProfileOption
forall a. a -> a -> Bounded a
maxBound :: ProfileOption
$cmaxBound :: ProfileOption
minBound :: ProfileOption
$cminBound :: ProfileOption
Bounded, 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
$cto :: forall x. Rep ProfileOption x -> ProfileOption
$cfrom :: forall x. ProfileOption -> Rep ProfileOption x
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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProfileOptions] -> ShowS
$cshowList :: [ProfileOptions] -> ShowS
show :: ProfileOptions -> String
$cshow :: ProfileOptions -> String
showsPrec :: Int -> ProfileOptions -> ShowS
$cshowsPrec :: Int -> ProfileOptions -> ShowS
Show, ProfileOptions -> ProfileOptions -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProfileOptions -> ProfileOptions -> Bool
$c/= :: ProfileOptions -> ProfileOptions -> Bool
== :: ProfileOptions -> ProfileOptions -> Bool
$c== :: ProfileOptions -> ProfileOptions -> Bool
Eq, ProfileOptions -> ()
forall a. (a -> ()) -> NFData a
rnf :: ProfileOptions -> ()
$crnf :: ProfileOptions -> ()
NFData)

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

addAllProfileOptions :: ProfileOptions -> ProfileOptions
addAllProfileOptions :: ProfileOptions -> ProfileOptions
addAllProfileOptions (ProfileOpts Set ProfileOption
opts) = Set ProfileOption -> ProfileOptions
ProfileOpts forall a b. (a -> 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 [forall a. Bounded a => a
minBound..forall a. Bounded a => a
maxBound]
  where
    ins :: Set ProfileOption -> ProfileOption -> Set ProfileOption
ins Set ProfileOption
os ProfileOption
o | 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               = 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" forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map ProfileOption -> String
optName [forall a. Bounded a => a
minBound .. forall a. Bounded a => a
maxBound :: ProfileOption]

parseOpt :: String -> Either String ProfileOption
parseOpt :: String -> Either String ProfileOption
parseOpt = \ String
s -> case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
s Map String ProfileOption
names of
    Maybe ProfileOption
Nothing -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ ShowS
err String
s
    Just ProfileOption
o  -> forall a b. b -> Either a b
Right ProfileOption
o
  where
    names :: Map String ProfileOption
names = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (ProfileOption -> String
optName ProfileOption
o, ProfileOption
o) | ProfileOption
o <- [forall a. Bounded a => a
minBound .. 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 forall a. Ord a => a -> a -> Bool
<= Int
3
    err :: ShowS
err  String
s = 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 forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
close String
s) (forall k a. Map k a -> [k]
Map.keys Map String ProfileOption
names) of
               [] -> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
"Valid options are ", forall a. [a] -> [[a]] -> [a]
intercalate String
", " forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
Map.keys Map String ProfileOption
names, String
", or all." ]
               [String]
ss -> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
"Did you mean ", forall a. [a] -> [[a]] -> [a]
intercalate String
" or " [String]
ss, String
"?" ]

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

incompatible :: ProfileOption -> ProfileOption -> Bool
incompatible :: ProfileOption -> ProfileOption -> Bool
incompatible ProfileOption
o1 ProfileOption
o2
  | ProfileOption
o1 forall a. Eq a => a -> a -> Bool
== ProfileOption
o2  = Bool
False
  | Bool
otherwise = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ [ProfileOption]
set -> forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ProfileOption
o1 [ProfileOption]
set Bool -> Bool -> 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure 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
  let conflicts :: [ProfileOption]
conflicts = forall a. (a -> Bool) -> [a] -> [a]
filter (ProfileOption -> ProfileOption -> Bool
incompatible ProfileOption
o) (forall a. Set a -> [a]
Set.toList Set ProfileOption
opts)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ProfileOption]
conflicts) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"Cannot use profiling option '", String
s, String
"' with '", ProfileOption -> String
optName forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ [ProfileOption]
conflicts, String
"'"]
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Set ProfileOption -> ProfileOptions
ProfileOpts forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
Set.insert ProfileOption
o Set ProfileOption
opts

-- | 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) = 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) = 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 forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList [ProfileOption]
opts