## Stream: PR reviews

### Topic: lean#260 expr lens

#### Gabriel Ebner (May 21 2020 at 18:26):

Do we already have something like this? Other opinions?

#### Johan Commelin (May 21 2020 at 18:39):

Didn't @Keeley Hoek write some sort of expr lens recently for the nth_rewrite tactic?

#### Scott Morrison (May 22 2020 at 01:47):

(I think this is actually a survivor from my work on rewrite_search, even pre-Keeley!)

#### Scott Morrison (May 22 2020 at 01:48):

I've only looked enough to see that they are not exactly the same, and I sort of doubt it's going to be easy to make something usable in both situations, but I didn't really try to understand @Edward Ayers' version.

#### Johan Commelin (May 22 2020 at 04:36):

@Scott Morrison Oops, sorry for misattributing

#### Edward Ayers (May 22 2020 at 09:05):

Hi gang, thanks for the interest!
I added a better set of comments to the PR which I will paste here:

One of the features of the widgets PR is that the lean pretty printer has been modified so that it also tags certain positions in the formatted expression with information about which subexpression of the original expression generated a pariticular part of the pretty printed string. This allows all of the highlighting and lookup of implicit arguments etc in the widget view.

The main thing it introduces is expr.coord which is an enum of labels for each recursive constructor argument in expr. Then an expr.address is simply a list of these coordinates. In this way you can reference subexpressions.

It could also be used to implement lenses (or maybe prisms?) on expressions, that is one could implement

meta def expr.lens {t} [alternative t] : expr.address → (expr → t expr) → (expr → t expr)


which runs the given function on the subexpression and then repackages it.
I didn't include it because I wanted to include in this PR only the minimum amount of stuff that was needed to get to the stage where I had the datatypes and some helper functions for the modified pretty printer.
If people think it doesn't bloat core too much I am happy to include an implementation for the other lensy things.

I also have an implementation of expression zippers in a different project if anyone is interested in that.

#### Edward Ayers (May 22 2020 at 09:09):

Afaict it's different to Scott's lenses because it includes support for the various binders and also it doesn't include the path construct (I have written a binder-ful version of path elsewhere) for implementing expr zippers. expr.address is just a list of enums that can be used to find a subexpression.

#### Edward Ayers (May 22 2020 at 09:15):

The other issue is that this file expr_address.lean has to be in init before tactic.show_info is declared.

#### Edward Ayers (May 22 2020 at 09:16):

So you can't use interactive tactics to derive things

#### Scott Morrison (May 22 2020 at 09:29):

All sounds good to me. I don't think there's much code-duplication-worry to be concerned about here at this stage, and we are all excited to get widgets asap. :-)

#### Patrick Massot (May 22 2020 at 09:40):

I vote for widgets asap because I have a propaganda talk scheduled for June 3rd.

#### Keeley Hoek (May 22 2020 at 15:34):

Indeed, that code is Scott's and I have merely performed an obfuscation pass or two (hence might have seized control of the git blame). Anyway, how is "lens" a name you both came up with!? (or is this common nomenclature? =O)

#### Patrick Massot (May 22 2020 at 15:58):

Standard answer when some programming stuff doesn't seem to make any sense at first...

#### Kevin Buzzard (May 22 2020 at 16:06):

So what I learn from the link is that you can make pong with lenses