@@ -7,7 +7,7 @@ Maintainer : The Idris Community.
8module Idris.Completion (replCompletion, proverCompletion) where
8module Idris.Completion (replCompletion, proverCompletion) where
10−import Idris.Core.Evaluate (ctxtAlist)
10+import Idris.Core.Evaluate (definitions, ctxtAlist)
11import Idris.Core.TT
11import Idris.Core.TT
13import Idris.AbsSyntax (runIO)
13import Idris.AbsSyntax (runIO)
@@ -24,11 +24,12 @@ import Control.Monad.State.Strict
24import Data.List
24import Data.List
25import Data.Maybe
25import Data.Maybe
26import Data.Char(toLower)
26import Data.Char(toLower)
27+import qualified Data.Map.Strict as Map
28+import qualified Data.Text as T
28import System.Console.Haskeline
30import System.Console.Haskeline
29import System.Console.ANSI (Color)
31import System.Console.ANSI (Color)
32commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]
33commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]
34tacticArgs :: [(String, Maybe TacticArg)]
35tacticArgs :: [(String, Maybe TacticArg)]
@@ -36,23 +37,27 @@ tacticArgs = [ (name, args) | (names, args, _) <- Idris.Parser.Expr.tactics
36 , name <- names ]
37 , name <- names ]
37tactics = map fst tacticArgs
38tactics = map fst tacticArgs
39−-- | Convert a name into a string usable for completion. Filters out names
40−-- that users probably don't want to see.
41−nameString :: Name -> Maybe String
42−nameString (UN n) = Just (str n)
43−nameString (NS n _) = nameString n
44−nameString _ = Nothing
46−-- FIXME: Respect module imports
47−-- Issue #1767 in the issue tracker.
48−-- https://github.com/idris-lang/Idris-dev/issues/1767
49-- | Get the user-visible names from the current interpreter state.
40-- | Get the user-visible names from the current interpreter state.
50names :: Idris [String]
41names :: Idris [String]
51names = do i <- get
42names = do i <- get
52 let ctxt = tt_ctxt i
43 let ctxt = tt_ctxt i
53− return . nub $
44+ return $
54− mapMaybe (nameString . fst) (ctxtAlist ctxt) ++
45+ mapMaybe nameString (allNames $ definitions ctxt) ++
55 "Type" : map fst Idris.Parser.Expr.constants
46 "Type" : map fst Idris.Parser.Expr.constants
48+ -- We need both fully qualified names and identifiers that map to them
49+ allNames :: Ctxt a -> [Name]
51+ let mappings = Map.toList ctxt
52+ in concatMap (\(name, mapping) -> name : Map.keys mapping) mappings
53+ -- Convert a name into a string usable for completion. Filters out names
54+ -- that users probably don't want to see.
55+ nameString :: Name -> Maybe String
56+ nameString (UN n) = Just (str n)
57+ nameString (NS n ns) =
58+ let path = intercalate "." . map T.unpack . reverse $ ns
59+ in fmap ((path ++ ".") ++) $ nameString n
60+ nameString _ = Nothing
57metavars :: Idris [String]
62metavars :: Idris [String]
58metavars = do i <- get
63metavars = do i <- get
@@ -63,26 +68,49 @@ modules :: Idris [String]
63modules = do i <- get
68modules = do i <- get
64 return $ map show $ imported i
69 return $ map show $ imported i
66−
71+namespaces :: Idris [String]
73+ ctxt <- fmap tt_ctxt get
74+ let names = map fst $ ctxtAlist ctxt
75+ return $ nub $ catMaybes $ map extractNS names
77+ extractNS :: Name -> Maybe String
78+ extractNS (NS n ns) = Just $ intercalate "." . map T.unpack . reverse $ ns
79+ extractNS _ = Nothing
81+-- UpTo means if user enters full name then no other completions are shown
82+-- Full always show other (longer) completions if there are any
83+data CompletionMode = UpTo | Full deriving Eq
68−completeWith :: [String] -> String -> [Completion]
85+completeWithMode :: CompletionMode -> [String] -> String -> [Completion]
86+completeWithMode mode ns n =
69−completeWith ns n = if uniqueExists
87+ if uniqueExists || (fullWord && mode == UpTo)
70− then [simpleCompletion n]
88+ then [simpleCompletion n]
71− else map simpleCompletion prefixMatches
89+ else map simpleCompletion prefixMatches
72 where prefixMatches = filter (isPrefixOf n) ns
90 where prefixMatches = filter (isPrefixOf n) ns
73 uniqueExists = [n] == prefixMatches
91 uniqueExists = [n] == prefixMatches
92+ fullWord = n `elem` ns
75−completeName :: [String] -> String -> Idris [Completion]
94+completeWith = completeWithMode Full
76−completeName extra n = do ns <- names
77− return $ completeWith (extra ++ ns) n
79−completeExpr :: [String] -> CompletionFunc Idris
96+completeName :: CompletionMode -> [String] -> CompletionFunc Idris
80−completeExpr extra = completeWord Nothing (" \t(){}:" ++ opChars) (completeName extra)
97+completeName mode extra = completeWord Nothing (" \t(){}:" ++ completionWhitespace) completeName
101+ return $ completeWithMode mode (extra ++ ns) n
102+ -- The '.' needs not to be taken into consideration because it serves as namespace separator
103+ completionWhitespace = opChars \\ "."
82completeMetaVar :: CompletionFunc Idris
105completeMetaVar :: CompletionFunc Idris
83completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
106completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
84 where completeM m = do mvs <- metavars
107 where completeM m = do mvs <- metavars
85− return $ completeWith mvs m
108+ return $ completeWithMode UpTo mvs m
110+completeNamespace :: CompletionFunc Idris
111+completeNamespace = completeWord Nothing " \t" completeN
112+ where completeN n = do ns <- namespaces
113+ return $ completeWithMode UpTo ns n
87completeOption :: CompletionFunc Idris
115completeOption :: CompletionFunc Idris
88completeOption = completeWord Nothing " \t" completeOpt
116completeOption = completeWord Nothing " \t" completeOpt
@@ -133,16 +161,16 @@ completeColour (prev, next) = case words (reverse prev) of
133completeCmd :: String -> CompletionFunc Idris
161completeCmd :: String -> CompletionFunc Idris
134completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
162completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
135 where completeArg FileArg = completeFilename (prev, next)
163 where completeArg FileArg = completeFilename (prev, next)
136− completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
164+ completeArg NameArg = completeName UpTo [] (prev, next)
137 completeArg OptionArg = completeOption (prev, next)
165 completeArg OptionArg = completeOption (prev, next)
138− completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
166+ completeArg ModuleArg = noCompletion (prev, next)
139− completeArg NamespaceArg = noCompletion (prev, next) -- FIXME do later
167+ completeArg NamespaceArg = completeNamespace (prev, next)
140− completeArg ExprArg = completeExpr [] (prev, next)
168+ completeArg ExprArg = completeName Full [] (prev, next)
141− completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
169+ completeArg MetaVarArg = completeMetaVar (prev, next)
142 completeArg ColourArg = completeColour (prev, next)
170 completeArg ColourArg = completeColour (prev, next)
143 completeArg NoArg = noCompletion (prev, next)
171 completeArg NoArg = noCompletion (prev, next)
144 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
172 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
145− completeArg DeclArg = completeExpr [] (prev, next)
173+ completeArg DeclArg = completeName Full [] (prev, next)
146 completeArg PkgArgs = completePkg (prev, next)
174 completeArg PkgArgs = completePkg (prev, next)
147 completeArg (ManyArgs a) = completeArg a
175 completeArg (ManyArgs a) = completeArg a
148 completeArg (OptionalArg a) = completeArg a
176 completeArg (OptionalArg a) = completeArg a
@@ -154,7 +182,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo
154replCompletion :: CompletionFunc Idris
182replCompletion :: CompletionFunc Idris
155replCompletion (prev, next) = case firstWord of
183replCompletion (prev, next) = case firstWord of
156 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
184 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
157− _ -> completeExpr [] (prev, next)
185+ _ -> completeName UpTo [] (prev, next)
158 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
186 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
@@ -171,7 +199,7 @@ completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeAr
171 where completeTacName = return ("", completeWith tactics tac)
199 where completeTacName = return ("", completeWith tactics tac)
172 completeArg Nothing = noCompletion (prev, next)
200 completeArg Nothing = noCompletion (prev, next)
173 completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!
201 completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!
174− completeArg (Just ExprTArg) = completeExpr as (prev, next)
202+ completeArg (Just ExprTArg) = completeName Full as (prev, next)
175 completeArg (Just StringLitTArg) = noCompletion (prev, next)
203 completeArg (Just StringLitTArg) = noCompletion (prev, next)
176 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
204 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO