git.iko.soy/Idris-dev
on 173e357 help sign in
Idris-dev/src/Idris/Completion.hs
139 lines 5.6 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
11import Control.Monad.State.Strict
13import Data.List
14import Data.Maybe
16import System.Console.Haskeline
19fst3 :: (a, b, c) -> a
20fst3 (a, b, c) = a
22commands = concatMap fst3 help
24-- | A specification of the arguments that tactics can take
25data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
26 | ExprTArg
27 | AltsTArg
29-- | A list of available tactics and their argument requirements
30tacticArgs :: [(String, Maybe TacticArg)]
31tacticArgs = [ ("intro", Nothing)
32 , ("intros", Nothing)
33 , ("refine", Just ExprTArg)
34 , ("rewrite", Just ExprTArg)
35 , ("let", Nothing) -- FIXME syntax for let
36 , ("focus", Just ExprTArg)
37 , ("exact", Just ExprTArg)
38 , ("applyTactic", Just ExprTArg)
39 , ("reflect", Just ExprTArg)
40 , ("fill", Just ExprTArg)
41 , ("try", Just AltsTArg)
42 ] ++ map (\x -> (x, Nothing)) [
43 "intro", "intros", "compute", "trivial", "solve", "attack",
44 "state", "term", "undo", "qed", "abandon", ":q"
45 ]
46tactics = map fst tacticArgs
48-- | Convert a name into a string usable for completion. Filters out names
49-- that users probably don't want to see.
50nameString :: Name -> Maybe String
51nameString (UN ('@':_)) = Nothing
52nameString (UN ('#':_)) = Nothing
53nameString (UN n) = Just n
54nameString (NS n _) = nameString n
55nameString _ = Nothing
57-- FIXME: Respect module imports
58-- | Get the user-visible names from the current interpreter state.
59names :: Idris [String]
60names = do i <- get
61 let ctxt = tt_ctxt i
62 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
64metavars :: Idris [String]
65metavars = do i <- get
66 return . map (show . nsroot) $ idris_metavars i \\ primDefs
69modules :: Idris [String]
70modules = do i <- get
71 return $ map show $ imported i
75completeWith :: [String] -> String -> [Completion]
76completeWith ns n = if uniqueExists
77 then [simpleCompletion n]
78 else map simpleCompletion prefixMatches
79 where prefixMatches = filter (isPrefixOf n) ns
80 uniqueExists = [n] == prefixMatches
82completeName :: [String] -> String -> Idris [Completion]
83completeName extra n = do ns <- names
84 return $ completeWith (extra ++ ns) n
86completeExpr :: [String] -> CompletionFunc Idris
87completeExpr extra = completeWord Nothing (" \t(){}:" ++ opChars) (completeName extra)
89completeMetaVar :: CompletionFunc Idris
90completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
91 where completeM m = do mvs <- metavars
92 return $ completeWith mvs m
94completeOption :: CompletionFunc Idris
95completeOption = completeWord Nothing " \t" completeOpt
96 where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])
98isWhitespace :: Char -> Bool
99isWhitespace = (flip elem) " \t\n"
101lookupInHelp :: String -> Maybe CmdArg
102lookupInHelp cmd = lookupInHelp' cmd help
103 where lookupInHelp' cmd ((cmds, arg, _):xs) | elem cmd cmds = Just arg
104 | otherwise = lookupInHelp' cmd xs
105 lookupInHelp' cmd [] = Nothing
107-- | Get the completion function for a particular command
108completeCmd :: String -> CompletionFunc Idris
109completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
110 where completeArg FileArg = completeFilename (prev, next)
111 completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
112 completeArg OptionArg = completeOption (prev, next)
113 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
114 completeArg ExprArg = completeExpr [] (prev, next)
115 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
116 completeArg NoArg = noCompletion (prev, next)
117 completeCmdName = return $ ("", completeWith commands cmd)
119-- | Complete REPL commands and defined identifiers
120replCompletion :: CompletionFunc Idris
121replCompletion (prev, next) = case firstWord of
122 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
123 _ -> completeExpr [] (prev, next)
124 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
127completeTactic :: [String] -> String -> CompletionFunc Idris
128completeTactic as tac (prev, next) = fromMaybe completeTacName $ fmap completeArg $ lookup tac tacticArgs
129 where completeTacName = return $ ("", completeWith tactics tac)
130 completeArg Nothing = noCompletion (prev, next)
131 completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!
132 completeArg (Just ExprTArg) = completeExpr as (prev, next)
133 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
135-- | Complete tactics and their arguments
136proverCompletion :: [String] -- ^ The names of current local assumptions
137 -> CompletionFunc Idris
138proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
139 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev