{-# 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 | (names :: [String]
names, _, _) <- [([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) | (names :: [String]
names, args :: Maybe TacticArg
args, _) <- [([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 (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]
++
"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 :: Ctxt a -> [Name]
allNames ctxt :: 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
name, mapping :: 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 n :: Text
n) = String -> Maybe String
forall a. a -> Maybe a
Just (Text -> String
str Text
n)
nameString (NS n :: Name
n ns :: [Text]
ns) =
let path :: String
path = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "." ([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 (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
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 _ = 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 (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 (\(_, (_,_,_,t :: Bool
t,_)) -> 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 (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 (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 n :: Name
n ns :: [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) -> ([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 _ = 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
/= :: 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 mode :: CompletionMode
mode ns :: [String]
ns n :: 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 (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 Idris
completeName mode :: CompletionMode
mode extra :: [String]
extra = Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc Idris
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing (" \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 n :: String
n = do
[String]
ns <- Idris [String]
names
[Completion] -> StateT IState (ExceptT Err IO) [Completion]
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]
\\ "."
completeMetaVar :: CompletionFunc Idris
completeMetaVar :: CompletionFunc Idris
completeMetaVar = Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc Idris
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing (" \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 m :: String
m = do [String]
mvs <- Idris [String]
metavars
[Completion] -> StateT IState (ExceptT Err IO) [Completion]
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 Idris
completeNamespace = Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc Idris
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing " \t" String -> StateT IState (ExceptT Err IO) [Completion]
completeN
where completeN :: String -> StateT IState (ExceptT Err IO) [Completion]
completeN n :: String
n = do [String]
ns <- Idris [String]
namespaces
[Completion] -> StateT IState (ExceptT Err IO) [Completion]
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 Idris
completeOption = Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc Idris
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing " \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 (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 Idris
completeConsoleWidth = Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc Idris
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing " \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 (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 ["auto", "infinite", "80", "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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem) " \t\n"
lookupInHelp :: String -> Maybe CmdArg
lookupInHelp :: String -> Maybe CmdArg
lookupInHelp cmd :: 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' cmd :: t
cmd ((cmds :: t t
cmds, arg :: a
arg, _):xs :: [(t t, a, c)]
xs) | t -> t t -> 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' cmd :: t
cmd [] = Maybe a
forall a. Maybe a
Nothing
completeColour :: CompletionFunc Idris
completeColour :: CompletionFunc Idris
completeColour (prev :: String
prev, next :: String
next) = case String -> [String]
words (String -> String
forall a. [a] -> [a]
reverse String
prev) of
[c :: String
c] | String -> Bool
isCmd String
c -> do [Completion]
cmpls <- String -> StateT IState (ExceptT Err IO) [Completion]
completeColourOpt String
next
(String, [Completion])
-> StateT IState (ExceptT Err IO) (String, [Completion])
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]
++ " ", [Completion]
cmpls)
[c :: String
c, o :: String
o] | String
o String -> [String] -> 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
forall a. [a] -> [a] -> [a]
++ String
o) in
(String, [Completion])
-> StateT IState (ExceptT Err IO) (String, [Completion])
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> String
forall a. [a] -> [a]
reverse String
correct, [String -> Completion
simpleCompletion ""])
| String
o String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
colourTypes -> CompletionFunc Idris
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]
++ " ") in
(String, [Completion])
-> StateT IState (ExceptT Err IO) (String, [Completion])
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> String
forall a. [a] -> [a]
reverse String
sofar, [Completion]
cmpls)
cmd :: [String]
cmd@(c :: String
c:o :: String
o:_) | String -> Bool
isCmd String
c Bool -> Bool -> Bool
&& String
o String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
colourTypes ->
CompletionFunc Idris
completeColourFormat (String
prev, String
next)
_ -> CompletionFunc Idris
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 (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 = ["on", "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 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 ":colour" = Bool
True
isCmd ":color" = Bool
True
isCmd _ = 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 = ["vivid", "dull", "underline", "nounderline", "bold", "nobold", "italic", "noitalic"]
completeColourFormat :: CompletionFunc Idris
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 Idris
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing " \t" ([Completion] -> StateT IState (ExceptT Err IO) [Completion]
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 Idris
completeCmd cmd :: String
cmd (prev :: String
prev, next :: String
next) = StateT IState (ExceptT Err IO) (String, [Completion])
-> Maybe (StateT IState (ExceptT Err IO) (String, [Completion]))
-> StateT IState (ExceptT Err IO) (String, [Completion])
forall a. a -> Maybe a -> a
fromMaybe StateT IState (ExceptT Err IO) (String, [Completion])
completeCmdName (Maybe (StateT IState (ExceptT Err IO) (String, [Completion]))
-> StateT IState (ExceptT Err IO) (String, [Completion]))
-> Maybe (StateT IState (ExceptT Err IO) (String, [Completion]))
-> StateT IState (ExceptT Err IO) (String, [Completion])
forall a b. (a -> b) -> a -> b
$ (CmdArg -> StateT IState (ExceptT Err IO) (String, [Completion]))
-> Maybe CmdArg
-> Maybe (StateT IState (ExceptT Err IO) (String, [Completion]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CmdArg -> StateT IState (ExceptT Err IO) (String, [Completion])
completeArg (Maybe CmdArg
-> Maybe (StateT IState (ExceptT Err IO) (String, [Completion])))
-> Maybe CmdArg
-> Maybe (StateT IState (ExceptT Err IO) (String, [Completion]))
forall a b. (a -> b) -> a -> b
$ String -> Maybe CmdArg
lookupInHelp String
cmd
where completeArg :: CmdArg -> StateT IState (ExceptT Err IO) (String, [Completion])
completeArg FileArg = CompletionFunc Idris
forall (m :: * -> *). MonadIO m => CompletionFunc m
completeFilename (String
prev, String
next)
completeArg ShellCommandArg = CompletionFunc Idris
forall (m :: * -> *). MonadIO m => CompletionFunc m
completeFilename (String
prev, String
next)
completeArg NameArg = CompletionMode -> [String] -> CompletionFunc Idris
completeName CompletionMode
UpTo [] (String
prev, String
next)
completeArg OptionArg = CompletionFunc Idris
completeOption (String
prev, String
next)
completeArg ModuleArg = CompletionFunc Idris
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
completeArg NamespaceArg = CompletionFunc Idris
completeNamespace (String
prev, String
next)
completeArg ExprArg = CompletionMode -> [String] -> CompletionFunc Idris
completeName CompletionMode
Full [] (String
prev, String
next)
completeArg MetaVarArg = CompletionFunc Idris
completeMetaVar (String
prev, String
next)
completeArg ColourArg = CompletionFunc Idris
completeColour (String
prev, String
next)
completeArg NoArg = CompletionFunc Idris
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
completeArg ConsoleWidthArg = CompletionFunc Idris
completeConsoleWidth (String
prev, String
next)
completeArg DeclArg = CompletionMode -> [String] -> CompletionFunc Idris
completeName CompletionMode
Full [] (String
prev, String
next)
completeArg PkgArgs = CompletionFunc Idris
completePkg (String
prev, String
next)
completeArg (ManyArgs a :: CmdArg
a) = CmdArg -> StateT IState (ExceptT Err IO) (String, [Completion])
completeArg CmdArg
a
completeArg (OptionalArg a :: CmdArg
a) = CmdArg -> StateT IState (ExceptT Err IO) (String, [Completion])
completeArg CmdArg
a
completeArg (SeqArgs a :: CmdArg
a b :: CmdArg
b) = CmdArg -> StateT IState (ExceptT Err IO) (String, [Completion])
completeArg CmdArg
a
completeArg _ = CompletionFunc Idris
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
completeCmdName :: StateT IState (ExceptT Err IO) (String, [Completion])
completeCmdName = (String, [Completion])
-> StateT IState (ExceptT Err IO) (String, [Completion])
forall (m :: * -> *) a. Monad m => a -> m a
return ("", [String] -> String -> [Completion]
completeWith [String]
commands String
cmd)
replCompletion :: CompletionFunc Idris
replCompletion :: CompletionFunc Idris
replCompletion (prev :: String
prev, next :: String
next) = case String
firstWord of
':':cmdName :: String
cmdName -> String -> CompletionFunc Idris
completeCmd (':'Char -> String -> String
forall a. a -> [a] -> [a]
:String
cmdName) (String
prev, String
next)
_ -> CompletionMode -> [String] -> CompletionFunc Idris
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 Idris
completePkg = Maybe Char
-> String
-> (String -> StateT IState (ExceptT Err IO) [Completion])
-> CompletionFunc Idris
forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord Maybe Char
forall a. Maybe a
Nothing " \t()" String -> StateT IState (ExceptT Err IO) [Completion]
completeP
where completeP :: String -> StateT IState (ExceptT Err IO) [Completion]
completeP p :: 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 (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 Idris
completeTactic as :: [String]
as tac :: String
tac (prev :: String
prev, next :: String
next) = StateT IState (ExceptT Err IO) (String, [Completion])
-> Maybe (StateT IState (ExceptT Err IO) (String, [Completion]))
-> StateT IState (ExceptT Err IO) (String, [Completion])
forall a. a -> Maybe a -> a
fromMaybe StateT IState (ExceptT Err IO) (String, [Completion])
completeTacName (Maybe (StateT IState (ExceptT Err IO) (String, [Completion]))
-> StateT IState (ExceptT Err IO) (String, [Completion]))
-> (Maybe (Maybe TacticArg)
-> Maybe (StateT IState (ExceptT Err IO) (String, [Completion])))
-> Maybe (Maybe TacticArg)
-> StateT IState (ExceptT Err IO) (String, [Completion])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe TacticArg
-> StateT IState (ExceptT Err IO) (String, [Completion]))
-> Maybe (Maybe TacticArg)
-> Maybe (StateT IState (ExceptT Err IO) (String, [Completion]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe TacticArg
-> StateT IState (ExceptT Err IO) (String, [Completion])
completeArg (Maybe (Maybe TacticArg)
-> StateT IState (ExceptT Err IO) (String, [Completion]))
-> Maybe (Maybe TacticArg)
-> StateT IState (ExceptT Err IO) (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 :: StateT IState (ExceptT Err IO) (String, [Completion])
completeTacName = (String, [Completion])
-> StateT IState (ExceptT Err IO) (String, [Completion])
forall (m :: * -> *) a. Monad m => a -> m a
return ("", [String] -> String -> [Completion]
completeWith [String]
tactics String
tac)
completeArg :: Maybe TacticArg
-> StateT IState (ExceptT Err IO) (String, [Completion])
completeArg Nothing = CompletionFunc Idris
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
completeArg (Just NameTArg) = CompletionFunc Idris
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
completeArg (Just ExprTArg) = CompletionMode -> [String] -> CompletionFunc Idris
completeName CompletionMode
Full [String]
as (String
prev, String
next)
completeArg (Just StringLitTArg) = CompletionFunc Idris
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
completeArg (Just AltsTArg) = CompletionFunc Idris
forall (m :: * -> *). Monad m => CompletionFunc m
noCompletion (String
prev, String
next)
proverCompletion :: [String]
-> CompletionFunc Idris
proverCompletion :: [String] -> CompletionFunc Idris
proverCompletion assumptions :: [String]
assumptions (prev :: String
prev, next :: String
next) = [String] -> String -> CompletionFunc Idris
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