{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wunused-matches #-}
{-# OPTIONS_GHC -Wunused-binds   #-}

-- | Tools for shell completion scripts.
--
-- Bash completion takes a list of completion words (the current commandline)
-- and a completion index (the current word to be completed) and returns
-- a list of possible completions of this word.
--
-- To do bash completion /inside/ Agda, we need to pass this data to Agda.
-- So we equip Agda with a special option @--bash-completion@ which takes
-- first the completion index (number) and then the completion words.
-- E.g.
--
-- @
--    agda --bash-completion 1 --warn
-- @
--
-- This should complete @--warn@ to @--warning=@.
--
-- @
--    agda --bash-completion 1 --warning=
-- @
--
-- This would list the possible values for WARNING.
-- However, these are too many and one may get the annoying question
-- whether one really wants to see all.
-- So we should only produce a small enough list.
-- We show the common prefixes of all values up to a maximal number (threshold).
-- To this end, we may store the possible completion as a compressed trie
-- where instead of letters we use maximal non-overlapping prefixes.
-- Then we compute a fair truncation of the tree so that the
-- total number of leaves stay below the threshold.

module Agda.Interaction.Options.BashCompletion where

import Prelude hiding (null)

import Data.Bifunctor ( first )
import Data.Map       qualified as Map
import Data.Maybe
import Text.Read      ( readMaybe )

import Agda.Interaction.Options.Arguments      ( optionValues )
import Agda.Interaction.Options.Base           ( standardOptions )

import Agda.Utils.Function       ( applyWhenJust )
import Agda.Utils.GetOpt         ( OptDescr(..), ArgDescr(..) )
import Agda.Utils.List           ( (!!!) )
import Agda.Utils.List1          qualified as List1
import Agda.Utils.Null
import Agda.Utils.Trie           (Trie)
import Agda.Utils.Trie           qualified as Trie
import Agda.Utils.CompressedTrie qualified as CompressedTrie

type Help = String

printedOptions :: [String]
printedOptions :: [Help]
printedOptions = ((Help, Help) -> Help) -> [(Help, Help)] -> [Help]
forall a b. (a -> b) -> [a] -> [b]
map (Help, Help) -> Help
forall a b. (a, b) -> a
fst [(Help, Help)]
printedOptionsWithHelp

printedOptionsWithHelp :: [(String, Help)]
printedOptionsWithHelp :: [(Help, Help)]
printedOptionsWithHelp = [OptDescr (Flag CommandLineOptions)] -> [(Help, Help)]
forall a. [OptDescr a] -> [(Help, Help)]
printOptions [OptDescr (Flag CommandLineOptions)]
standardOptions

-- | Print just the names of the given options (e.g. for bash completion scripts).
--   For long options with finitely enumerable arguments, print all variants.
printOptions :: [OptDescr a] -> [(String, Help)]
printOptions :: forall a. [OptDescr a] -> [(Help, Help)]
printOptions = [[(Help, Help)]] -> [(Help, Help)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Help, Help)]] -> [(Help, Help)])
-> ([OptDescr a] -> [[(Help, Help)]])
-> [OptDescr a]
-> [(Help, Help)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OptDescr a -> [(Help, Help)]) -> [OptDescr a] -> [[(Help, Help)]]
forall a b. (a -> b) -> [a] -> [b]
map \case
  Option Help
short [Help]
long ArgDescr a
arg Help
help -> [[(Help, Help)]] -> [(Help, Help)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Help, Help)]] -> [(Help, Help)])
-> [[(Help, Help)]] -> [(Help, Help)]
forall a b. (a -> b) -> a -> b
$
    (Help -> (Help, Help)) -> [Help] -> [(Help, Help)]
forall a b. (a -> b) -> [a] -> [b]
map (,Help
help) [Help]
ss [(Help, Help)] -> [[(Help, Help)]] -> [[(Help, Help)]]
forall a. a -> [a] -> [a]
:
    (Help -> (Help, Help)) -> [Help] -> [(Help, Help)]
forall a b. (a -> b) -> [a] -> [b]
map (,Help
help) [Help]
ls [(Help, Help)] -> [[(Help, Help)]] -> [[(Help, Help)]]
forall a. a -> [a] -> [a]
:
    ([Help] -> [(Help, Help)]) -> [[Help]] -> [[(Help, Help)]]
forall a b. (a -> b) -> [a] -> [b]
map ((Help -> (Help, Help)) -> [Help] -> [(Help, Help)]
forall a b. (a -> b) -> [a] -> [b]
map (,Help
noHelp))
    [ [ Help
s        Help -> Help -> Help
forall a. [a] -> [a] -> [a]
++ Help
a | Help
s <- [Help]
ss ] [Help] -> [Help] -> [Help]
forall a. [a] -> [a] -> [a]
++
      [ Help
l Help -> Help -> Help
forall a. [a] -> [a] -> [a]
++ Help
"=" Help -> Help -> Help
forall a. [a] -> [a] -> [a]
++ Help
a | Help
l <- [Help]
ls ]
    | Help
a <- [Help]
as
    ]
    where
      ss :: [String]
      ss :: [Help]
ss = [ Char
'-' Char -> Help -> Help
forall a. a -> [a] -> [a]
: Char
s Char -> Help -> Help
forall a. a -> [a] -> [a]
: Help
"" | Char
s <- Help
short ]
      ls :: [String]
      ls :: [Help]
ls = [ Help
"--" Help -> Help -> Help
forall a. [a] -> [a] -> [a]
++ Help
l | Help
l <- [Help]
long ]
      as :: [String]
      as :: [Help]
as = [Help] -> Maybe [Help] -> [Help]
forall a. a -> Maybe a -> a
fromMaybe [] do
        t <- Maybe Help
argType
        Map.lookup t optionValues
      argType :: Maybe String
      argType :: Maybe Help
argType = case ArgDescr a
arg of
        NoArg{}     -> Maybe Help
forall a. Maybe a
Nothing
        ReqArg Help -> a
_ Help
t -> Help -> Maybe Help
forall a. a -> Maybe a
Just Help
t
        OptArg Maybe Help -> a
_ Help
t -> Help -> Maybe Help
forall a. a -> Maybe a
Just Help
t
      noHelp :: Help
      noHelp :: Help
noHelp = Help
""

-- | Should the 'completions' be truncated to a given maximum number of prefixes?
type Truncate = Maybe Int

-- | Handle the option @--bash-complete@.
--   It expects the index @COMP_CWORD@ as first argument
--   that tells which of the following arguments @COMP_WORDS@
--   is supposed to be completed.
--
--   It either returns an error message or the result for @COMPREPLY@.
--
bashComplete ::
     Truncate
       -- ^ Truncate completions suggestions?  To how many?
  -> [String]
       -- ^ Arguments following @--bash-complete@.
  -> Either String String
       -- ^ Error or @COMPREPLY@.
bashComplete :: Truncate -> [Help] -> Either Help Help
bashComplete Truncate
tr = \case
  Help
cword : [Help]
words
    | Just Int
i <- Help -> Truncate
forall a. Read a => Help -> Maybe a
readMaybe Help
cword
    , [Help] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Help]
words Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i
    , Just Help
w <- [Help]
words [Help] -> Int -> Maybe Help
forall a. [a] -> Int -> Maybe a
!!! Int
i
    -> case Truncate -> Help -> Completion
complete Truncate
tr Help
w of
        Completion (Just Help
s) [(Help, Help)]
_ -> Help -> Either Help Help
forall a. a -> Either Help a
forall (m :: * -> *) a. Monad m => a -> m a
return Help
s
        Completion Maybe Help
ms [(Help, Help)]
cs ->
          Help -> Either Help Help
forall a. a -> Either Help a
forall (m :: * -> *) a. Monad m => a -> m a
return (Help -> Either Help Help) -> Help -> Either Help Help
forall a b. (a -> b) -> a -> b
$ [Help] -> Help
unlines ([Help] -> Help) -> [Help] -> Help
forall a b. (a -> b) -> a -> b
$ [[Help]] -> [Help]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ Maybe Help -> [Help]
forall a. Maybe a -> [a]
maybeToList Maybe Help
ms
            , ((Help, Help) -> Help) -> [(Help, Help)] -> [Help]
forall a b. (a -> b) -> [a] -> [b]
map (Help, Help) -> Help
forall a b. (a, b) -> a
fst [(Help, Help)]
cs
            ]
  [Help]
_args -> Help -> Either Help Help
forall a b. a -> Either a b
Left Help
"Error: Wrong invokation of --bash-complete"

-- | The result of an invokation of (bash) completion.
data Completion = Completion
  { Completion -> Maybe Help
extended :: Maybe String
      -- ^ If 'Nothing', then the completion word cannot become a valid option ever.
  , Completion -> [(Help, Help)]
completions :: [(String, Help)]
      -- ^ If 'null', the 'extended' word cannot be further completed.
  }

-- | Cached trie of options.
optionsTrie :: Trie Char Help
optionsTrie :: Trie Char Help
optionsTrie = [(Help, Help)] -> Trie Char Help
forall k v. Ord k => [([k], v)] -> Trie k v
Trie.fromList [(Help, Help)]
printedOptionsWithHelp

-- | Complete the given word as an option.
complete :: Truncate -> String -> Completion
complete :: Truncate -> Help -> Completion
complete Truncate
trunc Help
s
  -- No completion possible?
  | Trie Char Help -> Bool
forall a. Null a => a -> Bool
null Trie Char Help
t =
      Maybe Help -> [(Help, Help)] -> Completion
Completion Maybe Help
forall a. Maybe a
Nothing []
  -- Unambiguously (partially) complete by at least one letter.
  | Just (List1 Char
k, Trie Char Help
_t') <- Trie Char Help -> Maybe (List1 Char, Trie Char Help)
forall k v. Trie k v -> Maybe (List1 k, Trie k v)
CompressedTrie.isSingleBranch Trie Char Help
t =
      Maybe Help -> [(Help, Help)] -> Completion
Completion (Help -> Maybe Help
forall a. a -> Maybe a
Just (Help -> Maybe Help) -> Help -> Maybe Help
forall a b. (a -> b) -> a -> b
$ Help
s Help -> Help -> Help
forall a. [a] -> [a] -> [a]
++ List1 Char -> [Item (List1 Char)]
forall l. IsList l => l -> [Item l]
List1.toList List1 Char
k) [(Help, Help)]
compls
  -- No unambiguous completion possible: just return suggestions.
  | Bool
otherwise =
      Maybe Help -> [(Help, Help)] -> Completion
Completion Maybe Help
forall a. Maybe a
Nothing [(Help, Help)]
compls
  where
    -- The possible suffixes.
    t :: Trie Char Help
t = Trie Char Help -> Trie Char Help
forall k v. Ord k => Trie k v -> Trie k v
CompressedTrie.compress (Trie Char Help -> Trie Char Help)
-> Trie Char Help -> Trie Char Help
forall a b. (a -> b) -> a -> b
$ Help -> Trie Char Help -> Trie Char Help
forall k v. Ord k => [k] -> Trie k v -> Trie k v
Trie.delete [] (Trie Char Help -> Trie Char Help)
-> Trie Char Help -> Trie Char Help
forall a b. (a -> b) -> a -> b
$ Help -> Trie Char Help -> Trie Char Help
forall k v. Ord k => [k] -> Trie k v -> Trie k v
Trie.lookupTrie Help
s Trie Char Help
optionsTrie
    -- The possibly truncated list of completions.
    compls :: [(Help, Help)]
compls = ((Help, Help) -> (Help, Help)) -> [(Help, Help)] -> [(Help, Help)]
forall a b. (a -> b) -> [a] -> [b]
map ((Help -> Help) -> (Help, Help) -> (Help, Help)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Help
s Help -> Help -> Help
forall a. [a] -> [a] -> [a]
++)) ([(Help, Help)] -> [(Help, Help)])
-> [(Help, Help)] -> [(Help, Help)]
forall a b. (a -> b) -> a -> b
$ Trie Char Help -> [(Help, Help)]
forall k v. Ord k => Trie k v -> [([k], v)]
CompressedTrie.toList (Trie Char Help -> [(Help, Help)])
-> Trie Char Help -> [(Help, Help)]
forall a b. (a -> b) -> a -> b
$ (Maybe Help -> Trie Char Help) -> Trie Char Help -> Trie Char Help
forall v k. (Maybe v -> Trie k v) -> Trie k v -> Trie k v
CompressedTrie.substLeaves Maybe Help -> Trie Char Help
f Trie Char Help
tt
      where
        -- t truncated.
        tt :: Trie Char Help
tt = Truncate
-> (Int -> Trie Char Help -> Trie Char Help)
-> Trie Char Help
-> Trie Char Help
forall b a. Maybe b -> (b -> a -> a) -> a -> a
applyWhenJust Truncate
trunc Int -> Trie Char Help -> Trie Char Help
forall k v. Int -> Trie k v -> Trie k v
CompressedTrie.truncateSizeWithLeaves Trie Char Help
t
        -- Replace empty leaves by "..." branches.
        f :: Maybe Help -> Trie Char Help
f = Trie Char Help
-> (Help -> Trie Char Help) -> Maybe Help -> Trie Char Help
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Help -> Help -> Trie Char Help
forall k v. [k] -> v -> Trie k v
CompressedTrie.singleton Help
"..." Help
forall a. Null a => a
empty) Help -> Trie Char Help
forall v k. v -> Trie k v
CompressedTrie.root