diff options
| -rw-r--r-- | lib/Wayland.lean | 3 | ||||
| -rw-r--r-- | lib/Wayland/Basic/Duration.lean | 26 | ||||
| -rw-r--r-- | lib/Wayland/Basic/Lens.lean | 22 | ||||
| -rw-r--r-- | lib/Wayland/Basic/PosixSignal.lean | 23 | ||||
| -rw-r--r-- | lib/Wayland/Display.lean | 99 | ||||
| -rw-r--r-- | lib/Wayland/Native.lean | 38 |
6 files changed, 150 insertions, 61 deletions
diff --git a/lib/Wayland.lean b/lib/Wayland.lean index 8dd49c8..f3781ec 100644 --- a/lib/Wayland.lean +++ b/lib/Wayland.lean @@ -1,2 +1,5 @@ import Wayland.Native +import Wayland.Basic.Duration +import Wayland.Basic.PosixSignal +import Wayland.Basic.Lens import Wayland.Display diff --git a/lib/Wayland/Basic/Duration.lean b/lib/Wayland/Basic/Duration.lean new file mode 100644 index 0000000..5212ff0 --- /dev/null +++ b/lib/Wayland/Basic/Duration.lean @@ -0,0 +1,26 @@ +/-! +# Time Durations + +This interface abstracts the unit of time duration values. +-/ + +namespace Wayland + +/-- A duration value. -/ +structure Duration where + private milliseconds : UInt32 + deriving Repr, BEq, Inhabited + +def Duration.ofMilliseconds (val : UInt32) : Duration := ⟨val⟩ +def Duration.ofSeconds (val : UInt32) : Duration := .ofMilliseconds (val * 1000) +def Duration.ofMinutes (val : UInt32) : Duration := .ofSeconds (val * 60) + +def Duration.toMilliseconds (val : Duration) : UInt32 := val.milliseconds +def Duration.toSeconds (val : Duration) : UInt32 := val.toMilliseconds / 1000 +def Duration.toMinutes (val : Duration) : UInt32 := val.toSeconds / 60 + +notation:2000 val "ms" => Duration.ofMilliseconds val +notation:2000 val "sec" => Duration.ofSeconds val +notation:2000 val "min" => Duration.ofMinutes val + +end Wayland diff --git a/lib/Wayland/Basic/Lens.lean b/lib/Wayland/Basic/Lens.lean new file mode 100644 index 0000000..16de458 --- /dev/null +++ b/lib/Wayland/Basic/Lens.lean @@ -0,0 +1,22 @@ +/-! +# Lenses + +A `Lens` bundles a getter and an (updating) setter which can be used to elegantly describe a field of a structure. +-/ + +namespace Wayland + +/-- A lens that points into a substructure of type `I` within a structure of type `O`. -/ +structure Lens (O I : Type) where + /-- Get the substructure from the outer structure. -/ + get : O → I + /-- Update the outer structure to contain the updated substructure. -/ + set : I → O → O + +/-- Helper for writing a `Lens` constructor for a named field of a structure. -/ +macro "mk_lens " field:ident : term => do + let lvalNode := Lean.mkNode `Lean.Parser.Term.structInstLVal #[field.raw, Lean.mkNullNode #[]] + let lval : Lean.TSyntax `Lean.Parser.Term.structInstLVal := ⟨lvalNode⟩ + `({ get := fun x => x.$field, set := fun i x => { x with $lval := i } }) + +end Wayland diff --git a/lib/Wayland/Basic/PosixSignal.lean b/lib/Wayland/Basic/PosixSignal.lean new file mode 100644 index 0000000..45c7361 --- /dev/null +++ b/lib/Wayland/Basic/PosixSignal.lean @@ -0,0 +1,23 @@ +import Wayland.Native + +/-! +# POSIX Signals + +Data type representing a POSIX signal number. +-/ + +namespace Wayland + +/-- A POSIX signal number. -/ +structure PosixSignal where + signum : UInt32 + deriving Repr, BEq, Inhabited + +/-- The SIGINT (interrupted) signal. -/ +def PosixSignal.SIGINT : PosixSignal := ⟨Native.SIGINT ()⟩ +/-- The SIGUSR1 (first user-defined) signal. -/ +def PosixSignal.SIGUSR1 : PosixSignal := ⟨Native.SIGUSR1 ()⟩ +/-- The SIGUSR2 (second user-defined) signal. -/ +def PosixSignal.SIGUSR2 : PosixSignal := ⟨Native.SIGUSR2 ()⟩ + +end Wayland diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 18a05fa..7c628f3 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -1,53 +1,38 @@ import Wayland.Native +import Wayland.Basic.PosixSignal +import Wayland.Basic.Duration +import Wayland.Basic.Lens -namespace Wayland - -def EventSource := Native.EventSource - -structure PosixSignal where - private signum : UInt32 - deriving Repr, BEq, Inhabited - -def PosixSignal.SIGINT : PosixSignal := ⟨Native.SIGINT⟩ -def PosixSignal.SIGUSR1 : PosixSignal := ⟨Native.SIGUSR1⟩ -def PosixSignal.SIGUSR2 : PosixSignal := ⟨Native.SIGUSR2⟩ - -structure Duration where - private milliseconds : UInt32 - deriving Repr, BEq, Inhabited +/-! +# The Display Monad -def Duration.ofMilliseconds (val : UInt32) : Duration := ⟨val⟩ -def Duration.ofSeconds (val : UInt32) : Duration := .ofMilliseconds (val * 1000) -def Duration.ofMinutes (val : UInt32) : Duration := .ofSeconds (val * 60) +All event handlers and effectful code is run within the `DisplayM` monad, which encapsulates the connection to a +Wayland server. Its main purpose is managing its event loop -- processing timers, signal handlers, and Wayland events. +Furthermore, it manages a global state `σ` and allows focussing on a relevant part of that state using +lenses. +-/ -def Duration.toMilliseconds (val : Duration) : UInt32 := val.milliseconds -def Duration.toSeconds (val : Duration) : UInt32 := val.toMilliseconds / 1000 -def Duration.toMinutes (val : Duration) : UInt32 := val.toSeconds / 60 - -notation:2000 val "ms" => Duration.ofMilliseconds val -notation:2000 val "sec" => Duration.ofSeconds val -notation:2000 val "min" => Duration.ofMinutes val +variable {σ α : Type} -structure Lens (O I : Type) where - get : O → I - set : I → O → O +namespace Wayland -macro "mk_lens " field:ident : term => do - let lvalNode := Lean.mkNode `Lean.Parser.Term.structInstLVal #[field.raw, Lean.mkNullNode #[]] - let lval : Lean.TSyntax `Lean.Parser.Term.structInstLVal := ⟨lvalNode⟩ - `({ get := fun x => x.$field, set := fun i x => { x with $lval := i } }) +/-- 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 -abbrev Handler (σ : Type) := StateT σ IO Unit +/-- Internal handler interface passed as a message to the event loop. -/ +private abbrev Handler (σ : Type) := StateT σ IO Unit +/-- Access to the display and event loop, providing the main functionality. -/ structure Display (σ : Type) where - disp : Native.Display - addTimer : (delayMs : UInt32) → (msg : Handler σ) → IO EventSource - addSignal : (signum : UInt32) → (msg : Handler σ) → IO EventSource - remove : (source : EventSource) → IO Unit - quit : IO Unit - -variable {σ α : Type} + private disp : Native.Display + private addTimer : (delayMs : UInt32) → (msg : Handler σ) → IO EventSource + private addSignal : (signum : UInt32) → (msg : Handler σ) → IO EventSource + private remove : (source : EventSource) → IO Unit + private quit : IO Unit +/-- The display monad: A monad extending the `IO` monad with Wayland display related operations as well as state +management for a state type σ. -/ def DisplayM (σ : Type) : Type → Type := ReaderT (Display σ) (StateT σ IO) @@ -57,6 +42,12 @@ deriving instance MonadState σ for DisplayM σ private instance : MonadLift (ReaderT (Display σ) (StateT σ IO)) (DisplayM σ) where monadLift := id +/-- Connect to a Wayland server and start the application's main loop. + +Parameters: +· `setUp`: Executed on startup before launching the event loop. +· `initialState`: The initial state value within the monad. +· `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 loop ← Native.EventLoop.new @@ -76,23 +67,48 @@ partial def DisplayM.run' (setUp : DisplayM σ Unit) (initialState : σ) (name : inner main.run initialState |>.map Prod.snd +/-- Connect to a Wayland server and start the application's main loop. + +Parameters: +· `setUp`: Executed on startup before launching the event loop. +· `initialState`: The initial state value within the monad. +· `name`: Socket name for connecting to the Wayland server (by default, `wayland-0` is used). -/ def DisplayM.run (setUp : DisplayM σ Unit) (initialState : σ) (name : Option String := .none) : IO Unit := DisplayM.run' setUp initialState (name := name) |> discard +/-- Lift an `IO` operation into the Display monad. + +Note that `DisplayM` does not provide an instance for `MonadLift IO` to make access to `IO` more explicit. This should +not be used often. -/ def DisplayM.liftIO (io : IO α) : DisplayM σ α := io +/-- Request the application to stop processing events and exit the event loop. + +This can be sent at any time and stops the event loop before any further events can be processed. -/ def DisplayM.requestQuit : DisplayM σ Unit := do (← read).quit +/-- Register a (POSIX) signal handler. + +When the given `signal` is caught, the `handler` is executed as a part of the event loop. The returned event source can +be used to unregister the handler. -/ def DisplayM.registerSignal (signal : PosixSignal) (handler : DisplayM σ Unit) : DisplayM σ EventSource := do let global ← read global.addSignal signal.signum (ReaderT.run handler global) +/-- Register a (one-shot) timer. + +After the given `timeout`, the `handler` is executed as a part of the event loop. The returned event source can be used +to cancel the timer. -/ def DisplayM.registerTimer (timeout : Duration) (handler : DisplayM σ Unit) : DisplayM σ EventSource := do let global ← read global.addTimer timeout.toMilliseconds (ReaderT.run handler global) +/-- Unregister a previously registered event source. + +If the handler is currently active, it will run to completion, but the event is no longer processed as a part of the +event loop. -/ def DisplayM.unregister (source : EventSource) : DisplayM σ Unit := do (← read).remove source @@ -102,6 +118,9 @@ private def zoomState {σ₁ σ₂ : Type} {m : Type → Type} [Monad m] (lens : set (lens.set newInner oldOuter) return res +/-- Zoom into a specific part of the state using a lens. + +This is possible because handlers can only ever be submitted in the `DisplayM` monad, but never retrieved. -/ def DisplayM.zoom {σ₁ σ₂ : Type} (lens : Lens σ₁ σ₂) (inner : DisplayM σ₂ α) : DisplayM σ₁ α := do let global₁ : Display σ₁ ← read let global₂ : Display σ₂ := diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index 95d1739..bd85291 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -1,21 +1,27 @@ +variable {M : Type} + namespace Wayland.Native +private opaque DisplayP : NonemptyType +private opaque EventLoopP (M : Type) : NonemptyType +private opaque EventSourceP : NonemptyType + +def Display : Type := DisplayP.type +def EventLoop (M : Type) : Type := (EventLoopP M).type +def EventSource : Type := EventSourceP.type + +instance : Nonempty Display := DisplayP.property +instance : Nonempty (EventLoop M) := (EventLoopP M).property +instance : Nonempty EventSource := EventSourceP.property + @[extern "waylean_SIGINT"] -private opaque _SIGINT (u : Unit) : UInt32 +opaque SIGINT (u : Unit) : UInt32 @[extern "waylean_SIGUSR1"] -private opaque _SIGUSR1 (u : Unit) : UInt32 +opaque SIGUSR1 (u : Unit) : UInt32 @[extern "waylean_SIGUSR2"] -private opaque _SIGUSR2 (u : Unit) : UInt32 - -def SIGINT: UInt32 := _SIGINT () -def SIGUSR1: UInt32 := _SIGUSR1 () -def SIGUSR2: UInt32 := _SIGUSR2 () - -private opaque DisplayP : NonemptyType -def Display : Type := DisplayP.type -instance : Nonempty Display := DisplayP.property +opaque SIGUSR2 (u : Unit) : UInt32 @[extern "waylean_display_new"] opaque Display.new : (name : @& Option String) → IO Display @@ -23,16 +29,6 @@ opaque Display.new : (name : @& Option String) → IO Display @[extern "waylean_display_roundtrip"] opaque Display.roundtrip : (display : @& Display) → IO Unit -variable {M : Type} - -private opaque EventLoopP (M : Type) : NonemptyType -def EventLoop (M : Type) : Type := (EventLoopP M).type -instance : Nonempty (EventLoop M) := (EventLoopP M).property - -private opaque EventSourceP : NonemptyType -def EventSource : Type := EventSourceP.type -instance : Nonempty EventSource := EventSourceP.property - @[extern "waylean_event_loop_new"] opaque EventLoop.new : IO (EventLoop M) |