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