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