git.iko.soy/Idris-dev
on d66da21 help sign in
Idris-dev/src/Idris/Completion.hs
175 lines 8.0 kB history raw
1-- | Support for command-line completion at the REPL and in the prover
2module Idris.Completion (replCompletion, proverCompletion) where
4import Core.Evaluate (ctxtAlist)
5import 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 , ("reflect", Just ExprTArg)
44 , ("fill", Just ExprTArg)
45 , ("try", Just AltsTArg)
46 ] ++ map (\x -> (x, Nothing)) [
47 "intros", "compute", "trivial", "solve", "attack",
48 "state", "term", "undo", "qed", "abandon", ":q"
49 ]
50tactics = map fst tacticArgs
52-- | Convert a name into a string usable for completion. Filters out names
53-- that users probably don't want to see.
54nameString :: Name -> Maybe String
55nameString (UN ('@':_)) = Nothing
56nameString (UN ('#':_)) = Nothing
57nameString (UN n) = Just n
58nameString (NS n _) = nameString n
59nameString _ = Nothing
61-- FIXME: Respect module imports
62-- | Get the user-visible names from the current interpreter state.
63names :: Idris [String]
64names = do i <- get
65 let ctxt = tt_ctxt i
66 return . nub $
67 mapMaybe (nameString . fst) (ctxtAlist ctxt) ++
68 -- Explicitly add primitive types, as these are special-cased in the parser
69 ["Int", "Integer", "Float", "Char", "String", "Type",
70 "Ptr", "Bits8", "Bits16", "Bits32", "Bits64",
71 "Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]
73metavars :: Idris [String]
74metavars = do i <- get
75 return . map (show . nsroot) $ map fst (filter (\(_, (_,_,t)) -> not t) (idris_metavars i)) \\ primDefs
78modules :: Idris [String]
79modules = do i <- get
80 return $ map show $ imported i
84completeWith :: [String] -> String -> [Completion]
85completeWith ns n = if uniqueExists
86 then [simpleCompletion n]
87 else map simpleCompletion prefixMatches
88 where prefixMatches = filter (isPrefixOf n) ns
89 uniqueExists = [n] == prefixMatches
91completeName :: [String] -> String -> Idris [Completion]
92completeName extra n = do ns <- names
93 return $ completeWith (extra ++ ns) n
95completeExpr :: [String] -> CompletionFunc Idris
96completeExpr extra = completeWord Nothing (" \t(){}:" ++ opChars) (completeName extra)
98completeMetaVar :: CompletionFunc Idris
99completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
100 where completeM m = do mvs <- metavars
101 return $ completeWith mvs m
103completeOption :: CompletionFunc Idris
104completeOption = completeWord Nothing " \t" completeOpt
105 where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])
107isWhitespace :: Char -> Bool
108isWhitespace = (flip elem) " \t\n"
110lookupInHelp :: String -> Maybe CmdArg
111lookupInHelp cmd = lookupInHelp' cmd help
112 where lookupInHelp' cmd ((cmds, arg, _):xs) | elem cmd cmds = Just arg
113 | otherwise = lookupInHelp' cmd xs
114 lookupInHelp' cmd [] = Nothing
116completeColour :: CompletionFunc Idris
117completeColour (prev, next) = case words (reverse prev) of
118 [c] | isCmd c -> do cmpls <- completeColourOpt next
119 return (reverse $ c ++ " ", cmpls)
120 [c, o] | o `elem` opts -> let correct = (c ++ " " ++ o) in
121 return (reverse correct, [simpleCompletion ""])
122 | o `elem` colourTypes -> completeColourFormat (prev, next)
123 | otherwise -> let cmpls = completeWith (opts ++ colourTypes) o in
124 let sofar = (c ++ " ") in
125 return (reverse sofar, cmpls)
126 cmd@(c:o:_) | isCmd c && o `elem` colourTypes ->
127 completeColourFormat (prev, next)
128 _ -> noCompletion (prev, next)
129 where completeColourOpt :: String -> Idris [Completion]
130 completeColourOpt = return . completeWith (opts ++ colourTypes)
131 opts = ["on", "off"]
132 colourTypes = map (map toLower . reverse . drop 6 . reverse . show) $
133 enumFromTo (minBound::ColourType) maxBound
134 isCmd ":colour" = True
135 isCmd ":color" = True
136 isCmd _ = False
137 colours = map (map toLower . show) $ enumFromTo (minBound::Color) maxBound
138 formats = ["vivid", "dull", "underline", "nounderline", "bold", "nobold", "italic", "noitalic"]
139 completeColourFormat = let getCmpl = completeWith (colours ++ formats) in
140 completeWord Nothing " \t" (return . getCmpl)
142-- | Get the completion function for a particular command
143completeCmd :: String -> CompletionFunc Idris
144completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
145 where completeArg FileArg = completeFilename (prev, next)
146 completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
147 completeArg OptionArg = completeOption (prev, next)
148 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
149 completeArg ExprArg = completeExpr [] (prev, next)
150 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
151 completeArg ColourArg = completeColour (prev, next)
152 completeArg NoArg = 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
163completeTactic :: [String] -> String -> CompletionFunc Idris
164completeTactic as tac (prev, next) = fromMaybe completeTacName $ fmap completeArg $ lookup tac tacticArgs
165 where completeTacName = return $ ("", completeWith tactics tac)
166 completeArg Nothing = noCompletion (prev, next)
167 completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!
168 completeArg (Just ExprTArg) = completeExpr as (prev, next)
169 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
171-- | Complete tactics and their arguments
172proverCompletion :: [String] -- ^ The names of current local assumptions
173 -> CompletionFunc Idris
174proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
175 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev