Get arguments for tactic of form simple_intropattern_list(x)

[lukovdm]

I need to write an Intro tactic that also allows for receiving normal intro patterns and also my own intro patterns. To be able to properly accept an intro pattern, I need to have a notation in the form of:

Tactic Notation "eiIntros" "(" simple_intropattern_list(x) ")" :=
  elpi eiIntros x.

amongst other notations.
It would thus be nice to be able to read in an intro pattern list, be able to manipulate it when necessary and pass it on to the intro tactic.

[gares]

I see two ways forward.
The quick fix could be to make such a code work:

From elpi Require Import elpi.

Elpi Tactic app.
Elpi Accumulate lp:{{
  solve (goal _ _ _ _ [str X] as G) GL :- coq.ltac.call-ltac1 X G GL.
}}.
Elpi Typecheck.

Goal forall n, n + 1 = 1.
  let tac := intros n in
  elpi app "tac".

here tac is a thunk, so the simple intro pattern data type does not need to be known to elpi. Tactics are already called by name, but apparently we only look for them in the global ltac environment.

The better option would be to expose to elpi this data type

https://github.com/coq/coq/blob/967e2222e79def2c15c6652de2e9f4c015a6dc89/proofs/tactypes.mli#L19-L31

This latter option would make it possible to craft this data in elpi, and not just pass it along.

[gares]

Sorry, the implicit question is: would the first approach suffice for your use case?

[lukovdm]

Yes, I think this would work. I only need to call intros on an intro pattern that I have been given by the user on the tactic for now.
Thus my notation would become:

Tactic Notation "eiIntros" "(" simple_intropattern_list(x) ")" :=
  let coqintro := intros x in
  elpi eiIntros coqintro "".

[lukovdm]

After having a talk with my supervisor, I'm sorry to say, it turns out we actually do need to have full access to the intro pattern data type. We have to pull it apart and apply our own steps in between applications of parts of the intro pattern. Also we would need to create new ones from scratch. Would this be possible?