@@ -0,0 +1,143 @@
1+module Idris.Completion (replCompletion, proverCompletion) where
3+import Core.Evaluate (ctxtAlist)
6+import Idris.AbsSyntaxTree
8+import Control.Monad.State.Strict
13+import System.Console.Haskeline
15+-- TODO: add specific classes of identifiers to complete, fx metavariables
16+-- | A specification of the arguments that REPL commands can take
17+data CmdArg = ExprArg -- ^ The command takes an expression
18+ | NameArg -- ^ The command takes a name
19+ | FileArg -- ^ The command takes a file
20+ | ModuleArg -- ^ The command takes a module name
21+ | OptionArg -- ^ The command takes an option
23+-- | Information about how to complete the various commands
24+cmdArgs :: [(String, CmdArg)]
25+cmdArgs = [ (":t", ExprArg)
27+ , (":missing", NameArg)
30+ , (":total", NameArg)
33+ , (":m", ModuleArg) -- NOTE: Argumentless form is a different command
35+ , (":prove", NameArg)
37+ , (":addproof", NameArg)
38+ , (":rmproof", NameArg)
39+ , (":showproof", NameArg)
41+ , (":compile", FileArg)
43+ , (":javascript", FileArg)
44+ , (":set", OptionArg)
45+ , (":unset", OptionArg)
47+commands = map fst cmdArgs
49+-- | A specification of the arguments that tactics can take
50+data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
54+-- | A list of available tactics and their argument requirements
55+tacticArgs :: [(String, Maybe TacticArg)]
56+tacticArgs = [ ("intro", Nothing)
57+ , ("intros", Nothing)
58+ , ("refine", Just ExprTArg)
59+ , ("rewrite", Just ExprTArg)
60+ , ("let", Nothing) -- FIXME syntax for let
61+ , ("focus", Just ExprTArg)
62+ , ("exact", Just ExprTArg)
63+ , ("reflect", Just ExprTArg)
64+ , ("try", Just AltsTArg)
65+ ] ++ map (\x -> (x, Nothing)) [
66+ "intro", "intros", "compute", "trivial", "solve", "attack",
67+ "state", "term", "undo", "qed", "abandon", ":q"
69+tactics = map fst tacticArgs
71+-- | Convert a name into a string usable for completion. Filters out names
72+-- that users probably don't want to see.
73+nameString :: Name -> Maybe String
74+nameString (UN ('@':_)) = Nothing
75+nameString (UN ('#':_)) = Nothing
76+nameString (UN n) = Just n
77+nameString (NS n _) = nameString n
78+nameString _ = Nothing
80+-- FIXME: Respect module imports
81+-- | Get the user-visible names from the current interpreter state.
82+names :: Idris[String]
85+ return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
88+modules :: Idris [String]
90+ return $ map show $ imported i
94+completeWith :: [String] -> String -> [Completion]
95+completeWith ns n = if uniqueExists
96+ then [simpleCompletion n]
97+ else map simpleCompletion prefixMatches
98+ where prefixMatches = filter (isPrefixOf n) ns
99+ uniqueExists = n `elem` prefixMatches
101+completeName :: [String] -> String -> Idris [Completion]
102+completeName extra n = do ns <- names
103+ return $ completeWith (extra ++ ns) n
105+completeExpr :: [String] -> CompletionFunc Idris
106+completeExpr extra = completeWord Nothing " \t" (completeName extra)
108+completeOption :: CompletionFunc Idris
109+completeOption = completeWord Nothing " \t" completeOpt
110+ where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])
112+isWhitespace :: Char -> Bool
113+isWhitespace = (flip elem) " \t\n"
115+-- | Get the completion function for a particular command
116+completeCmd :: String -> CompletionFunc Idris
117+completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookup cmd cmdArgs
118+ where completeArg FileArg = completeFilename (prev, next)
119+ completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
120+ completeArg OptionArg = completeOption (prev, next)
121+ completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
122+ completeArg ExprArg = completeExpr [] (prev, next)
123+ completeCmdName = return $ ("", completeWith commands cmd)
125+replCompletion :: CompletionFunc Idris
126+replCompletion (prev, next) = case firstWord of
127+ ':':cmdName -> completeCmd (':':cmdName) (prev, next)
128+ _ -> completeExpr [] (prev, next)
129+ where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
132+completeTactic :: [String] -> String -> CompletionFunc Idris
133+completeTactic as tac (prev, next) = fromMaybe completeTacName $ fmap completeArg $ lookup tac tacticArgs
134+ where completeTacName = return $ ("", completeWith tactics tac)
135+ completeArg Nothing = noCompletion (prev, next)
136+ completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!
137+ completeArg (Just ExprTArg) = completeExpr as (prev, next)
138+ completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
141+proverCompletion :: [String] -> CompletionFunc Idris
142+proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
143+ where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev