initial codegen

1 files changed, 34 insertions, 9 deletions

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