git.iko.soy/Idris-dev
on 63ff875 help sign in
Idris-dev/src/Idris/Completion.hs
184 lines 8.8 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.ParseHelpers(opChars)
13import qualified Idris.ParseExpr (constants, tactics)
14import Idris.ParseExpr (TacticArg (..))
15import Idris.REPLParser (allHelp)
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.ParseExpr.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.ParseExpr.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 [ "errorcontext"
86 , "showimplicits"
87 , "originalerrors"
88 , "autosolve"
89 , "nobanner"
90 , "desugarnats"
91 ]
93completeConsoleWidth :: CompletionFunc Idris
94completeConsoleWidth = completeWord Nothing " \t" completeW
95 where completeW = return . completeWith ["auto", "infinite", "80", "120"]
97isWhitespace :: Char -> Bool
98isWhitespace = (flip elem) " \t\n"
100lookupInHelp :: String -> Maybe CmdArg
101lookupInHelp cmd = lookupInHelp' cmd allHelp
102 where lookupInHelp' cmd ((cmds, arg, _):xs) | elem cmd cmds = Just arg
103 | otherwise = lookupInHelp' cmd xs
104 lookupInHelp' cmd [] = Nothing
106completeColour :: CompletionFunc Idris
107completeColour (prev, next) = case words (reverse prev) of
108 [c] | isCmd c -> do cmpls <- completeColourOpt next
109 return (reverse $ c ++ " ", cmpls)
110 [c, o] | o `elem` opts -> let correct = (c ++ " " ++ o) in
111 return (reverse correct, [simpleCompletion ""])
112 | o `elem` colourTypes -> completeColourFormat (prev, next)
113 | otherwise -> let cmpls = completeWith (opts ++ colourTypes) o in
114 let sofar = (c ++ " ") in
115 return (reverse sofar, cmpls)
116 cmd@(c:o:_) | isCmd c && o `elem` colourTypes ->
117 completeColourFormat (prev, next)
118 _ -> noCompletion (prev, next)
119 where completeColourOpt :: String -> Idris [Completion]
120 completeColourOpt = return . completeWith (opts ++ colourTypes)
121 opts = ["on", "off"]
122 colourTypes = map (map toLower . reverse . drop 6 . reverse . show) $
123 enumFromTo (minBound::ColourType) maxBound
124 isCmd ":colour" = True
125 isCmd ":color" = True
126 isCmd _ = False
127 colours = map (map toLower . show) $ enumFromTo (minBound::Color) maxBound
128 formats = ["vivid", "dull", "underline", "nounderline", "bold", "nobold", "italic", "noitalic"]
129 completeColourFormat = let getCmpl = completeWith (colours ++ formats) in
130 completeWord Nothing " \t" (return . getCmpl)
132-- The FIXMEs are Issue #1768 on the issue tracker.
133-- https://github.com/idris-lang/Idris-dev/issues/1768
134-- | Get the completion function for a particular command
135completeCmd :: String -> CompletionFunc Idris
136completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
137 where completeArg FileArg = completeFilename (prev, next)
138 completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
139 completeArg OptionArg = completeOption (prev, next)
140 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
141 completeArg NamespaceArg = noCompletion (prev, next) -- FIXME do later
142 completeArg ExprArg = completeExpr [] (prev, next)
143 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
144 completeArg ColourArg = completeColour (prev, next)
145 completeArg NoArg = noCompletion (prev, next)
146 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
147 completeArg DeclArg = completeExpr [] (prev, next)
148 completeArg PkgArgs = completePkg (prev, next)
149 completeArg (ManyArgs a) = completeArg a
150 completeArg (OptionalArg a) = completeArg a
151 completeArg (SeqArgs a b) = completeArg a
152 completeArg _ = noCompletion (prev, next)
153 completeCmdName = return $ ("", completeWith commands cmd)
155-- | Complete REPL commands and defined identifiers
156replCompletion :: CompletionFunc Idris
157replCompletion (prev, next) = case firstWord of
158 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
159 _ -> completeExpr [] (prev, next)
160 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
163completePkg :: CompletionFunc Idris
164completePkg = completeWord Nothing " \t()" completeP
165 where completeP p = do pkgs <- runIO installedPackages
166 return $ completeWith pkgs p
168-- The TODOs are Issue #1769 on the issue tracker.
169-- https://github.com/idris-lang/Idris-dev/issues/1769
170completeTactic :: [String] -> String -> CompletionFunc Idris
171completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $
172 lookup tac tacticArgs
173 where completeTacName = return $ ("", completeWith tactics tac)
174 completeArg Nothing = noCompletion (prev, next)
175 completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!
176 completeArg (Just ExprTArg) = completeExpr as (prev, next)
177 completeArg (Just StringLitTArg) = noCompletion (prev, next)
178 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
180-- | Complete tactics and their arguments
181proverCompletion :: [String] -- ^ The names of current local assumptions
182 -> CompletionFunc Idris
183proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
184 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev