lens composition

2 files changed, 22 insertions, 15 deletions

diff --git a/lib/Wayland/Basic/Lens.lean b/lib/Wayland/Basic/Lens.lean
index 16de458..ee1e486 100644
--- a/lib/Wayland/Basic/Lens.lean
+++ b/lib/Wayland/Basic/Lens.lean
@@ -13,6 +13,16 @@ structure Lens (O I : Type) where
   /-- Update the outer structure to contain the updated substructure. -/
   set : I → O → O
 
+def Lens.id (X : Type) : Lens X X where
+  get x := x
+  set x _ := x
+
+def Lens.compose {X Y Z : Type} (l₁ : Lens X Y) (l₂ : Lens Y Z) : Lens X Z where
+  get := l₂.get ∘ l₁.get
+  set i o := l₁.set (l₂.set i (l₁.get o)) o
+
+scoped infixr:80 " ≫ " => Lens.compose
+
 /-- 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 #[]]
diff --git a/src/Waylean.lean b/src/Waylean.lean
index e47c6ad..dd43179 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -308,15 +308,14 @@ def initNewSeats (ctx : Context) : DisplayM State Unit := do
   let mods : RiverSeatV1.Modifiers := { mod1 := true }
 
   for s in (← get).seats.values.filter Seat.new do
-    DisplayM.zoom (mk_lens seats) do
-      DisplayM.zoom (Std.HashMap.lens s.proxy) do
-        set (Option.some { s with new := false })
-        Seat.createXkbBinding ctx mods space .spawnFoot
-        Seat.createXkbBinding ctx mods q .close
-        Seat.createXkbBinding ctx mods n .focusNext
-        Seat.createXkbBinding ctx mods esc .exit
-        Seat.createPointerBinding mods btnLeft .move
-        Seat.createPointerBinding mods btnRight .resize
+    DisplayM.zoom (mk_lens seats ≫ Std.HashMap.lens s.proxy) do
+      set (Option.some { s with new := false })
+      Seat.createXkbBinding ctx mods space .spawnFoot
+      Seat.createXkbBinding ctx mods q .close
+      Seat.createXkbBinding ctx mods n .focusNext
+      Seat.createXkbBinding ctx mods esc .exit
+      Seat.createPointerBinding mods btnLeft .move
+      Seat.createPointerBinding mods btnRight .resize
 
 def manageWindows : DisplayM State Unit := do
   let windows ← (← get).windows.mapM fun win ↦ do
@@ -400,15 +399,13 @@ def handle (ctx : Context) : RiverWindowManagerV1.Event → DisplayM State Unit
   | .output proxy => do
       let outputs := (← get).outputs.insert proxy { proxy }
       set { ← get with outputs }
-      DisplayM.zoom (mk_lens outputs) do
-        DisplayM.zoom (Std.HashMap.lens proxy) do
-          proxy.listen handleOutput
+      DisplayM.zoom (mk_lens outputs ≫ Std.HashMap.lens proxy) do
+        proxy.listen handleOutput
   | .seat proxy => do
       let seats := (← get).seats.insert proxy { proxy }
       set { ← get with seats }
-      DisplayM.zoom (mk_lens seats) do
-        DisplayM.zoom (Std.HashMap.lens proxy) do
-          proxy.listen handleSeat
+      DisplayM.zoom (mk_lens seats ≫ Std.HashMap.lens proxy) do
+        proxy.listen handleSeat
 
 def launch : DisplayM State Unit := do
   _ ← DisplayM.registerSignal .SIGINT do