From 92da08078a5459ca1089743eb58385e752bdb5fa Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Mon, 6 Apr 2026 07:19:48 +0200 Subject: fix generic new_ids --- tools/Scanner/Protocol.lean | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'tools/Scanner/Protocol.lean') diff --git a/tools/Scanner/Protocol.lean b/tools/Scanner/Protocol.lean index 183ef6a..7661f1e 100644 --- a/tools/Scanner/Protocol.lean +++ b/tools/Scanner/Protocol.lean @@ -155,8 +155,10 @@ inductive ArgumentType where | array | fd | object (nullability : Nullability) (interface : Option InterfaceRef) + | newID (interface : Option InterfaceRef) deriving Repr, BEq, Inhabited +/-- Logical argument (i.e., if there is a newID without an interface, this only includes the newID, not the string and uint). -/ structure ArgumentDesc where name : Identifier type : ArgumentType @@ -171,7 +173,6 @@ structure MessageDesc where since : Nat deprecatedSince : Option Nat arguments : Array ArgumentDesc - rawArguments : Array Raw.ArgumentDesc deriving Repr, BEq, Inhabited inductive ReturnType where @@ -179,10 +180,20 @@ inductive ReturnType where | object (type : Option InterfaceRef) deriving Repr, BEq, Inhabited +def ReturnType.isWlCallback : ReturnType → Bool + | .object (.some iface) => iface.interface == "wl_callback" + | _ => false + structure RequestDesc extends MessageDesc where returnType : ReturnType deriving Repr, BEq, Inhabited +def RequestDesc.inputArguments (req : RequestDesc) : Array ArgumentDesc := + req.arguments.filter fun arg ↦ + match arg.type with + | .newID _ => false + | _ => true + structure EventDesc extends MessageDesc deriving Repr, BEq, Inhabited -- cgit v1.3.1