From 7dabff382f3a166f11cdd1bcbaabddd20e4d691b Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Tue, 22 Dec 2020 22:00:25 -0500
Subject: [PATCH] feat: prepare for Ipc server testing

---
 src/Lean/Data/Lsp.lean              |  1 +
 src/Lean/Data/Lsp/Capabilities.lean |  6 +++
 src/Lean/Data/Lsp/InitShutdown.lean | 17 ++++++-
 src/Lean/Data/Lsp/Ipc.lean          | 77 +++++++++++++++++++++++++++++
 src/Lean/Data/Lsp/TextSync.lean     | 14 ++++++
 5 files changed, 114 insertions(+), 1 deletion(-)
 create mode 100644 src/Lean/Data/Lsp/Ipc.lean

diff --git a/src/Lean/Data/Lsp.lean b/src/Lean/Data/Lsp.lean
index 3f98478d54..23128e8390 100644
--- a/src/Lean/Data/Lsp.lean
+++ b/src/Lean/Data/Lsp.lean
@@ -14,3 +14,4 @@ import Lean.Data.Lsp.InitShutdown
 import Lean.Data.Lsp.TextSync
 import Lean.Data.Lsp.Utf16
 import Lean.Data.Lsp.Workspace
+import Lean.Data.Lsp.Ipc
diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean
index a1758f3816..4ed734643b 100644
--- a/src/Lean/Data/Lsp/Capabilities.lean
+++ b/src/Lean/Data/Lsp/Capabilities.lean
@@ -31,6 +31,12 @@ structure ServerCapabilities where
   textDocumentSync? : Option TextDocumentSyncOptions := none
   hoverProvider : Bool := false
 
+instance : FromJson ServerCapabilities :=
+  ⟨fun j => do
+    let textDocumentSync? := j.getObjValAs? TextDocumentSyncOptions "textDocumentSync"
+    let hoverProvider ← j.getObjValAs? Bool "hoverProvider"
+    pure ⟨textDocumentSync?, hoverProvider⟩⟩
+
 instance : ToJson ServerCapabilities := ⟨fun o => mkObj $
   opt "textDocumentSync" o.textDocumentSync? ++
     [⟨"hoverProvider", o.hoverProvider⟩]⟩
diff --git a/src/Lean/Data/Lsp/InitShutdown.lean b/src/Lean/Data/Lsp/InitShutdown.lean
index 966807fdb6..2d9a1cf102 100644
--- a/src/Lean/Data/Lsp/InitShutdown.lean
+++ b/src/Lean/Data/Lsp/InitShutdown.lean
@@ -89,12 +89,21 @@ inductive InitializedParams where
   | mk
 
 instance : FromJson InitializedParams :=
-  ⟨fun j => InitializedParams.mk⟩
+  ⟨fun _ => InitializedParams.mk⟩
+
+instance : ToJson InitializedParams :=
+  ⟨fun _ => Json.null⟩
 
 structure ServerInfo where
   name : String
   version? : Option String := none
 
+instance : FromJson ServerInfo :=
+  ⟨fun j => do
+    let name ← j.getObjValAs? String "name"
+    let version? := j.getObjValAs? String "version"
+    pure ⟨name, version?⟩⟩
+
 instance : ToJson ServerInfo := ⟨fun o => mkObj $
   ⟨"name", o.name⟩ ::
   opt "version" o.version?⟩
@@ -103,6 +112,12 @@ structure InitializeResult where
   capabilities : ServerCapabilities
   serverInfo? : Option ServerInfo := none
 
+instance : FromJson InitializeResult :=
+  ⟨fun j => do
+    let capabilities ← j.getObjValAs? ServerCapabilities "capabilities"
+    let serverInfo? := j.getObjValAs? ServerInfo "serverInfo"
+    pure ⟨capabilities, serverInfo?⟩⟩
+
 instance : ToJson InitializeResult := ⟨fun o =>
   mkObj $
      ⟨"capabilities", toJson o.capabilities⟩ ::
diff --git a/src/Lean/Data/Lsp/Ipc.lean b/src/Lean/Data/Lsp/Ipc.lean
new file mode 100644
index 0000000000..49fb345008
--- /dev/null
+++ b/src/Lean/Data/Lsp/Ipc.lean
@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga, Wojciech Nawrocki
+-/
+import Init.System.IO
+import Lean.Data.Json
+import Lean.Data.Lsp.Communication
+import Lean.Data.Lsp.Diagnostics
+import Lean.Data.Lsp.Extra
+
+/-! Provides an IpcM monad for interacting with an external LSP process.
+Used for testing the Lean server. -/
+
+namespace Lean.Lsp.Ipc
+
+open IO
+open JsonRpc
+
+def ipcStdioConfig : Process.StdioConfig where
+  stdin  := Process.Stdio.piped
+  stdout := Process.Stdio.piped
+  stderr := Process.Stdio.piped
+
+abbrev IpcM := ReaderT (Process.Child ipcStdioConfig) IO
+
+variable [ToJson α]
+
+def stdin : IpcM FS.Stream := do
+  FS.Stream.ofHandle (←read).stdin
+
+def stdout : IpcM FS.Stream := do
+  FS.Stream.ofHandle (←read).stdout
+
+def stderr : IpcM FS.Stream := do
+  FS.Stream.ofHandle (←read).stderr
+
+def writeRequest (r : Request α) : IpcM Unit := do
+  (←stdin).writeLspRequest r
+
+def writeNotification (n : Notification α) : IpcM Unit := do
+  (←stdin).writeLspNotification n
+
+def readMessage : IpcM JsonRpc.Message := do
+  (←stdout).readLspMessage
+
+def readResponseAs (expectedID : RequestID) (α) [FromJson α] : IpcM (Response α) := do
+  (←stdout).readLspResponseAs expectedID α
+
+/-- Waits for the worker to emit all diagnostics for the current document version
+and returns them as a list. -/
+partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : DocumentUri)
+: IpcM (List (Notification PublishDiagnosticsParams)) := do
+  writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParam.mk target⟩
+  let rec loop : IpcM (List (Notification PublishDiagnosticsParams)) := do
+    match ←readMessage with
+    | Message.response id _ =>
+      if id = waitForDiagnosticsId then
+        []
+      else
+        loop
+    | Message.notification "textDocument/publishDiagnostics" (some param) =>
+      match fromJson? (toJson param) with
+      | some diagnosticParam => ⟨"textDocument/publishDiagnostics", diagnosticParam⟩ :: (←loop)
+      | none                 => throw $ userError "Cannot decode publishDiagnostics parameters"
+    | _ => loop
+  loop
+
+def runWith (cmd : String) (args : Array String := #[]) (test : IpcM α) : IO α := do
+  let proc ← Process.spawn {
+    toStdioConfig := ipcStdioConfig
+    cmd := cmd
+    args := args }
+  ReaderT.run test proc
+
+end Lean.Lsp.Ipc
\ No newline at end of file
diff --git a/src/Lean/Data/Lsp/TextSync.lean b/src/Lean/Data/Lsp/TextSync.lean
index 868ec12f6b..a952a2d1a7 100644
--- a/src/Lean/Data/Lsp/TextSync.lean
+++ b/src/Lean/Data/Lsp/TextSync.lean
@@ -85,6 +85,11 @@ instance DidChangeTextDocumentParams.hasToJson : ToJson DidChangeTextDocumentPar
 structure SaveOptions where
   includeText : Bool
 
+instance : FromJson SaveOptions :=
+  ⟨fun j => do
+    let includeText ← j.getObjValAs? Bool "includeText"
+    pure ⟨includeText⟩⟩
+
 instance : ToJson SaveOptions := ⟨fun o =>
   mkObj $ [⟨"includeText", o.includeText⟩]⟩
 
@@ -107,6 +112,15 @@ structure TextDocumentSyncOptions where
   willSaveWaitUntil : Bool
   save? : Option SaveOptions := none
 
+instance : FromJson TextDocumentSyncOptions :=
+  ⟨fun j => do
+    let openClose ← j.getObjValAs? Bool "openClose"
+    let change ← j.getObjValAs? TextDocumentSyncKind "change"
+    let willSave ← j.getObjValAs? Bool "willSave"
+    let willSaveUntil ← j.getObjValAs? Bool "willSaveWaitUntil"
+    let save? := j.getObjValAs? SaveOptions "save"
+    pure ⟨openClose, change, willSave, willSaveUntil, save?⟩⟩
+
 instance : ToJson TextDocumentSyncOptions := ⟨fun o =>
   mkObj $
     opt "save" o.save? ++ [