git.iko.soy/Idris-dev
on dd09721 help sign in
Idris-dev/src/Idris/Completion.hs
191 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.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 NameTArg)
48 , (":t", Just ExprTArg)
49 , (":type", Just ExprTArg)
50 , (":e", Just ExprTArg)
51 , (":eval", Just ExprTArg)
52 ] ++ map (\x -> (x, Nothing)) [
53 "intros", "compute", "trivial", "search", "solve", "attack",
54 "state", "term", "undo", "qed", "abandon", ":q"
55 ]
56tactics = map fst tacticArgs
58-- | Convert a name into a string usable for completion. Filters out names
59-- that users probably don't want to see.
60nameString :: Name -> Maybe String
61nameString (UN nm)
62 | not (tnull nm) && (thead nm == '@' || thead nm == '#') = Nothing
63nameString (UN n) = Just (str n)
64nameString (NS n _) = nameString n
65nameString _ = Nothing
67-- FIXME: Respect module imports
68-- | Get the user-visible names from the current interpreter state.
69names :: Idris [String]
70names = do i <- get
71 let ctxt = tt_ctxt i
72 return . nub $
73 mapMaybe (nameString . fst) (ctxtAlist ctxt) ++
74 -- Explicitly add primitive types, as these are special-cased in the parser
75 ["Int", "Integer", "Float", "Char", "String", "Type",
76 "Ptr", "Bits8", "Bits16", "Bits32", "Bits64",
77 "Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]
79metavars :: Idris [String]
80metavars = do i <- get
81 return . map (show . nsroot) $ map fst (filter (\(_, (_,_,t)) -> not t) (idris_metavars i)) \\ primDefs
84modules :: Idris [String]
85modules = do i <- get
86 return $ map show $ imported i
90completeWith :: [String] -> String -> [Completion]
91completeWith ns n = if uniqueExists
92 then [simpleCompletion n]
93 else map simpleCompletion prefixMatches
94 where prefixMatches = filter (isPrefixOf n) ns
95 uniqueExists = [n] == prefixMatches
97completeName :: [String] -> String -> Idris [Completion]
98completeName extra n = do ns <- names
99 return $ completeWith (extra ++ ns) n
101completeExpr :: [String] -> CompletionFunc Idris
102completeExpr extra = completeWord Nothing (" \t(){}:" ++ opChars) (completeName extra)
104completeMetaVar :: CompletionFunc Idris
105completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
106 where completeM m = do mvs <- metavars
107 return $ completeWith mvs m
109completeOption :: CompletionFunc Idris
110completeOption = completeWord Nothing " \t" completeOpt
111 where completeOpt = return . completeWith [ "errorcontext"
112 , "showimplicits"
113 , "originalerrors"
114 , "autosolve"
115 ]
117completeConsoleWidth :: CompletionFunc Idris
118completeConsoleWidth = completeWord Nothing " \t" completeW
119 where completeW = return . completeWith ["auto", "infinite", "80", "120"]
121isWhitespace :: Char -> Bool
122isWhitespace = (flip elem) " \t\n"
124lookupInHelp :: String -> Maybe CmdArg
125lookupInHelp cmd = lookupInHelp' cmd help
126 where lookupInHelp' cmd ((cmds, arg, _):xs) | elem cmd cmds = Just arg
127 | otherwise = lookupInHelp' cmd xs
128 lookupInHelp' cmd [] = Nothing
130completeColour :: CompletionFunc Idris
131completeColour (prev, next) = case words (reverse prev) of
132 [c] | isCmd c -> do cmpls <- completeColourOpt next
133 return (reverse $ c ++ " ", cmpls)
134 [c, o] | o `elem` opts -> let correct = (c ++ " " ++ o) in
135 return (reverse correct, [simpleCompletion ""])
136 | o `elem` colourTypes -> completeColourFormat (prev, next)
137 | otherwise -> let cmpls = completeWith (opts ++ colourTypes) o in
138 let sofar = (c ++ " ") in
139 return (reverse sofar, cmpls)
140 cmd@(c:o:_) | isCmd c && o `elem` colourTypes ->
141 completeColourFormat (prev, next)
142 _ -> noCompletion (prev, next)
143 where completeColourOpt :: String -> Idris [Completion]
144 completeColourOpt = return . completeWith (opts ++ colourTypes)
145 opts = ["on", "off"]
146 colourTypes = map (map toLower . reverse . drop 6 . reverse . show) $
147 enumFromTo (minBound::ColourType) maxBound
148 isCmd ":colour" = True
149 isCmd ":color" = True
150 isCmd _ = False
151 colours = map (map toLower . show) $ enumFromTo (minBound::Color) maxBound
152 formats = ["vivid", "dull", "underline", "nounderline", "bold", "nobold", "italic", "noitalic"]
153 completeColourFormat = let getCmpl = completeWith (colours ++ formats) in
154 completeWord Nothing " \t" (return . getCmpl)
156-- | Get the completion function for a particular command
157completeCmd :: String -> CompletionFunc Idris
158completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
159 where completeArg FileArg = completeFilename (prev, next)
160 completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
161 completeArg OptionArg = completeOption (prev, next)
162 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
163 completeArg ExprArg = completeExpr [] (prev, next)
164 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
165 completeArg ColourArg = completeColour (prev, next)
166 completeArg NoArg = noCompletion (prev, next)
167 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
168 completeCmdName = return $ ("", completeWith commands cmd)
170-- | Complete REPL commands and defined identifiers
171replCompletion :: CompletionFunc Idris
172replCompletion (prev, next) = case firstWord of
173 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
174 _ -> completeExpr [] (prev, next)
175 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
178completeTactic :: [String] -> String -> CompletionFunc Idris
179completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $
180 lookup tac tacticArgs
181 where completeTacName = return $ ("", completeWith tactics tac)
182 completeArg Nothing = noCompletion (prev, next)
183 completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!
184 completeArg (Just ExprTArg) = completeExpr as (prev, next)
185 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
187-- | Complete tactics and their arguments
188proverCompletion :: [String] -- ^ The names of current local assumptions
189 -> CompletionFunc Idris
190proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
191 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev