clear state before loading files

Author: nvarner

agda-language-server.cabal

@@ -186,11 +186,13 @@ 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.NoDuplicateDecl
-      Test.Indexer.NoMissing
-      Test.Indexer.NoOverlap
+      Test.Indexer.Reload
       Test.LSP
       Test.Model
       Test.ModelMonad

src/Indexer.hs

@@ -27,6 +27,8 @@ import Server.Model.Monad (WithAgdaLibM)
 
 usingSrcAsCurrent :: Imp.Source -> WithAgdaLibM a -> WithAgdaLibM a
 usingSrcAsCurrent src x = do
+  TCM.liftTCM TCM.resetState
+
   TCM.liftTCM $ Imp.setOptionsFromSourcePragmas True src
 
   TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $
@@ -35,118 +37,30 @@ usingSrcAsCurrent src x = do
 
 #if MIN_VERSION_Agda(2,8,0)
   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
+  TCM.localTC (\e -> e {TCM.envCurrentPath = Just (TCM.srcFileId $ Imp.srcOrigin src)}) x
 #else
   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
+  TCM.localTC (\e -> e {TCM.envCurrentPath = Just (srcFilePath $ Imp.srcOrigin src)}) x
 #endif
-    x
 
 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
+#if MIN_VERSION_Agda(2,8,0)
+  let srcFile = Imp.srcOrigin src
 #else
-withAstFor src f = usingSrcAsCurrent src $ do
+  let srcFile = srcFilePath $ Imp.srcOrigin src
+#endif
   let topLevel =
         TopLevel
-          (srcFilePath $ Imp.srcOrigin src)
+          srcFile
           (Imp.srcModuleName src)
           (C.modDecls $ Imp.srcModule src)
   ast <- TCM.liftTCM $ toAbstract topLevel
   f ast
-#endif
 
 indexFile ::
   Imp.Source ->
   WithAgdaLibM AgdaFile
 indexFile src = withAstFor src $ \ast -> execIndexerM $ do
   indexAst ast
   postprocess
-
--- 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

test/Test.hs

@@ -14,6 +14,7 @@ import qualified Test.ModelMonad as ModelMonad
 import qualified Test.Indexer.Invariants as IndexerInvariants
 import qualified Test.Indexer.NoAnonFunSymbol as NoAnonFunSymbol
 import qualified Test.Uri as URI
+import qualified Test.Indexer as Indexer
 
 -- Define the custom option
 newtype AlsPathOption = AlsPathOption FilePath
@@ -33,7 +34,7 @@ main = do
 
 tests :: IO TestTree
 tests = do
-  indexerInvariantsTest <- IndexerInvariants.tests
+  indexerTests <- Indexer.tests
   return $ askOption $ \(AlsPathOption alsPath) ->
     testGroup
       "Tests"
@@ -42,8 +43,7 @@ tests = do
         URI.tests,
         Model.tests,
         ModelMonad.tests,
-        indexerInvariantsTest,
-        NoAnonFunSymbol.tests
+        indexerTests
 #if defined(wasm32_HOST_ARCH)
       , WASM.tests alsPath
 #endif

test/Test/Indexer.hs

@@ -0,0 +1,16 @@
+module Test.Indexer (tests) where
+
+import qualified Test.Indexer.Invariants as Invariants
+import qualified Test.Indexer.NoAnonFunSymbol as NoAnonFunSymbol
+import qualified Test.Indexer.Reload as Reload
+import Test.Tasty (TestTree, testGroup)
+
+tests :: IO TestTree
+tests = do
+  invariantsTests <- Invariants.tests
+  return $
+    testGroup "Indexer" $
+      [ invariantsTests,
+        NoAnonFunSymbol.tests,
+        Reload.tests
+      ]

test/Test/Indexer/Invariants.hs

@@ -1,9 +1,9 @@
 module Test.Indexer.Invariants (tests) where
 
 import Control.Monad (forM)
-import Test.Indexer.NoDuplicateDecl (testNoDuplicateDecl)
-import Test.Indexer.NoMissing (testNoMissing)
-import Test.Indexer.NoOverlap (testNoOverlap)
+import Test.Indexer.Invariants.NoDuplicateDecl (testNoDuplicateDecl)
+import Test.Indexer.Invariants.NoMissing (testNoMissing)
+import Test.Indexer.Invariants.NoOverlap (testNoOverlap)
 import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.Golden (findByExtension)
 import qualified TestData

test/Test/Indexer/NoDuplicateDecl.hs renamed to test/Test/Indexer/Invariants/NoDuplicateDecl.hs

@@ -1,4 +1,4 @@
-module Test.Indexer.NoDuplicateDecl (testNoDuplicateDecl) where
+module Test.Indexer.Invariants.NoDuplicateDecl (testNoDuplicateDecl) where
 
 import qualified Agda.Syntax.Abstract as A
 import Agda.Syntax.Common.Pretty (Pretty, align, pretty, prettyList, prettyShow, text, vcat, (<+>))

test/Test/Indexer/NoMissing.hs renamed to test/Test/Indexer/Invariants/NoMissing.hs

@@ -1,7 +1,7 @@
 -- | 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
+module Test.Indexer.Invariants.NoMissing (testNoMissing) where
 
 import Agda.Interaction.Highlighting.Precise (Aspects, HighlightingInfo)
 import qualified Agda.Interaction.Highlighting.Precise as HL

test/Test/Indexer/NoOverlap.hs renamed to test/Test/Indexer/Invariants/NoOverlap.hs

@@ -1,6 +1,6 @@
 -- | Check that `Ref`s don't overlap, so that there is only one `Ref` instance
 -- per actual reference.
-module Test.Indexer.NoOverlap (testNoOverlap) where
+module Test.Indexer.Invariants.NoOverlap (testNoOverlap) where
 
 import qualified Agda.Syntax.Abstract as A
 import Agda.Syntax.Common.Pretty (Doc, Pretty (prettyList), align, parens, pretty, prettyShow, text, vcat, (<+>))

test/Test/Indexer/Reload.hs

@@ -0,0 +1,30 @@
+module Test.Indexer.Reload (tests) where
+
+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 qualified TestData
+
+tests :: TestTree
+tests =
+  testGroup "Reload" $
+    [ testCase "Reload single file" $ testReloadFile "test/data/A.agda"
+    ]
+
+testReloadFile :: FilePath -> IO ()
+testReloadFile path = do
+  let uri = LSP.filePathToUri path
+  model <- TestData.getModel
+
+  LSP.runLspT undefined $ do
+    env <- TestData.getServerEnv model
+    runServerT env $ do
+      runWithAgdaLib uri $ do
+        src <- TestData.parseSourceFromPath path
+        _ <- indexFile src
+        _ <- indexFile src
+        return ()

test/TestData.hs

@@ -11,6 +11,7 @@ module TestData
     getServerEnv,
     AgdaFileDetails (..),
     agdaFileDetails,
+    parseSourceFromPath,
   )
 where
 
@@ -65,13 +66,7 @@ agdaFileDetails inPath = do
     runServerT env $ do
       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
+            src <- parseSourceFromPath inPath
 
             f src
 
@@ -89,6 +84,16 @@ agdaFileDetails inPath = do
 
   return $ AgdaFileDetails testName file interface
 
+parseSourceFromPath :: (TCM.MonadTCM m) => FilePath -> m Imp.Source
+parseSourceFromPath path = do
+  absPath <- liftIO $ absolute path
+#if MIN_VERSION_Agda(2,8,0)
+  srcFile <- TCM.liftTCM $ TCM.srcFromPath absPath
+#else
+  let srcFile = SourceFile absPath
+#endif
+  TCM.liftTCM $ Imp.parseSource srcFile
+
 --------------------------------------------------------------------------------
 
 documentSymbolMessage :: LSP.NormalizedUri -> LSP.TRequestMessage LSP.Method_TextDocumentDocumentSymbol