Lens-like notation

Stream: lean4

[Jovan Gerbscheid]

Would it be possible to add a notation for updating a field structure? I often find myself with code like this:

withReader (fun c => { c with fvars := fvar :: c.fvars })

And I would much prefer something like

withReader (fvars %~ (fvar :: ·))

I don't mind what the syntax exactly looks like, but something like this would make code a lot cleaner.
For example in Haskell, this notation is possible using lenses, so maybe some of those features could be reproduced in lean.
Here's my simple attempt:

syntax ident "%~" : term
syntax ident "%~" term : term
macro_rules
| `($n:ident %~ $f $x) => `({ $x with $n:ident := $f $x.$n })
| `($n:ident %~ $f) => `(fun x => { x with $n:ident := $f x.$n })
| `($n:ident %~) => `(fun f x => { x with $n:ident := f x.$n })

#eval fst %~ (· + 1) (1,3) -- (2,3)

[Alex J. Best]

There was some work on lenses / optics in #282, which takes the approach of deriving with and modify functions rather than adding notation

[Jovan Gerbscheid]

I suppose the advantage of a notation is that you can use it on all data types since you don't have to explicitly derive_optics

[Jovan Gerbscheid]

Here's a version of the notation that works a bit better:

syntax term "%." noWs ident term:max : term

macro_rules
| `($struct %.$field:ident $f) => `({ $struct with $field:ident := $f $struct.$field })

variable (x : Nat × Nat × Nat)

#check x %.fst fun x => x + 1
#check x %.snd.snd (· + 1) %.fst (· + 1)

[Jovan Gerbscheid]

And, in do notation with mutable variables:

syntax ident ":=." noWs ident term : doElem

macro_rules
| `(doElem| $var:ident :=.$field:ident $f) => `(doElem| $var:ident := $var %.$field $f)

def foo : Id Nat := do
  let mut a : Nat × Nat := (100,1)
  a :=.fst (· + 1)
  return a.fst

#eval foo -- 101

[Anand Rao Tadipatri]

And here's syntax for modifying a mutable element in do notation (the previous message is specifically about modifying structure field, this is for any mutable variable):

syntax ident ":>" term : doElem

macro_rules
| `(doElem| $var:ident :> $f) => `(doElem| $var:ident := $f $var)