git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/Completion.hs
198 lines 9.2 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.AbsSyntaxTree
8import Idris.Help
9import Idris.Colours
10import Idris.ParseHelpers(opChars)
12import Control.Monad.State.Strict
14import Data.List
15import Data.Maybe
16import Data.Char(toLower)
18import System.Console.Haskeline
19import System.Console.ANSI (Color)
22fst3 :: (a, b, c) -> a
23fst3 (a, b, c) = a
25commands = concatMap fst3 (help ++ extraHelp)
27-- | A specification of the arguments that tactics can take
28data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
29 | ExprTArg
30 | AltsTArg
32-- | A list of available tactics and their argument requirements
33tacticArgs :: [(String, Maybe TacticArg)]
34tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)
35 , ("refine", Just ExprTArg)
36 , ("mrefine", Just ExprTArg)
37 , ("rewrite", Just ExprTArg)
38 , ("let", Nothing) -- FIXME syntax for let
39 , ("focus", Just ExprTArg)
40 , ("exact", Just ExprTArg)
41 , ("equiv", Just ExprTArg)
42 , ("applyTactic", Just ExprTArg)
43 , ("byReflection", Just ExprTArg)
44 , ("reflect", Just ExprTArg)
45 , ("fill", Just ExprTArg)
46 , ("try", Just AltsTArg)
47 , ("induction", Just ExprTArg)
48 , ("case", Just ExprTArg)
49 , (":t", Just ExprTArg)
50 , (":type", Just ExprTArg)
51 , (":e", Just ExprTArg)
52 , (":eval", Just ExprTArg)
53 ] ++ map (\x -> (x, Nothing)) [
54 "intros", "compute", "trivial", "search", "solve", "attack",
55 "unify", "state", "term", "undo", "qed", "abandon", ":q"
56 ]
57tactics = map fst tacticArgs
59-- | Convert a name into a string usable for completion. Filters out names
60-- that users probably don't want to see.
61nameString :: Name -> Maybe String
62nameString (UN nm)
63 | not (tnull nm) && (thead nm == '@' || thead nm == '#') = Nothing
64nameString (UN n) = Just (str n)
65nameString (NS n _) = nameString n
66nameString _ = Nothing
68-- FIXME: Respect module imports
69-- | Get the user-visible names from the current interpreter state.
70names :: Idris [String]
71names = do i <- get
72 let ctxt = tt_ctxt i
73 return . nub $
74 mapMaybe (nameString . fst) (ctxtAlist ctxt) ++
75 -- Explicitly add primitive types, as these are special-cased in the parser
76 ["Int", "Integer", "Float", "Char", "String", "Type",
77 "Ptr", "Bits8", "Bits16", "Bits32", "Bits64",
78 "Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]
80metavars :: Idris [String]
81metavars = do i <- get
82 return . map (show . nsroot) $ map fst (filter (\(_, (_,_,t)) -> not t) (idris_metavars i)) \\ primDefs
85modules :: Idris [String]
86modules = do i <- get
87 return $ map show $ imported i
91completeWith :: [String] -> String -> [Completion]
92completeWith ns n = if uniqueExists
93 then [simpleCompletion n]
94 else map simpleCompletion prefixMatches
95 where prefixMatches = filter (isPrefixOf n) ns
96 uniqueExists = [n] == prefixMatches
98completeName :: [String] -> String -> Idris [Completion]
99completeName extra n = do ns <- names
100 return $ completeWith (extra ++ ns) n
102completeExpr :: [String] -> CompletionFunc Idris
103completeExpr extra = completeWord Nothing (" \t(){}:" ++ opChars) (completeName extra)
105completeMetaVar :: CompletionFunc Idris
106completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
107 where completeM m = do mvs <- metavars
108 return $ completeWith mvs m
110completeOption :: CompletionFunc Idris
111completeOption = completeWord Nothing " \t" completeOpt
112 where completeOpt = return . completeWith [ "errorcontext"
113 , "showimplicits"
114 , "originalerrors"
115 , "autosolve"
116 , "nobanner"
117 ]
119completeConsoleWidth :: CompletionFunc Idris
120completeConsoleWidth = completeWord Nothing " \t" completeW
121 where completeW = return . completeWith ["auto", "infinite", "80", "120"]
123isWhitespace :: Char -> Bool
124isWhitespace = (flip elem) " \t\n"
126lookupInHelp :: String -> Maybe CmdArg
127lookupInHelp cmd = lookupInHelp' cmd help
128 where lookupInHelp' cmd ((cmds, arg, _):xs) | elem cmd cmds = Just arg
129 | otherwise = lookupInHelp' cmd xs
130 lookupInHelp' cmd [] = Nothing
132completeColour :: CompletionFunc Idris
133completeColour (prev, next) = case words (reverse prev) of
134 [c] | isCmd c -> do cmpls <- completeColourOpt next
135 return (reverse $ c ++ " ", cmpls)
136 [c, o] | o `elem` opts -> let correct = (c ++ " " ++ o) in
137 return (reverse correct, [simpleCompletion ""])
138 | o `elem` colourTypes -> completeColourFormat (prev, next)
139 | otherwise -> let cmpls = completeWith (opts ++ colourTypes) o in
140 let sofar = (c ++ " ") in
141 return (reverse sofar, cmpls)
142 cmd@(c:o:_) | isCmd c && o `elem` colourTypes ->
143 completeColourFormat (prev, next)
144 _ -> noCompletion (prev, next)
145 where completeColourOpt :: String -> Idris [Completion]
146 completeColourOpt = return . completeWith (opts ++ colourTypes)
147 opts = ["on", "off"]
148 colourTypes = map (map toLower . reverse . drop 6 . reverse . show) $
149 enumFromTo (minBound::ColourType) maxBound
150 isCmd ":colour" = True
151 isCmd ":color" = True
152 isCmd _ = False
153 colours = map (map toLower . show) $ enumFromTo (minBound::Color) maxBound
154 formats = ["vivid", "dull", "underline", "nounderline", "bold", "nobold", "italic", "noitalic"]
155 completeColourFormat = let getCmpl = completeWith (colours ++ formats) in
156 completeWord Nothing " \t" (return . getCmpl)
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 NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
163 completeArg OptionArg = completeOption (prev, next)
164 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
165 completeArg NamespaceArg = noCompletion (prev, next) -- FIXME do later
166 completeArg ExprArg = completeExpr [] (prev, next)
167 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
168 completeArg ColourArg = completeColour (prev, next)
169 completeArg NoArg = noCompletion (prev, next)
170 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
171 completeArg DeclArg = completeExpr [] (prev, next)
172 completeArg (ManyArgs a) = completeArg a
173 completeArg (OptionalArg a) = completeArg a
174 completeArg (SeqArgs a b) = completeArg a
175 completeCmdName = return $ ("", completeWith commands cmd)
177-- | Complete REPL commands and defined identifiers
178replCompletion :: CompletionFunc Idris
179replCompletion (prev, next) = case firstWord of
180 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
181 _ -> completeExpr [] (prev, next)
182 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
185completeTactic :: [String] -> String -> CompletionFunc Idris
186completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $
187 lookup tac tacticArgs
188 where completeTacName = return $ ("", completeWith tactics tac)
189 completeArg Nothing = noCompletion (prev, next)
190 completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!
191 completeArg (Just ExprTArg) = completeExpr as (prev, next)
192 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
194-- | Complete tactics and their arguments
195proverCompletion :: [String] -- ^ The names of current local assumptions
196 -> CompletionFunc Idris
197proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
198 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev