basic argument (de-)marshalling

1 files changed, 43 insertions, 37 deletions

diff --git a/tools/Scanner/Generator.lean b/tools/Scanner/Generator.lean
index 5884a0d..1f889d0 100644
--- a/tools/Scanner/Generator.lean
+++ b/tools/Scanner/Generator.lean
@@ -68,6 +68,21 @@ private def resolveEnum (enum : EnumRef) : Generator String := do
   let iface ← resolveInterface enum.toInterfaceRef
   return s!"{iface}.{enum.enum.pascalCase}"
 
+private def typeToLean : ArgumentType → Generator String
+  | .int .none                      => do return "Int32"
+  | .int (.some enum)               => resolveEnum enum
+  | .uint .none                     => do return "UInt32"
+  | .uint (.some enum)              => resolveEnum enum
+  | .fixed                          => do return "Float32"
+  | .string .nullable               => do return "Option String"
+  | .string .notNull                => do return "String"
+  | .array                          => do return "ByteArray"
+  | .fd                             => do return "Fd"
+  | .object .nullable .none         => do return "Option AnyObject"
+  | .object .nullable (.some iface) => do return s!"Option {← resolveInterface iface}"
+  | .object .notNull  .none         => do return s!"AnyObject"
+  | .object .notNull  (.some iface) => resolveInterface iface
+
 section Header
 
 private def emitNameDefinitions (protocol : ProtocolDesc) : Generator Unit := do
@@ -76,7 +91,7 @@ private def emitNameDefinitions (protocol : ProtocolDesc) : Generator Unit := do
 
 private def emitObjectDefinitions (protocol : ProtocolDesc) : Generator Unit := do
   for iface in protocol.interfaces do
-    emitLine s!"def {iface.name.pascalCase} : Type := Object {iface.name.pascalCase}.name"
+    emitLine s!"abbrev {iface.name.pascalCase} : Type := Object {iface.name.pascalCase}.name"
 
 private def emitEnumDefinitions (protocol : ProtocolDesc) : Generator Unit := do
   for iface in protocol.interfaces do
@@ -91,6 +106,15 @@ private def emitEnumDefinitions (protocol : ProtocolDesc) : Generator Unit := do
         for entry in enum.entries do
           emitLine s!"  | {entry.name.camelCase}"
 
+private def emitEnumMarshallable (protocol : ProtocolDesc) : Generator Unit := do
+  for iface in protocol.interfaces do
+    for enum in iface.enums do
+      emitLine s!""
+      emitLine s!"instance : Marshallable {iface.name.pascalCase}.{enum.name.pascalCase} where"
+      emitLine s!"  marshal := sorry"
+      emitLine s!"  demarshal := sorry"
+      -- TODO
+
 def generateHeader (rootModule : String) (protocol : ProtocolDesc) : String :=
   Generator.runProtocol rootModule protocol ".Header" do
     emitNamespace rootModule do
@@ -99,6 +123,7 @@ def generateHeader (rootModule : String) (protocol : ProtocolDesc) : String :=
       emitLine ""
       emitObjectDefinitions protocol
       emitEnumDefinitions protocol
+      emitEnumMarshallable protocol
 
 end Header
 
@@ -110,21 +135,7 @@ private def emitEventDefinitions (protocol : ProtocolDesc) : Generator Unit := d
     for event in iface.events do
       emitLine s!"  | {event.name.camelCase}"
       for arg in event.arguments do
-        let argName := arg.name.camelCase
-        match arg.type with
-          | .int .none                      => emitLine s!"    ({argName} : Int32)"
-          | .int (.some enum)               => emitLine s!"    ({argName} : {← resolveEnum enum})"
-          | .uint .none                     => emitLine s!"    ({argName} : UInt32)"
-          | .uint (.some enum)              => emitLine s!"    ({argName} : {← resolveEnum enum})"
-          | .fixed                          => emitLine s!"    ({argName} : Float)"
-          | .string .nullable               => emitLine s!"    ({argName} : Option String)"
-          | .string .notNull                => emitLine s!"    ({argName} : String)"
-          | .array                          => emitLine s!"    ({argName} : ByteArray)"
-          | .fd                             => emitLine s!"    ({argName} : Int32)"
-          | .object .nullable .none         => emitLine s!"    ({argName} : Option AnyObject)"
-          | .object .nullable (.some iface) => emitLine s!"    ({argName} : Option {← resolveInterface iface})"
-          | .object .notNull  .none         => emitLine s!"    ({argName} : AnyObject)"
-          | .object .notNull  (.some iface) => emitLine s!"    ({argName} : {← resolveInterface iface})"
+        emitLine s!"    ({arg.name.camelCase} : {← typeToLean arg.type})"
     emitLine s!""
 
 private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit := do
@@ -168,8 +179,13 @@ private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit :=
     for ev in iface.events do
       emitMessageDesc ev.toMessageDesc
     emitLine s!"  ]"
-    emitLine s!"  demarshalEvent := sorry"
-    -- TODO
+    emitLine s!"  demarshalEvent"
+    for ev in iface.events do
+      emitLine s!"    | {ev.opcode} => do"
+      emitLine s!"      return .{ev.name.camelCase}"
+      for _ in ev.arguments do
+        emitLine s!"        (← Marshallable.demarshal)"
+    emitLine "    | _ => throw s!\"Received invalid opcode\""
 
 def generateInterface (rootModule : String) (protocol : ProtocolDesc) : String :=
   Generator.runProtocol rootModule protocol ".Interface" do
@@ -212,34 +228,24 @@ private def emitRequests (protocol : ProtocolDesc) : Generator Unit := do
       emitLine s!"    (ω : {iface.name.pascalCase})"
       -- TODO: Special wl_callback handling
       for arg in req.arguments do
-        let argName := arg.name.camelCase
-        match arg.type with
-          | .int .none                      => emitLine s!"    ({argName} : Int32)"
-          | .int (.some enum)               => emitLine s!"    ({argName} : {← resolveEnum enum})"
-          | .uint .none                     => emitLine s!"    ({argName} : UInt32)"
-          | .uint (.some enum)              => emitLine s!"    ({argName} : {← resolveEnum enum})"
-          | .fixed                          => emitLine s!"    ({argName} : Float)"
-          | .string .nullable               => emitLine s!"    ({argName} : Option String)"
-          | .string .notNull                => emitLine s!"    ({argName} : String)"
-          | .array                          => emitLine s!"    ({argName} : ByteArray)"
-          | .fd                             => emitLine s!"    ({argName} : Int32)"
-          | .object .nullable .none         => emitLine s!"    ({argName} : Option AnyObject)"
-          | .object .nullable (.some iface) => emitLine s!"    ({argName} : Option {← resolveInterface iface (suffix := ".Resolved")})"
-          | .object .notNull  .none         => emitLine s!"    ({argName} : AnyObject)"
-          | .object .notNull  (.some iface) => emitLine s!"    ({argName} : {← resolveInterface iface (suffix := ".Resolved")})"
+        emitLine s!"    ({arg.name.camelCase} : {← typeToLean arg.type})"
       match req.returnType with
         | .unit                 => emitLine s!"    : DisplayM σ Unit :="
-        | .object .none         => emitLine s!"    : DisplayM σ AnyObject :="
+        | .object .none         => emitLine s!"    : DisplayM σ (Object ι) :="
         | .object (.some iface) => emitLine s!"    : DisplayM σ {← resolveInterface iface (suffix := ".Resolved")} :="
-      emitLine s!"  sorry"
-      -- TODO
+      match req.returnType with
+        | .unit     => emitLine s!"  ω.send do"
+        | .object _ => emitLine s!"  ω.sendConstructor do"
+      for arg in req.arguments do
+        emitLine s!"    Marshallable.marshal {arg.name.camelCase}"
+      emitLine s!"    return {req.opcode}"
 
 def generateRequests (rootModule : String) (protocol : ProtocolDesc) : String :=
   Generator.runProtocol rootModule protocol ".Requests" do
     emitNamespace rootModule do
       emitImport "Wayland.Display"
       emitLocalImport protocol.name ".Resolved"
-      emitLine "variable {σ : Type}"
+      emitLine "variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]"
       emitRequests protocol
 
 end Requests