[ change ] Drop support for Agda-2.6.2.2 and Agda-2.6.4

src/Agda.hs

@@ -26,9 +26,7 @@ import           Agda.Interaction.Base          ( Command
                                                 , CommandState(optionsOnReload)
                                                 , IOTCM
                                                 , initCommandState
-#if MIN_VERSION_Agda(2,6,3)
                                                 , parseIOTCM
-#endif
                                                 )
 #if MIN_VERSION_Agda(2,6,4)
 import           Agda.Syntax.Common.Pretty      ( render, vcat )
@@ -180,14 +178,6 @@ handleCommandReq (CmdReq cmd) = do
       provideCommand iotcm
       return $ CmdRes Nothing
 
-#if !MIN_VERSION_Agda(2,6,3)
-parseIOTCM :: String -> Either String IOTCM
-parseIOTCM raw = case listToMaybe $ reads raw of
-  Just (x, ""     ) -> Right x
-  Just (_, remnent) -> Left $ "not consumed: " ++ remnent
-  _                 -> Left $ "cannot read: " ++ raw
-#endif
-
 --------------------------------------------------------------------------------
 
 getCommandLineOptions
@@ -202,12 +192,8 @@ getCommandLineOptions = do
 
   result <- runExceptT $ do
     let p = parseBackendOptions builtinBackends merged defaultOptions
-#if MIN_VERSION_Agda(2,6,3)
     let (r, _warns) = runOptM p
     (bs, opts) <- ExceptT $ pure r
-#else
-    (bs, opts) <- ExceptT $ runOptM p
-#endif
     return opts
   case result of
     -- something bad happened, use the default options instead

src/Agda/Convert.hs

@@ -22,10 +22,7 @@ import Agda.Syntax.Concrete as C
 import Agda.Syntax.Internal (alwaysUnblock)
 import Agda.Syntax.Position (HasRange (getRange), Range, noRange)
 import Agda.Syntax.Scope.Base
-import Agda.TypeChecking.Errors (getAllWarningsOfTCErr, prettyError)
-#if MIN_VERSION_Agda(2,6,3)
-import Agda.TypeChecking.Errors (explainWhyInScope)
-#endif
+import Agda.TypeChecking.Errors (getAllWarningsOfTCErr, prettyError, explainWhyInScope)
 import Agda.TypeChecking.Monad hiding (Function)
 import Agda.TypeChecking.Monad.MetaVars (withInteractionId)
 import Agda.TypeChecking.Pretty (prettyTCM)
@@ -278,13 +275,8 @@ fromDisplayInfo = \case
           "Definitions about"
             <+> text (List.intercalate ", " $ words names) $$ nest 2 (align 10 hitDocs)
     return $ IR.DisplayInfoGeneric "Search About" [Unlabeled (Render.text $ show doc) Nothing Nothing]
-#if MIN_VERSION_Agda(2,6,3)
   Info_WhyInScope why -> do
     doc <- explainWhyInScope why
-#else
-  Info_WhyInScope s cwd v xs ms -> do
-    doc <- explainWhyInScope s cwd v xs ms
-#endif
     return $ IR.DisplayInfoGeneric "Scope Info" [Unlabeled (Render.text $ show doc) Nothing Nothing]
   Info_Context ii ctx -> do
     doc <- localTCState (prettyResponseContexts ii False ctx)
@@ -373,91 +365,6 @@ lispifyGoalSpecificDisplayInfo ii kind = localTCState $
 
 --------------------------------------------------------------------------------
 
-#if !MIN_VERSION_Agda(2,6,3)
-explainWhyInScope ::
-  String ->
-  FilePath ->
-  Maybe LocalVar ->
-  [AbstractName] ->
-  [AbstractModule] ->
-  TCM Doc
-explainWhyInScope s _ Nothing [] [] = TCP.text (s ++ " is not in scope.")
-explainWhyInScope s _ v xs ms =
-  TCP.vcat
-    [ TCP.text (s ++ " is in scope as"),
-      TCP.nest 2 $ TCP.vcat [variable v xs, modules ms]
-    ]
-  where
-    -- variable :: Maybe _ -> [_] -> TCM Doc
-    variable Nothing vs = names vs
-    variable (Just x) vs
-      | null vs = asVar
-      | otherwise =
-        TCP.vcat
-          [ TCP.sep [asVar, TCP.nest 2 $ shadowing x],
-            TCP.nest 2 $ names vs
-          ]
-      where
-        asVar :: TCM Doc
-        asVar =
-          "* a variable bound at" TCP.<+> TCP.prettyTCM (nameBindingSite $ localVar x)
-        shadowing :: LocalVar -> TCM Doc
-        shadowing (LocalVar _ _ []) = "shadowing"
-        shadowing _ = "in conflict with"
-    names = TCP.vcat . fmap pName
-    modules = TCP.vcat . fmap pMod
-
-    pKind = \case
-      AxiomName                -> "postulate"
-      ConName                  -> "constructor"
-      CoConName                -> "coinductive constructor"
-      DataName                 -> "data type"
-      DisallowedGeneralizeName -> "generalizable variable from let open"
-      FldName                  -> "record field"
-      FunName                  -> "defined name"
-      GeneralizeName           -> "generalizable variable"
-      MacroName                -> "macro name"
-      PatternSynName           -> "pattern synonym"
-      PrimName                 -> "primitive function"
-      QuotableName             -> "quotable name"
-      -- previously DefName:
-      RecName                  -> "record type"
-      OtherDefName             -> "defined name"
-
-    pName :: AbstractName -> TCM Doc
-    pName a =
-      TCP.sep
-        [ "* a"
-            TCP.<+> pKind (anameKind a)
-            TCP.<+> TCP.text (prettyShow $ anameName a),
-          TCP.nest 2 "brought into scope by"
-        ]
-        TCP.$$ TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ anameName a) (anameLineage a))
-    pMod :: AbstractModule -> TCM Doc
-    pMod a =
-      TCP.sep
-        [ "* a module" TCP.<+> TCP.text (prettyShow $ amodName a),
-          TCP.nest 2 "brought into scope by"
-        ]
-        TCP.$$ TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ mnameToQName $ amodName a) (amodLineage a))
-
-    pWhy :: Range -> WhyInScope -> TCM Doc
-    pWhy r Defined = "- its definition at" TCP.<+> TCP.prettyTCM r
-    pWhy r (Opened (C.QName x) w) | isNoName x = pWhy r w
-    pWhy r (Opened m w) =
-      "- the opening of"
-        TCP.<+> TCP.prettyTCM m
-        TCP.<+> "at"
-        TCP.<+> TCP.prettyTCM (getRange m)
-        TCP.$$ pWhy r w
-    pWhy r (Applied m w) =
-      "- the application of"
-        TCP.<+> TCP.prettyTCM m
-        TCP.<+> "at"
-        TCP.<+> TCP.prettyTCM (getRange m)
-        TCP.$$ pWhy r w
-#endif
-
 -- | Pretty-prints the context of the given meta-variable.
 prettyResponseContexts ::
   -- | Context of this meta-variable.

src/Agda/Parser.hs

@@ -7,9 +7,7 @@ module Agda.Parser where
 import Agda.Syntax.Parser (parseFile, runPMIO, tokensParser)
 import Agda.Syntax.Parser.Tokens (Token)
 import Agda.Syntax.Position (Position' (posPos), PositionWithoutFile, Range, getRange, rEnd', rStart')
-#if MIN_VERSION_Agda(2,6,3)
 import Agda.Syntax.Position (RangeFile(RangeFile))
-#endif
 import Agda.Utils.FileName (mkAbsolute)
 import Monad ( ServerM )
 import Control.Monad.State
@@ -27,22 +25,12 @@ tokenAt :: LSP.Uri -> Text -> PositionWithoutFile -> ServerM (LspM Config) (Mayb
 tokenAt uri source position = case LSP.uriToFilePath uri of
   Nothing -> return Nothing
   Just filepath -> do
-    let file =
-#if MIN_VERSION_Agda(2,6,3)
-          RangeFile (mkAbsolute filepath) Nothing
-#else
-          mkAbsolute filepath
-#endif
+    let file = RangeFile (mkAbsolute filepath) Nothing
     (result, _warnings) <- liftIO $
       runPMIO $ do
         -- parse the file and get all tokens
         (r, _fileType) <- parseFile tokensParser file (unpack source)
-        let tokens =
-#if MIN_VERSION_Agda(2,6,3)
-              fst r
-#else
-              r
-#endif
+        let tokens = fst r
         -- find the token at the position
         return $ find (pointedBy position) tokens
     case result of

src/Agda/Position.hs

@@ -39,11 +39,7 @@ toAgdaRange table path (LSP.Range start end) = Range
   interval :: IntervalWithoutFile
   interval = Interval (toAgdaPositionWithoutFile table start)
                       (toAgdaPositionWithoutFile table end)
-#if MIN_VERSION_Agda(2,6,3)
   mkRangeFile path = RangeFile path Nothing
-#else
-  mkRangeFile = id
-#endif
 
 -- | LSP Position -> Agda PositionWithoutFile
 toAgdaPositionWithoutFile :: ToOffset -> LSP.Position -> PositionWithoutFile

src/Render/Common.hs

@@ -17,7 +17,10 @@ import Agda.Syntax.Common
       QωOrigin(..),
       LensCohesion(getCohesion),
       NameId(..),
-      Erased(..), asQuantity, Lock(..), LockOrigin (..), 
+      Erased(..), asQuantity, Lock(..), 
+#if MIN_VERSION_Agda(2,6,4)
+      LockOrigin (..), 
+#endif
 #if MIN_VERSION_Agda(2,7,0)
       OverlapMode (..),
 #endif
@@ -38,11 +41,7 @@ instance Render NameId where
 
 -- | MetaId
 instance Render MetaId where
-#if MIN_VERSION_Agda(2,6,3)
   render (MetaId n m) = text $ "_" ++ show n ++ "@" ++ show m
-#else
-  render (MetaId n) = text $ "_" ++ show n
-#endif
 
 -- | Relevance
 instance Render Relevance where
@@ -112,8 +111,12 @@ renderQuantity a d =
 
 instance Render Lock where
   render = \case
+#if MIN_VERSION_Agda(2,6,4)
     IsLock LockOLock -> "@lock"
     IsLock LockOTick -> "@tick"
+#else 
+    IsLock -> "@lock"
+#endif
     IsNotLock -> mempty
 
 #if MIN_VERSION_Agda(2,7,0)

src/Render/Concrete.hs

@@ -120,10 +120,6 @@ instance Render Expr where
     Rec _ xs -> sep ["record", bracesAndSemicolons (fmap render xs)]
     RecUpdate _ e xs ->
       sep ["record" <+> render e, bracesAndSemicolons (fmap render xs)]
-#if !MIN_VERSION_Agda(2,6,3)
-    ETel [] -> "()"
-    ETel tel -> fsep $ fmap render tel
-#endif
     Quote _ -> "quote"
     QuoteTerm _ -> "quoteTerm"
     Unquote _ -> "unquote"
@@ -550,10 +546,8 @@ instance Render Declaration where
       UnquoteDef _ xs t ->
         fsep ["unquoteDef" <+> fsep (fmap render xs) <+> "=", render t]
       Pragma pr -> sep ["{-#" <+> render pr, "#-}"]
-#if MIN_VERSION_Agda(2,6,3)
       UnquoteData _ x xs e ->
         fsep [ hsep [ "unquoteData", render x, fsep (fmap render xs), "=" ], render e ]
-#endif
 #if MIN_VERSION_Agda(2,6,4)
       Opaque _ ds ->
         namedBlock "opaque" ds
@@ -697,10 +691,8 @@ instance Render Pragma where
   render (PolarityPragma _ q occs) =
     hsep ("POLARITY" : render q : fmap render occs)
   render (NoUniverseCheckPragma _) = "NO_UNIVERSE_CHECK"
-#if MIN_VERSION_Agda(2,6,3)
   render (NotProjectionLikePragma _ q) =
     hsep [ "NOT_PROJECTION_LIKE", render q ]
-#endif
 #if MIN_VERSION_Agda(2,7,0)
   render (InjectiveForInferencePragma _ i) =
     hsep $ ["INJECTIVE_FOR_INFERENCE", render i]
@@ -716,20 +708,12 @@ instance Render Fixity where
         RightAssoc -> "infixr"
         NonAssoc -> "infix"
 
-#if MIN_VERSION_Agda(2,6,3)
 instance Render NotationPart where
   render = \case
     IdPart  x  -> text $ rangedThing x
     HolePart{} -> "_"
     VarPart {} -> "_"
     WildPart{} -> "_"
-#else
-instance Render GenPart where
-  render (IdPart x) = text $ rangedThing x
-  render BindHole {} = "_"
-  render NormalHole {} = "_"
-  render WildHole {} = "_"
-#endif
 
 instance Render Fixity' where
   render (Fixity' fix nota _)

src/Render/Interaction.hs

@@ -109,10 +109,8 @@ instance (Render a, Render b) => Render (OutputConstraint a b) where
     "Check lock" <+> render lk <+> "allows" <+> render t
   render (UsableAtMod modality t) =
     "Is usable at" <+> render modality <+> render t
-#if MIN_VERSION_Agda(2,6,3)
   render (DataSort _name expr) =
     fsep [ "Sort", render expr, "allows data/record definitions" ]
-#endif
 
 -- | IPBoundary'
 instance Render c => Render (IPBoundary' c) where

src/Render/Internal.hs

@@ -25,12 +25,7 @@ instance Render a => Render (Substitution' a) where
         IdS -> "idS"
         EmptyS _ -> "emptyS"
         t :# rho -> mparens (p > 2) $ sep [pr 2 rho <> ",", renderPrec 3 t]
-#if MIN_VERSION_Agda(2,6,3)
-        Strengthen _ _ rho ->
-#else
-        Strengthen _ rho ->
-#endif
-          mparens (p > 9) $ "strS" <+> pr 10 rho
+        Strengthen _ _ rho -> mparens (p > 9) $ "strS" <+> pr 10 rho
         Wk n rho -> mparens (p > 9) $ text ("wkS " ++ show n) <+> pr 10 rho
         Lift n rho -> mparens (p > 9) $ text ("liftS " ++ show n) <+> pr 10 rho
 
@@ -170,9 +165,7 @@ instance Render Sort where
       MetaS x es -> renderPrec p $ MetaV x es
       DefS d es -> renderPrec p $ Def d es
       DummyS s -> parens $ text s
-#if MIN_VERSION_Agda(2,6,3)
       IntervalUniv -> "IntervalUniv"
-#endif
 #if MIN_VERSION_Agda(2,6,4)
    where
      suffix n = applyWhen (n /= 0) (++ show n)
@@ -223,6 +216,4 @@ instance Render Blocker where
   render (UnblockOnAny us)      = "any" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)
   render (UnblockOnMeta m)      = render m
   render (UnblockOnProblem pid) = "problem" <+> render pid
-#if MIN_VERSION_Agda(2,6,3)
   render (UnblockOnDef q)       = "definition" <+> render q
-#endif

src/Render/Position.hs

@@ -12,10 +12,8 @@ import Render.RichText
 instance Render AbsolutePath where
   render = text . filePath
 
-#if MIN_VERSION_Agda(2,6,3)
 instance Render RangeFile where
   render = render . rangeFilePath  -- TODO rangeFileName ?
-#endif
 
 --------------------------------------------------------------------------------
 

src/Render/RichText.hs

@@ -214,10 +214,8 @@ instance {-# OVERLAPS #-} ToJSON Agda.SrcFile where
 instance ToJSON Agda.AbsolutePath where
   toJSON (Agda.AbsolutePath path) = toJSON path
 
-#if MIN_VERSION_Agda(2,6,3)
 instance ToJSON Agda.RangeFile where
   toJSON (Agda.RangeFile path _maybeTopLevelModuleName) = toJSON path
-#endif
 
 --------------------------------------------------------------------------------
 

src/Server/Handler.hs

@@ -100,12 +100,7 @@ inferTypeOfText filepath text = runCommandM $ do
   let norm = AsIs
   -- localStateCommandM: restore TC state afterwards, do we need this here?
   typ <- localStateCommandM $ do
-#if MIN_VERSION_Agda(2,6,3)
-    (e, _attrs)
-#else
-    e
-#endif
-       <- lift $ runPM $ parse exprParser (unpack text)
+    (e, _attrs) <- lift $ runPM $ parse exprParser (unpack text)
     lift $ atTopLevel $ do
       concreteToAbstract_ e >>= typeInCurrent norm