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