Inaccessible optional stuff

Stream: metaprogramming / tactics

[Patrick Massot]

In the following code, why is the dbg_trace returning none? Removing the "with" part works.

import Lean

elab "foo" x₁:ident x₂:ident new:("with" ident)? : tactic => do
  dbg_trace new

example : True := by
  foo a b with c
  trivial

[Kyle Miller]

It seems that elab might not be generating the right pattern, but I don't really know exactly what I'm looking at.

import Lean

set_option trace.Elab.command true
set_option pp.rawOnError true

elab "foo" x₁:ident x₂:ident new:("with" ident)? : tactic => do
  dbg_trace s!"{new}"

-- Generated pattern:
/-
[[(Term.quot
      "`("
      (tacticFoo__With_
        (token_antiquot "foo" "%" "$" `x._@.Mathlib.foo._hyg.4)
        (ident.antiquot "$" [] `x₁ [])
        (ident.antiquot "$" [] `x₂ [])
        [(optional.antiquot_suffix_splice (pseudo.antiquot "$" [] `new []) "?")])
      ")")]]
-/

elab_rules : tactic
  | `(tactic| foo $x₁ $x₂ $[with $new]?) => dbg_trace s!"{new}"; pure ()

-- Generated pattern:
/-
[[(Tactic.quot
    "`(tactic|"
    (tacticFoo__With_
    "foo"
    (ident.antiquot "$" [] `x₁ [])
    (ident.antiquot "$" [] `x₂ [])
    [(optional.antiquot_scope "$" [] "[" ["with" (ident.antiquot "$" [] `new [])] "]" "?")])
    ")")]]
-/

[Alex J. Best]

import Lean

elab "foo" x₁:ident x₂:ident new:(("with" ident) ?) : tactic => do
  dbg_trace  new
example : True := by
  foo a b with asd
  trivial

at least does something, no idea how to get precisely what you want though

[Alex J. Best]

You can at least use .raw.getArg 1 to get the ident

[Kyle Miller]

This seems to be creating a null node that's either length-0 or length-2, so I guess you can do cases on the length.

import Lean

open Lean

elab "foo" x₁:ident x₂:ident new':(("with" ident) ?) : tactic => do
  let new : Option Ident :=
    if new'.raw.getNumArgs == 0 then none else some ⟨new'.raw.getArg 1⟩
  dbg_trace new

example : True := by
  foo a b with asd
  foo a b
  trivial

[Patrick Massot]

Thanks Alex and Kyle. Maybe I should have said I know how to work around this issue, but I'm completely puzzled about the issue and wanted to understand what's going on. I guess we need to ping @Sebastian Ullrich.

[Sebastian Ullrich]

I don't think it's clear at all here what new should bind to, should it be something of type Option (Syntax \x Ident) where Syntax is the with keyword? I believe it would be better to reject such complex patterns in macro/elab and point users to using separate syntax+macro_rules/elab_rules instead.

[Patrick Massot]

Is using elab evil? This is news to me.

[Sebastian Ullrich]

Only its implementation

[Sebastian Ullrich]

so it is better to restrict it than somehow fix this case

[Patrick Massot]

To answer your question, I was hoping new to have type Option Syntax.

[Shreyas Srinivas]

I don't understand. I thought any non trivial tactic code would benefit from using elab. What sort of footguns should we watch out for?

[Thomas Murrills]

If we shouldn't allow new:("with" ident)?, would it be possible to allow elab "foo" x₁:ident x₂:ident ("with" new:ident)? : tactic => ... in parallel to the syntax match `(tactic| foo $x₁:ident $x₂:ident $[with $new:ident]?) ?

[Mario Carneiro]

Patrick Massot said:

To answer your question, I was hoping new to have type Option Syntax.

This doesn't quite answer the question; what should the Syntax be referring to? (My guess: the overall syntax node)

[Thomas Murrills]

I would assume the overall syntax node in that case too—I think it's fairly natural to expect chunks of syntax (like with together with the ident) to be grouped into a whole by the structure of (T)Syntax, not ×

[Patrick Massot]

Yes, I meant the whole thing. I would hope to access the interesting bit using new.raw[1]. But of course the ideal situation would be to be allowed to write elab "foo" x₁:ident x₂:ident ("with" new:ident)? : tactic => ... as Thomas wrote.

[Sebastian Ullrich]

Patrick Massot said:

I would hope to access the interesting bit using new.raw[1].

The point of these convenience commands is to never require access to raw. It would be better to nudge people towards elab_rules for these more complex matches than towards raw.

But of course the ideal situation would be to be allowed to write elab "foo" x₁:ident x₂:ident ("with" new:ident)? : tactic => ... as Thomas wrote.

I don't see this happening, it would require effectively a copy of the entire stx category adjusted for macro/elab with naming for subparts. Easier to nudge people towards elab_rules.

[Patrick Massot]

Could you nudge me a bit more explicitly then? What's wrong with

syntax "foo" ident ident ("with" ident)? : tactic

elab_rules
| `(tactic| foo $x₁:ident $x₂:ident $[with $new]?) => ...

[Sebastian Ullrich]

Is it the "specify category" error?

elab_rules : tactic
| `(tactic| foo $x₁:ident $x₂:ident $[with $new]?) => _

[Patrick Massot]

No difference

[Sebastian Ullrich]

Works on my machine

import Lean

syntax "foo" ident ident ("with" ident)? : tactic

elab_rules : tactic
| `(tactic| foo $x₁:ident $x₂:ident $[with $new]?) => sorry

[Patrick Massot]

Sorry, I tried so many variations that I ended up in a state missing a question mark.

[Patrick Massot]

Thanks for your help.

[Mac Malone]

Sebastian Ullrich said:

I don't see this happening, it would require effectively a copy of the entire stx category adjusted for macro/elab with naming for subparts. Easier to nudge people towards elab_rules.

My thought on this (and what I had hoped was the long-term plan) was to merge the macro and syntax categories for these and just produce an warning/error post-parse if subpart is named in a syntax declaration.

[Mac Malone]

(In the longer-term, one could even hope to allow subpart naming in syntax declarations and automatically generate the respective projection functions to derive them from the TSyntax of declared syntax kind.)