From 0c4667aa695b490657732fe34019e78428faff7e Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Sun, 1 Dec 2024 13:12:02 +0800 Subject: [PATCH 01/11] [ fix ] Upgrade instance of Render Declaration to v2.7.0 --- src/Render/Common.hs | 9 +++++- src/Render/Concrete.hs | 52 ++++++++++++++++++++++++++++---- src/Render/RichText.hs | 17 +++++++++-- stack-9.2-Agda-2.6.4.3.yaml.lock | 28 +++++++++++++++++ stack.yaml | 2 +- 5 files changed, 97 insertions(+), 11 deletions(-) diff --git a/src/Render/Common.hs b/src/Render/Common.hs index 74842f9..0ac1376 100644 --- a/src/Render/Common.hs +++ b/src/Render/Common.hs @@ -16,7 +16,9 @@ import Agda.Syntax.Common Cohesion(..), QωOrigin(..), LensCohesion(getCohesion), - NameId(..) ) + NameId(..), + Erased(..), asQuantity, + ) import qualified Agda.Utils.Null as Agda import Agda.Utils.List1 (toList) import Agda.Utils.Functor ((<&>)) @@ -91,6 +93,11 @@ renderQuantity :: LensQuantity a => a -> Inlines -> Inlines renderQuantity a d = if show d == "_" then d else render (getQuantity a) <+> d +#if MIN_VERSION_Agda(2,7,0) +renderErased :: Erased -> Inlines -> Inlines +renderErased = renderQuantity . asQuantity +#endif + renderCohesion :: LensCohesion a => a -> Inlines -> Inlines renderCohesion a d = if show d == "_" then d else render (getCohesion a) <+> d diff --git a/src/Render/Concrete.hs b/src/Render/Concrete.hs index 22abea6..757028a 100644 --- a/src/Render/Concrete.hs +++ b/src/Render/Concrete.hs @@ -418,15 +418,25 @@ instance Render Declaration where render e ] ] + +#if MIN_VERSION_Agda(2,7,0) + Record _ erased x dir tel e cs -> pRecord erased x dir tel (Just e) cs +#else #if MIN_VERSION_Agda(2,6,4) - Record _ _er x dir tel e cs -> + Record _ _er x dir tel e cs -> pRecord x dir tel (Just e) cs +#else + Record _ x dir tel e cs -> pRecord x dir tel (Just e) cs +#endif +#endif +#if MIN_VERSION_Agda(2,7,0) + RecordDef _ x dir tel cs -> pRecord defaultErased x dir tel Nothing cs #else - Record _ x dir tel e cs -> + RecordDef _ x dir tel cs -> pRecord x dir tel Nothing cs #endif - pRecord x dir tel (Just e) cs - RecordDef _ x dir tel cs -> - pRecord x dir tel Nothing cs +#if MIN_VERSION_Agda(2,7,0) +#else RecordDirective r -> pRecordDirective r +#endif Infix f xs -> render f <+> fsep (punctuate "," $ fmap render (toList xs)) Syntax n _ -> "syntax" <+> render n <+> "..." PatternSyn _ n as p -> @@ -523,7 +533,36 @@ pRecordDirective = \case Eta eta -> pHasEta0 (rangedThing eta) PatternOrCopattern{} -> "pattern" - +#if MIN_VERSION_Agda(2,7,0) +pRecord + :: Erased + -> Name + -> [RecordDirective] + -> [LamBinding] + -> Maybe Expr + -> [Declaration] + -> Inlines +pRecord erased x directives tel me ds = vcat + [ sep + [ hsep [ "record" + , renderErased erased (render x) + , fsep (map render tel) + ] + , pType me + ] + , vcat $ concat + [ map render directives + , map render ds + ] + ] + where pType (Just e) = hsep + [ ":" + , render e + , "where" + ] + pType Nothing = + "where" +#else pRecord :: Name -> RecordDirectives -> @@ -561,6 +600,7 @@ pRecord x (RecordDirectives ind eta pat con) tel me cs = YesEta -> "eta-equality" NoEta _ -> "no-eta-equality" pCon = maybeToList $ (("constructor" <+>) . render) . fst <$> con +#endif instance Render OpenShortHand where render DoOpen = "open" diff --git a/src/Render/RichText.hs b/src/Render/RichText.hs index ab8ec46..aecde9b 100644 --- a/src/Render/RichText.hs +++ b/src/Render/RichText.hs @@ -212,9 +212,20 @@ instance ToJSON Agda.RangeFile where -- | Utilities / Combinators --- -- TODO: implement this --- indent :: Inlines -> Inlines --- indent x = " " <> x + +-- TODO: implement this +-- Modeled after `nest` defined in ‘Text.PrettyPrint.Annotated.HughesPJ’ (pretty-1.1.3.6) +-- +-- Indent a Inline by a given number of positions (which may also be negative). `indent` satisfies the laws: +-- +-- `indent` 0 x = x +-- `indent` k ( `indent` k' x) = `indent` (k+k') x +-- `indent` k (x `<>` y) = `indent` k z `<>` `indent` k y +-- `indent` k (x `$$` y) = `indent` k x `$$` `indent` k y +-- `indent` k `empty` = `empty` +-- `x <> indent k y = x <> y` , if x non-empty +-- indent :: Int -> Inlines -> Inlines +-- indent 0 x = x punctuate :: Inlines -> [Inlines] -> [Inlines] punctuate _ [] = [] diff --git a/stack-9.2-Agda-2.6.4.3.yaml.lock b/stack-9.2-Agda-2.6.4.3.yaml.lock index ab40cde..4e8b7e4 100644 --- a/stack-9.2-Agda-2.6.4.3.yaml.lock +++ b/stack-9.2-Agda-2.6.4.3.yaml.lock @@ -11,6 +11,34 @@ packages: size: 42904 original: hackage: Agda-2.6.4.3 +- completed: + hackage: lsp-2.7.0.0@sha256:2a64b40a69fd9638056ca552d5660203019473061cff1d09dccc0c94e40a275c,3834 + pantry-tree: + sha256: 630a5e18d7783c35a296268959c8d9348ee6dc94540047ea58146b310d8de941 + size: 1120 + original: + hackage: lsp-2.7.0.0@sha256:2a64b40a69fd9638056ca552d5660203019473061cff1d09dccc0c94e40a275c,3834 +- completed: + hackage: lsp-types-2.3.0.0@sha256:ca17a686bda5dc7ff04105ca7081dce5a90bcd050c8800a13efd68b7f0901f1c,34215 + pantry-tree: + sha256: 0bf22e394dc804c8cee74d19a7f38021cfd48a15082b39a14753c037f2a64288 + size: 51996 + original: + hackage: lsp-types-2.3.0.0@sha256:ca17a686bda5dc7ff04105ca7081dce5a90bcd050c8800a13efd68b7f0901f1c,34215 +- completed: + hackage: mod-0.2.0.1@sha256:eeb316fef3a8c12f4e83bbeeea748e74d75fca54d4498d574ace92e464adb05a,2409 + pantry-tree: + sha256: d469d7e415c1593f052d3ca647e4085ab759be378d25ca7d2eea0aab0083ce38 + size: 590 + original: + hackage: mod-0.2.0.1@sha256:eeb316fef3a8c12f4e83bbeeea748e74d75fca54d4498d574ace92e464adb05a,2409 +- completed: + hackage: row-types-1.0.1.2@sha256:4d4c7cb95d06a32b28ba977852d52a26b4c1f695ef083a6fd874ab6d79933b64,3071 + pantry-tree: + sha256: 6a3617038d3970095100d14d026c396002a115700500cf3004ffb67ae5a75611 + size: 1060 + original: + hackage: row-types-1.0.1.2@sha256:4d4c7cb95d06a32b28ba977852d52a26b4c1f695ef083a6fd874ab6d79933b64,3071 snapshots: - completed: sha256: 5a59b2a405b3aba3c00188453be172b85893cab8ebc352b1ef58b0eae5d248a2 diff --git a/stack.yaml b/stack.yaml index c7c64fe..4009418 100644 --- a/stack.yaml +++ b/stack.yaml @@ -7,7 +7,7 @@ packages: - . extra-deps: -- Agda-2.6.4.3 +- Agda-2.7.0.1 - lsp-2.7.0.0@sha256:2a64b40a69fd9638056ca552d5660203019473061cff1d09dccc0c94e40a275c,3834 - lsp-types-2.3.0.0@sha256:ca17a686bda5dc7ff04105ca7081dce5a90bcd050c8800a13efd68b7f0901f1c,34215 - mod-0.2.0.1@sha256:eeb316fef3a8c12f4e83bbeeea748e74d75fca54d4498d574ace92e464adb05a,2409 From afe2c37ad405931ed7c3dd417dddb0e4d1055c45 Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Mon, 2 Dec 2024 12:56:07 +0800 Subject: [PATCH 02/11] [ fix ] Upgrade instance of Render NameBinding to v2.7.0 --- src/Render/Concrete.hs | 33 ++++++++++++++++++++++++++++++++- 1 file changed, 32 insertions(+), 1 deletion(-) diff --git a/src/Render/Concrete.hs b/src/Render/Concrete.hs index 757028a..82d65dd 100644 --- a/src/Render/Concrete.hs +++ b/src/Render/Concrete.hs @@ -17,7 +17,8 @@ import Agda.Utils.List1 as List1 (toList, fromList) import qualified Agda.Utils.List1 as List1 import qualified Agda.Utils.List2 as List2 import Agda.Utils.Float (toStringWithoutDotZero) -import Agda.Utils.Function (applyWhen) +import Agda.Utils.Function +import Agda.Utils.Null import Agda.Utils.Functor (dget, (<&>)) import Agda.Utils.Impossible (__IMPOSSIBLE__) @@ -27,6 +28,7 @@ import Render.Literal () import Render.Name () import Render.RichText import Render.TypeChecking () +import Prelude hiding (null) -------------------------------------------------------------------------------- @@ -172,6 +174,28 @@ instance Render a => Render (Binder' a) where -- | NamedBinding instance Render NamedBinding where +#if MIN_VERSION_Agda(2,7,0) + render (NamedBinding withH + x@(Arg (ArgInfo h (Modality r q c) _o _fv (Annotation lock)) + (Named _mn xb@(Binder _mp (BName _y _fix t _fin))))) = + applyWhen withH prH $ + applyWhenJust (isLabeled x) (\ l -> (text l <+>) . ("=" <+>)) (render xb) + -- isLabeled looks at _mn and _y + -- pretty xb prints also the pattern _mp + where + prH = (render r <>) + . renderHiding h mparens + . (coh <+>) + . (qnt <+>) + . (lck <+>) + . (tac <+>) + coh = render c + qnt = render q + tac = render t + lck = render lock + -- Parentheses are needed when an attribute @... is printed + mparens = applyUnless (null coh && null qnt && null lck && null tac) parens +#else render (NamedBinding withH x) = prH $ if @@ -192,13 +216,20 @@ instance Render NamedBinding where mparens' | noUserQuantity x, Nothing <- bnameTactic bn = id | otherwise = parens +#endif renderTactic :: BoundName -> Inlines -> Inlines renderTactic = renderTactic' . bnameTactic renderTactic' :: TacticAttribute -> Inlines -> Inlines +#if MIN_VERSION_Agda(2,7,0) +renderTactic' t = (render t <+>) +#else renderTactic' Nothing d = d renderTactic' (Just t) d = "@" <> (parens ("tactic " <> render t) <+> d) +#endif + + -------------------------------------------------------------------------------- From 11b92a1ab3c45d2e151cce39393790ab4992ef6e Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Mon, 2 Dec 2024 13:04:22 +0800 Subject: [PATCH 03/11] [ fix ] Upgrade instance of Render WhereClause to v2.7.0 --- src/Render/Concrete.hs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Render/Concrete.hs b/src/Render/Concrete.hs index 82d65dd..da4be15 100644 --- a/src/Render/Concrete.hs +++ b/src/Render/Concrete.hs @@ -297,6 +297,17 @@ instance Render WhereClause where | isNoName (unqualify x) = vcat ["where", vcat $ fmap render ds] render (AnyWhere _range ds) = vcat ["where", vcat $ fmap render ds] +#if MIN_VERSION_Agda(2,7,0) + render (SomeWhere _ erased m a ds) = + vcat [ hsep $ privateWhenUserWritten a + [ "module", renderErased erased (render m), "where" ] + , vcat $ map render ds + ] + where + privateWhenUserWritten = \case + PrivateAccess _ UserWritten -> ("private" :) + _ -> id +#else #if MIN_VERSION_Agda(2,6,4) render (SomeWhere _range _er m a ds) = #else @@ -310,6 +321,7 @@ instance Render WhereClause where ["module", render m, "where"], vcat $ fmap render ds ] +#endif instance Render LHS where render (LHS p eqs es) = From 9e88b32c77bf392a96b2079b1c56437eb51a2293 Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Mon, 2 Dec 2024 13:12:39 +0800 Subject: [PATCH 04/11] [ fix ] Make Inlines an instance of Null --- src/Render/Concrete.hs | 6 ++++++ src/Render/RichText.hs | 37 +++++++++++++++++++++---------------- 2 files changed, 27 insertions(+), 16 deletions(-) diff --git a/src/Render/Concrete.hs b/src/Render/Concrete.hs index da4be15..43731a5 100644 --- a/src/Render/Concrete.hs +++ b/src/Render/Concrete.hs @@ -32,6 +32,12 @@ import Prelude hiding (null) -------------------------------------------------------------------------------- +#if MIN_VERSION_Agda(2,7,0) +instance Render a => Render (TacticAttribute' a) where + render (TacticAttribute t) = + ifNull (render t) empty $ \ d -> "@" <> parens ("tactic" <+> d) +#endif + instance Render a => Render (Ranged a) where render = render . rangedThing diff --git a/src/Render/RichText.hs b/src/Render/RichText.hs index aecde9b..f63061f 100644 --- a/src/Render/RichText.hs +++ b/src/Render/RichText.hs @@ -53,6 +53,8 @@ import Data.String (IsString (..)) import qualified Data.Strict.Maybe as Strict import GHC.Generics (Generic) +import Agda.Utils.Null +import Prelude hiding (null) -------------------------------------------------------------------------------- -- | Block elements @@ -104,27 +106,30 @@ instance ToJSON Inlines where instance Show Inlines where show (Inlines xs) = unwords $ map show $ toList xs --- | see if the rendered text is "empty" -isEmpty :: Inlines -> Bool -isEmpty (Inlines elems) = all elemIsEmpty (Seq.viewl elems) - where - elemIsEmpty :: Inline -> Bool - elemIsEmpty (Icon _ _) = False - elemIsEmpty (Text "" _) = True - elemIsEmpty (Text _ _) = False - elemIsEmpty (Link _ xs _) = all elemIsEmpty $ unInlines xs - elemIsEmpty (Hole _) = False - elemIsEmpty (Horz xs) = all isEmpty xs - elemIsEmpty (Vert xs) = all isEmpty xs - elemIsEmpty (Parn _) = False - elemIsEmpty (PrHz _) = False +instance Null Inlines where + empty = mempty + null (Inlines elems) = all elemIsNull (Seq.viewl elems) + where + elemIsNull :: Inline -> Bool + elemIsNull (Icon _ _) = False + elemIsNull (Text "" _) = True + elemIsNull (Text _ _) = False + elemIsNull (Link _ xs _) = all elemIsNull $ unInlines xs + elemIsNull (Hole _) = False + elemIsNull (Horz xs) = all null xs + elemIsNull (Vert xs) = all null xs + elemIsNull (Parn _) = False + elemIsNull (PrHz _) = False + +-- -- | see if the rendered text is "empty" + infixr 6 <+> (<+>) :: Inlines -> Inlines -> Inlines x <+> y - | isEmpty x = y - | isEmpty y = x + | null x = y + | null y = x | otherwise = x <> " " <> y -- | Whitespace From 9d00f38a61bee437a5b1ef5ccf1d2d46be750edc Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Mon, 2 Dec 2024 13:18:10 +0800 Subject: [PATCH 05/11] [ fix ] Make Lock an instance of Render --- src/Render/Class.hs | 4 ++++ src/Render/Common.hs | 8 +++++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/Render/Class.hs b/src/Render/Class.hs index 201fe04..1bd3892 100644 --- a/src/Render/Class.hs +++ b/src/Render/Class.hs @@ -78,6 +78,10 @@ instance Render Bool where instance Render Doc where render = text . Doc.render +instance Render a => Render (Maybe a) where + renderPrec p Nothing = mempty + renderPrec p (Just x) = renderPrec p x + instance Render a => Render [a] where render xs = "[" <> fsep (punctuate "," (fmap render xs)) <> "]" instance Render a => Render (List1 a) where diff --git a/src/Render/Common.hs b/src/Render/Common.hs index 0ac1376..cde02fd 100644 --- a/src/Render/Common.hs +++ b/src/Render/Common.hs @@ -17,7 +17,7 @@ import Agda.Syntax.Common QωOrigin(..), LensCohesion(getCohesion), NameId(..), - Erased(..), asQuantity, + Erased(..), asQuantity, Lock(..), LockOrigin (..), ) import qualified Agda.Utils.Null as Agda import Agda.Utils.List1 (toList) @@ -93,6 +93,12 @@ renderQuantity :: LensQuantity a => a -> Inlines -> Inlines renderQuantity a d = if show d == "_" then d else render (getQuantity a) <+> d +instance Render Lock where + render = \case + IsLock LockOLock -> "@lock" + IsLock LockOTick -> "@tick" + IsNotLock -> mempty + #if MIN_VERSION_Agda(2,7,0) renderErased :: Erased -> Inlines -> Inlines renderErased = renderQuantity . asQuantity From e927b3d02ac6d7aee604cb8eaf4a23f3d2d1aeb7 Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Mon, 2 Dec 2024 13:33:26 +0800 Subject: [PATCH 06/11] [ fix ] Upgrade instance of Render Declaration to v2.7.0 --- src/Render/Concrete.hs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/Render/Concrete.hs b/src/Render/Concrete.hs index 43731a5..7850e89 100644 --- a/src/Render/Concrete.hs +++ b/src/Render/Concrete.hs @@ -392,10 +392,12 @@ instance Render Declaration where where mkInst (InstanceDef _) f = sep ["instance", f] mkInst NotInstanceDef f = f - - mkOverlap j f - | isOverlappable j = "overlap" <+> f - | otherwise = f +#if MIN_VERSION_Agda(2,7,0) + mkOverlap i d | isYesOverlap i = "overlap" <+> d +#else + mkOverlap i d | isOverlappable i = "overlap" <+> d +#endif + | otherwise = d Field _ fs -> sep [ "field", @@ -570,6 +572,9 @@ pHasEta0 = \case YesEta -> "eta-equality" NoEta () -> "no-eta-equality" +instance Render RecordDirective where + render = pRecordDirective + pRecordDirective :: RecordDirective -> Inlines From d2a7d2473f5b2a01d7b3b429b5cd875b0f507030 Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Mon, 2 Dec 2024 14:00:02 +0800 Subject: [PATCH 07/11] [ fix ] Exports from Agda.Interaction in v2.7.0 --- src/Agda.hs | 7 +++++++ src/Agda/Convert.hs | 4 ++++ src/Render/Class.hs | 1 - src/Render/Interaction.hs | 4 ++++ src/Server/Handler.hs | 12 ++++++++++-- 5 files changed, 25 insertions(+), 3 deletions(-) diff --git a/src/Agda.hs b/src/Agda.hs index 994bc98..9a5e614 100644 --- a/src/Agda.hs +++ b/src/Agda.hs @@ -17,7 +17,10 @@ import Agda.Compiler.Builtin ( builtinBackends ) import Agda.Convert ( fromResponse ) import Agda.Interaction.Base ( Command , Command'(Command, Done, Error) +#if MIN_VERSION_Agda(2,7,0) +#else , CommandM +#endif , CommandState(optionsOnReload) , IOTCM , initCommandState @@ -32,6 +35,10 @@ import Agda.Interaction.InteractionTop ( initialiseCommandQueue , maybeAbort , runInteraction +#if MIN_VERSION_Agda(2,7,0) + , CommandM +#else +#endif ) import Agda.Interaction.Options ( CommandLineOptions ( optAbsoluteIncludePaths diff --git a/src/Agda/Convert.hs b/src/Agda/Convert.hs index 152569a..7c9e835 100644 --- a/src/Agda/Convert.hs +++ b/src/Agda/Convert.hs @@ -58,6 +58,10 @@ import qualified Data.Map as Map import Data.String (IsString) import qualified Render +#if MIN_VERSION_Agda(2,7,0) +import Agda.Interaction.Output ( OutputConstraint ) +#endif + responseAbbr :: IsString a => Response -> a responseAbbr res = case res of Resp_HighlightingInfo {} -> "Resp_HighlightingInfo" diff --git a/src/Render/Class.hs b/src/Render/Class.hs index 1bd3892..6ac7718 100644 --- a/src/Render/Class.hs +++ b/src/Render/Class.hs @@ -1,7 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeSynonymInstances #-} module Render.Class ( Render (..), diff --git a/src/Render/Interaction.hs b/src/Render/Interaction.hs index b35958e..420b6ea 100644 --- a/src/Render/Interaction.hs +++ b/src/Render/Interaction.hs @@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} module Render.Interaction where @@ -7,6 +8,9 @@ import qualified Data.Map as Map import qualified Data.Set as Set import Agda.Interaction.Base +#if MIN_VERSION_Agda(2,7,0) +import Agda.Interaction.Output ( OutputForm, OutputConstraint ) +#endif import Agda.Syntax.Internal ( Blocker(..) ) import Agda.TypeChecking.Monad import Render.Class diff --git a/src/Server/Handler.hs b/src/Server/Handler.hs index f8cf932..d73538a 100644 --- a/src/Server/Handler.hs +++ b/src/Server/Handler.hs @@ -6,8 +6,12 @@ import Agda ( getCommandLineOptions , runAgda ) import qualified Agda.IR as IR -import Agda.Interaction.Base ( CommandM - , CommandQueue(..) + +import Agda.Interaction.Base ( CommandQueue(..) +#if MIN_VERSION_Agda(2,7,0) +#else + , CommandM +#endif , CommandState(optionsOnReload) , Rewrite(AsIs) , initCommandState @@ -21,6 +25,10 @@ import qualified Agda.Interaction.Imports as Imp import Agda.Interaction.InteractionTop ( cmd_load' , localStateCommandM +#if MIN_VERSION_Agda(2,7,0) + , CommandM +#else +#endif ) import Agda.Interaction.Options ( CommandLineOptions ( optAbsoluteIncludePaths From 8f270caec2b21ed77d55249db7db85b826995f06 Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Mon, 2 Dec 2024 14:08:07 +0800 Subject: [PATCH 08/11] [ fix ] Handle Response_Mimer from v2.7.0 --- src/Agda/Convert.hs | 6 ++++++ src/Agda/IR.hs | 1 + 2 files changed, 7 insertions(+) diff --git a/src/Agda/Convert.hs b/src/Agda/Convert.hs index 7c9e835..190d034 100644 --- a/src/Agda/Convert.hs +++ b/src/Agda/Convert.hs @@ -71,6 +71,9 @@ responseAbbr res = case res of Resp_GiveAction {} -> "Resp_GiveAction" Resp_MakeCase {} -> "Resp_MakeCase" Resp_SolveAll {} -> "Resp_SolveAll" +#if MIN_VERSION_Agda(2,7,0) + Resp_Mimer {} -> "Resp_Mimer" +#endif Resp_DisplayInfo {} -> "Resp_DisplayInfo" Resp_RunningInfo {} -> "Resp_RunningInfo" Resp_ClearRunningInfo {} -> "Resp_ClearRunningInfo" @@ -101,6 +104,9 @@ fromResponse (Resp_GiveAction (InteractionId i) giveAction) = return $ IR.ResponseGiveAction i (fromAgda giveAction) fromResponse (Resp_MakeCase _ Function pcs) = return $ IR.ResponseMakeCaseFunction pcs fromResponse (Resp_MakeCase _ ExtendedLambda pcs) = return $ IR.ResponseMakeCaseExtendedLambda pcs +#if MIN_VERSION_Agda(2,7,0) +fromResponse (Resp_Mimer (InteractionId i) s) = return $ IR.ResponseMimer i s +#endif fromResponse (Resp_SolveAll ps) = return $ IR.ResponseSolveAll (fmap prn ps) where prn (InteractionId i, e) = (i, prettyShow e) diff --git a/src/Agda/IR.hs b/src/Agda/IR.hs index bf454a8..fb96494 100644 --- a/src/Agda/IR.hs +++ b/src/Agda/IR.hs @@ -40,6 +40,7 @@ data Response ResponseMakeCaseFunction [String] | ResponseMakeCaseExtendedLambda [String] | ResponseSolveAll [(Int, String)] + | ResponseMimer Int (Maybe String) | -- priority: 3 ResponseJumpToError FilePath Int | ResponseEnd From 26def0e14c6d4558efb08a3ffcbc3976fed6c54b Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Mon, 2 Dec 2024 14:14:23 +0800 Subject: [PATCH 09/11] [ fix ] Handle new pragmas from v2.7.0 --- src/Render/Common.hs | 18 +++++++++++++++++- src/Render/Concrete.hs | 5 +++++ 2 files changed, 22 insertions(+), 1 deletion(-) diff --git a/src/Render/Common.hs b/src/Render/Common.hs index cde02fd..759fa74 100644 --- a/src/Render/Common.hs +++ b/src/Render/Common.hs @@ -17,7 +17,10 @@ import Agda.Syntax.Common QωOrigin(..), LensCohesion(getCohesion), NameId(..), - Erased(..), asQuantity, Lock(..), LockOrigin (..), + Erased(..), asQuantity, Lock(..), LockOrigin (..), +#if MIN_VERSION_Agda(2,7,0) + OverlapMode (..), +#endif ) import qualified Agda.Utils.Null as Agda import Agda.Utils.List1 (toList) @@ -74,6 +77,19 @@ instance Render Cohesion where -------------------------------------------------------------------------------- +#if MIN_VERSION_Agda(2,7,0) +instance Render OverlapMode where + render = \case + Overlappable -> "OVERLAPPABLE" + Overlapping -> "OVERLAPPING" + Incoherent -> "INCOHERENT" + Overlaps -> "OVERLAPS" + FieldOverlap -> "overlap" + DefaultOverlap -> mempty +#endif + +-------------------------------------------------------------------------------- + -- | From 'prettyHiding' -- @renderHiding info visible text@ puts the correct braces -- around @text@ according to info @info@ and returns diff --git a/src/Render/Concrete.hs b/src/Render/Concrete.hs index 7850e89..5aa5f7e 100644 --- a/src/Render/Concrete.hs +++ b/src/Render/Concrete.hs @@ -701,6 +701,11 @@ instance Render Pragma where 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] + render (OverlapPragma _ x m) = hsep [render m, render x] +#endif instance Render Fixity where render (Fixity _ Unrelated _) = __IMPOSSIBLE__ From 485e8b0c1c72c3d5a854a540f0a0012a5d06177a Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Mon, 2 Dec 2024 14:28:41 +0800 Subject: [PATCH 10/11] [ fix ] Make ALS compatible with Agda-2.7.0 --- src/Render/Common.hs | 4 ++++ src/Render/Interaction.hs | 3 +++ src/Render/RichText.hs | 6 ++++++ stack.yaml.lock | 8 ++++---- 4 files changed, 17 insertions(+), 4 deletions(-) diff --git a/src/Render/Common.hs b/src/Render/Common.hs index 759fa74..5e1579f 100644 --- a/src/Render/Common.hs +++ b/src/Render/Common.hs @@ -28,6 +28,7 @@ import Agda.Utils.Functor ((<&>)) import Render.Class import Render.RichText +import qualified Agda.Utils.List1 as List1 -------------------------------------------------------------------------------- @@ -131,6 +132,9 @@ instance (Render p, Render e) => Render (RewriteEqn' qn nm p e) where render = \case Rewrite es -> prefixedThings (text "rewrite") (render . snd <$> toList es) Invert _ pes -> prefixedThings (text "invert") (toList pes <&> (\ (p, e) -> render p <+> "<-" <+> render e) . namedThing) +#if MIN_VERSION_Agda(2,7,0) + LeftLet pes -> prefixedThings (text "using") [render p <+> "<-" <+> render e | (p, e) <- List1.toList pes] +#endif prefixedThings :: Inlines -> [Inlines] -> Inlines prefixedThings kw = \case diff --git a/src/Render/Interaction.hs b/src/Render/Interaction.hs index 420b6ea..e85dfa2 100644 --- a/src/Render/Interaction.hs +++ b/src/Render/Interaction.hs @@ -98,6 +98,9 @@ instance (Render a, Render b) => Render (OutputConstraint a b) where , "Candidate:" , vcat exprs' ] +#if MIN_VERSION_Agda(2,7,0) + render (ResolveInstanceOF q) = "Resolve output type of instance" render q +#endif render (PTSInstance name1 name2) = "PTS instance for (" <> render name1 <> ", " <> render name2 <> ")" render (PostponedCheckFunDef name expr _err) = diff --git a/src/Render/RichText.hs b/src/Render/RichText.hs index f63061f..f195f8c 100644 --- a/src/Render/RichText.hs +++ b/src/Render/RichText.hs @@ -16,6 +16,7 @@ module Render.RichText icon, -- combinators (<+>), + (), punctuate, braces, braces', @@ -132,6 +133,11 @@ x <+> y | null y = x | otherwise = x <> " " <> y +infixl 6 +-- | A synonym for '<+>' at the moment +() :: Inlines -> Inlines -> Inlines +() = (<+>) + -- | Whitespace space :: Inlines space = " " diff --git a/stack.yaml.lock b/stack.yaml.lock index 4e8b7e4..a23b31e 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -5,12 +5,12 @@ packages: - completed: - hackage: Agda-2.6.4.3@sha256:a8066d4b15827534d118846e98fd47bb9aadeb75e3d3b1f2c3bda8f5885c3f7c,29246 + hackage: Agda-2.7.0.1@sha256:37d363f323c1229f9ae16b4e0b2120d713b793a012847158fe6df736ec7736ec,30433 pantry-tree: - sha256: 8ec7c974decac30ceb45e9d728cf8b70b6da671dd80fe362e7e1fd4f0fcae77d - size: 42904 + sha256: c0324b33036f03017fd8b57188137d0ede9b8fbacc76876c67dd9b8b607873c7 + size: 43358 original: - hackage: Agda-2.6.4.3 + hackage: Agda-2.7.0.1 - completed: hackage: lsp-2.7.0.0@sha256:2a64b40a69fd9638056ca552d5660203019473061cff1d09dccc0c94e40a275c,3834 pantry-tree: From 0fd129ca306d646b35d17c20e2f0899492dbfd77 Mon Sep 17 00:00:00 2001 From: Ting-Gian LUA Date: Mon, 2 Dec 2024 14:44:32 +0800 Subject: [PATCH 11/11] [ new ] Release Agda v2.7.0.1 Language Server v0 --- package.yaml | 2 +- src/Options.hs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package.yaml b/package.yaml index 854273e..3ef3ac6 100644 --- a/package.yaml +++ b/package.yaml @@ -1,5 +1,5 @@ name: agda-language-server -version: 0.2.6.4.3.0 +version: 0.2.7.0.1.0 github: "banacorn/agda-language-server" license: MIT author: "Ting-Gian LUA" diff --git a/src/Options.hs b/src/Options.hs index 6d74773..83a0019 100644 --- a/src/Options.hs +++ b/src/Options.hs @@ -59,7 +59,7 @@ options = ] usage :: String -usage = "Agda Language Server v0.0.3.0 \nUsage: als [Options...]\n" +usage = "Agda v2.7.0.1 Language Server v0\nUsage: als [Options...]\n" usageAboutAgdaOptions :: String usageAboutAgdaOptions =