Syntax quotation for a tuple

Stream: lean4 dev

[Joachim Breitner]

I have an Array Syntax, and I want to create the syntax for a tuple, (b,c,d). How do I do that? Here is what I tried

import Mathlib.Tactic.RunCmd

set_option autoImplicit false

run_cmd liftTermElabM do
    let vs ← (List.range 3).mapM fun n => `(x)
    let body ← `(term| ( $[$vs],* ) )
    logInfo "{vs} {body}"

[Joachim Breitner]

I guess I can use docs#Lean.Elab.Term.Quotation.mkTuple instead of using quotation syntax (but still curious how that would work)

[Joachim Breitner]

(deleted)

[Kyle Miller]

The syntax for tuples is "(" term ", " sepBy1(term, ", ") ")", so you have to handle three cases.

import Mathlib.Tactic.RunCmd

open Lean

def mkTuple {m : Type → Type} [Monad m] [Lean.MonadQuotation m]
    (xs : Array Term) : m Term :=
  match xs.size with
  | 0 => `(())
  | 1 => pure xs[0]!
  | _ =>
    let x := xs[0]!
    let xs' := xs.extract 1 xs.size
    `(term| ($x, $xs',*))

run_cmd Elab.Command.liftTermElabM do
    let vs ← (List.range 3).toArray.mapM fun n => `(x)
    let body ← mkTuple vs
    logInfo m!"{vs} {body}"

[Kyle Miller]

If you know your array has length >= 2 then you could jump right into this third case, but you have to split your array up like this. Probably easier to use Lean.Elab.Term.Quotation.mkTuple.

[Joachim Breitner]

Thanks! I ended up with this: https://github.com/leanprover/lean4/blob/e8b6cb330547201ecb049bc9bb91d0ee50fada53/src/Lean/Elab/PreDefinition/WF/GuessLex.lean#L606

Will refine with how you do the separators later!

[Kyle Miller]

Huh, I didn't know that subarrays could be spliced. The third case in my code can just be | _ => `(term| ($(xs[0]!), $(xs[1:]),*)) then

[Joachim Breitner]

I assume it's just syntax for extract?

[Kyle Miller]

Nope, it gives a Subarray, which is an array along with a start and stop index, so potentially it's a bit more efficient.

[François G. Dorais]

But Lean has an unusual coercion from Subarray to Array which severely limits the efficiency.