@@ -3,6 +3,7 @@ module Idris.Completion (replCompletion, proverCompletion) where
33
44import Core.Evaluate (ctxtAlist)
55import Core.TT
6+import Core.CoreParser (opChars)
67
78import Idris.AbsSyntaxTree
89
@@ -20,6 +21,7 @@ data CmdArg = ExprArg -- ^ The command takes an expression
2021 | FileArg -- ^ The command takes a file
2122 | ModuleArg -- ^ The command takes a module name
2223 | OptionArg -- ^ The command takes an option
24+ | MetaVarArg -- ^ The command takes a metavariable
2325
2426-- | Information about how to complete the various commands
2527cmdArgs :: [(String, CmdArg)]
@@ -32,8 +34,8 @@ cmdArgs = [ (":t", ExprArg)
3234 , (":l", FileArg)
3335 , (":load", FileArg)
3436 , (":m", ModuleArg) -- NOTE: Argumentless form is a different command
35− , (":p", NameArg)
36− , (":prove", NameArg)
37+ , (":p", MetaVarArg)
38+ , (":prove", MetaVarArg)
3739 , (":a", NameArg)
3840 , (":addproof", NameArg)
3941 , (":rmproof", NameArg)
@@ -80,11 +82,15 @@ nameString _ = Nothing
8082
8183-- FIXME: Respect module imports
8284-- | Get the user-visible names from the current interpreter state.
83−names :: Idris[String]
85+names :: Idris [String]
8486names = do i <- get
8587 let ctxt = tt_ctxt i
8688 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
8789
90+metavars :: Idris [String]
91+metavars = do i <- get
92+ return . map (show . nsroot) $ idris_metavars i \\ primDefs
93+
8894
8995modules :: Idris [String]
9096modules = do i <- get
@@ -97,14 +103,19 @@ completeWith ns n = if uniqueExists
97103 then [simpleCompletion n]
98104 else map simpleCompletion prefixMatches
99105 where prefixMatches = filter (isPrefixOf n) ns
100− uniqueExists = n `elem` prefixMatches
106+ uniqueExists = [n] == prefixMatches
101107
102108completeName :: [String] -> String -> Idris [Completion]
103109completeName extra n = do ns <- names
104110 return $ completeWith (extra ++ ns) n
105111
106112completeExpr :: [String] -> CompletionFunc Idris
107−completeExpr extra = completeWord Nothing " \t" (completeName extra)
113+completeExpr extra = completeWord Nothing (" \t(){}:" ++ opChars) (completeName extra)
114+
115+completeMetaVar :: CompletionFunc Idris
116+completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
117+ where completeM m = do mvs <- metavars
118+ return $ completeWith mvs m
108119
109120completeOption :: CompletionFunc Idris
110121completeOption = completeWord Nothing " \t" completeOpt
@@ -121,6 +132,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo
121132 completeArg OptionArg = completeOption (prev, next)
122133 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
123134 completeArg ExprArg = completeExpr [] (prev, next)
135+ completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
124136 completeCmdName = return $ ("", completeWith commands cmd)
125137
126138-- | Complete REPL commands and defined identifiers