New notation: using tactics in syntax

Stream: lean4

[Robert Maxton]

Mostly for the sake of practice with the new notation system, I'm trying to implement the syntax psuedocoded below:

Σ| WalkingPair, ⟨if_left | if_right⟩ -- => Σ (x: WalkingPair), x |> fun | left => if_left | right => if_right
Σ| (Option Bool), ⟨if_none| if_false | if_true⟩
   -- => Σ (x: Option Bool), x |> fun | none => if_none | some.false => if_false |  some.true => if_true
-- ... and so on for arbitrary finitely constructible types

So far, I've managed to come up with this:

set_option trace.Elab.definition true in
syntax (name := sigma_rcases) "Σ| " term ", ""⟨"sepBy1(ppSpace colGt term, " | ")"⟩" : term

set_option trace.Elab.definition true in
macro_rules
| `(Σ| $btype:term, ⟨$ctr_cases:term|*⟩) => do
      let fresh ← Elab.Term.mkFreshIdent btype true
      let freshRef ← `(casesTarget|$fresh:ident)
      let exacts ← ctr_cases.getElems.mapM (λ x ↦ `(tactic|exact $x))
      let binders ← ctr_cases.getElems.mapM (λ x ↦ `(rcasesPat|$(⟨mkHole x true⟩)))
      let byTactic ← `(by rcases $freshRef with ($binders|*); $exacts;*)
      `(Σ $fresh:ident, $byTactic)

I'm using by rcases to generate the constructor names I need, and assuming that the user knows what they're doing/how many blanks they need.

Unfortunately, while it type-checks, it doesn't quite work:

#check Σ x: WalkingPair, by rcases fresh with (_ | _); exact ℕ; exact ℤ
-- (x : WalkingPair) × WalkingPair.casesOn x ℕ ℤ : Type

#check (Σ| WalkingPair, ⟨ℕ | ℤ⟩)
 -- unexpected syntax
--   rcases x✝ with (_ | _)

Any advice? Also, does this belong here or under #metaprogramming / tactics ?

[Robert Maxton]

In case anyone runs across this in the future: the error was at

let binders ← ctr_cases.getElems.mapM (λ x ↦ `(rcasesPat|$(⟨mkHole x true⟩)))

`(rcasesPat|... starts a parser for the parser category rcasesPat; rather than trying to synthesize the syntax, the solution was to just replace that line with

let binders ← ctr_cases.getElems.mapM (λ _ ↦ `(rcasesPat|_))

The full solution is

open Lean Macro Parser Parser.Term Syntax Tactic
syntax "Σ| " term ", ""⟨"sepBy1(ppSpace colGt term, " | ")"⟩" : term

macro_rules
| `(Σ| $btype:term, ⟨$ctr_cases:term|*⟩) => do
      let fresh ← mkFreshIdent btype true
      let binders ← ctr_cases.getElems.mapM (λ _ ↦ `(rcasesPat|_))
      `(Σ $fresh:ident:$btype, by
          rcases $fresh:ident with ($binders|*); $[exact $ctr_cases];*)

#check (Σ| WalkingPair, ⟨ℕ | ℤ⟩) -- (x : WalkingPair) × WalkingPair.casesOn x ℕ ℤ : Type