git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/Completion.hs
209 lines 9.7 kB history raw
1{-|
2Module : Idris.Completion
3Description : Support for command-line completion at the REPL and in the prover.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8module Idris.Completion (replCompletion, proverCompletion) where
10import Idris.AbsSyntax (runIO)
11import Idris.AbsSyntaxTree
12import Idris.Colours
13import Idris.Core.Evaluate (ctxtAlist, definitions)
14import Idris.Core.TT
15import Idris.Help
16import Idris.Imports (installedPackages)
17import Idris.Parser.Expr (TacticArg(..))
18import qualified Idris.Parser.Expr (constants, tactics)
19import Idris.Parser.Helpers (opChars)
20import Idris.REPL.Parser (allHelp, setOptions)
22import Control.Monad.State.Strict
23import Data.Char (toLower)
24import Data.List
25import qualified Data.Map.Strict as Map
26import Data.Maybe
27import qualified Data.Text as T
28import System.Console.ANSI (Color)
29import System.Console.Haskeline
31commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]
33tacticArgs :: [(String, Maybe TacticArg)]
34tacticArgs = [ (name, args) | (names, args, _) <- Idris.Parser.Expr.tactics
35 , name <- names ]
36tactics = map fst tacticArgs
38-- | Get the user-visible names from the current interpreter state.
39names :: Idris [String]
40names = do i <- get
41 let ctxt = tt_ctxt i
42 return $
43 mapMaybe nameString (allNames $ definitions ctxt) ++
44 "Type" : map fst Idris.Parser.Expr.constants
45 where
46 -- We need both fully qualified names and identifiers that map to them
47 allNames :: Ctxt a -> [Name]
48 allNames ctxt =
49 let mappings = Map.toList ctxt
50 in concatMap (\(name, mapping) -> name : Map.keys mapping) mappings
51 -- Convert a name into a string usable for completion. Filters out names
52 -- that users probably don't want to see.
53 nameString :: Name -> Maybe String
54 nameString (UN n) = Just (str n)
55 nameString (NS n ns) =
56 let path = intercalate "." . map T.unpack . reverse $ ns
57 in fmap ((path ++ ".") ++) $ nameString n
58 nameString _ = Nothing
60metavars :: Idris [String]
61metavars = do i <- get
62 return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t,_)) -> not t) (idris_metavars i)) \\ primDefs
65modules :: Idris [String]
66modules = do i <- get
67 return $ map show $ imported i
69namespaces :: Idris [String]
70namespaces = do
71 ctxt <- fmap tt_ctxt get
72 let names = map fst $ ctxtAlist ctxt
73 return $ nub $ catMaybes $ map extractNS names
74 where
75 extractNS :: Name -> Maybe String
76 extractNS (NS n ns) = Just $ intercalate "." . map T.unpack . reverse $ ns
77 extractNS _ = Nothing
79-- UpTo means if user enters full name then no other completions are shown
80-- Full always show other (longer) completions if there are any
81data CompletionMode = UpTo | Full deriving Eq
83completeWithMode :: CompletionMode -> [String] -> String -> [Completion]
84completeWithMode mode ns n =
85 if uniqueExists || (fullWord && mode == UpTo)
86 then [simpleCompletion n]
87 else map simpleCompletion prefixMatches
88 where prefixMatches = filter (isPrefixOf n) ns
89 uniqueExists = [n] == prefixMatches
90 fullWord = n `elem` ns
92completeWith = completeWithMode Full
94completeName :: CompletionMode -> [String] -> CompletionFunc Idris
95completeName mode extra = completeWord Nothing (" \t(){}:" ++ completionWhitespace) completeName
96 where
97 completeName n = do
98 ns <- names
99 return $ completeWithMode mode (extra ++ ns) n
100 -- The '.' needs not to be taken into consideration because it serves as namespace separator
101 completionWhitespace = opChars \\ "."
103completeMetaVar :: CompletionFunc Idris
104completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
105 where completeM m = do mvs <- metavars
106 return $ completeWithMode UpTo mvs m
108completeNamespace :: CompletionFunc Idris
109completeNamespace = completeWord Nothing " \t" completeN
110 where completeN n = do ns <- namespaces
111 return $ completeWithMode UpTo ns n
113completeOption :: CompletionFunc Idris
114completeOption = completeWord Nothing " \t" completeOpt
115 where completeOpt = return . completeWith (map fst setOptions)
117completeConsoleWidth :: CompletionFunc Idris
118completeConsoleWidth = completeWord Nothing " \t" completeW
119 where completeW = return . completeWith ["auto", "infinite", "80", "120"]
121isWhitespace :: Char -> Bool
122isWhitespace = (flip elem) " \t\n"
124lookupInHelp :: String -> Maybe CmdArg
125lookupInHelp cmd = lookupInHelp' cmd allHelp
126 where lookupInHelp' cmd ((cmds, arg, _):xs) | elem cmd cmds = Just arg
127 | otherwise = lookupInHelp' cmd xs
128 lookupInHelp' cmd [] = Nothing
130completeColour :: CompletionFunc Idris
131completeColour (prev, next) = case words (reverse prev) of
132 [c] | isCmd c -> do cmpls <- completeColourOpt next
133 return (reverse $ c ++ " ", cmpls)
134 [c, o] | o `elem` opts -> let correct = (c ++ " " ++ o) in
135 return (reverse correct, [simpleCompletion ""])
136 | o `elem` colourTypes -> completeColourFormat (prev, next)
137 | otherwise -> let cmpls = completeWith (opts ++ colourTypes) o in
138 let sofar = (c ++ " ") in
139 return (reverse sofar, cmpls)
140 cmd@(c:o:_) | isCmd c && o `elem` colourTypes ->
141 completeColourFormat (prev, next)
142 _ -> noCompletion (prev, next)
143 where completeColourOpt :: String -> Idris [Completion]
144 completeColourOpt = return . completeWith (opts ++ colourTypes)
145 opts = ["on", "off"]
146 colourTypes = map (map toLower . reverse . drop 6 . reverse . show) $
147 enumFromTo (minBound::ColourType) maxBound
148 isCmd ":colour" = True
149 isCmd ":color" = True
150 isCmd _ = False
151 colours = map (map toLower . show) $ enumFromTo (minBound::Color) maxBound
152 formats = ["vivid", "dull", "underline", "nounderline", "bold", "nobold", "italic", "noitalic"]
153 completeColourFormat = let getCmpl = completeWith (colours ++ formats) in
154 completeWord Nothing " \t" (return . getCmpl)
156-- The FIXMEs are Issue #1768 on the issue tracker.
157-- https://github.com/idris-lang/Idris-dev/issues/1768
158-- | Get the completion function for a particular command
159completeCmd :: String -> CompletionFunc Idris
160completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
161 where completeArg FileArg = completeFilename (prev, next)
162 completeArg ShellCommandArg = completeFilename (prev, next)
163 completeArg NameArg = completeName UpTo [] (prev, next)
164 completeArg OptionArg = completeOption (prev, next)
165 completeArg ModuleArg = noCompletion (prev, next)
166 completeArg NamespaceArg = completeNamespace (prev, next)
167 completeArg ExprArg = completeName Full [] (prev, next)
168 completeArg MetaVarArg = completeMetaVar (prev, next)
169 completeArg ColourArg = completeColour (prev, next)
170 completeArg NoArg = noCompletion (prev, next)
171 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
172 completeArg DeclArg = completeName Full [] (prev, next)
173 completeArg PkgArgs = completePkg (prev, next)
174 completeArg (ManyArgs a) = completeArg a
175 completeArg (OptionalArg a) = completeArg a
176 completeArg (SeqArgs a b) = completeArg a
177 completeArg _ = noCompletion (prev, next)
178 completeCmdName = return ("", completeWith commands cmd)
180-- | Complete REPL commands and defined identifiers
181replCompletion :: CompletionFunc Idris
182replCompletion (prev, next) = case firstWord of
183 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
184 _ -> completeName UpTo [] (prev, next)
185 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
188completePkg :: CompletionFunc Idris
189completePkg = completeWord Nothing " \t()" completeP
190 where completeP p = do pkgs <- runIO installedPackages
191 return $ completeWith pkgs p
193-- The TODOs are Issue #1769 on the issue tracker.
194-- https://github.com/idris-lang/Idris-dev/issues/1769
195completeTactic :: [String] -> String -> CompletionFunc Idris
196completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $
197 lookup tac tacticArgs
198 where completeTacName = return ("", completeWith tactics tac)
199 completeArg Nothing = noCompletion (prev, next)
200 completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!
201 completeArg (Just ExprTArg) = completeName Full as (prev, next)
202 completeArg (Just StringLitTArg) = noCompletion (prev, next)
203 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
205-- | Complete tactics and their arguments
206proverCompletion :: [String] -- ^ The names of current local assumptions
207 -> CompletionFunc Idris
208proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
209 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev