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