Ltac2: distinguishing between tactics with the same `beginning` of the name

Developing plugins
1

Dear community,

I was working with Ltac2 on creating some simple tactics, and I ran into the following problem: let us assume that we have some Ltac2 tactics

Ltac2 Notation "Tactic name" s(constr) := ...
Ltac2 Notation "Tactic name" s(ident) "one more word" t(constr) := ...

When calling the above tactics, Ltac2 does not always recognize which tactic I am calling. For instance, if I want to call the first tactic and just write

Tactic name s.

for some s that makes sense in a goal, I receive an error that there are more arguments needed (as it assumes that I am calling the second tactic, and I think this happens because it is the last one that is compiled).

Is it possible to circumvent this without changing the names of the tactics?

2

I believe it may be possible to do this using identifiers for these tactics.

For instance, if I define the following two tactics:

Ltac2 Notation "tactic" := print(of_string "Hello").
Ltac2 Notation "tactic" s(constr) := print(of_string "Hello with constr").

then we run into the same problem as I described earlier.

However, if instead I write as:

Ltac2 Notation "tactic" := print(of_string "Hello").
Ltac2 Notation tactic := tactic.
Ltac2 Notation "tactic" s(constr) := print(of_string "Hello with constr").

Then now both tactics seem to work (I believe the second line from above is an identifier). I have seen this done a few times in the Ltac2.Notations file.

However, the above works if I have a tactic with no arguments/variables. How can I extend this to tactics that have variables?

Moreover, the above seems to be really sensitive to writing the identifiers and the tactics with a lower case letter. Is it possible to extend this to capital letters for the tactic names?

3

I have discovered one more thing: if the tactics have input parameters only of type constr, everything works fine. For instance:

Ltac2 Notation "tactic" s(constr) := print(of_string "Hello with 1 constr").
Ltac2 Notation "tactic" s(constr) t(constr) := print(of_string "Hello with 2 constr").

works. However, If I replace any of the above constr with, for instance, an ident or an intropatterns, then again I run into the same issue.

I do not really understand why this is the case.

4

At least some of your symptoms (e.g. those in the first post) are consistent with a parsing problem — it might be too hard for the parser to distinguish the different tactics, since the distinction must happen “locally”, not by looking at the whole input:

I don’t know if Ltac2 notations have the same automated left-factoring of other notations.