display monad

1 files changed, 115 insertions, 0 deletions

diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
new file mode 100644
index 0000000..18a05fa
--- /dev/null
+++ b/lib/Wayland/Display.lean
@@ -0,0 +1,115 @@
+import Wayland.Native
+
+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
+
+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
+
+structure Lens (O I : Type) where
+  get : O → I
+  set : I → O → O
+
+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 } })
+
+abbrev Handler (σ : Type) := StateT σ IO Unit
+
+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}
+
+def DisplayM (σ : Type) : Type → Type :=
+  ReaderT (Display σ) (StateT σ IO)
+
+deriving instance Monad for DisplayM σ
+deriving instance MonadState σ for DisplayM σ
+
+private instance : MonadLift (ReaderT (Display σ) (StateT σ IO)) (DisplayM σ) where
+  monadLift := id
+
+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
+  _ ← loop.addDisplay disp
+  let global : Display σ :=
+    { disp := disp
+      addTimer := loop.addTimer
+      addSignal := loop.addSignal
+      remove := loop.remove
+      quit := loop.quit }
+  let rec inner : StateT σ IO Unit := do
+    match (← loop.poll) with
+    | .none => return
+    | .some msg => msg; inner
+  let main : StateT σ IO Unit := do
+    setUp.run global
+    inner
+  main.run initialState |>.map Prod.snd
+
+def DisplayM.run (setUp : DisplayM σ Unit) (initialState : σ) (name : Option String := .none) : IO Unit :=
+  DisplayM.run' setUp initialState (name := name) |> discard
+
+def DisplayM.liftIO (io : IO α) : DisplayM σ α :=
+  io
+
+def DisplayM.requestQuit : DisplayM σ Unit := do
+  (← read).quit
+
+def DisplayM.registerSignal (signal : PosixSignal) (handler : DisplayM σ Unit) : DisplayM σ EventSource := do
+  let global ← read
+  global.addSignal signal.signum (ReaderT.run handler global)
+
+def DisplayM.registerTimer (timeout : Duration) (handler : DisplayM σ Unit) : DisplayM σ EventSource := do
+  let global ← read
+  global.addTimer timeout.toMilliseconds (ReaderT.run handler global)
+
+def DisplayM.unregister (source : EventSource) : DisplayM σ Unit := do
+  (← read).remove source
+
+private def zoomState {σ₁ σ₂ : Type} {m : Type → Type} [Monad m] (lens : Lens σ₁ σ₂) (inner : StateT σ₂ m α) : StateT σ₁ m α := do
+  let oldOuter ← get
+  let (res, newInner) ← inner.run (lens.get oldOuter)
+  set (lens.set newInner oldOuter)
+  return res
+
+def DisplayM.zoom {σ₁ σ₂ : Type} (lens : Lens σ₁ σ₂) (inner : DisplayM σ₂ α) : DisplayM σ₁ α := do
+  let global₁ : Display σ₁ ← read
+  let global₂ : Display σ₂ :=
+    { disp := global₁.disp
+      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 Wayland