[ new ] LSP testing for agda-mode:load

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

@@ -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 )
@@ -251,6 +253,7 @@ data CommandReq
   | CmdReq String
   deriving (Generic)
 
+instance ToJSON CommandReq
 instance FromJSON CommandReq
 
 data CommandRes

stack.yaml

@@ -10,6 +10,7 @@ extra-deps:
 - Agda-2.7.0.1
 - lsp-2.7.0.0@sha256:2a64b40a69fd9638056ca552d5660203019473061cff1d09dccc0c94e40a275c,3834
 - lsp-types-2.3.0.0@sha256:ca17a686bda5dc7ff04105ca7081dce5a90bcd050c8800a13efd68b7f0901f1c,34215
+- lsp-test-0.17.1.0@sha256:f54757a564b46783cf67b13f4cb4ebc45e43f5afc3604d9757ee387c091b73e9,4406
 - mod-0.2.0.1@sha256:eeb316fef3a8c12f4e83bbeeea748e74d75fca54d4498d574ace92e464adb05a,2409
 - row-types-1.0.1.2@sha256:4d4c7cb95d06a32b28ba977852d52a26b4c1f695ef083a6fd874ab6d79933b64,3071
 

stack.yaml.lock

@@ -25,6 +25,13 @@ packages:
       size: 51996
   original:
     hackage: lsp-types-2.3.0.0@sha256:ca17a686bda5dc7ff04105ca7081dce5a90bcd050c8800a13efd68b7f0901f1c,34215
+- completed:
+    hackage: lsp-test-0.17.1.0@sha256:f54757a564b46783cf67b13f4cb4ebc45e43f5afc3604d9757ee387c091b73e9,4406
+    pantry-tree:
+      sha256: 66797a8efd50812189c410310dc0a9b72858ea3a3e78764e9cedd8f406df2564
+      size: 1561
+  original:
+    hackage: lsp-test-0.17.1.0@sha256:f54757a564b46783cf67b13f4cb4ebc45e43f5afc3604d9757ee387c091b73e9,4406
 - completed:
     hackage: mod-0.2.0.1@sha256:eeb316fef3a8c12f4e83bbeeea748e74d75fca54d4498d574ace92e464adb05a,2409
     pantry-tree:

test/Test.hs

@@ -1,4 +1,7 @@
+module Test where
+
 import qualified Test.SrcLoc                   as SrcLoc
+import qualified Test.LSP                   as LSP
 import           Test.Tasty                     ( TestTree
                                                 , defaultMain
                                                 , testGroup
@@ -8,4 +11,7 @@ main :: IO ()
 main = defaultMain tests
 
 tests :: TestTree
-tests = testGroup "Tests" [SrcLoc.tests]
+tests = testGroup "Tests" 
+    [SrcLoc.tests,
+        LSP.tests
+    ]

test/Test/LSP.hs

@@ -0,0 +1,39 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Test.LSP (tests) where
+
+import Control.Applicative.Combinators
+import Control.Monad.IO.Class
+import Language.LSP.Protocol.Message
+import Language.LSP.Protocol.Types
+import Language.LSP.Test
+import Test.Tasty
+import Test.Tasty.HUnit
+import qualified Data.Aeson                    as JSON
+import Switchboard ( agdaCustomMethod )
+import Agda
+
+tests :: TestTree
+tests = 
+  testGroup
+    "LSP"
+    [ testCase "load" demo
+    ]
+
+demo :: IO ()
+demo = runSession "als" fullLatestClientCaps "test/data/" $ do
+  doc <- openDoc "A.agda" "agda"
+
+  -- Use your favourite favourite combinators.
+  -- skipManyTill loggingNotification (count 1 publishDiagnosticsNotification)
+
+  testCustomMethod "IOTCM \"test/data/A.agdaa\" NonInteractive Direct( Cmd_load \"test/data/A.agda\" [] )"
+
+  -- Or use one of the helper functions
+  -- getDocumentSymbols doc >>= liftIO . print
+
+-- | Sends a custom method request to the server and expects a response of `CmdRes Nothing`
+testCustomMethod :: String -> Session ()
+testCustomMethod cmd = do 
+  TResponseMessage _ _ rsp <- request agdaCustomMethod $ 
+    JSON.toJSON $ CmdReq cmd
+  liftIO $ rsp @?= Right (JSON.toJSON (CmdRes Nothing))

test/data/A.agda

@@ -0,0 +1,4 @@
+module A where
+
+data ⊤ : Set where
+    tt : ⊤