diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/CWayland/CWayland.cc | 14 | ||||
| -rw-r--r-- | lib/CWayland/CWayland.h | 4 | ||||
| -rw-r--r-- | lib/Wayland/Display.lean | 23 | ||||
| -rw-r--r-- | lib/Wayland/Native.lean | 7 | ||||
| -rw-r--r-- | lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean | 28 | ||||
| -rw-r--r-- | lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean | 32 | ||||
| -rw-r--r-- | lib/Wayland/Protocols/Wayland/Header.lean | 38 |
7 files changed, 68 insertions, 78 deletions
diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc index f3c966c..08df50b 100644 --- a/lib/CWayland/CWayland.cc +++ b/lib/CWayland/CWayland.cc @@ -1299,17 +1299,9 @@ lean_obj_res waylean_proxy_get_type(b_lean_obj_arg proxy_obj) return lean_io_result_mk_ok(lean_mk_string(name)); } -// Proxy.isEqual : (x y : @& Proxy) → Bool -lean_obj_res waylean_proxy_is_equal(b_lean_obj_arg x, b_lean_obj_arg y) -{ - auto x_proxy = static_cast<wl_proxy*>(lean_get_external_data(x)); - auto y_proxy = static_cast<wl_proxy*>(lean_get_external_data(y)); - return lean_box(x_proxy == y_proxy ? 1 : 0); -} - -// Proxy.hash : (x : @& Proxy) → UInt64 -lean_obj_res waylean_proxy_hash(b_lean_obj_arg x) +// Proxy.getID : (x : @& Proxy) → IO UInt64 +lean_obj_res waylean_proxy_get_id(b_lean_obj_arg x) { auto proxy = static_cast<wl_proxy*>(lean_get_external_data(x)); - return lean_box_uint64(wl_proxy_get_id(proxy)); + return lean_io_result_mk_ok(lean_box_uint64(wl_proxy_get_id(proxy))); }
\ No newline at end of file diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h index e4a6897..ff71348 100644 --- a/lib/CWayland/CWayland.h +++ b/lib/CWayland/CWayland.h @@ -83,9 +83,7 @@ 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); -lean_obj_res waylean_proxy_is_equal (b_lean_obj_arg x, - b_lean_obj_arg y); -lean_obj_res waylean_proxy_hash (b_lean_obj_arg x); +lean_obj_res waylean_proxy_get_id (b_lean_obj_arg x); #ifdef __cplusplus } diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 3cfa679..d82a951 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -34,12 +34,14 @@ def Fd : Type := Int32 /-- Handle to a client object, possibly dead. -/ structure Object (ι : InterfaceName) : Type where private proxy : Native.Proxy + private id : UInt64 deriving Nonempty /-- Opaque handle to an object whose type is not statically known. -/ structure AnyObject : Type where private proxy : Native.Proxy private type : String + private id : UInt64 deriving Nonempty /-- Monad in which arguments can be marshalled one after another. -/ @@ -278,11 +280,12 @@ private instance : ArgumentDemarshaller (ExceptT String ArgumentBufferM) where demarshalString := do (← read).readString demarshalObject := do let proxy ← (← read).readObject - return proxy.map Object.mk + proxy.mapM fun proxy ↦ do + return ⟨proxy, ← proxy.getID⟩ demarshalAnyObject := do let proxy ← (← read).readObject proxy.mapM fun proxy ↦ do - return ⟨proxy, ← proxy.getType⟩ + return ⟨proxy, ← proxy.getType, ← proxy.getID⟩ demarshalArray := do (← read).readArray demarshalFd := do (← read).readFd @@ -412,21 +415,21 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter def DisplayM.getDisplay' : DisplayM σ (Object "wl_display") := do let proxy ← Native.Proxy.fromDisplay (← read).disp - return ⟨proxy⟩ + return ⟨proxy, ← proxy.getID⟩ variable {ι ι' : InterfaceName} instance : BEq (Object ι) where - beq x y := x.proxy.isEqual y.proxy + beq x y := x.id == y.id instance : Hashable (Object ι) where - hash x := x.proxy.hash + hash x := x.id instance : BEq AnyObject where - beq x y := x.proxy.isEqual y.proxy + beq x y := x.id == y.id instance : Hashable AnyObject where - hash x := x.proxy.hash + hash x := x.id private def marshalArguments (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : IO (Native.ArgumentBuffer × OpCode) := do let argBuffer ← Native.ArgumentBuffer.new @@ -445,7 +448,7 @@ def Object.sendConstructor [iface : ResolvedInterface ι'] (obj : Object ι) (ma let typeMap := (← read).typeMap let (argBuffer, opcode) ← marshalArguments marshaller let proxy ← obj.proxy.sendConstructor opcode argBuffer typeMap ι' - return ⟨proxy⟩ + return ⟨proxy, ← proxy.getID⟩ /-- Listen for events from the server for an object. -/ def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := do @@ -462,11 +465,11 @@ def Object.keep (obj : Object ι) : DisplayM σ Unit := /-- Erase the type information from an object. -/ def Object.toAny (obj : Object ι) : AnyObject := - ⟨obj.proxy, ι⟩ + ⟨obj.proxy, ι, obj.id⟩ /-- 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 + if obj.type == ι then .some ⟨obj.proxy, obj.id⟩ else .none end Proxies diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index 601c709..72b0cf2 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -142,10 +142,7 @@ opaque Proxy.keep : (proxy : @& Proxy) → IO Unit @[extern "waylean_proxy_get_type"] opaque Proxy.getType : (proxy : @& Proxy) → IO String -@[extern "waylean_proxy_is_equal"] -opaque Proxy.isEqual : (x y : @& Proxy) → Bool - -@[extern "waylean_proxy_hash"] -opaque Proxy.hash : (x : @& Proxy) → UInt64 +@[extern "waylean_proxy_get_id"] +opaque Proxy.getID : (x : @& Proxy) → IO UInt64 end Wayland.Native diff --git a/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean b/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean index 3f62b69..48f22dc 100644 --- a/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean +++ b/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean @@ -20,9 +20,9 @@ inductive RiverLibinputDeviceV1.Error where | invalidArg structure RiverLibinputDeviceV1.SendEventsModes where - enabled : Bool - disabled : Bool - disabledOnExternalMouse : Bool + enabled : Bool := false + disabled : Bool := false + disabledOnExternalMouse : Bool := false inductive RiverLibinputDeviceV1.TapState where | disabled @@ -53,10 +53,10 @@ inductive RiverLibinputDeviceV1.AccelProfile where | custom structure RiverLibinputDeviceV1.AccelProfiles where - none : Bool - flat : Bool - adaptive : Bool - custom : Bool + none : Bool := false + flat : Bool := false + adaptive : Bool := false + custom : Bool := false inductive RiverLibinputDeviceV1.NaturalScrollState where | disabled @@ -72,9 +72,9 @@ inductive RiverLibinputDeviceV1.ClickMethod where | clickfinger structure RiverLibinputDeviceV1.ClickMethods where - none : Bool - buttonAreas : Bool - clickfinger : Bool + none : Bool := false + buttonAreas : Bool := false + clickfinger : Bool := false inductive RiverLibinputDeviceV1.ClickfingerButtonMap where | lrm @@ -91,10 +91,10 @@ inductive RiverLibinputDeviceV1.ScrollMethod where | onButtonDown structure RiverLibinputDeviceV1.ScrollMethods where - noScroll : Bool - twoFinger : Bool - edge : Bool - onButtonDown : Bool + noScroll : Bool := false + twoFinger : Bool := false + edge : Bool := false + onButtonDown : Bool := false inductive RiverLibinputDeviceV1.ScrollButtonLockState where | disabled diff --git a/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean b/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean index 4acaf02..4da96e7 100644 --- a/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean +++ b/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean @@ -38,17 +38,17 @@ inductive RiverWindowV1.DecorationHint where | noPreference structure RiverWindowV1.Edges where - none : Bool - top : Bool - bottom : Bool - left : Bool - right : Bool + none : Bool := false + top : Bool := false + bottom : Bool := false + left : Bool := false + right : Bool := false structure RiverWindowV1.Capabilities where - windowMenu : Bool - maximize : Bool - fullscreen : Bool - minimize : Bool + windowMenu : Bool := false + maximize : Bool := false + fullscreen : Bool := false + minimize : Bool := false inductive RiverDecorationV1.Error where | noCommit @@ -65,13 +65,13 @@ inductive RiverOutputV1.PresentationMode where | async structure RiverSeatV1.Modifiers where - none : Bool - shift : Bool - ctrl : Bool - mod1 : Bool - mod3 : Bool - mod4 : Bool - mod5 : Bool + none : Bool := false + shift : Bool := false + ctrl : Bool := false + mod1 : Bool := false + mod3 : Bool := false + mod4 : Bool := false + mod5 : Bool := false namespace RiverWindowManagerV1.Error diff --git a/lib/Wayland/Protocols/Wayland/Header.lean b/lib/Wayland/Protocols/Wayland/Header.lean index a12c0bf..3d7346d 100644 --- a/lib/Wayland/Protocols/Wayland/Header.lean +++ b/lib/Wayland/Protocols/Wayland/Header.lean @@ -201,27 +201,27 @@ inductive WlDataDevice.Error where | usedSource structure WlDataDeviceManager.DndAction where - none : Bool - copy : Bool - move : Bool - ask : Bool + none : Bool := false + copy : Bool := false + move : Bool := false + ask : Bool := false inductive WlShell.Error where | role structure WlShellSurface.Resize where - none : Bool - top : Bool - bottom : Bool - left : Bool - topLeft : Bool - bottomLeft : Bool - right : Bool - topRight : Bool - bottomRight : Bool + none : Bool := false + top : Bool := false + bottom : Bool := false + left : Bool := false + topLeft : Bool := false + bottomLeft : Bool := false + right : Bool := false + topRight : Bool := false + bottomRight : Bool := false structure WlShellSurface.Transient where - inactive : Bool + inactive : Bool := false inductive WlShellSurface.FullscreenMethod where | default @@ -237,9 +237,9 @@ inductive WlSurface.Error where | defunctRoleObject structure WlSeat.Capability where - pointer : Bool - keyboard : Bool - touch : Bool + pointer : Bool := false + keyboard : Bool := false + touch : Bool := false inductive WlSeat.Error where | missingCapability @@ -293,8 +293,8 @@ inductive WlOutput.Transform where | flipped270 structure WlOutput.Mode where - current : Bool - preferred : Bool + current : Bool := false + preferred : Bool := false inductive WlSubcompositor.Error where | badSurface |