/-!
# 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

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 #[]]
  let lval : Lean.TSyntax `Lean.Parser.Term.structInstLVal := ⟨lvalNode⟩
  `({ get := fun x => x.$field, set := fun i x => { x with $lval := i } })

end Wayland