From bea68819c9f877caebc677be31eaba71e08d7f49 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Thu, 12 May 2022 14:19:12 -0400
Subject: [PATCH] feat: support optional RPC fields

---
 src/Lean/Server/Rpc/Deriving.lean       | 20 +++++++++++++++++---
 tests/lean/run/derivingRpcEncoding.lean | 22 ++++++++++++++++++++++
 2 files changed, 39 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean
index 1df65d9294..edc87ccb88 100644
--- a/src/Lean/Server/Rpc/Deriving.lean
+++ b/src/Lean/Server/Rpc/Deriving.lean
@@ -85,6 +85,9 @@ def withFieldsFlattened (indVal : InductiveVal) (params : Array Expr)
 
 end
 
+def isOptField (n : Name) : Bool :=
+  n.toString.endsWith "?"
+
 private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr) : TermElabM Syntax :=
   withFields indVal params fun fields => do
     trace[Elab.Deriving.RpcEncoding] "for structure {indVal.name} with params {params}"
@@ -97,20 +100,30 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
     let mut uniqFieldEncIds : Array Syntax := #[]
     let mut fieldEncIds' : DiscrTree Syntax := {}
     for (fieldName, fieldTp) in fields do
+      let mut fieldTp := fieldTp
+      if isOptField fieldName then
+        if !fieldTp.isAppOf ``Option then
+          throwError "optional field '{fieldName}' has type{indentD m!"{fieldTp}"}\nbut is expected to have type{indentD "Option _"}"
+        fieldTp := fieldTp.getArg! 0
+
       -- postulate that the field has an encoding and remember the encoding's binder name
       fieldIds := fieldIds.push <| mkIdent fieldName
+      let mut fieldEncId := Syntax.missing
       match (← fieldEncIds'.getMatch fieldTp).back? with
       | none =>
-        let fieldEncId ← mkIdent <$> mkFreshUserName fieldName
+        fieldEncId ← mkIdent <$> mkFreshUserName fieldName
         binders := binders.push <| ← `(Deriving.explicitBinderF| ( $fieldEncId:ident ))
         let stx ← PrettyPrinter.delab fieldTp
         binders := binders.push <|
           ← `(Deriving.instBinderF| [ $(mkIdent ``Lean.Server.RpcEncoding) $stx $fieldEncId:ident ])
         fieldEncIds' ← fieldEncIds'.insert fieldTp fieldEncId
         uniqFieldEncIds := uniqFieldEncIds.push fieldEncId
+      | some fid => fieldEncId := fid
+
+      if isOptField fieldName then
+        fieldEncIds := fieldEncIds.push <| ← ``(Option $fieldEncId:ident)
+      else
         fieldEncIds := fieldEncIds.push fieldEncId
-      | some fid =>
-        fieldEncIds := fieldEncIds.push fid
 
     -- helpers for field initialization syntax
     let fieldInits (func : Name) := fieldIds.mapM fun fid =>
@@ -222,6 +235,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
 
         inductive $(mkIdent packetNm) where
           $[$(st.ctors):ctor]*
+          deriving $(mkIdent ``FromJson), $(mkIdent ``ToJson)
 
         instance : $(mkIdent ``RpcEncoding) $typeId:ident $packetAppliedId:ident where
           rpcEncode := fun x => match x with
diff --git a/tests/lean/run/derivingRpcEncoding.lean b/tests/lean/run/derivingRpcEncoding.lean
index 6b0cf56b49..7708b1347f 100644
--- a/tests/lean/run/derivingRpcEncoding.lean
+++ b/tests/lean/run/derivingRpcEncoding.lean
@@ -2,10 +2,16 @@ import Lean.Server.Rpc.Basic
 
 open Lean Server
 
+@[reducible]
+def rpcPacketFor (α : Type) {β : outParam Type} [RpcEncoding α β] := β
+
 structure FooRef where
   a : Array Nat
   deriving RpcEncoding with { withRef := true }
 
+#synth FromJson (rpcPacketFor (WithRpcRef FooRef))
+#synth ToJson (rpcPacketFor (WithRpcRef FooRef))
+
 structure FooJson where
   s : String
   deriving FromJson, ToJson
@@ -15,19 +21,35 @@ structure Bar where
   fooJson : FooJson
   deriving RpcEncoding
 
+#synth FromJson (rpcPacketFor Bar)
+#synth ToJson (rpcPacketFor Bar)
+
 structure BarTrans where
   bar : Bar
   deriving RpcEncoding
 
+#synth FromJson (rpcPacketFor BarTrans)
+#synth ToJson (rpcPacketFor BarTrans)
+
 structure Baz where
   arr : Array String -- non-constant field
   deriving RpcEncoding
 
+#synth FromJson (rpcPacketFor Baz)
+#synth ToJson (rpcPacketFor Baz)
+
 structure FooGeneric (α : Type) where
   a : α
+  b? : Option α
   deriving RpcEncoding
 
+#synth FromJson (rpcPacketFor <| FooGeneric Nat)
+#synth ToJson (rpcPacketFor <| FooGeneric Nat)
+
 inductive FooInductive (α : Type) where
   | a : α → Bar → FooInductive α
   | b : (n : Nat) → (a : α) → Nat → FooInductive α
   deriving RpcEncoding
+
+#synth FromJson (rpcPacketFor <| FooInductive Nat)
+#synth ToJson (rpcPacketFor <| FooInductive Nat)