Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions CHANGELOG_NEXT.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
1 change: 1 addition & 0 deletions CONTRIBUTORS
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ George Pollard
GhiOm
Giuseppe Lomurno
Guillaume Allais
Hakan Aras
Hiroki Hattori
Ilya Rezvov
Jacob Walters
Expand Down
3 changes: 2 additions & 1 deletion idris2api.ipkg
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
4 changes: 4 additions & 0 deletions src/Idris/CommandLine.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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])
Expand Down
5 changes: 4 additions & 1 deletion src/Idris/Driver.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -149,10 +150,12 @@ 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)
when ideIndex $ update ROpts { ideIndex := Just initIDEIndex }
updateEnv
fname <- case (findInputs opts) of
Just (fname ::: Nil) => pure $ Just fname
Expand Down
15 changes: 13 additions & 2 deletions src/Idris/IDEMode/REPL.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down
112 changes: 112 additions & 0 deletions src/Idris/REPL/IDEIndex.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,112 @@
module Idris.REPL.IDEIndex

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
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.
findTtcFiles : String -> Core (List (String, Namespace))
findTtcFiles dir = go dir (mkNamespace "")
where
mkItem : String -> Namespace -> String -> (String, Namespace)
mkItem dir ns f
= ( dir </> f
, maybe ns (mkNestedNamespace (Just ns)) (fileStem f)
)

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

||| 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
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

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}
False -- don't set nested namespaces (irrelevant for us)
EmptyFC
False -- don't import as public (irrelevant to us)
ttcFile -- file to read
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, reexports)

||| 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 findTtcFiles pkgTtcDirs
(indexedDefs, reexports) <- concat <$> traverse indexDefsOfTtc pkgTtcFiles
pure $ MkIDEIndex indexedDefs reexports
4 changes: 4 additions & 0 deletions src/Idris/REPL/Opts.idr
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module Idris.REPL.Opts

import Compiler.Common
import Idris.REPL.IDEIndex
import Idris.Syntax
import Parser.Unlit
import TTImp.TTImp
Expand Down Expand Up @@ -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
Expand All @@ -78,6 +81,7 @@ defaultOpts fname outmode cgs
, gdResult = Nothing
, evalResultName = Nothing
, extraCodegens = cgs
, ideIndex = Nothing
, consoleWidth = Nothing
, color = True
, synHighlightOn = True
Expand Down
9 changes: 9 additions & 0 deletions src/Idris/SetOptions.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
19 changes: 17 additions & 2 deletions src/Protocol/IDE/Result.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand All @@ -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

Expand Down
Loading