rework file structure

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)