Zulip Chat Archive

Stream: PR reviews

Topic: lean#260 expr lens


view this post on Zulip Gabriel Ebner (May 21 2020 at 18:26):

Do we already have something like this? Other opinions?

view this post on Zulip Johan Commelin (May 21 2020 at 18:39):

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

view this post on Zulip Scott Morrison (May 22 2020 at 01:46):

It's at https://github.com/leanprover-community/mathlib/blob/master/src/meta/expr_lens.lean

view this post on Zulip Scott Morrison (May 22 2020 at 01:47):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 22 2020 at 04:36):

@Scott Morrison Oops, sorry for misattributing

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Edward Ayers (May 22 2020 at 09:16):

So you can't use interactive tactics to derive things

view this post on Zulip 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. :-)

view this post on Zulip Patrick Massot (May 22 2020 at 09:40):

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

view this post on Zulip 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)

view this post on Zulip Bhavik Mehta (May 22 2020 at 15:37):

https://hackage.haskell.org/package/lens :)

view this post on Zulip Patrick Massot (May 22 2020 at 15:58):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 16:06):

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

view this post on Zulip Bhavik Mehta (May 22 2020 at 17:22):

https://twitter.com/tangled_zans/status/1208167165104443392

view this post on Zulip Bhavik Mehta (May 22 2020 at 17:24):

If you do want to learn about lenses I recommend: https://skillsmatter.com/skillscasts/4251-lenses-compositional-data-access-and-manipulation

view this post on Zulip Patrick Massot (May 22 2020 at 18:01):

I've used trains in the UK, and I can totally believe they're ready to try anything to fix them.


Last updated: May 09 2021 at 14:10 UTC