From 4ce56f7c05ea7cf484fad782dc8894f7dda6d1e5 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 18 Jul 2022 11:38:54 +0200
Subject: [PATCH] fix: use field names if specified

---
 src/Lean/Server/Rpc/Deriving.lean                | 15 ++++++---------
 tests/lean/derivingRpcEncoding.lean.expected.out | 11 ++++++-----
 2 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean
index 8574f32bb4..c0333cdea1 100644
--- a/src/Lean/Server/Rpc/Deriving.lean
+++ b/src/Lean/Server/Rpc/Deriving.lean
@@ -144,16 +144,13 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
   let recInstTp := mkApp2 (mkConst ``RpcEncoding) (mkAppN (mkConst indVal.name) params) pktCtorTp
   withLocalDecl `inst .instImplicit recInstTp fun _ => do
   let st ← foldWithConstructors indVal params (init := { : CtorState }) fun acc ctor argVars _ => do
-    let mut pktCtorTp := pktCtorTp
     -- create the constructor
-    for arg in argVars.reverse do
-      let argTp ← inferType arg
-      let encTp ← getRpcPacketFor argTp
-      pktCtorTp := mkForall (← getFVarLocalDecl arg).userName BinderInfo.default encTp pktCtorTp
-    -- TODO(WN): this relies on delab printing non-macro-scoped user names in non-dependent foralls
-    -- to generate the expected JSON encoding
-    let pktCtorTpStx ← PrettyPrinter.delab pktCtorTp
-    let pktCtor ← `(Lean.Parser.Command.ctor| | $(mkIdent ctor.getString!):ident : $pktCtorTpStx:term)
+    let fieldStxs ← argVars.mapM fun arg => do
+      let packetTp ← getRpcPacketFor (← inferType arg)
+      let tyStx ← PrettyPrinter.delab packetTp
+      let name := (← getFVarLocalDecl arg).userName
+      `(bracketedBinder| ($(mkIdent name) : $tyStx))
+    let pktCtor ← `(Parser.Command.ctor| | $(mkIdent ctor.getString!):ident $[$fieldStxs]* : $(mkIdent packetNm))
 
     -- create encoder and decoder match arms
     let nms ← argVars.mapM fun _ => mkIdent <$> mkFreshBinderName
diff --git a/tests/lean/derivingRpcEncoding.lean.expected.out b/tests/lean/derivingRpcEncoding.lean.expected.out
index 197745270a..f22d0a4a1a 100644
--- a/tests/lean/derivingRpcEncoding.lean.expected.out
+++ b/tests/lean/derivingRpcEncoding.lean.expected.out
@@ -20,8 +20,9 @@ ok: {"a": 0}
 ok: {"b": 42, "a": 3}
 instRpcEncodingBazInductive : RpcEncoding BazInductive BazInductive.RpcEncodingPacket
 ok: {"baz":
- [{"fooRef": {"p": "0"}, "fooJson": {"s": ""}},
-  {"fooRef": {"p": "1"}, "fooJson": {"s": ""}}]}
+ {"arr":
+  [{"fooRef": {"p": "0"}, "fooJson": {"s": ""}},
+   {"fooRef": {"p": "1"}, "fooJson": {"s": ""}}]}}
 protected inductive FooInductive.RpcEncodingPacket : Type → Type
 number of parameters: 1
 constructors:
@@ -29,8 +30,8 @@ FooInductive.RpcEncodingPacket.a : {αPacket : Type} → αPacket → Lsp.RpcRef
 FooInductive.RpcEncodingPacket.b : {αPacket : Type} → Nat → αPacket → Nat → FooInductive.RpcEncodingPacket αPacket
 instRpcEncodingFooInductive : (α αPacket : Type) →
   [inst : RpcEncoding α αPacket] → RpcEncoding (FooInductive α) (FooInductive.RpcEncodingPacket αPacket)
-ok: {"a": [{"baz": []}, {"p": "0"}]}
-ok: {"b": [42, {"baz": []}, 0]}
+ok: {"a": [{"baz": {"arr": []}}, {"p": "0"}]}
+ok: {"b": {"n": 42, "m": 0, "a": {"baz": {"arr": []}}}}
 protected inductive FooNested.RpcEncodingPacket : Type → Type
 number of parameters: 1
 constructors:
@@ -38,7 +39,7 @@ FooNested.RpcEncodingPacket.a : {αPacket : Type} →
   αPacket → Array (FooNested.RpcEncodingPacket αPacket) → FooNested.RpcEncodingPacket αPacket
 @FooNested.RpcEncodingPacket.a : {αPacket : Type} →
   αPacket → Array (FooNested.RpcEncodingPacket αPacket) → FooNested.RpcEncodingPacket αPacket
-ok: {"a": [{"baz": []}, [{"a": [{"baz": []}, []]}]]}
+ok: {"a": [{"baz": {"arr": []}}, [{"a": [{"baz": {"arr": []}}, []]}]]}
 instRpcEncodingFooParam : (n : Nat) → RpcEncoding (FooParam n) FooParam.RpcEncodingPacket
 ok: {"a": 42}
 protected inductive Unused.RpcEncodingPacket : Type