From 7ba70dd7a249a7250c5a94ffdcec57b14a0ed10e Mon Sep 17 00:00:00 2001 From: arash Date: Sat, 6 Sep 2025 00:06:40 +0200 Subject: [PATCH 1/7] when starting in IdeMode read all TTCs from package_dirs, use them to provide more completions with auto-imports --- CONTRIBUTORS | 1 + src/Core/Binary.idr | 3 + src/Idris/CommandLine.idr | 4 ++ src/Idris/Driver.idr | 7 ++- src/Idris/IDEMode/REPL.idr | 15 ++++- src/Idris/REPL/IDEIndex.idr | 68 ++++++++++++++++++++ src/Idris/REPL/Opts.idr | 4 ++ src/Idris/SetOptions.idr | 9 +++ src/Protocol/IDE/Result.idr | 19 +++++- src/TTImp/Interactive/Completion.idr | 94 ++++++++++++++++++++-------- 10 files changed, 193 insertions(+), 31 deletions(-) create mode 100644 src/Idris/REPL/IDEIndex.idr diff --git a/CONTRIBUTORS b/CONTRIBUTORS index 7c9c9e4e8ca..d6732cf5ea2 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -32,6 +32,7 @@ George Pollard GhiOm Giuseppe Lomurno Guillaume Allais +Hakan Aras Hiroki Hattori Ilya Rezvov Jacob Walters diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index c24195d06dd..cde150444f7 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -37,6 +37,7 @@ checkTTCVersion : String -> Int -> Int -> Core () checkTTCVersion file ver exp = when (ver /= exp) (throw $ TTCError $ Format file ver exp) +public export record TTCFile extra where constructor MkTTCFile version : Int @@ -220,6 +221,7 @@ writeTTCFile b file_in toBuf (transforms file) toBuf (foreignExports file) +export readTTCFile : TTC extra => {auto c : Ref Ctxt Defs} -> Bool -> String -> Maybe (Namespace) -> @@ -339,6 +341,7 @@ writeToTTC extradata sourceFileName ttcFileName | Left err => throw (InternalError (ttcFileName ++ ": " ++ show err)) pure () +export addGlobalDef : {auto c : Ref Ctxt Defs} -> (modns : ModuleIdent) -> Namespace -> (importAs : Maybe Namespace) -> diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index e94fe5ba5b4..f4c26528521 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -131,6 +131,8 @@ data CLOpt IdeMode | ||| Whether or not to run IdeMode (using a socket instead of stdin/stdout) IdeModeSocket String | + ||| Index all available modules to extend IdeMode functionality + IdeIndex | ||| Run as a checker for the core language TTImp Yaffle String | ||| Dump metadata from a .ttm file @@ -324,6 +326,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] MkOpt ["--ide-mode-socket"] [Optional "host:port"] (\hp => [IdeModeSocket $ fromMaybe (formatSocketAddress (ideSocketModeAddress [])) hp]) (Just $ "Run the ide socket mode on given host and port (random open socket by default)"), + MkOpt ["--ide-index"] [] [IdeIndex] + (Just "Index all available modules to extend IdeMode functionality"), optSeparator, MkOpt ["--client"] [Required "REPL command"] (\f => [RunREPL f]) diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index 0a4f4cf6333..780ce43840f 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -16,6 +16,7 @@ import Idris.IDEMode.REPL import Idris.Package import Idris.ProcessIdr import Idris.REPL +import Idris.REPL.IDEIndex import Idris.SetOptions import Idris.Syntax import Idris.Version @@ -149,8 +150,9 @@ stMain cgs opts when (ignoreMissingIpkg opts) $ setSession ({ ignoreMissingPkg := True } !getSession) - let ide = ideMode opts + let ideIndex = ideIndex opts let ideSocket = ideModeSocket opts + let ide = ideMode opts || (ideIndex && not ideSocket) let outmode = if ide then IDEMode 0 stdin stdout else REPL InfoLvl o <- newRef ROpts (REPL.Opts.defaultOpts Nothing outmode cgs) updateEnv @@ -166,6 +168,9 @@ stMain cgs opts \{renderedSuggestion} """ update ROpts { mainfile := fname } + if ideIndex + then update ROpts { ideIndex := Just (MkIDEIndex []) } + else pure () -- start by going over the pre-options, and stop if we do not need to -- continue diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 80f0de0e964..57c5ee5df3b 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -11,6 +11,7 @@ import Idris.Package import Idris.Parser import Idris.Pretty import Idris.REPL +import Idris.REPL.IDEIndex import Idris.Syntax import Idris.Version import Idris.Doc.String @@ -124,7 +125,7 @@ todoCmd cmdName = iputStrLn $ reflow $ cmdName ++ ": command not yet implemented data IDEResult = REPL REPLResult - | CompletionList (List String) String + | CompletionList (List Completion) String | NameList (List Name) | FoundHoles (List Holes.Data) | Term String -- should be a PTerm + metadata, or SExp. @@ -393,7 +394,10 @@ displayIDEResult outf i (REPL $ (Edited (MadeCase lit cstr))) displayIDEResult outf i (FoundHoles holes) = printIDEResult outf i $ AHoleList $ map holeIDE holes displayIDEResult outf i (CompletionList ns r) - = printIDEResult outf i $ ACompletionList ns r + = printIDEResult outf i $ ACompletionList (map toCompletionItem ns) r + where + toCompletionItem : Completion -> CompletionItem + toCompletionItem (MkCompletion n i) = MkCompletionItem n i displayIDEResult outf i (NameList ns) = printIDEResult outf i $ ANameList (map show ns) displayIDEResult outf i (Term t) @@ -504,6 +508,13 @@ replIDE : {auto c : Ref Ctxt Defs} -> Core () replIDE = do res <- getOutput + ropts <- get ROpts + if isJust ropts.ideIndex + then do + d <- getDirs + ideIndex <- mkIdeIndex d.package_dirs + update ROpts { ideIndex := Just ideIndex } + else pure () case res of REPL _ => printError $ reflow "Running idemode but output isn't" IDEMode _ inf outf => do diff --git a/src/Idris/REPL/IDEIndex.idr b/src/Idris/REPL/IDEIndex.idr new file mode 100644 index 00000000000..e87af954ca0 --- /dev/null +++ b/src/Idris/REPL/IDEIndex.idr @@ -0,0 +1,68 @@ +module Idris.REPL.IDEIndex + +import Core.Binary +import Core.Core +import Core.Context +import Core.Name.Namespace +import Data.String +import Idris.Syntax +import Idris.Syntax.TTC +import Libraries.Data.WithDefault +import Libraries.Utils.Path +import System.Directory + +||| An index of exported definitions from modules of available packages. +public export +record IDEIndex where + constructor MkIDEIndex + indexedDefs : List GlobalDef + +findFiles : (String -> Bool) -> String -> Core (List String) +findFiles pred dir = do + Right list <- coreLift $ listDir dir + | Left _ => pure [] + let list = (dir ) <$> filter (\f => not $ f == "." || f == "..") list + concat <$> traverse go list + where + go : String -> Core (List String) + go file = do + if pred file + then pure [file] + else findFiles pred file + +readTtcFile : Ref Ctxt Defs => String -> Core (TTCFile SyntaxInfo) +readTtcFile fname = do + Right buffer <- coreLift $ readFromFile fname + | Left err => throw (InternalError (fname ++ ": " ++ show err)) + bin <- newRef Bin buffer -- for reading the file into + readTTCFile True fname Nothing bin + +defIfVisible : Ref Ctxt Defs => Name -> Core (Maybe GlobalDef) +defIfVisible nsn = do + defs <- get Ctxt + let (ns, n) = splitNS nsn + let cns = currentNS defs + Just def <- lookupCtxtExact nsn (gamma defs) + | Nothing => pure Nothing + if visibleIn cns nsn (collapseDefault $ visibility def) + then pure (Just def) + else pure Nothing + +allExportedDefs : Ref Ctxt Defs => Core (List GlobalDef) +allExportedDefs = do + allNames <- allNames (gamma $ !(get Ctxt)) + let names = filter (isJust . userNameRoot) allNames + mapMaybeM defIfVisible names + +export +mkIdeIndex : List String -> Core IDEIndex +mkIdeIndex pkg_dirs = do + let pkgTtcDirs = pkg_dirs <&> ( show ttcVersion) + pkgTtcFiles <- concat <$> traverse (findFiles $ isSuffixOf ".ttc") pkgTtcDirs + _ <- newRef Ctxt !initDefs + ttcs <- traverse readTtcFile pkgTtcFiles + modNS <- nsAsModuleIdent <$> getNS + traverse_ (\x => traverse_ (addGlobalDef modNS (currentNS x) Nothing) (context x)) ttcs + pure $ MkIDEIndex (!allExportedDefs) + + \ No newline at end of file diff --git a/src/Idris/REPL/Opts.idr b/src/Idris/REPL/Opts.idr index e339f24595e..6e7ed3e8ae6 100644 --- a/src/Idris/REPL/Opts.idr +++ b/src/Idris/REPL/Opts.idr @@ -1,6 +1,7 @@ module Idris.REPL.Opts import Compiler.Common +import Idris.REPL.IDEIndex import Idris.Syntax import Parser.Unlit import TTImp.TTImp @@ -52,6 +53,8 @@ record REPLOpts where -- TODO: Move extraCodegens from here, it doesn't belong, but there's nowhere -- better to stick it now. extraCodegens : List (String, Codegen) + -- TODO: Ditto for the ideIndex. + ideIndex : Maybe IDEIndex consoleWidth : Maybe Nat -- Nothing is auto color : Bool synHighlightOn : Bool @@ -78,6 +81,7 @@ defaultOpts fname outmode cgs , gdResult = Nothing , evalResultName = Nothing , extraCodegens = cgs + , ideIndex = Nothing , consoleWidth = Nothing , color = True , synHighlightOn = True diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 2615417d637..8fdd685c213 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -408,6 +408,9 @@ preOptions (IdeMode :: opts) preOptions (IdeModeSocket _ :: opts) = do setSession ({ nobanner := True } !getSession) preOptions opts +preOptions (IdeIndex :: opts) + = do setSession ({ nobanner := True } !getSession) + preOptions opts preOptions (CheckOnly :: opts) = do setSession ({ nobanner := True } !getSession) preOptions opts @@ -581,6 +584,12 @@ ideMode [] = False ideMode (IdeMode :: _) = True ideMode (_ :: xs) = ideMode xs +export +ideIndex : List CLOpt -> Bool +ideIndex [] = False +ideIndex (IdeIndex :: _) = True +ideIndex (_ :: xs) = ideIndex xs + export ideModeSocket : List CLOpt -> Bool ideModeSocket [] = False diff --git a/src/Protocol/IDE/Result.idr b/src/Protocol/IDE/Result.idr index 6cf5d88e4eb..26ab0fc7873 100644 --- a/src/Protocol/IDE/Result.idr +++ b/src/Protocol/IDE/Result.idr @@ -54,6 +54,21 @@ FromSExpable REPLOption where Just $ MkOption {name, type = ATOM, val} fromSExp _ = Nothing +public export +record CompletionItem where + constructor MkCompletionItem + name : String + import_ : Maybe String + +SExpable CompletionItem where + toSExp (MkCompletionItem n Nothing) = StringAtom n + toSExp (MkCompletionItem n (Just i)) = SExpList [StringAtom n, StringAtom i] + +FromSExpable CompletionItem where + fromSExp (StringAtom n) = Just $ MkCompletionItem n Nothing + fromSExp (SExpList [StringAtom n, StringAtom i]) = Just $ MkCompletionItem n (Just i) + fromSExp _ = Nothing + public export record MetaVarLemma where constructor MkMetaVarLemma @@ -109,7 +124,7 @@ data Result = | AMetaVarLemma MetaVarLemma | ANameLocList (List (String, FileContext)) | AHoleList (List HoleData) - | ACompletionList (List String) String + | ACompletionList (List CompletionItem) String | ANameList (List String) | AnOptionList (List REPLOption) | AnIntroList (List1 String) @@ -123,7 +138,7 @@ SExpable Result where toSExp (ANameLocList fcs) = toSExp fcs toSExp (AHoleList holes) = toSExp holes toSExp (ANameList names) = SExpList (map StringAtom names) - toSExp (ACompletionList names str) = SExpList [SExpList (map StringAtom names), StringAtom str] + toSExp (ACompletionList completions str) = SExpList [SExpList (map toSExp completions), StringAtom str] toSExp (AnOptionList opts) = toSExp opts toSExp (AnIntroList iss) = toSExp iss diff --git a/src/TTImp/Interactive/Completion.idr b/src/TTImp/Interactive/Completion.idr index 3b76e692bea..051b1bf8e58 100644 --- a/src/TTImp/Interactive/Completion.idr +++ b/src/TTImp/Interactive/Completion.idr @@ -4,13 +4,30 @@ import Core.Context import Core.Context.Log import Core.Core -import Idris.Syntax import Idris.Parser +import Idris.REPL.IDEIndex +import Idris.REPL.Opts +import Idris.Syntax import Data.String import Libraries.Data.WithDefault +||| A single suggested completion. +||| If import_ is Just, it's a module namespace that has to be imported +||| to access the name. +public export +record Completion where + constructor MkCompletion + name : String + import_ : Maybe String + +simpleCompletion : String -> Completion +simpleCompletion = flip MkCompletion Nothing + +autoImportCompletion : String -> String -> Completion +autoImportCompletion n = MkCompletion n . Just + ||| Completion tasks are varied: ||| are we trying to fill in a name, a REPL command, a pragma? data Task @@ -43,31 +60,54 @@ parseTask line = ||| Name completion receives the prefix of the name to be completed nameCompletion : {auto c : Ref Ctxt Defs} -> - (pref : String) -> Core (List String) + {auto o : Ref ROpts REPLOpts} -> + (pref : String) -> Core (List Completion) nameCompletion pref = do log "ide-mode.completion" 30 $ "Looking at name completions for \{show pref}" - defs <- get Ctxt - let cns = currentNS defs - nms <- flip mapMaybeM !(allNames (gamma defs)) $ \ nsn => do - -- the name better be a completion - log "ide-mode.completion" 50 $ "Looking at \{show nsn}" - let (ns, n) = splitNS nsn - let True = pref `isPrefixOf` nameRoot n - | False => pure Nothing - -- and it better be visible - Just def <- lookupCtxtExact nsn (gamma defs) - | Nothing => pure Nothing - let True = visibleIn cns nsn (collapseDefault $ visibility def) - | False => pure Nothing - pure (Just n) - pure (map show $ nub nms) + + ctxtDefs <- get Ctxt + let cns = currentNS ctxtDefs + + -- Look among already imported names: + ctxtNamesWithPrefix <- filter hasPrefix <$> allNames (gamma ctxtDefs) + ctxtVisibleGDefs <- filter (isVisible cns) <$> mapMaybeM (lookupName ctxtDefs) ctxtNamesWithPrefix + let ctxtVisibleNames = nub $ fst <$> ctxtVisibleGDefs + let ctxCompletions = simpleCompletion . unqualName <$> ctxtVisibleNames + + -- If we have an index, look there as well + Just ideIndex <- ideIndex <$> get ROpts + | Nothing => pure ctxCompletions + let idxDefs = filter (hasPrefix . fullname) $ indexedDefs ideIndex + let idxNames = filter (not . (`elem` ctxtVisibleNames)) $ fullname <$> idxDefs + let idxCompletions = autoImport <$> idxNames + pure (ctxCompletions ++ idxCompletions) + + where + unqualName : Name -> String + unqualName = nameRoot . snd . splitNS + + autoImport : Name -> Completion + autoImport n = autoImportCompletion (unqualName n) (show $ fst $ splitNS n) + + hasPrefix : Name -> Bool + hasPrefix = isPrefixOf pref . unqualName + + lookupName : Defs -> Name -> Core (Maybe (Name, GlobalDef)) + lookupName defs nsn = do + Just def <- lookupCtxtExact nsn (gamma defs) + | Nothing => pure Nothing + pure (Just (nsn, def)) + + isVisible : Namespace -> (Name, GlobalDef) -> Bool + isVisible cns gdef = visibleIn cns (fst gdef) (collapseDefault $ visibility (snd gdef)) + ||| Completion among a list of constants -oneOfCompletion : String -> List String -> Maybe (List String) +oneOfCompletion : String -> List String -> Maybe (List Completion) oneOfCompletion pref candidates = do let cs@(_ :: _) = filter (pref `isPrefixOf`) candidates | _ => Nothing - pure cs + pure $ simpleCompletion <$> cs ||| Pragma completion receives everything on the line following the % character ||| and completes either the pragma itself of one of its arguments @@ -75,18 +115,19 @@ oneOfCompletion pref candidates = do ||| %default to -> %default total ||| %logging "id -> %logging "ide-mode.(...)" with all the valid topics! pragmaCompletion : {auto c : Ref Ctxt Defs} -> + {auto o : Ref ROpts REPLOpts} -> (prag : Maybe KwPragma) -> (pref : String) -> - Core (Maybe (String, List String)) + Core (Maybe (String, List Completion)) pragmaCompletion Nothing pref = pure $ do let ps@(_ :: _) = flip List.mapMaybe allPragmas $ \ prag => do let prag = show prag guard ("%" ++ pref `isPrefixOf` prag) pure prag | _ => Nothing - pure ("", ps) + pure ("", simpleCompletion <$> ps) pragmaCompletion (Just kw) pref = go (pragmaArgs kw) (break isSpace pref) where - go : List PragmaArg -> (String, String) -> Core (Maybe (String, List String)) + go : List PragmaArg -> (String, String) -> Core (Maybe (String, List Completion)) go (AName {} :: _) (here, "") = do ns@(_ :: _) <- nameCompletion here | _ => pure Nothing @@ -97,7 +138,7 @@ pragmaCompletion (Just kw) pref = go (pragmaArgs kw) (break isSpace pref) where | _ => pure Nothing let lvls@(_ :: _) = filter ((here `isPrefixOf`) . fst) knownTopics | _ => pure Nothing - pure (Just ("", map (show . fst) lvls)) + pure (Just ("", map (simpleCompletion . show . fst) lvls)) go (ALangExt :: _) (here, "") = pure (("",) <$> oneOfCompletion here (map show allLangExts)) go (ATotalityLevel :: _) (here, "") = pure (("",) <$> oneOfCompletion here ["partial", "covering", "total"]) go (_ :: args) (skip, rest) = @@ -110,7 +151,8 @@ pragmaCompletion (Just kw) pref = go (pragmaArgs kw) (break isSpace pref) where ||| 2. the list of possible completions export completion : {auto c : Ref Ctxt Defs} -> - (line : String) -> Core (Maybe (String, List String)) + {auto o : Ref ROpts REPLOpts} -> + (line : String) -> Core (Maybe (String, List Completion)) completion line = do let Just (ctxt, task) = parseTask line | _ => pure Nothing @@ -118,8 +160,8 @@ completion line = do NameCompletion pref => (Just . (ctxt,)) <$> nameCompletion pref PragmaCompletion mprag pref => map (mapFst (ctxt ++)) <$> pragmaCompletion mprag pref CommandCompletion pref => case words pref of - ["logging"] => pure $ Just (ctxt ++ ":logging", map ((" " ++) . show . fst) knownTopics) + ["logging"] => pure $ Just (ctxt ++ ":logging", map (simpleCompletion . (" " ++) . show . fst) knownTopics) [pref] => let commands = concatMap fst parserCommandsForHelp in - pure $ map ((ctxt,) . map (":" ++)) $ oneOfCompletion pref commands + pure $ map ((ctxt,) . map ({ name $= (":" ++)})) $ oneOfCompletion pref commands ["logging", w] => pure $ map (ctxt ++ ":logging ",) (oneOfCompletion w (map (show . fst) knownTopics)) _ => pure Nothing From 13c941f896fd02866663622092b15166af906d20 Mon Sep 17 00:00:00 2001 From: arash Date: Sat, 6 Sep 2025 00:19:46 +0200 Subject: [PATCH 2/7] changelog-next for --ide-index option --- CHANGELOG_NEXT.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 45cb75a787b..d5f1d70d8a1 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -32,6 +32,11 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO * The `idris2 --exec` command now takes an arbitrary expression, not just the function name. +* A new `idris2 --ide-index` option reads all modules from dependencies and + uses them to provide completion for symbols that aren't yet imported. + If neither `--ide-mode` nor `--ide-mode-socket` is set, this option + automatically enables `--ide-mode`. + * Command-line arguments beginning with `--` which are not a known flag now produce an error. From cf7a42c66b4012a21ee18f9a3ccc02ef3ba734bb Mon Sep 17 00:00:00 2001 From: arash Date: Sat, 6 Sep 2025 16:33:20 +0200 Subject: [PATCH 3/7] store the module names along with definitions in IDEIndex (no easy way to recover them later) --- src/Idris/REPL/IDEIndex.idr | 31 ++++++++++++++++++---------- src/TTImp/Interactive/Completion.idr | 24 ++++++++++++++------- 2 files changed, 36 insertions(+), 19 deletions(-) diff --git a/src/Idris/REPL/IDEIndex.idr b/src/Idris/REPL/IDEIndex.idr index e87af954ca0..edb04895d4a 100644 --- a/src/Idris/REPL/IDEIndex.idr +++ b/src/Idris/REPL/IDEIndex.idr @@ -11,11 +11,17 @@ import Libraries.Data.WithDefault import Libraries.Utils.Path import System.Directory +public export +record IndexedDef where + constructor MkIndexedDef + moduleNS : Namespace + def : GlobalDef + ||| An index of exported definitions from modules of available packages. public export record IDEIndex where constructor MkIDEIndex - indexedDefs : List GlobalDef + indexedDefs : List IndexedDef findFiles : (String -> Bool) -> String -> Core (List String) findFiles pred dir = do @@ -48,21 +54,24 @@ defIfVisible nsn = do then pure (Just def) else pure Nothing -allExportedDefs : Ref Ctxt Defs => Core (List GlobalDef) -allExportedDefs = do - allNames <- allNames (gamma $ !(get Ctxt)) - let names = filter (isJust . userNameRoot) allNames - mapMaybeM defIfVisible names +indexDefsOfTtc : String -> Core (List IndexedDef) +indexDefsOfTtc ttcFile = do + _ <- newRef Ctxt !initDefs + ttc <- readTtcFile ttcFile + let ttcModNS = currentNS ttc + modNS <- nsAsModuleIdent <$> getNS + traverse_ (addGlobalDef modNS ttcModNS Nothing) (context ttc) + names <- filter (isJust . userNameRoot) <$> allNames (gamma !(get Ctxt)) + visibleDefs <- mapMaybeM defIfVisible names + pure $ MkIndexedDef ttcModNS <$> visibleDefs +||| Builds an IDE index from all TTC files found in the given package directories. export mkIdeIndex : List String -> Core IDEIndex mkIdeIndex pkg_dirs = do let pkgTtcDirs = pkg_dirs <&> ( show ttcVersion) pkgTtcFiles <- concat <$> traverse (findFiles $ isSuffixOf ".ttc") pkgTtcDirs - _ <- newRef Ctxt !initDefs - ttcs <- traverse readTtcFile pkgTtcFiles - modNS <- nsAsModuleIdent <$> getNS - traverse_ (\x => traverse_ (addGlobalDef modNS (currentNS x) Nothing) (context x)) ttcs - pure $ MkIDEIndex (!allExportedDefs) + indexedDefs <- concat <$> traverse indexDefsOfTtc pkgTtcFiles + pure $ MkIDEIndex indexedDefs \ No newline at end of file diff --git a/src/TTImp/Interactive/Completion.idr b/src/TTImp/Interactive/Completion.idr index 051b1bf8e58..f5f4b18c3e9 100644 --- a/src/TTImp/Interactive/Completion.idr +++ b/src/TTImp/Interactive/Completion.idr @@ -69,7 +69,7 @@ nameCompletion pref = do let cns = currentNS ctxtDefs -- Look among already imported names: - ctxtNamesWithPrefix <- filter hasPrefix <$> allNames (gamma ctxtDefs) + ctxtNamesWithPrefix <- filter validCompletion <$> allNames (gamma ctxtDefs) ctxtVisibleGDefs <- filter (isVisible cns) <$> mapMaybeM (lookupName ctxtDefs) ctxtNamesWithPrefix let ctxtVisibleNames = nub $ fst <$> ctxtVisibleGDefs let ctxCompletions = simpleCompletion . unqualName <$> ctxtVisibleNames @@ -77,20 +77,28 @@ nameCompletion pref = do -- If we have an index, look there as well Just ideIndex <- ideIndex <$> get ROpts | Nothing => pure ctxCompletions - let idxDefs = filter (hasPrefix . fullname) $ indexedDefs ideIndex - let idxNames = filter (not . (`elem` ctxtVisibleNames)) $ fullname <$> idxDefs - let idxCompletions = autoImport <$> idxNames + let idxDefs = filter (validCompletion . fullname . def) $ indexedDefs ideIndex + let idxUnseenDefs = filter (not . (`elem` ctxtVisibleNames) . fullname . def) idxDefs + let idxCompletions = autoImport <$> idxUnseenDefs pure (ctxCompletions ++ idxCompletions) where unqualName : Name -> String unqualName = nameRoot . snd . splitNS - autoImport : Name -> Completion - autoImport n = autoImportCompletion (unqualName n) (show $ fst $ splitNS n) + moduleOf : GlobalDef -> String + moduleOf d = let n = fullname d in case n of + NS ns _ => show ns + otherwise => "" - hasPrefix : Name -> Bool - hasPrefix = isPrefixOf pref . unqualName + autoImport : IndexedDef -> Completion + autoImport d = autoImportCompletion (unqualName $ fullname $ def d) (show $ moduleNS d) + + validIdentifier : String -> Bool + validIdentifier = all (\c => isAlphaNum c || c == '_' || c == '.' || c > chr 160) . unpack + + validCompletion : Name -> Bool + validCompletion n = let n' = unqualName n in isPrefixOf pref n' && validIdentifier n' lookupName : Defs -> Name -> Core (Maybe (Name, GlobalDef)) lookupName defs nsn = do From 987a7f4c64c8a164197def28dc60e90b853e6515 Mon Sep 17 00:00:00 2001 From: arash Date: Sun, 7 Sep 2025 11:52:23 +0200 Subject: [PATCH 4/7] ide-index no longer relies on previously private members of Core.Binary --- src/Core/Binary.idr | 3 -- src/Idris/REPL/IDEIndex.idr | 59 ++++++++++++++++------------ src/TTImp/Interactive/Completion.idr | 5 --- 3 files changed, 34 insertions(+), 33 deletions(-) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index cde150444f7..c24195d06dd 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -37,7 +37,6 @@ checkTTCVersion : String -> Int -> Int -> Core () checkTTCVersion file ver exp = when (ver /= exp) (throw $ TTCError $ Format file ver exp) -public export record TTCFile extra where constructor MkTTCFile version : Int @@ -221,7 +220,6 @@ writeTTCFile b file_in toBuf (transforms file) toBuf (foreignExports file) -export readTTCFile : TTC extra => {auto c : Ref Ctxt Defs} -> Bool -> String -> Maybe (Namespace) -> @@ -341,7 +339,6 @@ writeToTTC extradata sourceFileName ttcFileName | Left err => throw (InternalError (ttcFileName ++ ": " ++ show err)) pure () -export addGlobalDef : {auto c : Ref Ctxt Defs} -> (modns : ModuleIdent) -> Namespace -> (importAs : Maybe Namespace) -> diff --git a/src/Idris/REPL/IDEIndex.idr b/src/Idris/REPL/IDEIndex.idr index edb04895d4a..2410207d58b 100644 --- a/src/Idris/REPL/IDEIndex.idr +++ b/src/Idris/REPL/IDEIndex.idr @@ -4,6 +4,7 @@ import Core.Binary import Core.Core import Core.Context import Core.Name.Namespace +import Core.UnifyState import Data.String import Idris.Syntax import Idris.Syntax.TTC @@ -23,25 +24,28 @@ record IDEIndex where constructor MkIDEIndex indexedDefs : List IndexedDef -findFiles : (String -> Bool) -> String -> Core (List String) -findFiles pred dir = do - Right list <- coreLift $ listDir dir - | Left _ => pure [] - let list = (dir ) <$> filter (\f => not $ f == "." || f == "..") list - concat <$> traverse go list +||| Recursively finds all TTC files in the given directory and returns +||| their full paths along with their corresponding namespaces. +findTtcFiles : String -> Core (List (String, Namespace)) +findTtcFiles dir = go dir (mkNamespace "") where - go : String -> Core (List String) - go file = do - if pred file - then pure [file] - else findFiles pred file + mkItem : String -> Namespace -> String -> (String, Namespace) + mkItem dir ns f + = ( dir f + , maybe ns (mkNestedNamespace (Just ns)) (fileStem f) + ) -readTtcFile : Ref Ctxt Defs => String -> Core (TTCFile SyntaxInfo) -readTtcFile fname = do - Right buffer <- coreLift $ readFromFile fname - | Left err => throw (InternalError (fname ++ ": " ++ show err)) - bin <- newRef Bin buffer -- for reading the file into - readTTCFile True fname Nothing bin + go : String -> Namespace -> Core (List (String, Namespace)) + go dir ns = do + Right entries <- coreLift $ listDir dir + | Left _ => pure [] + let entries = filter (\f => not $ f == "." || f == "..") entries + let ttcFiles = mkItem dir ns <$> filter (".ttc" `isSuffixOf`) entries + let subdirs = filter (not . isInfixOf ".") entries + subdirFiles <- concat <$> traverse + (\dir' => go (dir dir') (mkNestedNamespace (Just ns) dir')) + subdirs + pure $ ttcFiles ++ subdirFiles defIfVisible : Ref Ctxt Defs => Name -> Core (Maybe GlobalDef) defIfVisible nsn = do @@ -54,13 +58,20 @@ defIfVisible nsn = do then pure (Just def) else pure Nothing -indexDefsOfTtc : String -> Core (List IndexedDef) -indexDefsOfTtc ttcFile = do +indexDefsOfTtc : (String, Namespace) -> Core (List IndexedDef) +indexDefsOfTtc (ttcFile, ttcModNS) = do _ <- newRef Ctxt !initDefs - ttc <- readTtcFile ttcFile - let ttcModNS = currentNS ttc + _ <- newRef UST initUState + Just (syntaxInfo, _, imports) <- readFromTTC {extra = SyntaxInfo} + False -- don't set nested namespaces (irrelevant for us) + EmptyFC + False -- don't import as public (irrelevant to us) + ttcFile -- file to read + (nsAsModuleIdent ttcModNS) -- module identifier + (ttcModNS) -- "importAs" (irrelevant to us) + | Nothing => pure [] + modNS <- nsAsModuleIdent <$> getNS - traverse_ (addGlobalDef modNS ttcModNS Nothing) (context ttc) names <- filter (isJust . userNameRoot) <$> allNames (gamma !(get Ctxt)) visibleDefs <- mapMaybeM defIfVisible names pure $ MkIndexedDef ttcModNS <$> visibleDefs @@ -70,8 +81,6 @@ export mkIdeIndex : List String -> Core IDEIndex mkIdeIndex pkg_dirs = do let pkgTtcDirs = pkg_dirs <&> ( show ttcVersion) - pkgTtcFiles <- concat <$> traverse (findFiles $ isSuffixOf ".ttc") pkgTtcDirs + pkgTtcFiles <- concat <$> traverse findTtcFiles pkgTtcDirs indexedDefs <- concat <$> traverse indexDefsOfTtc pkgTtcFiles pure $ MkIDEIndex indexedDefs - - \ No newline at end of file diff --git a/src/TTImp/Interactive/Completion.idr b/src/TTImp/Interactive/Completion.idr index f5f4b18c3e9..304eb7cd2cc 100644 --- a/src/TTImp/Interactive/Completion.idr +++ b/src/TTImp/Interactive/Completion.idr @@ -86,11 +86,6 @@ nameCompletion pref = do unqualName : Name -> String unqualName = nameRoot . snd . splitNS - moduleOf : GlobalDef -> String - moduleOf d = let n = fullname d in case n of - NS ns _ => show ns - otherwise => "" - autoImport : IndexedDef -> Completion autoImport d = autoImportCompletion (unqualName $ fullname $ def d) (show $ moduleNS d) From 1dbb43cf47a7719e9cffbd938717ef3099415feb Mon Sep 17 00:00:00 2001 From: arash Date: Sun, 7 Sep 2025 12:51:10 +0200 Subject: [PATCH 5/7] when completion symbols, suggest all modules that reexport it --- src/Idris/Driver.idr | 2 +- src/Idris/REPL/IDEIndex.idr | 40 +++++++++++++++++++++++----- src/TTImp/Interactive/Completion.idr | 16 ++++++++--- 3 files changed, 47 insertions(+), 11 deletions(-) diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index 780ce43840f..80a1326280c 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -169,7 +169,7 @@ stMain cgs opts """ update ROpts { mainfile := fname } if ideIndex - then update ROpts { ideIndex := Just (MkIDEIndex []) } + then update ROpts { ideIndex := Just initIDEIndex } else pure () -- start by going over the pre-options, and stop if we do not need to diff --git a/src/Idris/REPL/IDEIndex.idr b/src/Idris/REPL/IDEIndex.idr index 2410207d58b..77cd6d950a4 100644 --- a/src/Idris/REPL/IDEIndex.idr +++ b/src/Idris/REPL/IDEIndex.idr @@ -12,17 +12,32 @@ import Libraries.Data.WithDefault import Libraries.Utils.Path import System.Directory +||| An exported definition along with the module namespace it comes from. public export record IndexedDef where constructor MkIndexedDef moduleNS : Namespace def : GlobalDef +public export +||| Expresses one module re-exporting another module as a given namespace: +||| (reexporting module, reexported module, as namespace) +ReExport : Type +ReExport = (ModuleIdent, ModuleIdent, Namespace) + ||| An index of exported definitions from modules of available packages. public export record IDEIndex where constructor MkIDEIndex + ||| All exported definitions along with the module they come from. indexedDefs : List IndexedDef + ||| All re-exports that are happening between modules. + ||| Useful for things like auto-importing completions. + reexports : List ReExport + +export +initIDEIndex : IDEIndex +initIDEIndex = MkIDEIndex [] [] ||| Recursively finds all TTC files in the given directory and returns ||| their full paths along with their corresponding namespaces. @@ -47,6 +62,8 @@ findTtcFiles dir = go dir (mkNamespace "") subdirs pure $ ttcFiles ++ subdirFiles +||| If the given name is visible in the current context, +||| returns the corresponding definition. defIfVisible : Ref Ctxt Defs => Name -> Core (Maybe GlobalDef) defIfVisible nsn = do defs <- get Ctxt @@ -58,8 +75,10 @@ defIfVisible nsn = do then pure (Just def) else pure Nothing -indexDefsOfTtc : (String, Namespace) -> Core (List IndexedDef) +indexDefsOfTtc : (String, Namespace) -> Core (List IndexedDef, List ReExport) indexDefsOfTtc (ttcFile, ttcModNS) = do + let ttcModId = nsAsModuleIdent ttcModNS + _ <- newRef Ctxt !initDefs _ <- newRef UST initUState Just (syntaxInfo, _, imports) <- readFromTTC {extra = SyntaxInfo} @@ -67,14 +86,21 @@ indexDefsOfTtc (ttcFile, ttcModNS) = do EmptyFC False -- don't import as public (irrelevant to us) ttcFile -- file to read - (nsAsModuleIdent ttcModNS) -- module identifier - (ttcModNS) -- "importAs" (irrelevant to us) - | Nothing => pure [] + ttcModId -- module identifier + ttcModNS -- "importAs" (irrelevant to us) + | Nothing => pure ([], []) + + let reexports = mapMaybe + (\(impModId, pub, as) => if pub + then Just (ttcModId, impModId, as) + else Nothing) + imports modNS <- nsAsModuleIdent <$> getNS names <- filter (isJust . userNameRoot) <$> allNames (gamma !(get Ctxt)) visibleDefs <- mapMaybeM defIfVisible names - pure $ MkIndexedDef ttcModNS <$> visibleDefs + + pure $ (MkIndexedDef ttcModNS <$> visibleDefs, reexports) ||| Builds an IDE index from all TTC files found in the given package directories. export @@ -82,5 +108,5 @@ mkIdeIndex : List String -> Core IDEIndex mkIdeIndex pkg_dirs = do let pkgTtcDirs = pkg_dirs <&> ( show ttcVersion) pkgTtcFiles <- concat <$> traverse findTtcFiles pkgTtcDirs - indexedDefs <- concat <$> traverse indexDefsOfTtc pkgTtcFiles - pure $ MkIDEIndex indexedDefs + (indexedDefs, reexports) <- concat <$> traverse indexDefsOfTtc pkgTtcFiles + pure $ MkIDEIndex indexedDefs reexports diff --git a/src/TTImp/Interactive/Completion.idr b/src/TTImp/Interactive/Completion.idr index 304eb7cd2cc..85198795fa5 100644 --- a/src/TTImp/Interactive/Completion.idr +++ b/src/TTImp/Interactive/Completion.idr @@ -79,15 +79,25 @@ nameCompletion pref = do | Nothing => pure ctxCompletions let idxDefs = filter (validCompletion . fullname . def) $ indexedDefs ideIndex let idxUnseenDefs = filter (not . (`elem` ctxtVisibleNames) . fullname . def) idxDefs - let idxCompletions = autoImport <$> idxUnseenDefs + let idxCompletions = concat $ autoImport (reexports ideIndex) <$> idxUnseenDefs pure (ctxCompletions ++ idxCompletions) where + ||| The actual string that would be pasted at the completion site. unqualName : Name -> String unqualName = nameRoot . snd . splitNS - autoImport : IndexedDef -> Completion - autoImport d = autoImportCompletion (unqualName $ fullname $ def d) (show $ moduleNS d) + ||| If a module is re-exported by another module, suggest both modules as auto-imports. + unfoldReExports : ModuleIdent -> List ReExport -> List ReExport -> List ModuleIdent + unfoldReExports modId orig [] = [modId] + unfoldReExports modId orig ((to, from, as) :: rest) = if modId == from + then (unfoldReExports to orig orig) ++ (unfoldReExports modId orig rest) + else unfoldReExports modId orig rest + + + autoImport : List ReExport -> IndexedDef -> List Completion + autoImport reexps d = unfoldReExports (nsAsModuleIdent $ moduleNS d) reexps reexps + <&> (\m => autoImportCompletion (unqualName $ fullname $ def d) (show m)) validIdentifier : String -> Bool validIdentifier = all (\c => isAlphaNum c || c == '_' || c == '.' || c > chr 160) . unpack From 275d1dd99ac4e3fe061805a86d34f3f1fb7e657a Mon Sep 17 00:00:00 2001 From: arash Date: Sun, 7 Sep 2025 13:20:05 +0200 Subject: [PATCH 6/7] minor cleanup --- src/Idris/Driver.idr | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index 80a1326280c..a1a359275af 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -155,6 +155,7 @@ stMain cgs opts let ide = ideMode opts || (ideIndex && not ideSocket) let outmode = if ide then IDEMode 0 stdin stdout else REPL InfoLvl o <- newRef ROpts (REPL.Opts.defaultOpts Nothing outmode cgs) + when ideIndex $ update ROpts { ideIndex := Just initIDEIndex } updateEnv fname <- case (findInputs opts) of Just (fname ::: Nil) => pure $ Just fname @@ -168,9 +169,6 @@ stMain cgs opts \{renderedSuggestion} """ update ROpts { mainfile := fname } - if ideIndex - then update ROpts { ideIndex := Just initIDEIndex } - else pure () -- start by going over the pre-options, and stop if we do not need to -- continue From 1cd6d1147354f9ed9475a20c01ea634e31bc60a6 Mon Sep 17 00:00:00 2001 From: arash Date: Mon, 8 Sep 2025 19:48:16 +0200 Subject: [PATCH 7/7] remove trailing whitespace, add ide-index module to idris2api.ipkg --- idris2api.ipkg | 3 ++- src/Idris/REPL/IDEIndex.idr | 2 +- src/TTImp/Interactive/Completion.idr | 1 - 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/idris2api.ipkg b/idris2api.ipkg index 2b767b1fa28..d601e3da676 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -165,8 +165,9 @@ modules = Idris.IDEMode.TokenLine, Idris.REPL.Common, - Idris.REPL.Opts, Idris.REPL.FuzzySearch, + Idris.REPL.IDEIndex, + Idris.REPL.Opts, Libraries.Control.ANSI, Libraries.Control.ANSI.CSI, diff --git a/src/Idris/REPL/IDEIndex.idr b/src/Idris/REPL/IDEIndex.idr index 77cd6d950a4..2da00c9af83 100644 --- a/src/Idris/REPL/IDEIndex.idr +++ b/src/Idris/REPL/IDEIndex.idr @@ -90,7 +90,7 @@ indexDefsOfTtc (ttcFile, ttcModNS) = do ttcModNS -- "importAs" (irrelevant to us) | Nothing => pure ([], []) - let reexports = mapMaybe + let reexports = mapMaybe (\(impModId, pub, as) => if pub then Just (ttcModId, impModId, as) else Nothing) diff --git a/src/TTImp/Interactive/Completion.idr b/src/TTImp/Interactive/Completion.idr index 85198795fa5..707a19f13fb 100644 --- a/src/TTImp/Interactive/Completion.idr +++ b/src/TTImp/Interactive/Completion.idr @@ -94,7 +94,6 @@ nameCompletion pref = do then (unfoldReExports to orig orig) ++ (unfoldReExports modId orig rest) else unfoldReExports modId orig rest - autoImport : List ReExport -> IndexedDef -> List Completion autoImport reexps d = unfoldReExports (nsAsModuleIdent $ moduleNS d) reexps reexps <&> (\m => autoImportCompletion (unqualName $ fullname $ def d) (show m))