replacer

Stream: general

[Mario Carneiro]

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.

[Simon Hudon]

Does it accept any number of parameters?

[Mario Carneiro]

yes

[Mario Carneiro]

just one output, but we always bundle that anyway

[Mario Carneiro]

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

[Simon Hudon]

This supercalifragilisticexpialidocious!

[Simon Hudon]

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

[Simon Hudon]

This is a bit similar to hot code loading

[Mario Carneiro]

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

[Simon Hudon]

That is correct :)

[Simon Hudon]

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

[Simon Hudon]

What do you use from tactic.basic?

[Mario Carneiro]

just the has_reflect instance for binder_info

[Simon Hudon]

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)

[Mario Carneiro]

I don't think anything in mathlib uses it though

[Simon Hudon]

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.

[Simon Hudon]

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.

[Mario Carneiro]

that's more like alternate universe time travel

[Simon Hudon]

I'm happy with multi-universe interpretations