-- | Definitions and tools for arguments of command-line options.

module Agda.Interaction.Options.Arguments where

import Data.Map (Map)
import Data.Map qualified as Map

import Agda.Interaction.Options.Help (allHelpTopics)
import Agda.Interaction.Options.ProfileOptions (validProfileOptionStrings)
import Agda.Interaction.Options.Warnings (warningNameToString, warningSets)
import Agda.Setup.EmacsMode qualified as EmacsMode (setupFlag, compileFlag, locateFlag)

-- * Names of the arguments of options that have a finite enumeration.

-- | Print the possible values of an argument of the given type.
optionValues :: Map String [String]
optionValues :: Map [Char] [[Char]]
optionValues = [([Char], [[Char]])] -> Map [Char] [[Char]]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([([Char], [[Char]])] -> Map [Char] [[Char]])
-> [([Char], [[Char]])] -> Map [Char] [[Char]]
forall a b. (a -> b) -> a -> b
$
  ( [Char]
colorArg        , [[Char]]
colorValues        ) ([Char], [[Char]]) -> [([Char], [[Char]])] -> [([Char], [[Char]])]
forall a. a -> [a] -> [a]
:
  ( [Char]
emacsModeArg    , [[Char]]
emacsModeValues    ) ([Char], [[Char]]) -> [([Char], [[Char]])] -> [([Char], [[Char]])]
forall a. a -> [a] -> [a]
:
  ( [Char]
helpArg         , [[Char]]
helpValues         ) ([Char], [[Char]]) -> [([Char], [[Char]])] -> [([Char], [[Char]])]
forall a. a -> [a] -> [a]
:
  ( [Char]
profileArg      , [[Char]]
profileValues      ) ([Char], [[Char]]) -> [([Char], [[Char]])] -> [([Char], [[Char]])]
forall a. a -> [a] -> [a]
:
  ( [Char]
traceImportsArg , [[Char]]
traceImportsValues ) ([Char], [[Char]]) -> [([Char], [[Char]])] -> [([Char], [[Char]])]
forall a. a -> [a] -> [a]
:
  ( [Char]
warningArg      , [[Char]]
warningValues      ) ([Char], [[Char]]) -> [([Char], [[Char]])] -> [([Char], [[Char]])]
forall a. a -> [a] -> [a]
:
  []

-- ** @--color@

-- | Argument to @--color@.
colorArg :: String
colorArg :: [Char]
colorArg = [Char]
"COLOR_MODE"

-- | Possible values for @--color@.
colorValues :: [String]
colorValues :: [[Char]]
colorValues = [ [Char]
"always", [Char]
"auto", [Char]
"never" ]

-- ** @--emacs-mode@

-- | Argument to @--emacs-mode@.
emacsModeArg :: String
emacsModeArg :: [Char]
emacsModeArg = [Char]
"EMACS_MODE_COMMAND"

-- | Possible values for @--emacs-mode@.
emacsModeValues :: [String]
emacsModeValues :: [[Char]]
emacsModeValues = [[Char]
EmacsMode.setupFlag, [Char]
EmacsMode.compileFlag, [Char]
EmacsMode.locateFlag]

-- ** @--help@

-- | Argument to @--help@.
helpArg :: String
helpArg :: [Char]
helpArg = [Char]
"HELP_TOPIC"

-- | Possible values for @--help@.
helpValues :: [String]
helpValues :: [[Char]]
helpValues = (([Char], HelpTopic) -> [Char])
-> [([Char], HelpTopic)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], HelpTopic) -> [Char]
forall a b. (a, b) -> a
fst [([Char], HelpTopic)]
allHelpTopics

-- ** @--profile@

-- | Argument to @--profile@.
profileArg :: String
profileArg :: [Char]
profileArg = [Char]
"TO_PROFILE"

-- | Possible values for @--profile@.
profileValues :: [String]
profileValues :: [[Char]]
profileValues = [[Char]]
validProfileOptionStrings

-- ** @--trace-imports@

-- | Argument to @--trace-imports@.
traceImportsArg :: String
traceImportsArg :: [Char]
traceImportsArg = [Char]
"IMPORT_TRACING_LEVEL"

-- | Possible values for @--trace-imports@.
traceImportsValues :: [String]
traceImportsValues :: [[Char]]
traceImportsValues = [ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
n | Integer
n <- [Integer
0..Integer
3] ]

-- ** @--warning@

-- | Argument to @--warning@.
warningArg :: String
warningArg :: [Char]
warningArg = [Char]
"WARNING"

-- | Possible values for @--warning@.
warningValues :: [String]
warningValues :: [[Char]]
warningValues = [[[Char]]] -> [[Char]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[[Char]]] -> [[Char]]) -> [[[Char]]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$
  (([Char], (Set WarningName, [Char])) -> [Char])
-> [([Char], (Set WarningName, [Char]))] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], (Set WarningName, [Char])) -> [Char]
forall a b. (a, b) -> a
fst [([Char], (Set WarningName, [Char]))]
warningSets [[Char]] -> [[[Char]]] -> [[[Char]]]
forall a. a -> [a] -> [a]
:
  ([Char] -> [[Char]]) -> [[Char]] -> [[[Char]]]
forall a b. (a -> b) -> [a] -> [b]
map (\ [Char]
w -> [[Char]
w, [Char]
"no" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
w]) [[Char]]
ws
  where
    ws :: [[Char]]
ws = [Char]
"error" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (WarningName -> [Char]) -> [WarningName] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map WarningName -> [Char]
warningNameToString [WarningName
forall a. Bounded a => a
minBound..WarningName
forall a. Bounded a => a
maxBound]