Differentiating between tactic and term elaborators

Stream: metaprogramming / tactics

[Adam Topaz]

I am running into an annoying error that I don't know how to resolve. Here is a MWE:

import Lean

open Lean Elab

syntax (name := fooTacStx) "foo" str (tactic)? : tactic
--syntax (name := tooTermStx) "foo%" str term : term <<--- uncomment for error below.

open Tactic in
@[tactic fooTacStx]
def elabExplainTac : Tactic := fun stx =>
  match stx with
  | `(tactic|foo%$tk $s:str $(t)?) => do
    return
  | _ => throwUnsupportedSyntax

If you uncomment the indicated line, the elaborator results in an error at the location token tk, I suppose because Lean gets confused about foo%. Is there a way around this, or do I just need to use different names for the tactic foo and the term elaborator foo%?

[Eric Wieser]

Is defining foo% after the elaborator an option?

[Adam Topaz]

I guess, but that seems more like a hack than a fix.

[Eric Wieser]

It feels like a better hack than choosing different names

[Adam Topaz]

Yeah I agree with that.

[Eric Wieser]

Idealy something like $[foo]%$tk would work here to disambiguate

[Eric Wieser]

I've also wanted $[foo $x]%$tk in the past to refer to groups

[Adam Topaz]

FWIW, I'm using @Eric Wieser 's hack in #19378 (this is tagged with RFC for now)

[Adam Topaz]

(This is based on a discussion I had with @Johan Commelin earlier today, in case he wants to take a look)

[Damiano Testa]

I am not sure of the consequences, but this also "resolves" the error:

syntax (name := tooTermStx) "foo" "%" str term : term --<<--- uncomment for error below.

[Eric Wieser]

Can you use the same notation for both cases?

[Adam Topaz]

you mean explain ... for both the tactic and term I suppose?

[Adam Topaz]

and yes, I agree with your comment on the PR that explain ... in ... is nicer :)

[Eric Wieser]

Yes, in the same way that we have set_option .. in for both tactics and terms

[Eric Wieser]

(there might also be some pretty-printer instructions about indenting the term after in you can copy from elsewhere)

[Adam Topaz]

Hmm ok I'll try to look into that.

[Adam Topaz]

If you have somewhere you can point me to that would be very helpful

[Adam Topaz]

An example I know of that has such a pretty printing hint is proof_wanted, but I'm sure there are other more relevant examples.

[Damiano Testa]

count_heartbeats starts with

elab "count_heartbeats! " n:(num)? "in" ppLine tac:tacticSeq : tactic => do

[Damiano Testa]

I think that ppLine instructs the pretty-printer to use a new line.

[Adam Topaz]

yeah, I do think ppIndent is more appropriate here, right?

[Adam Topaz]

we want

explain "this" in
  that

as opposed to

explain "this" in
that

[Damiano Testa]

Probably. I would also say that in count_heartbeats there should be a space after num, if num is present.

[Damiano Testa]

Btw, I think that the ppRountrip linter may have an option to show the pp version of a command.

[Damiano Testa]

It certainly compares the current version with what the pretty-printer thinks that it should be,

[Adam Topaz]

Okay, I'll play around with this when I have time to do so (not now unfortunately)

[Damiano Testa]

Hmm, the ppRoundtrip was just some debugging command that did not make it to the final version, but that was just a convenience: it is easy enough to log the syntax anyway.

[Kyle Miller]

In case you still need it @Adam Topaz, one workaround is to index the syntax directly (ew)

open Tactic in
@[tactic fooTacStx]
def elabExplainTac : Tactic := fun stx =>
  match stx with
  | `(tactic|foo $s:str $(t)?) => do
    let tk := stx[0]
    return
  | _ => throwUnsupportedSyntax

[Adam Topaz]

ew is right :-/

[Adam Topaz]

What I find surprising is that I would expect lean to know that foo% ... is not valid syntax is the tactic syntax category because no such tactic syntax was declared, yet it still gets confused.

[Kyle Miller]

It's because when you define a term, foo% becomes a keyword, and keywords are keywords for all time in all contexts.

[Kyle Miller]

(It's worth pointing out that tactics are special: when you define them the initial token does not become a keyword. It's like it inserts & automatically.)

[Adam Topaz]

Should we reconsider the % convention for term elaborators?

[Eric Wieser]

I'd prefer that the quotation syntax gain some grouping operator to make this a non-issue, such as

Eric Wieser said:

I've also wanted $[foo $x]%$tk in the past to refer to groups

[Eric Wieser]

Though separately, I've heard that the foo% convention was intended to mean "this is an implementation detail" not "this is a term elaborator"

[Adam Topaz]

Is that really the case? There are many instances of reassoc_of% being used in mathlib.

[Adam Topaz]

If % is an implementation detail, do we even have a convention for term elaborators?

[Eric Wieser]

I think the context of that rumor was that core intended % to mean implementation detail, and mathlib adopted it to mean term elaborator

[Kyle Miller]

I think it's nice when there's some sort of indication so you know "ceci n'est pas une fonction"

For example, the congr(...) term uses parentheses with no whitespace, so you know it has to be something special.

[Eric Wieser]

Taking that to its extreme though we end up with return(x) instead of return x

[Kyle Miller]

Core language keywords are special though, since they don't vary project to project (plus that's a doElem not a term)

[Eric Wieser]

To some extent though the syntax highlighting acts as the indication that something is not a function

[Eric Wieser]

Though it would be helpful if all such keywords had the same parsing precedence (unsafe and no_index disagreeing gets me every time)