From 1f5491a5af7bd0f1ec4046994d6344886465cba5 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 5 Apr 2026 16:15:03 +0200 Subject: initial codegen --- lib/CWayland/CWayland.cc | 8 ++++++++ lib/CWayland/CWayland.h | 1 + lib/Wayland/Display.lean | 43 ++++++++++++++++++++++++++++++++++--------- lib/Wayland/Native.lean | 3 +++ 4 files changed, 46 insertions(+), 9 deletions(-) (limited to 'lib') 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(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 -- cgit v1.3.1