    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
      o <- String -> Either String ProfileOption
    parseOpt String
    s
      List1.ifNull (filter (incompatible o) $ Set.toList opts)
        {-then-}
        (return $ ProfileOpts $ Set.insert o opts)
        {-else-} $ \ 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