content: {-|
  Module      : Idris.Completion
  Description : Support for command-line completion at the REPL and in the prover.
  
  License     : BSD3
  Maintainer  : The Idris Community.
  -}
  
  {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
  {-# OPTIONS_GHC -fwarn-unused-imports #-}
  
  module Idris.Completion (replCompletion, proverCompletion) where
  
  import Idris.AbsSyntax (getIState, runIO)
  import Idris.AbsSyntaxTree
  import Idris.Colours
  import Idris.Core.Evaluate (ctxtAlist, visibleDefinitions)
  import Idris.Core.TT
  import Idris.Help
  import Idris.Imports (installedPackages)
  import Idris.Parser.Expr (TacticArg(..))
  import qualified Idris.Parser.Expr (constants, tactics)
  import Idris.Parser.Ops (opChars)
  import Idris.REPL.Parser (allHelp, setOptions)
  
  import Control.Monad.State.Strict
  import Data.Char (toLower)
  import Data.List
  import qualified Data.Map.Strict as Map
  import Data.Maybe
  import qualified Data.Text as T
  import System.Console.ANSI (Color)
  import System.Console.Haskeline
  
  commands :: [String]
  commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]
  
  tacticArgs :: [(String, Maybe TacticArg)]
  tacticArgs = [ (name, args) | (names, args, _) <- Idris.Parser.Expr.tactics
                              , name <- names ]
  
  tactics :: [String]
  tactics = map fst tacticArgs
  
  -- | Get the user-visible names from the current interpreter state.
  names :: Idris [String]
  names = do ctxt <- tt_ctxt <$> getIState
             return $
               mapMaybe nameString (allNames $ visibleDefinitions ctxt) ++
               "Type" : map fst Idris.Parser.Expr.constants
    where
      -- We need both fully qualified names and identifiers that map to them
      allNames :: Ctxt a -> [Name]
      allNames ctxt =
        let mappings = Map.toList ctxt
        in concatMap (\(name, mapping) -> name : Map.keys mapping) mappings
      -- Convert a name into a string usable for completion. Filters out names
      -- that users probably don't want to see.
      nameString :: Name -> Maybe String
      nameString (UN n)       = Just (str n)
      nameString (NS n ns)    =
        let path = intercalate "." . map T.unpack . reverse $ ns
        in fmap ((path ++ ".") ++) $ nameString n
      nameString _            = Nothing
  
  metavars :: Idris [String]
  metavars = do i <- get
                return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t,_)) -> not t) (idris_metavars i)) \\ primDefs
  
  namespaces :: Idris [String]
  namespaces = do
    ctxt <- fmap tt_ctxt get
    let names = map fst $ ctxtAlist ctxt
    return $ nub $ catMaybes $ map extractNS names
    where
      extractNS :: Name -> Maybe String
      extractNS (NS n ns) = Just $ intercalate "." . map T.unpack . reverse $ ns
      extractNS _ = Nothing
  
  -- UpTo means if user enters full name then no other completions are shown
  -- Full always show other (longer) completions if there are any
  data CompletionMode = UpTo | Full deriving Eq
  
  completeWithMode :: CompletionMode -> [String] -> String -> [Completion]
  completeWithMode mode ns n =
    if uniqueExists || (fullWord && mode == UpTo)
    then [simpleCompletion n]
    else map simpleCompletion prefixMatches
      where prefixMatches = filter (isPrefixOf n) ns
            uniqueExists = [n] == prefixMatches
            fullWord = n `elem` ns
  
  completeWith = completeWithMode Full
  
  completeName :: CompletionMode -> [String] -> CompletionFunc Idris
  completeName mode extra = completeWord Nothing (" \t(){}:" ++ completionWhitespace) completeName
    where
      completeName n = do
        ns <- names
        return $ completeWithMode mode (extra ++ ns) n
      -- The '.' needs not to be taken into consideration because it serves as namespace separator
      completionWhitespace = opChars \\ "."
  
  completeMetaVar :: CompletionFunc Idris
  completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
      where completeM m = do mvs <- metavars
                             return $ completeWithMode UpTo mvs m
  
  completeNamespace :: CompletionFunc Idris
  completeNamespace = completeWord Nothing " \t" completeN
    where completeN n = do ns <- namespaces
                           return $ completeWithMode UpTo ns n
  
  completeOption :: CompletionFunc Idris
  completeOption = completeWord Nothing " \t" completeOpt
      where completeOpt = return . completeWith (map fst setOptions)
  
  completeConsoleWidth :: CompletionFunc Idris
  completeConsoleWidth = completeWord Nothing " \t" completeW
      where completeW = return . completeWith ["auto", "infinite", "80", "120"]
  
  isWhitespace :: Char -> Bool
  isWhitespace = (flip elem) " \t\n"
  
  lookupInHelp :: String -> Maybe CmdArg
  lookupInHelp cmd = lookupInHelp' cmd allHelp
      where lookupInHelp' cmd ((cmds, arg, _):xs) | elem cmd cmds = Just arg
                                                  | otherwise   = lookupInHelp' cmd xs
            lookupInHelp' cmd [] = Nothing
  
  completeColour :: CompletionFunc Idris
  completeColour (prev, next) = case words (reverse prev) of
                                  [c] | isCmd c -> do cmpls <- completeColourOpt next
                                                      return (reverse $ c ++ " ", cmpls)
                                  [c, o] | o `elem` opts -> let correct = (c ++ " " ++ o) in
                                                            return (reverse correct, [simpleCompletion ""])
                                         | o `elem` colourTypes -> completeColourFormat (prev, next)
                                         | otherwise -> let cmpls = completeWith (opts ++ colourTypes) o in
                                                        let sofar = (c ++ " ") in
                                                        return (reverse sofar, cmpls)
                                  cmd@(c:o:_) | isCmd c && o `elem` colourTypes ->
                                          completeColourFormat (prev, next)
                                  _ -> noCompletion (prev, next)
      where completeColourOpt :: String -> Idris [Completion]
            completeColourOpt = return . completeWith (opts ++ colourTypes)
            opts = ["on", "off"]
            colourTypes = map (map toLower . reverse . drop 6 . reverse . show) $
                          enumFromTo (minBound::ColourType) maxBound
            isCmd ":colour" = True
            isCmd ":color"  = True
            isCmd _         = False
            colours = map (map toLower . show) $ enumFromTo (minBound::Color) maxBound
            formats = ["vivid", "dull", "underline", "nounderline", "bold", "nobold", "italic", "noitalic"]
            completeColourFormat = let getCmpl = completeWith (colours ++ formats) in
                                   completeWord Nothing " \t" (return . getCmpl)
  
  -- The FIXMEs are Issue #1768 on the issue tracker.
  --     https://github.com/idris-lang/Idris-dev/issues/1768
  -- | Get the completion function for a particular command
  completeCmd :: String -> CompletionFunc Idris
  completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
      where completeArg FileArg = completeFilename (prev, next)
            completeArg ShellCommandArg = completeFilename (prev, next)
            completeArg NameArg = completeName UpTo [] (prev, next)
            completeArg OptionArg = completeOption (prev, next)
            completeArg ModuleArg = noCompletion (prev, next)
            completeArg NamespaceArg = completeNamespace (prev, next)
            completeArg ExprArg = completeName Full [] (prev, next)
            completeArg MetaVarArg = completeMetaVar (prev, next)
            completeArg ColourArg = completeColour (prev, next)
            completeArg NoArg = noCompletion (prev, next)
            completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
            completeArg DeclArg = completeName Full [] (prev, next)
            completeArg PkgArgs = completePkg (prev, next)
            completeArg (ManyArgs a) = completeArg a
            completeArg (OptionalArg a) = completeArg a
            completeArg (SeqArgs a b) = completeArg a
            completeArg _ = noCompletion (prev, next)
            completeCmdName = return ("", completeWith commands cmd)
  
  -- | Complete REPL commands and defined identifiers
  replCompletion :: CompletionFunc Idris
  replCompletion (prev, next) = case firstWord of
                                  ':':cmdName -> completeCmd (':':cmdName) (prev, next)
                                  _           -> completeName UpTo [] (prev, next)
      where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
  
  
  completePkg :: CompletionFunc Idris
  completePkg = completeWord Nothing " \t()" completeP
      where completeP p = do pkgs <- runIO installedPackages
                             return $ completeWith pkgs p
  
  -- The TODOs are Issue #1769 on the issue tracker.
  --     https://github.com/idris-lang/Idris-dev/issues/1769
  completeTactic :: [String] -> String -> CompletionFunc Idris
  completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $
                                       lookup tac tacticArgs
      where completeTacName = return ("", completeWith tactics tac)
            completeArg Nothing              = noCompletion (prev, next)
            completeArg (Just NameTArg)      = noCompletion (prev, next) -- this is for binding new names!
            completeArg (Just ExprTArg)      = completeName Full as (prev, next)
            completeArg (Just StringLitTArg) = noCompletion (prev, next)
            completeArg (Just AltsTArg)      = noCompletion (prev, next) -- TODO
  
  -- | Complete tactics and their arguments
  proverCompletion :: [String] -- ^ The names of current local assumptions
                   -> CompletionFunc Idris
  proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
      where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
  