Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: tactic modes(?)


view this post on Zulip Reid Barton (Sep 18 2020 at 17:44):

Is there documentation on (or, failing that, some examples of) writing new tactic modes such as conv?

view this post on Zulip Reid Barton (Sep 18 2020 at 17:44):

@Simon Hudon what's the link to your temporal logic tactic? I poked around your github repos but didn't see it

view this post on Zulip Rob Lewis (Sep 18 2020 at 17:46):

I've followed the smt mode from core as an example, the handful of times I've tried to do this

view this post on Zulip Simon Hudon (Sep 18 2020 at 17:46):

Here it is: https://github.com/unitb/temporal-logic

view this post on Zulip Kevin Buzzard (Sep 18 2020 at 17:47):

The natural number game used some kind of modded tactic mode begin [natnumgame] and Rob Lewis wrote some code which ported most of the tactics over and let me redefine a few

view this post on Zulip Rob Lewis (Sep 18 2020 at 17:47):

:up: that's one of the handful

view this post on Zulip Kevin Buzzard (Sep 18 2020 at 17:48):

https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/tactic/nat_num_game.lean

view this post on Zulip Reid Barton (Sep 18 2020 at 17:53):

Thanks all. So I gather begin [smt] ... end means something like smt.interactive.execute t where t is the result of parsing the begin-end block using the smt.interactive namespace. And I guess if I want to support something like conv { ... }, then I just need to define my_tac.interactive.itactic := my_tac unit to represent the body and the parser will automatically use the my_tac parser for it?

view this post on Zulip Simon Hudon (Sep 18 2020 at 17:58):

Yes

view this post on Zulip Bryan Gin-ge Chen (Sep 18 2020 at 18:17):

There are a few tiny examples in the Lean tests as well: tests/lean/interactive/my_tac_class.lean, tests/lean/run/my_tac_class.lean, tests/lean/interactive/rb_map_ts.lean

view this post on Zulip Reid Barton (Sep 18 2020 at 18:18):

I found a helpful comment at https://github.com/unitb/temporal-logic/blob/master/src/temporal_logic/tactic.lean#L17-L31
clearly copied from somewhere else, but that's where I found it

view this post on Zulip Reid Barton (Sep 18 2020 at 18:19):

ah, it's indeed in the Lean C++ code somewhere

view this post on Zulip Mario Carneiro (Sep 18 2020 at 18:21):

https://github.com/leanprover-community/lean/blob/d907e6aed0b399f6512139c751b908979bf45eaf/src/frontends/lean/tactic_notation.cpp#L33-L52

view this post on Zulip Reid Barton (Sep 18 2020 at 18:31):

So with save_info, although all the examples I've found ultimately use tactic.to_formatto format the tactic state, I can also pass any old nonsense I like to save_info_thunk, right?

view this post on Zulip Reid Barton (Sep 18 2020 at 18:32):

(with the possible exception of the smt tactic which uses a different built-in formatter)

view this post on Zulip Simon Hudon (Sep 18 2020 at 18:34):

Yes that's right, that's where you feed in whatever you want to display

view this post on Zulip Reid Barton (Sep 18 2020 at 20:37):

To correct what I wrote earlier, Simon's temporal tactic does produce a custom format for the tactic state, it just does such a good job of imitating the standard one that I didn't notice :upside_down:

view this post on Zulip Simon Hudon (Sep 18 2020 at 20:39):

Ha! Sorry to mislead you like this!

view this post on Zulip Simon Hudon (Sep 18 2020 at 20:40):

Mainly what my pretty printing does is print hypotheses of the form h : Γ ⊢ φ as h : φ and omit the variable Γ from the context.

view this post on Zulip Simon Hudon (Sep 18 2020 at 20:41):

Was it hard to get it to build? I haven't ungraded it in a while (still in the process of upgrading the dependencies)

view this post on Zulip Reid Barton (Sep 18 2020 at 20:42):

Let's say it was not hard to get it to build to the point where I could inspect at least one [temporal] proof interactively

view this post on Zulip Reid Barton (Sep 18 2020 at 21:28):

In fact, what I want to do is broadly similar--basically I want to pretend that I have a variable x : X, while actually representing it by x : Γ → X.

view this post on Zulip Reid Barton (Sep 18 2020 at 21:30):

One thing I don't understand yet is what controls the environment that texpr gets parsed/typechecked in. When texpr is an argument of an interactive tactic, is the pexpr that gets passed to the tactic really independent of the environment? If it does depend on the environment, can I set the environment somehow?

view this post on Zulip Reid Barton (Sep 18 2020 at 22:12):

Oh, looking up a few inches I see

meta constant set_env : environment  parser unit

Can I run this from the tactic monad somehow? Or am I supposed to create a custom parser for my interactive tactics which manipulates the environment first? I see meta constant of_tactic : tactic α → parser α...

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:13):

sorry, that path only goes one way

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:14):

tactics can't run parsers

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:15):

Do you really want to replace the environment and not just the local context?

view this post on Zulip Reid Barton (Sep 18 2020 at 22:15):

I do just want to replace the local context but I don't understand how I'd do so

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:16):

An easy way is to revert_all and then backtrack when you are done

view this post on Zulip Reid Barton (Sep 18 2020 at 22:17):

that is, I want to have an underlying tactic state somewhere containing x : Γ → X but present to the user the illusion that x : X, and have my tactics fix up the expr in a certain way

view this post on Zulip Reid Barton (Sep 18 2020 at 22:18):

I guess what I don't really understand is how the parser knows what the local context is at all--couldn't I use some monad totally unrelated to tactic_state as my custom tactic monad?

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:18):

the parser doesn't have to care since it only produces pre-expressions

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:19):

If you are okay with the extra work the usual way I do more radical type reinterpretation is to perform post-processing directly on the pexpr, without calling to_expr on it

view this post on Zulip Reid Barton (Sep 18 2020 at 22:19):

ok, so does this mean a pre-expression might contain things like unresolved . syntax, overloaded notation, etc.?

view this post on Zulip Reid Barton (Sep 18 2020 at 22:20):

presumably as macros or something?

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:20):

yes, it has those things

view this post on Zulip Reid Barton (Sep 18 2020 at 22:20):

I see

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:21):

If you need to change name resolution then things get a bit more tricky

view this post on Zulip Reid Barton (Sep 18 2020 at 22:21):

I guess that's fine for the "operate directly on the pexpr" approach since I want to replace x.foo by (x i).foo or whatever anyways

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:22):

in your case you can probably send it to to_expr after your fixups to still get most of lean goodness

view this post on Zulip Reid Barton (Sep 18 2020 at 22:22):

in fact, I basically just want to do a bunch of substitutions of the form "replace x by x i" so maybe this functionality already exists

view this post on Zulip Reid Barton (Sep 18 2020 at 22:22):

and then use to_expr right

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:22):

Isn't that exactly what a parameter does?

view this post on Zulip Reid Barton (Sep 18 2020 at 22:25):

I guess so? though here the parameter i will be another local constant

view this post on Zulip Reid Barton (Sep 18 2020 at 22:25):

I was thinking more along the lines of Lean knowing how perform substitution in general

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:25):

well technically if you are in a section then the parameter is in your local context

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:26):

There is expr.replace I think

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:26):

which was updated to work on pexprs at some point

view this post on Zulip Reid Barton (Sep 18 2020 at 22:28):

this looks fancy

view this post on Zulip Reid Barton (Sep 18 2020 at 22:30):

but, it also looks like it only works on expr

view this post on Zulip Reid Barton (Sep 18 2020 at 22:31):

anyways, this is more than enough to keep me busy for a while

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:31):

@Rob Lewis Didn't you PR something like this?

view this post on Zulip Rob Lewis (Sep 18 2020 at 22:31):

Not me

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:32):

IIUC the only thing needed to make expr.replace work on pexprs is to generalize the signature

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:32):

this was something like 18 months ago or so

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:33):

pexprs need a general overhaul to make them more lean friendly

view this post on Zulip Simon Hudon (Sep 18 2020 at 22:34):

I think I made such adjustment for expr.fold the same should work for expr.replace

view this post on Zulip Reid Barton (Sep 18 2020 at 22:36):

Mario Carneiro said:

IIUC the only thing needed to make expr.replace work on pexprs is to generalize the signature

so, you're saying I can just unchecked_cast it :smiling_devil:

view this post on Zulip Mario Carneiro (Sep 18 2020 at 22:37):

yes, that will work

view this post on Zulip Reid Barton (Sep 18 2020 at 22:38):

is this the formal version of proof by reference to personal communication

view this post on Zulip Adam Topaz (Sep 19 2020 at 00:06):

Is there a tactic for that?


Last updated: May 09 2021 at 22:13 UTC