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