{-|
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 :: [String]
commands = [ String
n | ([String]
names, CmdArg
_, String
_) <- [([String], CmdArg, String)]
allHelp [([String], CmdArg, String)]
-> [([String], CmdArg, String)] -> [([String], CmdArg, String)]
forall a. [a] -> [a] -> [a]
++ [([String], CmdArg, String)]
extraHelp, String
n <- [String]
names ]

tacticArgs :: [(String, Maybe TacticArg)]
tacticArgs :: [(String, Maybe TacticArg)]
tacticArgs = [ (String
name, Maybe TacticArg
args) | ([String]
names, Maybe TacticArg
args, SyntaxInfo -> IdrisParser PTactic
_) <- [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]
Idris.Parser.Expr.tactics
                            , String
name <- [String]
names ]

tactics :: [String]
tactics :: [String]
tactics = ((String, Maybe TacticArg) -> String)
-> [(String, Maybe TacticArg)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Maybe TacticArg) -> String
forall a b. (a, b) -> a
fst [(String, Maybe TacticArg)]
tacticArgs

-- | Get the user-visible names from the current interpreter state.
names :: Idris [String]
names :: Idris [String]
names = do Context
ctxt <- IState -> Context
tt_ctxt (IState -> Context)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) Context
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (ExceptT Err IO) IState
getIState
           [String] -> Idris [String]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> Idris [String]) -> [String] -> Idris [String]
forall a b. (a -> b) -> a -> b
$
             (Name -> Maybe String) -> [Name] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Name -> Maybe String
nameString (Ctxt TTDecl -> [Name]
forall a. Ctxt a -> [Name]
allNames (Ctxt TTDecl -> [Name]) -> Ctxt TTDecl -> [Name]
forall a b. (a -> b) -> a -> b
$ Context -> Ctxt TTDecl
visibleDefinitions Context
ctxt) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
             String
"Type" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ((String, Const) -> String) -> [(String, Const)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Const) -> String
forall a b. (a, b) -> a
fst [(String, Const)]
Idris.Parser.Expr.constants
  where
    -- We need both fully qualified names and identifiers that map to them
    allNames :: Ctxt a -> [Name]
    allNames :: forall a. Ctxt a -> [Name]
allNames Ctxt a
ctxt =
      let mappings :: [(Name, Map Name a)]
mappings = Ctxt a -> [(Name, Map Name a)]
forall k a. Map k a -> [(k, a)]
Map.toList Ctxt a
ctxt
      in ((Name, Map Name a) -> [Name]) -> [(Name, Map Name a)] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Name
name, Map Name a
mapping) -> Name
name Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: Map Name a -> [Name]
forall k a. Map k a -> [k]
Map.keys Map Name a
mapping) [(Name, Map Name a)]
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 :: Name -> Maybe String
nameString (UN Text
n)       = String -> Maybe String
forall a. a -> Maybe a
Just (Text -> String
str Text
n)
    nameString (NS Name
n [Text]
ns)    =
      let path :: String
path = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." ([String] -> String) -> ([Text] -> [String]) -> [Text] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack ([Text] -> [String]) -> ([Text] -> [Text]) -> [Text] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> [Text]
forall a. [a] -> [a]
reverse ([Text] -> String) -> [Text] -> String
forall a b. (a -> b) -> a -> b
$ [Text]
ns
      in (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((String
path String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".") String -> String -> String
forall a. [a] -> [a] -> [a]
++) (Maybe String -> Maybe String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Name -> Maybe String
nameString Name
n
    nameString Name
_            = Maybe String
forall a. Maybe a
Nothing

metavars :: Idris [String]
metavars :: Idris [String]
metavars = do IState
i <- StateT IState (ExceptT Err IO) IState
forall s (m :: * -> *). MonadState s m => m s
get
              [String] -> Idris [String]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> Idris [String])
-> ([Name] -> [String]) -> [Name] -> Idris [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> String
forall a. Show a => a -> String
show (Name -> String) -> (Name -> Name) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nsroot) ([Name] -> Idris [String]) -> [Name] -> Idris [String]
forall a b. (a -> b) -> a -> b
$ ((Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name)
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name
forall a b. (a, b) -> a
fst (((Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Bool)
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
_, (Maybe Name
_,Int
_,[Name]
_,Bool
t,Bool
_)) -> Bool -> Bool
not Bool
t) (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i)) [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
primDefs

namespaces :: Idris [String]
namespaces :: Idris [String]
namespaces = do
  Context
ctxt <- (IState -> Context)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) Context
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IState -> Context
tt_ctxt StateT IState (ExceptT Err IO) IState
forall s (m :: * -> *). MonadState s m => m s
get
  let names :: [Name]
names = ((Name, Def) -> Name) -> [(Name, Def)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Def) -> Name
forall a b. (a, b) -> a
fst ([(Name, Def)] -> [Name]) -> [(Name, Def)] -> [Name]
forall a b. (a -> b) -> a -> b
$ Context -> [(Name, Def)]
ctxtAlist Context
ctxt
  [String] -> Idris [String]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> Idris [String]) -> [String] -> Idris [String]
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe String] -> [String]) -> [Maybe String] -> [String]
forall a b. (a -> b) -> a -> b
$ (Name -> Maybe String) -> [Name] -> [Maybe String]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Maybe String
extractNS [Name]
names
  where
    extractNS :: Name -> Maybe String
    extractNS :: Name -> Maybe String
extractNS (NS Name
n [Text]
ns) = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." ([String] -> String) -> ([Text] -> [String]) -> [Text] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack ([Text] -> [String]) -> ([Text] -> [Text]) -> [Text] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> [Text]
forall a. [a] -> [a]
reverse ([Text] -> String) -> [Text] -> String
forall a b. (a -> b) -> a -> b
$ [Text]
ns
    extractNS Name
_ = Maybe String
forall a. Maybe a
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 CompletionMode -> CompletionMode -> Bool
(CompletionMode -> CompletionMode -> Bool)
-> (CompletionMode -> CompletionMode -> Bool) -> Eq CompletionMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CompletionMode -> CompletionMode -> Bool
== :: CompletionMode -> CompletionMode -> Bool
$c/= :: CompletionMode -> CompletionMode -> Bool
/= :: CompletionMode -> CompletionMode -> Bool
Eq

completeWithMode :: CompletionMode -> [String] -> String -> [Completion]
completeWithMode :: CompletionMode -> [String] -> String -> [Completion]
completeWithMode CompletionMode
mode [String]
ns String
n =
  if Bool
uniqueExists Bool -> Bool -> Bool
|| (Bool
fullWord Bool -> Bool -> Bool
&& CompletionMode
mode CompletionMode -> CompletionMode -> Bool
forall a. Eq a => a -> a -> Bool
== CompletionMode
UpTo)
  then [String -> Completion
simpleCompletion String
n]
  else (String -> Completion) -> [String] -> [Completion]
forall a b. (a -> b) -> [a] -> [b]
map String -> Completion
simpleCompletion [String]
prefixMatches
    where prefixMatches :: [String]
prefixMatches = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
n) [String]
ns
          uniqueExists :: Bool
uniqueExists = [String
n] [String] -> [String] -> Bool
forall a. Eq a => a -> a -> Bool
== [String]
prefixMatches
          fullWord :: Bool
fullWord = String
n String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
ns

completeWith :: [String] -> String -> [Completion]
completeWith = CompletionMode -> [String] -> String -> [Completion]
completeWithMode CompletionMode
Full

completeName :: CompletionMode -> [String] -> CompletionFunc Idris
completeName :: CompletionMode
-> [String] -> CompletionFunc (StateT IState (ExceptT Err IO))
completeName CompletionMode
mode [String]
extra = Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing (String
" \t(){}:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
completionWhitespace) String -> StateT IState (ExceptT Err IO) [Completion]
completeName
  where
    completeName :: String -> StateT IState (ExceptT Err IO) [Completion]
completeName String
n = do
      [String]
ns <- Idris [String]
names
      [Completion] -> StateT IState (ExceptT Err IO) [Completion]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Completion] -> StateT IState (ExceptT Err IO) [Completion])
-> [Completion] -> StateT IState (ExceptT Err IO) [Completion]
forall a b. (a -> b) -> a -> b
$ CompletionMode -> [String] -> String -> [Completion]
completeWithMode CompletionMode
mode ([String]
extra [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ns) String
n
    -- The '.' needs not to be taken into consideration because it serves as namespace separator
    completionWhitespace :: String
completionWhitespace = String
opChars String -> String -> String
forall a. Eq a => [a] -> [a] -> [a]
\\ String
"."

completeMetaVar :: CompletionFunc Idris
completeMetaVar :: CompletionFunc (StateT IState (ExceptT Err IO))
completeMetaVar = Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing (String
" \t(){}:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
opChars) String -> StateT IState (ExceptT Err IO) [Completion]
completeM
    where completeM :: String -> StateT IState (ExceptT Err IO) [Completion]
completeM String
m = do [String]
mvs <- Idris [String]
metavars
                           [Completion] -> StateT IState (ExceptT Err IO) [Completion]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Completion] -> StateT IState (ExceptT Err IO) [Completion])
-> [Completion] -> StateT IState (ExceptT Err IO) [Completion]
forall a b. (a -> b) -> a -> b
$ CompletionMode -> [String] -> String -> [Completion]
completeWithMode CompletionMode
UpTo [String]
mvs String
m

completeNamespace :: CompletionFunc Idris
completeNamespace :: CompletionFunc (StateT IState (ExceptT Err IO))
completeNamespace = Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing String
" \t" String -> StateT IState (ExceptT Err IO) [Completion]
completeN
  where completeN :: String -> StateT IState (ExceptT Err IO) [Completion]
completeN String
n = do [String]
ns <- Idris [String]
namespaces
                         [Completion] -> StateT IState (ExceptT Err IO) [Completion]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Completion] -> StateT IState (ExceptT Err IO) [Completion])
-> [Completion] -> StateT IState (ExceptT Err IO) [Completion]
forall a b. (a -> b) -> a -> b
$ CompletionMode -> [String] -> String -> [Completion]
completeWithMode CompletionMode
UpTo [String]
ns String
n

completeOption :: CompletionFunc Idris
completeOption :: CompletionFunc (StateT IState (ExceptT Err IO))
completeOption = Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing String
" \t" String -> StateT IState (ExceptT Err IO) [Completion]
completeOpt
    where completeOpt :: String -> StateT IState (ExceptT Err IO) [Completion]
completeOpt = [Completion] -> StateT IState (ExceptT Err IO) [Completion]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Completion] -> StateT IState (ExceptT Err IO) [Completion])
-> (String -> [Completion])
-> String
-> StateT IState (ExceptT Err IO) [Completion]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String -> [Completion]
completeWith (((String, Opt) -> String) -> [(String, Opt)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Opt) -> String
forall a b. (a, b) -> a
fst [(String, Opt)]
setOptions)

completeConsoleWidth :: CompletionFunc Idris
completeConsoleWidth :: CompletionFunc (StateT IState (ExceptT Err IO))
completeConsoleWidth = Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing String
" \t" String -> StateT IState (ExceptT Err IO) [Completion]
completeW
    where completeW :: String -> StateT IState (ExceptT Err IO) [Completion]
completeW = [Completion] -> StateT IState (ExceptT Err IO) [Completion]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Completion] -> StateT IState (ExceptT Err IO) [Completion])
-> (String -> [Completion])
-> String
-> StateT IState (ExceptT Err IO) [Completion]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String -> [Completion]
completeWith [String
"auto", String
"infinite", String
"80", String
"120"]

isWhitespace :: Char -> Bool
isWhitespace :: Char -> Bool
isWhitespace = ((Char -> String -> Bool) -> String -> Char -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem) String
" \t\n"

lookupInHelp :: String -> Maybe CmdArg
lookupInHelp :: String -> Maybe CmdArg
lookupInHelp String
cmd = String -> [([String], CmdArg, String)] -> Maybe CmdArg
forall {t :: * -> *} {t} {a} {c}.
(Foldable t, Eq t) =>
t -> [(t t, a, c)] -> Maybe a
lookupInHelp' String
cmd [([String], CmdArg, String)]
allHelp
    where lookupInHelp' :: t -> [(t t, a, c)] -> Maybe a
lookupInHelp' t
cmd ((t t
cmds, a
arg, c
_):[(t t, a, c)]
xs) | t -> t t -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem t
cmd t t
cmds = a -> Maybe a
forall a. a -> Maybe a
Just a
arg
                                                | Bool
otherwise   = t -> [(t t, a, c)] -> Maybe a
lookupInHelp' t
cmd [(t t, a, c)]
xs
          lookupInHelp' t
cmd [] = Maybe a
forall a. Maybe a
Nothing

completeColour :: CompletionFunc Idris
completeColour :: CompletionFunc (StateT IState (ExceptT Err IO))
completeColour (String
prev, String
next) = case String -> [String]
words (String -> String
forall a. [a] -> [a]
reverse String
prev) of
                                [String
c] | String -> Bool
isCmd String
c -> do [Completion]
cmpls <- String -> StateT IState (ExceptT Err IO) [Completion]
completeColourOpt String
next
                                                    (String, [Completion]) -> Idris (String, [Completion])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> String
forall a. [a] -> [a]
reverse (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ", [Completion]
cmpls)
                                [String
c, String
o] | String
o String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
opts -> let correct :: String
correct = (String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o) in
                                                          (String, [Completion]) -> Idris (String, [Completion])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> String
forall a. [a] -> [a]
reverse String
correct, [String -> Completion
simpleCompletion String
""])
                                       | String
o String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
colourTypes -> CompletionFunc (StateT IState (ExceptT Err IO))
completeColourFormat (String
prev, String
next)
                                       | Bool
otherwise -> let cmpls :: [Completion]
cmpls = [String] -> String -> [Completion]
completeWith ([String]
opts [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
colourTypes) String
o in
                                                      let sofar :: String
sofar = (String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ") in
                                                      (String, [Completion]) -> Idris (String, [Completion])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> String
forall a. [a] -> [a]
reverse String
sofar, [Completion]
cmpls)
                                cmd :: [String]
cmd@(String
c:String
o:[String]
_) | String -> Bool
isCmd String
c Bool -> Bool -> Bool
&& String
o String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
colourTypes ->
                                        CompletionFunc (StateT IState (ExceptT Err IO))
completeColourFormat (String
prev, String
next)
                                [String]
_ -> CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
    where completeColourOpt :: String -> Idris [Completion]
          completeColourOpt :: String -> StateT IState (ExceptT Err IO) [Completion]
completeColourOpt = [Completion] -> StateT IState (ExceptT Err IO) [Completion]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Completion] -> StateT IState (ExceptT Err IO) [Completion])
-> (String -> [Completion])
-> String
-> StateT IState (ExceptT Err IO) [Completion]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String -> [Completion]
completeWith ([String]
opts [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
colourTypes)
          opts :: [String]
opts = [String
"on", String
"off"]
          colourTypes :: [String]
colourTypes = (ColourType -> String) -> [ColourType] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String)
-> (ColourType -> String) -> ColourType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
reverse (String -> String)
-> (ColourType -> String) -> ColourType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> String
forall a. Int -> [a] -> [a]
drop Int
6 (String -> String)
-> (ColourType -> String) -> ColourType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
reverse (String -> String)
-> (ColourType -> String) -> ColourType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ColourType -> String
forall a. Show a => a -> String
show) ([ColourType] -> [String]) -> [ColourType] -> [String]
forall a b. (a -> b) -> a -> b
$
                        ColourType -> ColourType -> [ColourType]
forall a. Enum a => a -> a -> [a]
enumFromTo (ColourType
forall a. Bounded a => a
minBound::ColourType) ColourType
forall a. Bounded a => a
maxBound
          isCmd :: String -> Bool
isCmd String
":colour" = Bool
True
          isCmd String
":color"  = Bool
True
          isCmd String
_         = Bool
False
          colours :: [String]
colours = (Color -> String) -> [Color] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String) -> (Color -> String) -> Color -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Color -> String
forall a. Show a => a -> String
show) ([Color] -> [String]) -> [Color] -> [String]
forall a b. (a -> b) -> a -> b
$ Color -> Color -> [Color]
forall a. Enum a => a -> a -> [a]
enumFromTo (Color
forall a. Bounded a => a
minBound::Color) Color
forall a. Bounded a => a
maxBound
          formats :: [String]
formats = [String
"vivid", String
"dull", String
"underline", String
"nounderline", String
"bold", String
"nobold", String
"italic", String
"noitalic"]
          completeColourFormat :: CompletionFunc (StateT IState (ExceptT Err IO))
completeColourFormat = let getCmpl :: String -> [Completion]
getCmpl = [String] -> String -> [Completion]
completeWith ([String]
colours [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
formats) in
                                 Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing String
" \t" ([Completion] -> StateT IState (ExceptT Err IO) [Completion]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Completion] -> StateT IState (ExceptT Err IO) [Completion])
-> (String -> [Completion])
-> String
-> StateT IState (ExceptT Err IO) [Completion]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Completion]
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 :: String -> CompletionFunc (StateT IState (ExceptT Err IO))
completeCmd String
cmd (String
prev, String
next) = Idris (String, [Completion])
-> Maybe (Idris (String, [Completion]))
-> Idris (String, [Completion])
forall a. a -> Maybe a -> a
fromMaybe Idris (String, [Completion])
completeCmdName (Maybe (Idris (String, [Completion]))
 -> Idris (String, [Completion]))
-> Maybe (Idris (String, [Completion]))
-> Idris (String, [Completion])
forall a b. (a -> b) -> a -> b
$ (CmdArg -> Idris (String, [Completion]))
-> Maybe CmdArg -> Maybe (Idris (String, [Completion]))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CmdArg -> Idris (String, [Completion])
completeArg (Maybe CmdArg -> Maybe (Idris (String, [Completion])))
-> Maybe CmdArg -> Maybe (Idris (String, [Completion]))
forall a b. (a -> b) -> a -> b
$ String -> Maybe CmdArg
lookupInHelp String
cmd
    where completeArg :: CmdArg -> Idris (String, [Completion])
completeArg CmdArg
FileArg = CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *). MonadIO m => CompletionFunc m
completeFilename (String
prev, String
next)
          completeArg CmdArg
ShellCommandArg = CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *). MonadIO m => CompletionFunc m
completeFilename (String
prev, String
next)
          completeArg CmdArg
NameArg = CompletionMode
-> [String] -> CompletionFunc (StateT IState (ExceptT Err IO))
completeName CompletionMode
UpTo [] (String
prev, String
next)
          completeArg CmdArg
OptionArg = CompletionFunc (StateT IState (ExceptT Err IO))
completeOption (String
prev, String
next)
          completeArg CmdArg
ModuleArg = CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
          completeArg CmdArg
NamespaceArg = CompletionFunc (StateT IState (ExceptT Err IO))
completeNamespace (String
prev, String
next)
          completeArg CmdArg
ExprArg = CompletionMode
-> [String] -> CompletionFunc (StateT IState (ExceptT Err IO))
completeName CompletionMode
Full [] (String
prev, String
next)
          completeArg CmdArg
MetaVarArg = CompletionFunc (StateT IState (ExceptT Err IO))
completeMetaVar (String
prev, String
next)
          completeArg CmdArg
ColourArg = CompletionFunc (StateT IState (ExceptT Err IO))
completeColour (String
prev, String
next)
          completeArg CmdArg
NoArg = CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
          completeArg CmdArg
ConsoleWidthArg = CompletionFunc (StateT IState (ExceptT Err IO))
completeConsoleWidth (String
prev, String
next)
          completeArg CmdArg
DeclArg = CompletionMode
-> [String] -> CompletionFunc (StateT IState (ExceptT Err IO))
completeName CompletionMode
Full [] (String
prev, String
next)
          completeArg CmdArg
PkgArgs = CompletionFunc (StateT IState (ExceptT Err IO))
completePkg (String
prev, String
next)
          completeArg (ManyArgs CmdArg
a) = CmdArg -> Idris (String, [Completion])
completeArg CmdArg
a
          completeArg (OptionalArg CmdArg
a) = CmdArg -> Idris (String, [Completion])
completeArg CmdArg
a
          completeArg (SeqArgs CmdArg
a CmdArg
b) = CmdArg -> Idris (String, [Completion])
completeArg CmdArg
a
          completeArg CmdArg
_ = CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
          completeCmdName :: Idris (String, [Completion])
completeCmdName = (String, [Completion]) -> Idris (String, [Completion])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
"", [String] -> String -> [Completion]
completeWith [String]
commands String
cmd)

-- | Complete REPL commands and defined identifiers
replCompletion :: CompletionFunc Idris
replCompletion :: CompletionFunc (StateT IState (ExceptT Err IO))
replCompletion (String
prev, String
next) = case String
firstWord of
                                Char
':':String
cmdName -> String -> CompletionFunc (StateT IState (ExceptT Err IO))
completeCmd (Char
':'Char -> String -> String
forall a. a -> [a] -> [a]
:String
cmdName) (String
prev, String
next)
                                String
_           -> CompletionMode
-> [String] -> CompletionFunc (StateT IState (ExceptT Err IO))
completeName CompletionMode
UpTo [] (String
prev, String
next)
    where firstWord :: String
firstWord = (String, String) -> String
forall a b. (a, b) -> a
fst ((String, String) -> String) -> (String, String) -> String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isWhitespace (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isWhitespace (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
reverse String
prev


completePkg :: CompletionFunc Idris
completePkg :: CompletionFunc (StateT IState (ExceptT Err IO))
completePkg = Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing String
" \t()" String -> StateT IState (ExceptT Err IO) [Completion]
completeP
    where completeP :: String -> StateT IState (ExceptT Err IO) [Completion]
completeP String
p = do [String]
pkgs <- IO [String] -> Idris [String]
forall a. IO a -> Idris a
runIO IO [String]
installedPackages
                           [Completion] -> StateT IState (ExceptT Err IO) [Completion]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Completion] -> StateT IState (ExceptT Err IO) [Completion])
-> [Completion] -> StateT IState (ExceptT Err IO) [Completion]
forall a b. (a -> b) -> a -> b
$ [String] -> String -> [Completion]
completeWith [String]
pkgs String
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 :: [String]
-> String -> CompletionFunc (StateT IState (ExceptT Err IO))
completeTactic [String]
as String
tac (String
prev, String
next) = Idris (String, [Completion])
-> Maybe (Idris (String, [Completion]))
-> Idris (String, [Completion])
forall a. a -> Maybe a -> a
fromMaybe Idris (String, [Completion])
completeTacName (Maybe (Idris (String, [Completion]))
 -> Idris (String, [Completion]))
-> (Maybe (Maybe TacticArg)
    -> Maybe (Idris (String, [Completion])))
-> Maybe (Maybe TacticArg)
-> Idris (String, [Completion])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe TacticArg -> Idris (String, [Completion]))
-> Maybe (Maybe TacticArg) -> Maybe (Idris (String, [Completion]))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe TacticArg -> Idris (String, [Completion])
completeArg (Maybe (Maybe TacticArg) -> Idris (String, [Completion]))
-> Maybe (Maybe TacticArg) -> Idris (String, [Completion])
forall a b. (a -> b) -> a -> b
$
                                     String -> [(String, Maybe TacticArg)] -> Maybe (Maybe TacticArg)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
tac [(String, Maybe TacticArg)]
tacticArgs
    where completeTacName :: Idris (String, [Completion])
completeTacName = (String, [Completion]) -> Idris (String, [Completion])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
"", [String] -> String -> [Completion]
completeWith [String]
tactics String
tac)
          completeArg :: Maybe TacticArg -> Idris (String, [Completion])
completeArg Maybe TacticArg
Nothing              = CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
          completeArg (Just TacticArg
NameTArg)      = CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next) -- this is for binding new names!
          completeArg (Just TacticArg
ExprTArg)      = CompletionMode
-> [String] -> CompletionFunc (StateT IState (ExceptT Err IO))
completeName CompletionMode
Full [String]
as (String
prev, String
next)
          completeArg (Just TacticArg
StringLitTArg) = CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
          completeArg (Just TacticArg
AltsTArg)      = CompletionFunc (StateT IState (ExceptT Err IO))
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next) -- TODO

-- | Complete tactics and their arguments
proverCompletion :: [String] -- ^ The names of current local assumptions
                 -> CompletionFunc Idris
proverCompletion :: [String] -> CompletionFunc (StateT IState (ExceptT Err IO))
proverCompletion [String]
assumptions (String
prev, String
next) = [String]
-> String -> CompletionFunc (StateT IState (ExceptT Err IO))
completeTactic [String]
assumptions String
firstWord (String
prev, String
next)
    where firstWord :: String
firstWord = (String, String) -> String
forall a b. (a, b) -> a
fst ((String, String) -> String) -> (String, String) -> String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isWhitespace (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isWhitespace (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
reverse String
prev