[ git ] Merge pull request #28 from agda/agda-2.7.0

Upgrade Agda to v2.7.0.1

Author: banacorn

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"

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

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"
@@ -67,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"
@@ -97,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)

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

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 =

src/Render/Class.hs

@@ -1,7 +1,6 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleInstances    #-}
 {-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE TypeSynonymInstances #-}
 
 module Render.Class
   ( Render (..),
@@ -78,6 +77,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

src/Render/Common.hs

@@ -16,13 +16,19 @@ import Agda.Syntax.Common
       Cohesion(..),
       QωOrigin(..),
       LensCohesion(getCohesion),
-      NameId(..) )
+      NameId(..),
+      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)
 import           Agda.Utils.Functor ((<&>))
 
 import Render.Class
 import Render.RichText
+import qualified Agda.Utils.List1 as List1
 
 --------------------------------------------------------------------------------
 
@@ -72,6 +78,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
@@ -91,6 +110,17 @@ 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
+#endif
+
 renderCohesion :: LensCohesion a => a -> Inlines -> Inlines
 renderCohesion a d =
   if show d == "_" then d else render (getCohesion a) <+> d
@@ -102,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

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,9 +28,16 @@ import Render.Literal ()
 import Render.Name ()
 import Render.RichText
 import Render.TypeChecking ()
+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
 
@@ -172,6 +180,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 +222,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
+
+
 
 --------------------------------------------------------------------------------
 
@@ -266,6 +303,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
@@ -279,6 +327,7 @@ instance Render WhereClause where
             ["module", render m, "where"],
         vcat $ fmap render ds
       ]
+#endif
 
 instance Render LHS where
   render (LHS p eqs es) =
@@ -343,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",
@@ -418,15 +469,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 ->
+      Record _ x dir tel e cs -> pRecord x dir tel (Just e) cs
 #endif
-        pRecord x dir tel (Just e) cs
-      RecordDef _ x dir tel cs ->
-        pRecord x dir tel Nothing cs
+#endif
+#if MIN_VERSION_Agda(2,7,0)
+      RecordDef _ x dir tel cs -> pRecord defaultErased x dir tel Nothing cs
+#else
+      RecordDef _ x dir tel cs -> pRecord x dir tel Nothing cs
+#endif
+#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 ->
@@ -511,6 +572,9 @@ pHasEta0 = \case
   YesEta   -> "eta-equality"
   NoEta () -> "no-eta-equality"
 
+instance Render RecordDirective where
+  render = pRecordDirective
+
 pRecordDirective ::
   RecordDirective ->
   Inlines
@@ -523,7 +587,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 +654,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"
@@ -607,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__