diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Wayland.lean | 1 | ||||
| -rw-r--r-- | lib/Wayland/Display.lean | 5 | ||||
| -rw-r--r-- | lib/Wayland/Helpers.lean | 15 |
3 files changed, 18 insertions, 3 deletions
diff --git a/lib/Wayland.lean b/lib/Wayland.lean index c9a06fa..5f78211 100644 --- a/lib/Wayland.lean +++ b/lib/Wayland.lean @@ -4,3 +4,4 @@ import Wayland.Basic.PosixSignal import Wayland.Basic.Lens import Wayland.Display import Wayland.Protocols +import Wayland.Helpers diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 9ba60bc..70f5c67 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -101,7 +101,7 @@ class Interface (ι : InterfaceName) where version : UInt32 /-- Interface where all dependency interfaces can be resolvew. -/ -class ResolvedInterface (ι : InterfaceName) where +class ResolvedInterface (ι : InterfaceName) extends Interface ι where referencedInterfaces : Array ((ι' : InterfaceName) × Interface ι') contains_self : ∃ α, ⟨ι, α⟩ ∈ referencedInterfaces := by exists inferInstance; simp -- TODO: Verify that dependencies of interfaces are in referencedInterfaces @@ -367,8 +367,7 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter events := iface'.events.map MessageDesc.toNative } (setComplete := if ι' == ι then 1 else 0) -/-- Get the `wl_display` instance within the display monad. -/ -def DisplayM.getDisplay : DisplayM σ (Object "wl_display") := do +def DisplayM.getDisplay' : DisplayM σ (Object "wl_display") := do let proxy ← Native.Proxy.fromDisplay (← read).disp return ⟨proxy⟩ diff --git a/lib/Wayland/Helpers.lean b/lib/Wayland/Helpers.lean new file mode 100644 index 0000000..7230fc2 --- /dev/null +++ b/lib/Wayland/Helpers.lean @@ -0,0 +1,15 @@ +import Wayland.Display +import Wayland.Protocols + +-- Helpers that depend on the protocols and can thus not be included in `Display.lean`. + +namespace Wayland + +open Protocols + +variable {σ : Type} + +/-- Get the `wl_display` instance within the display monad. -/ +def DisplayM.getDisplay : DisplayM σ WlDisplay := getDisplay' + +end Wayland |