{-|
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 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 = forall a b. (a -> b) -> [a] -> [b]
map 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState
           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
             forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Name -> Maybe String
nameString (forall a. Ctxt a -> [Name]
allNames forall a b. (a -> b) -> a -> b
$ Context -> Ctxt TTDecl
visibleDefinitions Context
ctxt) forall a. [a] -> [a] -> [a]
++
             String
"Type" forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map 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 = forall k a. Map k a -> [(k, a)]
Map.toList Ctxt a
ctxt
      in forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Name
name, Map Name a
mapping) -> Name
name forall a. a -> [a] -> [a]
: 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)       = forall a. a -> Maybe a
Just (Text -> String
str Text
n)
    nameString (NS Name
n [Text]
ns)    =
      let path :: String
path = forall a. [a] -> [[a]] -> [a]
intercalate String
"." forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ [Text]
ns
      in forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((String
path forall a. [a] -> [a] -> [a]
++ String
".") forall a. [a] -> [a] -> [a]
++) forall a b. (a -> b) -> a -> b
$ Name -> Maybe String
nameString Name
n
    nameString Name
_            = forall a. Maybe a
Nothing

metavars :: Idris [String]
metavars :: Idris [String]
metavars = do IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
              forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nsroot) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (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)) forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
primDefs

namespaces :: Idris [String]
namespaces :: Idris [String]
namespaces = do
  Context
ctxt <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IState -> Context
tt_ctxt forall s (m :: * -> *). MonadState s m => m s
get
  let names :: [Name]
names = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Context -> [(Name, Def)]
ctxtAlist Context
ctxt
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ 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) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [[a]] -> [a]
intercalate String
"." forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ [Text]
ns
    extractNS Name
_ = 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CompletionMode -> CompletionMode -> Bool
$c/= :: CompletionMode -> CompletionMode -> Bool
== :: CompletionMode -> CompletionMode -> Bool
$c== :: 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 forall a. Eq a => a -> a -> Bool
== CompletionMode
UpTo)
  then [String -> Completion
simpleCompletion String
n]
  else forall a b. (a -> b) -> [a] -> [b]
map String -> Completion
simpleCompletion [String]
prefixMatches
    where prefixMatches :: [String]
prefixMatches = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
n) [String]
ns
          uniqueExists :: Bool
uniqueExists = [String
n] forall a. Eq a => a -> a -> Bool
== [String]
prefixMatches
          fullWord :: Bool
fullWord = String
n 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 = forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord forall a. Maybe a
Nothing (String
" \t(){}:" 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
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CompletionMode -> [String] -> String -> [Completion]
completeWithMode CompletionMode
mode ([String]
extra 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 forall a. Eq a => [a] -> [a] -> [a]
\\ String
"."

completeMetaVar :: CompletionFunc Idris
completeMetaVar :: CompletionFunc (StateT IState (ExceptT Err IO))
completeMetaVar = forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord forall a. Maybe a
Nothing (String
" \t(){}:" 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
                           forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord 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
                         forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String -> [Completion]
completeWith (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(String, Opt)]
setOptions)

completeConsoleWidth :: CompletionFunc Idris
completeConsoleWidth :: CompletionFunc (StateT IState (ExceptT Err IO))
completeConsoleWidth = forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord 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 = forall (m :: * -> *) a. Monad m => a -> m a
return 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 = (forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 = 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) | forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem t
cmd t t
cmds = 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 [] = forall a. Maybe a
Nothing

completeColour :: CompletionFunc Idris
completeColour :: CompletionFunc (StateT IState (ExceptT Err IO))
completeColour (String
prev, String
next) = case String -> [String]
words (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
                                                    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ String
c forall a. [a] -> [a] -> [a]
++ String
" ", [Completion]
cmpls)
                                [String
c, String
o] | String
o forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
opts -> let correct :: String
correct = (String
c forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
o) in
                                                          forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
reverse String
correct, [String -> Completion
simpleCompletion String
""])
                                       | String
o 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 forall a. [a] -> [a] -> [a]
++ [String]
colourTypes) String
o in
                                                      let sofar :: String
sofar = (String
c forall a. [a] -> [a] -> [a]
++ String
" ") in
                                                      forall (m :: * -> *) a. Monad m => a -> m a
return (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 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]
_ -> 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String -> [Completion]
completeWith ([String]
opts forall a. [a] -> [a] -> [a]
++ [String]
colourTypes)
          opts :: [String]
opts = [String
"on", String
"off"]
          colourTypes :: [String]
colourTypes = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
drop Int
6 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) forall a b. (a -> b) -> a -> b
$
                        forall a. Enum a => a -> a -> [a]
enumFromTo (forall a. Bounded a => a
minBound::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 = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a -> [a]
enumFromTo (forall a. Bounded a => a
minBound::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 forall a. [a] -> [a] -> [a]
++ [String]
formats) in
                                 forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord forall a. Maybe a
Nothing String
" \t" (forall (m :: * -> *) a. Monad m => a -> m a
return 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) = forall a. a -> Maybe a -> a
fromMaybe Idris (String, [Completion])
completeCmdName forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CmdArg -> Idris (String, [Completion])
completeArg forall a b. (a -> b) -> a -> b
$ String -> Maybe CmdArg
lookupInHelp String
cmd
    where completeArg :: CmdArg -> Idris (String, [Completion])
completeArg CmdArg
FileArg = forall (m :: * -> *). MonadIO m => CompletionFunc m
completeFilename (String
prev, String
next)
          completeArg CmdArg
ShellCommandArg = 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 = 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 = 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
_ = forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
          completeCmdName :: Idris (String, [Completion])
completeCmdName = 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
':'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 = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isWhitespace forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isWhitespace forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse String
prev


completePkg :: CompletionFunc Idris
completePkg :: CompletionFunc (StateT IState (ExceptT Err IO))
completePkg = forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord 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 <- forall a. IO a -> Idris a
runIO IO [String]
installedPackages
                           forall (m :: * -> *) a. Monad m => a -> m a
return 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) = forall a. a -> Maybe a -> a
fromMaybe Idris (String, [Completion])
completeTacName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe TacticArg -> Idris (String, [Completion])
completeArg forall a b. (a -> b) -> a -> b
$
                                     forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
tac [(String, Maybe TacticArg)]
tacticArgs
    where completeTacName :: Idris (String, [Completion])
completeTacName = 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              = forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
          completeArg (Just TacticArg
NameTArg)      = 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) = forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
          completeArg (Just TacticArg
AltsTArg)      = 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 = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isWhitespace forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isWhitespace forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse String
prev