{-# 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
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
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
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
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
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)
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)
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
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)
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)
proverCompletion :: [String]
-> 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