[Draft] Deeper integration with Agda: foundational work

.gitignore

@@ -4,6 +4,7 @@
 cabal-dev
 dist
 dist-*
+test/data/AST/
 node_modules/
 *.o
 *.hi

agda-language-server.cabal

@@ -49,10 +49,21 @@ library
   exposed-modules:
       Agda
       Agda.Convert
+      Agda.Interaction.Imports.More
+      Agda.Interaction.Imports.Virtual
+      Agda.Interaction.Library.More
       Agda.IR
       Agda.Parser
       Agda.Position
+      Agda.Syntax.Abstract.More
+      Agda.TypeChecking.Monad.Options.More
       Control.Concurrent.SizedChan
+      Indexer
+      Indexer.Indexer
+      Indexer.Monad
+      Indexer.Postprocess
+      Language.LSP.Protocol.Types.More
+      Language.LSP.Protocol.Types.Uri.More
       Monad
       Options
       Render
@@ -70,6 +81,14 @@ library
       Server
       Server.CommandController
       Server.Handler
+      Server.Handler.TextDocument.DocumentSymbol
+      Server.Handler.TextDocument.FileManagement
+      Server.Model
+      Server.Model.AgdaFile
+      Server.Model.AgdaLib
+      Server.Model.Handler
+      Server.Model.Monad
+      Server.Model.Symbol
       Server.ResponseController
       Switchboard
   other-modules:
@@ -160,23 +179,44 @@ 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
   type: exitcode-stdio-1.0
   main-is: Test.hs
   other-modules:
+      Test.Indexer
+      Test.Indexer.Invariants
+      Test.Indexer.Invariants.NoDuplicateDecl
+      Test.Indexer.Invariants.NoMissing
+      Test.Indexer.Invariants.NoOverlap
+      Test.Indexer.NoAnonFunSymbol
+      Test.Indexer.Reload
       Test.LSP
+      Test.Model
+      Test.ModelMonad
       Test.SrcLoc
+      Test.Uri
       Test.WASM
+      TestData
       Agda
       Agda.Convert
+      Agda.Interaction.Imports.More
+      Agda.Interaction.Imports.Virtual
+      Agda.Interaction.Library.More
       Agda.IR
       Agda.Parser
       Agda.Position
+      Agda.Syntax.Abstract.More
+      Agda.TypeChecking.Monad.Options.More
       Control.Concurrent.SizedChan
+      Indexer
+      Indexer.Indexer
+      Indexer.Monad
+      Indexer.Postprocess
+      Language.LSP.Protocol.Types.More
+      Language.LSP.Protocol.Types.Uri.More
       Monad
       Options
       Render
@@ -194,6 +234,14 @@ test-suite als-test
       Server
       Server.CommandController
       Server.Handler
+      Server.Handler.TextDocument.DocumentSymbol
+      Server.Handler.TextDocument.FileManagement
+      Server.Model
+      Server.Model.AgdaFile
+      Server.Model.AgdaLib
+      Server.Model.Handler
+      Server.Model.Monad
+      Server.Model.Symbol
       Server.ResponseController
       Switchboard
       Paths_agda_language_server
@@ -242,6 +290,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

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

src/Agda/Interaction/Imports/More.hs

@@ -0,0 +1,209 @@
+{-# LANGUAGE CPP #-}
+
+module Agda.Interaction.Imports.More
+  ( setOptionsFromSourcePragmas,
+    checkModuleName',
+    runPMDropWarnings,
+    moduleName,
+    runPM,
+    beginningOfFile,
+  )
+where
+
+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.Interaction.Library.More ()
+import Agda.Syntax.Common (TopLevelModuleName')
+import qualified Agda.Syntax.Concrete as C
+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,
+    getRange,
+    intervalToRange,
+    mkRangeFile,
+    posToRange,
+    posToRange',
+    startPos,
+#if MIN_VERSION_Agda(2,8,0)
+    beginningOfFile,
+    rangeFromAbsolutePath,
+#endif
+  )
+import Agda.Syntax.TopLevelModuleName (
+    TopLevelModuleName,
+    RawTopLevelModuleName (..),
+#if MIN_VERSION_Agda(2,8,0)
+    rawTopLevelModuleNameForModule,
+#endif
+  )
+import Agda.Syntax.Common.Pretty (Pretty, pretty, text, prettyAssign, (<+>))
+import Agda.TypeChecking.Monad
+  ( Interface,
+    TCM,
+    setCurrentRange,
+    setOptionsFromPragma,
+    setTCLens,
+    stPragmaOptions,
+    useTC,
+#if MIN_VERSION_Agda(2,7,0)
+    checkAndSetOptionsFromPragma,
+#endif
+#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.FileName (AbsolutePath)
+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)
+#endif
+
+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)
+
+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
+#if MIN_VERSION_Agda(2,7,0)
+    setOpts
+      | checkOpts = checkAndSetOptionsFromPragma
+      | otherwise = setOptionsFromPragma
+#else
+    setOpts = setOptionsFromPragma
+#endif
+
+-- 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
+
+#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
+
+-- Orphan instances
+
+instance Pretty Imp.Source where
+  pretty src =
+    text "Source"
+      <+> pretty (Imp.srcModuleName src)
+      <+> pretty (Imp.srcProjectLibs src)