chore: use inaccessible name for RpcEncodingPacket
This commit is contained in:
Gabriel Ebner
Sebastian Ullrich
parent
4ce56f7c05
commit
f2e7cbfbaf
3 changed files with 19 additions and 57 deletions
|
|
@ -104,17 +104,15 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
|
|||
-- helpers for type name syntax
|
||||
let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
|
||||
let typeId := Syntax.mkApp (← `(@$(mkIdent indVal.name))) paramIds
|
||||
let packetId := mkIdent <| indVal.name ++ `RpcEncodingPacket
|
||||
let packetAppliedId ← `($packetId ..)
|
||||
let instId := mkIdent (`_root_ ++ indVal.name.appendBefore "instRpcEncoding")
|
||||
|
||||
`(variable $packetParamBinders* in
|
||||
protected structure $packetId:ident where
|
||||
structure RpcEncodingPacket where
|
||||
$[($fieldIds : $fieldEncTypeStxs)]*
|
||||
deriving FromJson, ToJson
|
||||
|
||||
variable $(paramBinders ++ packetParamBinders ++ encInstBinders)* in
|
||||
@[instance] def $instId := show RpcEncoding $typeId $packetAppliedId from {
|
||||
@[instance] def $instId := show RpcEncoding $typeId (RpcEncodingPacket ..) from {
|
||||
rpcEncode := fun a => return { $[$encInits],* }
|
||||
rpcDecode := fun a => return { $[$decInits],* }
|
||||
}
|
||||
|
|
@ -133,7 +131,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
|
|||
(paramBinders packetParamBinders encInstBinders : Array (TSyntax ``Parser.Term.bracketedBinder)) : TermElabM Command := do
|
||||
trace[Elab.Deriving.RpcEncoding] "for inductive {indVal.name} with params {params}"
|
||||
withoutModifyingEnv do
|
||||
let packetNm := indVal.name ++ `RpcEncodingPacket
|
||||
let packetNm := (← `(RpcEncodingPacket)).1.getId
|
||||
addDecl <| .axiomDecl {
|
||||
name := packetNm
|
||||
levelParams := []
|
||||
|
|
@ -150,7 +148,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
|
|||
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))
|
||||
let pktCtor ← `(Parser.Command.ctor| | $(mkIdent ctor.getString!):ident $[$fieldStxs]* : RpcEncodingPacket)
|
||||
|
||||
-- create encoder and decoder match arms
|
||||
let nms ← argVars.mapM fun _ => mkIdent <$> mkFreshBinderName
|
||||
|
|
@ -170,23 +168,22 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
|
|||
-- helpers for type name syntax
|
||||
let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
|
||||
let typeId := Syntax.mkApp (← `(@$(mkIdent indVal.name))) paramIds
|
||||
let packetId ← `($(mkIdent packetNm) ..)
|
||||
let instId := mkIdent (`_root_ ++ indVal.name.appendBefore "instRpcEncoding")
|
||||
|
||||
`(variable $packetParamBinders:bracketedBinder* in
|
||||
protected inductive $(mkIdent packetNm) where
|
||||
inductive RpcEncodingPacket where
|
||||
$[$(st.ctors):ctor]*
|
||||
deriving FromJson, ToJson
|
||||
|
||||
variable $(paramBinders ++ packetParamBinders ++ encInstBinders)* in
|
||||
@[instance] partial def $instId := show RpcEncoding $typeId $packetId from
|
||||
@[instance] partial def $instId := show RpcEncoding $typeId (RpcEncodingPacket ..) from
|
||||
{ rpcEncode, rpcDecode }
|
||||
where
|
||||
rpcEncode {m} [Monad m] [MonadRpcSession m] (x : $typeId) : ExceptT String m $packetId :=
|
||||
have inst : RpcEncoding $typeId $packetId := { rpcEncode, rpcDecode }
|
||||
rpcEncode {m} [Monad m] [MonadRpcSession m] (x : $typeId) : ExceptT String m (RpcEncodingPacket ..) :=
|
||||
have inst : RpcEncoding $typeId (RpcEncodingPacket ..) := { rpcEncode, rpcDecode }
|
||||
match x with $[$(st.encodes):matchAlt]*
|
||||
rpcDecode {m} [Monad m] [MonadRpcSession m] (x : $packetId) : ExceptT String m $typeId :=
|
||||
have inst : RpcEncoding $typeId $packetId := { rpcEncode, rpcDecode }
|
||||
rpcDecode {m} [Monad m] [MonadRpcSession m] (x : RpcEncodingPacket ..) : ExceptT String m $typeId :=
|
||||
have inst : RpcEncoding $typeId (RpcEncodingPacket ..) := { rpcEncode, rpcDecode }
|
||||
match x with $[$(st.decodes):matchAlt]*
|
||||
)
|
||||
|
||||
|
|
|
|||
|
|
@ -37,7 +37,6 @@ structure Bar where
|
|||
fooJson : FooJson
|
||||
deriving RpcEncoding, Inhabited
|
||||
|
||||
#print Bar.RpcEncodingPacket
|
||||
#check instRpcEncodingBar
|
||||
#eval test Bar default
|
||||
|
||||
|
|
@ -60,7 +59,6 @@ structure FooGeneric (α : Type) where
|
|||
b? : Option α
|
||||
deriving RpcEncoding, Inhabited
|
||||
|
||||
#print FooGeneric.RpcEncodingPacket
|
||||
#check instRpcEncodingFooGeneric
|
||||
#eval test (FooGeneric Nat) default
|
||||
#eval test (FooGeneric Nat) { a := 3, b? := some 42 }
|
||||
|
|
@ -77,7 +75,6 @@ inductive FooInductive (α : Type) where
|
|||
| b : (n : Nat) → (a : α) → (m : Nat) → FooInductive α
|
||||
deriving RpcEncoding, Inhabited
|
||||
|
||||
#print FooInductive.RpcEncodingPacket
|
||||
#check instRpcEncodingFooInductive
|
||||
#eval test (FooInductive BazInductive) (.a default default)
|
||||
#eval test (FooInductive BazInductive) (.b 42 default default)
|
||||
|
|
@ -86,8 +83,6 @@ inductive FooNested (α : Type) where
|
|||
| a : α → Array (FooNested α) → FooNested α
|
||||
deriving RpcEncoding, Inhabited
|
||||
|
||||
#print FooNested.RpcEncodingPacket
|
||||
#check @FooNested.RpcEncodingPacket.a
|
||||
#eval test (FooNested BazInductive) (.a default #[default])
|
||||
|
||||
inductive FooParam (n : Nat) where
|
||||
|
|
@ -100,7 +95,6 @@ inductive FooParam (n : Nat) where
|
|||
inductive Unused (α : Type) | a
|
||||
deriving RpcEncoding, Inhabited
|
||||
|
||||
#print Unused.RpcEncodingPacket
|
||||
#check instRpcEncodingUnused
|
||||
structure NoRpcEncoding
|
||||
#eval test (Unused NoRpcEncoding) default
|
||||
|
|
@ -108,7 +102,6 @@ structure NoRpcEncoding
|
|||
structure UnusedStruct (α : Type)
|
||||
deriving RpcEncoding, Inhabited
|
||||
|
||||
#print UnusedStruct.RpcEncodingPacket
|
||||
#check instRpcEncodingUnusedStruct
|
||||
#eval test (UnusedStruct NoRpcEncoding) default
|
||||
|
||||
|
|
|
|||
|
|
@ -1,57 +1,29 @@
|
|||
instRpcEncodingWithRpcRefFooRefRpcRef : RpcEncoding (WithRpcRef FooRef) Lsp.RpcRef
|
||||
ok: {"p": "0"}
|
||||
protected inductive Bar.RpcEncodingPacket : Type
|
||||
number of parameters: 0
|
||||
constructors:
|
||||
Bar.RpcEncodingPacket.mk : Lsp.RpcRef → FooJson → Bar.RpcEncodingPacket
|
||||
instRpcEncodingBar : RpcEncoding Bar Bar.RpcEncodingPacket
|
||||
instRpcEncodingBar : RpcEncoding Bar RpcEncodingPacket✝
|
||||
ok: {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}
|
||||
instRpcEncodingBarTrans : RpcEncoding BarTrans BarTrans.RpcEncodingPacket
|
||||
instRpcEncodingBarTrans : RpcEncoding BarTrans RpcEncodingPacket✝
|
||||
ok: {"bar": {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}}
|
||||
instRpcEncodingBaz : RpcEncoding Baz Baz.RpcEncodingPacket
|
||||
instRpcEncodingBaz : RpcEncoding Baz RpcEncodingPacket✝
|
||||
ok: {"arr": []}
|
||||
protected inductive FooGeneric.RpcEncodingPacket : Type → Type
|
||||
number of parameters: 1
|
||||
constructors:
|
||||
FooGeneric.RpcEncodingPacket.mk : {αPacket : Type} → αPacket → Option αPacket → FooGeneric.RpcEncodingPacket αPacket
|
||||
instRpcEncodingFooGeneric : (α αPacket : Type) →
|
||||
[inst : RpcEncoding α αPacket] → RpcEncoding (FooGeneric α) (FooGeneric.RpcEncodingPacket αPacket)
|
||||
[inst : RpcEncoding α αPacket] → RpcEncoding (FooGeneric α) (RpcEncodingPacket✝ αPacket)
|
||||
ok: {"a": 0}
|
||||
ok: {"b": 42, "a": 3}
|
||||
instRpcEncodingBazInductive : RpcEncoding BazInductive BazInductive.RpcEncodingPacket
|
||||
instRpcEncodingBazInductive : RpcEncoding BazInductive RpcEncodingPacket✝
|
||||
ok: {"baz":
|
||||
{"arr":
|
||||
[{"fooRef": {"p": "0"}, "fooJson": {"s": ""}},
|
||||
{"fooRef": {"p": "1"}, "fooJson": {"s": ""}}]}}
|
||||
protected inductive FooInductive.RpcEncodingPacket : Type → Type
|
||||
number of parameters: 1
|
||||
constructors:
|
||||
FooInductive.RpcEncodingPacket.a : {αPacket : Type} → αPacket → Lsp.RpcRef → FooInductive.RpcEncodingPacket αPacket
|
||||
FooInductive.RpcEncodingPacket.b : {αPacket : Type} → Nat → αPacket → Nat → FooInductive.RpcEncodingPacket αPacket
|
||||
instRpcEncodingFooInductive : (α αPacket : Type) →
|
||||
[inst : RpcEncoding α αPacket] → RpcEncoding (FooInductive α) (FooInductive.RpcEncodingPacket αPacket)
|
||||
[inst : RpcEncoding α αPacket] → RpcEncoding (FooInductive α) (RpcEncodingPacket✝ αPacket)
|
||||
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:
|
||||
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": {"arr": []}}, [{"a": [{"baz": {"arr": []}}, []]}]]}
|
||||
instRpcEncodingFooParam : (n : Nat) → RpcEncoding (FooParam n) FooParam.RpcEncodingPacket
|
||||
instRpcEncodingFooParam : (n : Nat) → RpcEncoding (FooParam n) RpcEncodingPacket✝
|
||||
ok: {"a": 42}
|
||||
protected inductive Unused.RpcEncodingPacket : Type
|
||||
number of parameters: 0
|
||||
constructors:
|
||||
Unused.RpcEncodingPacket.a : Unused.RpcEncodingPacket
|
||||
instRpcEncodingUnused : (α : Type) → RpcEncoding (Unused α) Unused.RpcEncodingPacket
|
||||
instRpcEncodingUnused : (α : Type) → RpcEncoding (Unused α) RpcEncodingPacket✝
|
||||
ok: "a"
|
||||
protected inductive UnusedStruct.RpcEncodingPacket : Type
|
||||
number of parameters: 0
|
||||
constructors:
|
||||
UnusedStruct.RpcEncodingPacket.mk : UnusedStruct.RpcEncodingPacket
|
||||
instRpcEncodingUnusedStruct : (α : Type) → RpcEncoding (UnusedStruct α) UnusedStruct.RpcEncodingPacket
|
||||
instRpcEncodingUnusedStruct : (α : Type) → RpcEncoding (UnusedStruct α) RpcEncodingPacket✝
|
||||
ok: {}
|
||||
Except.error "no inductive constructor matched"
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue