Redundant brackets in syntax function application

Stream: metaprogramming / tactics

[Paul Lezeau]

I'm currently writing a metaprogram that takes a function f with a variable number of inputs, and applies it to several of these inputs (the number of which may vary) by manipulating the corresponding syntax. Is there an easy way of doing this without ending up with redundant brackets when pretty printing the resulting syntax?
As an example, when running

import Lean

run_cmd do
  let myFun ← `(term| fun a b ↦ 0)
  let x ← `(term | 2)
  let y ← `(term | 3)
  let myAppliedFun ← `(term | $myFun $x)
  let myAppliedFun ← `(term | $myAppliedFun $y)
  Lean.logInfo myAppliedFun

the output is ((fun a✝ b✝ ↦ 0) 2) 3 and I'm looking for an easy way to get (fun a✝ b✝ ↦ 0) 2 3 instead.
(of course in this example this can be achieved by writing

let myAppliedFun ← `(term | $myFun $x $y)

instead of

let myAppliedFun ← `(term | $myFun $x)
let myAppliedFun ← `(term | $myAppliedFun $y)

but I'm looking for a solution that would generalize to a variable number of inputs:))

[Damiano Testa]

This works, but feels too low level:

import Lean

open Lean

/-- info: (fun a✝ b✝ ↦ 0) 2 3 -/
#guard_msgs in
run_cmd do
  let myFun ← `(term| (fun a b ↦ 0))
  let x ← `(2)
  let y ← `(3)
  let xy := mkNullNode #[x, y]
  let fxy := Syntax.node default ``Parser.Term.app #[myFun, xy]
  logInfo fxy

[Damiano Testa]

And then you can do:

/-- info: (fun a✝ b✝ ↦ 0) 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 -/
#guard_msgs in
run_cmd do
  let myFun ← `(term| (fun a b ↦ 0))
  let mut vars := #[]
  for i in [:20] do
    vars := vars.push (Syntax.mkNumLit s!"{i}")
  let xy := mkNullNode vars
  let fxy := Syntax.node default ``Parser.Term.app #[myFun, xy]
  logInfo fxy

[Eric Wieser]

import Lean

run_cmd do
  let myFun ← `(term| fun a b ↦ 0)
  let x ← `(term | 2)
  let y ← `(term | 3)
  let args := #[x, y]
  let myAppliedFun ← `(term | $myFun $args*)
  Lean.logInfo myAppliedFun

[Damiano Testa]

Ah, I was trying to put the square brackets inside the antiquotation and failed in all my attempts!

[Eric Wieser]

That would be `(term | $myFun $(#[x, y])*)

[Damiano Testa]

Thanks! My mistake was using $ instead of # for the array. :man_facepalming:

[Paul Lezeau]

Nice, thanks a lot!