max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: use field names if specified

Browse source
This commit is contained in:
Gabriel Ebner 2022-07-18 11:38:54 +02:00 • committed by Sebastian Ullrich
parent 59f528e678
commit 4ce56f7c05
2 changed files with 12 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Server/Rpc/Deriving.lean
View file

@ -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

11
tests/lean/derivingRpcEncoding.lean.expected.out
View file

@ -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