fix generic new_ids

3 files changed, 70 insertions, 26 deletions

diff --git a/tools/Scanner/Generator.lean b/tools/Scanner/Generator.lean
index 1f889d0..76542e7 100644
--- a/tools/Scanner/Generator.lean
+++ b/tools/Scanner/Generator.lean
@@ -82,6 +82,8 @@ private def typeToLean : ArgumentType → Generator String
   | .object .nullable (.some iface) => do return s!"Option {← resolveInterface iface}"
   | .object .notNull  .none         => do return s!"AnyObject"
   | .object .notNull  (.some iface) => resolveInterface iface
+  | .newID .none                    => do return s!"AnyObject"
+  | .newID (.some iface)            => resolveInterface iface
 
 section Header
 
@@ -142,23 +144,24 @@ private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit :=
   let emitMessageDesc (msg : MessageDesc) : Generator Unit := do
     emitLine   "    {"
     emitLine s!"      name := {msg.name.quoted}"
-    let nullability (arg : Raw.ArgumentDesc) : String :=
-      if arg.allowNull then ".nullable" else ".notNull"
-    let interfaceName (arg : Raw.ArgumentDesc) : String :=
-      match arg.interface with
-        | .some iface => s!"(.some \"{iface}\")"
-        | .none       =>   ".none"
-    let argumentDesc (arg : Raw.ArgumentDesc) : String :=
+    let nullability : Nullability → String
+      | .nullable => ".nullable"
+      | .notNull  => ".notNull"
+    let interfaceName : Option InterfaceRef → String
+      | .some iface => s!"(.some {iface.interface.quoted})"
+      | .none       =>   ".none"
+    let argumentDesc (arg : ArgumentDesc) : String :=
       match arg.type with
-        | .int    =>   ".int"
-        | .uint   =>   ".uint"
-        | .fixed  =>   ".fixed"
-        | .string => s!".string {nullability arg}"
-        | .object => s!".object {nullability arg} {interfaceName arg}"
-        | .newID  => s!".newID {interfaceName arg}"
-        | .array  =>   ".array"
-        | .fd     =>   ".fd"
-    let args := msg.rawArguments
+        | .int _               =>   ".int"
+        | .uint _              =>   ".uint"
+        | .fixed               =>   ".fixed"
+        | .string null         => s!".string {nullability null}"
+        | .object null iface   => s!".object {nullability null} {interfaceName iface}"
+        | .newID (.some iface) => s!".newID (.some {iface.interface.quoted})"
+        | .newID .none         =>   ".string .notNull, .uint, .newID .none"
+        | .array               =>   ".array"
+        | .fd                  =>   ".fd"
+    let args := msg.arguments
       |>.map argumentDesc
       |>.toList
       |> String.intercalate ", "
@@ -223,11 +226,15 @@ section Requests
 private def emitRequests (protocol : ProtocolDesc) : Generator Unit := do
   for iface in protocol.interfaces do
     for req in iface.requests do
+      let baseName := s!"{iface.name.pascalCase}.{req.name.camelCase}"
+      let rawName :=
+        if req.returnType.isWlCallback
+        then baseName ++ ".raw"
+        else baseName
       emitLine s!""
-      emitLine s!"def {iface.name.pascalCase}.{req.name.camelCase}"
+      emitLine s!"def {rawName}"
       emitLine s!"    (ω : {iface.name.pascalCase})"
-      -- TODO: Special wl_callback handling
-      for arg in req.arguments do
+      for arg in req.inputArguments do
         emitLine s!"    ({arg.name.camelCase} : {← typeToLean arg.type})"
       match req.returnType with
         | .unit                 => emitLine s!"    : DisplayM σ Unit :="
@@ -237,8 +244,31 @@ private def emitRequests (protocol : ProtocolDesc) : Generator Unit := do
         | .unit     => emitLine s!"  ω.send do"
         | .object _ => emitLine s!"  ω.sendConstructor do"
       for arg in req.arguments do
-        emitLine s!"    Marshallable.marshal {arg.name.camelCase}"
+        match arg.type with
+          | .newID (.some _) =>
+            emitLine s!"    ArgumentMarshaller.marshalAnyObject .none"
+          | .newID .none =>
+            emitLine s!"    ArgumentMarshaller.marshalString (.some ι)"
+            emitLine s!"    ArgumentMarshaller.marshalUInt (inferInstanceAs (Interface ι)).version"
+            emitLine s!"    ArgumentMarshaller.marshalAnyObject .none"
+          | _ =>
+            emitLine s!"    Marshallable.marshal {arg.name.camelCase}"
       emitLine s!"    return {req.opcode}"
+      -- Special case wl_callback handling
+      if req.returnType.isWlCallback then
+        emitLine s!""
+        emitLine s!"def {baseName}"
+        emitLine s!"    (ω : {iface.name.pascalCase})"
+        for arg in req.inputArguments do
+          emitLine s!"    ({arg.name.camelCase} : {← typeToLean arg.type})"
+        emitLine s!"    (γ : DisplayM σ Unit)"
+        emitLine s!"    : DisplayM σ Unit := do"
+        let argNames := #["ω"] ++ (req.inputArguments.map fun arg ↦ arg.name.camelCase)
+          |>.toList
+          |> String.intercalate " "
+        emitLine s!"  let ρ ← {rawName} {argNames}"
+        emitLine s!"  ρ.listen fun"
+        emitLine s!"    | .done _ => do ρ.keep; γ"
 
 def generateRequests (rootModule : String) (protocol : ProtocolDesc) : String :=
   Generator.runProtocol rootModule protocol ".Requests" do
diff --git a/tools/Scanner/Processor.lean b/tools/Scanner/Processor.lean
index a50767f..fd952a2 100644
--- a/tools/Scanner/Processor.lean
+++ b/tools/Scanner/Processor.lean
@@ -87,14 +87,13 @@ private def processArgument (raw : Raw.ArgumentDesc) : TrackingProcessor Client.
         | .string => Client.ArgumentType.string (.ofAllowNull raw.allowNull) |> pure
         | .array  => Client.ArgumentType.array |> pure
         | .fd     => Client.ArgumentType.fd |> pure
-        | .newID  => Client.ArgumentType.object .notNull <$> raw.interface.mapM resolveInterface
+        | .newID  => Client.ArgumentType.newID <$> raw.interface.mapM resolveInterface
         | .object => Client.ArgumentType.object (.ofAllowNull raw.allowNull) <$> raw.interface.mapM resolveInterface
     description := raw.description
   }
 
 private def processRequest (raw : Raw.MessageDesc) : TrackingProcessor Client.RequestDesc := do
   let newIDArgs := raw.arguments.filter fun arg ↦ arg.type == .newID
-  let otherArgs := raw.arguments.filter fun arg ↦ arg.type != .newID
   let returnType ←
     match newIDArgs with
       | #[]    => Client.ReturnType.unit |> pure
@@ -107,12 +106,17 @@ private def processRequest (raw : Raw.MessageDesc) : TrackingProcessor Client.Re
     isDestructor := raw.type == .destructor
     since := raw.since
     deprecatedSince := raw.deprecatedSince
-    rawArguments := raw.arguments
-    arguments := ← otherArgs.mapM processArgument
+    arguments := ← raw.arguments.mapM processArgument
     returnType := returnType
   }
 
 private def processEvent (raw : Raw.MessageDesc) : TrackingProcessor Client.EventDesc := do
+  let hasInvalidArg := raw.arguments.any fun arg ↦
+    match arg.type, arg.interface with
+      | .newID, .none => true
+      | _,      _     => false
+  if hasInvalidArg then
+    throw s!"Event arguments of type new_id must have an interface type specified (in {raw.name})"
   return {
     name := raw.name
     opcode := raw.opcode
@@ -120,7 +124,6 @@ private def processEvent (raw : Raw.MessageDesc) : TrackingProcessor Client.Even
     isDestructor := raw.type == .destructor
     since := raw.since
     deprecatedSince := raw.deprecatedSince
-    rawArguments := raw.arguments
     arguments := ← raw.arguments.mapM processArgument
   }
 
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