diff options
Diffstat (limited to 'lib/Wayland/Basic/Lens.lean')
| -rw-r--r-- | lib/Wayland/Basic/Lens.lean | 22 |
1 files changed, 22 insertions, 0 deletions
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 |