{-# 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
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
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
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
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
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)
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)
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
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)
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)
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 = (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