adding ellipsis to a term

Stream: lean4

[Patrick Massot]

I have some syntax x : term and I would like to create the syntax x .. adding an ellipsis. This works as I would expect it only sometimes. If x is already a Term.app, my naive attempt creates a nested Term.app instead of a single app with multiple arguments. How can I do this reliably?

[Patrick Massot]

If this is not clear enough, here is a mwe:

variable (f : Nat → Nat → Nat)

elab "do_nothing" x:term : command => do
  dbg_trace x

elab "add_ellipsis" x:term : command => do
  let y ← `($x ..)
  dbg_trace y

add_ellipsis f
do_nothing f ..
add_ellipsis f 1
do_nothing f 1 ..

[Patrick Massot]

My hope would be to have add_ellipsis f 1 and do_nothing f 1 .. to return the same thing, just as add_ellipsis f and do_nothing f .. return the same thing.

[Damiano Testa]

I'm not at a computer, but I wonder if you should push the .. at the end of the x.getArgs array, instead of using the `() constructor for the syntax.

[Eric Wieser]

Is there a reason you care about the difference here? One reason to prefer the nested .app is to distinguish the application in the source code from the the one you created synthetically

[Kyle Miller]

Maybe jumping a head a bit, you can make a term elaborator for this:

import Lean

open Lean Elab Term

def expandApp' (stx : Syntax) : MetaM (Syntax × Array NamedArg × Array Arg × Bool) := do
  if stx.isOfKind ``Parser.Term.app then
    expandApp stx
  else
    return (stx, #[], #[], false)

syntax (name := addEllipsis) "add_ellipsis" term : term

@[term_elab addEllipsis]
def elabAddEllipsis : TermElab
  | `(add_ellipsis $x) => fun expectedType? => do
    let (f, namedArgs, args, _ellipsis) ← expandApp' x
    elabAppArgs (← elabTerm f none) namedArgs args expectedType? (explicit := false) (ellipsis := true)
  | _ => fun _ => throwUnsupportedSyntax

variable (f : Nat → Nat → Nat)

#check add_ellipsis f -- f ?m.1103 ?m.1104 : Nat
#check add_ellipsis f 1 -- f 1 ?m.1122 : Nat
#check add_ellipsis f 1 2 -- f 1 2 : Nat

[Kyle Miller]

There's probably a cleaner way to do it, but here's a function that tacks on .. if it's not already present.

import Lean

open Lean Elab Term

def withEllipsis (stx : Term) : Term := Unhygienic.run <| withRef stx do
  if stx.raw.isOfKind ``Parser.Term.app then
    if stx.raw[1].getArgs.back.isOfKind ``Parser.Term.ellipsis then
      return stx
    else
      let ellipsis ← `(Parser.Term.ellipsis| ..)
      return ⟨stx.raw.modifyArg 1 fun arg => arg.modifyArgs fun args => args.push ellipsis⟩
  else
    `($(⟨stx⟩) ..)

macro "add_ellipsis " x:term : term => return withEllipsis x

variable (f : Nat → Nat → Nat)

#check add_ellipsis f -- f ?m.1103 ?m.1104 : Nat
#check add_ellipsis f 1 -- f 1 ?m.1122 : Nat
#check add_ellipsis f 1 2 -- f 1 2 : Nat

[Thomas Murrills]

Nice! I recently had to make a (repeated) syntax app myself; I opted for nested apps, but maybe it’s worth having e.g. Term.mkAppN (and Term.mkApp) somewhere which does it this way.