simulating interactive tactics in metaprogramming

Stream: metaprogramming / tactics

[Xavier Martinet]

Hi everyone,

I am trying to simulate a sequence of tactic.interactive.<tactic_name> within a standard meta def metaprogramming definition. In order to to so, I write :

g ← tactic.mk_meta_var goal,
tactic.set_goals [g]

then

tactic.<tactic_name>`  -- instead of `tactic.interactive.<tactic_name>`

However, due to the specific implicit arguments of the tactic.interactive.<tactic_name> (parsed arguments), I have to unfold the definition. For instance, if I want to use norm_num, I would write :

f ← norm_num.get_step,
tactic.norm_num f [] interactive.loc.wildcard

However this solution is not tractable for some tactics, such as linarith for instance: as tactic.linarith calls linarith.mk_single_comp_zero_pf whose definition contains a [norm_num] that is parsed as tactic.interactive.norm_num. But as we are not in interactive mode anymore, there is no implicit parsed arguments, so the call fails. The workaround I found is to copy-paste ALL functions called as to eventually change [norm_num] by do f ← norm_num.get_step, tactic.norm_num f [] interactive.loc.wildcard. This is obviously not super pratical nor scalable to other tactics.

Is there a way in metaprogramming to have constructions such as [<tactic_name>]` are correctly called with their implicit parsed arguments?

cc @Timothee Lacroix

[Gabriel Ebner]

You can call tactic.interactive.linarith directly, the parser arguments are just wrappers. For example, parse p? reduces to option ...:

#check tactic.interactive.linarith none (some ()) (some []) { split_ne := tt } -- tactic unit

[Gabriel Ebner]

(If you don't know what to write after some, you can at first write some _. Then Lean will tell you explicitly what type it expected there.)

[Xavier Martinet]

Thanks.

However for some reasons the issue remains: when there is something like [norm_num] written in a definition, it just fails unless I change it explicitely to tactic.interactive.norm_num none none

As tactic.interactive.linarith calls mk_single_comp_zero_pf which contains [norm_num,done], it does not do exactly the same thing as in interactive mode

[Xavier Martinet]

(sorry, I meant tactic.interactive.norm_num [] interactive.loc.wildcard)

[Xavier Martinet]

Actually even the cfg.discharger, which is equal by default to [norm_num], needs to be set to {discharger := tactic.interactive.ring none}

so a regular by linarith is actually a tactic.interactive.linarith none none none {discharger := tactic.interactive.ring none} instead of a tactic.interactive.linarith none none none

and then, as mentionned above, I still need to patch mk_single_comp_zero_pf for the same reason (it contains [norm_num,done])

[Rob Lewis]

To call a tactic literally as you would write it in interactive mode, you can use the notation `[linarith]. This is a term with type tactic unit. But you won't be able to pass variable arguments to it. That is, you can write `[linarith [h1, h2]], but h1 and h2 will refer to whatever is in the context at the time the tactic is called; if you have e : expr when you're defining your tactic, you can't write `[linarith [e]].

[Xavier Martinet]

Thanks!

But how are the implicit parsed arguments created? For instance:
1) in tactic.interactive.linarith, there is a cfg : linarith.linarith_config where by default cfg.discharger := [ring]. When tactic.interactive.ring is actually called, its parameter red : parse (tk "!")? is automatically filled with none.
2) in the case of [norm_num,done] in mk_single_comp_zero_pf, the same goes for the [norm_num] parameters: (hs : parse simp_arg_list) and (l : parse location)are respectively set to "empty/default" values hs := [] and l := interactive.loc.wildcard.

What I don't quite understand is: how are those arguments created? Is there some kind of "parsing context" in interactive mode that enable argument creation? If so, is there a way when in metaprogramming to fill out this context so in 1) cfg.discharger := [ring] is actually interpreted as cfg.discharger := tactic.interactive.ring none, and in 2) [norm_num,done] is interpreted as tactic.interactive.norm_num [] interactive.loc.wildcard >> tactic.interactive.done ?

[Xavier Martinet]

I assume I would have to fiddle with the lean.parser_state: any way to do it in Lean itself?

[Rob Lewis]

When you write ring in interactive mode, you're calling src#tactic.interactive.ring . The argument red has type interactive.parse (optional (lean.parser.tk "!")). If p : parser T, interactive.parse p is defeq to T, so this argument red really has type option unit. The interactive.parse tag is what makes the input syntax different in interactive mode: if it wants to parse optional (tk "!"), it will try to parse tk "!" and return some if it succeds, otherwise none.

[Rob Lewis]

I'm not sure what you mean by the rest of your question. `[ring] is the same as tactic.interactive.ring none. It runs interactive mode parsing inside the `[...] block.

[Xavier Martinet]

Thanks Rob. I need to process that as I am surely being confused between several notions

[Xavier Martinet]

Thanks a lot for your answers.

I have isolated the code that caused me troubles:

import tactic

meta def tactic.interactive.dummy : tactic unit := tactic.trace "DUMMY"

meta def apply_dummy_on_app: expr → tactic unit
| e@(expr.app _ _) := `[dummy] <|> tactic.trace "FAIL"
| e@(expr.lam _ _ _ _) := do ⟨_, body⟩ ← tactic.open_n_lambdas e 1, apply_dummy_on_app body
| _ := return ()

meta def apply_dummy (decl_nm : name) : tactic unit := do
  env ← tactic.get_env,
  decl ← env.get decl_nm,
  apply_dummy_on_app decl.value

meta def apply_dummy_with_ref (decl_nm : name) : tactic unit := do
  tactic.using_new_ref (0 : ℕ) $ λ dp_ref, apply_dummy decl_nm


theorem mythm : 0 = 0 := eq.refl _

run_cmd apply_dummy `mythm  -- SUCCESS
run_cmd apply_dummy_with_ref `mythm  -- FAILS

For a reason I cannot fathom, the fact that there is a tactic.using_new_ref makes the use of the [<tactic>] construction fail.
Do you see any explanations?

[Gabriel Ebner]

MWE:

run_cmd tactic.using_new_ref (0 : ℕ) $ λ _, `[skip]
-- Failed to copy state to another thread

[Gabriel Ebner]

What's happening is that Lean records the tactic state in interactive tactics (yes, even the ones in `[] blocks) to show the goal in the editor.

[Xavier Martinet]

Thanks!!! And why does it fail to copy the tactic state? the "other" thread is the one where there is a specific value for the ref?

[Gabriel Ebner]

That's just because the case with references wasn't implemented. lean#666

[Gabriel Ebner]

References are just a tactic-state specific map from number->object.