summaryrefslogtreecommitdiff
path: root/lib/Wayland
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Wayland')
-rw-r--r--lib/Wayland/Display.lean134
-rw-r--r--lib/Wayland/Native.lean23
-rw-r--r--lib/Wayland/Object.lean98
3 files changed, 157 insertions, 98 deletions
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 7c628f3..76e5b7d 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -16,9 +16,99 @@ variable {σ α : Type}
namespace Wayland
+section Interfaces
+
+/-- The name of an interface (e.g., `"wl_display"`), commonly used to resolve the corresponding interface description
+using the `Interface` class. -/
+def InterfaceName : Type := String
+ deriving Repr, Nonempty, BEq, ToString
+
+/-- The numeric identifier of a request/event in an interface. -/
+def OpCode : Type := UInt32
+ deriving Repr, Nonempty, BEq, OfNat
+
+/-- Handle to a client object, possibly dead. -/
+structure Object (ι : InterfaceName) where
+
+/-- Monad in which arguments can be marshalled one after another. -/
+class ArgumentMarshaller (m : Type → Type) extends Monad m where
+ marshalInt : Int32 → m Unit
+ marshalUInt : UInt32 → m Unit
+ marshalFixed : Float32 → m Unit
+ marshalString : Option String → m Unit
+ marshalObject {ι : InterfaceName} : Option (Object ι) → m Unit
+ marshalNewID {ι : InterfaceName} : Object ι → m Unit
+ marshalArray : ByteArray → m Unit
+ marshalFD : Int32 → m Unit
+
+/-- Monad in which arguments can be demarshalled one after another. -/
+class ArgumentDemarshaller (m : Type → Type) extends Monad m where
+ demarshalInt : m Int32
+ demarshalUInt : m UInt32
+ demarshalFixed : m Float32
+ demarshalString : m (Option String)
+ demarshalObject {ι : InterfaceName} : m (Option (Object ι))
+ demarshalNewID {ι : InterfaceName} : m (Object ι)
+ demarshalArray : m ByteArray
+ demarshalFD : m Int32
+
+/-- Nullability annotation in an interface's message. -/
+inductive Nullability where
+ | nullable
+ | notNull
+
+/-- Argument description in an interface's message. -/
+inductive ArgumentDesc where
+ | int : ArgumentDesc
+ | uint : ArgumentDesc
+ | fixed : ArgumentDesc
+ | string : Nullability → ArgumentDesc
+ | object : Nullability → InterfaceName → ArgumentDesc
+ | newID : InterfaceName → ArgumentDesc
+ | array : ArgumentDesc
+ | fd : ArgumentDesc
+
+/-- Message description for an interface. -/
+structure MessageDesc where
+ name : String
+ args : Array ArgumentDesc
+ since : UInt32
+ isDestructor : Bool
+
+/-- Class for types describing the request messages of an interface. -/
+class Request (α : Type) where
+ messages : Array MessageDesc
+ signature : α → MessageDesc
+ marshal {m : Type → Type} [ArgumentMarshaller m] : α → m OpCode
+
+/-- Class for types describing the event messages of an interface. -/
+class Event (α : Type) where
+ messages : Array MessageDesc
+ signature : α → MessageDesc
+ demarshal {m : Type → Type} [ArgumentDemarshaller m] : OpCode → m α
+
+/-- Class describing an interface. This is not associated with a type, but rather with the interface's name. -/
+class Interface (ι : InterfaceName) where
+ request : Type
+ [requestClass : Request request]
+ event : Type
+ [eventClass : Event event]
+ version : UInt32
+
+/-- Interface where all dependent interfaces can be resolvew. -/
+class ResolvedInterface (ι : InterfaceName) where
+ referencedInterfaces : Array ((ι' : InterfaceName) × Interface ι')
+ contains_self : ∃ α, ⟨ι, α⟩ ∈ referencedInterfaces := by exists inferInstance; simp
+ -- TODO: Verify that dependencies of interfaces are in referencedInterfaces
+
+end Interfaces
+
+section DisplayMonad
+
/-- A token managing a single source of events such as a timer or a signal handler. This can be used to unregister the
event. -/
def EventSource : Type := Native.EventSource
+ deriving Nonempty
/-- Internal handler interface passed as a message to the event loop. -/
private abbrev Handler (σ : Type) := StateT σ IO Unit
@@ -26,6 +116,7 @@ private abbrev Handler (σ : Type) := StateT σ IO Unit
/-- Access to the display and event loop, providing the main functionality. -/
structure Display (σ : Type) where
private disp : Native.Display
+ private typeMap : Native.TypeMap
private addTimer : (delayMs : UInt32) → (msg : Handler σ) → IO EventSource
private addSignal : (signum : UInt32) → (msg : Handler σ) → IO EventSource
private remove : (source : EventSource) → IO Unit
@@ -50,10 +141,12 @@ Parameters:
· `name`: Socket name for connecting to the Wayland server (by default, `wayland-0` is used). -/
partial def DisplayM.run' (setUp : DisplayM σ Unit) (initialState : σ) (name : Option String := .none) : IO σ := do
let disp ← Native.Display.new name
+ let typeMap ← Native.TypeMap.new
let loop ← Native.EventLoop.new
_ ← loop.addDisplay disp
let global : Display σ :=
{ disp := disp
+ typeMap := typeMap
addTimer := loop.addTimer
addSignal := loop.addSignal
remove := loop.remove
@@ -125,10 +218,51 @@ def DisplayM.zoom {σ₁ σ₂ : Type} (lens : Lens σ₁ σ₂) (inner : Displa
let global₁ : Display σ₁ ← read
let global₂ : Display σ₂ :=
{ disp := global₁.disp
+ typeMap := global₁.typeMap
addTimer := fun x y ↦ global₁.addTimer x (zoomState lens y)
addSignal := fun x y ↦ global₁.addSignal x (zoomState lens y)
remove := global₁.remove
quit := global₁.quit }
zoomState lens (ReaderT.run inner global₂)
+end DisplayMonad
+
+section Proxies
+
+private def MessageDesc.toNative (msg : MessageDesc) : Native.Message :=
+ let argString : ArgumentDesc → String
+ | .int => "i"
+ | .uint => "u"
+ | .fixed => "f"
+ | .string .nullable => "?s"
+ | .string .notNull => "s"
+ | .object .nullable _ => "?o"
+ | .object .notNull _ => "o"
+ | .newID _ => "n"
+ | .array => "a"
+ | .fd => "h"
+ let argType : ArgumentDesc → Option String
+ | .object _ iface => .some iface
+ | .newID iface => .some iface
+ | _ => .none
+ { name := msg.name
+ signature := s!"{msg.since}{String.join (msg.args.toList.map argString)}"
+ types := msg.args.map argType }
+
+private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInterface ι] : DisplayM σ Unit := do
+ let typeMap := (← read).typeMap
+ for ⟨ι', iface'⟩ in iface.referencedInterfaces do
+ if !(← typeMap.contains ι') then
+ typeMap.register
+ { name := ι'
+ version := iface'.version
+ requests := iface'.requestClass.messages.map MessageDesc.toNative
+ events := iface'.eventClass.messages.map MessageDesc.toNative }
+
+
+-- def Object.send [iface : Interface ι] (obj : Object ι) (req : iface.request) : DisplayM σ Unit := sorry
+-- def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := sorry
+
+end Proxies
+
end Wayland
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index bd85291..e695e5f 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -2,17 +2,31 @@ variable {M : Type}
namespace Wayland.Native
+structure Message where
+ name : String
+ signature : String
+ types : Array (Option String)
+
+structure Interface where
+ name : String
+ version : UInt32
+ requests : Array Message
+ events : Array Message
+
private opaque DisplayP : NonemptyType
private opaque EventLoopP (M : Type) : NonemptyType
private opaque EventSourceP : NonemptyType
+private opaque TypeMapP : NonemptyType
def Display : Type := DisplayP.type
def EventLoop (M : Type) : Type := (EventLoopP M).type
def EventSource : Type := EventSourceP.type
+def TypeMap : Type := TypeMapP.type
instance : Nonempty Display := DisplayP.property
instance : Nonempty (EventLoop M) := (EventLoopP M).property
instance : Nonempty EventSource := EventSourceP.property
+instance : Nonempty TypeMap := TypeMapP.property
@[extern "waylean_SIGINT"]
opaque SIGINT (u : Unit) : UInt32
@@ -50,4 +64,13 @@ opaque EventLoop.quit : (eventLoop : @& (EventLoop M)) → IO Unit
@[extern "waylean_event_loop_poll"]
opaque EventLoop.poll : (eventLoop : @& (EventLoop M)) → IO (Option M)
+@[extern "waylean_type_map_new"]
+opaque TypeMap.new : IO TypeMap
+
+@[extern "waylean_type_map_contains"]
+opaque TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Bool
+
+@[extern "waylean_type_map_register"]
+opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit
+
end Wayland.Native
diff --git a/lib/Wayland/Object.lean b/lib/Wayland/Object.lean
deleted file mode 100644
index 6c5dbb7..0000000
--- a/lib/Wayland/Object.lean
+++ /dev/null
@@ -1,98 +0,0 @@
-import Wayland.Display
-
-namespace Wayland
-
-def InterfaceName : Type := String
- deriving Repr, BEq
-
-def OpCode : Type := UInt32
- deriving Repr, BEq
-
-structure Object (ι : InterfaceName) where
-
-structure NewID (ι : InterfaceName) where
-
-class ArgumentMarshaller (m : Type → Type) extends Monad m where
- marshalInt : Int32 → m Unit
- marshalUInt : UInt32 → m Unit
- marshalFixed : Float32 → m Unit
- marshalString : Option String → m Unit
- marshalObject {ι : InterfaceName} : Option (Object ι) → m Unit
- marshalNewID {ι : InterfaceName} : NewID ι → m Unit
- marshalArray : ByteArray → m Unit
- marshalFD : Int32 → m Unit
-
-class ArgumentDemarshaller (m : Type → Type) extends Monad m where
- demarshalInt : m Int32
- demarshalUInt : m UInt32
- demarshalFixed : m Float32
- demarshalString : m (Option String)
- demarshalObject {ι : InterfaceName} : m (Option (Object ι))
- demarshalNewID {ι : InterfaceName} : m (NewID ι)
- demarshalArray : m ByteArray
- demarshalFD : m Int32
-
-inductive Nullability where
- | nullable
- | notNull
-
-inductive Argument where
- | int : Argument
- | uint : Argument
- | fixed : Argument
- | string : Nullability → Argument
- | object : Nullability → InterfaceName → Argument
- | newID : InterfaceName → Argument
- | array : Argument
- | fd : Argument
-
-structure Message where
- name : String
- args : Array Argument
- since : UInt32
- isDestructor : Bool
-
-class Request (α : Type) where
- messages : Array Message
- signature : α → Message
- marshal {m : Type → Type} [ArgumentMarshaller m] : α → m OpCode
-
-class Event (α : Type) where
- messages : Array Message
- signature : α → Message
- demarshal {m : Type → Type} [ArgumentDemarshaller m] : OpCode → m α
-
-class Interface (ι : InterfaceName) where
- request : Type
- [requestClass : Request request]
- event : Type
- [eventClass : Event event]
- version : UInt32
-
-variable {σ : Type} {ι : InterfaceName}
-
-def Object.send [iface : Interface ι] (obj : Object ι) (req : iface.request) : DisplayM σ Unit := sorry
-def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := sorry
-
--- def WLDisplay.name : InterfaceName := "wl_display"
--- abbrev WLDisplay : Type := Object WLDisplay.name
-
--- inductive WLDisplay.Request where
--- | sync : Request
-
--- inductive WLDisplay.Event where
--- | error : Event
-
--- instance : Request WLDisplay.Request := sorry
--- instance : Event WLDisplay.Event := sorry
--- instance : Interface WLDisplay.name where
--- request := WLDisplay.Request
--- event := WLDisplay.Event
--- version := 1
-
--- def test (disp : WLDisplay) : DisplayM σ Unit := do
--- disp.listen fun
--- | .error => DisplayM.liftIO (IO.println "error!")
--- disp.send .sync
-
-end Wayland
generated by cgit v1.3.1 (git 2.54.0) at 2026-11-10 15:20:34 +0000