fail with reference to term

Stream: lean4

[Heather Macbeth]

I'd like to write a failure message which references a term I have. I guessed a syntax but I guessed wrongly:

syntax "foo " term : tactic

macro_rules | `(tactic| foo $a) => `(tactic | fail "foo {$a} failed")

[Kyle Miller]

Here's the best I could come up with:

import Lean

syntax "foo " term : tactic

open Lean Elab.Tactic

elab "fail_tactic " t:tactic : tactic => do
  let goals ← getGoals
  let goalsMsg := MessageData.joinSep (goals.map MessageData.ofGoal) m!"\n\n"
  throwError "tactic '{t}' failed\n{goalsMsg}"

macro_rules | `(tactic| foo $_) => do `(tactic | fail_tactic $(⟨← getRef⟩))

example : 1 + 1 = 2 := by foo 12 + 13
/-
tactic 'foo 12 + 13' failed
⊢ 1 + 1 = 2
-/

[Kyle Miller]

I couldn't find a way to embed $a into the string for fail and also pretty print it (I'm not under the impression that macros have access to the pretty printer)

[Kyle Miller]

For example,

macro_rules | `(tactic| foo $a) => do
  let msg := s!"'{a}' failed"
  `(tactic | fail $(Lean.Syntax.mkStrLit msg))

example : 1 + 1 = 2 := by foo 12 + 13
/-
'(«term_+_» (num "12") "+" (num "13"))' failed
⊢ 1 + 1 = 2
-/

[Heather Macbeth]

Thanks Kyle for the detailed explanation!