From 8dba10b48c2bf0a17b114f70e92921fef7aa018c Mon Sep 17 00:00:00 2001 From: nvarner Date: Mon, 4 Aug 2025 15:33:10 -0700 Subject: [PATCH 01/23] typo: consumer --- src/Monad.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Monad.hs b/src/Monad.hs index 3726b86..563c340 100644 --- a/src/Monad.hs +++ b/src/Monad.hs @@ -78,7 +78,7 @@ provideCommand iotcm = do controller <- asks envCommandController liftIO $ CommandController.put controller iotcm --- | Consumter +-- | Consumer consumeCommand :: (Monad m, MonadIO m) => Env -> m IOTCM consumeCommand env = liftIO $ CommandController.take (envCommandController env) From 2c5a2f2be58365d0a0c184e87131508a2bb1644e Mon Sep 17 00:00:00 2001 From: nvarner Date: Mon, 4 Aug 2025 18:43:45 -0700 Subject: [PATCH 02/23] set up basic indexing infrastructure --- agda-language-server.cabal | 10 ++++++ src/Language/LSP/Protocol/Types/Uri/More.hs | 16 ++++++++++ src/Monad.hs | 7 ++++- src/Server/Model.hs | 15 +++++++++ src/Server/Model/AgdaFile.hs | 10 ++++++ src/Server/Model/AgdaLib.hs | 25 +++++++++++++++ src/Server/Model/Symbol.hs | 34 +++++++++++++++++++++ 7 files changed, 116 insertions(+), 1 deletion(-) create mode 100644 src/Language/LSP/Protocol/Types/Uri/More.hs create mode 100644 src/Server/Model.hs create mode 100644 src/Server/Model/AgdaFile.hs create mode 100644 src/Server/Model/AgdaLib.hs create mode 100644 src/Server/Model/Symbol.hs diff --git a/agda-language-server.cabal b/agda-language-server.cabal index 378b857..d5add18 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -53,6 +53,7 @@ library Agda.Parser Agda.Position Control.Concurrent.SizedChan + Language.LSP.Protocol.Types.Uri.More Monad Options Render @@ -70,6 +71,10 @@ library Server Server.CommandController Server.Handler + Server.Model + Server.Model.AgdaFile + Server.Model.AgdaLib + Server.Model.Symbol Server.ResponseController Switchboard other-modules: @@ -177,6 +182,7 @@ test-suite als-test Agda.Parser Agda.Position Control.Concurrent.SizedChan + Language.LSP.Protocol.Types.Uri.More Monad Options Render @@ -194,6 +200,10 @@ test-suite als-test Server Server.CommandController Server.Handler + Server.Model + Server.Model.AgdaFile + Server.Model.AgdaLib + Server.Model.Symbol Server.ResponseController Switchboard Paths_agda_language_server diff --git a/src/Language/LSP/Protocol/Types/Uri/More.hs b/src/Language/LSP/Protocol/Types/Uri/More.hs new file mode 100644 index 0000000..efadd4b --- /dev/null +++ b/src/Language/LSP/Protocol/Types/Uri/More.hs @@ -0,0 +1,16 @@ +module Language.LSP.Protocol.Types.Uri.More (isUriAncestorOf) where + +import Data.Text (Text) +import qualified Data.Text as Text +import qualified Language.LSP.Protocol.Types as LSP + +getNormalizedUri :: LSP.NormalizedUri -> Text +getNormalizedUri = LSP.getUri . LSP.fromNormalizedUri + +-- | Determine if the first URI is an ancestor of the second. +-- +-- This is a heuristic implementation and may need replacement if the heuristic +-- leads to bugs. +isUriAncestorOf :: LSP.NormalizedUri -> LSP.NormalizedUri -> Bool +isUriAncestorOf ancestor descendant = + getNormalizedUri ancestor `Text.isPrefixOf` getNormalizedUri descendant diff --git a/src/Monad.hs b/src/Monad.hs index 563c340..a798201 100644 --- a/src/Monad.hs +++ b/src/Monad.hs @@ -28,6 +28,9 @@ import Language.LSP.Server import Options import Server.CommandController (CommandController) import qualified Server.CommandController as CommandController +import Server.Model (Model) +import qualified Server.Model as Model +import Server.Model.AgdaLib (AgdaLib) import Server.ResponseController (ResponseController) import qualified Server.ResponseController as ResponseController @@ -40,7 +43,8 @@ data Env = Env envLogChan :: Chan Text, envCommandController :: CommandController, envResponseChan :: Chan Response, - envResponseController :: ResponseController + envResponseController :: ResponseController, + envModel :: !(IORef Model) } createInitEnv :: (MonadIO m, MonadLsp Config m) => Options -> m Env @@ -51,6 +55,7 @@ createInitEnv options = <*> liftIO CommandController.new <*> liftIO newChan <*> liftIO ResponseController.new + <*> liftIO (newIORef Model.empty) -------------------------------------------------------------------------------- diff --git a/src/Server/Model.hs b/src/Server/Model.hs new file mode 100644 index 0000000..90ae171 --- /dev/null +++ b/src/Server/Model.hs @@ -0,0 +1,15 @@ +module Server.Model (Model, empty) where + +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Language.LSP.Protocol.Types as LSP +import Server.Model.AgdaFile (AgdaFile) +import Server.Model.AgdaLib (AgdaLib) + +data Model = Model + { _modelAgdaLibs :: !([AgdaLib]), + _modelAgdaFiles :: !(Map LSP.Uri AgdaFile) + } + +empty :: Model +empty = Model [] Map.empty diff --git a/src/Server/Model/AgdaFile.hs b/src/Server/Model/AgdaFile.hs new file mode 100644 index 0000000..ce4d52c --- /dev/null +++ b/src/Server/Model/AgdaFile.hs @@ -0,0 +1,10 @@ +module Server.Model.AgdaFile (AgdaFile) where + +import qualified Agda.Syntax.Abstract as A +import Data.Map (Map) +import Server.Model.Symbol (Ref, SymbolInfo) + +data AgdaFile = AgdaFile + { _agdaFileSymbols :: !(Map A.QName SymbolInfo), + _agdaFileRefs :: !(Map A.QName [Ref]) + } diff --git a/src/Server/Model/AgdaLib.hs b/src/Server/Model/AgdaLib.hs new file mode 100644 index 0000000..d65a78d --- /dev/null +++ b/src/Server/Model/AgdaLib.hs @@ -0,0 +1,25 @@ +module Server.Model.AgdaLib + ( AgdaLib, + isAgdaLibForUri, + ) +where + +import qualified Agda.TypeChecking.Monad as TCM +import Agda.Utils.IORef (IORef) +import Agda.Utils.Lens (Lens', (<&>), (^.)) +import Data.Map (Map) +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Protocol.Types.Uri.More as LSP +import Server.Model.AgdaFile (AgdaFile) + +data AgdaLib = AgdaLib + { _agdaLibIncludes :: ![LSP.NormalizedUri], + _agdaLibTcState :: !(IORef TCM.TCState), + _agdaLibTcEnv :: !TCM.TCEnv + } + +agdaLibIncludes :: Lens' AgdaLib [LSP.NormalizedUri] +agdaLibIncludes f a = f (_agdaLibIncludes a) <&> \x -> a {_agdaLibIncludes = x} + +isAgdaLibForUri :: AgdaLib -> LSP.NormalizedUri -> Bool +isAgdaLibForUri agdaLib uri = any (`LSP.isUriAncestorOf` uri) (agdaLib ^. agdaLibIncludes) diff --git a/src/Server/Model/Symbol.hs b/src/Server/Model/Symbol.hs new file mode 100644 index 0000000..5506f15 --- /dev/null +++ b/src/Server/Model/Symbol.hs @@ -0,0 +1,34 @@ +module Server.Model.Symbol (SymbolInfo, Ref) where + +import qualified Agda.Syntax.Abstract as A +import Agda.Syntax.Position (Position, PositionWithoutFile) +import qualified Language.LSP.Protocol.Types as LSP + +data SymbolKind + = Con + | CoCon + | Field + | PatternSyn + | GeneralizeVar + | Macro + | Data + | Record + | Fun + | Axiom + | Prim + | Module + | Param + | Local + | Unknown + deriving (Show) + +data SymbolInfo = SymbolInfo + { _symbolKind :: !SymbolKind, + _symbolType :: !(Maybe String), + _symbolParent :: !(Maybe A.QName) + } + +data Ref = Ref + { _refSymbol :: !A.QName, + _refRange :: !LSP.Range + } From 2c0a0bf1f61c9e1532ff998009e7aeb1c5fc1df7 Mon Sep 17 00:00:00 2001 From: nvarner Date: Wed, 6 Aug 2025 18:52:43 -0700 Subject: [PATCH 03/23] look up indexed file to handle requests --- agda-language-server.cabal | 7 + src/Language/LSP/Protocol/Types/Uri/More.hs | 6 +- src/Monad.hs | 7 + src/Options.hs | 1 + src/Server.hs | 2 +- src/Server/Handler/Monad.hs | 176 ++++++++++++++++++ .../Handler/TextDocument/DocumentSymbol.hs | 18 ++ src/Server/Model.hs | 17 +- src/Server/Model/AgdaFile.hs | 15 +- src/Server/Model/AgdaLib.hs | 23 ++- test/Test.hs | 6 +- test/Test/HandlerMonad.hs | 92 +++++++++ test/Test/Model.hs | 59 ++++++ test/TestData.hs | 80 ++++++++ 14 files changed, 499 insertions(+), 10 deletions(-) create mode 100644 src/Server/Handler/Monad.hs create mode 100644 src/Server/Handler/TextDocument/DocumentSymbol.hs create mode 100644 test/Test/HandlerMonad.hs create mode 100644 test/Test/Model.hs create mode 100644 test/TestData.hs diff --git a/agda-language-server.cabal b/agda-language-server.cabal index d5add18..7b83d61 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -71,6 +71,8 @@ library Server Server.CommandController Server.Handler + Server.Handler.Monad + Server.Handler.TextDocument.DocumentSymbol Server.Model Server.Model.AgdaFile Server.Model.AgdaLib @@ -173,9 +175,12 @@ test-suite als-test type: exitcode-stdio-1.0 main-is: Test.hs other-modules: + Test.HandlerMonad Test.LSP + Test.Model Test.SrcLoc Test.WASM + TestData Agda Agda.Convert Agda.IR @@ -200,6 +205,8 @@ test-suite als-test Server Server.CommandController Server.Handler + Server.Handler.Monad + Server.Handler.TextDocument.DocumentSymbol Server.Model Server.Model.AgdaFile Server.Model.AgdaLib diff --git a/src/Language/LSP/Protocol/Types/Uri/More.hs b/src/Language/LSP/Protocol/Types/Uri/More.hs index efadd4b..f8c1b69 100644 --- a/src/Language/LSP/Protocol/Types/Uri/More.hs +++ b/src/Language/LSP/Protocol/Types/Uri/More.hs @@ -1,4 +1,8 @@ -module Language.LSP.Protocol.Types.Uri.More (isUriAncestorOf) where +module Language.LSP.Protocol.Types.Uri.More + ( getNormalizedUri, + isUriAncestorOf, + ) +where import Data.Text (Text) import qualified Data.Text as Text diff --git a/src/Monad.hs b/src/Monad.hs index a798201..ff0d346 100644 --- a/src/Monad.hs +++ b/src/Monad.hs @@ -1,11 +1,13 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE RankNTypes #-} module Monad where import Agda.IR import Agda.Interaction.Base (IOTCM) import Agda.TypeChecking.Monad (TCMT) +import Agda.Utils.Lens (Lens', (^.)) import Control.Concurrent import Control.Monad.Reader import Data.IORef @@ -77,6 +79,11 @@ writeLog' x = do chan <- asks envLogChan liftIO $ writeChan chan $ pack $ show x +askModel :: (MonadIO m) => ServerM m Model +askModel = do + modelVar <- asks envModel + liftIO $ readIORef modelVar + -- | Provider provideCommand :: (Monad m, MonadIO m) => IOTCM -> ServerM m () provideCommand iotcm = do diff --git a/src/Options.hs b/src/Options.hs index 27742d5..b5c3808 100644 --- a/src/Options.hs +++ b/src/Options.hs @@ -3,6 +3,7 @@ module Options ( Options (..), + defaultOptions, getOptionsFromArgv, versionNumber, versionString, diff --git a/src/Server.hs b/src/Server.hs index df833f4..db8cfbb 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -81,7 +81,7 @@ run options = do } lspOptions :: LSP.Options -lspOptions = defaultOptions {optTextDocumentSync = Just syncOptions} +lspOptions = LSP.defaultOptions {optTextDocumentSync = Just syncOptions} -- these `TextDocumentSyncOptions` are essential for receiving notifications from the client -- syncOptions :: TextDocumentSyncOptions diff --git a/src/Server/Handler/Monad.hs b/src/Server/Handler/Monad.hs new file mode 100644 index 0000000..863060b --- /dev/null +++ b/src/Server/Handler/Monad.hs @@ -0,0 +1,176 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} + +module Server.Handler.Monad + ( MonadAgdaLib (..), + useAgdaLib, + MonadAgdaFile (..), + useAgdaFile, + withAgdaFile, + ) +where + +import Agda.Interaction.Options (CommandLineOptions (optPragmaOptions), PragmaOptions) +import Agda.TypeChecking.Monad (HasOptions (..), MonadTCEnv (..), MonadTCM (..), MonadTCState (..), PersistentTCState (stPersistentOptions), ReadTCState (..), TCEnv, TCM, TCMT (..), TCState (stPersistentState), modifyTCLens, setTCLens, stPragmaOptions, useTC) +import Agda.Utils.IORef (modifyIORef', readIORef, writeIORef) +import Agda.Utils.Lens (Lens', locally, over, use, view, (<&>), (^.)) +import Agda.Utils.Monad (bracket_) +import Control.Monad.IO.Class (MonadIO (liftIO)) +import Control.Monad.Reader (MonadReader (local), ReaderT (runReaderT), asks) +import Control.Monad.Trans (MonadTrans, lift) +import qualified Language.LSP.Protocol.Lens as LSP +import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Protocol.Types.Uri.More as LSP +import Language.LSP.Server (LspM) +import qualified Language.LSP.Server as LSP +import Monad (ServerM, askModel) +import Options (Config) +import qualified Server.Model as Model +import Server.Model.AgdaFile (AgdaFile) +import Server.Model.AgdaLib (AgdaLib, agdaLibTcEnv, agdaLibTcStateRef) + +-------------------------------------------------------------------------------- + +class (MonadTCM m, ReadTCState m) => MonadAgdaLib m where + askAgdaLib :: m AgdaLib + localAgdaLib :: (AgdaLib -> AgdaLib) -> m a -> m a + +useAgdaLib :: (MonadAgdaLib m) => Lens' AgdaLib a -> m a +useAgdaLib lens = do + agdaLib <- askAgdaLib + return $ agdaLib ^. lens + +class (MonadAgdaLib m) => MonadAgdaFile m where + askAgdaFile :: m AgdaFile + localAgdaFile :: (AgdaFile -> AgdaFile) -> m a -> m a + +useAgdaFile :: (MonadAgdaFile m) => Lens' AgdaFile a -> m a +useAgdaFile lens = do + agdaFile <- askAgdaFile + return $ agdaFile ^. lens + +-------------------------------------------------------------------------------- + +defaultAskTC :: (MonadAgdaLib m) => m TCEnv +defaultAskTC = useAgdaLib agdaLibTcEnv + +defaultLocalTC :: (MonadAgdaLib m) => (TCEnv -> TCEnv) -> m a -> m a +defaultLocalTC f = localAgdaLib (over agdaLibTcEnv f) + +defaultGetTC :: (MonadAgdaLib m) => m TCState +defaultGetTC = do + tcStateRef <- useAgdaLib agdaLibTcStateRef + liftIO $ readIORef tcStateRef + +defaultPutTC :: (MonadAgdaLib m) => TCState -> m () +defaultPutTC tcState = do + tcStateRef <- useAgdaLib agdaLibTcStateRef + liftIO $ writeIORef tcStateRef tcState + +defaultModifyTC :: (MonadAgdaLib m) => (TCState -> TCState) -> m () +defaultModifyTC f = do + tcStateRef <- useAgdaLib agdaLibTcStateRef + liftIO $ modifyIORef' tcStateRef f + +-- Taken from TCMT implementation +defaultLocallyTCState :: (MonadAgdaLib m) => Lens' TCState a -> (a -> a) -> m b -> m b +defaultLocallyTCState lens f = bracket_ (useTC lens <* modifyTCLens lens f) (setTCLens lens) + +-- Taken from TCMT implementation +defaultPragmaOptionsImpl :: (MonadAgdaLib m) => m PragmaOptions +defaultPragmaOptionsImpl = useTC stPragmaOptions + +-- Taken from TCMT implementation +defaultCommandLineOptionsImpl :: (MonadAgdaLib m) => m CommandLineOptions +defaultCommandLineOptionsImpl = do + p <- useTC stPragmaOptions + cl <- stPersistentOptions . stPersistentState <$> getTC + return $ cl {optPragmaOptions = p} + +defaultLiftTCM :: (MonadAgdaLib m) => TCM a -> m a +defaultLiftTCM (TCM f) = do + tcStateRef <- useAgdaLib agdaLibTcStateRef + tcEnv <- useAgdaLib agdaLibTcEnv + liftIO $ f tcStateRef tcEnv + +-------------------------------------------------------------------------------- + +data WithAgdaFileEnv = WithAgdaFileEnv + { _withAgdaFileEnvAgdaLib :: !AgdaLib, + _withAgdaFileEnvAgdaFile :: !AgdaFile + } + +withAgdaFileEnvAgdaLib :: Lens' WithAgdaFileEnv AgdaLib +withAgdaFileEnvAgdaLib f a = f (_withAgdaFileEnvAgdaLib a) <&> \x -> a {_withAgdaFileEnvAgdaLib = x} + +withAgdaFileEnvAgdaFile :: Lens' WithAgdaFileEnv AgdaFile +withAgdaFileEnvAgdaFile f a = f (_withAgdaFileEnvAgdaFile a) <&> \x -> a {_withAgdaFileEnvAgdaFile = x} + +newtype WithAgdaFileT m a = WithAgdaFileT + {unWithAgdaFileT :: ReaderT WithAgdaFileEnv m a} + deriving (Functor, Applicative, Monad, MonadIO, MonadTrans) + +runWithAgdaFileT :: AgdaLib -> AgdaFile -> WithAgdaFileT m a -> m a +runWithAgdaFileT agdaLib agdaFile = + let env = WithAgdaFileEnv agdaLib agdaFile + in flip runReaderT env . unWithAgdaFileT + +type WithAgdaFileM = WithAgdaFileT (ServerM (LspM Config)) + +type HandlerWithAgdaFile m = + LSP.TRequestMessage m -> + (Either (LSP.TResponseError m) (LSP.MessageResult m) -> WithAgdaFileM ()) -> + WithAgdaFileM () + +withAgdaFile :: + forall (m :: LSP.Method LSP.ClientToServer LSP.Request). + (LSP.HasTextDocument (LSP.MessageParams m) LSP.TextDocumentIdentifier) => + LSP.SMethod m -> + HandlerWithAgdaFile m -> + LSP.Handlers (ServerM (LspM Config)) +withAgdaFile m handler = LSP.requestHandler m $ \req responder -> do + let uri = req ^. LSP.params . LSP.textDocument . LSP.uri + normUri = LSP.toNormalizedUri uri + + model <- askModel + case Model.getAgdaFile normUri model of + Nothing -> do + let message = "Request for unknown Agda file at URI: " <> LSP.getUri uri + responder $ Left $ LSP.TResponseError (LSP.InR LSP.ErrorCodes_InvalidParams) message Nothing + Just agdaFile -> do + agdaLib <- Model.getAgdaLib normUri model + let responder' = lift . responder + runWithAgdaFileT agdaLib agdaFile $ handler req responder' + +instance (MonadIO m) => MonadAgdaLib (WithAgdaFileT m) where + askAgdaLib = WithAgdaFileT $ view withAgdaFileEnvAgdaLib + localAgdaLib f = WithAgdaFileT . locally withAgdaFileEnvAgdaLib f . unWithAgdaFileT + +instance (MonadIO m) => MonadAgdaFile (WithAgdaFileT m) where + askAgdaFile = WithAgdaFileT $ view withAgdaFileEnvAgdaFile + localAgdaFile f = WithAgdaFileT . locally withAgdaFileEnvAgdaFile f . unWithAgdaFileT + +instance (MonadIO m) => MonadTCEnv (WithAgdaFileT m) where + askTC = defaultAskTC + localTC = defaultLocalTC + +instance (MonadIO m) => MonadTCState (WithAgdaFileT m) where + getTC = defaultGetTC + putTC = defaultPutTC + modifyTC = defaultModifyTC + +instance (MonadIO m) => ReadTCState (WithAgdaFileT m) where + getTCState = defaultGetTC + locallyTCState = defaultLocallyTCState + +instance (MonadIO m) => HasOptions (WithAgdaFileT m) where + pragmaOptions = defaultPragmaOptionsImpl + commandLineOptions = defaultCommandLineOptionsImpl + +instance (MonadIO m) => MonadTCM (WithAgdaFileT m) where + liftTCM = defaultLiftTCM diff --git a/src/Server/Handler/TextDocument/DocumentSymbol.hs b/src/Server/Handler/TextDocument/DocumentSymbol.hs new file mode 100644 index 0000000..71940b3 --- /dev/null +++ b/src/Server/Handler/TextDocument/DocumentSymbol.hs @@ -0,0 +1,18 @@ +module Server.Handler.TextDocument.DocumentSymbol (documentSymbolHandler) where + +import Agda.Utils.Lens ((^.)) +import qualified Language.LSP.Protocol.Lens as LSP +import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Types as LSP +import Language.LSP.Server (LspM) +import qualified Language.LSP.Server as LSP +import Monad (ServerM) +import Options (Config) +import Server.Handler.Monad (useAgdaFile, withAgdaFile) +import qualified Server.Model as Model +import Server.Model.AgdaFile (agdaFileSymbols) + +documentSymbolHandler :: LSP.Handlers (ServerM (LspM Config)) +documentSymbolHandler = withAgdaFile LSP.SMethod_TextDocumentDocumentSymbol $ \req responder -> do + symbols <- useAgdaFile agdaFileSymbols + return () diff --git a/src/Server/Model.hs b/src/Server/Model.hs index 90ae171..cc11217 100644 --- a/src/Server/Model.hs +++ b/src/Server/Model.hs @@ -1,15 +1,26 @@ -module Server.Model (Model, empty) where +module Server.Model (Model (Model), empty, getKnownAgdaLib, getAgdaLib, getAgdaFile) where +import Control.Monad.IO.Class (MonadIO) +import Data.Foldable (find) import Data.Map (Map) import qualified Data.Map as Map import qualified Language.LSP.Protocol.Types as LSP import Server.Model.AgdaFile (AgdaFile) -import Server.Model.AgdaLib (AgdaLib) +import Server.Model.AgdaLib (AgdaLib, initAgdaLib, isAgdaLibForUri) data Model = Model { _modelAgdaLibs :: !([AgdaLib]), - _modelAgdaFiles :: !(Map LSP.Uri AgdaFile) + _modelAgdaFiles :: !(Map LSP.NormalizedUri AgdaFile) } empty :: Model empty = Model [] Map.empty + +getKnownAgdaLib :: LSP.NormalizedUri -> Model -> Maybe AgdaLib +getKnownAgdaLib uri = find (`isAgdaLibForUri` uri) . _modelAgdaLibs + +getAgdaLib :: (MonadIO m) => LSP.NormalizedUri -> Model -> m AgdaLib +getAgdaLib uri = maybe initAgdaLib return . getKnownAgdaLib uri + +getAgdaFile :: LSP.NormalizedUri -> Model -> Maybe AgdaFile +getAgdaFile uri = Map.lookup uri . _modelAgdaFiles diff --git a/src/Server/Model/AgdaFile.hs b/src/Server/Model/AgdaFile.hs index ce4d52c..afabdc6 100644 --- a/src/Server/Model/AgdaFile.hs +++ b/src/Server/Model/AgdaFile.hs @@ -1,10 +1,23 @@ -module Server.Model.AgdaFile (AgdaFile) where +module Server.Model.AgdaFile + ( AgdaFile, + emptyAgdaFile, + agdaFileSymbols, + ) +where import qualified Agda.Syntax.Abstract as A +import Agda.Utils.Lens (Lens', (<&>)) import Data.Map (Map) +import qualified Data.Map as Map import Server.Model.Symbol (Ref, SymbolInfo) data AgdaFile = AgdaFile { _agdaFileSymbols :: !(Map A.QName SymbolInfo), _agdaFileRefs :: !(Map A.QName [Ref]) } + +emptyAgdaFile :: AgdaFile +emptyAgdaFile = AgdaFile Map.empty Map.empty + +agdaFileSymbols :: Lens' AgdaFile (Map A.QName SymbolInfo) +agdaFileSymbols f a = f (_agdaFileSymbols a) <&> \x -> a {_agdaFileSymbols = x} diff --git a/src/Server/Model/AgdaLib.hs b/src/Server/Model/AgdaLib.hs index d65a78d..24b5df2 100644 --- a/src/Server/Model/AgdaLib.hs +++ b/src/Server/Model/AgdaLib.hs @@ -1,12 +1,17 @@ module Server.Model.AgdaLib - ( AgdaLib, + ( AgdaLib (AgdaLib), + initAgdaLib, + agdaLibIncludes, + agdaLibTcStateRef, + agdaLibTcEnv, isAgdaLibForUri, ) where import qualified Agda.TypeChecking.Monad as TCM -import Agda.Utils.IORef (IORef) +import Agda.Utils.IORef (IORef, newIORef) import Agda.Utils.Lens (Lens', (<&>), (^.)) +import Control.Monad.IO.Class (MonadIO (liftIO)) import Data.Map (Map) import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.Protocol.Types.Uri.More as LSP @@ -14,12 +19,24 @@ import Server.Model.AgdaFile (AgdaFile) data AgdaLib = AgdaLib { _agdaLibIncludes :: ![LSP.NormalizedUri], - _agdaLibTcState :: !(IORef TCM.TCState), + _agdaLibTcStateRef :: !(IORef TCM.TCState), _agdaLibTcEnv :: !TCM.TCEnv } +initAgdaLib :: (MonadIO m) => m AgdaLib +initAgdaLib = do + tcStateRef <- liftIO $ newIORef TCM.initState + let tcEnv = TCM.initEnv + return $ AgdaLib [] tcStateRef tcEnv + agdaLibIncludes :: Lens' AgdaLib [LSP.NormalizedUri] agdaLibIncludes f a = f (_agdaLibIncludes a) <&> \x -> a {_agdaLibIncludes = x} +agdaLibTcStateRef :: Lens' AgdaLib (IORef TCM.TCState) +agdaLibTcStateRef f a = f (_agdaLibTcStateRef a) <&> \x -> a {_agdaLibTcStateRef = x} + +agdaLibTcEnv :: Lens' AgdaLib TCM.TCEnv +agdaLibTcEnv f a = f (_agdaLibTcEnv a) <&> \x -> a {_agdaLibTcEnv = x} + isAgdaLibForUri :: AgdaLib -> LSP.NormalizedUri -> Bool isAgdaLibForUri agdaLib uri = any (`LSP.isUriAncestorOf` uri) (agdaLib ^. agdaLibIncludes) diff --git a/test/Test.hs b/test/Test.hs index cb14b2a..67d8960 100644 --- a/test/Test.hs +++ b/test/Test.hs @@ -9,6 +9,8 @@ import qualified Test.WASM as WASM #endif import Test.Tasty import Test.Tasty.Options +import qualified Test.Model as Model +import qualified Test.HandlerMonad as HandlerMonad -- Define the custom option newtype AlsPathOption = AlsPathOption FilePath @@ -31,7 +33,9 @@ tests = askOption $ \(AlsPathOption alsPath) -> testGroup "Tests" [ SrcLoc.tests, - LSP.tests alsPath + LSP.tests alsPath, + Model.tests, + HandlerMonad.tests #if defined(wasm32_HOST_ARCH) , WASM.tests alsPath #endif diff --git a/test/Test/HandlerMonad.hs b/test/Test/HandlerMonad.hs new file mode 100644 index 0000000..768bb43 --- /dev/null +++ b/test/Test/HandlerMonad.hs @@ -0,0 +1,92 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE RankNTypes #-} + +module Test.HandlerMonad (tests) where + +import Agda.Utils.Either (isLeft, isRight) +import Agda.Utils.IORef (newIORef, readIORef, writeIORef) +import Agda.Utils.Lens ((^.)) +import Control.Concurrent (newChan) +import Control.Monad.IO.Class (MonadIO (liftIO)) +import Control.Monad.Reader (ReaderT (ReaderT, runReaderT)) +import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Protocol.Utils.SMethodMap as SMethodMap +import qualified Language.LSP.Server as LSP +import Monad (Env (Env, envModel), ServerM, createInitEnv, runServerM) +import Options (Config, defaultOptions, initConfig) +import qualified Server.CommandController as CommandController +import Server.Handler.Monad (MonadAgdaLib (askAgdaLib), withAgdaFile) +import Server.Model (Model) +import Server.Model.AgdaLib (agdaLibIncludes) +import qualified Server.ResponseController as ResponseController +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@?), (@?=)) +import qualified TestData + +tests :: TestTree +tests = + testGroup + "Handler monads" + [ testGroup + "WithAgdaFileM" + [ testCase "gets known Agda file" $ do + let method = LSP.SMethod_TextDocumentDocumentSymbol + message = TestData.documentSymbolMessage TestData.fileUri1 + + let handlers = withAgdaFile method $ \req responder -> do + agdaLib <- askAgdaLib + liftIO $ length (agdaLib ^. agdaLibIncludes) @?= 3 + responder $ Right $ LSP.InL [] + + model <- TestData.getModel + result <- runHandler method message model handlers + + isRight result @? "didn't get known Agda file: " <> show result + + return (), + testCase "fails on unknown Agda file" $ do + let method = LSP.SMethod_TextDocumentDocumentSymbol + message = TestData.documentSymbolMessage TestData.fakeUri + + let handlers = withAgdaFile method $ \req responder -> do + responder $ Right $ LSP.InL [] + + model <- TestData.getModel + result <- runHandler method message model handlers + + isLeft result @? "got Agda file, but should be unknown" + + return () + ] + ] + +runHandler :: + forall (m :: LSP.Method LSP.ClientToServer LSP.Request). + (Show (LSP.ErrorData m)) => + LSP.SMethod m -> + LSP.TRequestMessage m -> + Model -> + LSP.Handlers (ServerM (LSP.LspM Config)) -> + IO (Either (LSP.TResponseError m) (LSP.MessageResult m)) +runHandler m request model handlers = do + resultRef <- newIORef Nothing + let callback = \response -> liftIO $ writeIORef resultRef (Just response) + + let Just (LSP.ClientMessageHandler handler) = SMethodMap.lookup m $ LSP.reqHandlers handlers + + LSP.runLspT undefined $ do + env <- + Env defaultOptions True initConfig + <$> liftIO newChan + <*> liftIO CommandController.new + <*> liftIO newChan + <*> liftIO ResponseController.new + <*> liftIO (newIORef model) + runServerM env $ do + handler request callback + + Just result <- readIORef resultRef + return result diff --git a/test/Test/Model.hs b/test/Test/Model.hs new file mode 100644 index 0000000..e4f5432 --- /dev/null +++ b/test/Test/Model.hs @@ -0,0 +1,59 @@ +module Test.Model (tests) where + +import Agda.Utils.Lens (set, (<&>), (^.)) +import Agda.Utils.Maybe (isJust, isNothing) +import qualified Data.Map as Map +import qualified Language.LSP.Protocol.Types as LSP +import Server.Model (Model (Model)) +import qualified Server.Model as Model +import Server.Model.AgdaFile (emptyAgdaFile) +import Server.Model.AgdaLib (agdaLibIncludes, initAgdaLib) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@?), (@?=)) +import qualified TestData + +tests :: TestTree +tests = + testGroup + "Model" + [ testCase "getKnownAgdaLib gets known Agda lib" $ do + model <- TestData.getModel + + let Just agdaLib = Model.getKnownAgdaLib TestData.fileUri1 model + length (agdaLib ^. agdaLibIncludes) @?= 3 + + let Just agdaLib = Model.getKnownAgdaLib TestData.fileUri2 model + length (agdaLib ^. agdaLibIncludes) @?= 1 + + let Just agdaLib = Model.getKnownAgdaLib TestData.fileUri3 model + length (agdaLib ^. agdaLibIncludes) @?= 3 + + return (), + testCase "getKnownAgdaLib fails on unknown Agda lib" $ do + model <- TestData.getModel + + let result = Model.getKnownAgdaLib TestData.fakeUri model + isNothing result @? "got Agda lib, but should be unknown" + + return (), + testCase "getAgdaFile gets known Agda file" $ do + model <- TestData.getModel + + let result = Model.getAgdaFile TestData.fileUri1 model + isJust result @? "didn't get known Agda file" + + let result = Model.getAgdaFile TestData.fileUri2 model + isJust result @? "didn't get known Agda file" + + let result = Model.getAgdaFile TestData.fileUri3 model + isJust result @? "didn't get known Agda file" + + return (), + testCase "getAgdaFile fails on unknown Agda file" $ do + model <- TestData.getModel + + let result = Model.getAgdaFile TestData.fakeUri model + isNothing result @? "got Agda file, but should be unknown" + + return () + ] diff --git a/test/TestData.hs b/test/TestData.hs new file mode 100644 index 0000000..d2528ee --- /dev/null +++ b/test/TestData.hs @@ -0,0 +1,80 @@ +{-# LANGUAGE DataKinds #-} + +module TestData + ( documentSymbolMessage, + getModel, + fileUri1, + fileUri2, + fileUri3, + fakeUri, + ) +where + +import Agda.Utils.Lens (set, (<&>)) +import qualified Data.Map as Map +import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Types as LSP +import Server.Model (Model (Model)) +import Server.Model.AgdaFile (emptyAgdaFile) +import Server.Model.AgdaLib (agdaLibIncludes, initAgdaLib) + +documentSymbolMessage :: LSP.NormalizedUri -> LSP.TRequestMessage LSP.Method_TextDocumentDocumentSymbol +documentSymbolMessage uri = + let params = + LSP.DocumentSymbolParams + Nothing + Nothing + (LSP.TextDocumentIdentifier $ LSP.fromNormalizedUri uri) + in LSP.TRequestMessage + "2.0" + (LSP.IdInt 0) + LSP.SMethod_TextDocumentDocumentSymbol + params + +-------------------------------------------------------------------------------- + +fileUri1 :: LSP.NormalizedUri +fileUri1 = LSP.toNormalizedUri $ LSP.Uri "file:///home/user2/project2/A/B/C.agda" + +fileUri2 :: LSP.NormalizedUri +fileUri2 = LSP.toNormalizedUri $ LSP.Uri "file:///home/user/project2/X.agda" + +fileUri3 :: LSP.NormalizedUri +fileUri3 = LSP.toNormalizedUri $ LSP.Uri "https://example.com/agda/Main.agda" + +fakeUri :: LSP.NormalizedUri +fakeUri = LSP.toNormalizedUri $ LSP.Uri "file:///home/user2/project/Test.agda" + +getModel :: IO Model +getModel = do + let includes1 = + LSP.toNormalizedUri . LSP.Uri + <$> [ "file:///home/user/project1/", + "file:///home/user2/project2/", + "https://example.com/agda/" + ] + testLib1 <- + initAgdaLib + <&> set agdaLibIncludes includes1 + + let includes2 = + LSP.toNormalizedUri . LSP.Uri + <$> ["file:///home/user/project2/"] + testLib2 <- + initAgdaLib + <&> set agdaLibIncludes includes2 + + let libs = [testLib1, testLib2] + + let testFile1 = emptyAgdaFile + let testFile2 = emptyAgdaFile + let testFile3 = emptyAgdaFile + + let files = + Map.fromList + [ (fileUri1, testFile1), + (fileUri2, testFile2), + (fileUri3, testFile3) + ] + + return $ Model libs files From c6348c2b6d1f992f1118bac79bff75397b4b7679 Mon Sep 17 00:00:00 2001 From: nvarner Date: Tue, 12 Aug 2025 16:39:20 -0700 Subject: [PATCH 04/23] rough edged indexer --- agda-language-server.cabal | 20 +- src/Agda/Interaction/Imports/More.hs | 50 ++ src/Agda/Position.hs | 40 +- src/Indexer.hs | 127 ++++ src/Indexer/Indexer.hs | 622 ++++++++++++++++++ src/Indexer/Monad.hs | 218 ++++++ src/Language/LSP/Protocol/Types/More.hs | 24 + .../Handler/TextDocument/DocumentSymbol.hs | 18 - src/Server/Model/AgdaFile.hs | 27 +- src/Server/{Handler => Model}/Monad.hs | 49 +- src/Server/Model/Symbol.hs | 62 +- test/Test.hs | 28 +- test/Test/Indexer/Invariants.hs | 54 ++ test/Test/Indexer/NoOverlap.hs | 152 +++++ test/Test/{HandlerMonad.hs => ModelMonad.hs} | 18 +- test/TestData.hs | 19 + test/data/Indexer/Basic.agda | 54 ++ 17 files changed, 1512 insertions(+), 70 deletions(-) create mode 100644 src/Agda/Interaction/Imports/More.hs create mode 100644 src/Indexer.hs create mode 100644 src/Indexer/Indexer.hs create mode 100644 src/Indexer/Monad.hs create mode 100644 src/Language/LSP/Protocol/Types/More.hs delete mode 100644 src/Server/Handler/TextDocument/DocumentSymbol.hs rename src/Server/{Handler => Model}/Monad.hs (81%) create mode 100644 test/Test/Indexer/Invariants.hs create mode 100644 test/Test/Indexer/NoOverlap.hs rename test/Test/{HandlerMonad.hs => ModelMonad.hs} (87%) create mode 100644 test/data/Indexer/Basic.agda diff --git a/agda-language-server.cabal b/agda-language-server.cabal index 7b83d61..7592b1b 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -49,10 +49,15 @@ library exposed-modules: Agda Agda.Convert + Agda.Interaction.Imports.More Agda.IR Agda.Parser Agda.Position Control.Concurrent.SizedChan + Indexer + Indexer.Indexer + Indexer.Monad + Language.LSP.Protocol.Types.More Language.LSP.Protocol.Types.Uri.More Monad Options @@ -71,11 +76,10 @@ library Server Server.CommandController Server.Handler - Server.Handler.Monad - Server.Handler.TextDocument.DocumentSymbol Server.Model Server.Model.AgdaFile Server.Model.AgdaLib + Server.Model.Monad Server.Model.Symbol Server.ResponseController Switchboard @@ -175,18 +179,25 @@ test-suite als-test type: exitcode-stdio-1.0 main-is: Test.hs other-modules: - Test.HandlerMonad + Test.Indexer.Invariants + Test.Indexer.NoOverlap Test.LSP Test.Model + Test.ModelMonad Test.SrcLoc Test.WASM TestData Agda Agda.Convert + Agda.Interaction.Imports.More Agda.IR Agda.Parser Agda.Position Control.Concurrent.SizedChan + Indexer + Indexer.Indexer + Indexer.Monad + Language.LSP.Protocol.Types.More Language.LSP.Protocol.Types.Uri.More Monad Options @@ -205,11 +216,10 @@ test-suite als-test Server Server.CommandController Server.Handler - Server.Handler.Monad - Server.Handler.TextDocument.DocumentSymbol Server.Model Server.Model.AgdaFile Server.Model.AgdaLib + Server.Model.Monad Server.Model.Symbol Server.ResponseController Switchboard diff --git a/src/Agda/Interaction/Imports/More.hs b/src/Agda/Interaction/Imports/More.hs new file mode 100644 index 0000000..37ac8d5 --- /dev/null +++ b/src/Agda/Interaction/Imports/More.hs @@ -0,0 +1,50 @@ +-- | This module reexports unexported functions +module Agda.Interaction.Imports.More + ( setOptionsFromSourcePragmas, + checkModuleName', + ) +where + +import Agda.Interaction.FindFile (SourceFile, checkModuleName) +import Agda.Interaction.Imports (Source) +import qualified Agda.Interaction.Imports as Imp +import Agda.Interaction.Library (OptionsPragma (..), _libPragmas) +import Agda.Syntax.Common (TopLevelModuleName') +import qualified Agda.Syntax.Concrete as C +import Agda.Syntax.Position (Range) +import Agda.Syntax.TopLevelModuleName (TopLevelModuleName) +import Agda.TypeChecking.Monad (Interface, TCM, checkAndSetOptionsFromPragma, setCurrentRange, setOptionsFromPragma, setTCLens, stPragmaOptions, useTC) +import Agda.Utils.Monad (bracket_) + +srcDefaultPragmas :: Imp.Source -> [OptionsPragma] +srcDefaultPragmas src = map _libPragmas (Imp.srcProjectLibs src) + +srcFilePragmas :: Imp.Source -> [OptionsPragma] +srcFilePragmas src = pragmas + where + cpragmas = C.modPragmas (Imp.srcModule src) + pragmas = + [ OptionsPragma + { pragmaStrings = opts, + pragmaRange = r + } + | C.OptionsPragma r opts <- cpragmas + ] + +-- | Set options from a 'Source' pragma, using the source +-- ranges of the pragmas for error reporting. Flag to check consistency. +setOptionsFromSourcePragmas :: Bool -> Imp.Source -> TCM () +setOptionsFromSourcePragmas checkOpts src = do + mapM_ setOpts (srcDefaultPragmas src) + mapM_ setOpts (srcFilePragmas src) + where + setOpts + | checkOpts = checkAndSetOptionsFromPragma + | otherwise = setOptionsFromPragma + +-- Andreas, 2016-07-11, issue 2092 +-- The error range should be set to the file with the wrong module name +-- not the importing one (which would be the default). +checkModuleName' :: TopLevelModuleName' Range -> SourceFile -> TCM () +checkModuleName' m f = + setCurrentRange m $ checkModuleName m f Nothing diff --git a/src/Agda/Position.hs b/src/Agda/Position.hs index 3e65b88..4122326 100644 --- a/src/Agda/Position.hs +++ b/src/Agda/Position.hs @@ -10,8 +10,8 @@ module Agda.Position toAgdaPositionWithoutFile, toAgdaRange, prettyPositionWithoutFile, - -- , toLSPRange - -- , toLSPPosition + toLspRange, + toLspPosition, ) where @@ -64,6 +64,31 @@ prettyPositionWithoutFile pos@(Pn () offset _line _col) = -------------------------------------------------------------------------------- +-- | Agda source locations => LSP source locations + +intervalStart :: Interval -> PositionWithoutFile +intervalEnd :: Interval -> PositionWithoutFile + +#if MIN_VERSION_Agda(2,8,0) +intervalStart (Interval _ start _end) = start +intervalEnd (Interval _ _start end) = end +#else +intervalStart (Interval start _end) = start +intervalEnd (Interval _start end) = end +#endif + +-- | Agda Range -> LSP Range +toLspRange :: Range -> LSP.Range +toLspRange range = case rangeToIntervalWithFile range of + Nothing -> LSP.Range (LSP.Position (-1) (-1)) (LSP.Position (-1) (-1)) + Just interval -> LSP.Range (toLspPosition $ intervalStart interval) (toLspPosition $ intervalEnd interval) + +-- | Agda Position -> LSP Position +toLspPosition :: Position' a -> LSP.Position +toLspPosition (Pn _ offset line col) = LSP.Position (fromIntegral line - 1) (fromIntegral col - 1) + +-------------------------------------------------------------------------------- + -- | Positon => Offset convertion -- Keeps record of offsets of every line break ("\n", "\r" and "\r\n") @@ -142,14 +167,3 @@ makeFromOffset = go (Accum previous n l table) '\r' = Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table) go (Accum previous n l table) char = Accum (Just char) (1 + n) l table - --- -------------------------------------------------------------------------------- --- -- | Agda Highlighting Range -> Agda Range - --- fromAgdaHighlightingRangeToLSPRange :: Range -> LSP.Range --- fromAgdaHighlightingRangeToLSPRange range = case rangeToIntervalWithFile range of --- Nothing -> LSP.Range (LSP.Position (-1) (-1)) (LSP.Position (-1) (-1)) --- Just (Interval start end) -> LSP.Range (toLSPPosition start) (toLSPPosition end) - --- toLSPPosition :: Position -> LSP.Position --- toLSPPosition (Pn _ offset line col) = LSP.Position (fromIntegral line - 1) (fromIntegral col - 1) diff --git a/src/Indexer.hs b/src/Indexer.hs new file mode 100644 index 0000000..315c4c9 --- /dev/null +++ b/src/Indexer.hs @@ -0,0 +1,127 @@ +module Indexer (indexFile) where + +import Agda.Interaction.FindFile (SourceFile (SourceFile)) +import qualified Agda.Interaction.FindFile as Imp +import qualified Agda.Interaction.Imports as Imp +import qualified Agda.Interaction.Imports.More as Imp +import Agda.Interaction.Library (getPrimitiveLibDir) +import Agda.Interaction.Options (defaultOptions, optLoadPrimitives) +import qualified Agda.Syntax.Concrete as C +import Agda.Syntax.Translation.ConcreteToAbstract (ToAbstract (toAbstract), TopLevel (TopLevel)) +import Agda.Syntax.Translation.ReflectedToAbstract (toAbstract_) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.Utils.FileName (AbsolutePath, filePath, mkAbsolute) +import Agda.Utils.Monad (bracket_, unlessM, when) +import qualified Agda.Utils.Trie as Trie +import Control.Monad (forM_, void) +import Control.Monad.IO.Class (liftIO) +import qualified Data.Map as Map +import qualified Data.Set as Set +import qualified Data.Strict as Strict +import Indexer.Indexer (abstractToIndex) +import Server.Model.AgdaFile (AgdaFile) +import Server.Model.Monad (MonadAgdaLib, WithAgdaLibM) +import System.FilePath (()) + +indexFile :: + Imp.Source -> + WithAgdaLibM AgdaFile +indexFile src = do + currentOptions <- TCM.useTC TCM.stPragmaOptions + + TCM.liftTCM $ + TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $ + -- Now reset the options + TCM.setCommandLineOptions . TCM.stPersistentOptions . TCM.stPersistentState =<< TCM.getTC + + TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (Imp.srcFilePath $ Imp.srcOrigin src) + + TCM.localTC (\e -> e {TCM.envCurrentPath = Just (Imp.srcFilePath $ Imp.srcOrigin src)}) $ do + let topLevel = + TopLevel + (Imp.srcFilePath $ Imp.srcOrigin src) + (Imp.srcModuleName src) + (C.modDecls $ Imp.srcModule src) + ast <- TCM.liftTCM $ toAbstract topLevel + abstractToIndex ast + +-- let options = defaultOptions + +-- TCM.liftTCM TCM.resetState + +-- TCM.liftTCM $ TCM.setCommandLineOptions' rootPath options +-- TCM.liftTCM $ Imp.setOptionsFromSourcePragmas True src +-- loadPrims <- optLoadPrimitives <$> TCM.pragmaOptions + +-- when loadPrims $ do +-- libdirPrim <- liftIO getPrimitiveLibDir + +-- -- Turn off import-chasing messages. +-- -- We have to modify the persistent verbosity setting, since +-- -- getInterface resets the current verbosity settings to the persistent ones. + +-- bracket_ (TCM.getsTC TCM.getPersistentVerbosity) TCM.putPersistentVerbosity $ do +-- TCM.modifyPersistentVerbosity +-- (Strict.Just . Trie.insert [] 0 . Strict.fromMaybe Trie.empty) +-- -- set root verbosity to 0 + +-- -- We don't want to generate highlighting information for Agda.Primitive. +-- TCM.liftTCM $ +-- TCM.withHighlightingLevel TCM.None $ +-- forM_ (Set.map (libdirPrim ) TCM.primitiveModules) $ \f -> do +-- primSource <- Imp.parseSource (SourceFile $ mkAbsolute f) +-- Imp.checkModuleName' (Imp.srcModuleName primSource) (Imp.srcOrigin primSource) +-- void $ Imp.getNonMainInterface (Imp.srcModuleName primSource) (Just primSource) + +-- TCM.liftTCM $ Imp.checkModuleName' (Imp.srcModuleName src) (Imp.srcOrigin src) + +-- addImportCycleCheck (Imp.srcModuleName src) $ +-- TCM.localTC (\e -> e {TCM.envCurrentPath = Just $ TCM.srcFileId srcFile}) $ do +-- let topLevel = +-- C.TopLevel +-- srcFile +-- (Imp.srcModuleName src) +-- (C.modDecls $ Imp.srcModule src) +-- ast <- TCM.liftTCM $ C.toAbstract topLevel + +-- deps <- TCM.useTC TCM.stImportedModulesTransitive +-- moduleToSourceId <- TCM.useTC TCM.stModuleToSourceId +-- forM_ deps $ maybeUpdateCacheForDepFile moduleToSourceId + +-- cache <- getCache +-- let entries = LSP.fromNormalizedUri . fst <$> Cache.getAllEntries cache +-- alwaysReportSDoc "lsp.cache" 20 $ return (text "cache entries:" <+> pretty entries) + +-- let ds = C.topLevelDecls ast +-- let scope = C.topLevelScope ast + +-- TCM.liftTCM TCM.activateLoadedFileCache + +-- TCM.liftTCM TCM.cachingStarts +-- opts <- TCM.liftTCM $ TCM.useTC TCM.stPragmaOptions +-- me <- TCM.liftTCM TCM.readFromCachedLog +-- case me of +-- Just (TCM.Pragmas opts', _) +-- | opts == opts' -> +-- return () +-- _ -> TCM.liftTCM TCM.cleanCachedLog +-- TCM.liftTCM $ TCM.writeToCurrentLog $ TCM.Pragmas opts + +-- TCM.liftTCM $ +-- mapM_ TC.checkDeclCached ds `TCM.finally_` TCM.cacheCurrentLog + +-- TCM.liftTCM TCM.unfreezeMetas + +-- TCM.liftTCM $ TCM.setScope scope + +-- TCM.liftTCM $ +-- TCM.stCurrentModule +-- `TCM.setTCLens'` Just +-- ( C.topLevelModuleName ast, +-- Imp.srcModuleName src +-- ) + +-- file <- Index.abstractToIndex $ C.topLevelDecls ast + +-- -- return (file, moduleToSourceId, deps) +-- return file diff --git a/src/Indexer/Indexer.hs b/src/Indexer/Indexer.hs new file mode 100644 index 0000000..a490936 --- /dev/null +++ b/src/Indexer/Indexer.hs @@ -0,0 +1,622 @@ +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeSynonymInstances #-} + +module Indexer.Indexer (abstractToIndex) where + +import qualified Agda.Syntax.Abstract as A +import qualified Agda.Syntax.Common as C +import Agda.Syntax.Common.Pretty (render) +import qualified Agda.Syntax.Concrete as C +import qualified Agda.Syntax.Info as Info +import qualified Agda.Syntax.Internal as I +import qualified Agda.Syntax.Literal as Lit +import qualified Agda.Syntax.Scope.Base as Scope +import Agda.Syntax.Translation.ConcreteToAbstract (TopLevelInfo (TopLevelInfo)) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.TypeChecking.Pretty (prettyTCM) +import Agda.Utils.Functor ((<&>)) +import Agda.Utils.List1 (List1) +import qualified Agda.Utils.List1 as List1 +import Agda.Utils.Maybe (whenJust) +import Data.Foldable (forM_, traverse_) +import qualified Data.Set as Set +import Data.Void (absurd) +import Indexer.Monad + ( AmbiguousNameLike (..), + HasParamNames (..), + IndexerM, + NameLike (..), + NoType (NoType), + SymbolKindLike (..), + TypeLike (..), + UnknownType (UnknownType), + execIndexerM, + tellDecl, + tellDef, + tellImport, + tellNamedArgUsage, + tellParamNames, + tellUsage, + withParent, + ) +import qualified Language.LSP.Server as LSP +import Monad (ServerM) +import Options (Config) +import Server.Model.AgdaFile (AgdaFile) +import Server.Model.Monad (WithAgdaLibM) +import Server.Model.Symbol (SymbolKind (..)) + +abstractToIndex :: TopLevelInfo -> WithAgdaLibM AgdaFile +abstractToIndex (TopLevelInfo decls _scope) = execIndexerM $ index decls + +class Indexable a where + index :: a -> IndexerM () + default index :: (Foldable f, Indexable b, a ~ f b) => a -> IndexerM () + index = traverse_ index + +instance Indexable A.Declaration where + index = \case + A.Axiom kindOfName defInfo _argInfo _polarities name type' -> do + tellDecl name kindOfName type' + index defInfo + index type' + A.Generalize _generalizeVars defInfo _argInfo name type' -> do + tellDecl name GeneralizeVar type' + index defInfo + index type' + A.Field defInfo name type' -> do + tellDecl name Field type' + index defInfo + index type' + A.Primitive defInfo name type' -> do + tellDecl name Prim type' + index defInfo + index type' + A.Mutual _mutualInfo decls -> + index decls + A.Section _range _erased moduleName genTel decls -> do + tellDecl moduleName Module NoType + tellParamNames moduleName genTel + index genTel + withParent moduleName $ do + index decls + A.Apply _moduleInfo _erased moduleName moduleApp _scopeCopyInfo importDirective -> do + tellUsage moduleName + index moduleApp + index importDirective + A.Import _moduleInfo moduleName importDirective -> do + tellUsage moduleName + index importDirective + A.Pragma _range pragma -> + index pragma + A.Open _moduleInfo moduleName importDirective -> do + tellUsage moduleName + index importDirective + A.FunDef _defInfo name clauses -> do + withParent name $ do + index clauses + A.DataSig defInfo _erased name genTel type' -> do + tellDecl name Data type' + index defInfo + index genTel + index type' + A.DataDef defInfo name _univCheck dataDefParams constructors -> do + tellDef name Data UnknownType + index defInfo + index dataDefParams + index constructors + A.RecSig defInfo _erased name genTel type' -> do + tellDecl name Record type' + index defInfo + index genTel + index type' + A.RecDef defInfo name _univCheck recDirectives dataDefParams type' decls -> do + tellDef name Record type' + index defInfo + index dataDefParams + index type' + withParent name $ do + index recDirectives + index decls + A.PatternSynDef name bindings pat -> do + tellDecl name PatternSyn UnknownType + forM_ bindings $ \(C.WithHiding _hiding binding) -> + tellDef binding Param UnknownType + let pat' :: A.Pattern = fmap absurd pat + index pat' + A.UnquoteDecl _mutualInfo defInfos names expr -> do + forM_ names $ \name -> + tellDef name Unknown UnknownType + index defInfos + index expr + A.UnquoteDef defInfos names expr -> do + forM_ names $ \name -> + tellDef name Unknown UnknownType + index defInfos + index expr + A.UnquoteData defInfos name _univCheck conDefInfos conNames expr -> do + tellDef name Data UnknownType + forM_ conNames $ \conName -> + tellDef conName Con UnknownType + index defInfos + index conDefInfos + index expr + A.ScopedDecl _scope decls -> + index decls + A.UnfoldingDecl _range names -> + forM_ names $ \name -> + tellUsage name + +instance Indexable A.Expr where + index = \case + A.Var name -> + tellUsage name + A.Def' name _suffix -> + tellUsage name + A.Proj _origin ambiguousName -> + tellUsage ambiguousName + A.Con ambiguousName -> + tellUsage ambiguousName + A.PatternSyn ambiguousName -> + tellUsage ambiguousName + A.Macro name -> + tellUsage name + A.Lit _exprInfo lit -> + index lit + A.QuestionMark _metaInfo _interactionId -> + return () + A.Underscore _metaInfo -> + return () + A.Dot _exprInfo expr' -> + index expr' + A.App _appInfo exprF exprArg -> do + index exprF + case funNameFromExpr exprF of + Just name -> indexNamedArgs name [exprArg] + Nothing -> index $ C.namedThing $ C.unArg exprArg + A.WithApp _appInfo exprF exprArgs -> do + index exprF + index exprArgs + A.Lam _exprInfo binding body -> do + index binding + index body + A.AbsurdLam _exprInfo _hiding -> + return () + A.ExtendedLam _exprInfo defInfo _erased _generatedFn clauses -> do + index defInfo + index clauses + A.Pi _exprInfo tel type' -> do + index tel + index type' + A.Generalized _generalizeVars type' -> do + index type' + A.Fun _exprInfo dom codom -> do + index dom + index codom + A.Let _exprInfo bindings body -> do + index bindings + index body + A.Rec _exprInfo recAssigns -> + index recAssigns + A.RecUpdate _exprInfo exprRec assigns -> do + index exprRec + index assigns + A.ScopedExpr _scope expr' -> + index expr' + A.Quote _exprInfo -> return () + A.QuoteTerm _exprInfo -> return () + A.Unquote _exprInfo -> return () + A.DontCare expr' -> index expr' + +funNameFromExpr :: A.Expr -> Maybe A.AmbiguousQName +funNameFromExpr = \case + A.Var name -> Just $ A.unambiguous $ A.qualify_ name + A.Def' name _suffix -> Just $ A.unambiguous name + A.Proj _origin name -> Just name + A.Con name -> Just name + A.PatternSyn name -> Just name + A.Dot _exprInfo expr -> funNameFromExpr expr + A.App _appInfo exprF _exprArgs -> funNameFromExpr exprF + A.WithApp _appInfo exprF _exprArgs -> funNameFromExpr exprF + A.ScopedExpr _scopeInfo expr -> funNameFromExpr expr + A.DontCare expr -> funNameFromExpr expr + _noFunName -> Nothing + +instance (Indexable a) => Indexable (A.Pattern' a) where + index = \case + A.VarP binding -> do + tellDef binding Local UnknownType + A.ConP _conPatInfo ambiguousName naps -> do + tellUsage ambiguousName + indexNamedArgs ambiguousName naps + A.ProjP _patInfo _projOrigin ambiguousName -> + tellUsage ambiguousName + A.DefP _patInfo ambiguousName naps -> do + tellUsage ambiguousName + indexNamedArgs ambiguousName naps + A.WildP _patInfo -> return () + A.AsP _patInfo binding pat' -> do + tellDef binding Local UnknownType + index pat' + A.DotP _patInfo expr -> + index expr + A.AbsurdP _patInfo -> return () + A.LitP _patInfo lit -> + index lit + A.PatternSynP _patInfo ambiguousName naps -> do + tellUsage ambiguousName + indexNamedArgs ambiguousName naps + A.EqualP _patInfo exprPairs -> + forM_ exprPairs $ \(lhs, rhs) -> do + index lhs + index rhs + A.WithP _patInfo pat' -> + index pat' + A.RecP _conPatInfo fieldAssignments -> + index fieldAssignments + A.AnnP _patInfo type' pat' -> do + index type' + index pat' + +instance (Indexable a) => Indexable (Maybe a) + +instance (Indexable a) => Indexable [a] + +instance (Indexable a) => Indexable (List1 a) + +instance (Indexable a) => Indexable (C.Arg a) + +instance Indexable A.TacticAttribute + +instance Indexable A.DefInfo where + index = index . Info.defTactic + +indexNamedArgs :: (AmbiguousNameLike n, Indexable a) => n -> [C.NamedArg a] -> IndexerM () +indexNamedArgs headNameLike args = do + let headName = toAmbiguousQName headNameLike + forM_ args $ \(C.Arg _argInfo (C.Named maybeName x)) -> do + whenJust maybeName $ tellNamedArgUsage headName + index x + +indexWithExpr :: A.WithExpr -> IndexerM () +indexWithExpr (C.Named maybeName (C.Arg _argInfo expr)) = do + whenJust maybeName $ \(A.BindName name) -> + tellDef name Param UnknownType + index expr + +instance Indexable Lit.Literal where + index = \case + Lit.LitQName name -> tellUsage name + _otherLit -> return () + +instance (Indexable a) => Indexable (C.FieldAssignment' a) where + index (C.FieldAssignment fieldCName expr) = do + scope <- TCM.getScope + let fieldNames = Scope.anameName <$> Scope.scopeLookup (C.QName fieldCName) scope + List1.ifNull fieldNames (return ()) $ \fieldNames1 -> do + let fieldName = A.AmbQ fieldNames1 + tellUsage fieldName + index expr + +instance Indexable A.RecordAssign where + index = \case + Left assign -> + index assign + Right moduleName -> + tellUsage moduleName + +instance Indexable A.WhereDeclarations where + index whereDecls = case whereDecls of + A.WhereDecls (Just moduleName) _ decl -> do + tellDecl moduleName Module NoType + withParent moduleName $ + index decl + A.WhereDecls Nothing _ decl -> + index decl + +instance (Indexable a) => Indexable (A.LHSCore' a) where + index core = case core of + A.LHSHead name pats -> do + tellDef name Param UnknownType + indexNamedArgs name pats + A.LHSProj destructor focus pats -> do + tellUsage destructor + -- TODO: what does the named arg in `focus` mean? + indexNamedArgs destructor [focus] + indexNamedArgs destructor pats + A.LHSWith lhsHead withPatterns pats -> do + index lhsHead + index withPatterns + -- TODO: what do the named args mean? + forM_ pats $ \(C.Arg _argInfo (C.Named _name pat)) -> + index pat + +instance Indexable A.LHS where + index (A.LHS lhsInfo core) = case Info.lhsEllipsis lhsInfo of + C.ExpandedEllipsis _range _withArgs -> return () + C.NoEllipsis -> index core + +instance Indexable A.RewriteEqn where + index eqn = case eqn of + C.Rewrite exprs -> + forM_ exprs $ \(_name, expr) -> + index expr + C.Invert _generatedFn bindings -> + forM_ bindings $ \(C.Named maybeName (pat, expr)) -> do + whenJust maybeName $ \bindName -> + tellDef bindName Param UnknownType + index pat + index expr + C.LeftLet bindings -> + forM_ bindings $ \(pat, expr) -> do + index pat + index expr + +instance Indexable A.RHS where + index rhs = case rhs of + A.RHS expr _concrete -> + index expr + A.AbsurdRHS -> + return () + A.WithRHS _generatedFn withExprs clauses -> do + forM_ withExprs indexWithExpr + index clauses + A.RewriteRHS rewriteExprs _strippedPats rewriteRhs whereDecls -> do + index rewriteExprs + index rewriteRhs + index whereDecls + +instance (Indexable a) => Indexable (A.Clause' a) where + index (A.Clause lhs _strippedPats rhs whereDecls _catchall) = do + index lhs + index rhs + index whereDecls + +instance Indexable A.ModuleApplication where + index = \case + A.SectionApp tele moduleName args -> do + index tele + tellUsage moduleName + indexNamedArgs moduleName args + A.RecordModuleInstance moduleName -> + tellUsage moduleName + +-- Since `HidingDirective' a b` is just `[ImportedName' a b]`, it's much more +-- explicit to give it a special function than try to use instance resolution. +indexHidingDirective :: C.HidingDirective' A.QName A.ModuleName -> IndexerM () +indexHidingDirective = traverse_ tellUsage + +instance Indexable A.Renaming where + index (C.Renaming fromName toName _toFixity _toRange) = do + tellUsage fromName + let toNameKind = case toName of + C.ImportedModule _moduleName -> Module + C.ImportedName _name -> Unknown + tellImport fromName + -- TODO: better handling of renamed imports + tellDef toName toNameKind UnknownType + +instance Indexable (C.Using' A.QName A.ModuleName) where + index using = case using of + C.UseEverything -> return () + C.Using importedNames -> traverse_ tellImport importedNames + +instance Indexable A.ImportDirective where + index (C.ImportDirective _range using hiding renaming _publicRange) = do + index using + indexHidingDirective hiding + index renaming + +instance Indexable A.LetBinding where + index = \case + A.LetBind _letInfo _argInfo boundName type' expr -> do + tellDef boundName Local type' + index type' + index expr + A.LetPatBind _letInfo pat expr -> do + index pat + index expr + A.LetApply _moduleInfo _erased moduleName moduleApp _scopeCopyInfo importDirective -> do + tellUsage moduleName + index moduleApp + index importDirective + A.LetOpen _moduleInfo moduleName importDirective -> do + tellUsage moduleName + index importDirective + A.LetDeclaredVariable boundName -> + tellDef boundName Local UnknownType + +indexNamedArgBinder :: + (TypeLike t, HasParamNames t) => + C.NamedArg A.Binder -> t -> IndexerM () +indexNamedArgBinder namedArgBinder typeLike = do + let A.Binder pat name = C.namedThing $ C.unArg namedArgBinder + tellDef name Param typeLike + index pat + +instance Indexable A.TypedBinding where + index = \case + A.TBind _range typedBindInfo binders type' -> do + index $ A.tbTacticAttr typedBindInfo + forM_ binders $ \binder -> + indexNamedArgBinder binder type' + index type' + A.TLet _range letBindings -> index letBindings + +instance Indexable A.LamBinding where + index lamBinding = case lamBinding of + A.DomainFree tacticAttr binder -> do + index tacticAttr + indexNamedArgBinder binder UnknownType + A.DomainFull binding -> + index binding + +instance Indexable A.GeneralizeTelescope where + index (A.GeneralizeTel _generalizeVars tel) = index tel + +instance Indexable A.DataDefParams where + index (A.DataDefParams _generalizeParams params) = index params + +instance Indexable A.RecordDirectives where + index = \case + (C.RecordDirectives inductive _hasEta _patRange (Just conName)) -> + tellDef conName (constructorSymbolKind inductive) UnknownType + _noUserConstructor -> return () + where + constructorSymbolKind :: Maybe (C.Ranged C.Induction) -> SymbolKind + constructorSymbolKind (Just (C.Ranged _range C.CoInductive)) = CoCon + constructorSymbolKind _inductive = Con + +instance Indexable A.Pragma where + index = \case + A.OptionsPragma _options -> + return () + A.BuiltinPragma _rstring resolvedName -> + whenJust (resolvedNameToAmbiguousQName resolvedName) $ \name -> + tellUsage name + A.BuiltinNoDefPragma _rstring kindOfName name -> do + tellDef name kindOfName UnknownType + A.RewritePragma _range ruleNames -> + forM_ ruleNames $ \ruleName -> + tellUsage ruleName + A.CompilePragma _backendName name _compileAs -> + tellUsage name + A.StaticPragma name -> + tellUsage name + A.EtaPragma name -> + tellUsage name + A.InjectivePragma name -> + tellUsage name + A.InjectiveForInferencePragma name -> + tellUsage name + A.InlinePragma _shouldInline name -> + tellUsage name + A.NotProjectionLikePragma name -> + tellUsage name + A.OverlapPragma name _overlapMode -> + tellUsage name + A.DisplayPragma name args displayExpr -> do + tellUsage name + indexNamedArgs name args + index displayExpr + +-------------------------------------------------------------------------------- + +instance NameLike A.QName where + toQName = id + +instance NameLike A.ModuleName where + toQName = A.mnameToQName + +instance NameLike A.Name where + toQName = A.qualify_ + +instance NameLike A.BindName where + toQName = toQName . A.unBind + +instance (NameLike n, NameLike m) => NameLike (C.ImportedName' n m) where + toQName (C.ImportedModule moduleName) = toQName moduleName + toQName (C.ImportedName name) = toQName name + +instance AmbiguousNameLike A.AmbiguousQName where + toAmbiguousQName = id + +instance AmbiguousNameLike A.QName where + toAmbiguousQName = A.unambiguous + +instance AmbiguousNameLike A.ModuleName where + toAmbiguousQName = toAmbiguousQName . A.mnameToQName + +instance AmbiguousNameLike A.Name where + toAmbiguousQName = toAmbiguousQName . A.qualify_ + +instance AmbiguousNameLike A.BindName where + toAmbiguousQName = toAmbiguousQName . A.unBind + +instance AmbiguousNameLike Scope.AbstractName where + toAmbiguousQName = toAmbiguousQName . Scope.anameName + +instance (AmbiguousNameLike n, AmbiguousNameLike m) => AmbiguousNameLike (C.ImportedName' n m) where + toAmbiguousQName (C.ImportedModule moduleName) = toAmbiguousQName moduleName + toAmbiguousQName (C.ImportedName name) = toAmbiguousQName name + +resolvedNameToAmbiguousQName :: Scope.ResolvedName -> Maybe A.AmbiguousQName +resolvedNameToAmbiguousQName = \case + Scope.VarName name _bindingSource -> Just $ toAmbiguousQName name + Scope.DefinedName _access name _suffix -> Just $ toAmbiguousQName name + Scope.FieldName name -> Just $ toAmbiguousQName name + Scope.ConstructorName _inductive name -> Just $ toAmbiguousQName name + Scope.PatternSynResName name -> Just $ toAmbiguousQName name + Scope.UnknownName -> Nothing + +instance SymbolKindLike SymbolKind where + toSymbolKind = id + +instance SymbolKindLike Scope.KindOfName where + toSymbolKind = \case + Scope.ConName -> Con + Scope.CoConName -> CoCon + Scope.FldName -> Field + Scope.PatternSynName -> PatternSyn + Scope.GeneralizeName -> GeneralizeVar + Scope.DisallowedGeneralizeName -> GeneralizeVar + Scope.MacroName -> Macro + Scope.QuotableName -> Unknown + Scope.DataName -> Data + Scope.RecName -> Record + Scope.FunName -> Fun + Scope.AxiomName -> Axiom + Scope.PrimName -> Prim + Scope.OtherDefName -> Unknown + +instance SymbolKindLike TCM.Defn where + toSymbolKind = \case + TCM.AxiomDefn _axiomData -> Axiom + TCM.DataOrRecSigDefn _dataOrRecSigData -> Unknown + TCM.GeneralizableVar -> GeneralizeVar + TCM.AbstractDefn defn -> toSymbolKind defn + TCM.FunctionDefn _functionData -> Fun + TCM.DatatypeDefn _datatypeData -> Data + TCM.RecordDefn _recordData -> Record + TCM.ConstructorDefn _constructorData -> Con + TCM.PrimitiveDefn _primitiveData -> Prim + TCM.PrimitiveSortDefn _primitiveSortData -> Prim + +instance (TypeLike t) => TypeLike (C.Arg t) where + toTypeString = toTypeString . C.unArg + +instance TypeLike A.Type where + toTypeString = fmap (Just . render) . TCM.liftTCM . prettyTCM + +instance TypeLike I.Type where + toTypeString = fmap (Just . render) . TCM.liftTCM . prettyTCM + +instance (HasParamNames p) => HasParamNames (C.Arg p) where + getParamNames = getParamNames . C.unArg + +instance (HasParamNames p) => HasParamNames [p] + +instance (HasParamNames p) => HasParamNames (List1 p) + +instance HasParamNames A.Type where + getParamNames = \case + A.Pi _exprInfo tel codom -> + getParamNames tel <> getParamNames codom + A.Fun _exprInfo _dom codom -> getParamNames codom + A.Generalized varNames codom -> + Set.toList varNames <> getParamNames codom + A.ScopedExpr _scopeInfo expr -> getParamNames expr + _noMoreParams -> [] + +instance HasParamNames A.TypedBinding where + getParamNames = \case + A.TBind _range _typedBindingInfo binders' _type -> + List1.toList binders' + <&> C.namedThing . C.unArg + <&> (A.qualify_ . A.unBind . A.binderName) + A.TLet _range _letBindings -> [] + +instance HasParamNames A.GeneralizeTelescope where + getParamNames (A.GeneralizeTel _vars tel) = getParamNames tel diff --git a/src/Indexer/Monad.hs b/src/Indexer/Monad.hs new file mode 100644 index 0000000..61d4fcf --- /dev/null +++ b/src/Indexer/Monad.hs @@ -0,0 +1,218 @@ +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} + +module Indexer.Monad + ( IndexerM, + execIndexerM, + tellParamNames, + tellDef, + tellDecl, + tellUsage, + tellImport, + tellNamedArgUsage, + withParent, + NameLike (..), + AmbiguousNameLike (..), + SymbolKindLike (..), + TypeLike (..), + HasParamNames (..), + UnknownType (UnknownType), + NoType (NoType), + ) +where + +import Agda.Position (toLspRange) +import qualified Agda.Syntax.Abstract as A +import qualified Agda.Syntax.Common as C +import Agda.Syntax.Position (HasRange, getRange) +import Agda.Utils.IORef (IORef, modifyIORef', newIORef, readIORef) +import Agda.Utils.Lens (over) +import Agda.Utils.List1 (List1, concatMap1) +import Agda.Utils.Maybe (isNothing) +import Control.Applicative ((<|>)) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad.Reader (MonadReader (local), ReaderT (runReaderT), asks) +import Control.Monad.Trans (lift) +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Language.LSP.Server as LSP +import Monad (ServerM) +import Options (Config) +import Server.Model.AgdaFile (AgdaFile, agdaFileRefs, agdaFileSymbols, emptyAgdaFile, insertRef, insertSymbolInfo) +import Server.Model.Monad (WithAgdaLibM) +import Server.Model.Symbol (Ref (Ref), RefKind (..), SymbolInfo (..), SymbolKind (..)) + +data NamedArgUsage = NamedArgUsage + { nauHead :: !A.AmbiguousQName, + nauArg :: !C.NamedName + } + +data Env = Env + { envAgdaFile :: !(IORef AgdaFile), + envParent :: !(Maybe A.QName), + -- | Parameter names in implicit arguments, such as x in `f {x = y} = y` and + -- `g y = f {x = y}`, are represented by strings in abstract syntax. This is + -- because we need type checking information to resolve these names, not + -- just scope checking information. + -- + -- Agda doesn't seem to expose its internal type checker resolution of these + -- names. We hack around it by storing the implicit parameter names for each + -- function ourselves, then looking up the strings at the end and emitting + -- them as references. Ideally, this solution is eventually replaced by + -- changing the type checker so it emits this information for us. + -- + -- These are the stored parameter names, indexed by the name of the function + -- (or other defined symbol). + envParamNames :: !(IORef (Map A.QName [A.QName])), + envNamedArgUsages :: !(IORef [NamedArgUsage]) + } + +initEnv :: (MonadIO m) => m Env +initEnv = do + agdaFile <- liftIO $ newIORef emptyAgdaFile + let parent = Nothing + paramNames <- liftIO $ newIORef Map.empty + namedArgUsages <- liftIO $ newIORef [] + return $ Env agdaFile parent paramNames namedArgUsages + +type IndexerM = ReaderT Env WithAgdaLibM + +execIndexerM :: IndexerM a -> WithAgdaLibM AgdaFile +execIndexerM x = do + env <- initEnv + _ <- runReaderT x env + -- TODO: resolve named arg usages + liftIO $ readIORef $ envAgdaFile env + +-------------------------------------------------------------------------------- + +-- Used when inserting a new `SymbolInfo` into a map already containing a +-- `SymbolInfo` for the given symbol +updateSymbolInfo :: SymbolInfo -> SymbolInfo -> SymbolInfo +updateSymbolInfo new old = + SymbolInfo + (symbolKind old <> symbolKind new) + (symbolType old <|> symbolType new) + (symbolParent old <|> symbolParent new) + +tellSymbolInfo' :: A.QName -> SymbolInfo -> IndexerM () +tellSymbolInfo' name symbolInfo = do + agdaFileRef <- asks envAgdaFile + liftIO $ modifyIORef' agdaFileRef $ insertSymbolInfo updateSymbolInfo name symbolInfo + +tellSymbolInfo :: + (NameLike n, SymbolKindLike s, TypeLike t) => + n -> s -> t -> IndexerM () +tellSymbolInfo nameLike symbolKindLike typeLike = do + let name = toQName nameLike + symbolKind = toSymbolKind symbolKindLike + type' <- lift $ toTypeString typeLike + parent <- asks envParent + let symbolInfo = SymbolInfo symbolKind type' parent + tellSymbolInfo' name symbolInfo + +tellRef' :: A.AmbiguousQName -> Ref -> IndexerM () +tellRef' ambiguousName ref = do + agdaFileRef <- asks envAgdaFile + liftIO $ modifyIORef' agdaFileRef $ insertRef ambiguousName ref + +tellRef :: + (AmbiguousNameLike n) => + n -> RefKind -> IndexerM () +tellRef nameLike refKind = do + let name = toAmbiguousQName nameLike + range = toLspRange $ getRange name + ref = Ref refKind range (A.isAmbiguous name) + tellRef' name ref + +tellParamNames :: (NameLike n, HasParamNames p) => n -> p -> IndexerM () +tellParamNames nameLike hasParamNames = do + let name = toQName nameLike + let paramNames = getParamNames hasParamNames + paramNamesRef <- asks envParamNames + liftIO $ modifyIORef' paramNamesRef $ Map.insert name paramNames + +tellDef :: + (NameLike n, SymbolKindLike s, TypeLike t, HasParamNames t) => + n -> s -> t -> IndexerM () +tellDef n s t = do + tellSymbolInfo n s t + tellRef n Def + tellParamNames n t + +tellDecl :: + (NameLike n, SymbolKindLike s, TypeLike t, HasParamNames t) => + n -> s -> t -> IndexerM () +tellDecl n s t = do + tellSymbolInfo n s t + tellRef n Decl + tellParamNames n t + +tellUsage :: (AmbiguousNameLike n) => n -> IndexerM () +tellUsage n = tellRef n Usage + +tellImport :: (AmbiguousNameLike n) => n -> IndexerM () +tellImport n = tellRef n Import + +tellNamedArgUsage :: (AmbiguousNameLike n) => n -> C.NamedName -> IndexerM () +tellNamedArgUsage headNameLike argName = do + let headName = toAmbiguousQName headNameLike + namedArgUsage = NamedArgUsage headName argName + namedArgUsagesRef <- asks envNamedArgUsages + liftIO $ modifyIORef' namedArgUsagesRef $ (namedArgUsage :) + +withParent :: (NameLike n) => n -> IndexerM a -> IndexerM a +withParent nameLike = local $ \e -> e {envParent = Just $ toQName nameLike} + +-------------------------------------------------------------------------------- + +class (AmbiguousNameLike n) => NameLike n where + toQName :: n -> A.QName + +class AmbiguousNameLike n where + toAmbiguousQName :: n -> A.AmbiguousQName + +instance (AmbiguousNameLike n) => AmbiguousNameLike (List1 n) where + toAmbiguousQName = A.AmbQ . concatMap1 (A.unAmbQ . toAmbiguousQName) + +class SymbolKindLike a where + toSymbolKind :: a -> SymbolKind + +class HasParamNames p where + getParamNames :: p -> [A.QName] + default getParamNames :: (Foldable f, HasParamNames b, p ~ f b) => p -> [A.QName] + getParamNames = foldMap getParamNames + +instance (HasParamNames p) => HasParamNames (Maybe p) where + getParamNames = maybe [] getParamNames + +class TypeLike t where + -- | Try to render a type to a @String@. Strings were chosen because: + -- - they are easily obtained from abstract and internal terms + -- - they do not depend on the scope, context, or other TC state + -- - they have a low memory footprint compared to unrendered @Doc@s + -- + -- However, strings do lose semantic information otherwise available to us, + -- so this representation may be switched in the future if that information is + -- needed. + toTypeString :: t -> WithAgdaLibM (Maybe String) + +instance (TypeLike t) => TypeLike (Maybe t) where + toTypeString = maybe (return Nothing) toTypeString + +data UnknownType = UnknownType + +instance HasParamNames UnknownType where + getParamNames UnknownType = [] + +instance TypeLike UnknownType where + toTypeString UnknownType = return Nothing + +data NoType = NoType + +instance HasParamNames NoType where + getParamNames NoType = [] + +instance TypeLike NoType where + toTypeString NoType = return Nothing diff --git a/src/Language/LSP/Protocol/Types/More.hs b/src/Language/LSP/Protocol/Types/More.hs new file mode 100644 index 0000000..c64f51f --- /dev/null +++ b/src/Language/LSP/Protocol/Types/More.hs @@ -0,0 +1,24 @@ +module Language.LSP.Protocol.Types.More () where + +import Agda.Syntax.Common.Pretty +import Agda.Utils.Lens ((^.)) +import qualified Data.Text as Text +import qualified Language.LSP.Protocol.Lens as LSP +import qualified Language.LSP.Protocol.Types as LSP + +instance Pretty LSP.Uri where + pretty = text . Text.unpack . LSP.getUri + +instance Pretty LSP.Position where + pretty pos = pshow (pos ^. LSP.line + 1) <> text ":" <> pshow (pos ^. LSP.character + 1) + +instance Pretty LSP.Range where + pretty range = + if range ^. LSP.start . LSP.line == range ^. LSP.end . LSP.line + then + pshow (range ^. LSP.start . LSP.line + 1) + <> text ":" + <> pshow (range ^. LSP.start . LSP.character + 1) + <> text "-" + <> pshow (range ^. LSP.end . LSP.character + 1) + else pretty (range ^. LSP.start) <> text "-" <> pretty (range ^. LSP.end) diff --git a/src/Server/Handler/TextDocument/DocumentSymbol.hs b/src/Server/Handler/TextDocument/DocumentSymbol.hs deleted file mode 100644 index 71940b3..0000000 --- a/src/Server/Handler/TextDocument/DocumentSymbol.hs +++ /dev/null @@ -1,18 +0,0 @@ -module Server.Handler.TextDocument.DocumentSymbol (documentSymbolHandler) where - -import Agda.Utils.Lens ((^.)) -import qualified Language.LSP.Protocol.Lens as LSP -import qualified Language.LSP.Protocol.Message as LSP -import qualified Language.LSP.Protocol.Types as LSP -import Language.LSP.Server (LspM) -import qualified Language.LSP.Server as LSP -import Monad (ServerM) -import Options (Config) -import Server.Handler.Monad (useAgdaFile, withAgdaFile) -import qualified Server.Model as Model -import Server.Model.AgdaFile (agdaFileSymbols) - -documentSymbolHandler :: LSP.Handlers (ServerM (LspM Config)) -documentSymbolHandler = withAgdaFile LSP.SMethod_TextDocumentDocumentSymbol $ \req responder -> do - symbols <- useAgdaFile agdaFileSymbols - return () diff --git a/src/Server/Model/AgdaFile.hs b/src/Server/Model/AgdaFile.hs index afabdc6..3298f97 100644 --- a/src/Server/Model/AgdaFile.hs +++ b/src/Server/Model/AgdaFile.hs @@ -2,13 +2,19 @@ module Server.Model.AgdaFile ( AgdaFile, emptyAgdaFile, agdaFileSymbols, + agdaFileRefs, + insertSymbolInfo, + insertRef, ) where import qualified Agda.Syntax.Abstract as A -import Agda.Utils.Lens (Lens', (<&>)) +import Agda.Utils.Lens (Lens', over, (<&>)) +import Control.Monad (forM) +import Data.Foldable (fold) import Data.Map (Map) import qualified Data.Map as Map +import Data.Monoid (Endo (Endo, appEndo)) import Server.Model.Symbol (Ref, SymbolInfo) data AgdaFile = AgdaFile @@ -21,3 +27,22 @@ emptyAgdaFile = AgdaFile Map.empty Map.empty agdaFileSymbols :: Lens' AgdaFile (Map A.QName SymbolInfo) agdaFileSymbols f a = f (_agdaFileSymbols a) <&> \x -> a {_agdaFileSymbols = x} + +agdaFileRefs :: Lens' AgdaFile (Map A.QName [Ref]) +agdaFileRefs f a = f (_agdaFileRefs a) <&> \x -> a {_agdaFileRefs = x} + +insertSymbolInfo :: + (SymbolInfo -> SymbolInfo -> SymbolInfo) -> + A.QName -> + SymbolInfo -> + AgdaFile -> + AgdaFile +insertSymbolInfo update name symbolInfo = over agdaFileSymbols $ Map.insertWith update name symbolInfo + +insertRef :: A.AmbiguousQName -> Ref -> AgdaFile -> AgdaFile +insertRef ambiguousName ref = + over agdaFileRefs $ + appEndo $ + foldMap (\name -> Endo $ Map.insertWith (<>) name [ref]) (A.unAmbQ ambiguousName) + +-- Map.insertWith (<>) name [ref] diff --git a/src/Server/Handler/Monad.hs b/src/Server/Model/Monad.hs similarity index 81% rename from src/Server/Handler/Monad.hs rename to src/Server/Model/Monad.hs index 863060b..a4068c3 100644 --- a/src/Server/Handler/Monad.hs +++ b/src/Server/Model/Monad.hs @@ -1,16 +1,20 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeSynonymInstances #-} -module Server.Handler.Monad +module Server.Model.Monad ( MonadAgdaLib (..), useAgdaLib, MonadAgdaFile (..), useAgdaFile, withAgdaFile, + WithAgdaLibM, + withAgdaLibFor, ) where @@ -20,7 +24,7 @@ import Agda.Utils.IORef (modifyIORef', readIORef, writeIORef) import Agda.Utils.Lens (Lens', locally, over, use, view, (<&>), (^.)) import Agda.Utils.Monad (bracket_) import Control.Monad.IO.Class (MonadIO (liftIO)) -import Control.Monad.Reader (MonadReader (local), ReaderT (runReaderT), asks) +import Control.Monad.Reader (MonadReader (local), ReaderT (runReaderT), ask, asks) import Control.Monad.Trans (MonadTrans, lift) import qualified Language.LSP.Protocol.Lens as LSP import qualified Language.LSP.Protocol.Message as LSP @@ -100,6 +104,47 @@ defaultLiftTCM (TCM f) = do -------------------------------------------------------------------------------- +newtype WithAgdaLibT m a = WithAgdaLibT {unWithAgdaLibT :: ReaderT AgdaLib m a} + deriving (Functor, Applicative, Monad, MonadIO, MonadTrans) + +runWithAgdaLibT :: AgdaLib -> WithAgdaLibT m a -> m a +runWithAgdaLibT agdaLib = flip runReaderT agdaLib . unWithAgdaLibT + +type WithAgdaLibM = WithAgdaLibT (ServerM (LspM Config)) + +withAgdaLibFor :: LSP.Uri -> WithAgdaLibM a -> ServerM (LspM Config) a +withAgdaLibFor uri x = do + let normUri = LSP.toNormalizedUri uri + model <- askModel + agdaLib <- Model.getAgdaLib normUri model + runWithAgdaLibT agdaLib x + +instance (MonadIO m) => MonadAgdaLib (WithAgdaLibT m) where + askAgdaLib = WithAgdaLibT ask + localAgdaLib f = WithAgdaLibT . local f . unWithAgdaLibT + +instance (MonadIO m) => MonadTCEnv (WithAgdaLibT m) where + askTC = defaultAskTC + localTC = defaultLocalTC + +instance (MonadIO m) => MonadTCState (WithAgdaLibT m) where + getTC = defaultGetTC + putTC = defaultPutTC + modifyTC = defaultModifyTC + +instance (MonadIO m) => ReadTCState (WithAgdaLibT m) where + getTCState = defaultGetTC + locallyTCState = defaultLocallyTCState + +instance (MonadIO m) => HasOptions (WithAgdaLibT m) where + pragmaOptions = defaultPragmaOptionsImpl + commandLineOptions = defaultCommandLineOptionsImpl + +instance (MonadIO m) => MonadTCM (WithAgdaLibT m) where + liftTCM = defaultLiftTCM + +-------------------------------------------------------------------------------- + data WithAgdaFileEnv = WithAgdaFileEnv { _withAgdaFileEnvAgdaLib :: !AgdaLib, _withAgdaFileEnvAgdaFile :: !AgdaFile diff --git a/src/Server/Model/Symbol.hs b/src/Server/Model/Symbol.hs index 5506f15..e50727f 100644 --- a/src/Server/Model/Symbol.hs +++ b/src/Server/Model/Symbol.hs @@ -1,8 +1,16 @@ -module Server.Model.Symbol (SymbolInfo, Ref) where +module Server.Model.Symbol + ( SymbolKind (..), + SymbolInfo (..), + RefKind (..), + Ref (..), + ) +where import qualified Agda.Syntax.Abstract as A +import Agda.Syntax.Common.Pretty (Doc, Pretty, comma, parens, pretty, pshow, text, (<+>)) import Agda.Syntax.Position (Position, PositionWithoutFile) import qualified Language.LSP.Protocol.Types as LSP +import Language.LSP.Protocol.Types.More () data SymbolKind = Con @@ -20,15 +28,55 @@ data SymbolKind | Param | Local | Unknown - deriving (Show) + deriving (Show, Eq) + +instance Semigroup SymbolKind where + Unknown <> k = k + k <> _k = k data SymbolInfo = SymbolInfo - { _symbolKind :: !SymbolKind, - _symbolType :: !(Maybe String), - _symbolParent :: !(Maybe A.QName) + { symbolKind :: !SymbolKind, + symbolType :: !(Maybe String), + symbolParent :: !(Maybe A.QName) } +data RefKind + = -- | The symbol is being declared. There should be at most one declaration + -- for any given symbol (in correct Agda code). Roughly speaking, this is + -- the "single most important defining reference" + -- + -- For example, a function's name in its signature + Decl + | -- | The symbol is being defined, but is not being declared in the sense + -- that @Decl@ would apply. Typically, this means the definition may be + -- split into several parts, and this is one of the "less important" parts + -- + -- For example, a function's name in the LHS of a clause in its definition + Def + | -- | The symbol is (expected to be) already defined and is being used + -- + -- For example, a function's name in function application + Usage + | -- | The symbol is being imported here + Import + deriving (Show, Eq) + +instance Pretty RefKind where + pretty = pshow + data Ref = Ref - { _refSymbol :: !A.QName, - _refRange :: !LSP.Range + { refKind :: !RefKind, + refRange :: !LSP.Range, + refIsAmbiguous :: !Bool } + +prettyAmbiguity :: Ref -> Doc +prettyAmbiguity ref = + if refIsAmbiguous ref + then text "ambiguous" + else text "unambiguous" + +instance Pretty Ref where + pretty ref = + ((prettyAmbiguity ref <+> pretty (refKind ref)) <> comma) + <+> pretty (refRange ref) diff --git a/test/Test.hs b/test/Test.hs index 67d8960..34aa3eb 100644 --- a/test/Test.hs +++ b/test/Test.hs @@ -10,7 +10,8 @@ import qualified Test.WASM as WASM import Test.Tasty import Test.Tasty.Options import qualified Test.Model as Model -import qualified Test.HandlerMonad as HandlerMonad +import qualified Test.ModelMonad as ModelMonad +import qualified Test.Indexer.Invariants as IndexerInvariants -- Define the custom option newtype AlsPathOption = AlsPathOption FilePath @@ -26,17 +27,20 @@ main :: IO () main = do let opts = [Option (Proxy :: Proxy AlsPathOption)] ingredients = includingOptions opts : defaultIngredients - defaultMainWithIngredients ingredients tests + defaultMainWithIngredients ingredients =<< tests -tests :: TestTree -tests = askOption $ \(AlsPathOption alsPath) -> - testGroup - "Tests" - [ SrcLoc.tests, - LSP.tests alsPath, - Model.tests, - HandlerMonad.tests +tests :: IO TestTree +tests = do + indexerInvariantsTest <- IndexerInvariants.tests + return $ askOption $ \(AlsPathOption alsPath) -> + testGroup + "Tests" + [ SrcLoc.tests, + LSP.tests alsPath, + Model.tests, + ModelMonad.tests, + indexerInvariantsTest #if defined(wasm32_HOST_ARCH) - , WASM.tests alsPath + , WASM.tests alsPath #endif - ] \ No newline at end of file + ] \ No newline at end of file diff --git a/test/Test/Indexer/Invariants.hs b/test/Test/Indexer/Invariants.hs new file mode 100644 index 0000000..dca595e --- /dev/null +++ b/test/Test/Indexer/Invariants.hs @@ -0,0 +1,54 @@ +module Test.Indexer.Invariants (tests) where + +import Agda.Interaction.FindFile (SourceFile (SourceFile)) +import qualified Agda.Interaction.Imports as Imp +import Agda.Interaction.Options (defaultOptions) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.Utils.FileName (absolute) +import Agda.Utils.Lens ((^.)) +import Control.Monad (forM) +import Control.Monad.IO.Class (liftIO) +import Data.Foldable (traverse_) +import Data.IntMap (IntMap) +import qualified Data.IntMap as IntMap +import qualified Data.Map as Map +import Indexer (indexFile) +import Indexer.Indexer (abstractToIndex) +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Server as LSP +import Monad (runServerM) +import Server.Model.AgdaFile (AgdaFile, agdaFileRefs) +import Server.Model.Monad (withAgdaLibFor) +import System.FilePath (takeBaseName) +import Test.Indexer.NoOverlap (testNoOverlap) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Golden (findByExtension) +import Test.Tasty.HUnit (testCase) +import qualified TestData + +tests :: IO TestTree +tests = do + inPaths <- findByExtension [".agda"] "test/data/Indexer" + namedFiles <- forM inPaths $ \inPath -> do + let testName = takeBaseName inPath + uri = LSP.filePathToUri inPath + model <- TestData.getModel + + file <- LSP.runLspT undefined $ do + env <- TestData.getServerEnv model + runServerM env $ do + withAgdaLibFor uri $ do + TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions + absInPath <- liftIO $ absolute inPath + let srcFile = SourceFile absInPath + src <- TCM.liftTCM $ Imp.parseSource srcFile + + indexFile src + + return (testName, file) + + return $ + testGroup + "Invariants" + [ testGroup "No reference overlap" (uncurry testNoOverlap <$> namedFiles) + ] diff --git a/test/Test/Indexer/NoOverlap.hs b/test/Test/Indexer/NoOverlap.hs new file mode 100644 index 0000000..9470604 --- /dev/null +++ b/test/Test/Indexer/NoOverlap.hs @@ -0,0 +1,152 @@ +module Test.Indexer.NoOverlap (testNoOverlap) where + +import qualified Agda.Syntax.Abstract as A +import Agda.Syntax.Common.Pretty (Doc, Pretty (prettyList), align, parens, pretty, prettyShow, text, vcat, (<+>)) +import Agda.Utils.Lens ((^.)) +import Control.Monad (forM, forM_) +import Control.Monad.Writer.CPS (Writer, execWriter, tell) +import Data.Foldable (foldrM) +import Data.IntMap (IntMap) +import qualified Data.IntMap as IntMap +import qualified Data.Map as Map +import qualified Language.LSP.Protocol.Lens as LSP +import qualified Language.LSP.Protocol.Types as LSP +import Server.Model.AgdaFile (AgdaFile, agdaFileRefs) +import Server.Model.Symbol (Ref (refRange), refIsAmbiguous) +import Test.Tasty (TestTree) +import Test.Tasty.HUnit (assertFailure, testCase) + +data OverlapError = OverlapError + { oeLineNum :: !Int, + oePart1 :: !LinePart, + oePart2 :: !LinePart + } + +instance Pretty OverlapError where + pretty err = + vcat + [ text "Overlap error at line number" + <+> pretty (oeLineNum err + 1) + <+> linePartPrettyRange (oePart1 err) + <+> text "and" + <+> linePartPrettyRange (oePart2 err), + pretty (linePartName (oePart1 err)) + <+> pretty (linePartRef (oePart1 err)), + pretty (linePartName (oePart2 err)) + <+> pretty (linePartRef (oePart2 err)) + ] + + prettyList = \case + [] -> text "No overlap errors" + [err] -> pretty err + errs -> align 5 $ (\err -> ("-", vcat [pretty err, text ""])) <$> errs + +type OverlapResult = Writer [OverlapError] + +data LinePart + = RangePart !A.QName !Ref !Int !Int + | ToEndPart !A.QName !Ref !Int + +linePartPrettyRange :: LinePart -> Doc +linePartPrettyRange (RangePart _ _ start end) = text "from" <+> pretty start <+> text "to" <+> pretty end +linePartPrettyRange (ToEndPart _ _ start) = text "from" <+> pretty start <+> text "to the end of the line" + +linePartName :: LinePart -> A.QName +linePartName (RangePart name _ _ _) = name +linePartName (ToEndPart name _ _) = name + +linePartRef :: LinePart -> Ref +linePartRef (RangePart _ ref _ _) = ref +linePartRef (ToEndPart _ ref _) = ref + +assertPartsNonoverlapping :: Int -> LinePart -> LinePart -> OverlapResult () +assertPartsNonoverlapping lineNum part1 part2 = case (part1, part2) of + -- Allow refs known to be ambiguous + (_, _) + | refIsAmbiguous (linePartRef part1) + && refIsAmbiguous (linePartRef part2) -> + return () + (ToEndPart _ _ _, ToEndPart _ _ _) -> err + (RangePart _ _ _ rangeEnd, ToEndPart _ _ toEndStart) + | rangeEnd > toEndStart -> err + (ToEndPart _ _ toEndStart, RangePart _ _ _ rangeEnd) + | rangeEnd > toEndStart -> err + (RangePart _ _ start1 end1, RangePart _ _ start2 end2) + | (start1 <= start2 && end1 > start2) + || (start2 <= start1 && end2 > start1) -> + err + _ -> return () + where + err = tell $ [OverlapError lineNum part1 part2] + +newtype Line = Line [LinePart] + +rangePart :: (Integral n) => A.QName -> Ref -> n -> n -> Line +rangePart name ref start end = Line [RangePart name ref (fromIntegral start) (fromIntegral end)] + +toEndPart :: (Integral n) => A.QName -> Ref -> n -> Line +toEndPart name ref start = Line [ToEndPart name ref (fromIntegral start)] + +tryInsertPart :: Int -> LinePart -> Line -> OverlapResult (Line) +tryInsertPart lineNum part (Line parts) = do + forM_ parts $ \part2 -> + assertPartsNonoverlapping lineNum part part2 + return $ Line $ part : parts + +tryMerge :: Int -> Line -> Line -> OverlapResult (Line) +tryMerge lineNum (Line newParts) line = foldrM (tryInsertPart lineNum) line newParts + +rangeToLines :: A.QName -> Ref -> LSP.Range -> [(Int, Line)] +rangeToLines name ref range = + if startLine == endLine + then + [ ( startLine, + rangePart + name + ref + (range ^. LSP.start . LSP.character) + (range ^. LSP.end . LSP.character) + ) + ] + else + let start = (startLine, toEndPart name ref $ range ^. LSP.start . LSP.character) + end = (endLine, rangePart name ref 0 $ range ^. LSP.end . LSP.character) + middle = do + lineNum <- [startLine + 1 .. endLine - 1] + return (lineNum, toEndPart name ref 0) + in [start] <> middle <> [end] + where + startLine = fromIntegral $ range ^. LSP.start . LSP.line + endLine = fromIntegral $ range ^. LSP.end . LSP.line + +newtype FileRanges = FileRanges (IntMap (Line)) + +emptyFileRanges :: FileRanges +emptyFileRanges = FileRanges IntMap.empty + +tryInsertLine :: Int -> Line -> FileRanges -> OverlapResult (FileRanges) +tryInsertLine lineNum line (FileRanges ranges) = + FileRanges <$> IntMap.alterF helper lineNum ranges + where + helper Nothing = return $ Just line + helper (Just oldLine) = Just <$> tryMerge lineNum line oldLine + +tryInsertRange :: A.QName -> Ref -> LSP.Range -> FileRanges -> OverlapResult (FileRanges) +tryInsertRange name ref range fileRanges = do + let lines = rangeToLines name ref range + foldrM (uncurry tryInsertLine) fileRanges lines + +testNoOverlap :: String -> AgdaFile -> TestTree +testNoOverlap name file = testCase name $ do + let refs = + concatMap (\(name, refs) -> (\ref -> (name, ref)) <$> refs) $ + Map.toList $ + file ^. agdaFileRefs + let fileRanges = emptyFileRanges + let errors = + execWriter $ + foldrM (\(name, ref) -> tryInsertRange name ref (refRange ref)) fileRanges refs + + case errors of + [] -> return () + _ -> assertFailure $ prettyShow errors diff --git a/test/Test/HandlerMonad.hs b/test/Test/ModelMonad.hs similarity index 87% rename from test/Test/HandlerMonad.hs rename to test/Test/ModelMonad.hs index 768bb43..e96eb19 100644 --- a/test/Test/HandlerMonad.hs +++ b/test/Test/ModelMonad.hs @@ -3,8 +3,9 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} -module Test.HandlerMonad (tests) where +module Test.ModelMonad (tests) where +import qualified Agda.Compiler.Backend as TestData import Agda.Utils.Either (isLeft, isRight) import Agda.Utils.IORef (newIORef, readIORef, writeIORef) import Agda.Utils.Lens ((^.)) @@ -18,9 +19,9 @@ import qualified Language.LSP.Server as LSP import Monad (Env (Env, envModel), ServerM, createInitEnv, runServerM) import Options (Config, defaultOptions, initConfig) import qualified Server.CommandController as CommandController -import Server.Handler.Monad (MonadAgdaLib (askAgdaLib), withAgdaFile) import Server.Model (Model) import Server.Model.AgdaLib (agdaLibIncludes) +import Server.Model.Monad (MonadAgdaLib (askAgdaLib), withAgdaFile) import qualified Server.ResponseController as ResponseController import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (testCase, (@?), (@?=)) @@ -29,7 +30,7 @@ import qualified TestData tests :: TestTree tests = testGroup - "Handler monads" + "Model monads" [ testGroup "WithAgdaFileM" [ testCase "gets known Agda file" $ do @@ -78,15 +79,8 @@ runHandler m request model handlers = do let Just (LSP.ClientMessageHandler handler) = SMethodMap.lookup m $ LSP.reqHandlers handlers LSP.runLspT undefined $ do - env <- - Env defaultOptions True initConfig - <$> liftIO newChan - <*> liftIO CommandController.new - <*> liftIO newChan - <*> liftIO ResponseController.new - <*> liftIO (newIORef model) - runServerM env $ do - handler request callback + env <- TestData.getServerEnv model + runServerM env $ handler request callback Just result <- readIORef resultRef return result diff --git a/test/TestData.hs b/test/TestData.hs index d2528ee..d9d9e00 100644 --- a/test/TestData.hs +++ b/test/TestData.hs @@ -7,16 +7,24 @@ module TestData fileUri2, fileUri3, fakeUri, + getServerEnv, ) where +import Agda.Utils.IORef (newIORef) import Agda.Utils.Lens (set, (<&>)) +import Control.Concurrent (newChan) +import Control.Monad.IO.Class (MonadIO, liftIO) import qualified Data.Map as Map import qualified Language.LSP.Protocol.Message as LSP import qualified Language.LSP.Protocol.Types as LSP +import Monad (Env (Env)) +import Options (defaultOptions, initConfig) +import qualified Server.CommandController as CommandController import Server.Model (Model (Model)) import Server.Model.AgdaFile (emptyAgdaFile) import Server.Model.AgdaLib (agdaLibIncludes, initAgdaLib) +import qualified Server.ResponseController as ResponseController documentSymbolMessage :: LSP.NormalizedUri -> LSP.TRequestMessage LSP.Method_TextDocumentDocumentSymbol documentSymbolMessage uri = @@ -78,3 +86,14 @@ getModel = do ] return $ Model libs files + +-------------------------------------------------------------------------------- + +getServerEnv :: (MonadIO m) => Model -> m Env +getServerEnv model = + Env defaultOptions True initConfig + <$> liftIO newChan + <*> liftIO CommandController.new + <*> liftIO newChan + <*> liftIO ResponseController.new + <*> liftIO (newIORef model) diff --git a/test/data/Indexer/Basic.agda b/test/data/Indexer/Basic.agda new file mode 100644 index 0000000..3ddbb80 --- /dev/null +++ b/test/data/Indexer/Basic.agda @@ -0,0 +1,54 @@ +module Basic where + +data Nat : Set where + zero : Nat + suc : Nat -> Nat + +one : Nat +one = suc zero + +two : Nat +two = suc one + +data Test : Set where + test : Test + +data Test' : Set where + test : Test' + +hello : Test +hello = test + +data Empty : Set where + +Not : Set -> Set +Not A = A -> Empty + +Goodbye : Set +Goodbye = Not Test + +postulate A : Test -> Set + +testId : Test -> Test +testId test = test + +id : {A : Set} -> A -> A +id = \where x -> x + +id' : {A : Set} -> A -> A +id' = \x -> let x = x in x + +id'' : {A : Set} -> A -> A +id'' {A = A} x = + let x = x + A = A + in x + +record World : Set where + field + north : Test + south : Test' + +earth : World +earth .World.north = test +earth .World.south = test From 78f67857bbadc5f718569be6df79aff258dcb326 Mon Sep 17 00:00:00 2001 From: nvarner Date: Tue, 12 Aug 2025 19:06:54 -0700 Subject: [PATCH 05/23] check that we don't miss Refs --- agda-language-server.cabal | 1 + src/Indexer.hs | 9 ++-- src/Server/Model/AgdaFile.hs | 12 +++-- src/Server/Model/Symbol.hs | 10 +++- test/Test/Indexer/Invariants.hs | 25 +++++++--- test/Test/Indexer/NoMissing.hs | 82 +++++++++++++++++++++++++++++++++ test/Test/Indexer/NoOverlap.hs | 2 + test/data/Indexer/Basic.agda | 21 +++++++++ test/data/Indexer/Small.agda | 1 + 9 files changed, 148 insertions(+), 15 deletions(-) create mode 100644 test/Test/Indexer/NoMissing.hs create mode 100644 test/data/Indexer/Small.agda diff --git a/agda-language-server.cabal b/agda-language-server.cabal index 7592b1b..e04e290 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -180,6 +180,7 @@ test-suite als-test main-is: Test.hs other-modules: Test.Indexer.Invariants + Test.Indexer.NoMissing Test.Indexer.NoOverlap Test.LSP Test.Model diff --git a/src/Indexer.hs b/src/Indexer.hs index 315c4c9..9b65b45 100644 --- a/src/Indexer.hs +++ b/src/Indexer.hs @@ -1,7 +1,6 @@ module Indexer (indexFile) where -import Agda.Interaction.FindFile (SourceFile (SourceFile)) -import qualified Agda.Interaction.FindFile as Imp +import Agda.Interaction.FindFile (SourceFile (SourceFile), srcFilePath) import qualified Agda.Interaction.Imports as Imp import qualified Agda.Interaction.Imports.More as Imp import Agda.Interaction.Library (getPrimitiveLibDir) @@ -34,12 +33,12 @@ indexFile src = do -- Now reset the options TCM.setCommandLineOptions . TCM.stPersistentOptions . TCM.stPersistentState =<< TCM.getTC - TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (Imp.srcFilePath $ Imp.srcOrigin src) + TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (srcFilePath $ Imp.srcOrigin src) - TCM.localTC (\e -> e {TCM.envCurrentPath = Just (Imp.srcFilePath $ Imp.srcOrigin src)}) $ do + TCM.localTC (\e -> e {TCM.envCurrentPath = Just (srcFilePath $ Imp.srcOrigin src)}) $ do let topLevel = TopLevel - (Imp.srcFilePath $ Imp.srcOrigin src) + (srcFilePath $ Imp.srcOrigin src) (Imp.srcModuleName src) (C.modDecls $ Imp.srcModule src) ast <- TCM.liftTCM $ toAbstract topLevel diff --git a/src/Server/Model/AgdaFile.hs b/src/Server/Model/AgdaFile.hs index 3298f97..b6c0941 100644 --- a/src/Server/Model/AgdaFile.hs +++ b/src/Server/Model/AgdaFile.hs @@ -9,7 +9,8 @@ module Server.Model.AgdaFile where import qualified Agda.Syntax.Abstract as A -import Agda.Utils.Lens (Lens', over, (<&>)) +import Agda.Syntax.Common.Pretty (Pretty, pretty, prettyAssign, prettyMap, text, vcat) +import Agda.Utils.Lens (Lens', over, (<&>), (^.)) import Control.Monad (forM) import Data.Foldable (fold) import Data.Map (Map) @@ -22,6 +23,13 @@ data AgdaFile = AgdaFile _agdaFileRefs :: !(Map A.QName [Ref]) } +instance Pretty AgdaFile where + pretty agdaFile = + vcat + [ prettyAssign (text "symbols", prettyMap $ Map.toList $ agdaFile ^. agdaFileSymbols), + prettyAssign (text "refs", prettyMap $ Map.toList $ agdaFile ^. agdaFileRefs) + ] + emptyAgdaFile :: AgdaFile emptyAgdaFile = AgdaFile Map.empty Map.empty @@ -44,5 +52,3 @@ insertRef ambiguousName ref = over agdaFileRefs $ appEndo $ foldMap (\name -> Endo $ Map.insertWith (<>) name [ref]) (A.unAmbQ ambiguousName) - --- Map.insertWith (<>) name [ref] diff --git a/src/Server/Model/Symbol.hs b/src/Server/Model/Symbol.hs index e50727f..1ea8f02 100644 --- a/src/Server/Model/Symbol.hs +++ b/src/Server/Model/Symbol.hs @@ -7,7 +7,7 @@ module Server.Model.Symbol where import qualified Agda.Syntax.Abstract as A -import Agda.Syntax.Common.Pretty (Doc, Pretty, comma, parens, pretty, pshow, text, (<+>)) +import Agda.Syntax.Common.Pretty (Doc, Pretty, comma, parens, parensNonEmpty, pretty, pshow, text, (<+>)) import Agda.Syntax.Position (Position, PositionWithoutFile) import qualified Language.LSP.Protocol.Types as LSP import Language.LSP.Protocol.Types.More () @@ -30,6 +30,9 @@ data SymbolKind | Unknown deriving (Show, Eq) +instance Pretty SymbolKind where + pretty = pshow + instance Semigroup SymbolKind where Unknown <> k = k k <> _k = k @@ -40,6 +43,11 @@ data SymbolInfo = SymbolInfo symbolParent :: !(Maybe A.QName) } +instance Pretty SymbolInfo where + pretty symbolInfo = + pretty (symbolKind symbolInfo) + <+> parensNonEmpty (pretty $ symbolType symbolInfo) + data RefKind = -- | The symbol is being declared. There should be at most one declaration -- for any given symbol (in correct Agda code). Roughly speaking, this is diff --git a/test/Test/Indexer/Invariants.hs b/test/Test/Indexer/Invariants.hs index dca595e..bdc067c 100644 --- a/test/Test/Indexer/Invariants.hs +++ b/test/Test/Indexer/Invariants.hs @@ -1,6 +1,6 @@ module Test.Indexer.Invariants (tests) where -import Agda.Interaction.FindFile (SourceFile (SourceFile)) +import Agda.Interaction.FindFile (SourceFile (SourceFile), srcFilePath) import qualified Agda.Interaction.Imports as Imp import Agda.Interaction.Options (defaultOptions) import qualified Agda.TypeChecking.Monad as TCM @@ -20,6 +20,7 @@ import Monad (runServerM) import Server.Model.AgdaFile (AgdaFile, agdaFileRefs) import Server.Model.Monad (withAgdaLibFor) import System.FilePath (takeBaseName) +import Test.Indexer.NoMissing (testNoMissing) import Test.Indexer.NoOverlap (testNoOverlap) import Test.Tasty (TestTree, testGroup) import Test.Tasty.Golden (findByExtension) @@ -29,26 +30,38 @@ import qualified TestData tests :: IO TestTree tests = do inPaths <- findByExtension [".agda"] "test/data/Indexer" - namedFiles <- forM inPaths $ \inPath -> do + files <- forM inPaths $ \inPath -> do let testName = takeBaseName inPath uri = LSP.filePathToUri inPath model <- TestData.getModel - file <- LSP.runLspT undefined $ do + (file, interface) <- LSP.runLspT undefined $ do env <- TestData.getServerEnv model runServerM env $ do + interface <- withAgdaLibFor uri $ do + TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions + absInPath <- liftIO $ absolute inPath + let srcFile = SourceFile absInPath + src <- TCM.liftTCM $ Imp.parseSource srcFile + + TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (srcFilePath $ Imp.srcOrigin src) + checkResult <- TCM.liftTCM $ Imp.typeCheckMain Imp.TypeCheck src + return $ Imp.crInterface checkResult + withAgdaLibFor uri $ do TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions absInPath <- liftIO $ absolute inPath let srcFile = SourceFile absInPath src <- TCM.liftTCM $ Imp.parseSource srcFile - indexFile src + agdaFile <- indexFile src + return (agdaFile, interface) - return (testName, file) + return (testName, file, interface) return $ testGroup "Invariants" - [ testGroup "No reference overlap" (uncurry testNoOverlap <$> namedFiles) + [ testGroup "No reference overlap" ((\(name, file, _interface) -> testNoOverlap name file) <$> files), + testGroup "No missing references" ((\(name, file, interface) -> testNoMissing name file interface) <$> files) ] diff --git a/test/Test/Indexer/NoMissing.hs b/test/Test/Indexer/NoMissing.hs new file mode 100644 index 0000000..69525ce --- /dev/null +++ b/test/Test/Indexer/NoMissing.hs @@ -0,0 +1,82 @@ +-- | Check that highlighting data doesn't show more references than we have +-- `Ref`s. We expect to sometimes pick up references that highlighting does not, +-- so it's okay if we have more. +module Test.Indexer.NoMissing (testNoMissing) where + +import Agda.Interaction.Highlighting.Precise (Aspects, HighlightingInfo) +import qualified Agda.Interaction.Highlighting.Precise as HL +import Agda.Position (FromOffset, fromOffset, makeFromOffset) +import Agda.Syntax.Common.Pretty (Pretty, align, pretty, prettyList, prettyShow, pshow, text, vcat, (<+>)) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.Utils.Lens ((^.)) +import Agda.Utils.Maybe (isJust, isNothing) +import Agda.Utils.RangeMap (PairInt (PairInt), RangeMap (rangeMap)) +import Control.Monad (forM_, guard) +import Control.Monad.Writer.CPS (Writer, execWriter, tell) +import qualified Data.Map as Map +import Data.Strict (Pair ((:!:))) +import qualified Data.Strict as Strict +import qualified Language.LSP.Protocol.Types as LSP +import Server.Model.AgdaFile (AgdaFile, agdaFileRefs) +import Server.Model.Symbol (Ref (refRange)) +import Test.Tasty (TestTree) +import Test.Tasty.HUnit (assertFailure, testCase) + +data MissingRefError = MissingRefError + { mreAspects :: !Aspects, + mreRange :: !LSP.Range + } + +instance Pretty MissingRefError where + pretty err = + text "Missing ref error at" + <+> pretty (mreRange err) + <+> text "with aspects" + <+> pshow (mreAspects err) + + prettyList = \case + [] -> text "No missing ref errors" + [err] -> pretty err + errs -> align 5 $ (\err -> ("-", vcat [pretty err, text ""])) <$> errs + +areAspectsRef :: Aspects -> Bool +areAspectsRef aspects = case HL.aspect aspects of + Just HL.PrimitiveType -> True + Just (HL.Name _ _) -> True + _ -> False + +highlightingRefRanges :: FromOffset -> HighlightingInfo -> [(Aspects, LSP.Range)] +highlightingRefRanges table highlightingInfo = do + (startOffset, PairInt (endOffset :!: aspects)) <- Map.toList $ rangeMap highlightingInfo + guard $ areAspectsRef aspects + let (startLine, startChar) = fromOffset table startOffset + startPos = LSP.Position (fromIntegral startLine) (fromIntegral startChar - 1) + (endLine, endChar) = fromOffset table (endOffset - 1) + endPos = LSP.Position (fromIntegral endLine) (fromIntegral endChar) + range = LSP.Range startPos endPos + return (aspects, range) + +hasCorrespondingRef :: AgdaFile -> Aspects -> LSP.Range -> Bool +hasCorrespondingRef agdaFile aspects range = + let refs = concat $ Map.elems $ agdaFile ^. agdaFileRefs + in isNothing (HL.definitionSite aspects) + || any (\ref -> refRange ref == range) refs + +checkCorrespondingRef :: AgdaFile -> Aspects -> LSP.Range -> Writer [MissingRefError] () +checkCorrespondingRef agdaFile aspects range = + if hasCorrespondingRef agdaFile aspects range + then return () + else tell $ [MissingRefError aspects range] + +testNoMissing :: String -> AgdaFile -> TCM.Interface -> TestTree +testNoMissing name agdaFile interface = testCase name $ do + let highlighting = TCM.iHighlighting interface + let table = makeFromOffset $ Strict.toStrict $ TCM.iSource interface + let highlightingRanges = highlightingRefRanges table highlighting + + let errors = execWriter $ forM_ highlightingRanges $ \(aspects, range) -> + checkCorrespondingRef agdaFile aspects range + + case errors of + [] -> return () + _ -> assertFailure $ prettyShow errors diff --git a/test/Test/Indexer/NoOverlap.hs b/test/Test/Indexer/NoOverlap.hs index 9470604..9f24df3 100644 --- a/test/Test/Indexer/NoOverlap.hs +++ b/test/Test/Indexer/NoOverlap.hs @@ -1,3 +1,5 @@ +-- | Check that `Ref`s don't overlap, so that there is only one `Ref` instance +-- per actual reference. module Test.Indexer.NoOverlap (testNoOverlap) where import qualified Agda.Syntax.Abstract as A diff --git a/test/data/Indexer/Basic.agda b/test/data/Indexer/Basic.agda index 3ddbb80..43a86ef 100644 --- a/test/data/Indexer/Basic.agda +++ b/test/data/Indexer/Basic.agda @@ -52,3 +52,24 @@ record World : Set where earth : World earth .World.north = test earth .World.south = test + +interleaved mutual + record MutualRecord (A : Set) : Set + data MutualData : Set + data MutualData' : Set + mutualFun : MutualRecord MutualData -> MutualRecord MutualData + + record MutualRecord A where + constructor makeMutualRecord + field + mutFieldX : A + field mutFieldY : Nat + + data MutualData where + mutCtorX : MutualData + + data _ where + mutCtorX' : MutualData' + mutCtorY : MutualData + + mutualFun = id diff --git a/test/data/Indexer/Small.agda b/test/data/Indexer/Small.agda new file mode 100644 index 0000000..56db13e --- /dev/null +++ b/test/data/Indexer/Small.agda @@ -0,0 +1 @@ +module Small where \ No newline at end of file From 6e77a52970d555ab806e248bb59ad3626f0ca37a Mon Sep 17 00:00:00 2001 From: nvarner Date: Fri, 15 Aug 2025 16:52:53 -0400 Subject: [PATCH 06/23] respect arg info origin in indexer --- agda-language-server.cabal | 8 +- src/Agda/Syntax/Abstract/More.hs | 181 +++++++++++++++++++++++ src/Indexer/Indexer.hs | 45 ++++-- test/data/AST/Basic | 237 ++++++++++++++++++++++++++++++ test/data/AST/FunWithoutDeclOrDef | 34 +++++ test/data/AST/Module | 42 ++++++ test/data/AST/Mutual | 133 +++++++++++++++++ test/data/AST/Record | 68 +++++++++ test/data/AST/Small | 6 + test/data/Indexer/Module.agda | 12 ++ 10 files changed, 747 insertions(+), 19 deletions(-) create mode 100644 src/Agda/Syntax/Abstract/More.hs create mode 100644 test/data/AST/Basic create mode 100644 test/data/AST/FunWithoutDeclOrDef create mode 100644 test/data/AST/Module create mode 100644 test/data/AST/Mutual create mode 100644 test/data/AST/Record create mode 100644 test/data/AST/Small create mode 100644 test/data/Indexer/Module.agda diff --git a/agda-language-server.cabal b/agda-language-server.cabal index e04e290..e8b0e64 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -53,6 +53,7 @@ library Agda.IR Agda.Parser Agda.Position + Agda.Syntax.Abstract.More Control.Concurrent.SizedChan Indexer Indexer.Indexer @@ -171,8 +172,7 @@ executable als if arch(wasm32) build-depends: unix >=2.8.0.0 && <2.9 - ghc-options: -with-rtsopts=-V1 - else + if !arch(wasm32) ghc-options: -threaded -with-rtsopts=-N test-suite als-test @@ -194,6 +194,7 @@ test-suite als-test Agda.IR Agda.Parser Agda.Position + Agda.Syntax.Abstract.More Control.Concurrent.SizedChan Indexer Indexer.Indexer @@ -270,6 +271,5 @@ test-suite als-test if arch(wasm32) build-depends: unix >=2.8.0.0 && <2.9 - ghc-options: -with-rtsopts=-V1 - else + if !arch(wasm32) ghc-options: -threaded -with-rtsopts=-N diff --git a/src/Agda/Syntax/Abstract/More.hs b/src/Agda/Syntax/Abstract/More.hs new file mode 100644 index 0000000..7582e9b --- /dev/null +++ b/src/Agda/Syntax/Abstract/More.hs @@ -0,0 +1,181 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} + +module Agda.Syntax.Abstract.More () where + +import Agda.Syntax.Abstract +import Agda.Syntax.Common +import Agda.Syntax.Common (ArgInfo (argInfoOrigin)) +import Agda.Syntax.Common.Pretty +import Agda.Syntax.Concrete (TacticAttribute' (theTacticAttribute)) +import Agda.Syntax.Info +import Agda.Utils.Functor ((<&>)) +import Data.Foldable (Foldable (toList)) +import qualified Data.Map as Map + +instance Pretty Declaration where + pretty decl = prettyAssign $ case decl of + Axiom kindOfName _defInfo _argInfo _polarities name type' -> + ( text "Axiom", + prettyMap + [ (text "kindOfName", pshow kindOfName), + (text "name", pretty name), + (text "type", pretty type') + ] + ) + Generalize _namesInType _defInfo _argInfo name type' -> + ( text "Generalize", + prettyMap + [ (text "name", pretty name), + (text "type", pretty type') + ] + ) + Field _defInfo name type' -> + ( text "Field", + prettyMap + [ (text "name", pretty name), + (text "type", pretty type') + ] + ) + Primitive _defInfo name type' -> + ( text "Primitive", + prettyMap + [ (text "name", pretty name), + (text "type", pretty type') + ] + ) + Mutual _mutualInfo decls -> (text "Mutual", pretty decls) + Section _range _erased moduleName genTel decls -> + ( text "Section", + prettyMap + [ (text "moduleName", pretty moduleName), + (text "genTel", pretty genTel), + (text "decls", pretty decls) + ] + ) + Apply _moduleInfo _erased moduleName _moduleApp _scopeCopyInfo _importDirective -> + (text "Apply", pretty moduleName) + Import _moduleInfo moduleName _importDirective -> (text "Import", pretty moduleName) + Pragma _range _pragma -> (text "Pragma", mempty) + Open _moduleInfo moduleName _importDirective -> + (text "Open", pretty moduleName) + FunDef _defInfo name clauses -> + ( text "FunDef", + prettyMap + [ (text "name", pretty name), + (text "clauses", pretty clauses) + ] + ) + DataSig _defInfo _erased name _genTel type' -> + ( text "DataSig", + prettyMap + [ (text "name", pretty name), + (text "type", pretty type') + ] + ) + DataDef _defIngo name _univCheck _dataDefParams _ctors -> + (text "DataDef", prettyMap [(text "name", pretty name)]) + RecSig _defInfo _erased name genTel type' -> + ( text "RecSig", + prettyMap + [ (text "name", pretty name), + (text "type", pretty type') + ] + ) + RecDef _defInfo name _univCheck _recDirs _dataDefParams type' decls -> + ( text "RecDef", + prettyMap + [ (text "name", pretty name), + (text "type", pretty type'), + (text "decls", pretty decls) + ] + ) + PatternSynDef name _args _body -> (text "PatternSynDef", pretty name) + -- ... + ScopedDecl scopeInfo decls -> (text "ScopedDecl", pretty decls) + -- ... + _ -> ("Decl", mempty) + +instance Pretty Expr where + pretty expr = prettyAssign $ case expr of + Var name -> (text "Var", pretty name) + Def' name _suffix -> (text "Def'", pretty name) + Proj _origin name -> (text "Proj", pretty name) + Con name -> (text "Con", pretty name) + PatternSyn name -> (text "PatternSyn", pretty name) + Macro name -> (text "Macro", pretty name) + -- ... + App _appInfo f arg -> + ( text "App", + prettyMap + [ (text "f", pretty f), + (text "arg", pretty arg) + ] + ) + -- ... + Pi _exprInfo dom codom -> + ( text "Pi", + prettyMap + [ (text "dom", pretty dom), + (text "codom", pretty codom) + ] + ) + Generalized dom codom -> + ( text "Generalized", + prettyMap + [ (text "dom", pretty $ toList dom), + (text "codom", pretty codom) + ] + ) + Fun _exprInfo dom codom -> + ( text "Fun", + prettyMap + [ (text "dom", pretty dom), + (text "codom", pretty codom) + ] + ) + -- ... + ScopedExpr _scopeInfo expr -> (text "ScopedExpr", pretty expr) + -- ... + _ -> ("Expr", mempty) + +debugNamedBinder :: NamedArg Binder -> Doc +debugNamedBinder (Arg argInfo binder) = pshow (argInfoOrigin argInfo) <+> pretty binder + +instance Pretty TypedBinding where + pretty = \case + TBind _range _typedBindingInfo binders type' -> + parens (prettyList (debugNamedBinder <$> toList binders) <+> colon <+> pretty type') + TLet _range _letBindings -> text "TLet" + +instance Pretty LetBinding where + pretty = \case + LetBind _letInfo _argInfo name type' expr -> + text "let" <+> pretty (unBind name) <+> text "=" <+> pretty expr + LetPatBind _letInfo pat expr -> + text "letPat" <+> pretty pat <+> text "=" <+> pretty expr + _ -> text "LetBinding" + +instance Pretty Binder where + pretty binder = pretty $ unBind $ binderName binder + +instance (Pretty t) => Pretty (DefInfo' t) where + pretty defInfo = + align + 20 + [("DefInfo", prettyMap [(text "defTactic", defTactic defInfo)])] + +instance Pretty GeneralizeTelescope where + pretty genTel = + align + 20 + [ ( "GeneralizeTelescope", + prettyMap + [ (text "generalizeTelVars", prettyMap $ Map.toList $ generalizeTelVars genTel), + (text "generalizeTel", pretty $ show <$> generalizeTel genTel) + ] + ) + ] + +instance Pretty (Clause' lhs) where + pretty clause = text "clause" diff --git a/src/Indexer/Indexer.hs b/src/Indexer/Indexer.hs index a490936..3f87951 100644 --- a/src/Indexer/Indexer.hs +++ b/src/Indexer/Indexer.hs @@ -20,6 +20,7 @@ import Agda.Utils.Functor ((<&>)) import Agda.Utils.List1 (List1) import qualified Agda.Utils.List1 as List1 import Agda.Utils.Maybe (whenJust) +import Agda.Utils.Monad (when) import Data.Foldable (forM_, traverse_) import qualified Data.Set as Set import Data.Void (absurd) @@ -59,10 +60,13 @@ class Indexable a where instance Indexable A.Declaration where index = \case A.Axiom kindOfName defInfo _argInfo _polarities name type' -> do + -- TODO: what does the `ArgInfo` mean? + -- Includes postulates, function declarations tellDecl name kindOfName type' index defInfo index type' A.Generalize _generalizeVars defInfo _argInfo name type' -> do + -- TODO: what does the `ArgInfo` mean? tellDecl name GeneralizeVar type' index defInfo index type' @@ -175,7 +179,9 @@ instance Indexable A.Expr where index exprF case funNameFromExpr exprF of Just name -> indexNamedArgs name [exprArg] - Nothing -> index $ C.namedThing $ C.unArg exprArg + Nothing -> + when (C.argInfoOrigin (C.argInfo exprArg) == C.UserWritten) $ do + index $ C.namedThing $ C.unArg exprArg A.WithApp _appInfo exprF exprArgs -> do index exprF index exprArgs @@ -266,7 +272,10 @@ instance (Indexable a) => Indexable [a] instance (Indexable a) => Indexable (List1 a) -instance (Indexable a) => Indexable (C.Arg a) +instance (Indexable a) => Indexable (C.Arg a) where + index (C.Arg argInfo x) = + when (C.argInfoOrigin argInfo == C.UserWritten) $ + index x instance Indexable A.TacticAttribute @@ -276,15 +285,17 @@ instance Indexable A.DefInfo where indexNamedArgs :: (AmbiguousNameLike n, Indexable a) => n -> [C.NamedArg a] -> IndexerM () indexNamedArgs headNameLike args = do let headName = toAmbiguousQName headNameLike - forM_ args $ \(C.Arg _argInfo (C.Named maybeName x)) -> do - whenJust maybeName $ tellNamedArgUsage headName - index x + forM_ args $ \(C.Arg argInfo (C.Named maybeName x)) -> + when (C.argInfoOrigin argInfo == C.UserWritten) $ do + whenJust maybeName $ tellNamedArgUsage headName + index x indexWithExpr :: A.WithExpr -> IndexerM () -indexWithExpr (C.Named maybeName (C.Arg _argInfo expr)) = do - whenJust maybeName $ \(A.BindName name) -> - tellDef name Param UnknownType - index expr +indexWithExpr (C.Named maybeName (C.Arg argInfo expr)) = + when (C.argInfoOrigin argInfo == C.UserWritten) $ do + whenJust maybeName $ \(A.BindName name) -> + tellDef name Param UnknownType + index expr instance Indexable Lit.Literal where index = \case @@ -330,8 +341,9 @@ instance (Indexable a) => Indexable (A.LHSCore' a) where index lhsHead index withPatterns -- TODO: what do the named args mean? - forM_ pats $ \(C.Arg _argInfo (C.Named _name pat)) -> - index pat + forM_ pats $ \(C.Arg argInfo (C.Named _name pat)) -> + when (C.argInfoOrigin argInfo == C.UserWritten) $ + index pat instance Indexable A.LHS where index (A.LHS lhsInfo core) = case Info.lhsEllipsis lhsInfo of @@ -412,6 +424,7 @@ instance Indexable A.ImportDirective where instance Indexable A.LetBinding where index = \case A.LetBind _letInfo _argInfo boundName type' expr -> do + -- TODO: what does the `ArgInfo` mean? tellDef boundName Local type' index type' index expr @@ -431,10 +444,12 @@ instance Indexable A.LetBinding where indexNamedArgBinder :: (TypeLike t, HasParamNames t) => C.NamedArg A.Binder -> t -> IndexerM () -indexNamedArgBinder namedArgBinder typeLike = do - let A.Binder pat name = C.namedThing $ C.unArg namedArgBinder - tellDef name Param typeLike - index pat +indexNamedArgBinder + (C.Arg argInfo (C.Named _maybeArgName (A.Binder pat name))) + typeLike = + when (C.argInfoOrigin argInfo == C.UserWritten) $ do + tellDef name Param typeLike + index pat instance Indexable A.TypedBinding where index = \case diff --git a/test/data/AST/Basic b/test/data/AST/Basic new file mode 100644 index 0000000..49fe7d5 --- /dev/null +++ b/test/data/AST/Basic @@ -0,0 +1,237 @@ +[ScopedDecl -> [Import -> Agda.Primitive], + Section -> + {moduleName -> Basic, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Basic.Nat, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Basic.Nat, dataDefParams -> []}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.one, + type -> ScopedExpr -> ScopedExpr -> Def' -> Basic.Nat}], + ScopedDecl -> + [FunDef -> + {name -> Basic.one, + clauses -> + [lhs = ScopedExpr -> + ScopedExpr -> + App -> + {f -> ScopedExpr -> Con -> Basic.Nat.suc, + arg -> ScopedExpr -> Con -> Basic.Nat.zero}]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.two, + type -> ScopedExpr -> ScopedExpr -> Def' -> Basic.Nat}], + ScopedDecl -> + [FunDef -> + {name -> Basic.two, + clauses -> + [lhs = ScopedExpr -> + ScopedExpr -> + App -> + {f -> ScopedExpr -> Con -> Basic.Nat.suc, + arg -> ScopedExpr -> Def' -> Basic.one}]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Basic.Test, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Basic.Test, dataDefParams -> []}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Basic.Test', + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Basic.Test', dataDefParams -> []}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.hello, + type -> ScopedExpr -> ScopedExpr -> Def' -> Basic.Test}], + ScopedDecl -> + [FunDef -> + {name -> Basic.hello, + clauses -> + [lhs = ScopedExpr -> + Con -> Basic.Test.test | Basic.Test'.test]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Basic.Empty, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Basic.Empty, dataDefParams -> []}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.Not, + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> Agda.Primitive.Set, + codom -> ScopedExpr -> Def' -> Agda.Primitive.Set}}], + ScopedDecl -> + [FunDef -> + {name -> Basic.Not, + clauses -> + [lhs = ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Var -> A, + codom -> ScopedExpr -> Def' -> Basic.Empty}]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.Goodbye, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [FunDef -> + {name -> Basic.Goodbye, + clauses -> + [lhs = ScopedExpr -> + ScopedExpr -> + App -> + {f -> ScopedExpr -> Def' -> Basic.Not, + arg -> ScopedExpr -> Def' -> Basic.Test}]}]]], + ScopedDecl -> + [Axiom -> + {kindOfName -> AxiomName, name -> Basic.A, + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> Basic.Test, + codom -> ScopedExpr -> Def' -> Agda.Primitive.Set}}], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.testId, + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> Basic.Test, + codom -> ScopedExpr -> Def' -> Basic.Test}}], + ScopedDecl -> + [FunDef -> + {name -> Basic.testId, + clauses -> + [lhs = ScopedExpr -> + Con -> Basic.Test.test | Basic.Test'.test]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.id, + type -> + ScopedExpr -> + ScopedExpr -> + Pi -> + {dom -> + [([UserWritten A] : ScopedExpr -> Def' -> Agda.Primitive.Set)], + codom -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Var -> A, + codom -> ScopedExpr -> Var -> A}}}], + ScopedDecl -> + [FunDef -> + {name -> Basic.id, clauses -> [lhs = ScopedExpr -> Expr ->]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.id', + type -> + ScopedExpr -> + ScopedExpr -> + Pi -> + {dom -> + [([UserWritten A] : ScopedExpr -> Def' -> Agda.Primitive.Set)], + codom -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Var -> A, + codom -> ScopedExpr -> Var -> A}}}], + ScopedDecl -> + [FunDef -> + {name -> Basic.id', clauses -> [lhs = ScopedExpr -> Expr ->]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.id'', + type -> + ScopedExpr -> + ScopedExpr -> + Pi -> + {dom -> + [([UserWritten A] : ScopedExpr -> Def' -> Agda.Primitive.Set)], + codom -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Var -> A, + codom -> ScopedExpr -> Var -> A}}}], + ScopedDecl -> + [FunDef -> + {name -> Basic.id'', + clauses -> + [lhs = ScopedExpr -> + Let -> + {bindings -> + [letDeclared x, let x = ScopedExpr -> Var -> x, letDeclared A, + let A = ScopedExpr -> Var -> A], + body -> ScopedExpr -> Var -> x}]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [RecSig -> + {name -> Basic.World, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + type -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [RecDef -> + {name -> Basic.World, dataDefParams -> [], + decls -> + [ScopedDecl -> + [Field -> + {name -> Basic.World.north, + type -> ScopedExpr -> ScopedExpr -> Def' -> Basic.Test}], + ScopedDecl -> + [Field -> + {name -> Basic.World.south, + type -> ScopedExpr -> ScopedExpr -> Def' -> Basic.Test'}]]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.earth, + type -> ScopedExpr -> ScopedExpr -> Def' -> Basic.World}], + ScopedDecl -> + [FunDef -> + {name -> Basic.earth, + clauses -> + [lhs = ScopedExpr -> Con -> Basic.Test.test | Basic.Test'.test, + lhs = ScopedExpr -> + Con -> Basic.Test.test | Basic.Test'.test]}]]]]}] \ No newline at end of file diff --git a/test/data/AST/FunWithoutDeclOrDef b/test/data/AST/FunWithoutDeclOrDef new file mode 100644 index 0000000..b731557 --- /dev/null +++ b/test/data/AST/FunWithoutDeclOrDef @@ -0,0 +1,34 @@ +[ScopedDecl -> [Import -> Agda.Primitive], + Section -> + {moduleName -> FunWithoutDeclOrDef, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> FunWithoutDeclOrDef.Nat, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> + {name -> FunWithoutDeclOrDef.Nat, dataDefParams -> []}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> FunWithoutDeclOrDef.sucsuc, + type -> ScopedExpr -> Expr ->}], + ScopedDecl -> + [FunDef -> + {name -> FunWithoutDeclOrDef.sucsuc, + clauses -> [lhs = ScopedExpr -> Expr ->]}]]], + ScopedDecl -> + [Axiom -> + {kindOfName -> AxiomName, name -> FunWithoutDeclOrDef.sucsucsuc, + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> FunWithoutDeclOrDef.Nat, + codom -> ScopedExpr -> Def' -> FunWithoutDeclOrDef.Nat}}]]}] \ No newline at end of file diff --git a/test/data/AST/Module b/test/data/AST/Module new file mode 100644 index 0000000..69683cc --- /dev/null +++ b/test/data/AST/Module @@ -0,0 +1,42 @@ +[ScopedDecl -> [Import -> Agda.Primitive], + Section -> + {moduleName -> Module, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Module.Nat, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Module.Nat, dataDefParams -> []}]]], + ScopedDecl -> + [Section -> + {moduleName -> Module.M, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Module.M.f, + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> Module.Nat, + codom -> ScopedExpr -> Def' -> Module.Nat}}], + ScopedDecl -> + [FunDef -> + {name -> Module.M.f, clauses -> [lhs = ScopedExpr -> Var -> n]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Module.M.N, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Module.M.N, dataDefParams -> []}]]]]}]]}] \ No newline at end of file diff --git a/test/data/AST/Mutual b/test/data/AST/Mutual new file mode 100644 index 0000000..3afcbad --- /dev/null +++ b/test/data/AST/Mutual @@ -0,0 +1,133 @@ +[ScopedDecl -> [Import -> Agda.Primitive], + Section -> + {moduleName -> Mutual, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Mutual.Nat, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Mutual.Nat, dataDefParams -> []}]]], + ScopedDecl -> + [Section -> + {moduleName -> Mutual.Forward, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [RecSig -> + {name -> Mutual.Forward.MutualRecord, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, + generalizeTel -> + [([UserWritten A] : ScopedExpr -> + Def' -> + Agda.Primitive.Set), + ([UserWritten n] : ScopedExpr -> + Def' -> Mutual.Nat)]}, + type -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataSig -> + {name -> Mutual.Forward.MutualData, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataSig -> + {name -> Mutual.Forward.MutualData', + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> Mutual.Nat, + codom -> ScopedExpr -> Def' -> Agda.Primitive.Set}}], + ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Mutual.Forward.mutualFun, + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> + ScopedExpr -> + App -> + {f -> + ScopedExpr -> + App -> + {f -> + ScopedExpr -> + Def' -> Mutual.Forward.MutualRecord, + arg -> + ScopedExpr -> + Def' -> Mutual.Forward.MutualData}, + arg -> ScopedExpr -> Con -> Mutual.Nat.zero}, + codom -> + ScopedExpr -> + ScopedExpr -> + App -> + {f -> + ScopedExpr -> + App -> + {f -> + ScopedExpr -> + Def' -> Mutual.Forward.MutualRecord, + arg -> + ScopedExpr -> + Def' -> Mutual.Forward.MutualData}, + arg -> ScopedExpr -> Con -> Mutual.Nat.zero}}}], + ScopedDecl -> + [RecDef -> + {name -> Mutual.Forward.MutualRecord, + dataDefParams -> [UserWritten A, UserWritten m], + decls -> + [ScopedDecl -> + [Field -> + {name -> Mutual.Forward.MutualRecord.mutFieldX, + type -> ScopedExpr -> ScopedExpr -> Var -> A}], + ScopedDecl -> + [Field -> + {name -> Mutual.Forward.MutualRecord.mutFieldY, + type -> ScopedExpr -> ScopedExpr -> Def' -> Mutual.Nat}]]}], + ScopedDecl -> + [DataDef -> + {name -> Mutual.Forward.MutualData, dataDefParams -> []}], + ScopedDecl -> + [DataDef -> + {name -> Mutual.Forward.MutualData', + dataDefParams -> [UserWritten A]}], + ScopedDecl -> + [FunDef -> + {name -> Mutual.Forward.mutualFun, + clauses -> [lhs = ScopedExpr -> Var -> x]}]]]]}], + ScopedDecl -> + [Section -> + {moduleName -> Mutual.Backward, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> AxiomName, name -> Mutual.Backward.MutualData, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [Axiom -> + {kindOfName -> AxiomName, name -> Mutual.Backward.MutualData', + type -> + ScopedExpr -> + ScopedExpr -> + Pi -> + {dom -> + [([UserWritten A] : ScopedExpr -> + Def' -> Agda.Primitive.Set)], + codom -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> Mutual.Nat, + codom -> + ScopedExpr -> Def' -> Agda.Primitive.Set}}}]]]]}]]}] \ No newline at end of file diff --git a/test/data/AST/Record b/test/data/AST/Record new file mode 100644 index 0000000..85f93a6 --- /dev/null +++ b/test/data/AST/Record @@ -0,0 +1,68 @@ +[ScopedDecl -> [Import -> Agda.Primitive], + Section -> + {moduleName -> Record, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Record.Nat, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Record.Nat, dataDefParams -> []}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [RecSig -> + {name -> Record.R, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, + generalizeTel -> + [([UserWritten n] : ScopedExpr -> Def' -> Record.Nat), + ([UserWritten A] : ScopedExpr -> + Fun -> + {dom -> + ScopedExpr -> + Def' -> Record.Nat, + codom -> + ScopedExpr -> + Def' -> + Agda.Primitive.Set}), + ([UserWritten x] : ScopedExpr -> + ScopedExpr -> + App -> + {f -> ScopedExpr -> Var -> A, + arg -> + ScopedExpr -> Var -> n})]}, + type -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [RecDef -> + {name -> Record.R, + dataDefParams -> [UserWritten n, UserWritten A, UserWritten x], + decls -> + [ScopedDecl -> + [Field -> + {name -> Record.R.fieldX, + type -> ScopedExpr -> ScopedExpr -> Def' -> Record.Nat}], + ScopedDecl -> + [Field -> + {name -> Record.R.fieldY, + type -> + ScopedExpr -> + ScopedExpr -> + ScopedExpr -> + App -> + {f -> ScopedExpr -> Var -> A, + arg -> ScopedExpr -> Var -> n}}], + ScopedDecl -> + [Field -> + {name -> Record.R.fieldZ, + type -> + ScopedExpr -> + ScopedExpr -> + ScopedExpr -> + App -> + {f -> ScopedExpr -> Var -> A, + arg -> ScopedExpr -> Proj -> Record.R.fieldX}}]]}]]]]}] \ No newline at end of file diff --git a/test/data/AST/Small b/test/data/AST/Small new file mode 100644 index 0000000..5651642 --- /dev/null +++ b/test/data/AST/Small @@ -0,0 +1,6 @@ +[ScopedDecl -> [Import -> Agda.Primitive], + Section -> + {moduleName -> Small, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> []}] \ No newline at end of file diff --git a/test/data/Indexer/Module.agda b/test/data/Indexer/Module.agda new file mode 100644 index 0000000..6685305 --- /dev/null +++ b/test/data/Indexer/Module.agda @@ -0,0 +1,12 @@ +module Module where + +data Nat : Set where + zero : Nat + suc : Nat -> Nat + +module M where + f : Nat -> Nat + f n = n + + data N : Set where + n : N From 7af7bd24939fb97c34c271ee98edc9db5a96c5be Mon Sep 17 00:00:00 2001 From: nvarner Date: Fri, 15 Aug 2025 16:55:09 -0400 Subject: [PATCH 07/23] deduplicate simultaneous declaration/definition --- src/Indexer/Monad.hs | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) diff --git a/src/Indexer/Monad.hs b/src/Indexer/Monad.hs index 61d4fcf..1af5b42 100644 --- a/src/Indexer/Monad.hs +++ b/src/Indexer/Monad.hs @@ -27,13 +27,14 @@ import qualified Agda.Syntax.Abstract as A import qualified Agda.Syntax.Common as C import Agda.Syntax.Position (HasRange, getRange) import Agda.Utils.IORef (IORef, modifyIORef', newIORef, readIORef) -import Agda.Utils.Lens (over) +import Agda.Utils.Lens (over, (^.)) import Agda.Utils.List1 (List1, concatMap1) import Agda.Utils.Maybe (isNothing) import Control.Applicative ((<|>)) import Control.Monad.IO.Class (MonadIO, liftIO) import Control.Monad.Reader (MonadReader (local), ReaderT (runReaderT), asks) import Control.Monad.Trans (lift) +import Data.Foldable (find) import Data.Map (Map) import qualified Data.Map as Map import qualified Language.LSP.Server as LSP @@ -41,7 +42,7 @@ import Monad (ServerM) import Options (Config) import Server.Model.AgdaFile (AgdaFile, agdaFileRefs, agdaFileSymbols, emptyAgdaFile, insertRef, insertSymbolInfo) import Server.Model.Monad (WithAgdaLibM) -import Server.Model.Symbol (Ref (Ref), RefKind (..), SymbolInfo (..), SymbolKind (..)) +import Server.Model.Symbol (Ref (Ref), RefKind (..), SymbolInfo (..), SymbolKind (..), refKind, refRange) data NamedArgUsage = NamedArgUsage { nauHead :: !A.AmbiguousQName, @@ -81,8 +82,7 @@ type IndexerM = ReaderT Env WithAgdaLibM execIndexerM :: IndexerM a -> WithAgdaLibM AgdaFile execIndexerM x = do env <- initEnv - _ <- runReaderT x env - -- TODO: resolve named arg usages + _ <- runReaderT (x >> postprocess) env liftIO $ readIORef $ envAgdaFile env -------------------------------------------------------------------------------- @@ -167,6 +167,27 @@ withParent nameLike = local $ \e -> e {envParent = Just $ toQName nameLike} -------------------------------------------------------------------------------- +postprocess :: IndexerM () +postprocess = do + agdaFileRef <- asks envAgdaFile + -- TODO: resolve named arg usages + liftIO $ modifyIORef' agdaFileRef $ over agdaFileRefs $ Map.map dedupSimultaneousDeclDef + +-- | We sometimes emit a `Decl` and `Def` for the same source range. For +-- example, we must emit a distinct `Decl` and `Def` when a `data` is declared +-- and defined separately, but not when it is declared and defined all at once. +-- It is harder distinguish these in abstract syntax than to idenfify and +-- correct them at the end. +dedupSimultaneousDeclDef :: [Ref] -> [Ref] +dedupSimultaneousDeclDef refs = + case find (\ref -> refKind ref == Decl) refs of + Nothing -> refs + Just decl -> + let pred ref = not (refKind ref == Def && refRange ref == refRange decl) + in filter pred refs + +-------------------------------------------------------------------------------- + class (AmbiguousNameLike n) => NameLike n where toQName :: n -> A.QName From f5bf5efca701202665a7dc86cdbc036354c44685 Mon Sep 17 00:00:00 2001 From: nvarner Date: Fri, 15 Aug 2025 17:21:00 -0400 Subject: [PATCH 08/23] write ASTs to file for debugging purposes --- .gitignore | 1 + src/Indexer.hs | 49 +++++++++++++++++++++++++++------ test/Test/Indexer/Invariants.hs | 18 ++++++++++-- 3 files changed, 57 insertions(+), 11 deletions(-) diff --git a/.gitignore b/.gitignore index 14ce36d..c978c7c 100644 --- a/.gitignore +++ b/.gitignore @@ -4,6 +4,7 @@ cabal-dev dist dist-* +test/data/AST/ node_modules/ *.o *.hi diff --git a/src/Indexer.hs b/src/Indexer.hs index 9b65b45..d9e1b5f 100644 --- a/src/Indexer.hs +++ b/src/Indexer.hs @@ -1,12 +1,21 @@ -module Indexer (indexFile) where - -import Agda.Interaction.FindFile (SourceFile (SourceFile), srcFilePath) +{-# LANGUAGE CPP #-} + +module Indexer + ( withAstFor, + indexFile, + ) +where + +#if MIN_VERSION_Agda(2,8,0) +#else +import Agda.Interaction.FindFile (srcFilePath) +#endif import qualified Agda.Interaction.Imports as Imp import qualified Agda.Interaction.Imports.More as Imp import Agda.Interaction.Library (getPrimitiveLibDir) import Agda.Interaction.Options (defaultOptions, optLoadPrimitives) import qualified Agda.Syntax.Concrete as C -import Agda.Syntax.Translation.ConcreteToAbstract (ToAbstract (toAbstract), TopLevel (TopLevel)) +import Agda.Syntax.Translation.ConcreteToAbstract (ToAbstract (toAbstract), TopLevel (TopLevel), TopLevelInfo) import Agda.Syntax.Translation.ReflectedToAbstract (toAbstract_) import qualified Agda.TypeChecking.Monad as TCM import Agda.Utils.FileName (AbsolutePath, filePath, mkAbsolute) @@ -22,10 +31,26 @@ import Server.Model.AgdaFile (AgdaFile) import Server.Model.Monad (MonadAgdaLib, WithAgdaLibM) import System.FilePath (()) -indexFile :: - Imp.Source -> - WithAgdaLibM AgdaFile -indexFile src = do +withAstFor :: Imp.Source -> (TopLevelInfo -> WithAgdaLibM a) -> WithAgdaLibM a +#if MIN_VERSION_Agda(2,8,0) +withAstFor src f = do + TCM.liftTCM $ + TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $ + -- Now reset the options + TCM.setCommandLineOptions . TCM.stPersistentOptions . TCM.stPersistentState =<< TCM.getTC + + TCM.modifyTCLens TCM.stModuleToSourceId $ Map.insert (Imp.srcModuleName src) (Imp.srcOrigin src) + + TCM.localTC (\e -> e {TCM.envCurrentPath = Just (TCM.srcFileId $ Imp.srcOrigin src)}) $ do + let topLevel = + TopLevel + (Imp.srcOrigin src) + (Imp.srcModuleName src) + (C.modDecls $ Imp.srcModule src) + ast <- TCM.liftTCM $ toAbstract topLevel + f ast +#else +withAstFor src f = do currentOptions <- TCM.useTC TCM.stPragmaOptions TCM.liftTCM $ @@ -42,7 +67,13 @@ indexFile src = do (Imp.srcModuleName src) (C.modDecls $ Imp.srcModule src) ast <- TCM.liftTCM $ toAbstract topLevel - abstractToIndex ast + f ast +#endif + +indexFile :: + Imp.Source -> + WithAgdaLibM AgdaFile +indexFile src = withAstFor src abstractToIndex -- let options = defaultOptions diff --git a/test/Test/Indexer/Invariants.hs b/test/Test/Indexer/Invariants.hs index bdc067c..8873aba 100644 --- a/test/Test/Indexer/Invariants.hs +++ b/test/Test/Indexer/Invariants.hs @@ -3,6 +3,9 @@ module Test.Indexer.Invariants (tests) where import Agda.Interaction.FindFile (SourceFile (SourceFile), srcFilePath) import qualified Agda.Interaction.Imports as Imp import Agda.Interaction.Options (defaultOptions) +import Agda.Syntax.Abstract.More () +import Agda.Syntax.Common.Pretty (prettyShow) +import Agda.Syntax.Translation.ConcreteToAbstract (TopLevelInfo (topLevelDecls)) import qualified Agda.TypeChecking.Monad as TCM import Agda.Utils.FileName (absolute) import Agda.Utils.Lens ((^.)) @@ -12,14 +15,14 @@ import Data.Foldable (traverse_) import Data.IntMap (IntMap) import qualified Data.IntMap as IntMap import qualified Data.Map as Map -import Indexer (indexFile) +import Indexer (indexFile, withAstFor) import Indexer.Indexer (abstractToIndex) import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.Server as LSP import Monad (runServerM) import Server.Model.AgdaFile (AgdaFile, agdaFileRefs) import Server.Model.Monad (withAgdaLibFor) -import System.FilePath (takeBaseName) +import System.FilePath (takeBaseName, ()) import Test.Indexer.NoMissing (testNoMissing) import Test.Indexer.NoOverlap (testNoOverlap) import Test.Tasty (TestTree, testGroup) @@ -48,6 +51,17 @@ tests = do checkResult <- TCM.liftTCM $ Imp.typeCheckMain Imp.TypeCheck src return $ Imp.crInterface checkResult + ast <- withAgdaLibFor uri $ do + TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions + absInPath <- liftIO $ absolute inPath + let srcFile = SourceFile absInPath + src <- TCM.liftTCM $ Imp.parseSource srcFile + + withAstFor src return + + -- Write the AST to a file for debugging purposes + liftIO $ writeFile ("test/data/AST" testName) $ prettyShow $ topLevelDecls ast + withAgdaLibFor uri $ do TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions absInPath <- liftIO $ absolute inPath From aef4fc1cf71f2d36633159587dbaa8943847bf9f Mon Sep 17 00:00:00 2001 From: nvarner Date: Fri, 15 Aug 2025 17:42:08 -0400 Subject: [PATCH 09/23] don't reindex record type --- src/Indexer/Indexer.hs | 8 +++++--- test/data/Indexer/Record.agda | 12 ++++++++++++ 2 files changed, 17 insertions(+), 3 deletions(-) create mode 100644 test/data/Indexer/Record.agda diff --git a/src/Indexer/Indexer.hs b/src/Indexer/Indexer.hs index 3f87951..e57627e 100644 --- a/src/Indexer/Indexer.hs +++ b/src/Indexer/Indexer.hs @@ -116,11 +116,13 @@ instance Indexable A.Declaration where index defInfo index genTel index type' - A.RecDef defInfo name _univCheck recDirectives dataDefParams type' decls -> do - tellDef name Record type' + A.RecDef defInfo name _univCheck recDirectives dataDefParams _type' decls -> do + -- The type associated with a `RecDef` is a Pi type including the record's + -- fields, which is not what we want. The `RecSig` does have the type we + -- want, so we use that instead. + tellDef name Record UnknownType index defInfo index dataDefParams - index type' withParent name $ do index recDirectives index decls diff --git a/test/data/Indexer/Record.agda b/test/data/Indexer/Record.agda new file mode 100644 index 0000000..3330b2c --- /dev/null +++ b/test/data/Indexer/Record.agda @@ -0,0 +1,12 @@ +module Record where + +data Nat : Set where + zero : Nat + suc : Nat -> Nat + +record R (n : Nat) (A : Nat -> Set) (x : A n) : Set where + constructor makeR + field + fieldX : Nat + fieldY : A n + fieldZ : A fieldX From 2f5152480b1098eed6ed1339c31bf8570a38f3c8 Mon Sep 17 00:00:00 2001 From: nvarner Date: Fri, 15 Aug 2025 18:22:26 -0400 Subject: [PATCH 10/23] deduplicate decl/defs in let bindings --- src/Agda/Syntax/Abstract/More.hs | 30 +++++++++++++++++++++++++----- src/Indexer/Indexer.hs | 2 +- 2 files changed, 26 insertions(+), 6 deletions(-) diff --git a/src/Agda/Syntax/Abstract/More.hs b/src/Agda/Syntax/Abstract/More.hs index 7582e9b..cc003ce 100644 --- a/src/Agda/Syntax/Abstract/More.hs +++ b/src/Agda/Syntax/Abstract/More.hs @@ -79,14 +79,14 @@ instance Pretty Declaration where ( text "RecSig", prettyMap [ (text "name", pretty name), + (text "genTel", pretty genTel), (text "type", pretty type') ] ) - RecDef _defInfo name _univCheck _recDirs _dataDefParams type' decls -> + RecDef _defInfo name _univCheck _recDirs _dataDefParams _type' decls -> ( text "RecDef", prettyMap [ (text "name", pretty name), - (text "type", pretty type'), (text "decls", pretty decls) ] ) @@ -134,11 +134,21 @@ instance Pretty Expr where (text "codom", pretty codom) ] ) + Let _exprInfo bindings body -> + ( text "Let", + prettyMap + [ (text "bindings", pretty bindings), + (text "body", pretty body) + ] + ) -- ... ScopedExpr _scopeInfo expr -> (text "ScopedExpr", pretty expr) -- ... _ -> ("Expr", mempty) +instance (Pretty a) => Pretty (Pattern' a) where + pretty _pat = text "pat" + debugNamedBinder :: NamedArg Binder -> Doc debugNamedBinder (Arg argInfo binder) = pshow (argInfoOrigin argInfo) <+> pretty binder @@ -154,6 +164,7 @@ instance Pretty LetBinding where text "let" <+> pretty (unBind name) <+> text "=" <+> pretty expr LetPatBind _letInfo pat expr -> text "letPat" <+> pretty pat <+> text "=" <+> pretty expr + LetDeclaredVariable name -> text "letDeclared" <+> pretty (unBind name) _ -> text "LetBinding" instance Pretty Binder where @@ -172,10 +183,19 @@ instance Pretty GeneralizeTelescope where [ ( "GeneralizeTelescope", prettyMap [ (text "generalizeTelVars", prettyMap $ Map.toList $ generalizeTelVars genTel), - (text "generalizeTel", pretty $ show <$> generalizeTel genTel) + (text "generalizeTel", pretty $ generalizeTel genTel) ] ) ] -instance Pretty (Clause' lhs) where - pretty clause = text "clause" +instance (Pretty lhs) => Pretty (Clause' lhs) where + pretty (Clause lhs _strippedPats rhs whereDecls _catchall) = + pretty lhs <+> text "=" <+> pretty rhs + +instance Pretty LHS where + pretty _lhs = text "lhs" + +instance Pretty RHS where + pretty = \case + RHS expr _concrete -> pretty expr + _ -> text "rhs" diff --git a/src/Indexer/Indexer.hs b/src/Indexer/Indexer.hs index e57627e..2d46f8a 100644 --- a/src/Indexer/Indexer.hs +++ b/src/Indexer/Indexer.hs @@ -441,7 +441,7 @@ instance Indexable A.LetBinding where tellUsage moduleName index importDirective A.LetDeclaredVariable boundName -> - tellDef boundName Local UnknownType + tellDecl boundName Local UnknownType indexNamedArgBinder :: (TypeLike t, HasParamNames t) => From 5b4f545922c6bc4e70d65820750a2be753c4f177 Mon Sep 17 00:00:00 2001 From: nvarner Date: Fri, 15 Aug 2025 18:35:20 -0400 Subject: [PATCH 11/23] test functions without definitions/declarations --- test/data/Indexer/FunWithoutDeclOrDef.agda | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test/data/Indexer/FunWithoutDeclOrDef.agda diff --git a/test/data/Indexer/FunWithoutDeclOrDef.agda b/test/data/Indexer/FunWithoutDeclOrDef.agda new file mode 100644 index 0000000..86f00bd --- /dev/null +++ b/test/data/Indexer/FunWithoutDeclOrDef.agda @@ -0,0 +1,11 @@ +module FunWithoutDeclOrDef where + +data Nat : Set where + zero : Nat + suc : Nat -> Nat + +-- No declaration +sucsuc = \n -> suc (suc n) + +-- No definition +sucsucsuc : Nat -> Nat From 23c647b2d99cbb31689b877a772b2838ed15071d Mon Sep 17 00:00:00 2001 From: nvarner Date: Mon, 18 Aug 2025 11:00:02 -0400 Subject: [PATCH 12/23] deduplicate data/record params --- agda-language-server.cabal | 2 + src/Agda/Syntax/Abstract/More.hs | 20 ++++- src/Indexer.hs | 24 ++---- src/Indexer/Indexer.hs | 86 +++++++++++---------- src/Indexer/Monad.hs | 128 +++++++++++++++++++------------ src/Indexer/Postprocess.hs | 57 ++++++++++++++ src/Server/Model/AgdaFile.hs | 26 ++++++- src/Server/Model/Symbol.hs | 11 ++- test/Test/Indexer/Invariants.hs | 7 -- test/data/Indexer/Basic.agda | 21 ----- test/data/Indexer/Mutual.agda | 41 ++++++++++ 11 files changed, 281 insertions(+), 142 deletions(-) create mode 100644 src/Indexer/Postprocess.hs create mode 100644 test/data/Indexer/Mutual.agda diff --git a/agda-language-server.cabal b/agda-language-server.cabal index e8b0e64..2356b16 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -58,6 +58,7 @@ library Indexer Indexer.Indexer Indexer.Monad + Indexer.Postprocess Language.LSP.Protocol.Types.More Language.LSP.Protocol.Types.Uri.More Monad @@ -199,6 +200,7 @@ test-suite als-test Indexer Indexer.Indexer Indexer.Monad + Indexer.Postprocess Language.LSP.Protocol.Types.More Language.LSP.Protocol.Types.Uri.More Monad diff --git a/src/Agda/Syntax/Abstract/More.hs b/src/Agda/Syntax/Abstract/More.hs index cc003ce..efd4131 100644 --- a/src/Agda/Syntax/Abstract/More.hs +++ b/src/Agda/Syntax/Abstract/More.hs @@ -73,8 +73,13 @@ instance Pretty Declaration where (text "type", pretty type') ] ) - DataDef _defIngo name _univCheck _dataDefParams _ctors -> - (text "DataDef", prettyMap [(text "name", pretty name)]) + DataDef _defIngo name _univCheck dataDefParams _ctors -> + ( text "DataDef", + prettyMap + [ (text "name", pretty name), + (text "dataDefParams", pretty dataDefParams) + ] + ) RecSig _defInfo _erased name genTel type' -> ( text "RecSig", prettyMap @@ -83,10 +88,11 @@ instance Pretty Declaration where (text "type", pretty type') ] ) - RecDef _defInfo name _univCheck _recDirs _dataDefParams _type' decls -> + RecDef _defInfo name _univCheck _recDirs dataDefParams _type' decls -> ( text "RecDef", prettyMap [ (text "name", pretty name), + (text "dataDefParams", pretty dataDefParams), (text "decls", pretty decls) ] ) @@ -170,6 +176,11 @@ instance Pretty LetBinding where instance Pretty Binder where pretty binder = pretty $ unBind $ binderName binder +instance Pretty LamBinding where + pretty = \case + DomainFree _tacticAttr namedArgBinder -> debugNamedBinder namedArgBinder + DomainFull binding -> pretty binding + instance (Pretty t) => Pretty (DefInfo' t) where pretty defInfo = align @@ -199,3 +210,6 @@ instance Pretty RHS where pretty = \case RHS expr _concrete -> pretty expr _ -> text "rhs" + +instance Pretty DataDefParams where + pretty (DataDefParams _generalized params) = pretty params diff --git a/src/Indexer.hs b/src/Indexer.hs index d9e1b5f..73b13fb 100644 --- a/src/Indexer.hs +++ b/src/Indexer.hs @@ -11,25 +11,15 @@ where import Agda.Interaction.FindFile (srcFilePath) #endif import qualified Agda.Interaction.Imports as Imp -import qualified Agda.Interaction.Imports.More as Imp -import Agda.Interaction.Library (getPrimitiveLibDir) -import Agda.Interaction.Options (defaultOptions, optLoadPrimitives) import qualified Agda.Syntax.Concrete as C import Agda.Syntax.Translation.ConcreteToAbstract (ToAbstract (toAbstract), TopLevel (TopLevel), TopLevelInfo) -import Agda.Syntax.Translation.ReflectedToAbstract (toAbstract_) import qualified Agda.TypeChecking.Monad as TCM -import Agda.Utils.FileName (AbsolutePath, filePath, mkAbsolute) -import Agda.Utils.Monad (bracket_, unlessM, when) -import qualified Agda.Utils.Trie as Trie -import Control.Monad (forM_, void) -import Control.Monad.IO.Class (liftIO) import qualified Data.Map as Map -import qualified Data.Set as Set -import qualified Data.Strict as Strict -import Indexer.Indexer (abstractToIndex) +import Indexer.Indexer (indexAst) +import Indexer.Monad (execIndexerM) +import Indexer.Postprocess (postprocess) import Server.Model.AgdaFile (AgdaFile) -import Server.Model.Monad (MonadAgdaLib, WithAgdaLibM) -import System.FilePath (()) +import Server.Model.Monad (WithAgdaLibM) withAstFor :: Imp.Source -> (TopLevelInfo -> WithAgdaLibM a) -> WithAgdaLibM a #if MIN_VERSION_Agda(2,8,0) @@ -51,8 +41,6 @@ withAstFor src f = do f ast #else withAstFor src f = do - currentOptions <- TCM.useTC TCM.stPragmaOptions - TCM.liftTCM $ TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $ -- Now reset the options @@ -73,7 +61,9 @@ withAstFor src f = do indexFile :: Imp.Source -> WithAgdaLibM AgdaFile -indexFile src = withAstFor src abstractToIndex +indexFile src = withAstFor src $ \ast -> execIndexerM $ do + indexAst ast + postprocess -- let options = defaultOptions diff --git a/src/Indexer/Indexer.hs b/src/Indexer/Indexer.hs index 2d46f8a..5394729 100644 --- a/src/Indexer/Indexer.hs +++ b/src/Indexer/Indexer.hs @@ -3,7 +3,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeSynonymInstances #-} -module Indexer.Indexer (abstractToIndex) where +module Indexer.Indexer (indexAst) where import qualified Agda.Syntax.Abstract as A import qualified Agda.Syntax.Common as C @@ -26,6 +26,7 @@ import qualified Data.Set as Set import Data.Void (absurd) import Indexer.Monad ( AmbiguousNameLike (..), + BindingKind (..), HasParamNames (..), IndexerM, NameLike (..), @@ -33,24 +34,22 @@ import Indexer.Monad SymbolKindLike (..), TypeLike (..), UnknownType (UnknownType), - execIndexerM, + tellBinding, tellDecl, tellDef, + tellDefParams, + tellGenTel, tellImport, tellNamedArgUsage, tellParamNames, tellUsage, + withBindingKind, withParent, ) -import qualified Language.LSP.Server as LSP -import Monad (ServerM) -import Options (Config) -import Server.Model.AgdaFile (AgdaFile) -import Server.Model.Monad (WithAgdaLibM) import Server.Model.Symbol (SymbolKind (..)) -abstractToIndex :: TopLevelInfo -> WithAgdaLibM AgdaFile -abstractToIndex (TopLevelInfo decls _scope) = execIndexerM $ index decls +indexAst :: TopLevelInfo -> IndexerM () +indexAst (TopLevelInfo decls _scope) = index decls class Indexable a where index :: a -> IndexerM () @@ -98,34 +97,41 @@ instance Indexable A.Declaration where A.Open _moduleInfo moduleName importDirective -> do tellUsage moduleName index importDirective - A.FunDef _defInfo name clauses -> do + A.FunDef _defInfo name clauses -> withBindingKind DefBinding $ do + -- function declarations are captured by the `Axiom` case withParent name $ do index clauses - A.DataSig defInfo _erased name genTel type' -> do - tellDecl name Data type' - index defInfo - index genTel - index type' - A.DataDef defInfo name _univCheck dataDefParams constructors -> do - tellDef name Data UnknownType - index defInfo - index dataDefParams - index constructors - A.RecSig defInfo _erased name genTel type' -> do - tellDecl name Record type' - index defInfo - index genTel - index type' - A.RecDef defInfo name _univCheck recDirectives dataDefParams _type' decls -> do - -- The type associated with a `RecDef` is a Pi type including the record's - -- fields, which is not what we want. The `RecSig` does have the type we - -- want, so we use that instead. - tellDef name Record UnknownType - index defInfo - index dataDefParams - withParent name $ do - index recDirectives - index decls + A.DataSig defInfo _erased name genTel type' -> + withBindingKind DeclBinding $ do + tellDecl name Data type' + index defInfo + index genTel + tellGenTel name genTel + index type' + A.DataDef _defInfo name _univCheck dataDefParams constructors -> + withBindingKind DefBinding $ do + tellDef name Data UnknownType + index dataDefParams + tellDefParams name dataDefParams + index constructors + A.RecSig defInfo _erased name genTel type' -> + withBindingKind DeclBinding $ do + tellDecl name Record type' + index defInfo + index genTel + tellGenTel name genTel + index type' + A.RecDef _defInfo name _univCheck recDirectives dataDefParams _type' decls -> + withBindingKind DefBinding $ do + -- The type associated with a `RecDef` is a Pi type including the record's + -- fields, which is not what we want. The `RecSig` does have the type we + -- want, so we use that instead. + tellDef name Record UnknownType + index dataDefParams + tellDefParams name dataDefParams + withParent name $ do + index recDirectives + index decls A.PatternSynDef name bindings pat -> do tellDecl name PatternSyn UnknownType forM_ bindings $ \(C.WithHiding _hiding binding) -> @@ -391,7 +397,7 @@ instance (Indexable a) => Indexable (A.Clause' a) where instance Indexable A.ModuleApplication where index = \case A.SectionApp tele moduleName args -> do - index tele + withBindingKind DeclBinding $ index tele tellUsage moduleName indexNamedArgs moduleName args A.RecordModuleInstance moduleName -> @@ -427,7 +433,7 @@ instance Indexable A.LetBinding where index = \case A.LetBind _letInfo _argInfo boundName type' expr -> do -- TODO: what does the `ArgInfo` mean? - tellDef boundName Local type' + tellBinding boundName Local type' index type' index expr A.LetPatBind _letInfo pat expr -> do @@ -441,6 +447,7 @@ instance Indexable A.LetBinding where tellUsage moduleName index importDirective A.LetDeclaredVariable boundName -> + -- This is always a declaration tellDecl boundName Local UnknownType indexNamedArgBinder :: @@ -450,7 +457,7 @@ indexNamedArgBinder (C.Arg argInfo (C.Named _maybeArgName (A.Binder pat name))) typeLike = when (C.argInfoOrigin argInfo == C.UserWritten) $ do - tellDef name Param typeLike + tellBinding name Param typeLike index pat instance Indexable A.TypedBinding where @@ -474,7 +481,8 @@ instance Indexable A.GeneralizeTelescope where index (A.GeneralizeTel _generalizeVars tel) = index tel instance Indexable A.DataDefParams where - index (A.DataDefParams _generalizeParams params) = index params + index (A.DataDefParams _generalizeParams params) = + withBindingKind DefBinding $ index params instance Indexable A.RecordDirectives where index = \case diff --git a/src/Indexer/Monad.hs b/src/Indexer/Monad.hs index 1af5b42..ac16e94 100644 --- a/src/Indexer/Monad.hs +++ b/src/Indexer/Monad.hs @@ -5,13 +5,21 @@ module Indexer.Monad ( IndexerM, execIndexerM, + modifyAgdaFile', tellParamNames, + DataRecordParams (..), + tellDefParams, + tellGenTel, + getDataRecordParams, tellDef, tellDecl, + tellBinding, tellUsage, tellImport, tellNamedArgUsage, withParent, + BindingKind (..), + withBindingKind, NameLike (..), AmbiguousNameLike (..), SymbolKindLike (..), @@ -25,33 +33,45 @@ where import Agda.Position (toLspRange) import qualified Agda.Syntax.Abstract as A import qualified Agda.Syntax.Common as C -import Agda.Syntax.Position (HasRange, getRange) +import Agda.Syntax.Position (getRange) import Agda.Utils.IORef (IORef, modifyIORef', newIORef, readIORef) -import Agda.Utils.Lens (over, (^.)) import Agda.Utils.List1 (List1, concatMap1) -import Agda.Utils.Maybe (isNothing) import Control.Applicative ((<|>)) import Control.Monad.IO.Class (MonadIO, liftIO) import Control.Monad.Reader (MonadReader (local), ReaderT (runReaderT), asks) import Control.Monad.Trans (lift) -import Data.Foldable (find) import Data.Map (Map) import qualified Data.Map as Map -import qualified Language.LSP.Server as LSP -import Monad (ServerM) -import Options (Config) -import Server.Model.AgdaFile (AgdaFile, agdaFileRefs, agdaFileSymbols, emptyAgdaFile, insertRef, insertSymbolInfo) +import Server.Model.AgdaFile (AgdaFile, emptyAgdaFile, insertRef, insertSymbolInfo) import Server.Model.Monad (WithAgdaLibM) -import Server.Model.Symbol (Ref (Ref), RefKind (..), SymbolInfo (..), SymbolKind (..), refKind, refRange) +import Server.Model.Symbol (Ref (Ref), RefKind (..), SymbolInfo (..), SymbolKind (..)) data NamedArgUsage = NamedArgUsage { nauHead :: !A.AmbiguousQName, nauArg :: !C.NamedName } +data DataRecordParams = DataRecordParams + { drpGenTel :: !(Maybe A.GeneralizeTelescope), + drpParams :: !(Maybe A.DataDefParams) + } + +instance Semigroup DataRecordParams where + DataRecordParams x y <> DataRecordParams x' y' = DataRecordParams (x <|> x') (y <|> y') + +instance Monoid DataRecordParams where + mempty = DataRecordParams Nothing Nothing + +data BindingKind = DeclBinding | DefBinding + +bindingKindToRefKind :: BindingKind -> RefKind +bindingKindToRefKind DeclBinding = Decl +bindingKindToRefKind DefBinding = Def + data Env = Env { envAgdaFile :: !(IORef AgdaFile), envParent :: !(Maybe A.QName), + envBindingKind :: !BindingKind, -- | Parameter names in implicit arguments, such as x in `f {x = y} = y` and -- `g y = f {x = y}`, are represented by strings in abstract syntax. This is -- because we need type checking information to resolve these names, not @@ -66,7 +86,8 @@ data Env = Env -- These are the stored parameter names, indexed by the name of the function -- (or other defined symbol). envParamNames :: !(IORef (Map A.QName [A.QName])), - envNamedArgUsages :: !(IORef [NamedArgUsage]) + envNamedArgUsages :: !(IORef [NamedArgUsage]), + envDataRecordParams :: !(IORef (Map A.QName DataRecordParams)) } initEnv :: (MonadIO m) => m Env @@ -75,31 +96,28 @@ initEnv = do let parent = Nothing paramNames <- liftIO $ newIORef Map.empty namedArgUsages <- liftIO $ newIORef [] - return $ Env agdaFile parent paramNames namedArgUsages + dataRecordParams <- liftIO $ newIORef mempty + return $ Env agdaFile parent DeclBinding paramNames namedArgUsages dataRecordParams type IndexerM = ReaderT Env WithAgdaLibM execIndexerM :: IndexerM a -> WithAgdaLibM AgdaFile execIndexerM x = do env <- initEnv - _ <- runReaderT (x >> postprocess) env + _ <- runReaderT x env liftIO $ readIORef $ envAgdaFile env -------------------------------------------------------------------------------- --- Used when inserting a new `SymbolInfo` into a map already containing a --- `SymbolInfo` for the given symbol -updateSymbolInfo :: SymbolInfo -> SymbolInfo -> SymbolInfo -updateSymbolInfo new old = - SymbolInfo - (symbolKind old <> symbolKind new) - (symbolType old <|> symbolType new) - (symbolParent old <|> symbolParent new) +modifyAgdaFile' :: (AgdaFile -> AgdaFile) -> IndexerM () +modifyAgdaFile' f = do + agdaFileRef <- asks envAgdaFile + liftIO $ modifyIORef' agdaFileRef f tellSymbolInfo' :: A.QName -> SymbolInfo -> IndexerM () tellSymbolInfo' name symbolInfo = do agdaFileRef <- asks envAgdaFile - liftIO $ modifyIORef' agdaFileRef $ insertSymbolInfo updateSymbolInfo name symbolInfo + liftIO $ modifyIORef' agdaFileRef $ insertSymbolInfo name symbolInfo tellSymbolInfo :: (NameLike n, SymbolKindLike s, TypeLike t) => @@ -133,21 +151,51 @@ tellParamNames nameLike hasParamNames = do paramNamesRef <- asks envParamNames liftIO $ modifyIORef' paramNamesRef $ Map.insert name paramNames -tellDef :: +tellDefParams :: (NameLike n) => n -> A.DataDefParams -> IndexerM () +tellDefParams nameLike defParams = do + let name = toQName nameLike + dataRecordParamsRef <- asks envDataRecordParams + liftIO $ + modifyIORef' dataRecordParamsRef $ + Map.insertWith (<>) name (DataRecordParams Nothing (Just defParams)) + +tellGenTel :: (NameLike n) => n -> A.GeneralizeTelescope -> IndexerM () +tellGenTel nameLike genTel = do + let name = toQName nameLike + dataRecordParamsRef <- asks envDataRecordParams + liftIO $ + modifyIORef' dataRecordParamsRef $ + Map.insertWith (<>) name (DataRecordParams (Just genTel) Nothing) + +getDataRecordParams :: IndexerM (Map A.QName DataRecordParams) +getDataRecordParams = do + dataRecordParamsRef <- asks envDataRecordParams + liftIO $ readIORef dataRecordParamsRef + +tellBinding' :: (NameLike n, SymbolKindLike s, TypeLike t, HasParamNames t) => - n -> s -> t -> IndexerM () -tellDef n s t = do + BindingKind -> n -> s -> t -> IndexerM () +tellBinding' b n s t = do tellSymbolInfo n s t - tellRef n Def + tellRef n (bindingKindToRefKind b) tellParamNames n t +tellDef :: + (NameLike n, SymbolKindLike s, TypeLike t, HasParamNames t) => + n -> s -> t -> IndexerM () +tellDef = tellBinding' DefBinding + tellDecl :: (NameLike n, SymbolKindLike s, TypeLike t, HasParamNames t) => n -> s -> t -> IndexerM () -tellDecl n s t = do - tellSymbolInfo n s t - tellRef n Decl - tellParamNames n t +tellDecl = tellBinding' DeclBinding + +tellBinding :: + (NameLike n, SymbolKindLike s, TypeLike t, HasParamNames t) => + n -> s -> t -> IndexerM () +tellBinding n s t = do + b <- asks envBindingKind + tellBinding' b n s t tellUsage :: (AmbiguousNameLike n) => n -> IndexerM () tellUsage n = tellRef n Usage @@ -165,26 +213,8 @@ tellNamedArgUsage headNameLike argName = do withParent :: (NameLike n) => n -> IndexerM a -> IndexerM a withParent nameLike = local $ \e -> e {envParent = Just $ toQName nameLike} --------------------------------------------------------------------------------- - -postprocess :: IndexerM () -postprocess = do - agdaFileRef <- asks envAgdaFile - -- TODO: resolve named arg usages - liftIO $ modifyIORef' agdaFileRef $ over agdaFileRefs $ Map.map dedupSimultaneousDeclDef - --- | We sometimes emit a `Decl` and `Def` for the same source range. For --- example, we must emit a distinct `Decl` and `Def` when a `data` is declared --- and defined separately, but not when it is declared and defined all at once. --- It is harder distinguish these in abstract syntax than to idenfify and --- correct them at the end. -dedupSimultaneousDeclDef :: [Ref] -> [Ref] -dedupSimultaneousDeclDef refs = - case find (\ref -> refKind ref == Decl) refs of - Nothing -> refs - Just decl -> - let pred ref = not (refKind ref == Def && refRange ref == refRange decl) - in filter pred refs +withBindingKind :: BindingKind -> IndexerM a -> IndexerM a +withBindingKind bindingKind = local $ \e -> e {envBindingKind = bindingKind} -------------------------------------------------------------------------------- diff --git a/src/Indexer/Postprocess.hs b/src/Indexer/Postprocess.hs new file mode 100644 index 0000000..2ad2879 --- /dev/null +++ b/src/Indexer/Postprocess.hs @@ -0,0 +1,57 @@ +module Indexer.Postprocess (postprocess) where + +import qualified Agda.Syntax.Abstract as A +import qualified Agda.Syntax.Common as C +import Agda.Utils.Lens (over) +import Control.Arrow ((>>>)) +import Data.Foldable (Foldable (toList), find) +import qualified Data.Map as Map +import Indexer.Monad (DataRecordParams (DataRecordParams), IndexerM, getDataRecordParams, modifyAgdaFile') +import Server.Model.AgdaFile (AgdaFile, agdaFileRefs, mergeSymbols) +import Server.Model.Symbol (Ref, RefKind (..), refKind, refRange) + +postprocess :: IndexerM () +postprocess = do + dataRecordParams <- Map.elems <$> getDataRecordParams + modifyAgdaFile' $ + dedupDataRecordParams dataRecordParams + >>> dedupSimultaneousDeclDef + +-- | We sometimes emit a `Decl` and `Def` for the same source range. For +-- example, we must emit a distinct `Decl` and `Def` when a `data` is declared +-- and defined separately, but not when it is declared and defined all at once. +-- It is harder distinguish these in abstract syntax than to idenfify and +-- correct them at the end. +dedupSimultaneousDeclDef :: AgdaFile -> AgdaFile +dedupSimultaneousDeclDef = over agdaFileRefs $ Map.map worker + where + worker :: [Ref] -> [Ref] + worker refs = + case find (\ref -> refKind ref == Decl) refs of + Nothing -> refs + Just decl -> + let pred ref = not (refKind ref == Def && refRange ref == refRange decl) + in filter pred refs + +dedupDataRecordParams :: [DataRecordParams] -> AgdaFile -> AgdaFile +dedupDataRecordParams dataRecordParams file = foldl' (flip worker) file dataRecordParams + where + namedArgBinderName :: C.NamedArg A.Binder -> A.QName + namedArgBinderName namedArgBinder = + A.qualify_ $ A.unBind $ A.binderName $ C.namedThing $ C.unArg namedArgBinder + typedBindingNames :: A.TypedBinding -> [A.QName] + typedBindingNames = \case + A.TBind _range _typedBindingInfo nabs _type' -> + namedArgBinderName <$> toList nabs + A.TLet _range _letBindings -> [] + lamBindingNames :: A.LamBinding -> [A.QName] + lamBindingNames = \case + A.DomainFree _tacticAttr nab -> [namedArgBinderName nab] + A.DomainFull typedBindings -> typedBindingNames typedBindings + worker :: DataRecordParams -> AgdaFile -> AgdaFile + worker (DataRecordParams (Just genTel) (Just params)) file = + let paramsNames = concatMap lamBindingNames $ A.dataDefParams params + genTelNames = concatMap typedBindingNames $ A.generalizeTel genTel + names = zip paramsNames genTelNames + in foldl' (\file (old, new) -> mergeSymbols old new file) file names + worker _missingParams file = file diff --git a/src/Server/Model/AgdaFile.hs b/src/Server/Model/AgdaFile.hs index b6c0941..2afad8d 100644 --- a/src/Server/Model/AgdaFile.hs +++ b/src/Server/Model/AgdaFile.hs @@ -5,14 +5,14 @@ module Server.Model.AgdaFile agdaFileRefs, insertSymbolInfo, insertRef, + mergeSymbols, ) where import qualified Agda.Syntax.Abstract as A import Agda.Syntax.Common.Pretty (Pretty, pretty, prettyAssign, prettyMap, text, vcat) import Agda.Utils.Lens (Lens', over, (<&>), (^.)) -import Control.Monad (forM) -import Data.Foldable (fold) +import Data.Function ((&)) import Data.Map (Map) import qualified Data.Map as Map import Data.Monoid (Endo (Endo, appEndo)) @@ -40,15 +40,33 @@ agdaFileRefs :: Lens' AgdaFile (Map A.QName [Ref]) agdaFileRefs f a = f (_agdaFileRefs a) <&> \x -> a {_agdaFileRefs = x} insertSymbolInfo :: - (SymbolInfo -> SymbolInfo -> SymbolInfo) -> A.QName -> SymbolInfo -> AgdaFile -> AgdaFile -insertSymbolInfo update name symbolInfo = over agdaFileSymbols $ Map.insertWith update name symbolInfo +insertSymbolInfo name symbolInfo = + over agdaFileSymbols $ Map.insertWith (<>) name symbolInfo insertRef :: A.AmbiguousQName -> Ref -> AgdaFile -> AgdaFile insertRef ambiguousName ref = over agdaFileRefs $ appEndo $ foldMap (\name -> Endo $ Map.insertWith (<>) name [ref]) (A.unAmbQ ambiguousName) + +mergeSymbols :: A.QName -> A.QName -> AgdaFile -> AgdaFile +mergeSymbols old new file = + file + & over + agdaFileSymbols + ( \symbols -> + let (oldSymbolInfo, symbols') = + Map.updateLookupWithKey (\_ _ -> Nothing) old symbols + in Map.alter (<> oldSymbolInfo) new symbols' + ) + & over + agdaFileRefs + ( \refs -> + let (oldRefs, refs') = + Map.updateLookupWithKey (\_ _ -> Nothing) old refs + in Map.alter (<> oldRefs) new refs' + ) diff --git a/src/Server/Model/Symbol.hs b/src/Server/Model/Symbol.hs index 1ea8f02..a45c7b2 100644 --- a/src/Server/Model/Symbol.hs +++ b/src/Server/Model/Symbol.hs @@ -7,8 +7,8 @@ module Server.Model.Symbol where import qualified Agda.Syntax.Abstract as A -import Agda.Syntax.Common.Pretty (Doc, Pretty, comma, parens, parensNonEmpty, pretty, pshow, text, (<+>)) -import Agda.Syntax.Position (Position, PositionWithoutFile) +import Agda.Syntax.Common.Pretty (Doc, Pretty, comma, parensNonEmpty, pretty, pshow, text, (<+>)) +import Control.Applicative ((<|>)) import qualified Language.LSP.Protocol.Types as LSP import Language.LSP.Protocol.Types.More () @@ -48,6 +48,13 @@ instance Pretty SymbolInfo where pretty (symbolKind symbolInfo) <+> parensNonEmpty (pretty $ symbolType symbolInfo) +instance Semigroup SymbolInfo where + new <> old = + SymbolInfo + (symbolKind old <> symbolKind new) + (symbolType old <|> symbolType new) + (symbolParent old <|> symbolParent new) + data RefKind = -- | The symbol is being declared. There should be at most one declaration -- for any given symbol (in correct Agda code). Roughly speaking, this is diff --git a/test/Test/Indexer/Invariants.hs b/test/Test/Indexer/Invariants.hs index 8873aba..6884457 100644 --- a/test/Test/Indexer/Invariants.hs +++ b/test/Test/Indexer/Invariants.hs @@ -8,26 +8,19 @@ import Agda.Syntax.Common.Pretty (prettyShow) import Agda.Syntax.Translation.ConcreteToAbstract (TopLevelInfo (topLevelDecls)) import qualified Agda.TypeChecking.Monad as TCM import Agda.Utils.FileName (absolute) -import Agda.Utils.Lens ((^.)) import Control.Monad (forM) import Control.Monad.IO.Class (liftIO) -import Data.Foldable (traverse_) -import Data.IntMap (IntMap) -import qualified Data.IntMap as IntMap import qualified Data.Map as Map import Indexer (indexFile, withAstFor) -import Indexer.Indexer (abstractToIndex) import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.Server as LSP import Monad (runServerM) -import Server.Model.AgdaFile (AgdaFile, agdaFileRefs) import Server.Model.Monad (withAgdaLibFor) import System.FilePath (takeBaseName, ()) import Test.Indexer.NoMissing (testNoMissing) import Test.Indexer.NoOverlap (testNoOverlap) import Test.Tasty (TestTree, testGroup) import Test.Tasty.Golden (findByExtension) -import Test.Tasty.HUnit (testCase) import qualified TestData tests :: IO TestTree diff --git a/test/data/Indexer/Basic.agda b/test/data/Indexer/Basic.agda index 43a86ef..3ddbb80 100644 --- a/test/data/Indexer/Basic.agda +++ b/test/data/Indexer/Basic.agda @@ -52,24 +52,3 @@ record World : Set where earth : World earth .World.north = test earth .World.south = test - -interleaved mutual - record MutualRecord (A : Set) : Set - data MutualData : Set - data MutualData' : Set - mutualFun : MutualRecord MutualData -> MutualRecord MutualData - - record MutualRecord A where - constructor makeMutualRecord - field - mutFieldX : A - field mutFieldY : Nat - - data MutualData where - mutCtorX : MutualData - - data _ where - mutCtorX' : MutualData' - mutCtorY : MutualData - - mutualFun = id diff --git a/test/data/Indexer/Mutual.agda b/test/data/Indexer/Mutual.agda new file mode 100644 index 0000000..68f4f07 --- /dev/null +++ b/test/data/Indexer/Mutual.agda @@ -0,0 +1,41 @@ +module Mutual where + +data Nat : Set where + zero : Nat + suc : Nat -> Nat + +module Forward where + interleaved mutual + record MutualRecord (A : Set) (n : Nat) : Set + data MutualData : Set + data MutualData' (A : Set) : Nat -> Set + mutualFun : MutualRecord MutualData zero -> MutualRecord MutualData zero + + record MutualRecord A m where + constructor makeMutualRecord + field + mutFieldX : A + field mutFieldY : Nat + + data MutualData where + mutCtorX : MutualData + + data _ where + mutCtorX' : MutualData' A zero + mutCtorY : MutualData + + mutualFun x = x + +module Backward where + interleaved mutual + data MutualData where + mutCtorX : MutualData + + data MutualData' where + mutCtorX' : MutualData' A zero + + data MutualData where + mutCtorY : MutualData + + data MutualData : Set + data MutualData' (A : Set) : Nat -> Set From 63ae4b639922fe61480a65eb1b1bd65b50a5b7b8 Mon Sep 17 00:00:00 2001 From: nvarner Date: Mon, 18 Aug 2025 12:07:14 -0400 Subject: [PATCH 13/23] check for duplicate declarations --- agda-language-server.cabal | 1 + test/Test/Indexer/Invariants.hs | 4 ++- test/Test/Indexer/NoDuplicateDecl.hs | 46 ++++++++++++++++++++++++++++ 3 files changed, 50 insertions(+), 1 deletion(-) create mode 100644 test/Test/Indexer/NoDuplicateDecl.hs diff --git a/agda-language-server.cabal b/agda-language-server.cabal index 2356b16..3c6c8a5 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -181,6 +181,7 @@ test-suite als-test main-is: Test.hs other-modules: Test.Indexer.Invariants + Test.Indexer.NoDuplicateDecl Test.Indexer.NoMissing Test.Indexer.NoOverlap Test.LSP diff --git a/test/Test/Indexer/Invariants.hs b/test/Test/Indexer/Invariants.hs index 6884457..793067d 100644 --- a/test/Test/Indexer/Invariants.hs +++ b/test/Test/Indexer/Invariants.hs @@ -17,6 +17,7 @@ import qualified Language.LSP.Server as LSP import Monad (runServerM) import Server.Model.Monad (withAgdaLibFor) import System.FilePath (takeBaseName, ()) +import Test.Indexer.NoDuplicateDecl (testNoDuplicateDecl) import Test.Indexer.NoMissing (testNoMissing) import Test.Indexer.NoOverlap (testNoOverlap) import Test.Tasty (TestTree, testGroup) @@ -70,5 +71,6 @@ tests = do testGroup "Invariants" [ testGroup "No reference overlap" ((\(name, file, _interface) -> testNoOverlap name file) <$> files), - testGroup "No missing references" ((\(name, file, interface) -> testNoMissing name file interface) <$> files) + testGroup "No missing references" ((\(name, file, interface) -> testNoMissing name file interface) <$> files), + testGroup "No duplicate declarations" ((\(name, file, _interface) -> testNoDuplicateDecl name file) <$> files) ] diff --git a/test/Test/Indexer/NoDuplicateDecl.hs b/test/Test/Indexer/NoDuplicateDecl.hs new file mode 100644 index 0000000..d09869f --- /dev/null +++ b/test/Test/Indexer/NoDuplicateDecl.hs @@ -0,0 +1,46 @@ +module Test.Indexer.NoDuplicateDecl (testNoDuplicateDecl) where + +import qualified Agda.Syntax.Abstract as A +import Agda.Syntax.Common.Pretty (Pretty, align, pretty, prettyList, prettyShow, text, vcat, (<+>)) +import Agda.Utils.Lens ((^.)) +import Control.Monad (forM_) +import Control.Monad.Writer.CPS (Writer, execWriter, tell) +import qualified Data.Map as Map +import Server.Model.AgdaFile (AgdaFile, agdaFileRefs) +import Server.Model.Symbol (Ref, RefKind (..), refKind) +import Test.Tasty (TestTree) +import Test.Tasty.HUnit (assertFailure, testCase) + +data DuplicateDecl = DuplicateDecl + { ddName :: A.QName, + ddDecls :: [Ref] + } + +instance Pretty DuplicateDecl where + pretty dupDecl = + vcat $ + [text "Duplicate declarations for" <+> pretty (ddName dupDecl)] + <> fmap pretty (ddDecls dupDecl) + + prettyList = \case + [] -> text "No duplicate declarations" + [err] -> pretty err + errs -> align 5 $ (\err -> ("-", vcat [pretty err, text ""])) <$> errs + +checkDupDecls :: A.QName -> [Ref] -> Writer [DuplicateDecl] () +checkDupDecls name refs = do + let decls = filter (\ref -> refKind ref == Decl) refs + if length decls > 1 + then tell [DuplicateDecl name decls] + else return () + +testNoDuplicateDecl :: String -> AgdaFile -> TestTree +testNoDuplicateDecl name agdaFile = + testCase name $ do + let symbolRefs = (Map.toList $ agdaFile ^. agdaFileRefs) + let dupDecls = execWriter $ forM_ symbolRefs $ \(name, refs) -> + checkDupDecls name refs + + case dupDecls of + [] -> return () + _ -> assertFailure $ prettyShow dupDecls From da1b1d090eb0662a29fa31b97f2d44261491493d Mon Sep 17 00:00:00 2001 From: nvarner Date: Mon, 18 Aug 2025 13:47:24 -0400 Subject: [PATCH 14/23] rename ServerM to ServerT --- src/Agda.hs | 14 +++++++------- src/Agda/Parser.hs | 4 ++-- src/Monad.hs | 23 +++++++++++++---------- src/Server.hs | 4 ++-- src/Server/Handler.hs | 6 +++--- src/Server/Model/Monad.hs | 10 +++++----- test/Test/Indexer/Invariants.hs | 4 ++-- test/Test/ModelMonad.hs | 6 +++--- 8 files changed, 37 insertions(+), 34 deletions(-) diff --git a/src/Agda.hs b/src/Agda.hs index 53f7330..ff053b1 100644 --- a/src/Agda.hs +++ b/src/Agda.hs @@ -99,7 +99,7 @@ import Agda.Interaction.JSONTop () getAgdaVersion :: String getAgdaVersion = versionWithCommitInfo -start :: ServerM IO () +start :: ServerT IO () start = do env <- ask @@ -136,7 +136,7 @@ start = do Left _err -> return () Right _val -> return () where - loop :: Env -> ServerM CommandM () + loop :: Env -> ServerT CommandM () loop env = do Bench.reset done <- Bench.billTo [] $ do @@ -163,7 +163,7 @@ start = do -- | Convert "CommandReq" to "CommandRes" -sendCommand :: MonadIO m => Value -> ServerM m Value +sendCommand :: MonadIO m => Value -> ServerT m Value sendCommand value = do -- JSON Value => Request => Response case fromJSON value of @@ -179,7 +179,7 @@ sendCommand value = do JSON.Success request -> toJSON <$> handleCommandReq request -handleCommandReq :: MonadIO m => CommandReq -> ServerM m CommandRes +handleCommandReq :: MonadIO m => CommandReq -> ServerT m CommandRes handleCommandReq CmdReqSYN = return $ CmdResACK Agda.getAgdaVersion versionNumber handleCommandReq (CmdReq cmd) = do case parseIOTCM cmd of @@ -194,7 +194,7 @@ handleCommandReq (CmdReq cmd) = do -------------------------------------------------------------------------------- getCommandLineOptions - :: (HasOptions m, MonadIO m) => ServerM m CommandLineOptions + :: (HasOptions m, MonadIO m) => ServerT m CommandLineOptions getCommandLineOptions = do -- command line options from ARGV argv <- asks (optRawAgdaOptions . envOptions) @@ -215,10 +215,10 @@ getCommandLineOptions = do -- | Run a TCM action in IO and throw away all of the errors -- TODO: handle the caught errors -runAgda :: MonadIO m => ServerM TCM a -> ServerM m (Either String a) +runAgda :: MonadIO m => ServerT TCM a -> ServerT m (Either String a) runAgda p = do env <- ask - let p' = runServerM env p + let p' = runServerT env p liftIO $ runTCMTop' ( (Right <$> p') diff --git a/src/Agda/Parser.hs b/src/Agda/Parser.hs index 6e52b91..10cfc07 100644 --- a/src/Agda/Parser.hs +++ b/src/Agda/Parser.hs @@ -15,12 +15,12 @@ import Data.Text (Text, unpack) import qualified Data.Text as Text import qualified Language.LSP.Protocol.Types as LSP import Language.LSP.Server (LspM) -import Monad (ServerM) +import Monad (ServerM, ServerT) import Options (Config) -------------------------------------------------------------------------------- -tokenAt :: LSP.Uri -> Text -> PositionWithoutFile -> ServerM (LspM Config) (Maybe (Token, Text)) +tokenAt :: LSP.Uri -> Text -> PositionWithoutFile -> ServerM (Maybe (Token, Text)) tokenAt uri source position = case LSP.uriToFilePath uri of Nothing -> return Nothing Just filepath -> do diff --git a/src/Monad.hs b/src/Monad.hs index ff0d346..24c091d 100644 --- a/src/Monad.hs +++ b/src/Monad.hs @@ -24,7 +24,8 @@ import Data.Text ) import qualified Language.LSP.Protocol.Types as LSP import Language.LSP.Server - ( MonadLsp, + ( LspM, + MonadLsp, getConfig, ) import Options @@ -62,30 +63,32 @@ createInitEnv options = -------------------------------------------------------------------------------- -- | OUR monad -type ServerM m = ReaderT Env m +type ServerT m = ReaderT Env m -runServerM :: Env -> ServerM m a -> m a -runServerM = flip runReaderT +type ServerM = ServerT (LspM Config) + +runServerT :: Env -> ServerT m a -> m a +runServerT = flip runReaderT -------------------------------------------------------------------------------- -writeLog :: (Monad m, MonadIO m) => Text -> ServerM m () +writeLog :: (Monad m, MonadIO m) => Text -> ServerT m () writeLog msg = do chan <- asks envLogChan liftIO $ writeChan chan msg -writeLog' :: (Monad m, MonadIO m, Show a) => a -> ServerM m () +writeLog' :: (Monad m, MonadIO m, Show a) => a -> ServerT m () writeLog' x = do chan <- asks envLogChan liftIO $ writeChan chan $ pack $ show x -askModel :: (MonadIO m) => ServerM m Model +askModel :: (MonadIO m) => ServerT m Model askModel = do modelVar <- asks envModel liftIO $ readIORef modelVar -- | Provider -provideCommand :: (Monad m, MonadIO m) => IOTCM -> ServerM m () +provideCommand :: (Monad m, MonadIO m) => IOTCM -> ServerT m () provideCommand iotcm = do controller <- asks envCommandController liftIO $ CommandController.put controller iotcm @@ -94,12 +97,12 @@ provideCommand iotcm = do consumeCommand :: (Monad m, MonadIO m) => Env -> m IOTCM consumeCommand env = liftIO $ CommandController.take (envCommandController env) -waitUntilResponsesSent :: (Monad m, MonadIO m) => ServerM m () +waitUntilResponsesSent :: (Monad m, MonadIO m) => ServerT m () waitUntilResponsesSent = do controller <- asks envResponseController liftIO $ ResponseController.setCheckpointAndWait controller -signalCommandFinish :: (Monad m, MonadIO m) => ServerM m () +signalCommandFinish :: (Monad m, MonadIO m) => ServerT m () signalCommandFinish = do writeLog "[Command] Finished" -- send `ResponseEnd` diff --git a/src/Server.hs b/src/Server.hs index db8cfbb..e78166c 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -74,7 +74,7 @@ run options = do staticHandlers = const handlers, interpretHandler = \(ctxEnv, env) -> Iso - { forward = runLspT ctxEnv . runServerM env, + { forward = runLspT ctxEnv . runServerT env, backward = liftIO }, options = lspOptions @@ -104,7 +104,7 @@ syncOptions = } -- handlers of the LSP server -handlers :: Handlers (ServerM (LspM Config)) +handlers :: Handlers ServerM handlers = mconcat [ -- custom methods, not part of LSP diff --git a/src/Server/Handler.hs b/src/Server/Handler.hs index 05f33d0..1f3b64a 100644 --- a/src/Server/Handler.hs +++ b/src/Server/Handler.hs @@ -81,7 +81,7 @@ import Options ( Config initialiseCommandQueue :: IO CommandQueue initialiseCommandQueue = CommandQueue <$> newTChanIO <*> newTVarIO Nothing -runCommandM :: CommandM a -> ServerM (LspM Config) (Either String a) +runCommandM :: CommandM a -> ServerM (Either String a) runCommandM program = do env <- ask runAgda $ do @@ -100,7 +100,7 @@ runCommandM program = do lift $ evalStateT program commandState inferTypeOfText - :: FilePath -> Text -> ServerM (LspM Config) (Either String String) + :: FilePath -> Text -> ServerM (Either String String) inferTypeOfText filepath text = runCommandM $ do -- load first cmd_load' filepath [] True Imp.TypeCheck $ \_ -> return () @@ -114,7 +114,7 @@ inferTypeOfText filepath text = runCommandM $ do render <$> prettyATop typ -onHover :: LSP.Uri -> LSP.Position -> ServerM (LspM Config) (LSP.Hover LSP.|? LSP.Null) +onHover :: LSP.Uri -> LSP.Position -> ServerM (LSP.Hover LSP.|? LSP.Null) onHover uri pos = do result <- LSP.getVirtualFile (LSP.toNormalizedUri uri) case result of diff --git a/src/Server/Model/Monad.hs b/src/Server/Model/Monad.hs index a4068c3..ae66e85 100644 --- a/src/Server/Model/Monad.hs +++ b/src/Server/Model/Monad.hs @@ -32,7 +32,7 @@ import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.Protocol.Types.Uri.More as LSP import Language.LSP.Server (LspM) import qualified Language.LSP.Server as LSP -import Monad (ServerM, askModel) +import Monad (ServerM, ServerT, askModel) import Options (Config) import qualified Server.Model as Model import Server.Model.AgdaFile (AgdaFile) @@ -110,9 +110,9 @@ newtype WithAgdaLibT m a = WithAgdaLibT {unWithAgdaLibT :: ReaderT AgdaLib m a} runWithAgdaLibT :: AgdaLib -> WithAgdaLibT m a -> m a runWithAgdaLibT agdaLib = flip runReaderT agdaLib . unWithAgdaLibT -type WithAgdaLibM = WithAgdaLibT (ServerM (LspM Config)) +type WithAgdaLibM = WithAgdaLibT ServerM -withAgdaLibFor :: LSP.Uri -> WithAgdaLibM a -> ServerM (LspM Config) a +withAgdaLibFor :: LSP.Uri -> WithAgdaLibM a -> ServerM a withAgdaLibFor uri x = do let normUri = LSP.toNormalizedUri uri model <- askModel @@ -165,7 +165,7 @@ runWithAgdaFileT agdaLib agdaFile = let env = WithAgdaFileEnv agdaLib agdaFile in flip runReaderT env . unWithAgdaFileT -type WithAgdaFileM = WithAgdaFileT (ServerM (LspM Config)) +type WithAgdaFileM = WithAgdaFileT ServerM type HandlerWithAgdaFile m = LSP.TRequestMessage m -> @@ -177,7 +177,7 @@ withAgdaFile :: (LSP.HasTextDocument (LSP.MessageParams m) LSP.TextDocumentIdentifier) => LSP.SMethod m -> HandlerWithAgdaFile m -> - LSP.Handlers (ServerM (LspM Config)) + LSP.Handlers ServerM withAgdaFile m handler = LSP.requestHandler m $ \req responder -> do let uri = req ^. LSP.params . LSP.textDocument . LSP.uri normUri = LSP.toNormalizedUri uri diff --git a/test/Test/Indexer/Invariants.hs b/test/Test/Indexer/Invariants.hs index 793067d..a39ee71 100644 --- a/test/Test/Indexer/Invariants.hs +++ b/test/Test/Indexer/Invariants.hs @@ -14,7 +14,7 @@ import qualified Data.Map as Map import Indexer (indexFile, withAstFor) import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.Server as LSP -import Monad (runServerM) +import Monad (runServerT) import Server.Model.Monad (withAgdaLibFor) import System.FilePath (takeBaseName, ()) import Test.Indexer.NoDuplicateDecl (testNoDuplicateDecl) @@ -34,7 +34,7 @@ tests = do (file, interface) <- LSP.runLspT undefined $ do env <- TestData.getServerEnv model - runServerM env $ do + runServerT env $ do interface <- withAgdaLibFor uri $ do TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions absInPath <- liftIO $ absolute inPath diff --git a/test/Test/ModelMonad.hs b/test/Test/ModelMonad.hs index e96eb19..bfc9c09 100644 --- a/test/Test/ModelMonad.hs +++ b/test/Test/ModelMonad.hs @@ -16,7 +16,7 @@ import qualified Language.LSP.Protocol.Message as LSP import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.Protocol.Utils.SMethodMap as SMethodMap import qualified Language.LSP.Server as LSP -import Monad (Env (Env, envModel), ServerM, createInitEnv, runServerM) +import Monad (Env (Env, envModel), ServerT, createInitEnv, runServerT) import Options (Config, defaultOptions, initConfig) import qualified Server.CommandController as CommandController import Server.Model (Model) @@ -70,7 +70,7 @@ runHandler :: LSP.SMethod m -> LSP.TRequestMessage m -> Model -> - LSP.Handlers (ServerM (LSP.LspM Config)) -> + LSP.Handlers (ServerT (LSP.LspM Config)) -> IO (Either (LSP.TResponseError m) (LSP.MessageResult m)) runHandler m request model handlers = do resultRef <- newIORef Nothing @@ -80,7 +80,7 @@ runHandler m request model handlers = do LSP.runLspT undefined $ do env <- TestData.getServerEnv model - runServerM env $ handler request callback + runServerT env $ handler request callback Just result <- readIORef resultRef return result From 8235f2886724ca6a2f3a34f08e4dfaa9effdc152 Mon Sep 17 00:00:00 2001 From: nvarner Date: Sun, 14 Sep 2025 16:24:03 -0500 Subject: [PATCH 15/23] preliminary document symbol handler --- agda-language-server.cabal | 2 + src/Indexer/Monad.hs | 2 +- src/Server.hs | 2 + .../Handler/TextDocument/DocumentSymbol.hs | 46 +++++++++++++++++++ src/Server/Model/AgdaFile.hs | 25 +++++++++- src/Server/Model/Symbol.hs | 38 ++++++++++++++- 6 files changed, 111 insertions(+), 4 deletions(-) create mode 100644 src/Server/Handler/TextDocument/DocumentSymbol.hs diff --git a/agda-language-server.cabal b/agda-language-server.cabal index 3c6c8a5..f1eff71 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -78,6 +78,7 @@ library Server Server.CommandController Server.Handler + Server.Handler.TextDocument.DocumentSymbol Server.Model Server.Model.AgdaFile Server.Model.AgdaLib @@ -221,6 +222,7 @@ test-suite als-test Server Server.CommandController Server.Handler + Server.Handler.TextDocument.DocumentSymbol Server.Model Server.Model.AgdaFile Server.Model.AgdaLib diff --git a/src/Indexer/Monad.hs b/src/Indexer/Monad.hs index ac16e94..543c6d0 100644 --- a/src/Indexer/Monad.hs +++ b/src/Indexer/Monad.hs @@ -127,7 +127,7 @@ tellSymbolInfo nameLike symbolKindLike typeLike = do symbolKind = toSymbolKind symbolKindLike type' <- lift $ toTypeString typeLike parent <- asks envParent - let symbolInfo = SymbolInfo symbolKind type' parent + let symbolInfo = SymbolInfo name symbolKind type' parent tellSymbolInfo' name symbolInfo tellRef' :: A.AmbiguousQName -> Ref -> IndexerM () diff --git a/src/Server.hs b/src/Server.hs index e78166c..a2c7b16 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -28,6 +28,7 @@ import Options import qualified Server.Handler as Handler import Switchboard (Switchboard, agdaCustomMethod) import qualified Switchboard +import Server.Handler.TextDocument.DocumentSymbol (documentSymbolHandler) #if defined(wasm32_HOST_ARCH) import Agda.Utils.IO (catchIO) @@ -117,6 +118,7 @@ handlers = let TRequestMessage _ _ _ (HoverParams (TextDocumentIdentifier uri) pos _workDone) = req result <- Handler.onHover uri pos responder $ Right result, + documentSymbolHandler, -- -- syntax highlighting -- , requestHandler STextDocumentSemanticTokensFull $ \req responder -> do -- result <- Handler.onHighlight (req ^. (params . textDocument . uri)) diff --git a/src/Server/Handler/TextDocument/DocumentSymbol.hs b/src/Server/Handler/TextDocument/DocumentSymbol.hs new file mode 100644 index 0000000..9199d90 --- /dev/null +++ b/src/Server/Handler/TextDocument/DocumentSymbol.hs @@ -0,0 +1,46 @@ +module Server.Handler.TextDocument.DocumentSymbol (documentSymbolHandler) where + +import qualified Agda.Syntax.Abstract as A +import Agda.Syntax.Common.Pretty (prettyShow) +import Agda.Utils.Maybe (fromMaybe, mapMaybe) +import Control.Monad (forM) +import Control.Monad.Trans (lift) +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Data.Text as Text +import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Server as LSP +import Monad (ServerM) +import Server.Model.AgdaFile (AgdaFile, agdaFileSymbols, defNameRange, symbolByName, symbolsByParent) +import Server.Model.Monad (MonadAgdaFile (askAgdaFile), useAgdaFile, withAgdaFile) +import Server.Model.Symbol (SymbolInfo (symbolName), lspSymbolKind, symbolShortName, symbolType) + +documentSymbolHandler :: LSP.Handlers ServerM +documentSymbolHandler = withAgdaFile LSP.SMethod_TextDocumentDocumentSymbol $ \req responder -> do + file <- askAgdaFile + let symbols = symbolsByParent file + let topLevelNames = fromMaybe [] $ Map.lookup Nothing symbols + let topLevelSymbols = mapMaybe (symbolByName file) topLevelNames + topLevelDocumentSymbols <- lift $ forM topLevelSymbols $ symbolToDocumentSymbol file symbols + responder $ Right $ LSP.InR $ LSP.InL topLevelDocumentSymbols + +symbolToDocumentSymbol :: AgdaFile -> Map (Maybe A.QName) [A.QName] -> SymbolInfo -> ServerM LSP.DocumentSymbol +symbolToDocumentSymbol file symbolsByParent symbol = do + let name = symbolName symbol + let range = defNameRange file name + let childrenNames = fromMaybe [] $ Map.lookup (Just name) symbolsByParent + let childrenSymbols = mapMaybe (symbolByName file) childrenNames + childrenDocumentSymbols <- + forM childrenSymbols $ + symbolToDocumentSymbol file symbolsByParent + return $ + LSP.DocumentSymbol + (symbolShortName symbol) + (Text.pack <$> symbolType symbol) + (lspSymbolKind symbol) + Nothing + Nothing + range + range + (Just childrenDocumentSymbols) diff --git a/src/Server/Model/AgdaFile.hs b/src/Server/Model/AgdaFile.hs index 2afad8d..8b04452 100644 --- a/src/Server/Model/AgdaFile.hs +++ b/src/Server/Model/AgdaFile.hs @@ -6,17 +6,24 @@ module Server.Model.AgdaFile insertSymbolInfo, insertRef, mergeSymbols, + symbolByName, + symbolsByParent, + defNameRange, ) where +import Agda.Position (toLspRange) import qualified Agda.Syntax.Abstract as A import Agda.Syntax.Common.Pretty (Pretty, pretty, prettyAssign, prettyMap, text, vcat) +import Agda.Syntax.Position (getRange) import Agda.Utils.Lens (Lens', over, (<&>), (^.)) +import Data.Foldable (find) import Data.Function ((&)) import Data.Map (Map) import qualified Data.Map as Map import Data.Monoid (Endo (Endo, appEndo)) -import Server.Model.Symbol (Ref, SymbolInfo) +import qualified Language.LSP.Protocol.Types as LSP +import Server.Model.Symbol (Ref, SymbolInfo, refIsDef, refRange, symbolParent) data AgdaFile = AgdaFile { _agdaFileSymbols :: !(Map A.QName SymbolInfo), @@ -70,3 +77,19 @@ mergeSymbols old new file = Map.updateLookupWithKey (\_ _ -> Nothing) old refs in Map.alter (<> oldRefs) new refs' ) + +symbolByName :: AgdaFile -> A.QName -> Maybe SymbolInfo +symbolByName agdaFile symbolName = Map.lookup symbolName $ agdaFile ^. agdaFileSymbols + +symbolsByParent :: AgdaFile -> Map (Maybe A.QName) [A.QName] +symbolsByParent agdaFile = + let symbols = Map.toList $ agdaFile ^. agdaFileSymbols + in Map.fromListWith (++) $ (\(symbolName, symbol) -> (symbolParent symbol, [symbolName])) <$> symbols + +refsByName :: AgdaFile -> A.QName -> [Ref] +refsByName agdaFile name = Map.findWithDefault [] name $ agdaFile ^. agdaFileRefs + +defNameRange :: AgdaFile -> A.QName -> LSP.Range +defNameRange agdaFile name = + let defs = find refIsDef $ refsByName agdaFile name + in maybe (toLspRange $ getRange name) refRange defs diff --git a/src/Server/Model/Symbol.hs b/src/Server/Model/Symbol.hs index a45c7b2..291a540 100644 --- a/src/Server/Model/Symbol.hs +++ b/src/Server/Model/Symbol.hs @@ -1,14 +1,19 @@ module Server.Model.Symbol ( SymbolKind (..), SymbolInfo (..), + symbolShortName, + lspSymbolKind, RefKind (..), Ref (..), + refIsDef, ) where import qualified Agda.Syntax.Abstract as A -import Agda.Syntax.Common.Pretty (Doc, Pretty, comma, parensNonEmpty, pretty, pshow, text, (<+>)) +import Agda.Syntax.Common.Pretty (Doc, Pretty, comma, parensNonEmpty, pretty, prettyShow, pshow, text, (<+>)) import Control.Applicative ((<|>)) +import Data.Text (Text) +import qualified Data.Text as Text import qualified Language.LSP.Protocol.Types as LSP import Language.LSP.Protocol.Types.More () @@ -37,8 +42,27 @@ instance Semigroup SymbolKind where Unknown <> k = k k <> _k = k +toLspSymbolKind :: SymbolKind -> LSP.SymbolKind +toLspSymbolKind = \case + Con -> LSP.SymbolKind_Constructor + CoCon -> LSP.SymbolKind_Constructor + Field -> LSP.SymbolKind_Field + PatternSyn -> LSP.SymbolKind_Function + GeneralizeVar -> LSP.SymbolKind_Variable + Macro -> LSP.SymbolKind_Function + Data -> LSP.SymbolKind_Enum + Record -> LSP.SymbolKind_Struct + Fun -> LSP.SymbolKind_Function + Axiom -> LSP.SymbolKind_Constant + Prim -> LSP.SymbolKind_Constant + Module -> LSP.SymbolKind_Module + Param -> LSP.SymbolKind_Variable + Local -> LSP.SymbolKind_Variable + Unknown -> LSP.SymbolKind_Variable + data SymbolInfo = SymbolInfo - { symbolKind :: !SymbolKind, + { symbolName :: !A.QName, + symbolKind :: !SymbolKind, symbolType :: !(Maybe String), symbolParent :: !(Maybe A.QName) } @@ -51,10 +75,17 @@ instance Pretty SymbolInfo where instance Semigroup SymbolInfo where new <> old = SymbolInfo + (symbolName new) (symbolKind old <> symbolKind new) (symbolType old <|> symbolType new) (symbolParent old <|> symbolParent new) +symbolShortName :: SymbolInfo -> Text +symbolShortName = Text.pack . prettyShow . symbolName + +lspSymbolKind :: SymbolInfo -> LSP.SymbolKind +lspSymbolKind = toLspSymbolKind . symbolKind + data RefKind = -- | The symbol is being declared. There should be at most one declaration -- for any given symbol (in correct Agda code). Roughly speaking, this is @@ -95,3 +126,6 @@ instance Pretty Ref where pretty ref = ((prettyAmbiguity ref <+> pretty (refKind ref)) <> comma) <+> pretty (refRange ref) + +refIsDef :: Ref -> Bool +refIsDef ref = refKind ref == Def From 800901d7603276b5d39f9a599e50e02af9bfe106 Mon Sep 17 00:00:00 2001 From: nvarner Date: Sun, 28 Sep 2025 15:24:50 -0500 Subject: [PATCH 16/23] respond to files opening, closing, and saving --- agda-language-server.cabal | 4 + src/Agda/Interaction/Imports/More.hs | 188 +++++++++++++++++- src/Agda/Interaction/Library/More.hs | 39 ++++ src/Language/LSP/Protocol/Types/Uri/More.hs | 14 ++ src/Monad.hs | 30 ++- src/Server.hs | 9 +- .../Handler/TextDocument/DocumentSymbol.hs | 4 +- .../Handler/TextDocument/FileManagement.hs | 47 +++++ src/Server/Model.hs | 32 ++- src/Server/Model/AgdaLib.hs | 71 ++++++- src/Server/Model/Monad.hs | 35 +++- test/Test/Indexer/Invariants.hs | 8 +- test/Test/ModelMonad.hs | 6 +- 13 files changed, 451 insertions(+), 36 deletions(-) create mode 100644 src/Agda/Interaction/Library/More.hs create mode 100644 src/Server/Handler/TextDocument/FileManagement.hs diff --git a/agda-language-server.cabal b/agda-language-server.cabal index f1eff71..787db94 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -50,6 +50,7 @@ library Agda Agda.Convert Agda.Interaction.Imports.More + Agda.Interaction.Library.More Agda.IR Agda.Parser Agda.Position @@ -79,6 +80,7 @@ library Server.CommandController Server.Handler Server.Handler.TextDocument.DocumentSymbol + Server.Handler.TextDocument.FileManagement Server.Model Server.Model.AgdaFile Server.Model.AgdaLib @@ -194,6 +196,7 @@ test-suite als-test Agda Agda.Convert Agda.Interaction.Imports.More + Agda.Interaction.Library.More Agda.IR Agda.Parser Agda.Position @@ -223,6 +226,7 @@ test-suite als-test Server.CommandController Server.Handler Server.Handler.TextDocument.DocumentSymbol + Server.Handler.TextDocument.FileManagement Server.Model Server.Model.AgdaFile Server.Model.AgdaLib diff --git a/src/Agda/Interaction/Imports/More.hs b/src/Agda/Interaction/Imports/More.hs index 37ac8d5..549625b 100644 --- a/src/Agda/Interaction/Imports/More.hs +++ b/src/Agda/Interaction/Imports/More.hs @@ -1,20 +1,157 @@ --- | This module reexports unexported functions +{-# LANGUAGE CPP #-} + module Agda.Interaction.Imports.More - ( setOptionsFromSourcePragmas, + ( parseVirtualSource, + setOptionsFromSourcePragmas, checkModuleName', ) where -import Agda.Interaction.FindFile (SourceFile, checkModuleName) -import Agda.Interaction.Imports (Source) +import Agda.Interaction.FindFile ( + SourceFile (SourceFile), + checkModuleName, +#if MIN_VERSION_Agda(2,8,0) + rootNameModule, +#else + moduleName, +#endif + ) +import Agda.Interaction.Imports (Source (..)) import qualified Agda.Interaction.Imports as Imp import Agda.Interaction.Library (OptionsPragma (..), _libPragmas) import Agda.Syntax.Common (TopLevelModuleName') import qualified Agda.Syntax.Concrete as C -import Agda.Syntax.Position (Range) -import Agda.Syntax.TopLevelModuleName (TopLevelModuleName) -import Agda.TypeChecking.Monad (Interface, TCM, checkAndSetOptionsFromPragma, setCurrentRange, setOptionsFromPragma, setTCLens, stPragmaOptions, useTC) +import Agda.Syntax.Parser ( + moduleParser, + parseFile, +#if MIN_VERSION_Agda(2,8,0) + parse, + moduleNameParser, +#else + PM, + runPMIO, +#endif + ) +import Agda.Syntax.Position + ( Range, + Range' (Range), + RangeFile, + beginningOfFile, + getRange, + intervalToRange, + mkRangeFile, + posToRange, + posToRange', + startPos, +#if MIN_VERSION_Agda(2,8,0) + rangeFromAbsolutePath, +#endif + ) +import Agda.Syntax.TopLevelModuleName ( + TopLevelModuleName, + RawTopLevelModuleName (..), +#if MIN_VERSION_Agda(2,8,0) + rawTopLevelModuleNameForModule, +#endif + ) +import Agda.TypeChecking.Monad + ( AbsolutePath, + Interface, + TCM, + checkAndSetOptionsFromPragma, + setCurrentRange, + setOptionsFromPragma, + setTCLens, + stPragmaOptions, + useTC, +#if MIN_VERSION_Agda(2,8,0) + runPM, + runPMDropWarnings, +#endif + ) +import qualified Agda.TypeChecking.Monad as TCM +import qualified Agda.TypeChecking.Monad.Benchmark as Bench +#if MIN_VERSION_Agda(2,8,0) +#else +import Agda.TypeChecking.Warnings (runPM) +#endif import Agda.Utils.Monad (bracket_) +#if MIN_VERSION_Agda(2,8,0) +import qualified Data.Text as T +#endif +import qualified Data.Text.Lazy as TL +import Control.Monad.Error.Class ( +#if MIN_VERSION_Agda(2,8,0) + catchError, +#else + throwError, +#endif + ) +#if MIN_VERSION_Agda(2,8,0) +import Agda.Utils.Singleton (singleton) +#else +import Agda.Syntax.Common.Pretty (pretty) +#endif + +-- | Parse a source file without talking to the filesystem +parseVirtualSource :: + -- | Logical path of the source file. Used in ranges, not filesystem access. + SourceFile -> + -- | Logical contents of the source file + TL.Text -> + TCM Imp.Source +parseVirtualSource sourceFile source = Bench.billTo [Bench.Parsing] $ do + f <- srcFilePath sourceFile + let rf0 = mkRangeFile f Nothing + setCurrentRange (beginningOfFile rf0) $ do + parsedModName0 <- moduleName f . fst . fst =<< do + runPMDropWarnings $ parseFile moduleParser rf0 $ TL.unpack source + + let rf = mkRangeFile f $ Just parsedModName0 + ((parsedMod, attrs), fileType) <- runPM $ parseFile moduleParser rf $ TL.unpack source + parsedModName <- moduleName f parsedMod + + -- TODO: handle libs properly + let libs = [] + + return + Source + { srcText = source, + srcFileType = fileType, + srcOrigin = sourceFile, + srcModule = parsedMod, + srcModuleName = parsedModName, + srcProjectLibs = libs, + srcAttributes = attrs + } + +srcFilePath :: SourceFile -> TCM AbsolutePath +#if MIN_VERSION_Agda(2,8,0) +srcFilePath = TCM.srcFilePath +#else +srcFilePath (SourceFile f) = return f +#endif + +#if MIN_VERSION_Agda(2,8,0) +-- beginningOfFile was generalized in Agda 2.8.0 to support the features we +-- need, so we just import it +#else +beginningOfFile :: RangeFile -> Range +beginningOfFile rf = posToRange (startPos $ Just rf) (startPos $ Just rf) +#endif + +#if MIN_VERSION_Agda(2,8,0) +-- runPMDropWarnings was introduced in Agda 2.8.0, so we just import it +#else +runPMDropWarnings :: PM a -> TCM a +runPMDropWarnings m = do + (res, _ws) <- runPMIO m + case res of + Left e -> throwError $ TCM.Exception (getRange e) (pretty e) + Right a -> return a +#endif + +-- Unexported Agda functions srcDefaultPragmas :: Imp.Source -> [OptionsPragma] srcDefaultPragmas src = map _libPragmas (Imp.srcProjectLibs src) @@ -48,3 +185,40 @@ setOptionsFromSourcePragmas checkOpts src = do checkModuleName' :: TopLevelModuleName' Range -> SourceFile -> TCM () checkModuleName' m f = setCurrentRange m $ checkModuleName m f Nothing + +#if MIN_VERSION_Agda(2,8,0) +-- moduleName was exported until 2.8.0 + +-- | Computes the module name of the top-level module in the given file. +-- +-- If no top-level module name is given, then an attempt is made to +-- use the file name as a module name. + +moduleName :: + AbsolutePath + -- ^ The path to the file. + -> C.Module + -- ^ The parsed module. + -> TCM TopLevelModuleName +moduleName file parsedModule = Bench.billTo [Bench.ModuleName] $ do + let defaultName = rootNameModule file + raw = rawTopLevelModuleNameForModule parsedModule + TCM.topLevelModuleName =<< if C.isNoName raw + then setCurrentRange (rangeFromAbsolutePath file) $ do + m <- runPM (fst <$> parse moduleNameParser defaultName) + `catchError` \_ -> + TCM.typeError $ TCM.InvalidFileName file TCM.DoesNotCorrespondToValidModuleName + case m of + C.Qual{} -> + TCM.typeError $ TCM.InvalidFileName file $ + TCM.RootNameModuleNotAQualifiedModuleName $ T.pack defaultName + C.QName{} -> + return $ RawTopLevelModuleName + { rawModuleNameRange = getRange m + , rawModuleNameParts = singleton (T.pack defaultName) + , rawModuleNameInferred = True + -- Andreas, 2025-06-21, issue #7953: + -- Remember we made up this module name to improve errors. + } + else return raw +#endif diff --git a/src/Agda/Interaction/Library/More.hs b/src/Agda/Interaction/Library/More.hs new file mode 100644 index 0000000..72f98c7 --- /dev/null +++ b/src/Agda/Interaction/Library/More.hs @@ -0,0 +1,39 @@ +{-# LANGUAGE CPP #-} + +module Agda.Interaction.Library.More + ( tryRunLibM, +#if MIN_VERSION_Agda(2,8,0) +#else + runLibErrorIO, +#endif + ) +where + +import Agda.Interaction.Library (LibM) +import Agda.Interaction.Library.Base (LibErrorIO) +import Agda.Utils.Either (maybeRight) +import Agda.Utils.Null (Null (empty)) +import Control.Category ((>>>)) +import Control.Monad.Except (runExceptT) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad.State.Lazy (evalStateT) +import Control.Monad.Writer.Lazy (runWriterT) + +#if MIN_VERSION_Agda(2,8,0) +-- Unneeded in 2.8.0 due to API changes +#else +runLibErrorIO :: (MonadIO m) => LibErrorIO a -> m a +runLibErrorIO = + runWriterT + >>> flip evalStateT empty + >>> fmap fst + >>> liftIO +#endif + +tryRunLibM :: (MonadIO m) => LibM a -> m (Maybe a) +tryRunLibM = + runExceptT + >>> runWriterT + >>> flip evalStateT empty + >>> fmap (fst >>> maybeRight) + >>> liftIO diff --git a/src/Language/LSP/Protocol/Types/Uri/More.hs b/src/Language/LSP/Protocol/Types/Uri/More.hs index f8c1b69..dea62db 100644 --- a/src/Language/LSP/Protocol/Types/Uri/More.hs +++ b/src/Language/LSP/Protocol/Types/Uri/More.hs @@ -1,11 +1,16 @@ module Language.LSP.Protocol.Types.Uri.More ( getNormalizedUri, isUriAncestorOf, + uriToPossiblyInvalidAbsolutePath, ) where +import Agda.Utils.FileName (AbsolutePath (AbsolutePath), absolute) +import Agda.Utils.Maybe (fromMaybe) +import Control.Monad.IO.Class (MonadIO, liftIO) import Data.Text (Text) import qualified Data.Text as Text +import Language.LSP.Protocol.Types (uriToFilePath) import qualified Language.LSP.Protocol.Types as LSP getNormalizedUri :: LSP.NormalizedUri -> Text @@ -18,3 +23,12 @@ getNormalizedUri = LSP.getUri . LSP.fromNormalizedUri isUriAncestorOf :: LSP.NormalizedUri -> LSP.NormalizedUri -> Bool isUriAncestorOf ancestor descendant = getNormalizedUri ancestor `Text.isPrefixOf` getNormalizedUri descendant + +uriToPossiblyInvalidAbsolutePath :: (MonadIO m) => LSP.NormalizedUri -> m AbsolutePath +uriToPossiblyInvalidAbsolutePath uri = do + case LSP.uriToFilePath $ LSP.fromNormalizedUri uri of + Just path -> liftIO $ absolute path + Nothing -> return $ uriToInvalidAbsolutePath uri + +uriToInvalidAbsolutePath :: LSP.NormalizedUri -> AbsolutePath +uriToInvalidAbsolutePath = AbsolutePath . getNormalizedUri diff --git a/src/Monad.hs b/src/Monad.hs index 24c091d..b84c362 100644 --- a/src/Monad.hs +++ b/src/Monad.hs @@ -6,6 +6,8 @@ module Monad where import Agda.IR import Agda.Interaction.Base (IOTCM) +import Agda.Interaction.Library (findProjectRoot) +import Agda.Interaction.Library.More (tryRunLibM) import Agda.TypeChecking.Monad (TCMT) import Agda.Utils.Lens (Lens', (^.)) import Control.Concurrent @@ -17,7 +19,7 @@ import Data.IORef readIORef, writeIORef, ) -import Data.Maybe (isJust) +import Data.Maybe (fromMaybe, isJust) import Data.Text ( Text, pack, @@ -33,9 +35,10 @@ import Server.CommandController (CommandController) import qualified Server.CommandController as CommandController import Server.Model (Model) import qualified Server.Model as Model -import Server.Model.AgdaLib (AgdaLib) +import Server.Model.AgdaLib (AgdaLib, agdaLibFromFs, initAgdaLib) import Server.ResponseController (ResponseController) import qualified Server.ResponseController as ResponseController +import System.FilePath (takeDirectory) -------------------------------------------------------------------------------- @@ -87,6 +90,29 @@ askModel = do modelVar <- asks envModel liftIO $ readIORef modelVar +modifyModel :: (MonadIO m) => (Model -> Model) -> ServerT m () +modifyModel f = do + modelVar <- asks envModel + liftIO $ modifyIORef' modelVar f + +-- | Find cached 'AgdaLib', or else make one from @.agda-lib@ files on the file +-- system, or else provide a default +findAgdaLib :: (MonadIO m) => LSP.NormalizedUri -> ServerT m AgdaLib +findAgdaLib uri = do + model <- askModel + case Model.getKnownAgdaLib uri model of + Just lib -> return lib + Nothing -> do + lib <- case LSP.uriToFilePath $ LSP.fromNormalizedUri uri of + Just path -> do + lib <- agdaLibFromFs $ takeDirectory path + case lib of + Just lib -> return lib + Nothing -> initAgdaLib + Nothing -> initAgdaLib + modifyModel $ Model.withAgdaLib lib + return lib + -- | Provider provideCommand :: (Monad m, MonadIO m) => IOTCM -> ServerT m () provideCommand iotcm = do diff --git a/src/Server.hs b/src/Server.hs index a2c7b16..bbebd50 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -29,6 +29,7 @@ import qualified Server.Handler as Handler import Switchboard (Switchboard, agdaCustomMethod) import qualified Switchboard import Server.Handler.TextDocument.DocumentSymbol (documentSymbolHandler) +import Server.Handler.TextDocument.FileManagement (didOpenHandler, didCloseHandler, didSaveHandler) #if defined(wasm32_HOST_ARCH) import Agda.Utils.IO (catchIO) @@ -129,11 +130,11 @@ handlers = -- `workspace/didChangeConfiguration` notificationHandler SMethod_WorkspaceDidChangeConfiguration $ \_notification -> return (), -- `textDocument/didOpen` - notificationHandler SMethod_TextDocumentDidOpen $ \_notification -> return (), + didOpenHandler, -- `textDocument/didClose` - notificationHandler SMethod_TextDocumentDidClose $ \_notification -> return (), + didCloseHandler, -- `textDocument/didChange` notificationHandler SMethod_TextDocumentDidChange $ \_notification -> return (), -- `textDocument/didSave` - notificationHandler SMethod_TextDocumentDidSave $ \_notification -> return () - ] \ No newline at end of file + didSaveHandler + ] diff --git a/src/Server/Handler/TextDocument/DocumentSymbol.hs b/src/Server/Handler/TextDocument/DocumentSymbol.hs index 9199d90..6e1b451 100644 --- a/src/Server/Handler/TextDocument/DocumentSymbol.hs +++ b/src/Server/Handler/TextDocument/DocumentSymbol.hs @@ -13,11 +13,11 @@ import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.Server as LSP import Monad (ServerM) import Server.Model.AgdaFile (AgdaFile, agdaFileSymbols, defNameRange, symbolByName, symbolsByParent) -import Server.Model.Monad (MonadAgdaFile (askAgdaFile), useAgdaFile, withAgdaFile) +import Server.Model.Monad (MonadAgdaFile (askAgdaFile), requestHandlerWithAgdaFile, useAgdaFile) import Server.Model.Symbol (SymbolInfo (symbolName), lspSymbolKind, symbolShortName, symbolType) documentSymbolHandler :: LSP.Handlers ServerM -documentSymbolHandler = withAgdaFile LSP.SMethod_TextDocumentDocumentSymbol $ \req responder -> do +documentSymbolHandler = requestHandlerWithAgdaFile LSP.SMethod_TextDocumentDocumentSymbol $ \req responder -> do file <- askAgdaFile let symbols = symbolsByParent file let topLevelNames = fromMaybe [] $ Map.lookup Nothing symbols diff --git a/src/Server/Handler/TextDocument/FileManagement.hs b/src/Server/Handler/TextDocument/FileManagement.hs new file mode 100644 index 0000000..2dda162 --- /dev/null +++ b/src/Server/Handler/TextDocument/FileManagement.hs @@ -0,0 +1,47 @@ +module Server.Handler.TextDocument.FileManagement + ( didOpenHandler, + didCloseHandler, + didSaveHandler, + ) +where + +import Agda.Interaction.FindFile (SourceFile (SourceFile)) +import qualified Agda.Interaction.Imports.More as Imp +import Agda.TypeChecking.Monad (MonadTCM (liftTCM)) +import Agda.Utils.Lens ((^.)) +import Control.Monad.Trans (lift) +import Data.Strict (Strict (toLazy)) +import Indexer (indexFile) +import qualified Language.LSP.Protocol.Lens as LSP +import qualified Language.LSP.Protocol.Message as LSP +import Language.LSP.Protocol.Types.Uri.More (uriToPossiblyInvalidAbsolutePath) +import qualified Language.LSP.Server as LSP +import qualified Language.LSP.Server as VFS +import qualified Language.LSP.VFS as VFS +import Monad (ServerM, modifyModel) +import qualified Server.Model as Model +import Server.Model.Monad (notificationHandlerWithAgdaLib) + +didOpenHandler :: LSP.Handlers ServerM +didOpenHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidOpen $ \notification uri -> do + sourceFile <- SourceFile <$> uriToPossiblyInvalidAbsolutePath uri + let sourceText = toLazy $ notification ^. LSP.params . LSP.textDocument . LSP.text + src <- liftTCM $ Imp.parseVirtualSource sourceFile sourceText + agdaFile <- indexFile src + lift $ modifyModel $ Model.setAgdaFile uri agdaFile + +didCloseHandler :: LSP.Handlers ServerM +didCloseHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidClose $ \notification uri -> do + lift $ modifyModel $ Model.deleteAgdaFile uri + +didSaveHandler :: LSP.Handlers ServerM +didSaveHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidSave $ \notification uri -> do + sourceFile <- SourceFile <$> uriToPossiblyInvalidAbsolutePath uri + virtualFile <- lift $ VFS.getVirtualFile uri + case virtualFile of + Nothing -> return () + Just virtualFile -> do + let sourceText = toLazy $ VFS.virtualFileText virtualFile + src <- liftTCM $ Imp.parseVirtualSource sourceFile sourceText + agdaFile <- indexFile src + lift $ modifyModel $ Model.setAgdaFile uri agdaFile diff --git a/src/Server/Model.hs b/src/Server/Model.hs index cc11217..8ed9001 100644 --- a/src/Server/Model.hs +++ b/src/Server/Model.hs @@ -1,7 +1,19 @@ -module Server.Model (Model (Model), empty, getKnownAgdaLib, getAgdaLib, getAgdaFile) where +module Server.Model + ( Model (Model), + empty, + getKnownAgdaLib, + getAgdaLib, + withAgdaLib, + getAgdaFile, + setAgdaFile, + deleteAgdaFile, + ) +where +import Agda.Utils.Lens (Lens', over) import Control.Monad.IO.Class (MonadIO) import Data.Foldable (find) +import Data.Functor ((<&>)) import Data.Map (Map) import qualified Data.Map as Map import qualified Language.LSP.Protocol.Types as LSP @@ -16,11 +28,29 @@ data Model = Model empty :: Model empty = Model [] Map.empty +agdaLibs :: Lens' Model [AgdaLib] +agdaLibs f a = f (_modelAgdaLibs a) <&> \x -> a {_modelAgdaLibs = x} + +agdaFiles :: Lens' Model (Map LSP.NormalizedUri AgdaFile) +agdaFiles f a = f (_modelAgdaFiles a) <&> \x -> a {_modelAgdaFiles = x} + getKnownAgdaLib :: LSP.NormalizedUri -> Model -> Maybe AgdaLib getKnownAgdaLib uri = find (`isAgdaLibForUri` uri) . _modelAgdaLibs +-- | Get the Agda library for the given URI if known. Otherwise, get a generic +-- default Agda library. getAgdaLib :: (MonadIO m) => LSP.NormalizedUri -> Model -> m AgdaLib getAgdaLib uri = maybe initAgdaLib return . getKnownAgdaLib uri +-- | Add an 'AgdaLib' to the model +withAgdaLib :: AgdaLib -> Model -> Model +withAgdaLib lib model = model {_modelAgdaLibs = lib : _modelAgdaLibs model} + getAgdaFile :: LSP.NormalizedUri -> Model -> Maybe AgdaFile getAgdaFile uri = Map.lookup uri . _modelAgdaFiles + +setAgdaFile :: LSP.NormalizedUri -> AgdaFile -> Model -> Model +setAgdaFile uri agdaFile = over agdaFiles $ Map.insert uri agdaFile + +deleteAgdaFile :: LSP.NormalizedUri -> Model -> Model +deleteAgdaFile uri = over agdaFiles $ Map.delete uri diff --git a/src/Server/Model/AgdaLib.hs b/src/Server/Model/AgdaLib.hs index 24b5df2..aaa9b6b 100644 --- a/src/Server/Model/AgdaLib.hs +++ b/src/Server/Model/AgdaLib.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE CPP #-} + module Server.Model.AgdaLib ( AgdaLib (AgdaLib), initAgdaLib, @@ -5,12 +7,30 @@ module Server.Model.AgdaLib agdaLibTcStateRef, agdaLibTcEnv, isAgdaLibForUri, + agdaLibFromFs, ) where +import Agda.Interaction.Library ( + AgdaLibFile (_libIncludes), + findProjectRoot, +#if MIN_VERSION_Agda(2,8,0) + getAgdaLibFile, +#else + getAgdaLibFiles', +#endif + ) +import Agda.Interaction.Library.More ( + tryRunLibM, +#if MIN_VERSION_Agda(2,8,0) +#else + runLibErrorIO, +#endif + ) import qualified Agda.TypeChecking.Monad as TCM import Agda.Utils.IORef (IORef, newIORef) import Agda.Utils.Lens (Lens', (<&>), (^.)) +import Agda.Utils.Maybe (listToMaybe) import Control.Monad.IO.Class (MonadIO (liftIO)) import Data.Map (Map) import qualified Language.LSP.Protocol.Types as LSP @@ -23,11 +43,19 @@ data AgdaLib = AgdaLib _agdaLibTcEnv :: !TCM.TCEnv } -initAgdaLib :: (MonadIO m) => m AgdaLib -initAgdaLib = do - tcStateRef <- liftIO $ newIORef TCM.initState +initAgdaLibWithIncludes :: (MonadIO m) => [LSP.NormalizedUri] -> m AgdaLib +initAgdaLibWithIncludes includes = do +#if MIN_VERSION_Agda(2,8,0) + tcState <- liftIO TCM.initStateIO +#else + let tcState = TCM.initState +#endif + tcStateRef <- liftIO $ newIORef tcState let tcEnv = TCM.initEnv - return $ AgdaLib [] tcStateRef tcEnv + return $ AgdaLib includes tcStateRef tcEnv + +initAgdaLib :: (MonadIO m) => m AgdaLib +initAgdaLib = initAgdaLibWithIncludes [] agdaLibIncludes :: Lens' AgdaLib [LSP.NormalizedUri] agdaLibIncludes f a = f (_agdaLibIncludes a) <&> \x -> a {_agdaLibIncludes = x} @@ -40,3 +68,38 @@ agdaLibTcEnv f a = f (_agdaLibTcEnv a) <&> \x -> a {_agdaLibTcEnv = x} isAgdaLibForUri :: AgdaLib -> LSP.NormalizedUri -> Bool isAgdaLibForUri agdaLib uri = any (`LSP.isUriAncestorOf` uri) (agdaLib ^. agdaLibIncludes) + +-- | Get an 'AgdaLib' from @.agda-lib@ files on the filesystem. These files are +-- searched for by traversing parent directories until one is found. +agdaLibFromFs :: + (MonadIO m) => + -- | Directory to start the search from + FilePath -> + m (Maybe AgdaLib) +agdaLibFromFs path = do + root <- tryRunLibM $ findProjectRoot path + case root of + Just (Just root) -> do + libFile <- tryGetLibFileFromRootPath root + case libFile of + Just libFile -> Just <$> agdaLibFromFile libFile + Nothing -> return Nothing + _noRoot -> return Nothing + +tryGetLibFileFromRootPath :: (MonadIO m) => FilePath -> m (Maybe AgdaLibFile) +#if MIN_VERSION_Agda(2,8,0) +tryGetLibFileFromRootPath root = do + maybeLibFiles <- tryRunLibM $ getAgdaLibFile root + case maybeLibFiles of + Just (libFile:_) -> return $ Just libFile + _ -> return Nothing +#else +tryGetLibFileFromRootPath root = do + libFiles <- runLibErrorIO $ getAgdaLibFiles' root + return $ listToMaybe libFiles +#endif + +agdaLibFromFile :: (MonadIO m) => AgdaLibFile -> m AgdaLib +agdaLibFromFile libFile = do + let includes = LSP.toNormalizedUri . LSP.filePathToUri <$> _libIncludes libFile + initAgdaLibWithIncludes includes diff --git a/src/Server/Model/Monad.hs b/src/Server/Model/Monad.hs index ae66e85..22a00cc 100644 --- a/src/Server/Model/Monad.hs +++ b/src/Server/Model/Monad.hs @@ -10,11 +10,12 @@ module Server.Model.Monad ( MonadAgdaLib (..), useAgdaLib, + notificationHandlerWithAgdaLib, MonadAgdaFile (..), useAgdaFile, - withAgdaFile, + requestHandlerWithAgdaFile, WithAgdaLibM, - withAgdaLibFor, + runWithAgdaLib, ) where @@ -32,7 +33,7 @@ import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.Protocol.Types.Uri.More as LSP import Language.LSP.Server (LspM) import qualified Language.LSP.Server as LSP -import Monad (ServerM, ServerT, askModel) +import Monad (ServerM, ServerT, askModel, findAgdaLib) import Options (Config) import qualified Server.Model as Model import Server.Model.AgdaFile (AgdaFile) @@ -112,13 +113,29 @@ runWithAgdaLibT agdaLib = flip runReaderT agdaLib . unWithAgdaLibT type WithAgdaLibM = WithAgdaLibT ServerM -withAgdaLibFor :: LSP.Uri -> WithAgdaLibM a -> ServerM a -withAgdaLibFor uri x = do +runWithAgdaLib :: LSP.Uri -> WithAgdaLibM a -> ServerM a +runWithAgdaLib uri x = do let normUri = LSP.toNormalizedUri uri model <- askModel agdaLib <- Model.getAgdaLib normUri model runWithAgdaLibT agdaLib x +type NotificationHandlerWithAgdaLib m = + LSP.TNotificationMessage m -> LSP.NormalizedUri -> WithAgdaLibM () + +notificationHandlerWithAgdaLib :: + forall (m :: LSP.Method LSP.ClientToServer LSP.Notification) textdoc. + (LSP.HasTextDocument (LSP.MessageParams m) textdoc, LSP.HasUri textdoc LSP.Uri) => + LSP.SMethod m -> + NotificationHandlerWithAgdaLib m -> + LSP.Handlers ServerM +notificationHandlerWithAgdaLib m handler = LSP.notificationHandler m $ \notification -> do + let uri = notification ^. LSP.params . LSP.textDocument . LSP.uri + normUri = LSP.toNormalizedUri uri + + agdaLib <- findAgdaLib normUri + runWithAgdaLibT agdaLib $ handler notification normUri + instance (MonadIO m) => MonadAgdaLib (WithAgdaLibT m) where askAgdaLib = WithAgdaLibT ask localAgdaLib f = WithAgdaLibT . local f . unWithAgdaLibT @@ -167,18 +184,18 @@ runWithAgdaFileT agdaLib agdaFile = type WithAgdaFileM = WithAgdaFileT ServerM -type HandlerWithAgdaFile m = +type RequestHandlerWithAgdaFile m = LSP.TRequestMessage m -> (Either (LSP.TResponseError m) (LSP.MessageResult m) -> WithAgdaFileM ()) -> WithAgdaFileM () -withAgdaFile :: +requestHandlerWithAgdaFile :: forall (m :: LSP.Method LSP.ClientToServer LSP.Request). (LSP.HasTextDocument (LSP.MessageParams m) LSP.TextDocumentIdentifier) => LSP.SMethod m -> - HandlerWithAgdaFile m -> + RequestHandlerWithAgdaFile m -> LSP.Handlers ServerM -withAgdaFile m handler = LSP.requestHandler m $ \req responder -> do +requestHandlerWithAgdaFile m handler = LSP.requestHandler m $ \req responder -> do let uri = req ^. LSP.params . LSP.textDocument . LSP.uri normUri = LSP.toNormalizedUri uri diff --git a/test/Test/Indexer/Invariants.hs b/test/Test/Indexer/Invariants.hs index a39ee71..0a80b52 100644 --- a/test/Test/Indexer/Invariants.hs +++ b/test/Test/Indexer/Invariants.hs @@ -15,7 +15,7 @@ import Indexer (indexFile, withAstFor) import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.Server as LSP import Monad (runServerT) -import Server.Model.Monad (withAgdaLibFor) +import Server.Model.Monad (runWithAgdaLib) import System.FilePath (takeBaseName, ()) import Test.Indexer.NoDuplicateDecl (testNoDuplicateDecl) import Test.Indexer.NoMissing (testNoMissing) @@ -35,7 +35,7 @@ tests = do (file, interface) <- LSP.runLspT undefined $ do env <- TestData.getServerEnv model runServerT env $ do - interface <- withAgdaLibFor uri $ do + interface <- runWithAgdaLib uri $ do TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions absInPath <- liftIO $ absolute inPath let srcFile = SourceFile absInPath @@ -45,7 +45,7 @@ tests = do checkResult <- TCM.liftTCM $ Imp.typeCheckMain Imp.TypeCheck src return $ Imp.crInterface checkResult - ast <- withAgdaLibFor uri $ do + ast <- runWithAgdaLib uri $ do TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions absInPath <- liftIO $ absolute inPath let srcFile = SourceFile absInPath @@ -56,7 +56,7 @@ tests = do -- Write the AST to a file for debugging purposes liftIO $ writeFile ("test/data/AST" testName) $ prettyShow $ topLevelDecls ast - withAgdaLibFor uri $ do + runWithAgdaLib uri $ do TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions absInPath <- liftIO $ absolute inPath let srcFile = SourceFile absInPath diff --git a/test/Test/ModelMonad.hs b/test/Test/ModelMonad.hs index bfc9c09..dbc310e 100644 --- a/test/Test/ModelMonad.hs +++ b/test/Test/ModelMonad.hs @@ -21,7 +21,7 @@ import Options (Config, defaultOptions, initConfig) import qualified Server.CommandController as CommandController import Server.Model (Model) import Server.Model.AgdaLib (agdaLibIncludes) -import Server.Model.Monad (MonadAgdaLib (askAgdaLib), withAgdaFile) +import Server.Model.Monad (MonadAgdaLib (askAgdaLib), requestHandlerWithAgdaFile) import qualified Server.ResponseController as ResponseController import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (testCase, (@?), (@?=)) @@ -37,7 +37,7 @@ tests = let method = LSP.SMethod_TextDocumentDocumentSymbol message = TestData.documentSymbolMessage TestData.fileUri1 - let handlers = withAgdaFile method $ \req responder -> do + let handlers = requestHandlerWithAgdaFile method $ \req responder -> do agdaLib <- askAgdaLib liftIO $ length (agdaLib ^. agdaLibIncludes) @?= 3 responder $ Right $ LSP.InL [] @@ -52,7 +52,7 @@ tests = let method = LSP.SMethod_TextDocumentDocumentSymbol message = TestData.documentSymbolMessage TestData.fakeUri - let handlers = withAgdaFile method $ \req responder -> do + let handlers = requestHandlerWithAgdaFile method $ \req responder -> do responder $ Right $ LSP.InL [] model <- TestData.getModel From a6754e18ac262b8d1f6da5e4ca9e5eea3c6dd43a Mon Sep 17 00:00:00 2001 From: nvarner Date: Sun, 26 Oct 2025 19:16:16 -0500 Subject: [PATCH 17/23] refactor handlers, handle errors --- agda-language-server.cabal | 2 + src/Monad.hs | 10 ++ .../Handler/TextDocument/DocumentSymbol.hs | 3 +- .../Handler/TextDocument/FileManagement.hs | 8 +- src/Server/Model/Handler.hs | 93 +++++++++++++++++++ src/Server/Model/Monad.hs | 56 +++-------- test/Test/ModelMonad.hs | 3 +- 7 files changed, 124 insertions(+), 51 deletions(-) create mode 100644 src/Server/Model/Handler.hs diff --git a/agda-language-server.cabal b/agda-language-server.cabal index 787db94..86bd57d 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -84,6 +84,7 @@ library Server.Model Server.Model.AgdaFile Server.Model.AgdaLib + Server.Model.Handler Server.Model.Monad Server.Model.Symbol Server.ResponseController @@ -230,6 +231,7 @@ test-suite als-test Server.Model Server.Model.AgdaFile Server.Model.AgdaLib + Server.Model.Handler Server.Model.Monad Server.Model.Symbol Server.ResponseController diff --git a/src/Monad.hs b/src/Monad.hs index b84c362..e837de0 100644 --- a/src/Monad.hs +++ b/src/Monad.hs @@ -9,8 +9,11 @@ import Agda.Interaction.Base (IOTCM) import Agda.Interaction.Library (findProjectRoot) import Agda.Interaction.Library.More (tryRunLibM) import Agda.TypeChecking.Monad (TCMT) +import qualified Agda.TypeChecking.Monad as TCM import Agda.Utils.Lens (Lens', (^.)) import Control.Concurrent +import Control.Exception (Exception) +import qualified Control.Exception as E import Control.Monad.Reader import Data.IORef ( IORef, @@ -30,6 +33,7 @@ import Language.LSP.Server MonadLsp, getConfig, ) +import qualified Language.LSP.Server as LSP import Options import Server.CommandController (CommandController) import qualified Server.CommandController as CommandController @@ -113,6 +117,12 @@ findAgdaLib uri = do modifyModel $ Model.withAgdaLib lib return lib +catchTCError :: ServerM a -> (TCM.TCErr -> ServerM a) -> ServerM a +catchTCError m h = + ReaderT $ \env -> LSP.LspT $ ReaderT $ \lspEnv -> + LSP.runLspT lspEnv (runServerT env m) + `E.catch` \err -> LSP.runLspT lspEnv (runServerT env (h err)) + -- | Provider provideCommand :: (Monad m, MonadIO m) => IOTCM -> ServerT m () provideCommand iotcm = do diff --git a/src/Server/Handler/TextDocument/DocumentSymbol.hs b/src/Server/Handler/TextDocument/DocumentSymbol.hs index 6e1b451..bd5b695 100644 --- a/src/Server/Handler/TextDocument/DocumentSymbol.hs +++ b/src/Server/Handler/TextDocument/DocumentSymbol.hs @@ -13,7 +13,8 @@ import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.Server as LSP import Monad (ServerM) import Server.Model.AgdaFile (AgdaFile, agdaFileSymbols, defNameRange, symbolByName, symbolsByParent) -import Server.Model.Monad (MonadAgdaFile (askAgdaFile), requestHandlerWithAgdaFile, useAgdaFile) +import Server.Model.Handler (requestHandlerWithAgdaFile) +import Server.Model.Monad (MonadAgdaFile (askAgdaFile), useAgdaFile) import Server.Model.Symbol (SymbolInfo (symbolName), lspSymbolKind, symbolShortName, symbolType) documentSymbolHandler :: LSP.Handlers ServerM diff --git a/src/Server/Handler/TextDocument/FileManagement.hs b/src/Server/Handler/TextDocument/FileManagement.hs index 2dda162..a43d8f9 100644 --- a/src/Server/Handler/TextDocument/FileManagement.hs +++ b/src/Server/Handler/TextDocument/FileManagement.hs @@ -20,10 +20,10 @@ import qualified Language.LSP.Server as VFS import qualified Language.LSP.VFS as VFS import Monad (ServerM, modifyModel) import qualified Server.Model as Model -import Server.Model.Monad (notificationHandlerWithAgdaLib) +import Server.Model.Handler (notificationHandlerWithAgdaLib) didOpenHandler :: LSP.Handlers ServerM -didOpenHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidOpen $ \notification uri -> do +didOpenHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidOpen $ \uri notification -> do sourceFile <- SourceFile <$> uriToPossiblyInvalidAbsolutePath uri let sourceText = toLazy $ notification ^. LSP.params . LSP.textDocument . LSP.text src <- liftTCM $ Imp.parseVirtualSource sourceFile sourceText @@ -31,11 +31,11 @@ didOpenHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidOpen lift $ modifyModel $ Model.setAgdaFile uri agdaFile didCloseHandler :: LSP.Handlers ServerM -didCloseHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidClose $ \notification uri -> do +didCloseHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidClose $ \uri notification -> do lift $ modifyModel $ Model.deleteAgdaFile uri didSaveHandler :: LSP.Handlers ServerM -didSaveHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidSave $ \notification uri -> do +didSaveHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidSave $ \uri notification -> do sourceFile <- SourceFile <$> uriToPossiblyInvalidAbsolutePath uri virtualFile <- lift $ VFS.getVirtualFile uri case virtualFile of diff --git a/src/Server/Model/Handler.hs b/src/Server/Model/Handler.hs new file mode 100644 index 0000000..bef30ec --- /dev/null +++ b/src/Server/Model/Handler.hs @@ -0,0 +1,93 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} + +module Server.Model.Handler + ( notificationHandlerWithAgdaLib, + requestHandlerWithAgdaFile, + ) +where + +import Agda.Syntax.Common (WithHiding (whHiding)) +import Agda.Syntax.Common.Pretty (prettyShow) +import qualified Agda.TypeChecking.Monad as TCM +import qualified Agda.TypeChecking.Pretty as TCM +import Agda.Utils.Either (fromRightM) +import Agda.Utils.Lens ((^.)) +import Control.Monad.Trans (MonadTrans, lift) +import qualified Data.Text as Text +import qualified Language.LSP.Protocol.Lens as LSP +import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Message as Lsp +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Server as LSP +import Monad (ServerM, askModel, catchTCError, findAgdaLib) +import qualified Server.Model as Model +import Server.Model.Monad (WithAgdaFileM, WithAgdaLibM, runWithAgdaFileT, runWithAgdaLibT) + +tryTC :: ServerM a -> ServerM (Either TCM.TCErr a) +tryTC handler = (Right <$> handler) `catchTCError` (return . Left) + +-------------------------------------------------------------------------------- + +type NotificationHandlerWithAgdaLib + (m :: LSP.Method LSP.ClientToServer LSP.Notification) = + LSP.NormalizedUri -> LSP.TNotificationMessage m -> WithAgdaLibM () + +notificationHandlerWithAgdaLib :: + (LSP.HasTextDocument (LSP.MessageParams m) textdoc, LSP.HasUri textdoc LSP.Uri) => + LSP.SMethod m -> + NotificationHandlerWithAgdaLib m -> + LSP.Handlers ServerM +notificationHandlerWithAgdaLib m handlerWithAgdaLib = LSP.notificationHandler m $ \notification -> do + let uri = notification ^. LSP.params . LSP.textDocument . LSP.uri + normUri = LSP.toNormalizedUri uri + agdaLib <- findAgdaLib normUri + + let notificationHandler = runWithAgdaLibT agdaLib . handlerWithAgdaLib normUri + let handler = tryTC $ notificationHandler notification + + let onErr = \err -> runWithAgdaLibT agdaLib $ do + message <- Text.pack . prettyShow <$> TCM.liftTCM (TCM.prettyTCM err) + lift $ LSP.sendNotification LSP.SMethod_WindowShowMessage $ LSP.ShowMessageParams LSP.MessageType_Error message + + fromRightM onErr handler + +-------------------------------------------------------------------------------- + +type RequestCallbackWithAgdaFile + (m :: LSP.Method LSP.ClientToServer LSP.Request) = + Either (LSP.TResponseError m) (LSP.MessageResult m) -> WithAgdaFileM () + +type RequestHandlerWithAgdaFile + (m :: LSP.Method LSP.ClientToServer LSP.Request) = + LSP.TRequestMessage m -> + RequestCallbackWithAgdaFile m -> + WithAgdaFileM () + +requestHandlerWithAgdaFile :: + (LSP.HasTextDocument (LSP.MessageParams m) textdoc, LSP.HasUri textdoc LSP.Uri) => + LSP.SMethod m -> + RequestHandlerWithAgdaFile m -> + LSP.Handlers ServerM +requestHandlerWithAgdaFile m handlerWithAgdaFile = LSP.requestHandler m $ \req responder -> do + let uri = req ^. LSP.params . LSP.textDocument . LSP.uri + normUri = LSP.toNormalizedUri uri + + model <- askModel + case Model.getAgdaFile normUri model of + Nothing -> do + let message = "Request for unknown Agda file at URI: " <> LSP.getUri uri + responder $ Left $ LSP.TResponseError (LSP.InR LSP.ErrorCodes_InvalidParams) message Nothing + Just agdaFile -> do + agdaLib <- Model.getAgdaLib normUri model + let responderWithAgdaFile = lift . responder + let handler = tryTC $ runWithAgdaFileT agdaLib agdaFile $ handlerWithAgdaFile req responderWithAgdaFile + + let onErr = \err -> runWithAgdaFileT agdaLib agdaFile $ do + message <- Text.pack . prettyShow <$> TCM.liftTCM (TCM.prettyTCM err) + lift $ responder $ Left $ LSP.TResponseError (LSP.InL LSP.LSPErrorCodes_RequestFailed) message Nothing + + fromRightM onErr handler diff --git a/src/Server/Model/Monad.hs b/src/Server/Model/Monad.hs index 22a00cc..ba2e8b0 100644 --- a/src/Server/Model/Monad.hs +++ b/src/Server/Model/Monad.hs @@ -10,30 +10,37 @@ module Server.Model.Monad ( MonadAgdaLib (..), useAgdaLib, - notificationHandlerWithAgdaLib, MonadAgdaFile (..), useAgdaFile, - requestHandlerWithAgdaFile, + WithAgdaLibT, + runWithAgdaLibT, WithAgdaLibM, runWithAgdaLib, + WithAgdaFileT, + runWithAgdaFileT, + WithAgdaFileM, ) where import Agda.Interaction.Options (CommandLineOptions (optPragmaOptions), PragmaOptions) -import Agda.TypeChecking.Monad (HasOptions (..), MonadTCEnv (..), MonadTCM (..), MonadTCState (..), PersistentTCState (stPersistentOptions), ReadTCState (..), TCEnv, TCM, TCMT (..), TCState (stPersistentState), modifyTCLens, setTCLens, stPragmaOptions, useTC) +import Agda.Syntax.Common.Pretty (prettyShow) +import Agda.TypeChecking.Monad (HasOptions (..), MonadTCEnv (..), MonadTCM (..), MonadTCState (..), PersistentTCState (stPersistentOptions), ReadTCState (..), TCEnv, TCM, TCMT (..), TCState (stPersistentState), catchError_, modifyTCLens, setTCLens, stPragmaOptions, useTC) +import qualified Agda.TypeChecking.Monad as TCM +import qualified Agda.TypeChecking.Pretty as TCM import Agda.Utils.IORef (modifyIORef', readIORef, writeIORef) import Agda.Utils.Lens (Lens', locally, over, use, view, (<&>), (^.)) import Agda.Utils.Monad (bracket_) import Control.Monad.IO.Class (MonadIO (liftIO)) import Control.Monad.Reader (MonadReader (local), ReaderT (runReaderT), ask, asks) import Control.Monad.Trans (MonadTrans, lift) +import qualified Data.Text as Text import qualified Language.LSP.Protocol.Lens as LSP import qualified Language.LSP.Protocol.Message as LSP import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.Protocol.Types.Uri.More as LSP import Language.LSP.Server (LspM) import qualified Language.LSP.Server as LSP -import Monad (ServerM, ServerT, askModel, findAgdaLib) +import Monad (ServerM, ServerT, askModel, catchTCError, findAgdaLib) import Options (Config) import qualified Server.Model as Model import Server.Model.AgdaFile (AgdaFile) @@ -120,22 +127,6 @@ runWithAgdaLib uri x = do agdaLib <- Model.getAgdaLib normUri model runWithAgdaLibT agdaLib x -type NotificationHandlerWithAgdaLib m = - LSP.TNotificationMessage m -> LSP.NormalizedUri -> WithAgdaLibM () - -notificationHandlerWithAgdaLib :: - forall (m :: LSP.Method LSP.ClientToServer LSP.Notification) textdoc. - (LSP.HasTextDocument (LSP.MessageParams m) textdoc, LSP.HasUri textdoc LSP.Uri) => - LSP.SMethod m -> - NotificationHandlerWithAgdaLib m -> - LSP.Handlers ServerM -notificationHandlerWithAgdaLib m handler = LSP.notificationHandler m $ \notification -> do - let uri = notification ^. LSP.params . LSP.textDocument . LSP.uri - normUri = LSP.toNormalizedUri uri - - agdaLib <- findAgdaLib normUri - runWithAgdaLibT agdaLib $ handler notification normUri - instance (MonadIO m) => MonadAgdaLib (WithAgdaLibT m) where askAgdaLib = WithAgdaLibT ask localAgdaLib f = WithAgdaLibT . local f . unWithAgdaLibT @@ -184,31 +175,6 @@ runWithAgdaFileT agdaLib agdaFile = type WithAgdaFileM = WithAgdaFileT ServerM -type RequestHandlerWithAgdaFile m = - LSP.TRequestMessage m -> - (Either (LSP.TResponseError m) (LSP.MessageResult m) -> WithAgdaFileM ()) -> - WithAgdaFileM () - -requestHandlerWithAgdaFile :: - forall (m :: LSP.Method LSP.ClientToServer LSP.Request). - (LSP.HasTextDocument (LSP.MessageParams m) LSP.TextDocumentIdentifier) => - LSP.SMethod m -> - RequestHandlerWithAgdaFile m -> - LSP.Handlers ServerM -requestHandlerWithAgdaFile m handler = LSP.requestHandler m $ \req responder -> do - let uri = req ^. LSP.params . LSP.textDocument . LSP.uri - normUri = LSP.toNormalizedUri uri - - model <- askModel - case Model.getAgdaFile normUri model of - Nothing -> do - let message = "Request for unknown Agda file at URI: " <> LSP.getUri uri - responder $ Left $ LSP.TResponseError (LSP.InR LSP.ErrorCodes_InvalidParams) message Nothing - Just agdaFile -> do - agdaLib <- Model.getAgdaLib normUri model - let responder' = lift . responder - runWithAgdaFileT agdaLib agdaFile $ handler req responder' - instance (MonadIO m) => MonadAgdaLib (WithAgdaFileT m) where askAgdaLib = WithAgdaFileT $ view withAgdaFileEnvAgdaLib localAgdaLib f = WithAgdaFileT . locally withAgdaFileEnvAgdaLib f . unWithAgdaFileT diff --git a/test/Test/ModelMonad.hs b/test/Test/ModelMonad.hs index dbc310e..13bc440 100644 --- a/test/Test/ModelMonad.hs +++ b/test/Test/ModelMonad.hs @@ -21,7 +21,8 @@ import Options (Config, defaultOptions, initConfig) import qualified Server.CommandController as CommandController import Server.Model (Model) import Server.Model.AgdaLib (agdaLibIncludes) -import Server.Model.Monad (MonadAgdaLib (askAgdaLib), requestHandlerWithAgdaFile) +import Server.Model.Handler (requestHandlerWithAgdaFile) +import Server.Model.Monad (MonadAgdaLib (askAgdaLib)) import qualified Server.ResponseController as ResponseController import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (testCase, (@?), (@?=)) From 269caa4eb526f73b2551dbc9d006c75d291db667 Mon Sep 17 00:00:00 2001 From: nvarner Date: Thu, 30 Oct 2025 19:50:07 -0500 Subject: [PATCH 18/23] use unqualified symbol name --- src/Server/Model/Symbol.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Server/Model/Symbol.hs b/src/Server/Model/Symbol.hs index 291a540..e178690 100644 --- a/src/Server/Model/Symbol.hs +++ b/src/Server/Model/Symbol.hs @@ -81,7 +81,7 @@ instance Semigroup SymbolInfo where (symbolParent old <|> symbolParent new) symbolShortName :: SymbolInfo -> Text -symbolShortName = Text.pack . prettyShow . symbolName +symbolShortName = Text.pack . prettyShow . A.qnameName . symbolName lspSymbolKind :: SymbolInfo -> LSP.SymbolKind lspSymbolKind = toLspSymbolKind . symbolKind From 001d043fca4ecc611d9637d5bad5bcc0393bbe82 Mon Sep 17 00:00:00 2001 From: nvarner Date: Fri, 31 Oct 2025 20:15:48 -0500 Subject: [PATCH 19/23] no anonymous function symbols --- agda-language-server.cabal | 1 + src/Indexer/Indexer.hs | 34 +++++++++------ test/Test.hs | 4 +- test/Test/Indexer/Invariants.hs | 39 +---------------- test/Test/Indexer/NoAnonFunSymbol.hs | 25 +++++++++++ test/TestData.hs | 64 +++++++++++++++++++++++++++- test/data/AnonFun.agda | 4 ++ 7 files changed, 117 insertions(+), 54 deletions(-) create mode 100644 test/Test/Indexer/NoAnonFunSymbol.hs create mode 100644 test/data/AnonFun.agda diff --git a/agda-language-server.cabal b/agda-language-server.cabal index 86bd57d..a64e3c5 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -185,6 +185,7 @@ test-suite als-test main-is: Test.hs other-modules: Test.Indexer.Invariants + Test.Indexer.NoAnonFunSymbol Test.Indexer.NoDuplicateDecl Test.Indexer.NoMissing Test.Indexer.NoOverlap diff --git a/src/Indexer/Indexer.hs b/src/Indexer/Indexer.hs index 5394729..e900bb8 100644 --- a/src/Indexer/Indexer.hs +++ b/src/Indexer/Indexer.hs @@ -22,6 +22,7 @@ import qualified Agda.Utils.List1 as List1 import Agda.Utils.Maybe (whenJust) import Agda.Utils.Monad (when) import Data.Foldable (forM_, traverse_) +import Data.Functor.Compose (Compose (Compose, getCompose)) import qualified Data.Set as Set import Data.Void (absurd) import Indexer.Monad @@ -100,7 +101,7 @@ instance Indexable A.Declaration where A.FunDef _defInfo name clauses -> withBindingKind DefBinding $ do -- function declarations are captured by the `Axiom` case withParent name $ do - index clauses + index $ WithLHSNaming LHSNamed <$> clauses A.DataSig defInfo _erased name genTel type' -> withBindingKind DeclBinding $ do tellDecl name Data type' @@ -200,7 +201,7 @@ instance Indexable A.Expr where return () A.ExtendedLam _exprInfo defInfo _erased _generatedFn clauses -> do index defInfo - index clauses + index $ WithLHSNaming LHSAnonymous <$> clauses A.Pi _exprInfo tel type' -> do index tel index type' @@ -335,28 +336,33 @@ instance Indexable A.WhereDeclarations where A.WhereDecls Nothing _ decl -> index decl -instance (Indexable a) => Indexable (A.LHSCore' a) where - index core = case core of +data LHSNaming = LHSNamed | LHSAnonymous deriving (Eq) + +data WithLHSNaming a = WithLHSNaming LHSNaming a + +instance (Indexable a) => Indexable (WithLHSNaming (A.LHSCore' a)) where + index (WithLHSNaming lhsNaming core) = case core of A.LHSHead name pats -> do - tellDef name Param UnknownType + when (lhsNaming == LHSNamed) $ + tellDef name Param UnknownType indexNamedArgs name pats A.LHSProj destructor focus pats -> do tellUsage destructor -- TODO: what does the named arg in `focus` mean? - indexNamedArgs destructor [focus] + indexNamedArgs destructor [getCompose $ WithLHSNaming lhsNaming <$> Compose focus] indexNamedArgs destructor pats A.LHSWith lhsHead withPatterns pats -> do - index lhsHead + index $ WithLHSNaming lhsNaming lhsHead index withPatterns -- TODO: what do the named args mean? forM_ pats $ \(C.Arg argInfo (C.Named _name pat)) -> when (C.argInfoOrigin argInfo == C.UserWritten) $ index pat -instance Indexable A.LHS where - index (A.LHS lhsInfo core) = case Info.lhsEllipsis lhsInfo of +instance Indexable (WithLHSNaming A.LHS) where + index (WithLHSNaming lhsNaming (A.LHS lhsInfo core)) = case Info.lhsEllipsis lhsInfo of C.ExpandedEllipsis _range _withArgs -> return () - C.NoEllipsis -> index core + C.NoEllipsis -> index $ WithLHSNaming lhsNaming core instance Indexable A.RewriteEqn where index eqn = case eqn of @@ -382,15 +388,15 @@ instance Indexable A.RHS where return () A.WithRHS _generatedFn withExprs clauses -> do forM_ withExprs indexWithExpr - index clauses + index $ WithLHSNaming LHSAnonymous <$> clauses A.RewriteRHS rewriteExprs _strippedPats rewriteRhs whereDecls -> do index rewriteExprs index rewriteRhs index whereDecls -instance (Indexable a) => Indexable (A.Clause' a) where - index (A.Clause lhs _strippedPats rhs whereDecls _catchall) = do - index lhs +instance Indexable (WithLHSNaming A.Clause) where + index (WithLHSNaming lhsNaming (A.Clause lhs _strippedPats rhs whereDecls _catchall)) = do + index $ WithLHSNaming lhsNaming lhs index rhs index whereDecls diff --git a/test/Test.hs b/test/Test.hs index 34aa3eb..0c2c0ca 100644 --- a/test/Test.hs +++ b/test/Test.hs @@ -12,6 +12,7 @@ import Test.Tasty.Options import qualified Test.Model as Model import qualified Test.ModelMonad as ModelMonad import qualified Test.Indexer.Invariants as IndexerInvariants +import qualified Test.Indexer.NoAnonFunSymbol as NoAnonFunSymbol -- Define the custom option newtype AlsPathOption = AlsPathOption FilePath @@ -39,7 +40,8 @@ tests = do LSP.tests alsPath, Model.tests, ModelMonad.tests, - indexerInvariantsTest + indexerInvariantsTest, + NoAnonFunSymbol.tests #if defined(wasm32_HOST_ARCH) , WASM.tests alsPath #endif diff --git a/test/Test/Indexer/Invariants.hs b/test/Test/Indexer/Invariants.hs index 0a80b52..bc41b79 100644 --- a/test/Test/Indexer/Invariants.hs +++ b/test/Test/Indexer/Invariants.hs @@ -22,49 +22,14 @@ import Test.Indexer.NoMissing (testNoMissing) import Test.Indexer.NoOverlap (testNoOverlap) import Test.Tasty (TestTree, testGroup) import Test.Tasty.Golden (findByExtension) +import TestData (AgdaFileDetails (AgdaFileDetails)) import qualified TestData tests :: IO TestTree tests = do inPaths <- findByExtension [".agda"] "test/data/Indexer" files <- forM inPaths $ \inPath -> do - let testName = takeBaseName inPath - uri = LSP.filePathToUri inPath - model <- TestData.getModel - - (file, interface) <- LSP.runLspT undefined $ do - env <- TestData.getServerEnv model - runServerT env $ do - interface <- runWithAgdaLib uri $ do - TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions - absInPath <- liftIO $ absolute inPath - let srcFile = SourceFile absInPath - src <- TCM.liftTCM $ Imp.parseSource srcFile - - TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (srcFilePath $ Imp.srcOrigin src) - checkResult <- TCM.liftTCM $ Imp.typeCheckMain Imp.TypeCheck src - return $ Imp.crInterface checkResult - - ast <- runWithAgdaLib uri $ do - TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions - absInPath <- liftIO $ absolute inPath - let srcFile = SourceFile absInPath - src <- TCM.liftTCM $ Imp.parseSource srcFile - - withAstFor src return - - -- Write the AST to a file for debugging purposes - liftIO $ writeFile ("test/data/AST" testName) $ prettyShow $ topLevelDecls ast - - runWithAgdaLib uri $ do - TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions - absInPath <- liftIO $ absolute inPath - let srcFile = SourceFile absInPath - src <- TCM.liftTCM $ Imp.parseSource srcFile - - agdaFile <- indexFile src - return (agdaFile, interface) - + TestData.AgdaFileDetails testName file interface <- TestData.agdaFileDetails inPath return (testName, file, interface) return $ diff --git a/test/Test/Indexer/NoAnonFunSymbol.hs b/test/Test/Indexer/NoAnonFunSymbol.hs new file mode 100644 index 0000000..4a6f997 --- /dev/null +++ b/test/Test/Indexer/NoAnonFunSymbol.hs @@ -0,0 +1,25 @@ +module Test.Indexer.NoAnonFunSymbol (tests) where + +import Agda.Syntax.Common.Pretty (prettyShow) +import Agda.Utils.Lens ((^.)) +import Agda.Utils.Maybe (ifJustM, whenJust, whenJustM) +import Control.Monad (forM) +import Data.Foldable (find) +import Data.List (isInfixOf) +import qualified Data.Map as Map +import Server.Model.AgdaFile (agdaFileSymbols) +import Test.Tasty (TestTree) +import Test.Tasty.HUnit (assertFailure, testCase) +import qualified TestData + +tests :: TestTree +tests = + testCase "No symbols for internal anonymous function names" $ do + TestData.AgdaFileDetails name agdaFile interface <- TestData.agdaFileDetails "test/data/AnonFun.agda" + + let symbolNames = prettyShow <$> Map.keys (agdaFile ^. agdaFileSymbols) + whenJust (find isAnonFunName symbolNames) $ \name -> + assertFailure $ "Found symbol for internal anonymous function: " ++ name + +isAnonFunName :: String -> Bool +isAnonFunName name = ".extendedlambda" `isInfixOf` name diff --git a/test/TestData.hs b/test/TestData.hs index d9d9e00..299e697 100644 --- a/test/TestData.hs +++ b/test/TestData.hs @@ -8,23 +8,83 @@ module TestData fileUri3, fakeUri, getServerEnv, + AgdaFileDetails (..), + agdaFileDetails, ) where +import Agda.Interaction.FindFile (SourceFile (SourceFile), srcFilePath) +import qualified Agda.Interaction.Imports as Imp +import qualified Agda.Interaction.Options +import Agda.Syntax.Abstract.More () +import Agda.Syntax.Common.Pretty (prettyShow) +import Agda.Syntax.Translation.ConcreteToAbstract (topLevelDecls) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.Utils.FileName (absolute) import Agda.Utils.IORef (newIORef) import Agda.Utils.Lens (set, (<&>)) import Control.Concurrent (newChan) import Control.Monad.IO.Class (MonadIO, liftIO) import qualified Data.Map as Map +import Indexer (indexFile, withAstFor) import qualified Language.LSP.Protocol.Message as LSP import qualified Language.LSP.Protocol.Types as LSP -import Monad (Env (Env)) +import qualified Language.LSP.Server as LSP +import Monad (Env (Env), runServerT) import Options (defaultOptions, initConfig) import qualified Server.CommandController as CommandController import Server.Model (Model (Model)) -import Server.Model.AgdaFile (emptyAgdaFile) +import Server.Model.AgdaFile (AgdaFile, emptyAgdaFile) import Server.Model.AgdaLib (agdaLibIncludes, initAgdaLib) +import Server.Model.Monad (runWithAgdaLib) import qualified Server.ResponseController as ResponseController +import System.FilePath (takeBaseName, ()) + +data AgdaFileDetails = AgdaFileDetails + { fileName :: String, + agdaFile :: AgdaFile, + interface :: TCM.Interface + } + +agdaFileDetails :: FilePath -> IO AgdaFileDetails +agdaFileDetails inPath = do + let testName = takeBaseName inPath + uri = LSP.filePathToUri inPath + model <- TestData.getModel + + (file, interface) <- LSP.runLspT undefined $ do + env <- TestData.getServerEnv model + runServerT env $ do + interface <- runWithAgdaLib uri $ do + TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions + absInPath <- liftIO $ absolute inPath + let srcFile = SourceFile absInPath + src <- TCM.liftTCM $ Imp.parseSource srcFile + + TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (srcFilePath $ Imp.srcOrigin src) + checkResult <- TCM.liftTCM $ Imp.typeCheckMain Imp.TypeCheck src + return $ Imp.crInterface checkResult + + ast <- runWithAgdaLib uri $ do + TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions + absInPath <- liftIO $ absolute inPath + let srcFile = SourceFile absInPath + src <- TCM.liftTCM $ Imp.parseSource srcFile + + withAstFor src return + + runWithAgdaLib uri $ do + TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions + absInPath <- liftIO $ absolute inPath + let srcFile = SourceFile absInPath + src <- TCM.liftTCM $ Imp.parseSource srcFile + + agdaFile <- indexFile src + return (agdaFile, interface) + + return $ AgdaFileDetails testName file interface + +-------------------------------------------------------------------------------- documentSymbolMessage :: LSP.NormalizedUri -> LSP.TRequestMessage LSP.Method_TextDocumentDocumentSymbol documentSymbolMessage uri = diff --git a/test/data/AnonFun.agda b/test/data/AnonFun.agda new file mode 100644 index 0000000..c62b8a6 --- /dev/null +++ b/test/data/AnonFun.agda @@ -0,0 +1,4 @@ +module AnonFun where + +f : {A : Set} -> A -> A +f = \where x -> x From 768f723c6fad5992d75178bc86036be667cfad86 Mon Sep 17 00:00:00 2001 From: nvarner Date: Sat, 1 Nov 2025 14:16:51 -0500 Subject: [PATCH 20/23] support Agda 2.8.0 indexing --- src/Indexer/Indexer.hs | 44 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 42 insertions(+), 2 deletions(-) diff --git a/src/Indexer/Indexer.hs b/src/Indexer/Indexer.hs index e900bb8..090ddcd 100644 --- a/src/Indexer/Indexer.hs +++ b/src/Indexer/Indexer.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -21,7 +22,7 @@ import Agda.Utils.List1 (List1) import qualified Agda.Utils.List1 as List1 import Agda.Utils.Maybe (whenJust) import Agda.Utils.Monad (when) -import Data.Foldable (forM_, traverse_) +import Data.Foldable (forM_, traverse_, toList) import Data.Functor.Compose (Compose (Compose, getCompose)) import qualified Data.Set as Set import Data.Void (absurd) @@ -213,9 +214,17 @@ instance Indexable A.Expr where A.Let _exprInfo bindings body -> do index bindings index body +#if MIN_VERSION_Agda(2,8,0) + A.Rec _kwRange _exprInfo recAssigns -> +#else A.Rec _exprInfo recAssigns -> +#endif index recAssigns +#if MIN_VERSION_Agda(2,8,0) + A.RecUpdate _kwRange _exprInfo exprRec assigns -> do +#else A.RecUpdate _exprInfo exprRec assigns -> do +#endif index exprRec index assigns A.ScopedExpr _scope expr' -> @@ -269,11 +278,18 @@ instance (Indexable a) => Indexable (A.Pattern' a) where index rhs A.WithP _patInfo pat' -> index pat' +#if MIN_VERSION_Agda(2,8,0) + A.RecP _kwRange _conPatInfo fieldAssignments -> +#else A.RecP _conPatInfo fieldAssignments -> +#endif index fieldAssignments +#if MIN_VERSION_Agda(2,8,0) +#else A.AnnP _patInfo type' pat' -> do index type' index pat' +#endif instance (Indexable a) => Indexable (Maybe a) @@ -452,19 +468,35 @@ instance Indexable A.LetBinding where A.LetOpen _moduleInfo moduleName importDirective -> do tellUsage moduleName index importDirective +#if MIN_VERSION_Agda(2,8,0) + A.LetAxiom _letInfo _argInfo boundName type' -> do + -- TODO: what does the `ArgInfo` mean? + tellBinding boundName Axiom type' + index type' +#else A.LetDeclaredVariable boundName -> -- This is always a declaration tellDecl boundName Local UnknownType +#endif indexNamedArgBinder :: (TypeLike t, HasParamNames t) => C.NamedArg A.Binder -> t -> IndexerM () +#if MIN_VERSION_Agda(2,8,0) +indexNamedArgBinder + (C.Arg argInfo (C.Named _maybeArgName (A.Binder pat nameOrigin name))) + typeLike = + when (C.argInfoOrigin argInfo == C.UserWritten && nameOrigin == C.UserBinderName) $ do + tellBinding name Param typeLike + index pat +#else indexNamedArgBinder (C.Arg argInfo (C.Named _maybeArgName (A.Binder pat name))) typeLike = when (C.argInfoOrigin argInfo == C.UserWritten) $ do tellBinding name Param typeLike index pat +#endif instance Indexable A.TypedBinding where index = \case @@ -492,7 +524,11 @@ instance Indexable A.DataDefParams where instance Indexable A.RecordDirectives where index = \case +#if MIN_VERSION_Agda(2,8,0) + (C.RecordDirectives inductive _hasEta _patRange (A.NamedRecCon conName)) -> +#else (C.RecordDirectives inductive _hasEta _patRange (Just conName)) -> +#endif tellDef conName (constructorSymbolKind inductive) UnknownType _noUserConstructor -> return () where @@ -606,7 +642,11 @@ instance SymbolKindLike TCM.Defn where toSymbolKind = \case TCM.AxiomDefn _axiomData -> Axiom TCM.DataOrRecSigDefn _dataOrRecSigData -> Unknown +#if MIN_VERSION_Agda(2,8,0) + TCM.GeneralizableVar _numGeneralizableArgs -> GeneralizeVar +#else TCM.GeneralizableVar -> GeneralizeVar +#endif TCM.AbstractDefn defn -> toSymbolKind defn TCM.FunctionDefn _functionData -> Fun TCM.DatatypeDefn _datatypeData -> Data @@ -637,7 +677,7 @@ instance HasParamNames A.Type where getParamNames tel <> getParamNames codom A.Fun _exprInfo _dom codom -> getParamNames codom A.Generalized varNames codom -> - Set.toList varNames <> getParamNames codom + toList varNames <> getParamNames codom A.ScopedExpr _scopeInfo expr -> getParamNames expr _noMoreParams -> [] From 094a883c11cf8f2ea8738636bb0401e3545e8f89 Mon Sep 17 00:00:00 2001 From: nvarner Date: Sat, 1 Nov 2025 16:29:45 -0500 Subject: [PATCH 21/23] support Agda 2.8.0 file management --- agda-language-server.cabal | 2 + src/Agda/Interaction/Imports/More.hs | 39 +------- src/Agda/Interaction/Imports/Virtual.hs | 96 +++++++++++++++++++ src/Agda/Syntax/Abstract/More.hs | 1 - .../Handler/TextDocument/FileManagement.hs | 27 +++--- src/Server/Model/Monad.hs | 20 ++++ 6 files changed, 138 insertions(+), 47 deletions(-) create mode 100644 src/Agda/Interaction/Imports/Virtual.hs diff --git a/agda-language-server.cabal b/agda-language-server.cabal index a64e3c5..727fbd3 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -50,6 +50,7 @@ library Agda Agda.Convert Agda.Interaction.Imports.More + Agda.Interaction.Imports.Virtual Agda.Interaction.Library.More Agda.IR Agda.Parser @@ -198,6 +199,7 @@ test-suite als-test Agda Agda.Convert Agda.Interaction.Imports.More + Agda.Interaction.Imports.Virtual Agda.Interaction.Library.More Agda.IR Agda.Parser diff --git a/src/Agda/Interaction/Imports/More.hs b/src/Agda/Interaction/Imports/More.hs index 549625b..3d905be 100644 --- a/src/Agda/Interaction/Imports/More.hs +++ b/src/Agda/Interaction/Imports/More.hs @@ -1,9 +1,12 @@ {-# LANGUAGE CPP #-} module Agda.Interaction.Imports.More - ( parseVirtualSource, - setOptionsFromSourcePragmas, + ( setOptionsFromSourcePragmas, checkModuleName', + runPMDropWarnings, + moduleName, + runPM, + beginningOfFile, ) where @@ -93,38 +96,6 @@ import Agda.Utils.Singleton (singleton) import Agda.Syntax.Common.Pretty (pretty) #endif --- | Parse a source file without talking to the filesystem -parseVirtualSource :: - -- | Logical path of the source file. Used in ranges, not filesystem access. - SourceFile -> - -- | Logical contents of the source file - TL.Text -> - TCM Imp.Source -parseVirtualSource sourceFile source = Bench.billTo [Bench.Parsing] $ do - f <- srcFilePath sourceFile - let rf0 = mkRangeFile f Nothing - setCurrentRange (beginningOfFile rf0) $ do - parsedModName0 <- moduleName f . fst . fst =<< do - runPMDropWarnings $ parseFile moduleParser rf0 $ TL.unpack source - - let rf = mkRangeFile f $ Just parsedModName0 - ((parsedMod, attrs), fileType) <- runPM $ parseFile moduleParser rf $ TL.unpack source - parsedModName <- moduleName f parsedMod - - -- TODO: handle libs properly - let libs = [] - - return - Source - { srcText = source, - srcFileType = fileType, - srcOrigin = sourceFile, - srcModule = parsedMod, - srcModuleName = parsedModName, - srcProjectLibs = libs, - srcAttributes = attrs - } - srcFilePath :: SourceFile -> TCM AbsolutePath #if MIN_VERSION_Agda(2,8,0) srcFilePath = TCM.srcFilePath diff --git a/src/Agda/Interaction/Imports/Virtual.hs b/src/Agda/Interaction/Imports/Virtual.hs new file mode 100644 index 0000000..30535a0 --- /dev/null +++ b/src/Agda/Interaction/Imports/Virtual.hs @@ -0,0 +1,96 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleContexts #-} + +module Agda.Interaction.Imports.Virtual + ( VSourceFile (..), + vSrcFileId, + vSrcFromUri, + parseVSource, + ) +where + +#if MIN_VERSION_Agda(2,8,0) +#else +import Agda.Interaction.FindFile (SourceFile (SourceFile)) +#endif +import qualified Agda.Interaction.Imports as Imp +import qualified Agda.Interaction.Imports.More as Imp +import Agda.Syntax.Parser (moduleParser, parseFile) +import Agda.Syntax.Position (mkRangeFile) +import qualified Agda.TypeChecking.Monad as TCM +import Control.Monad.IO.Class (MonadIO) +import Control.Monad.Trans (lift) +import qualified Data.Strict as Strict +import qualified Data.Text as Text +import qualified Language.LSP.Protocol.Types as LSP +import Language.LSP.Protocol.Types.Uri.More (uriToPossiblyInvalidAbsolutePath) +import qualified Language.LSP.Server as LSP +import qualified Language.LSP.VFS as VFS + +data VSourceFile = VSourceFile + { vSrcFileSrcFile :: TCM.SourceFile, + vSrcUri :: LSP.NormalizedUri, + vSrcVFile :: VFS.VirtualFile + } + +vSrcFilePath :: (TCM.MonadFileId m) => VSourceFile -> m TCM.AbsolutePath +vSrcFilePath = TCM.srcFilePath . vSrcFileSrcFile + +vSrcFileId :: VSourceFile -> TCM.FileId +vSrcFileId = TCM.srcFileId . vSrcFileSrcFile + +#if MIN_VERSION_Agda(2,8,0) +vSrcFromUri :: + (TCM.MonadFileId m, MonadIO m) => + LSP.NormalizedUri -> + VFS.VirtualFile -> + m VSourceFile +vSrcFromUri normUri file = do + absPath <- uriToPossiblyInvalidAbsolutePath normUri + src <- TCM.srcFromPath absPath + return $ VSourceFile src normUri file +#else +vSrcFromUri :: + (MonadIO m) => + LSP.NormalizedUri -> + VFS.VirtualFile -> + m VSourceFile +vSrcFromUri normUri file = do + absPath <- uriToPossiblyInvalidAbsolutePath normUri + let src = SourceFile absPath + return $ VSourceFile src normUri file +#endif + +-- | Based on @parseSource@ +parseVSource :: (TCM.MonadTCM m) => VSourceFile -> m Imp.Source +parseVSource vSrcFile = TCM.liftTCM $ do + let sourceFile = vSrcFileSrcFile vSrcFile + f <- vSrcFilePath vSrcFile + + let rf0 = mkRangeFile f Nothing + TCM.setCurrentRange (Imp.beginningOfFile rf0) $ do + let sourceStrict = VFS.virtualFileText $ vSrcVFile vSrcFile + let source = Strict.toLazy sourceStrict + let txt = Text.unpack sourceStrict + + parsedModName0 <- + Imp.moduleName f . fst . fst =<< do + Imp.runPMDropWarnings $ parseFile moduleParser rf0 txt + + let rf = mkRangeFile f $ Just parsedModName0 + ((parsedMod, attrs), fileType) <- Imp.runPM $ parseFile moduleParser rf txt + parsedModName <- Imp.moduleName f parsedMod + + -- TODO: handle libs properly + let libs = [] + + return + Imp.Source + { Imp.srcText = source, + Imp.srcFileType = fileType, + Imp.srcOrigin = sourceFile, + Imp.srcModule = parsedMod, + Imp.srcModuleName = parsedModName, + Imp.srcProjectLibs = libs, + Imp.srcAttributes = attrs + } diff --git a/src/Agda/Syntax/Abstract/More.hs b/src/Agda/Syntax/Abstract/More.hs index efd4131..fbe4f2b 100644 --- a/src/Agda/Syntax/Abstract/More.hs +++ b/src/Agda/Syntax/Abstract/More.hs @@ -170,7 +170,6 @@ instance Pretty LetBinding where text "let" <+> pretty (unBind name) <+> text "=" <+> pretty expr LetPatBind _letInfo pat expr -> text "letPat" <+> pretty pat <+> text "=" <+> pretty expr - LetDeclaredVariable name -> text "letDeclared" <+> pretty (unBind name) _ -> text "LetBinding" instance Pretty Binder where diff --git a/src/Server/Handler/TextDocument/FileManagement.hs b/src/Server/Handler/TextDocument/FileManagement.hs index a43d8f9..c95f349 100644 --- a/src/Server/Handler/TextDocument/FileManagement.hs +++ b/src/Server/Handler/TextDocument/FileManagement.hs @@ -7,6 +7,7 @@ where import Agda.Interaction.FindFile (SourceFile (SourceFile)) import qualified Agda.Interaction.Imports.More as Imp +import Agda.Interaction.Imports.Virtual (parseVSource, vSrcFromUri) import Agda.TypeChecking.Monad (MonadTCM (liftTCM)) import Agda.Utils.Lens ((^.)) import Control.Monad.Trans (lift) @@ -14,9 +15,9 @@ import Data.Strict (Strict (toLazy)) import Indexer (indexFile) import qualified Language.LSP.Protocol.Lens as LSP import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Types as LSP import Language.LSP.Protocol.Types.Uri.More (uriToPossiblyInvalidAbsolutePath) import qualified Language.LSP.Server as LSP -import qualified Language.LSP.Server as VFS import qualified Language.LSP.VFS as VFS import Monad (ServerM, modifyModel) import qualified Server.Model as Model @@ -24,11 +25,14 @@ import Server.Model.Handler (notificationHandlerWithAgdaLib) didOpenHandler :: LSP.Handlers ServerM didOpenHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidOpen $ \uri notification -> do - sourceFile <- SourceFile <$> uriToPossiblyInvalidAbsolutePath uri - let sourceText = toLazy $ notification ^. LSP.params . LSP.textDocument . LSP.text - src <- liftTCM $ Imp.parseVirtualSource sourceFile sourceText - agdaFile <- indexFile src - lift $ modifyModel $ Model.setAgdaFile uri agdaFile + vfile <- lift $ LSP.getVirtualFile uri + case vfile of + Nothing -> return () + Just vfile -> do + vSourceFile <- vSrcFromUri uri vfile + src <- liftTCM $ parseVSource vSourceFile + agdaFile <- indexFile src + lift $ modifyModel $ Model.setAgdaFile uri agdaFile didCloseHandler :: LSP.Handlers ServerM didCloseHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidClose $ \uri notification -> do @@ -36,12 +40,11 @@ didCloseHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidClos didSaveHandler :: LSP.Handlers ServerM didSaveHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidSave $ \uri notification -> do - sourceFile <- SourceFile <$> uriToPossiblyInvalidAbsolutePath uri - virtualFile <- lift $ VFS.getVirtualFile uri - case virtualFile of + vfile <- lift $ LSP.getVirtualFile uri + case vfile of Nothing -> return () - Just virtualFile -> do - let sourceText = toLazy $ VFS.virtualFileText virtualFile - src <- liftTCM $ Imp.parseVirtualSource sourceFile sourceText + Just vfile -> do + vSourceFile <- vSrcFromUri uri vfile + src <- liftTCM $ parseVSource vSourceFile agdaFile <- indexFile src lift $ modifyModel $ Model.setAgdaFile uri agdaFile diff --git a/src/Server/Model/Monad.hs b/src/Server/Model/Monad.hs index ba2e8b0..1a8a313 100644 --- a/src/Server/Model/Monad.hs +++ b/src/Server/Model/Monad.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} @@ -45,6 +46,9 @@ import Options (Config) import qualified Server.Model as Model import Server.Model.AgdaFile (AgdaFile) import Server.Model.AgdaLib (AgdaLib, agdaLibTcEnv, agdaLibTcStateRef) +#if MIN_VERSION_Agda(2,8,0) +import Agda.Utils.FileId (File, getIdFile) +#endif -------------------------------------------------------------------------------- @@ -110,6 +114,16 @@ defaultLiftTCM (TCM f) = do tcEnv <- useAgdaLib agdaLibTcEnv liftIO $ f tcStateRef tcEnv +#if MIN_VERSION_Agda(2,8,0) +-- Taken from TCMT implementation +defaultFileFromId :: (MonadAgdaLib m) => TCM.FileId -> m File +defaultFileFromId fi = useTC TCM.stFileDict <&> (`getIdFile` fi) + +-- Taken from TCMT implementation +defaultIdFromFile :: (MonadAgdaLib m) => File -> m TCM.FileId +defaultIdFromFile = TCM.stateTCLens TCM.stFileDict . TCM.registerFileIdWithBuiltin +#endif + -------------------------------------------------------------------------------- newtype WithAgdaLibT m a = WithAgdaLibT {unWithAgdaLibT :: ReaderT AgdaLib m a} @@ -151,6 +165,12 @@ instance (MonadIO m) => HasOptions (WithAgdaLibT m) where instance (MonadIO m) => MonadTCM (WithAgdaLibT m) where liftTCM = defaultLiftTCM +#if MIN_VERSION_Agda(2,8,0) +instance (MonadIO m) => TCM.MonadFileId (WithAgdaLibT m) where + fileFromId = defaultFileFromId + idFromFile = defaultIdFromFile +#endif + -------------------------------------------------------------------------------- data WithAgdaFileEnv = WithAgdaFileEnv From 91ec6d41f32b511e5e0d0616b7fbf3779679ad63 Mon Sep 17 00:00:00 2001 From: nvarner Date: Sat, 1 Nov 2025 17:40:20 -0500 Subject: [PATCH 22/23] support Agda 2.8.0 in tests --- src/Indexer.hs | 46 +++++++++++++++----------- test/Test/Indexer/Invariants.hs | 17 ---------- test/TestData.hs | 57 ++++++++++++++++++--------------- test/data/Indexer/Module.agda | 2 +- test/data/test.agda-lib | 2 ++ 5 files changed, 61 insertions(+), 63 deletions(-) create mode 100644 test/data/test.agda-lib diff --git a/src/Indexer.hs b/src/Indexer.hs index 73b13fb..2861528 100644 --- a/src/Indexer.hs +++ b/src/Indexer.hs @@ -2,6 +2,7 @@ module Indexer ( withAstFor, + usingSrcAsCurrent, indexFile, ) where @@ -21,9 +22,9 @@ import Indexer.Postprocess (postprocess) import Server.Model.AgdaFile (AgdaFile) import Server.Model.Monad (WithAgdaLibM) -withAstFor :: Imp.Source -> (TopLevelInfo -> WithAgdaLibM a) -> WithAgdaLibM a +usingSrcAsCurrent :: Imp.Source -> WithAgdaLibM a -> WithAgdaLibM a #if MIN_VERSION_Agda(2,8,0) -withAstFor src f = do +usingSrcAsCurrent src x = do TCM.liftTCM $ TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $ -- Now reset the options @@ -31,16 +32,9 @@ withAstFor src f = do TCM.modifyTCLens TCM.stModuleToSourceId $ Map.insert (Imp.srcModuleName src) (Imp.srcOrigin src) - TCM.localTC (\e -> e {TCM.envCurrentPath = Just (TCM.srcFileId $ Imp.srcOrigin src)}) $ do - let topLevel = - TopLevel - (Imp.srcOrigin src) - (Imp.srcModuleName src) - (C.modDecls $ Imp.srcModule src) - ast <- TCM.liftTCM $ toAbstract topLevel - f ast + TCM.localTC (\e -> e {TCM.envCurrentPath = Just (TCM.srcFileId $ Imp.srcOrigin src)}) x #else -withAstFor src f = do +usingSrcAsCurrent src x = do TCM.liftTCM $ TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $ -- Now reset the options @@ -48,14 +42,28 @@ withAstFor src f = do TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (srcFilePath $ Imp.srcOrigin src) - TCM.localTC (\e -> e {TCM.envCurrentPath = Just (srcFilePath $ Imp.srcOrigin src)}) $ do - let topLevel = - TopLevel - (srcFilePath $ Imp.srcOrigin src) - (Imp.srcModuleName src) - (C.modDecls $ Imp.srcModule src) - ast <- TCM.liftTCM $ toAbstract topLevel - f ast + TCM.localTC (\e -> e {TCM.envCurrentPath = Just (srcFilePath $ Imp.srcOrigin src)}) x +#endif + +withAstFor :: Imp.Source -> (TopLevelInfo -> WithAgdaLibM a) -> WithAgdaLibM a +#if MIN_VERSION_Agda(2,8,0) +withAstFor src f = usingSrcAsCurrent src $ do + let topLevel = + TopLevel + (Imp.srcOrigin src) + (Imp.srcModuleName src) + (C.modDecls $ Imp.srcModule src) + ast <- TCM.liftTCM $ toAbstract topLevel + f ast +#else +withAstFor src f = usingSrcAsCurrent src $ do + let topLevel = + TopLevel + (srcFilePath $ Imp.srcOrigin src) + (Imp.srcModuleName src) + (C.modDecls $ Imp.srcModule src) + ast <- TCM.liftTCM $ toAbstract topLevel + f ast #endif indexFile :: diff --git a/test/Test/Indexer/Invariants.hs b/test/Test/Indexer/Invariants.hs index bc41b79..8345bc5 100644 --- a/test/Test/Indexer/Invariants.hs +++ b/test/Test/Indexer/Invariants.hs @@ -1,28 +1,11 @@ module Test.Indexer.Invariants (tests) where -import Agda.Interaction.FindFile (SourceFile (SourceFile), srcFilePath) -import qualified Agda.Interaction.Imports as Imp -import Agda.Interaction.Options (defaultOptions) -import Agda.Syntax.Abstract.More () -import Agda.Syntax.Common.Pretty (prettyShow) -import Agda.Syntax.Translation.ConcreteToAbstract (TopLevelInfo (topLevelDecls)) -import qualified Agda.TypeChecking.Monad as TCM -import Agda.Utils.FileName (absolute) import Control.Monad (forM) -import Control.Monad.IO.Class (liftIO) -import qualified Data.Map as Map -import Indexer (indexFile, withAstFor) -import qualified Language.LSP.Protocol.Types as LSP -import qualified Language.LSP.Server as LSP -import Monad (runServerT) -import Server.Model.Monad (runWithAgdaLib) -import System.FilePath (takeBaseName, ()) import Test.Indexer.NoDuplicateDecl (testNoDuplicateDecl) import Test.Indexer.NoMissing (testNoMissing) import Test.Indexer.NoOverlap (testNoOverlap) import Test.Tasty (TestTree, testGroup) import Test.Tasty.Golden (findByExtension) -import TestData (AgdaFileDetails (AgdaFileDetails)) import qualified TestData tests :: IO TestTree diff --git a/test/TestData.hs b/test/TestData.hs index 299e697..8f9b7c3 100644 --- a/test/TestData.hs +++ b/test/TestData.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} module TestData @@ -13,7 +14,13 @@ module TestData ) where -import Agda.Interaction.FindFile (SourceFile (SourceFile), srcFilePath) +import Agda.Interaction.FindFile + ( SourceFile (SourceFile), +#if MIN_VERSION_Agda(2,8,0) +#else + srcFilePath, +#endif + ) import qualified Agda.Interaction.Imports as Imp import qualified Agda.Interaction.Options import Agda.Syntax.Abstract.More () @@ -26,11 +33,11 @@ import Agda.Utils.Lens (set, (<&>)) import Control.Concurrent (newChan) import Control.Monad.IO.Class (MonadIO, liftIO) import qualified Data.Map as Map -import Indexer (indexFile, withAstFor) +import Indexer (indexFile, withAstFor, usingSrcAsCurrent) import qualified Language.LSP.Protocol.Message as LSP import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.Server as LSP -import Monad (Env (Env), runServerT) +import Monad (Env (Env), runServerT, catchTCError) import Options (defaultOptions, initConfig) import qualified Server.CommandController as CommandController import Server.Model (Model (Model)) @@ -39,6 +46,7 @@ import Server.Model.AgdaLib (agdaLibIncludes, initAgdaLib) import Server.Model.Monad (runWithAgdaLib) import qualified Server.ResponseController as ResponseController import System.FilePath (takeBaseName, ()) +import Agda.TypeChecking.Pretty (prettyTCM) data AgdaFileDetails = AgdaFileDetails { fileName :: String, @@ -55,32 +63,29 @@ agdaFileDetails inPath = do (file, interface) <- LSP.runLspT undefined $ do env <- TestData.getServerEnv model runServerT env $ do - interface <- runWithAgdaLib uri $ do - TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions - absInPath <- liftIO $ absolute inPath - let srcFile = SourceFile absInPath - src <- TCM.liftTCM $ Imp.parseSource srcFile - - TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (srcFilePath $ Imp.srcOrigin src) + let withSrc f = runWithAgdaLib uri $ do + TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions + absInPath <- liftIO $ absolute inPath +#if MIN_VERSION_Agda(2,8,0) + srcFile <- TCM.srcFromPath absInPath +#else + let srcFile = SourceFile absInPath +#endif + src <- TCM.liftTCM $ Imp.parseSource srcFile + + f src + + let onErr = \err -> runWithAgdaLib uri $ do + t <- TCM.liftTCM $ prettyTCM err + error $ prettyShow t + + interface <- (withSrc $ \src -> usingSrcAsCurrent src $ do checkResult <- TCM.liftTCM $ Imp.typeCheckMain Imp.TypeCheck src - return $ Imp.crInterface checkResult - - ast <- runWithAgdaLib uri $ do - TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions - absInPath <- liftIO $ absolute inPath - let srcFile = SourceFile absInPath - src <- TCM.liftTCM $ Imp.parseSource srcFile - - withAstFor src return + return $ Imp.crInterface checkResult) `catchTCError` onErr - runWithAgdaLib uri $ do - TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions - absInPath <- liftIO $ absolute inPath - let srcFile = SourceFile absInPath - src <- TCM.liftTCM $ Imp.parseSource srcFile + file <- withSrc indexFile `catchTCError` onErr - agdaFile <- indexFile src - return (agdaFile, interface) + return (file, interface) return $ AgdaFileDetails testName file interface diff --git a/test/data/Indexer/Module.agda b/test/data/Indexer/Module.agda index 6685305..817d050 100644 --- a/test/data/Indexer/Module.agda +++ b/test/data/Indexer/Module.agda @@ -1,4 +1,4 @@ -module Module where +module Indexer.Module where data Nat : Set where zero : Nat diff --git a/test/data/test.agda-lib b/test/data/test.agda-lib new file mode 100644 index 0000000..33f7e30 --- /dev/null +++ b/test/data/test.agda-lib @@ -0,0 +1,2 @@ +name: test +include: . \ No newline at end of file From 6e86f66541af5b6cc799c1dd00e8c620c06e1c42 Mon Sep 17 00:00:00 2001 From: nvarner Date: Sat, 1 Nov 2025 18:34:08 -0500 Subject: [PATCH 23/23] Agda 2.7.0.1 compatibility fixes --- src/Agda/Interaction/Imports/More.hs | 6 +++--- src/Agda/Interaction/Imports/Virtual.hs | 17 +++++++++++------ src/Agda/Position.hs | 5 +++-- stack.yaml.lock | 4 ++-- 4 files changed, 19 insertions(+), 13 deletions(-) diff --git a/src/Agda/Interaction/Imports/More.hs b/src/Agda/Interaction/Imports/More.hs index 3d905be..987da8e 100644 --- a/src/Agda/Interaction/Imports/More.hs +++ b/src/Agda/Interaction/Imports/More.hs @@ -39,7 +39,6 @@ import Agda.Syntax.Position ( Range, Range' (Range), RangeFile, - beginningOfFile, getRange, intervalToRange, mkRangeFile, @@ -47,6 +46,7 @@ import Agda.Syntax.Position posToRange', startPos, #if MIN_VERSION_Agda(2,8,0) + beginningOfFile, rangeFromAbsolutePath, #endif ) @@ -58,8 +58,7 @@ import Agda.Syntax.TopLevelModuleName ( #endif ) import Agda.TypeChecking.Monad - ( AbsolutePath, - Interface, + ( Interface, TCM, checkAndSetOptionsFromPragma, setCurrentRange, @@ -78,6 +77,7 @@ import qualified Agda.TypeChecking.Monad.Benchmark as Bench #else import Agda.TypeChecking.Warnings (runPM) #endif +import Agda.Utils.FileName (AbsolutePath) import Agda.Utils.Monad (bracket_) #if MIN_VERSION_Agda(2,8,0) import qualified Data.Text as T diff --git a/src/Agda/Interaction/Imports/Virtual.hs b/src/Agda/Interaction/Imports/Virtual.hs index 30535a0..932076c 100644 --- a/src/Agda/Interaction/Imports/Virtual.hs +++ b/src/Agda/Interaction/Imports/Virtual.hs @@ -3,13 +3,13 @@ module Agda.Interaction.Imports.Virtual ( VSourceFile (..), - vSrcFileId, vSrcFromUri, parseVSource, ) where #if MIN_VERSION_Agda(2,8,0) +import Agda.TypeChecking.Monad (SourceFile (SourceFile)) #else import Agda.Interaction.FindFile (SourceFile (SourceFile)) #endif @@ -18,6 +18,7 @@ import qualified Agda.Interaction.Imports.More as Imp import Agda.Syntax.Parser (moduleParser, parseFile) import Agda.Syntax.Position (mkRangeFile) import qualified Agda.TypeChecking.Monad as TCM +import Agda.Utils.FileName (AbsolutePath) import Control.Monad.IO.Class (MonadIO) import Control.Monad.Trans (lift) import qualified Data.Strict as Strict @@ -28,16 +29,20 @@ import qualified Language.LSP.Server as LSP import qualified Language.LSP.VFS as VFS data VSourceFile = VSourceFile - { vSrcFileSrcFile :: TCM.SourceFile, + { vSrcFileSrcFile :: SourceFile, vSrcUri :: LSP.NormalizedUri, vSrcVFile :: VFS.VirtualFile } -vSrcFilePath :: (TCM.MonadFileId m) => VSourceFile -> m TCM.AbsolutePath +#if MIN_VERSION_Agda(2,8,0) +vSrcFilePath :: (TCM.MonadFileId m) => VSourceFile -> m AbsolutePath vSrcFilePath = TCM.srcFilePath . vSrcFileSrcFile - -vSrcFileId :: VSourceFile -> TCM.FileId -vSrcFileId = TCM.srcFileId . vSrcFileSrcFile +#else +vSrcFilePath :: (Monad m) => VSourceFile -> m AbsolutePath +vSrcFilePath vSourceFile = do + let (SourceFile path) = vSrcFileSrcFile vSourceFile + return path +#endif #if MIN_VERSION_Agda(2,8,0) vSrcFromUri :: diff --git a/src/Agda/Position.hs b/src/Agda/Position.hs index 4122326..d90e96d 100644 --- a/src/Agda/Position.hs +++ b/src/Agda/Position.hs @@ -24,6 +24,7 @@ import qualified Data.Strict.Maybe as Strict import Data.Text (Text) import qualified Data.Text as Text import qualified Language.LSP.Protocol.Types as LSP +import Data.Functor (void) -- Note: LSP srclocs are 0-base -- Agda srclocs are 1-base @@ -73,8 +74,8 @@ intervalEnd :: Interval -> PositionWithoutFile intervalStart (Interval _ start _end) = start intervalEnd (Interval _ _start end) = end #else -intervalStart (Interval start _end) = start -intervalEnd (Interval _start end) = end +intervalStart (Interval start _end) = void start +intervalEnd (Interval _start end) = void end #endif -- | Agda Range -> LSP Range diff --git a/stack.yaml.lock b/stack.yaml.lock index d9c754b..82be79c 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -5,9 +5,9 @@ packages: - completed: - hackage: Agda-2.8.0@sha256:f85f3b10eb034687b07d073686ab97c947082eecc5ad268cbe20a4c774abcaae,34434 + hackage: Agda-2.8.0@sha256:b73b1b6685650d4429074f10440952cecb7aef190a994f75d168c354d20b01a8,34453 pantry-tree: - sha256: 01cbe34629f37fa56a411390d4d9fa281bb92b8a66a6757232240f58380678a7 + sha256: 7dace5cc1fe5a4f09212dda58392ae29f34bb1382c6eb04cb86514b5f5e2da32 size: 43914 original: hackage: Agda-2.8.0