test reloading is compatible with changes

nvarner · nvarner · commit 688a1a8a9ca8 · 2025-11-09T15:29:18.000-06:00
diff --git a/src/Agda/Interaction/Imports/Virtual.hs b/src/Agda/Interaction/Imports/Virtual.hs
@@ -4,6 +4,7 @@
 module Agda.Interaction.Imports.Virtual
   ( VSourceFile (..),
     vSrcFromUri,
+    parseSourceFromContents,
     parseVSource,
   )
 where
@@ -37,15 +38,20 @@ data VSourceFile = VSourceFile
     vSrcVFile :: VFS.VirtualFile
   }
 
+#if MIN_VERSION_Agda(2,8,0)
+srcFilePath :: (TCM.MonadFileId m) => SourceFile -> m AbsolutePath
+srcFilePath = TCM.srcFilePath
+#else
+srcFilePath :: (Monad m) => SourceFile -> m AbsolutePath
+srcFilePath (SourceFile path) = return path
+#endif
+
 #if MIN_VERSION_Agda(2,8,0)
 vSrcFilePath :: (TCM.MonadFileId m) => VSourceFile -> m AbsolutePath
-vSrcFilePath = TCM.srcFilePath . vSrcFileSrcFile
 #else
 vSrcFilePath :: (Monad m) => VSourceFile -> m AbsolutePath
-vSrcFilePath vSourceFile = do
-  let (SourceFile path) = vSrcFileSrcFile vSourceFile
-  return path
 #endif
+vSrcFilePath = srcFilePath . vSrcFileSrcFile
 
 #if MIN_VERSION_Agda(2,8,0)
 vSrcFromUri ::
@@ -69,37 +75,44 @@ vSrcFromUri normUri file = do
   return $ VSourceFile src normUri file
 #endif
 
--- | Based on @parseSource@
-parseVSource :: (TCM.MonadTCM m, TCM.MonadTrace m, MonadAgdaLib m) => VSourceFile -> m Imp.Source
-parseVSource vSrcFile = do
-  let sourceFile = vSrcFileSrcFile vSrcFile
-  f <- TCM.liftTCM $ vSrcFilePath vSrcFile
+parseSourceFromContents ::
+  (TCM.MonadTCM m, TCM.MonadTrace m, MonadAgdaLib m) =>
+  LSP.NormalizedUri ->
+  SourceFile ->
+  Text.Text ->
+  m Imp.Source
+parseSourceFromContents srcUri srcFile contentsStrict = do
+  f <- TCM.liftTCM $ srcFilePath srcFile
 
   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
+    let contents = Strict.toLazy contentsStrict
+    let contentsString = Text.unpack contentsStrict
 
     parsedModName0 <-
       TCM.liftTCM $
         Imp.moduleName f . fst . fst =<< do
-          Imp.runPMDropWarnings $ parseFile moduleParser rf0 txt
+          Imp.runPMDropWarnings $ parseFile moduleParser rf0 contentsString
 
     let rf = mkRangeFile f $ Just parsedModName0
-    ((parsedMod, attrs), fileType) <- TCM.liftTCM $ Imp.runPM $ parseFile moduleParser rf txt
+    ((parsedMod, attrs), fileType) <- TCM.liftTCM $ Imp.runPM $ parseFile moduleParser rf contentsString
     parsedModName <- TCM.liftTCM $ Imp.moduleName f parsedMod
 
     agdaLib <- askAgdaLib
-    let libs = maybeToList $ agdaLibToFile (vSrcUri vSrcFile) agdaLib
+    let libs = maybeToList $ agdaLibToFile srcUri agdaLib
 
     return
       Imp.Source
-        { Imp.srcText = source,
+        { Imp.srcText = contents,
           Imp.srcFileType = fileType,
-          Imp.srcOrigin = sourceFile,
+          Imp.srcOrigin = srcFile,
           Imp.srcModule = parsedMod,
           Imp.srcModuleName = parsedModName,
           Imp.srcProjectLibs = libs,
           Imp.srcAttributes = attrs
         }
+
+-- | Based on @parseSource@
+parseVSource :: (TCM.MonadTCM m, TCM.MonadTrace m, MonadAgdaLib m) => VSourceFile -> m Imp.Source
+parseVSource (VSourceFile srcFile uri vFile) =
+  parseSourceFromContents uri srcFile (VFS.virtualFileText vFile)
diff --git a/src/Server/Model/AgdaFile.hs b/src/Server/Model/AgdaFile.hs
@@ -14,7 +14,7 @@ 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.Common.Pretty (Pretty, pretty, prettyAssign, prettyMap, prettyShow, text, vcat)
 import Agda.Syntax.Position (getRange)
 import Agda.Utils.Lens (Lens', over, (<&>), (^.))
 import Data.Foldable (find)
@@ -29,6 +29,7 @@ data AgdaFile = AgdaFile
   { _agdaFileSymbols :: !(Map A.QName SymbolInfo),
     _agdaFileRefs :: !(Map A.QName [Ref])
   }
+  deriving (Eq)
 
 instance Pretty AgdaFile where
   pretty agdaFile =
@@ -37,6 +38,9 @@ instance Pretty AgdaFile where
         prettyAssign (text "refs", prettyMap $ Map.toList $ agdaFile ^. agdaFileRefs)
       ]
 
+instance Show AgdaFile where
+  show = prettyShow
+
 emptyAgdaFile :: AgdaFile
 emptyAgdaFile = AgdaFile Map.empty Map.empty
 
diff --git a/src/Server/Model/Symbol.hs b/src/Server/Model/Symbol.hs
@@ -66,6 +66,7 @@ data SymbolInfo = SymbolInfo
     symbolType :: !(Maybe String),
     symbolParent :: !(Maybe A.QName)
   }
+  deriving (Eq)
 
 instance Pretty SymbolInfo where
   pretty symbolInfo =
@@ -115,6 +116,7 @@ data Ref = Ref
     refRange :: !LSP.Range,
     refIsAmbiguous :: !Bool
   }
+  deriving (Eq)
 
 prettyAmbiguity :: Ref -> Doc
 prettyAmbiguity ref =
diff --git a/test/Test/Indexer/Reload.hs b/test/Test/Indexer/Reload.hs
@@ -1,18 +1,23 @@
 module Test.Indexer.Reload (tests) where
 
+import Agda.Interaction.Imports.Virtual (parseSourceFromContents)
+import Agda.Syntax.Common.Pretty (prettyShow)
+import Control.Monad.IO.Class (liftIO)
+import qualified Data.Text as Text
 import Indexer (indexFile)
 import qualified Language.LSP.Protocol.Types as LSP
 import qualified Language.LSP.Server as LSP
 import Monad (runServerT)
 import Server.Model.Monad (runWithAgdaLib)
 import Test.Tasty (TestTree, testGroup)
-import Test.Tasty.HUnit (testCase)
+import Test.Tasty.HUnit (assertFailure, testCase, (@?=))
 import qualified TestData
 
 tests :: TestTree
 tests =
   testGroup "Reload" $
-    [ testCase "Reload single file" $ testReloadFile "test/data/A.agda"
+    [ testCase "Reload single file" $ testReloadFile "test/data/A.agda",
+      testCase "Reload after changes" testReloadChanges
     ]
 
 testReloadFile :: FilePath -> IO ()
@@ -28,3 +33,42 @@ testReloadFile path = do
         _ <- indexFile src
         _ <- indexFile src
         return ()
+
+testReloadChanges :: IO ()
+testReloadChanges = do
+  let path = "test/data/A.agda"
+  let contentsA =
+        Text.unlines
+          [ "module A where",
+            "",
+            "data T : Set where",
+            "  tt : T"
+          ]
+  let contentsB =
+        Text.unlines
+          [ "module A where",
+            "",
+            "data T : Set where",
+            "  tt : T",
+            "",
+            "f : T -> T",
+            "f x = x"
+          ]
+
+  let uri = LSP.filePathToUri path
+  model <- TestData.getModel
+
+  LSP.runLspT undefined $ do
+    env <- TestData.getServerEnv model
+    runServerT env $ do
+      runWithAgdaLib uri $ do
+        src0 <- TestData.parseSourceFromPathAndContents path contentsA
+        agdaFile0 <- indexFile src0
+
+        src1 <- TestData.parseSourceFromPathAndContents path contentsB
+        agdaFile1 <- indexFile src1
+
+        src2 <- TestData.parseSourceFromPathAndContents path contentsA
+        agdaFile2 <- indexFile src2
+
+        liftIO $ agdaFile0 @?= agdaFile2
diff --git a/test/TestData.hs b/test/TestData.hs
@@ -12,6 +12,7 @@ module TestData
     AgdaFileDetails (..),
     agdaFileDetails,
     parseSourceFromPath,
+    parseSourceFromPathAndContents,
   )
 where
 
@@ -44,10 +45,12 @@ import qualified Server.CommandController as CommandController
 import Server.Model (Model (Model))
 import Server.Model.AgdaFile (AgdaFile, emptyAgdaFile)
 import Server.Model.AgdaLib (agdaLibIncludes, initAgdaLib)
-import Server.Model.Monad (runWithAgdaLib)
+import Server.Model.Monad (runWithAgdaLib, MonadAgdaLib)
 import qualified Server.ResponseController as ResponseController
 import System.FilePath (takeBaseName, (</>))
 import Agda.TypeChecking.Pretty (prettyTCM)
+import Data.Text (Text)
+import Agda.Interaction.Imports.Virtual (parseSourceFromContents)
 
 data AgdaFileDetails = AgdaFileDetails
   { fileName :: String,
@@ -84,16 +87,30 @@ agdaFileDetails inPath = do
 
   return $ AgdaFileDetails testName file interface
 
-parseSourceFromPath :: (TCM.MonadTCM m) => FilePath -> m Imp.Source
-parseSourceFromPath path = do
+sourceFileFromPath :: (TCM.MonadTCM m) => FilePath -> m SourceFile
+sourceFileFromPath path = do
   absPath <- liftIO $ absolute path
 #if MIN_VERSION_Agda(2,8,0)
-  srcFile <- TCM.liftTCM $ TCM.srcFromPath absPath
+  TCM.liftTCM $ TCM.srcFromPath absPath
 #else
-  let srcFile = SourceFile absPath
+  return $ SourceFile absPath
 #endif
+
+parseSourceFromPath :: (TCM.MonadTCM m) => FilePath -> m Imp.Source
+parseSourceFromPath path = do
+  srcFile <- sourceFileFromPath path
   TCM.liftTCM $ Imp.parseSource srcFile
 
+parseSourceFromPathAndContents ::
+  (TCM.MonadTCM m, TCM.MonadTrace m, MonadAgdaLib m) =>
+  FilePath ->
+  Text ->
+    m Imp.Source
+parseSourceFromPathAndContents path contents = do
+  srcFile <- sourceFileFromPath path
+  let uri = LSP.toNormalizedUri $ LSP.filePathToUri path
+  parseSourceFromContents uri srcFile contents
+
 --------------------------------------------------------------------------------
 
 documentSymbolMessage :: LSP.NormalizedUri -> LSP.TRequestMessage LSP.Method_TextDocumentDocumentSymbol

Original file line number	Diff line number	Diff line change
`@@ -66,6 +66,7 @@ data SymbolInfo = SymbolInfo`
`66`	`66`	`symbolType :: !(Maybe String),`
`67`	`67`	`symbolParent :: !(Maybe A.QName)`
`68`	`68`	`}`
	`69`	`+ deriving (Eq)`
`69`	`70`
`70`	`71`	`instance Pretty SymbolInfo where`
`71`	`72`	`pretty symbolInfo =`
`@@ -115,6 +116,7 @@ data Ref = Ref`
`115`	`116`	`refRange :: !LSP.Range,`
`116`	`117`	`refIsAmbiguous :: !Bool`
`117`	`118`	`}`
	`119`	`+ deriving (Eq)`
`118`	`120`
`119`	`121`	`prettyAmbiguity :: Ref -> Doc`
`120`	`122`	`prettyAmbiguity ref =`