Zulip Chat Archive

Stream: lean4 dev

Topic: Syntax quotation for a tuple


Joachim Breitner (Nov 10 2023 at 15:44):

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 (Nov 10 2023 at 16:11):

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 (Nov 10 2023 at 16:30):

(deleted)

Kyle Miller (Nov 17 2023 at 19:09):

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 (Nov 17 2023 at 19:10):

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 (Nov 17 2023 at 19:29):

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 (Nov 17 2023 at 19:50):

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 (Nov 17 2023 at 19:52):

I assume it's just syntax for extract?

Kyle Miller (Nov 17 2023 at 19:53):

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 (Nov 17 2023 at 20:00):

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


Last updated: Dec 20 2023 at 11:08 UTC