preliminary document symbol handler

Author: nvarner

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

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

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

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)

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

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