@@ -7,7 +7,7 @@ Maintainer : The Idris Community.
77-}
88module Idris.Completion (replCompletion, proverCompletion) where
99
10−import Idris.Core.Evaluate (ctxtAlist)
10+import Idris.Core.Evaluate (definitions, ctxtAlist)
1111import Idris.Core.TT
1212
1313import Idris.AbsSyntax (runIO)
@@ -24,11 +24,12 @@ import Control.Monad.State.Strict
2424import Data.List
2525import Data.Maybe
2626import Data.Char(toLower)
27+import qualified Data.Map.Strict as Map
28+import qualified Data.Text as T
2729
2830import System.Console.Haskeline
2931import System.Console.ANSI (Color)
3032
31−
3233commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]
3334
3435tacticArgs :: [(String, Maybe TacticArg)]
@@ -36,23 +37,27 @@ tacticArgs = [ (name, args) | (names, args, _) <- Idris.Parser.Expr.tactics
3637 , name <- names ]
3738tactics = map fst tacticArgs
3839
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
45−
46−-- FIXME: Respect module imports
47−-- Issue #1767 in the issue tracker.
48−-- https://github.com/idris-lang/Idris-dev/issues/1767
4940-- | Get the user-visible names from the current interpreter state.
5041names :: Idris [String]
5142names = do i <- get
5243 let ctxt = tt_ctxt i
53− return . nub $
54− mapMaybe (nameString . fst) (ctxtAlist ctxt) ++
44+ return $
45+ mapMaybe nameString (allNames $ definitions ctxt) ++
5546 "Type" : map fst Idris.Parser.Expr.constants
47+ where
48+ -- We need both fully qualified names and identifiers that map to them
49+ allNames :: Ctxt a -> [Name]
50+ allNames ctxt =
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
5661
5762metavars :: Idris [String]
5863metavars = do i <- get
@@ -63,26 +68,49 @@ modules :: Idris [String]
6368modules = do i <- get
6469 return $ map show $ imported i
6570
66−
67−
68−completeWith :: [String] -> String -> [Completion]
69−completeWith ns n = if uniqueExists
70− then [simpleCompletion n]
71− else map simpleCompletion prefixMatches
71+namespaces :: Idris [String]
72+namespaces = do
73+ ctxt <- fmap tt_ctxt get
74+ let names = map fst $ ctxtAlist ctxt
75+ return $ nub $ catMaybes $ map extractNS names
76+ where
77+ extractNS :: Name -> Maybe String
78+ extractNS (NS n ns) = Just $ intercalate "." . map T.unpack . reverse $ ns
79+ extractNS _ = Nothing
80+
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
84+
85+completeWithMode :: CompletionMode -> [String] -> String -> [Completion]
86+completeWithMode mode ns n =
87+ if uniqueExists || (fullWord && mode == UpTo)
88+ then [simpleCompletion n]
89+ else map simpleCompletion prefixMatches
7290 where prefixMatches = filter (isPrefixOf n) ns
7391 uniqueExists = [n] == prefixMatches
92+ fullWord = n `elem` ns
7493
75−completeName :: [String] -> String -> Idris [Completion]
76−completeName extra n = do ns <- names
77− return $ completeWith (extra ++ ns) n
94+completeWith = completeWithMode Full
7895
79−completeExpr :: [String] -> CompletionFunc Idris
80−completeExpr extra = completeWord Nothing (" \t(){}:" ++ opChars) (completeName extra)
96+completeName :: CompletionMode -> [String] -> CompletionFunc Idris
97+completeName mode extra = completeWord Nothing (" \t(){}:" ++ completionWhitespace) completeName
98+ where
99+ completeName n = do
100+ ns <- names
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 \\ "."
81104
82105completeMetaVar :: CompletionFunc Idris
83106completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
84107 where completeM m = do mvs <- metavars
85− return $ completeWith mvs m
108+ return $ completeWithMode UpTo mvs m
109+
110+completeNamespace :: CompletionFunc Idris
111+completeNamespace = completeWord Nothing " \t" completeN
112+ where completeN n = do ns <- namespaces
113+ return $ completeWithMode UpTo ns n
86114
87115completeOption :: CompletionFunc Idris
88116completeOption = completeWord Nothing " \t" completeOpt
@@ -133,16 +161,16 @@ completeColour (prev, next) = case words (reverse prev) of
133161completeCmd :: String -> CompletionFunc Idris
134162completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
135163 where completeArg FileArg = completeFilename (prev, next)
136− completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
164+ completeArg NameArg = completeName UpTo [] (prev, next)
137165 completeArg OptionArg = completeOption (prev, next)
138− completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
139− completeArg NamespaceArg = noCompletion (prev, next) -- FIXME do later
140− completeArg ExprArg = completeExpr [] (prev, next)
141− completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
166+ completeArg ModuleArg = noCompletion (prev, next)
167+ completeArg NamespaceArg = completeNamespace (prev, next)
168+ completeArg ExprArg = completeName Full [] (prev, next)
169+ completeArg MetaVarArg = completeMetaVar (prev, next)
142170 completeArg ColourArg = completeColour (prev, next)
143171 completeArg NoArg = noCompletion (prev, next)
144172 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
145− completeArg DeclArg = completeExpr [] (prev, next)
173+ completeArg DeclArg = completeName Full [] (prev, next)
146174 completeArg PkgArgs = completePkg (prev, next)
147175 completeArg (ManyArgs a) = completeArg a
148176 completeArg (OptionalArg a) = completeArg a
@@ -154,7 +182,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo
154182replCompletion :: CompletionFunc Idris
155183replCompletion (prev, next) = case firstWord of
156184 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
157− _ -> completeExpr [] (prev, next)
185+ _ -> completeName UpTo [] (prev, next)
158186 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
159187
160188
@@ -171,7 +199,7 @@ completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeAr
171199 where completeTacName = return ("", completeWith tactics tac)
172200 completeArg Nothing = noCompletion (prev, next)
173201 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)
175203 completeArg (Just StringLitTArg) = noCompletion (prev, next)
176204 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
177205