initial codegen

10 files changed, 392 insertions, 93 deletions

diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc
index 5f9b052..0c02d66 100644
--- a/lib/CWayland/CWayland.cc
+++ b/lib/CWayland/CWayland.cc
@@ -1279,4 +1279,12 @@ lean_obj_res waylean_proxy_keep(b_lean_obj_arg proxy)
 {
     (void)proxy;
     return lean_io_result_mk_ok(lean_box(0));
+}
+
+// Proxy.getType : (proxy : @& Proxy) → IO String
+lean_obj_res waylean_proxy_get_type(b_lean_obj_arg proxy_obj)
+{
+    auto proxy = static_cast<wl_proxy*>(lean_get_external_data(proxy_obj));
+    auto name = wl_proxy_get_interface(proxy)->name;
+    return lean_io_result_mk_ok(lean_mk_string(name));
 }
\ No newline at end of file
diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h
index 74ed5e6..1eeb98f 100644
--- a/lib/CWayland/CWayland.h
+++ b/lib/CWayland/CWayland.h
@@ -82,6 +82,7 @@ lean_obj_res waylean_proxy_send_constructor(b_lean_obj_arg proxy,
 lean_obj_res waylean_proxy_listen          (b_lean_obj_arg proxy,
                                             lean_obj_arg   handler);
 lean_obj_res waylean_proxy_keep            (b_lean_obj_arg proxy);
+lean_obj_res waylean_proxy_get_type        (b_lean_obj_arg proxy);
 
 #ifdef __cplusplus
 }
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 7bf55c5..9b3b0da 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -32,6 +32,12 @@ structure Object (ι : InterfaceName) : Type where
   private proxy : Native.Proxy
   deriving Nonempty
 
+/-- Opaque handle to an object whose type is not statically known. -/
+structure AnyObject : Type where
+  private proxy : Native.Proxy
+  private type : String
+  deriving Nonempty
+
 /-- Monad in which arguments can be marshalled one after another. -/
 class ArgumentMarshaller (m : Type → Type) extends Monad m where
   marshalInt                        : Int32             → m Unit
@@ -39,6 +45,7 @@ class ArgumentMarshaller (m : Type → Type) extends Monad m where
   marshalFixed                      : Float32           → m Unit
   marshalString                     : Option String     → m Unit
   marshalObject {ι : InterfaceName} : Option (Object ι) → m Unit
+  marshalAnyObject                  : Option AnyObject  → m Unit
   marshalArray                      : ByteArray         → m Unit
   marshalFD                         : Int32             → m Unit
 
@@ -49,6 +56,7 @@ class ArgumentDemarshaller (m : Type → Type) extends Monad m where
   demarshalFixed                      : m Float32
   demarshalString                     : m (Option String)
   demarshalObject {ι : InterfaceName} : m (Option (Object ι))
+  demarshalAnyObject                  : m (Option AnyObject)
   demarshalArray                      : m ByteArray
   demarshalFD                         : m Int32
 
@@ -63,8 +71,8 @@ inductive ArgumentDesc where
   | uint : ArgumentDesc
   | fixed : ArgumentDesc
   | string : Nullability → ArgumentDesc
-  | object : Nullability → InterfaceName → ArgumentDesc
-  | newID : InterfaceName → ArgumentDesc
+  | object : Nullability → (Option InterfaceName) → ArgumentDesc
+  | newID : (Option InterfaceName) → ArgumentDesc
   | array : ArgumentDesc
   | fd : ArgumentDesc
 
@@ -239,6 +247,7 @@ private instance : ArgumentMarshaller ArgumentBufferM where
   marshalFixed v := do (← read).writeFixed v
   marshalString v := do (← read).writeString v
   marshalObject v := do (← read).writeObject (v.map Object.proxy)
+  marshalAnyObject v := do (← read).writeObject (v.map AnyObject.proxy)
   marshalArray v := do (← read).writeArray v
   marshalFD v := do (← read).writeFD v
 
@@ -247,7 +256,13 @@ private instance : ArgumentDemarshaller ArgumentBufferM where
   demarshalUInt := do (← read).readUInt
   demarshalFixed := do (← read).readFixed
   demarshalString := do (← read).readString
-  demarshalObject := do let proxy ← (← read).readObject; return proxy.map Object.mk
+  demarshalObject := do
+    let proxy ← (← read).readObject
+    return proxy.map Object.mk
+  demarshalAnyObject := do
+    let proxy ← (← read).readObject
+    proxy.mapM fun proxy ↦ do
+      return ⟨proxy, ← proxy.getType⟩
   demarshalArray := do (← read).readArray
   demarshalFD := do (← read).readFD
 
@@ -271,8 +286,8 @@ private def MessageDesc.toNative (msg : MessageDesc) : Native.Message :=
     | .array => "a"
     | .fd => "h"
   let argType : ArgumentDesc → Option String
-    | .object _ iface => .some iface
-    | .newID iface => .some iface
+    | .object _ iface => iface
+    | .newID iface => iface
     | _ => .none
   { name := msg.name
     signature := s!"{msg.since}{String.join (msg.args.toList.map argString)}"
@@ -295,14 +310,16 @@ def DisplayM.getDisplay : DisplayM σ (Object "wl_display") := do
   let proxy ← Native.Proxy.fromDisplay (← read).disp
   return ⟨proxy⟩
 
+variable {ι ι' : InterfaceName}
+
 /-- Send a request for an object to the server that doesn't construct any new object. -/
-def Object.send {ι : InterfaceName} (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ Unit := do
+def Object.send (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ Unit := do
   let argBuffer ← Native.ArgumentBuffer.new
   let opcode ← ArgumentBufferM.run marshaller argBuffer
   obj.proxy.send opcode argBuffer
 
 /-- Send a request for an object to the server, allocating a new id for a constructed object in the process. -/
-def Object.sendConstructor {ι ι' : InterfaceName} [iface : ResolvedInterface ι'] (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ (Object ι') := do
+def Object.sendConstructor [iface : ResolvedInterface ι'] (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ (Object ι') := do
   DisplayM.ensureInterface ι'
   let typeMap := (← read).typeMap
   let argBuffer ← Native.ArgumentBuffer.new
@@ -311,7 +328,7 @@ def Object.sendConstructor {ι ι' : InterfaceName} [iface : ResolvedInterface �
   return ⟨proxy⟩
 
 /-- Listen for events from the server for an object. -/
-def Object.listen {ι : InterfaceName} [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := do
+def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := do
   let global ← read
   let actualHandler (opcode : UInt32) (argBuffer : Native.ArgumentBuffer) : StateT σ IO Unit := do
     let event ← ArgumentBufferM.run (iface.demarshalEvent opcode) argBuffer
@@ -319,9 +336,17 @@ def Object.listen {ι : InterfaceName} [iface : Interface ι] (obj : Object ι)
   global.listen obj.proxy actualHandler
 
 /-- Shorthand to ensure the reference count of an `Object` does not drop to `0`. -/
-def Object.keep {ι : InterfaceName} (obj : Object ι) : DisplayM σ Unit :=
+def Object.keep (obj : Object ι) : DisplayM σ Unit :=
   obj.proxy.keep
 
+/-- Erase the type information from an object. -/
+def Object.toAny (obj : Object ι) : AnyObject :=
+  ⟨obj.proxy, ι⟩
+
+/-- Try to cast a type-erased object into a typed object. -/
+def AnyObject.cast (obj : AnyObject) : Option (Object ι) :=
+  if obj.type == ι then .some ⟨obj.proxy⟩ else .none
+
 end Proxies
 
 end Wayland
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index 430472b..25884ed 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -139,4 +139,7 @@ opaque Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentBuffe
 @[extern "waylean_proxy_keep"]
 opaque Proxy.keep : (proxy : @& Proxy) → IO Unit
 
+@[extern "waylean_proxy_get_type"]
+opaque Proxy.getType : (proxy : @& Proxy) → IO String
+
 end Wayland.Native
diff --git a/src/Waylean.lean b/src/Waylean.lean
index b595672..f7eb668 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,67 +1,10 @@
 import Wayland
-open Wayland
+open Wayland Protocols
 
-
-def WLCallback.name : InterfaceName := "wl_callback"
-def WLDisplay.name : InterfaceName := "wl_display"
-
-def WLDisplay : Type := Object WLDisplay.name
-def WLCallback : Type := Object WLCallback.name
-
-inductive WLDisplay.Event where
-  | error : (code : UInt32) → (message : String) → Event
-
-instance : Interface WLDisplay.name where
-  event := WLDisplay.Event
-  requests :=
-    #[ { name := "sync"
-         args := #[.newID WLCallback.name]
-         since := 0
-         isDestructor := False } ]
-  events :=
-    #[ { name := "error"
-         args := #[.object .notNull WLDisplay.name, .uint, .string .notNull]
-         since := 0
-         isDestructor := False } ]
-  demarshalEvent
-    | 0 => do
-      (_ : Option (Object WLDisplay.name)) ← ArgumentDemarshaller.demarshalObject
-      return .error
-        (← ArgumentDemarshaller.demarshalUInt)
-        ((← ArgumentDemarshaller.demarshalString).getD "")
-    | _ => sorry
-  version := 1
-
-inductive WLCallback.Event where
-  | done : (data : UInt32) → Event
-
-instance : Interface WLCallback.name where
-  event := WLCallback.Event
-  requests :=
-    #[]
-  events :=
-    #[ { name := "done"
-         args := #[.uint]
-         since := 0
-         isDestructor := False } ]
-  demarshalEvent
-    | 0 => do
-      return .done
-        (← ArgumentDemarshaller.demarshalUInt)
-    | _ => sorry
-  version := 1
-
-instance : ResolvedInterface WLDisplay.name where
-  referencedInterfaces := #[⟨WLDisplay.name, inferInstance⟩, ⟨WLCallback.name, inferInstance⟩]
-
-instance : ResolvedInterface WLCallback.name where
-  referencedInterfaces := #[⟨WLCallback.name, inferInstance⟩]
-
-def WLDisplay.sync {σ : Type} (display : WLDisplay) (handler : DisplayM σ Unit) : DisplayM σ Unit := do
-  let callback : WLCallback ← display.sendConstructor do
-    return 0
+def Wayland.Protocols.WlDisplay.roundtrip {σ : Type} (display : WlDisplay) (handler : DisplayM σ Unit) : DisplayM σ Unit := do
+  let callback ← display.sync
   callback.listen fun
-  | .done _ => do
+    | .done _ => do
       callback.keep
       handler
 
@@ -81,8 +24,8 @@ def launch : DisplayM State Unit := do
     DisplayM.requestQuit
   DisplayM.zoom (mk_lens count) nextTimer
 
-  let disp : WLDisplay ← DisplayM.getDisplay
-  disp.sync do
+  let disp : WlDisplay ← DisplayM.getDisplay
+  disp.roundtrip do
     DisplayM.liftIO (IO.println "Roundtrip complete")
 
 def main : IO Unit :=
diff --git a/tools/Scanner.lean b/tools/Scanner.lean
index 81b4181..1daed2a 100644
--- a/tools/Scanner.lean
+++ b/tools/Scanner.lean
@@ -1,6 +1,7 @@
 import Scanner.Protocol
 import Scanner.Parser
 import Scanner.Processor
+import Scanner.Generator
 
 open WaylandScanner
 
@@ -9,6 +10,24 @@ def parseRawProtocol (path : System.FilePath) : IO Raw.ProtocolDesc := do
     |>.mapError (fun ε ↦ s!"{path}: {ε}")
     |> IO.ofExcept
 
+def writeProtocol (protocol : Client.ProtocolDesc) (rootModule : String) (rootModulePath : System.FilePath) : IO Unit := do
+  let protocolPath := rootModulePath / protocol.name.pascalCase
+  IO.FS.createDirAll protocolPath
+  let umbrellaPath := protocolPath.addExtension "lean"
+  IO.FS.writeFile umbrellaPath <| generateUmbrella rootModule protocol
+  let headerPath := protocolPath / "Header.lean"
+  IO.FS.writeFile headerPath <| generateHeader rootModule protocol
+  let interfacePath := protocolPath / "Interface.lean"
+  IO.FS.writeFile interfacePath <| generateInterface rootModule protocol
+  let resolvedPath := protocolPath / "Resolved.lean"
+  IO.FS.writeFile resolvedPath <| generateResolved rootModule protocol
+  let requestsPath := protocolPath / "Requests.lean"
+  IO.FS.writeFile requestsPath <| generateRequests rootModule protocol
+
+def writeIndex (protocols : Array Client.ProtocolDesc) (rootModule : String) (rootModulePath : System.FilePath) : IO Unit := do
+  let indexPath := rootModulePath.addExtension "lean"
+  IO.FS.writeFile indexPath <| generateIndex rootModule protocols
+
 def process (rootModule : String) (outPath : System.FilePath) (srcPath : System.FilePath) : IO UInt32 := do
   let rawProtocols ← (← srcPath.readDir)
     |>.map IO.FS.DirEntry.path
@@ -19,10 +38,10 @@ def process (rootModule : String) (outPath : System.FilePath) (srcPath : System.
     |>.map String.Slice.toString
     |>.toArray
   let rootModulePath := rootModuleComponents.foldl (· / ·) outPath
-  IO.println (reprStr clientProtocols)
   IO.FS.createDirAll rootModulePath
-  let indexPath := rootModulePath.addExtension "lean"
-  IO.FS.writeFile indexPath ""
+  for protocol in clientProtocols do
+    writeProtocol protocol rootModule rootModulePath
+  writeIndex clientProtocols rootModule rootModulePath
   return 0
 
 def usage : IO UInt32 := do
diff --git a/tools/Scanner/Generator.lean b/tools/Scanner/Generator.lean
new file mode 100644
index 0000000..1ac8139
--- /dev/null
+++ b/tools/Scanner/Generator.lean
@@ -0,0 +1,267 @@
+import Std.Data.TreeSet
+import Scanner.Protocol
+
+/-!
+# Generating Code from Protocol Descriptions
+
+This turns a `Client.ProtocolDesc` into the various Lean source files containing bindings for said protocol.
+-/
+
+namespace WaylandScanner
+
+open Client
+
+-- TODO: Maybe use Lean's `Syntax` API here instead of a custom formatter?
+
+private structure GeneratorState where
+  imports : Std.TreeSet String := .empty
+  code : Array String := #[]
+
+private structure GeneratorContext where
+  rootModule : String
+  currentModule : String
+
+private abbrev Generator := StateT GeneratorState (ReaderM GeneratorContext)
+
+private def emitImport (mod : String) : Generator Unit := do
+  let current := (← read).currentModule
+  if current != mod then
+    let oldState ← get
+    set { oldState with imports := oldState.imports.insert mod }
+  return ()
+
+private def emitLocalImport (protocolName : Identifier) (suffix : String := "") : Generator Unit := do
+  let root := (← read).rootModule
+  emitImport s!"{root}.{protocolName.pascalCase}{suffix}"
+
+private def emitLine (line : String) : Generator Unit := do
+  let oldState ← get
+  set { oldState with code := oldState.code ++ #[line] }
+
+private def emitNamespace {α : Type} (space : String) (gen : Generator α) : Generator α := do
+  emitLine s!"namespace {space}"
+  emitLine s!""
+  let res ← gen
+  emitLine s!""
+  emitLine s!"end {space}"
+  return res
+
+private def Generator.run (gen : Generator Unit) : ReaderM GeneratorContext String := do
+  let (_, res) ← StateT.run gen {}
+  let imports := res.imports
+    |>.toArray
+    |>.map fun m ↦ s!"import {m}"
+  let lines := imports ++ #[""] ++ res.code
+  return String.intercalate "\n" lines.toList
+
+private def Generator.runProtocol (rootModule : String) (protocol : ProtocolDesc) (suffix : String := "") (gen : Generator Unit) : String :=
+  gen.run.run { rootModule, currentModule := s!"{rootModule}.{protocol.name.pascalCase}{suffix}" }
+
+private def Generator.runIndex (rootModule : String) (gen : Generator Unit) : String :=
+  gen.run.run { rootModule, currentModule := rootModule }
+
+private def resolveInterface (iface : InterfaceRef) (suffix : String := ".Header") : Generator String := do
+  emitLocalImport iface.moduleName suffix
+  return iface.typeName.pascalCase
+
+private def resolveEnum (enum : EnumRef) : Generator String := do
+  let iface ← resolveInterface enum.toInterfaceRef
+  return s!"{iface}.{enum.enumName.pascalCase}"
+
+section Header
+
+private def emitNameDefinitions (protocol : ProtocolDesc) : Generator Unit := do
+  for iface in protocol.interfaces do
+    emitLine s!"abbrev {iface.name.pascalCase}.name : InterfaceName := {iface.name.quoted}"
+
+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"
+
+private def emitEnumDefinitions (protocol : ProtocolDesc) : Generator Unit := do
+  for iface in protocol.interfaces do
+    for enum in iface.enums do
+      emitLine s!""
+      if enum.bitfield then
+        emitLine s!"structure {iface.name.pascalCase}.{enum.name.pascalCase} where"
+        for entry in enum.entries do
+          emitLine s!"  {entry.name.camelCase} : Bool"
+      else
+        emitLine s!"inductive {iface.name.pascalCase}.{enum.name.pascalCase} where"
+        for entry in enum.entries do
+          emitLine s!"  | {entry.name.camelCase}"
+
+def generateHeader (rootModule : String) (protocol : ProtocolDesc) : String :=
+  Generator.runProtocol rootModule protocol ".Header" do
+    emitNamespace rootModule do
+      emitImport "Wayland.Display"
+      emitNameDefinitions protocol
+      emitLine ""
+      emitObjectDefinitions protocol
+      emitEnumDefinitions protocol
+
+end Header
+
+section Interface
+
+private def emitEventDefinitions (protocol : ProtocolDesc) : Generator Unit := do
+  for iface in protocol.interfaces do
+    emitLine s!"inductive {iface.name.pascalCase}.Event where"
+    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!""
+
+private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit := do
+  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 :=
+      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
+      |>.map argumentDesc
+      |>.toList
+      |> String.intercalate ", "
+    emitLine s!"      args := #[{args}]"
+    emitLine s!"      since := {msg.since}"
+    emitLine s!"      isDestructor := {msg.isDestructor}"
+    emitLine   "    },"
+  for iface in protocol.interfaces do
+    emitLine s!""
+    emitLine s!"instance : Interface {iface.name.pascalCase}.name where"
+    emitLine s!"  event := {iface.name.pascalCase}.Event"
+    emitLine s!"  version := {iface.version}"
+    emitLine s!"  requests := #["
+    for req in iface.requests do
+      emitMessageDesc req.toMessageDesc
+    emitLine s!"  ]"
+    emitLine s!"  events := #["
+    for ev in iface.events do
+      emitMessageDesc ev.toMessageDesc
+    emitLine s!"  ]"
+    emitLine s!"  demarshalEvent := sorry"
+    -- TODO
+
+def generateInterface (rootModule : String) (protocol : ProtocolDesc) : String :=
+  Generator.runProtocol rootModule protocol ".Interface" do
+    emitNamespace rootModule do
+      emitImport "Wayland.Display"
+      emitLocalImport protocol.name ".Header"
+      emitEventDefinitions protocol
+      emitInterfaceInstances protocol
+
+end Interface
+
+section Resolved
+
+private def emitResolvedInterfaces (protocol : ProtocolDesc) : Generator Unit := do
+  for iface in protocol.interfaces do
+    emitLine s!"instance : ResolvedInterface {iface.name.pascalCase}.name where"
+    emitLine s!"  referencedInterfaces := #["
+    for ref in iface.referencedInterfaces do
+      let name ← resolveInterface ref (suffix := ".Interface")
+      emitLine s!"    ⟨{name}.name, inferInstance⟩,"
+    emitLine s!"  ]"
+    emitLine s!""
+
+def generateResolved (rootModule : String) (protocol : ProtocolDesc) : String :=
+  Generator.runProtocol rootModule protocol ".Resolved" do
+    emitNamespace rootModule do
+      emitImport "Wayland.Display"
+      emitLocalImport protocol.name ".Interface"
+      emitResolvedInterfaces protocol
+
+end Resolved
+
+section Requests
+
+private def emitRequests (protocol : ProtocolDesc) : Generator Unit := do
+  for iface in protocol.interfaces do
+    for req in iface.requests do
+      emitLine s!""
+      emitLine s!"def {iface.name.pascalCase}.{req.name.camelCase}"
+      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")})"
+      match req.returnType with
+        | .unit                 => emitLine s!"    : DisplayM σ Unit :="
+        | .object .none         => emitLine s!"    : DisplayM σ AnyObject :="
+        | .object (.some iface) => emitLine s!"    : DisplayM σ {← resolveInterface iface (suffix := ".Resolved")} :="
+      emitLine s!"  sorry"
+      -- TODO
+
+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}"
+      emitRequests protocol
+
+end Requests
+
+section Umbrella
+
+def generateUmbrella (rootModule : String) (protocol : ProtocolDesc) : String :=
+  Generator.runProtocol rootModule protocol "" do
+    emitLocalImport protocol.name ".Header"
+    emitLocalImport protocol.name ".Interface"
+    emitLocalImport protocol.name ".Resolved"
+    emitLocalImport protocol.name ".Requests"
+
+end Umbrella
+
+section Index
+
+def generateIndex (rootModule : String) (protocols : Array ProtocolDesc) : String :=
+  Generator.runIndex rootModule do
+    for protocol in protocols do
+      emitLocalImport protocol.name
+
+end Index
+
+end WaylandScanner
diff --git a/tools/Scanner/Parser.lean b/tools/Scanner/Parser.lean
index f89c239..5ee867b 100644
--- a/tools/Scanner/Parser.lean
+++ b/tools/Scanner/Parser.lean
@@ -93,9 +93,10 @@ private def ArgumentType.ofString : String → Except String ArgumentType
 
 private def processDescription (el : Xml.Element) : Except String Description := do
   el.ensureName "description"
+  let body := el.textContent
   return {
     summary := el.getAttribute "summary"
-    body := el.textContent
+    body := if body.isEmpty then .none else .some body
   }
 
 private def processEnumEntry (el : Xml.Element) : Except String EnumEntryDesc := do
diff --git a/tools/Scanner/Processor.lean b/tools/Scanner/Processor.lean
index d591ee7..22148ed 100644
--- a/tools/Scanner/Processor.lean
+++ b/tools/Scanner/Processor.lean
@@ -21,9 +21,12 @@ private abbrev InterfaceMap := Std.TreeMap String InterfaceInfo
 private structure Context where
   interfaces : InterfaceMap
   currentInterface : Client.InterfaceRef
+
+private structure TrackingState where
   referencedInterfaces : Std.TreeSet Client.InterfaceRef
 
-private abbrev Processor : Type → Type := StateT Context (Except String)
+private abbrev Processor : Type → Type := ReaderT Context (Except String)
+private abbrev TrackingProcessor : Type → Type := StateT TrackingState Processor
 
 private def processEnumEntry (raw : Raw.EnumEntryDesc) : Processor Client.EnumEntryDesc := do
   return {
@@ -35,11 +38,11 @@ private def processEnumEntry (raw : Raw.EnumEntryDesc) : Processor Client.EnumEn
   }
 
 private def interfaceInfo (name : String) : Processor InterfaceInfo := do
-  match (← get).interfaces.get? name with
+  match (← read).interfaces.get? name with
   | .some info => pure info
   | .none => .error s!"Unable to find referenced interface {name}"
 
-private def resolveInterface (name : String) : Processor Client.InterfaceRef := do
+private def resolveInterface (name : String) : TrackingProcessor Client.InterfaceRef := do
   let info ← interfaceInfo name
   let ref := {
     moduleName := info.moduleName
@@ -52,7 +55,7 @@ private def resolveInterface (name : String) : Processor Client.InterfaceRef :=
 private def resolveEnum (name : String) : Processor Client.EnumRef := do
   let (interface, enum) ←
     match (name.split ".").toArray with
-    | #[enum]            => pure ((← get).currentInterface.typeName, enum.toString)
+    | #[enum]            => pure ((← read).currentInterface.typeName, enum.toString)
     | #[interface, enum] => pure (interface.toString, enum.toString)
     | _                  => throw s!"Malformed enum reference {name}"
   let info ← interfaceInfo interface
@@ -66,20 +69,20 @@ private def resolveEnum (name : String) : Processor Client.EnumRef := do
 
 private def processEnum (raw : Raw.EnumDesc) : Processor Client.EnumDesc := do
   return {
-    name := raw.name
+    name := if raw.name != "event" then raw.name else "event'" -- We define an `Iface.Event` type, so avoid any possible conflicts.
     description := raw.description
     since := raw.since
     bitfield := raw.bitfield
     entries := ← raw.entries.mapM processEnumEntry
   }
 
-private def processArgument (raw : Raw.ArgumentDesc) : Processor Client.ArgumentDesc := do
+private def processArgument (raw : Raw.ArgumentDesc) : TrackingProcessor Client.ArgumentDesc := do
   return {
     name := raw.name
     type :=
       ← match raw.type with
-      | .int    => Client.ArgumentType.int <$> raw.enum.mapM resolveEnum
-      | .uInt   => Client.ArgumentType.uInt <$> raw.enum.mapM resolveEnum
+      | .int    => Client.ArgumentType.int <$> raw.enum.mapM (liftM ∘ resolveEnum)
+      | .uInt   => Client.ArgumentType.uInt <$> raw.enum.mapM (liftM ∘ resolveEnum)
       | .fixed  => Client.ArgumentType.fixed |> pure
       | .string => Client.ArgumentType.string (.ofAllowNull raw.allowNull) |> pure
       | .array  => Client.ArgumentType.array |> pure
@@ -89,7 +92,7 @@ private def processArgument (raw : Raw.ArgumentDesc) : Processor Client.Argument
     description := raw.description
   }
 
-private def processRequest (raw : Raw.MessageDesc) : Processor Client.RequestDesc := do
+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 ←
@@ -104,11 +107,12 @@ private def processRequest (raw : Raw.MessageDesc) : Processor Client.RequestDes
     isDestructor := raw.type == .destructor
     since := raw.since
     deprecatedSince := raw.deprecatedSince
+    rawArguments := raw.arguments
     arguments := ← otherArgs.mapM processArgument
     returnType := returnType
   }
 
-private def processEvent (raw : Raw.MessageDesc) : Processor Client.EventDesc := do
+private def processEvent (raw : Raw.MessageDesc) : TrackingProcessor Client.EventDesc := do
   return {
     name := raw.name
     opcode := raw.opcode
@@ -116,14 +120,16 @@ private def processEvent (raw : Raw.MessageDesc) : Processor Client.EventDesc :=
     isDestructor := raw.type == .destructor
     since := raw.since
     deprecatedSince := raw.deprecatedSince
+    rawArguments := raw.arguments
     arguments := ← raw.arguments.mapM processArgument
   }
 
 private def processInterface (raw : Raw.InterfaceDesc) : Processor Client.InterfaceDesc := do
-  let requests ← raw.requests.mapM processRequest
-  let events ← raw.events.mapM processEvent
-  let state ← get
-  let referencedInterfaces := state.referencedInterfaces.insert state.currentInterface
+  let state : TrackingState := {
+    referencedInterfaces := { (← read).currentInterface }
+  }
+  let (requests, state) ← StateT.run (raw.requests.mapM processRequest) state
+  let (events, state) ← StateT.run (raw.events.mapM processEvent) state
   return {
     name := raw.name
     version := raw.version
@@ -131,7 +137,7 @@ private def processInterface (raw : Raw.InterfaceDesc) : Processor Client.Interf
     enums := ← raw.enums.mapM processEnum
     requests := requests
     events := events
-    referencedInterfaces := referencedInterfaces
+    referencedInterfaces := state.referencedInterfaces
   }
 
 private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc) : Except String Client.ProtocolDesc := do
@@ -140,10 +146,9 @@ private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc)
     copyright := raw.copyright
     description := raw.description
     interfaces := ← raw.interfaces.mapM
-      fun iface ↦ (processInterface iface).run' {
+      fun iface ↦ (processInterface iface).run {
         interfaces := interfaces
         currentInterface := { moduleName := raw.name, typeName := iface.name }
-        referencedInterfaces := .empty
       }
   }
 
diff --git a/tools/Scanner/Protocol.lean b/tools/Scanner/Protocol.lean
index 77908d9..6f74126 100644
--- a/tools/Scanner/Protocol.lean
+++ b/tools/Scanner/Protocol.lean
@@ -15,6 +15,32 @@ def Description.ofSummary (s : String) : Description :=
 def Identifier := String
   deriving Repr, BEq, Ord, Inhabited
 
+def Identifier.quoted (ident : Identifier) : String :=
+  let s : String := ident
+  s!"\"{s}\""
+
+private def Identifier.pascalCase' (parts : List String.Slice) : String :=
+  parts
+    |>.map (String.capitalize ∘ String.Slice.toString)
+    |> String.join
+
+private def sanitize (s : String) : String :=
+  let isInvalid :=
+    ((0 : String.Pos.Raw).get s).isDigit || s == "class"
+  if isInvalid then "_" ++ s else s
+
+def Identifier.pascalCase (ident : Identifier) : String :=
+  ident
+    |>.split "_"
+    |>.toList
+    |> pascalCase'
+    |> sanitize
+
+def Identifier.camelCase (ident : Identifier) : String :=
+  match (ident.split "_").toList with
+  | [] => ""
+  | x::xs => sanitize (x.toString ++ pascalCase' xs)
+
 namespace Raw
 
 structure EnumEntryDesc where
@@ -145,6 +171,7 @@ structure MessageDesc where
   since : Nat
   deprecatedSince : Option Nat
   arguments : Array ArgumentDesc
+  rawArguments : Array Raw.ArgumentDesc
   deriving Repr, BEq, Inhabited
 
 inductive ReturnType where