[ git ] Merge branch 'test' into ci

Author: banacorn

agda-language-server.cabal

@@ -5,7 +5,7 @@ cabal-version: 1.12
 -- see: https://github.com/sol/hpack
 
 name:           agda-language-server
-version:        0.2.6.4.3.0
+version:        0.2.7.0.1.0
 synopsis:       An implementation of language server protocal (LSP) for Agda 2.
 description:    Please see the README on GitHub at <https://github.com/agda/agda-language-server#readme>
 category:       Development
@@ -171,6 +171,7 @@ test-suite als-test
   type: exitcode-stdio-1.0
   main-is: Test.hs
   other-modules:
+      Test.LSP
       Test.SrcLoc
       Agda
       Agda.Convert
@@ -216,6 +217,7 @@ test-suite als-test
     , directory
     , filepath
     , lsp >=2
+    , lsp-test
     , lsp-types >=2
     , mtl
     , network

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"
@@ -130,6 +130,7 @@ tests:
       - test
       - src
     dependencies:
+      - lsp-test
       - tasty
       - tasty-hunit
       - tasty-golden

src/Agda.hs

@@ -8,6 +8,8 @@ module Agda
   , runAgda
   , sendCommand
   , getCommandLineOptions
+  , CommandReq(..)
+  , CommandRes(..)
   ) where
 
 import           Prelude                        hiding ( null )
@@ -17,7 +19,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 +37,10 @@ import           Agda.Interaction.InteractionTop
                                                 ( initialiseCommandQueue
                                                 , maybeAbort
                                                 , runInteraction
+#if MIN_VERSION_Agda(2,7,0)
+                                                , CommandM
+#else
+#endif
                                                 )
 import           Agda.Interaction.Options       ( CommandLineOptions
                                                   ( optAbsoluteIncludePaths
@@ -244,6 +253,7 @@ data CommandReq
   | CmdReq String
   deriving (Generic)
 
+instance ToJSON CommandReq
 instance FromJSON CommandReq
 
 data CommandRes

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