support Agda 2.8.0 file management

Author: nvarner

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

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

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

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

src/Server/Handler/TextDocument/FileManagement.hs

@@ -7,41 +7,44 @@ 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)
 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
 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
   lift $ modifyModel $ Model.deleteAgdaFile uri
 
 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

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