Quoting syntax arrays

Stream: lean4

[Joachim Breitner]

I keep spending an awful lot of time guessing at the right syntax for syntax quotations, especially around sequences. For example, what am I doing wrong here:

import Std.Tactic.TryThis
import Std.Tactic.ShowTerm
import Lean

open Lean Elab Tactic Meta

open Std.Tactic.TryThis (delabToRefinableSyntax addSuggestion)

def CalcProof := Expr × Array (Expr × Expr)

def delabCalcProof : CalcProof → MetaM (TSyntax `tactic)
  | (lhs, steps) => do
  let lhsStx ← delabToRefinableSyntax lhs
  let firstStep ← `(calcFirstStep| $lhsStx:term )
  let stepStx ← steps.mapM fun (proof, rhs) => do
    `(calcStep|_ = $(← delabToRefinableSyntax rhs) := $(← delabToRefinableSyntax proof))
  `(tactic|calc $lhsStx:calcFirstStep $[$stepStx:calcStep]*)

More generally, could lean give more helpful guidance here than just

unexpected token '$'; expected ')'

somehow?

For reference:

-- first step of a `calc` block
syntax calcFirstStep := ppIndent(colGe term (" := " term)?)
-- enforce indentation of calc steps so we know when to stop parsing them
syntax calcStep := ppIndent(colGe term " := " term)
syntax calcSteps := ppLine withPosition(calcFirstStep) withPosition((ppLine linebreak calcStep)*)
syntax (name := calc) "calc" calcSteps : term

[Joachim Breitner]

Ok, this seems to work. Indentation matters, it seems…

import Std.Tactic.TryThis
import Std.Tactic.ShowTerm
import Lean

open Lean Elab Tactic Meta

open Std.Tactic.TryThis (delabToRefinableSyntax addSuggestion)

def CalcProof := Expr × Array (Expr × Expr)

def delabCalcProof : CalcProof → MetaM (TSyntax `tactic)
  | (lhs, steps) => do
  let stepStx ← steps.mapM fun (proof, rhs) => do
    `(calcStep|_ = $(← delabToRefinableSyntax rhs) := $(← delabToRefinableSyntax proof))
  `(tactic|calc
      $(← delabToRefinableSyntax lhs):term
      $stepStx*)