Delaborating !![] notation

Stream: mathlib4

[Eric Wieser]

I am trying to write a delaborator for !![] notation, but I fairly immediately run into trouble when trying to generate syntax:

import Mathlib.Data.Matrix.Notation

open Lean PrettyPrinter.Delaborator SubExpr Qq
@[delab app.DFunLike.coe]
def delabMatrixOf : Delab :=
  whenPPOption getPPNotation <| do
    let e ← getExpr
    let ⟨_, ~q(Matrix (Fin (OfNat.ofNat $n)) (Fin (OfNat.ofNat $m)) $α), ~q(Matrix.of $e)⟩ ← inferTypeQ' e | failure
    let some m := m.natLit? | failure
    let some n := n.natLit? | failure
    if m = 0 then
      let semicolons : Term := ⟨mkNullNode <| .mk <| List.replicate n <| Syntax.atom (← MonadRef.mkInfoFromRefPos)  ";"⟩
      return (← `(!![$semicolons]))
    failure

#check !![;;]

Is there any way to use syntax quotations to build the repeated ;s?

[Mario Carneiro]

#mwe

[Eric Wieser]

Edited above, sorry

[Mario Carneiro]

for the case other than 0xN or Nx0 I would bet you can do it, but sequences of atoms don't really work well with syntax quotations

[Mario Carneiro]

I guess that's the case you are having issues with

[Eric Wieser]

I didn't even try the nondegenerate cases, but I agree that they sound a little easier

[Mario Carneiro]

actually, the same syntax used to parse them seems to work to generate them too:

    if m = 0 then
      let semicolons := Array.mkArray n (← getRef)
      return (← `(!![$[;%$semicolons]*]))
    failure

#check !![;;]

[Eric Wieser]

Wow, I would not have expected % to accept an array

[Mario Carneiro]

well, it's the $[...]* that generates an array

[Mario Carneiro]

all of the bindings inside that are array-ified

[Eric Wieser]

Mario Carneiro said:

well, it's the $[...]* that generates an array

What documentation could I read to learn this?

[Mario Carneiro]

good question

[Mario Carneiro]

I'm not aware of any documentation that covers quotation syntax, which is bad since it's so arcane

[Mario Carneiro]

well it's always bad not to have docs but it's especially bad when it's rarely used and sigil heavy