git.iko.soy/Idris-dev
on fd6898e help sign in
Idris-dev/src/Idris/Completion.hs
178 lines 8.5 kB history raw
1-- | Support for command-line completion at the REPL and in the prover
2module Idris.Completion (replCompletion, proverCompletion) where
4import Idris.Core.Evaluate (ctxtAlist)
5import Idris.Core.TT
7import Idris.AbsSyntax (runIO)
8import Idris.AbsSyntaxTree
9import Idris.Help
10import Idris.Imports (installedPackages)
11import Idris.Colours
12import Idris.Parser.Helpers(opChars)
13import qualified Idris.Parser.Expr (constants, tactics)
14import Idris.Parser.Expr (TacticArg (..))
15import Idris.REPL.Parser (allHelp, setOptions)
16import Control.Monad.State.Strict
18import Data.List
19import Data.Maybe
20import Data.Char(toLower)
22import System.Console.Haskeline
23import System.Console.ANSI (Color)
26commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]
28tacticArgs :: [(String, Maybe TacticArg)]
29tacticArgs = [ (name, args) | (names, args, _) <- Idris.Parser.Expr.tactics
30 , name <- names ]
31tactics = map fst tacticArgs
33-- | Convert a name into a string usable for completion. Filters out names
34-- that users probably don't want to see.
35nameString :: Name -> Maybe String
36nameString (UN nm)
37 | not (tnull nm) && (thead nm == '@' || thead nm == '#') = Nothing
38nameString (UN n) = Just (str n)
39nameString (NS n _) = nameString n
40nameString _ = Nothing
42-- FIXME: Respect module imports
43-- Issue #1767 in the issue tracker.
44-- https://github.com/idris-lang/Idris-dev/issues/1767
45-- | Get the user-visible names from the current interpreter state.
46names :: Idris [String]
47names = do i <- get
48 let ctxt = tt_ctxt i
49 return . nub $
50 mapMaybe (nameString . fst) (ctxtAlist ctxt) ++
51 "Type" : map fst Idris.Parser.Expr.constants
53metavars :: Idris [String]
54metavars = do i <- get
55 return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t,_)) -> not t) (idris_metavars i)) \\ primDefs
58modules :: Idris [String]
59modules = do i <- get
60 return $ map show $ imported i
64completeWith :: [String] -> String -> [Completion]
65completeWith ns n = if uniqueExists
66 then [simpleCompletion n]
67 else map simpleCompletion prefixMatches
68 where prefixMatches = filter (isPrefixOf n) ns
69 uniqueExists = [n] == prefixMatches
71completeName :: [String] -> String -> Idris [Completion]
72completeName extra n = do ns <- names
73 return $ completeWith (extra ++ ns) n
75completeExpr :: [String] -> CompletionFunc Idris
76completeExpr extra = completeWord Nothing (" \t(){}:" ++ opChars) (completeName extra)
78completeMetaVar :: CompletionFunc Idris
79completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
80 where completeM m = do mvs <- metavars
81 return $ completeWith mvs m
83completeOption :: CompletionFunc Idris
84completeOption = completeWord Nothing " \t" completeOpt
85 where completeOpt = return . completeWith (map fst setOptions)
87completeConsoleWidth :: CompletionFunc Idris
88completeConsoleWidth = completeWord Nothing " \t" completeW
89 where completeW = return . completeWith ["auto", "infinite", "80", "120"]
91isWhitespace :: Char -> Bool
92isWhitespace = (flip elem) " \t\n"
94lookupInHelp :: String -> Maybe CmdArg
95lookupInHelp cmd = lookupInHelp' cmd allHelp
96 where lookupInHelp' cmd ((cmds, arg, _):xs) | elem cmd cmds = Just arg
97 | otherwise = lookupInHelp' cmd xs
98 lookupInHelp' cmd [] = Nothing
100completeColour :: CompletionFunc Idris
101completeColour (prev, next) = case words (reverse prev) of
102 [c] | isCmd c -> do cmpls <- completeColourOpt next
103 return (reverse $ c ++ " ", cmpls)
104 [c, o] | o `elem` opts -> let correct = (c ++ " " ++ o) in
105 return (reverse correct, [simpleCompletion ""])
106 | o `elem` colourTypes -> completeColourFormat (prev, next)
107 | otherwise -> let cmpls = completeWith (opts ++ colourTypes) o in
108 let sofar = (c ++ " ") in
109 return (reverse sofar, cmpls)
110 cmd@(c:o:_) | isCmd c && o `elem` colourTypes ->
111 completeColourFormat (prev, next)
112 _ -> noCompletion (prev, next)
113 where completeColourOpt :: String -> Idris [Completion]
114 completeColourOpt = return . completeWith (opts ++ colourTypes)
115 opts = ["on", "off"]
116 colourTypes = map (map toLower . reverse . drop 6 . reverse . show) $
117 enumFromTo (minBound::ColourType) maxBound
118 isCmd ":colour" = True
119 isCmd ":color" = True
120 isCmd _ = False
121 colours = map (map toLower . show) $ enumFromTo (minBound::Color) maxBound
122 formats = ["vivid", "dull", "underline", "nounderline", "bold", "nobold", "italic", "noitalic"]
123 completeColourFormat = let getCmpl = completeWith (colours ++ formats) in
124 completeWord Nothing " \t" (return . getCmpl)
126-- The FIXMEs are Issue #1768 on the issue tracker.
127-- https://github.com/idris-lang/Idris-dev/issues/1768
128-- | Get the completion function for a particular command
129completeCmd :: String -> CompletionFunc Idris
130completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
131 where completeArg FileArg = completeFilename (prev, next)
132 completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
133 completeArg OptionArg = completeOption (prev, next)
134 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
135 completeArg NamespaceArg = noCompletion (prev, next) -- FIXME do later
136 completeArg ExprArg = completeExpr [] (prev, next)
137 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
138 completeArg ColourArg = completeColour (prev, next)
139 completeArg NoArg = noCompletion (prev, next)
140 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
141 completeArg DeclArg = completeExpr [] (prev, next)
142 completeArg PkgArgs = completePkg (prev, next)
143 completeArg (ManyArgs a) = completeArg a
144 completeArg (OptionalArg a) = completeArg a
145 completeArg (SeqArgs a b) = completeArg a
146 completeArg _ = noCompletion (prev, next)
147 completeCmdName = return $ ("", completeWith commands cmd)
149-- | Complete REPL commands and defined identifiers
150replCompletion :: CompletionFunc Idris
151replCompletion (prev, next) = case firstWord of
152 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
153 _ -> completeExpr [] (prev, next)
154 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
157completePkg :: CompletionFunc Idris
158completePkg = completeWord Nothing " \t()" completeP
159 where completeP p = do pkgs <- runIO installedPackages
160 return $ completeWith pkgs p
162-- The TODOs are Issue #1769 on the issue tracker.
163-- https://github.com/idris-lang/Idris-dev/issues/1769
164completeTactic :: [String] -> String -> CompletionFunc Idris
165completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $
166 lookup tac tacticArgs
167 where completeTacName = return $ ("", completeWith tactics tac)
168 completeArg Nothing = noCompletion (prev, next)
169 completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!
170 completeArg (Just ExprTArg) = completeExpr as (prev, next)
171 completeArg (Just StringLitTArg) = noCompletion (prev, next)
172 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
174-- | Complete tactics and their arguments
175proverCompletion :: [String] -- ^ The names of current local assumptions
176 -> CompletionFunc Idris
177proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
178 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev