blob: 26455bbe2f6a7d8487c28fc61f3bf4875209f149 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
import Std.Data.HashMap
/-!
# 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
/-- A lens into a hash-map, either containing .none or the value associated with the key. -/
def Std.HashMap.lens {α β : Type} [BEq α] [Hashable α] (key : α) : Wayland.Lens (Std.HashMap α β) (Option β) where
get x := x.get? key
set v x := x.alter key fun _ ↦ v
|
