git.iko.soy/Idris-dev
on dda9b49 help sign in
Idris-dev/src/Idris/Completion.hs
192 lines 8.9 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 "unify", "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 NamespaceArg = noCompletion (prev, next) -- FIXME do later
164 completeArg ExprArg = completeExpr [] (prev, next)
165 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
166 completeArg ColourArg = completeColour (prev, next)
167 completeArg NoArg = noCompletion (prev, next)
168 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
169 completeCmdName = return $ ("", completeWith commands cmd)
171-- | Complete REPL commands and defined identifiers
172replCompletion :: CompletionFunc Idris
173replCompletion (prev, next) = case firstWord of
174 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
175 _ -> completeExpr [] (prev, next)
176 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
179completeTactic :: [String] -> String -> CompletionFunc Idris
180completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $
181 lookup tac tacticArgs
182 where completeTacName = return $ ("", completeWith tactics tac)
183 completeArg Nothing = noCompletion (prev, next)
184 completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!
185 completeArg (Just ExprTArg) = completeExpr as (prev, next)
186 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
188-- | Complete tactics and their arguments
189proverCompletion :: [String] -- ^ The names of current local assumptions
190 -> CompletionFunc Idris
191proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
192 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev