fix generic new_ids

1 files changed, 50 insertions, 20 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