From d2e23ff5cf0955e2c54470410cfb78fe3e730ff8 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <t-wnawrocki@microsoft.com>
Date: Mon, 26 Jul 2021 00:10:24 -0700
Subject: [PATCH] fix: deriving RpcEncoding

---
 src/Lean/Server/Rpc/Basic.lean                |  3 +++
 src/Lean/Server/Rpc/Deriving.lean             | 23 +++++++++----------
 ...Encoding.lean => derivingRpcEncoding.lean} | 10 ++++----
 3 files changed, 19 insertions(+), 17 deletions(-)
 rename tests/lean/run/{derivingLspEncoding.lean => derivingRpcEncoding.lean} (65%)

diff --git a/src/Lean/Server/Rpc/Basic.lean b/src/Lean/Server/Rpc/Basic.lean
index bb65afa48e..9254288f16 100644
--- a/src/Lean/Server/Rpc/Basic.lean
+++ b/src/Lean/Server/Rpc/Basic.lean
@@ -76,6 +76,9 @@ instance [RpcEncoding α α'] [RpcEncoding β β']  : RpcEncoding (α × β) (α
     let b ← rpcDecode b'
     return (a, b)
 
+structure RpcEncoding.DerivingParams where
+  withRef : Bool := false
+
 /-- Marks fields to encode as opaque references in LSP packets. -/
 structure WithRpcRef (α : Type u) where
   val : α
diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean
index cfe30bada0..dc9674db6e 100644
--- a/src/Lean/Server/Rpc/Deriving.lean
+++ b/src/Lean/Server/Rpc/Deriving.lean
@@ -13,9 +13,6 @@ import Lean.Server.Rpc.Basic
 
 namespace Lean.Server.RpcEncoding
 
-structure DerivingParams where
-  withRef : Bool := false
-
 open Meta Elab Command Term
 
 private def deriveWithRefInstance (typeNm : Name) : CommandElabM Bool := do
@@ -24,22 +21,24 @@ private def deriveWithRefInstance (typeNm : Name) : CommandElabM Bool := do
   let typeId := mkIdent typeNm
   let cmds ← `(
     namespace $typeId:ident
-    variable {m : Type → Type} [Monad m] [MonadRpcSession m]
-    private unsafe def encodeUnsafe (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef :=
+    variable {m : Type → Type}
+    private unsafe def encodeUnsafe [Monad m] [MonadRpcSession m] (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef :=
       WithRpcRef.encodeUnsafe $(quote typeNm) r
 
     @[implementedBy encodeUnsafe]
-    private constant encode (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef
+    private constant encode [Monad m] [MonadRpcSession m] (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef :=
+      pure ⟨0⟩
 
-    private unsafe def decodeUnsafe (r : Lsp.RpcRef) : m (WithRpcRef $typeId:ident) :=
+    private unsafe def decodeUnsafe [Monad m] [MonadRpcSession m] (r : Lsp.RpcRef) : ExceptT String m (WithRpcRef $typeId:ident) :=
       WithRpcRef.decodeUnsafeAs $typeId:ident $(quote typeNm) r
 
     @[implementedBy decodeUnsafe]
-    private constant decode (r : Lsp.RpcRef) : m (WithRpcRef $typeId:ident)
+    private constant decode [Monad m] [MonadRpcSession m] (r : Lsp.RpcRef) : ExceptT String m (WithRpcRef $typeId:ident) :=
+      throw "unreachable"
 
     instance : RpcEncoding (WithRpcRef $typeId:ident) Lsp.RpcRef where
-      lspEncode a := encode a
-      lspDecode a := decode a
+      rpcEncode a := encode a
+      rpcDecode a := decode a
     end $typeId:ident
   )
   elabCommand cmds
@@ -101,11 +100,11 @@ private def deriveInstance (typeName : Name) : CommandElabM Bool := do
           deriving $(mkIdent ``Lean.FromJson), $(mkIdent ``Lean.ToJson)
 
         instance : RpcEncoding $typeId:ident RpcEncodingPacket where
-          lspEncode a := do
+          rpcEncode a := do
             return {
               $[$encFields]*
             }
-          lspDecode a := do
+          rpcDecode a := do
             return {
               $[$decFields]*
             }
diff --git a/tests/lean/run/derivingLspEncoding.lean b/tests/lean/run/derivingRpcEncoding.lean
similarity index 65%
rename from tests/lean/run/derivingLspEncoding.lean
rename to tests/lean/run/derivingRpcEncoding.lean
index 5386e9a973..87171eca6e 100644
--- a/tests/lean/run/derivingLspEncoding.lean
+++ b/tests/lean/run/derivingRpcEncoding.lean
@@ -1,10 +1,10 @@
-import Lean.Server.FileWorker.LspEncoding
+import Lean.Server.Rpc.Basic
 
 open Lean Server
 
 structure FooRef where
   a : Array Nat
-  deriving LspEncoding with { withRef := true }
+  deriving RpcEncoding with { withRef := true }
 
 structure FooJson where
   s : String
@@ -13,12 +13,12 @@ structure FooJson where
 structure Bar where
   fooRef : WithRpcRef FooRef
   fooJson : FooJson
-  deriving LspEncoding
+  deriving RpcEncoding
 
 structure BarTrans where
   bar : Bar
-  deriving LspEncoding
+  deriving RpcEncoding
 
 structure Baz where
   arr : Array String -- non-constant field
-  deriving LspEncoding
+  deriving RpcEncoding