[ fix ] Make ALS compatible with Agda-2.7.0

agda · Dec 2, 2024 · 485e8b0 · 485e8b0
1 parent 26def0e
commit 485e8b0
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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: