Agda 2.7.0.1 compatibility fixes

Author: nvarner

src/Agda/Interaction/Imports/More.hs

@@ -39,14 +39,14 @@ import Agda.Syntax.Position
   ( Range,
     Range' (Range),
     RangeFile,
-    beginningOfFile,
     getRange,
     intervalToRange,
     mkRangeFile,
     posToRange,
     posToRange',
     startPos,
 #if MIN_VERSION_Agda(2,8,0)
+    beginningOfFile,
     rangeFromAbsolutePath,
 #endif
   )
@@ -58,8 +58,7 @@ import Agda.Syntax.TopLevelModuleName (
 #endif
   )
 import Agda.TypeChecking.Monad
-  ( AbsolutePath,
-    Interface,
+  ( Interface,
     TCM,
     checkAndSetOptionsFromPragma,
     setCurrentRange,
@@ -78,6 +77,7 @@ import qualified Agda.TypeChecking.Monad.Benchmark as Bench
 #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

src/Agda/Interaction/Imports/Virtual.hs

@@ -3,13 +3,13 @@
 
 module Agda.Interaction.Imports.Virtual
   ( VSourceFile (..),
-    vSrcFileId,
     vSrcFromUri,
     parseVSource,
   )
 where
 
 #if MIN_VERSION_Agda(2,8,0)
+import Agda.TypeChecking.Monad (SourceFile (SourceFile))
 #else
 import Agda.Interaction.FindFile (SourceFile (SourceFile))
 #endif
@@ -18,6 +18,7 @@ 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 Agda.Utils.FileName (AbsolutePath)
 import Control.Monad.IO.Class (MonadIO)
 import Control.Monad.Trans (lift)
 import qualified Data.Strict as Strict
@@ -28,16 +29,20 @@ import qualified Language.LSP.Server as LSP
 import qualified Language.LSP.VFS as VFS
 
 data VSourceFile = VSourceFile
-  { vSrcFileSrcFile :: TCM.SourceFile,
+  { vSrcFileSrcFile :: SourceFile,
     vSrcUri :: LSP.NormalizedUri,
     vSrcVFile :: VFS.VirtualFile
   }
 
-vSrcFilePath :: (TCM.MonadFileId m) => VSourceFile -> m TCM.AbsolutePath
+#if MIN_VERSION_Agda(2,8,0)
+vSrcFilePath :: (TCM.MonadFileId m) => VSourceFile -> m AbsolutePath
 vSrcFilePath = TCM.srcFilePath . vSrcFileSrcFile
-
-vSrcFileId :: VSourceFile -> TCM.FileId
-vSrcFileId = TCM.srcFileId . vSrcFileSrcFile
+#else
+vSrcFilePath :: (Monad m) => VSourceFile -> m AbsolutePath
+vSrcFilePath vSourceFile = do
+  let (SourceFile path) = vSrcFileSrcFile vSourceFile
+  return path
+#endif
 
 #if MIN_VERSION_Agda(2,8,0)
 vSrcFromUri ::

src/Agda/Position.hs

@@ -24,6 +24,7 @@ import qualified Data.Strict.Maybe as Strict
 import Data.Text (Text)
 import qualified Data.Text as Text
 import qualified Language.LSP.Protocol.Types as LSP
+import Data.Functor (void)
 
 -- Note:  LSP srclocs are 0-base
 --        Agda srclocs are 1-base
@@ -73,8 +74,8 @@ intervalEnd :: Interval -> PositionWithoutFile
 intervalStart (Interval _ start _end) = start
 intervalEnd (Interval _ _start end) = end
 #else
-intervalStart (Interval start _end) = start
-intervalEnd (Interval _start end) = end
+intervalStart (Interval start _end) = void start
+intervalEnd (Interval _start end) = void end
 #endif
 
 -- | Agda Range -> LSP Range

stack.yaml.lock

@@ -5,9 +5,9 @@
 
 packages:
 - completed:
-    hackage: Agda-2.8.0@sha256:f85f3b10eb034687b07d073686ab97c947082eecc5ad268cbe20a4c774abcaae,34434
+    hackage: Agda-2.8.0@sha256:b73b1b6685650d4429074f10440952cecb7aef190a994f75d168c354d20b01a8,34453
     pantry-tree:
-      sha256: 01cbe34629f37fa56a411390d4d9fa281bb92b8a66a6757232240f58380678a7
+      sha256: 7dace5cc1fe5a4f09212dda58392ae29f34bb1382c6eb04cb86514b5f5e2da32
       size: 43914
   original:
     hackage: Agda-2.8.0