Zulip Chat Archive

Stream: general

Topic: replacer


view this post on Zulip Mario Carneiro (Sep 11 2018 at 00:53):

By the suggestion of Simon, I've extended replacer to support parameters in its type. That is, you can define a replaceable definition foo : A -> tactic B where you have arbitrary input and output, rather than just tactic unit. Incidentally, implementing this required my first attempt at meta-metaprogramming, since the defined tactics are written programmatically.

view this post on Zulip Simon Hudon (Sep 11 2018 at 00:55):

Does it accept any number of parameters?

view this post on Zulip Mario Carneiro (Sep 11 2018 at 00:55):

yes

view this post on Zulip Mario Carneiro (Sep 11 2018 at 00:55):

just one output, but we always bundle that anyway

view this post on Zulip Mario Carneiro (Sep 11 2018 at 00:57):

It doesn't support monads other than tactic, and the prev tactic access does not allow changing parameters

view this post on Zulip Simon Hudon (Sep 11 2018 at 01:04):

This supercalifragilisticexpialidocious!

view this post on Zulip Simon Hudon (Sep 11 2018 at 01:06):

To let other people in on the idea, I wanted this so that we can write a tactic at the same as we write a proof, even if the tactic is a core tactic, we can put them in the same file and stop recompiling everything every time we change the tactic

view this post on Zulip Simon Hudon (Sep 11 2018 at 01:06):

This is a bit similar to hot code loading

view this post on Zulip Mario Carneiro (Sep 11 2018 at 01:08):

you don't mean "core" as in "core lean" though. Like time travel, you can't go back before the time machine was invented

view this post on Zulip Simon Hudon (Sep 11 2018 at 01:08):

That is correct :)

view this post on Zulip Simon Hudon (Sep 11 2018 at 01:09):

You can only replace definitions in files where you can import this replacer tactic.

view this post on Zulip Simon Hudon (Sep 11 2018 at 01:18):

What do you use from tactic.basic?

view this post on Zulip Mario Carneiro (Sep 11 2018 at 01:24):

just the has_reflect instance for binder_info

view this post on Zulip Simon Hudon (Sep 11 2018 at 01:26):

Cool, I left you a comment on the commit. I think it should be moved to tactic.replacer so that tactic.basic can import tactic.replacer (since it's a tool for writing tactics)

view this post on Zulip Mario Carneiro (Sep 11 2018 at 01:31):

I don't think anything in mathlib uses it though

view this post on Zulip Simon Hudon (Sep 11 2018 at 01:35):

That's ok. What i intend to do with it when I write tactics for mathlib is to temporarily have tactic.basic import tactic.replacer, make all the routines I use replaceable, go write an example and, next to it, keep a version of the functions and tactics that I modify. When I'm done, I remove the def_replacers and the import tactic.basic statement.

view this post on Zulip Simon Hudon (Sep 11 2018 at 01:46):

Btw, there is a way we could go back in time passed the creation of our machine: using meta programming, we create a dynamic namespace in which we copy all the visible declarations that depend on what we want to replace and and we rewrite their definitions to insert the replacer instead of the original definition.

view this post on Zulip Mario Carneiro (Sep 11 2018 at 01:50):

that's more like alternate universe time travel

view this post on Zulip Simon Hudon (Sep 11 2018 at 01:51):

I'm happy with multi-universe interpretations


Last updated: May 12 2021 at 22:15 UTC