git.iko.soy/Idris-dev
on master help sign in
Merge pull request #228 from david-christiansen/completion
46fa727Edwin Brady
src/Core/CoreParser.hs+6−3
compare with master
unifiedsplit
@@ -1,7 +1,7 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2
2
3module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName,
3module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName,
4− idrisLexer, maybeWithNS, pDocComment) where
4+ idrisLexer, maybeWithNS, pDocComment, opChars) where
5
5
6import Core.TT
6import Core.TT
7
7
@@ -39,8 +39,11 @@ idrisDef = haskellDef {
39 "Bits8", "Bits16", "Bits32", "Bits64"]
39 "Bits8", "Bits16", "Bits32", "Bits64"]
40 }
40 }
41
41
42+-- | The characters allowed in operator names
43+opChars = ":!#$%&*+./<=>?@\\^|-~"
44+
42−iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"
45+iOpStart = oneOf opChars
43−iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
46+iOpLetter = oneOf opChars
44-- <|> letter
47-- <|> letter
45
48
46idrisLexer :: TokenParser a
49idrisLexer :: TokenParser a
src/Idris/Completion.hs+17−5
@@ -3,6 +3,7 @@ module Idris.Completion (replCompletion, proverCompletion) where
3
3
4import Core.Evaluate (ctxtAlist)
4import Core.Evaluate (ctxtAlist)
5import Core.TT
5import Core.TT
6+import Core.CoreParser (opChars)
6
7
7import Idris.AbsSyntaxTree
8import Idris.AbsSyntaxTree
8
9
@@ -20,6 +21,7 @@ data CmdArg = ExprArg -- ^ The command takes an expression
20 | FileArg -- ^ The command takes a file
21 | FileArg -- ^ The command takes a file
21 | ModuleArg -- ^ The command takes a module name
22 | ModuleArg -- ^ The command takes a module name
22 | OptionArg -- ^ The command takes an option
23 | OptionArg -- ^ The command takes an option
24+ | MetaVarArg -- ^ The command takes a metavariable
23
25
24-- | Information about how to complete the various commands
26-- | Information about how to complete the various commands
25cmdArgs :: [(String, CmdArg)]
27cmdArgs :: [(String, CmdArg)]
@@ -32,8 +34,8 @@ cmdArgs = [ (":t", ExprArg)
32 , (":l", FileArg)
34 , (":l", FileArg)
33 , (":load", FileArg)
35 , (":load", FileArg)
34 , (":m", ModuleArg) -- NOTE: Argumentless form is a different command
36 , (":m", ModuleArg) -- NOTE: Argumentless form is a different command
35− , (":p", NameArg)
37+ , (":p", MetaVarArg)
36− , (":prove", NameArg)
38+ , (":prove", MetaVarArg)
37 , (":a", NameArg)
39 , (":a", NameArg)
38 , (":addproof", NameArg)
40 , (":addproof", NameArg)
39 , (":rmproof", NameArg)
41 , (":rmproof", NameArg)
@@ -80,11 +82,15 @@ nameString _ = Nothing
80
82
81-- FIXME: Respect module imports
83-- FIXME: Respect module imports
82-- | Get the user-visible names from the current interpreter state.
84-- | Get the user-visible names from the current interpreter state.
83−names :: Idris[String]
85+names :: Idris [String]
84names = do i <- get
86names = do i <- get
85 let ctxt = tt_ctxt i
87 let ctxt = tt_ctxt i
86 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
88 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
87
89
90+metavars :: Idris [String]
91+metavars = do i <- get
92+ return . map (show . nsroot) $ idris_metavars i \\ primDefs
93+
88
94
89modules :: Idris [String]
95modules :: Idris [String]
90modules = do i <- get
96modules = do i <- get
@@ -97,14 +103,19 @@ completeWith ns n = if uniqueExists
97 then [simpleCompletion n]
103 then [simpleCompletion n]
98 else map simpleCompletion prefixMatches
104 else map simpleCompletion prefixMatches
99 where prefixMatches = filter (isPrefixOf n) ns
105 where prefixMatches = filter (isPrefixOf n) ns
100− uniqueExists = n `elem` prefixMatches
106+ uniqueExists = [n] == prefixMatches
101
107
102completeName :: [String] -> String -> Idris [Completion]
108completeName :: [String] -> String -> Idris [Completion]
103completeName extra n = do ns <- names
109completeName extra n = do ns <- names
104 return $ completeWith (extra ++ ns) n
110 return $ completeWith (extra ++ ns) n
105
111
106completeExpr :: [String] -> CompletionFunc Idris
112completeExpr :: [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
108
119
109completeOption :: CompletionFunc Idris
120completeOption :: CompletionFunc Idris
110completeOption = completeWord Nothing " \t" completeOpt
121completeOption = completeWord Nothing " \t" completeOpt
@@ -121,6 +132,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo
121 completeArg OptionArg = completeOption (prev, next)
132 completeArg OptionArg = completeOption (prev, next)
122 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
133 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
123 completeArg ExprArg = completeExpr [] (prev, next)
134 completeArg ExprArg = completeExpr [] (prev, next)
135+ completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
124 completeCmdName = return $ ("", completeWith commands cmd)
136 completeCmdName = return $ ("", completeWith commands cmd)
125
137
126-- | Complete REPL commands and defined identifiers
138-- | Complete REPL commands and defined identifiers