support Agda 2.8.0 in tests

Author: nvarner

src/Indexer.hs

@@ -2,6 +2,7 @@
 
 module Indexer
   ( withAstFor,
+    usingSrcAsCurrent,
     indexFile,
   )
 where
@@ -21,41 +22,48 @@ import Indexer.Postprocess (postprocess)
 import Server.Model.AgdaFile (AgdaFile)
 import Server.Model.Monad (WithAgdaLibM)
 
-withAstFor :: Imp.Source -> (TopLevelInfo -> WithAgdaLibM a) -> WithAgdaLibM a
+usingSrcAsCurrent :: Imp.Source -> WithAgdaLibM a -> WithAgdaLibM a
 #if MIN_VERSION_Agda(2,8,0)
-withAstFor src f = do
+usingSrcAsCurrent src x = do
   TCM.liftTCM $
     TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $
       -- Now reset the options
       TCM.setCommandLineOptions . TCM.stPersistentOptions . TCM.stPersistentState =<< TCM.getTC
 
   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
-    let topLevel =
-          TopLevel
-            (Imp.srcOrigin src)
-            (Imp.srcModuleName src)
-            (C.modDecls $ Imp.srcModule src)
-    ast <- TCM.liftTCM $ toAbstract topLevel
-    f ast
+  TCM.localTC (\e -> e {TCM.envCurrentPath = Just (TCM.srcFileId $ Imp.srcOrigin src)}) x
 #else
-withAstFor src f = do
+usingSrcAsCurrent src x = do
   TCM.liftTCM $
     TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $
       -- Now reset the options
       TCM.setCommandLineOptions . TCM.stPersistentOptions . TCM.stPersistentState =<< TCM.getTC
 
   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
-    let topLevel =
-          TopLevel
-            (srcFilePath $ Imp.srcOrigin src)
-            (Imp.srcModuleName src)
-            (C.modDecls $ Imp.srcModule src)
-    ast <- TCM.liftTCM $ toAbstract topLevel
-    f ast
+  TCM.localTC (\e -> e {TCM.envCurrentPath = Just (srcFilePath $ Imp.srcOrigin src)}) x
+#endif
+
+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
+#else
+withAstFor src f = usingSrcAsCurrent src $ do
+  let topLevel =
+        TopLevel
+          (srcFilePath $ Imp.srcOrigin src)
+          (Imp.srcModuleName src)
+          (C.modDecls $ Imp.srcModule src)
+  ast <- TCM.liftTCM $ toAbstract topLevel
+  f ast
 #endif
 
 indexFile ::

test/Test/Indexer/Invariants.hs

@@ -1,28 +1,11 @@
 module Test.Indexer.Invariants (tests) where
 
-import Agda.Interaction.FindFile (SourceFile (SourceFile), srcFilePath)
-import qualified Agda.Interaction.Imports as Imp
-import Agda.Interaction.Options (defaultOptions)
-import Agda.Syntax.Abstract.More ()
-import Agda.Syntax.Common.Pretty (prettyShow)
-import Agda.Syntax.Translation.ConcreteToAbstract (TopLevelInfo (topLevelDecls))
-import qualified Agda.TypeChecking.Monad as TCM
-import Agda.Utils.FileName (absolute)
 import Control.Monad (forM)
-import Control.Monad.IO.Class (liftIO)
-import qualified Data.Map as Map
-import Indexer (indexFile, withAstFor)
-import qualified Language.LSP.Protocol.Types as LSP
-import qualified Language.LSP.Server as LSP
-import Monad (runServerT)
-import Server.Model.Monad (runWithAgdaLib)
-import System.FilePath (takeBaseName, (</>))
 import Test.Indexer.NoDuplicateDecl (testNoDuplicateDecl)
 import Test.Indexer.NoMissing (testNoMissing)
 import Test.Indexer.NoOverlap (testNoOverlap)
 import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.Golden (findByExtension)
-import TestData (AgdaFileDetails (AgdaFileDetails))
 import qualified TestData
 
 tests :: IO TestTree

test/TestData.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 
 module TestData
@@ -13,7 +14,13 @@ module TestData
   )
 where
 
-import Agda.Interaction.FindFile (SourceFile (SourceFile), srcFilePath)
+import Agda.Interaction.FindFile
+  ( SourceFile (SourceFile),
+#if MIN_VERSION_Agda(2,8,0)
+#else
+    srcFilePath,
+#endif
+  )
 import qualified Agda.Interaction.Imports as Imp
 import qualified Agda.Interaction.Options
 import Agda.Syntax.Abstract.More ()
@@ -26,11 +33,11 @@ import Agda.Utils.Lens (set, (<&>))
 import Control.Concurrent (newChan)
 import Control.Monad.IO.Class (MonadIO, liftIO)
 import qualified Data.Map as Map
-import Indexer (indexFile, withAstFor)
+import Indexer (indexFile, withAstFor, usingSrcAsCurrent)
 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 (Env (Env), runServerT)
+import Monad (Env (Env), runServerT, catchTCError)
 import Options (defaultOptions, initConfig)
 import qualified Server.CommandController as CommandController
 import Server.Model (Model (Model))
@@ -39,6 +46,7 @@ import Server.Model.AgdaLib (agdaLibIncludes, initAgdaLib)
 import Server.Model.Monad (runWithAgdaLib)
 import qualified Server.ResponseController as ResponseController
 import System.FilePath (takeBaseName, (</>))
+import Agda.TypeChecking.Pretty (prettyTCM)
 
 data AgdaFileDetails = AgdaFileDetails
   { fileName :: String,
@@ -55,32 +63,29 @@ agdaFileDetails inPath = do
   (file, interface) <- LSP.runLspT undefined $ do
     env <- TestData.getServerEnv model
     runServerT env $ do
-      interface <- runWithAgdaLib uri $ do
-        TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions
-        absInPath <- liftIO $ absolute inPath
-        let srcFile = SourceFile absInPath
-        src <- TCM.liftTCM $ Imp.parseSource srcFile
-
-        TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (srcFilePath $ Imp.srcOrigin src)
+      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
+
+            f src
+
+      let onErr = \err -> runWithAgdaLib uri $ do
+            t <- TCM.liftTCM $ prettyTCM err
+            error $ prettyShow t
+
+      interface <- (withSrc $ \src -> usingSrcAsCurrent src $ do
         checkResult <- TCM.liftTCM $ Imp.typeCheckMain Imp.TypeCheck src
-        return $ Imp.crInterface checkResult
-
-      ast <- runWithAgdaLib uri $ do
-        TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions
-        absInPath <- liftIO $ absolute inPath
-        let srcFile = SourceFile absInPath
-        src <- TCM.liftTCM $ Imp.parseSource srcFile
-
-        withAstFor src return
+        return $ Imp.crInterface checkResult) `catchTCError` onErr
 
-      runWithAgdaLib uri $ do
-        TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions
-        absInPath <- liftIO $ absolute inPath
-        let srcFile = SourceFile absInPath
-        src <- TCM.liftTCM $ Imp.parseSource srcFile
+      file <- withSrc indexFile `catchTCError` onErr
 
-        agdaFile <- indexFile src
-        return (agdaFile, interface)
+      return (file, interface)
 
   return $ AgdaFileDetails testName file interface
 

test/data/Indexer/Module.agda

@@ -1,4 +1,4 @@
-module Module where
+module Indexer.Module where
 
 data Nat : Set where
   zero : Nat

test/data/test.agda-lib

@@ -0,0 +1,2 @@
+name: test
+include: .