Skip to content

Commit e9651ad

Browse files
banacornbanacorn
committed
[ change ] Drop support for Agda-2.6.2.2 and Agda-2.6.4
1 parent 8341835 commit e9651ad

16 files changed

+20
-302
lines changed

‎src/Agda.hs‎

Lines changed: 0 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -26,9 +26,7 @@ import Agda.Interaction.Base ( Command
2626
, CommandState(optionsOnReload)
2727
, IOTCM
2828
, initCommandState
29-
#if MIN_VERSION_Agda(2,6,3)
3029
, parseIOTCM
31-
#endif
3230
)
3331
#if MIN_VERSION_Agda(2,6,4)
3432
import Agda.Syntax.Common.Pretty ( render, vcat )
@@ -180,14 +178,6 @@ handleCommandReq (CmdReq cmd) = do
180178
provideCommand iotcm
181179
return $ CmdRes Nothing
182180

183-
#if !MIN_VERSION_Agda(2,6,3)
184-
parseIOTCM :: String -> Either String IOTCM
185-
parseIOTCM raw = case listToMaybe $ reads raw of
186-
Just (x, "" ) -> Right x
187-
Just (_, remnent) -> Left $ "not consumed: " ++ remnent
188-
_ -> Left $ "cannot read: " ++ raw
189-
#endif
190-
191181
--------------------------------------------------------------------------------
192182

193183
getCommandLineOptions
@@ -202,12 +192,8 @@ getCommandLineOptions = do
202192

203193
result <- runExceptT $ do
204194
let p = parseBackendOptions builtinBackends merged defaultOptions
205-
#if MIN_VERSION_Agda(2,6,3)
206195
let (r, _warns) = runOptM p
207196
(bs, opts) <- ExceptT $ pure r
208-
#else
209-
(bs, opts) <- ExceptT $ runOptM p
210-
#endif
211197
return opts
212198
case result of
213199
-- something bad happened, use the default options instead

‎src/Agda/Convert.hs‎

Lines changed: 1 addition & 94 deletions
Original file line numberDiff line numberDiff line change
@@ -22,10 +22,7 @@ import Agda.Syntax.Concrete as C
2222
import Agda.Syntax.Internal (alwaysUnblock)
2323
import Agda.Syntax.Position (HasRange (getRange), Range, noRange)
2424
import Agda.Syntax.Scope.Base
25-
import Agda.TypeChecking.Errors (getAllWarningsOfTCErr, prettyError)
26-
#if MIN_VERSION_Agda(2,6,3)
27-
import Agda.TypeChecking.Errors (explainWhyInScope)
28-
#endif
25+
import Agda.TypeChecking.Errors (getAllWarningsOfTCErr, prettyError, explainWhyInScope)
2926
import Agda.TypeChecking.Monad hiding (Function)
3027
import Agda.TypeChecking.Monad.MetaVars (withInteractionId)
3128
import Agda.TypeChecking.Pretty (prettyTCM)
@@ -278,13 +275,8 @@ fromDisplayInfo = \case
278275
"Definitions about"
279276
<+> text (List.intercalate ", " $ words names) $$ nest 2 (align 10 hitDocs)
280277
return $ IR.DisplayInfoGeneric "Search About" [Unlabeled (Render.text $ show doc) Nothing Nothing]
281-
#if MIN_VERSION_Agda(2,6,3)
282278
Info_WhyInScope why -> do
283279
doc <- explainWhyInScope why
284-
#else
285-
Info_WhyInScope s cwd v xs ms -> do
286-
doc <- explainWhyInScope s cwd v xs ms
287-
#endif
288280
return $ IR.DisplayInfoGeneric "Scope Info" [Unlabeled (Render.text $ show doc) Nothing Nothing]
289281
Info_Context ii ctx -> do
290282
doc <- localTCState (prettyResponseContexts ii False ctx)
@@ -373,91 +365,6 @@ lispifyGoalSpecificDisplayInfo ii kind = localTCState $
373365

374366
--------------------------------------------------------------------------------
375367

376-
#if !MIN_VERSION_Agda(2,6,3)
377-
explainWhyInScope ::
378-
String ->
379-
FilePath ->
380-
Maybe LocalVar ->
381-
[AbstractName] ->
382-
[AbstractModule] ->
383-
TCM Doc
384-
explainWhyInScope s _ Nothing [] [] = TCP.text (s ++ " is not in scope.")
385-
explainWhyInScope s _ v xs ms =
386-
TCP.vcat
387-
[ TCP.text (s ++ " is in scope as"),
388-
TCP.nest 2 $ TCP.vcat [variable v xs, modules ms]
389-
]
390-
where
391-
-- variable :: Maybe _ -> [_] -> TCM Doc
392-
variable Nothing vs = names vs
393-
variable (Just x) vs
394-
| null vs = asVar
395-
| otherwise =
396-
TCP.vcat
397-
[ TCP.sep [asVar, TCP.nest 2 $ shadowing x],
398-
TCP.nest 2 $ names vs
399-
]
400-
where
401-
asVar :: TCM Doc
402-
asVar =
403-
"* a variable bound at" TCP.<+> TCP.prettyTCM (nameBindingSite $ localVar x)
404-
shadowing :: LocalVar -> TCM Doc
405-
shadowing (LocalVar _ _ []) = "shadowing"
406-
shadowing _ = "in conflict with"
407-
names = TCP.vcat . fmap pName
408-
modules = TCP.vcat . fmap pMod
409-
410-
pKind = \case
411-
AxiomName -> "postulate"
412-
ConName -> "constructor"
413-
CoConName -> "coinductive constructor"
414-
DataName -> "data type"
415-
DisallowedGeneralizeName -> "generalizable variable from let open"
416-
FldName -> "record field"
417-
FunName -> "defined name"
418-
GeneralizeName -> "generalizable variable"
419-
MacroName -> "macro name"
420-
PatternSynName -> "pattern synonym"
421-
PrimName -> "primitive function"
422-
QuotableName -> "quotable name"
423-
-- previously DefName:
424-
RecName -> "record type"
425-
OtherDefName -> "defined name"
426-
427-
pName :: AbstractName -> TCM Doc
428-
pName a =
429-
TCP.sep
430-
[ "* a"
431-
TCP.<+> pKind (anameKind a)
432-
TCP.<+> TCP.text (prettyShow $ anameName a),
433-
TCP.nest 2 "brought into scope by"
434-
]
435-
TCP.$$ TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ anameName a) (anameLineage a))
436-
pMod :: AbstractModule -> TCM Doc
437-
pMod a =
438-
TCP.sep
439-
[ "* a module" TCP.<+> TCP.text (prettyShow $ amodName a),
440-
TCP.nest 2 "brought into scope by"
441-
]
442-
TCP.$$ TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ mnameToQName $ amodName a) (amodLineage a))
443-
444-
pWhy :: Range -> WhyInScope -> TCM Doc
445-
pWhy r Defined = "- its definition at" TCP.<+> TCP.prettyTCM r
446-
pWhy r (Opened (C.QName x) w) | isNoName x = pWhy r w
447-
pWhy r (Opened m w) =
448-
"- the opening of"
449-
TCP.<+> TCP.prettyTCM m
450-
TCP.<+> "at"
451-
TCP.<+> TCP.prettyTCM (getRange m)
452-
TCP.$$ pWhy r w
453-
pWhy r (Applied m w) =
454-
"- the application of"
455-
TCP.<+> TCP.prettyTCM m
456-
TCP.<+> "at"
457-
TCP.<+> TCP.prettyTCM (getRange m)
458-
TCP.$$ pWhy r w
459-
#endif
460-
461368
-- | Pretty-prints the context of the given meta-variable.
462369
prettyResponseContexts ::
463370
-- | Context of this meta-variable.

‎src/Agda/Parser.hs‎

Lines changed: 2 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,7 @@ module Agda.Parser where
77
import Agda.Syntax.Parser (parseFile, runPMIO, tokensParser)
88
import Agda.Syntax.Parser.Tokens (Token)
99
import Agda.Syntax.Position (Position' (posPos), PositionWithoutFile, Range, getRange, rEnd', rStart')
10-
#if MIN_VERSION_Agda(2,6,3)
1110
import Agda.Syntax.Position (RangeFile(RangeFile))
12-
#endif
1311
import Agda.Utils.FileName (mkAbsolute)
1412
import Monad ( ServerM )
1513
import Control.Monad.State
@@ -27,22 +25,12 @@ tokenAt :: LSP.Uri -> Text -> PositionWithoutFile -> ServerM (LspM Config) (Mayb
2725
tokenAt uri source position = case LSP.uriToFilePath uri of
2826
Nothing -> return Nothing
2927
Just filepath -> do
30-
let file =
31-
#if MIN_VERSION_Agda(2,6,3)
32-
RangeFile (mkAbsolute filepath) Nothing
33-
#else
34-
mkAbsolute filepath
35-
#endif
28+
let file = RangeFile (mkAbsolute filepath) Nothing
3629
(result, _warnings) <- liftIO $
3730
runPMIO $ do
3831
-- parse the file and get all tokens
3932
(r, _fileType) <- parseFile tokensParser file (unpack source)
40-
let tokens =
41-
#if MIN_VERSION_Agda(2,6,3)
42-
fst r
43-
#else
44-
r
45-
#endif
33+
let tokens = fst r
4634
-- find the token at the position
4735
return $ find (pointedBy position) tokens
4836
case result of

‎src/Agda/Position.hs‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -39,11 +39,7 @@ toAgdaRange table path (LSP.Range start end) = Range
3939
interval :: IntervalWithoutFile
4040
interval = Interval (toAgdaPositionWithoutFile table start)
4141
(toAgdaPositionWithoutFile table end)
42-
#if MIN_VERSION_Agda(2,6,3)
4342
mkRangeFile path = RangeFile path Nothing
44-
#else
45-
mkRangeFile = id
46-
#endif
4743

4844
-- | LSP Position -> Agda PositionWithoutFile
4945
toAgdaPositionWithoutFile :: ToOffset -> LSP.Position -> PositionWithoutFile

‎src/Render/Common.hs‎

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,10 @@ import Agda.Syntax.Common
1717
QωOrigin(..),
1818
LensCohesion(getCohesion),
1919
NameId(..),
20-
Erased(..), asQuantity, Lock(..), LockOrigin (..),
20+
Erased(..), asQuantity, Lock(..),
21+
#if MIN_VERSION_Agda(2,6,4)
22+
LockOrigin (..),
23+
#endif
2124
#if MIN_VERSION_Agda(2,7,0)
2225
OverlapMode (..),
2326
#endif
@@ -38,11 +41,7 @@ instance Render NameId where
3841

3942
-- | MetaId
4043
instance Render MetaId where
41-
#if MIN_VERSION_Agda(2,6,3)
4244
render (MetaId n m) = text $ "_" ++ show n ++ "@" ++ show m
43-
#else
44-
render (MetaId n) = text $ "_" ++ show n
45-
#endif
4645

4746
-- | Relevance
4847
instance Render Relevance where
@@ -112,8 +111,12 @@ renderQuantity a d =
112111

113112
instance Render Lock where
114113
render = \case
114+
#if MIN_VERSION_Agda(2,6,4)
115115
IsLock LockOLock -> "@lock"
116116
IsLock LockOTick -> "@tick"
117+
#else
118+
IsLock -> "@lock"
119+
#endif
117120
IsNotLock -> mempty
118121

119122
#if MIN_VERSION_Agda(2,7,0)

‎src/Render/Concrete.hs‎

Lines changed: 0 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -120,10 +120,6 @@ instance Render Expr where
120120
Rec _ xs -> sep ["record", bracesAndSemicolons (fmap render xs)]
121121
RecUpdate _ e xs ->
122122
sep ["record" <+> render e, bracesAndSemicolons (fmap render xs)]
123-
#if !MIN_VERSION_Agda(2,6,3)
124-
ETel [] -> "()"
125-
ETel tel -> fsep $ fmap render tel
126-
#endif
127123
Quote _ -> "quote"
128124
QuoteTerm _ -> "quoteTerm"
129125
Unquote _ -> "unquote"
@@ -550,10 +546,8 @@ instance Render Declaration where
550546
UnquoteDef _ xs t ->
551547
fsep ["unquoteDef" <+> fsep (fmap render xs) <+> "=", render t]
552548
Pragma pr -> sep ["{-#" <+> render pr, "#-}"]
553-
#if MIN_VERSION_Agda(2,6,3)
554549
UnquoteData _ x xs e ->
555550
fsep [ hsep [ "unquoteData", render x, fsep (fmap render xs), "=" ], render e ]
556-
#endif
557551
#if MIN_VERSION_Agda(2,6,4)
558552
Opaque _ ds ->
559553
namedBlock "opaque" ds
@@ -697,10 +691,8 @@ instance Render Pragma where
697691
render (PolarityPragma _ q occs) =
698692
hsep ("POLARITY" : render q : fmap render occs)
699693
render (NoUniverseCheckPragma _) = "NO_UNIVERSE_CHECK"
700-
#if MIN_VERSION_Agda(2,6,3)
701694
render (NotProjectionLikePragma _ q) =
702695
hsep [ "NOT_PROJECTION_LIKE", render q ]
703-
#endif
704696
#if MIN_VERSION_Agda(2,7,0)
705697
render (InjectiveForInferencePragma _ i) =
706698
hsep $ ["INJECTIVE_FOR_INFERENCE", render i]
@@ -716,20 +708,12 @@ instance Render Fixity where
716708
RightAssoc -> "infixr"
717709
NonAssoc -> "infix"
718710

719-
#if MIN_VERSION_Agda(2,6,3)
720711
instance Render NotationPart where
721712
render = \case
722713
IdPart x -> text $ rangedThing x
723714
HolePart{} -> "_"
724715
VarPart {} -> "_"
725716
WildPart{} -> "_"
726-
#else
727-
instance Render GenPart where
728-
render (IdPart x) = text $ rangedThing x
729-
render BindHole {} = "_"
730-
render NormalHole {} = "_"
731-
render WildHole {} = "_"
732-
#endif
733717

734718
instance Render Fixity' where
735719
render (Fixity' fix nota _)

‎src/Render/Interaction.hs‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -109,10 +109,8 @@ instance (Render a, Render b) => Render (OutputConstraint a b) where
109109
"Check lock" <+> render lk <+> "allows" <+> render t
110110
render (UsableAtMod modality t) =
111111
"Is usable at" <+> render modality <+> render t
112-
#if MIN_VERSION_Agda(2,6,3)
113112
render (DataSort _name expr) =
114113
fsep [ "Sort", render expr, "allows data/record definitions" ]
115-
#endif
116114

117115
-- | IPBoundary'
118116
instance Render c => Render (IPBoundary' c) where

‎src/Render/Internal.hs‎

Lines changed: 1 addition & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -25,12 +25,7 @@ instance Render a => Render (Substitution' a) where
2525
IdS -> "idS"
2626
EmptyS _ -> "emptyS"
2727
t :# rho -> mparens (p > 2) $ sep [pr 2 rho <> ",", renderPrec 3 t]
28-
#if MIN_VERSION_Agda(2,6,3)
29-
Strengthen _ _ rho ->
30-
#else
31-
Strengthen _ rho ->
32-
#endif
33-
mparens (p > 9) $ "strS" <+> pr 10 rho
28+
Strengthen _ _ rho -> mparens (p > 9) $ "strS" <+> pr 10 rho
3429
Wk n rho -> mparens (p > 9) $ text ("wkS " ++ show n) <+> pr 10 rho
3530
Lift n rho -> mparens (p > 9) $ text ("liftS " ++ show n) <+> pr 10 rho
3631

@@ -170,9 +165,7 @@ instance Render Sort where
170165
MetaS x es -> renderPrec p $ MetaV x es
171166
DefS d es -> renderPrec p $ Def d es
172167
DummyS s -> parens $ text s
173-
#if MIN_VERSION_Agda(2,6,3)
174168
IntervalUniv -> "IntervalUniv"
175-
#endif
176169
#if MIN_VERSION_Agda(2,6,4)
177170
where
178171
suffix n = applyWhen (n /= 0) (++ show n)
@@ -223,6 +216,4 @@ instance Render Blocker where
223216
render (UnblockOnAny us) = "any" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)
224217
render (UnblockOnMeta m) = render m
225218
render (UnblockOnProblem pid) = "problem" <+> render pid
226-
#if MIN_VERSION_Agda(2,6,3)
227219
render (UnblockOnDef q) = "definition" <+> render q
228-
#endif

‎src/Render/Position.hs‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,8 @@ import Render.RichText
1212
instance Render AbsolutePath where
1313
render = text . filePath
1414

15-
#if MIN_VERSION_Agda(2,6,3)
1615
instance Render RangeFile where
1716
render = render . rangeFilePath -- TODO rangeFileName ?
18-
#endif
1917

2018
--------------------------------------------------------------------------------
2119

‎src/Render/RichText.hs‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -214,10 +214,8 @@ instance {-# OVERLAPS #-} ToJSON Agda.SrcFile where
214214
instance ToJSON Agda.AbsolutePath where
215215
toJSON (Agda.AbsolutePath path) = toJSON path
216216

217-
#if MIN_VERSION_Agda(2,6,3)
218217
instance ToJSON Agda.RangeFile where
219218
toJSON (Agda.RangeFile path _maybeTopLevelModuleName) = toJSON path
220-
#endif
221219

222220
--------------------------------------------------------------------------------
223221

0 commit comments

Comments
 (0)