Agda 2.6.4.3 compatibility

Author: nvarner

src/Agda/Interaction/Imports/More.hs

@@ -62,12 +62,14 @@ import Agda.Syntax.Common.Pretty (Pretty, pretty, text, prettyAssign, (<+>))
 import Agda.TypeChecking.Monad
   ( Interface,
     TCM,
-    checkAndSetOptionsFromPragma,
     setCurrentRange,
     setOptionsFromPragma,
     setTCLens,
     stPragmaOptions,
     useTC,
+#if MIN_VERSION_Agda(2,7,0)
+    checkAndSetOptionsFromPragma,
+#endif
 #if MIN_VERSION_Agda(2,8,0)
     runPM,
     runPMDropWarnings,
@@ -146,9 +148,13 @@ setOptionsFromSourcePragmas checkOpts src = do
   mapM_ setOpts (srcDefaultPragmas src)
   mapM_ setOpts (srcFilePragmas src)
   where
+#if MIN_VERSION_Agda(2,7,0)
     setOpts
       | checkOpts = checkAndSetOptionsFromPragma
       | otherwise = setOptionsFromPragma
+#else
+    setOpts = setOptionsFromPragma
+#endif
 
 -- Andreas, 2016-07-11, issue 2092
 -- The error range should be set to the file with the wrong module name

src/Agda/Syntax/Abstract/More.hs

@@ -7,7 +7,6 @@ import Agda.Syntax.Abstract
 import Agda.Syntax.Common
 import Agda.Syntax.Common (ArgInfo (argInfoOrigin))
 import Agda.Syntax.Common.Pretty
-import Agda.Syntax.Concrete (TacticAttribute' (theTacticAttribute))
 import Agda.Syntax.Info
 import Agda.Utils.Functor ((<&>))
 import Data.Foldable (Foldable (toList))

src/Indexer/Indexer.hs

@@ -136,7 +136,11 @@ instance Indexable A.Declaration where
           index decls
     A.PatternSynDef name bindings pat -> do
       tellDecl name PatternSyn UnknownType
+#if MIN_VERSION_Agda(2,7,0)
       forM_ bindings $ \(C.WithHiding _hiding binding) ->
+#else
+      forM_ bindings $ \(C.Arg _argInfo binding) ->
+#endif
         tellDef binding Param UnknownType
       let pat' :: A.Pattern = fmap absurd pat
       index pat'
@@ -302,7 +306,11 @@ instance (Indexable a) => Indexable (C.Arg a) where
     when (C.argInfoOrigin argInfo == C.UserWritten) $
       index x
 
+#if MIN_VERSION_Agda(2,7,0)
 instance Indexable A.TacticAttribute
+#else
+instance (Indexable a) => Indexable (C.Ranged a)
+#endif
 
 instance Indexable A.DefInfo where
   index = index . Info.defTactic
@@ -391,10 +399,12 @@ instance Indexable A.RewriteEqn where
           tellDef bindName Param UnknownType
         index pat
         index expr
+#if MIN_VERSION_Agda(2,7,0)
     C.LeftLet bindings ->
       forM_ bindings $ \(pat, expr) -> do
         index pat
         index expr
+#endif
 
 instance Indexable A.RHS where
   index rhs = case rhs of
@@ -556,18 +566,20 @@ instance Indexable A.Pragma where
       tellUsage name
     A.InjectivePragma name ->
       tellUsage name
-    A.InjectiveForInferencePragma name ->
-      tellUsage name
     A.InlinePragma _shouldInline name ->
       tellUsage name
     A.NotProjectionLikePragma name ->
       tellUsage name
-    A.OverlapPragma name _overlapMode ->
-      tellUsage name
     A.DisplayPragma name args displayExpr -> do
       tellUsage name
       indexNamedArgs name args
       index displayExpr
+#if MIN_VERSION_Agda(2,7,0)
+    A.InjectiveForInferencePragma name ->
+      tellUsage name
+    A.OverlapPragma name _overlapMode ->
+      tellUsage name
+#endif
 
 --------------------------------------------------------------------------------
 

src/Server/Model/Handler.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE KindSignatures #-}
@@ -26,6 +27,10 @@ import qualified Language.LSP.Server as LSP
 import Monad (ServerM, askModel, catchTCError, findAgdaLib)
 import qualified Server.Model as Model
 import Server.Model.Monad (WithAgdaFileM, WithAgdaLibM, runWithAgdaFileT, runWithAgdaLibT)
+#if MIN_VERSION_Agda(2,7,0)
+#else
+import Agda.TypeChecking.Errors ()
+#endif
 
 tryTC :: ServerM a -> ServerM (Either TCM.TCErr a)
 tryTC handler = (Right <$> handler) `catchTCError` (return . Left)

src/Server/Model/Monad.hs

@@ -25,7 +25,6 @@ module Server.Model.Monad
 where
 
 import Agda.Interaction.Options (CommandLineOptions (optPragmaOptions), PragmaOptions)
-import Agda.Interaction.Response (Response_boot (Resp_HighlightingInfo))
 import Agda.Syntax.Common.Pretty (prettyShow)
 import Agda.Syntax.Position (getRange)
 import Agda.TypeChecking.Monad (HasOptions (..), MonadTCEnv (..), MonadTCM (..), MonadTCState (..), MonadTrace, PersistentTCState (stPersistentOptions), ReadTCState (..), TCEnv (..), TCM, TCMT (..), TCState (stPersistentState), catchError_, modifyTCLens, setTCLens, stPragmaOptions, useTC, viewTC)
@@ -54,6 +53,11 @@ import Prelude hiding (null)
 #if MIN_VERSION_Agda(2,8,0)
 import Agda.Utils.FileId (File, getIdFile)
 #endif
+#if MIN_VERSION_Agda(2,7,0)
+import Agda.Interaction.Response (Response_boot(Resp_HighlightingInfo))
+#else
+import Agda.Interaction.Response (Response(Resp_HighlightingInfo))
+#endif
 
 --------------------------------------------------------------------------------