diff options
Diffstat (limited to 'tools/Scanner/Protocol.lean')
| -rw-r--r-- | tools/Scanner/Protocol.lean | 13 |
1 files changed, 12 insertions, 1 deletions
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 |