Missing Unexpanders for Core Functions?

Stream: lean4

[Mac]

I noticed that Lean is missing unexpanders for a lot of basic functions. For example, Array.empty and Array.push. Is there any reasons why defining unexpanders like the following would be a problem?

@[appUnexpander Array.empty]
def unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander
| `($_f:ident) => `(#[])
| _  => throw ()

@[appUnexpander Array.push]
def unexpandArrayPush : Lean.PrettyPrinter.Unexpander
| `($_f:ident #[] $x) => `(#[$x])
| `($_f:ident #[$xs,*] $y) => `(#[$xs,*, $y])
| _  => throw ()

[Daniel Selsam]

@Mac What problem are you trying to solve? Notation already unexpands nicely. Why would you want to unexpand pushes that way?

[Daniel Selsam]

Note: Array notation is defined in terms of List:

set_option pp.notation false
#check (#[] : Array Nat) -- List.toArray List.nil : Array Nat
#check (#[1] : Array Nat) -- List.toArray (List.cons 1 List.nil) : Array Nat

[Mac]

The goal is to pretty-print sequence of pushes. The reason why this is relevant is that sequences of pushes are often used to construct arrays in some macro code (and such arrays end up being less than pretty).

[Daniel Selsam]

how about reducing the result explicitly, rather than having the pretty-printer do it?

[Mac]

Maybe Array is a bad example. A better example of something that does not get pretty printed ever is Name:

#check `foo.bar
/-
  Name.mkStr (Name.mkStr Name.anonymous "foo") "bar" : Name
-/

I would hope it would be pretty-printed as `foo.bar .

[Mac]

Also, fyi, using #reduce on an Array doesn't result in a pretty literal either:

#reduce #[2, 3]
/-
 { data := [2, 3] }
-/

[Daniel Selsam]

I don't know why the devs decided to represent Array literals this way, but given that decision, I think it would be confusing to have different representations of arrays that all pretty-print the same way.

[Daniel Selsam]

I meant reducingconverting the array to whatever the canonical representation is, which is currently the List.toArray <list> representation.

[Mac]

Daniel Selsam said:

I meant reducingconverting the array to whatever the canonical representation is, which is currently the List.toArray <list> representation.

Unfortunately, that is often not possible. Many built-in pieces use the push representation and thus errors are not very pretty. For example:

open Lean Syntax in
def badArrayQuote : Syntax -> Syntax
  := fun _ => `( #[2, 3] )
/-
  type mismatch
    do
      let info ← MonadRef.mkInfoFromRefPos
      let scp ← getCurrMacroScope
      let mainModule ← getMainModule
      pure
          (node (Name.mkStr Name.anonymous "term#[_,]")
            (Array.push
              (Array.push (Array.push Array.empty (atom info "#["))
                (node (Name.mkStr Name.anonymous "null")
                  (Array.push
                    (Array.push
                      (Array.push Array.empty
                        (node (Name.mkStr Name.anonymous "numLit") (Array.push Array.empty (atom info "2"))))
                      (atom info ","))
                    (node (Name.mkStr Name.anonymous "numLit") (Array.push Array.empty (atom info "3"))))))
              (atom info "]")))
  has type
    ?m.1784 Syntax : Type
  but is expected to have type
    Syntax : Type
-/

[Mac]

In fact, the above is a great example of why both Array and Name unexpanders would be quite desirable.

[Mac]

The ones I've written on my own produce the following:

open Lean Syntax in
def prettyBadArrayQuote : Syntax -> Syntax
  := fun _ => `( #[2, 3] )

/-
type mismatch
  do
    let info ← MonadRef.mkInfoFromRefPos
    let scp ← getCurrMacroScope
    let mainModule ← getMainModule
    pure
        (node `«term#[_,]»
          #[atom info "#[",
            node `«null» #[node `«numLit» #[atom info "2"], atom info ",", node `«numLit» #[atom info "3"]],
            atom info "]"])
has type
  ?m.51556 Syntax : Type
but is expected to have type
  Syntax : Type
-/

which is much cleaner in my opinion.

[Daniel Selsam]

That is a good example, thanks. I agree it would be nice for these to pretty-print as they do with your proposed unexpanders. I am still a little concerned about having different Array representations all rendering the same way though. Perhaps the Array.push representation can become the standard?

[Mac]

I can understand the qualms with having the toArray and push print the same way.

However, I would note that Array.empty and List.toArray [] are defeq:

example : (Array.empty : Array a) = List.toArray [] := rfl

So I don't think there would be as much as problem for them to print the same way.

[Mac]

For my particular example (quoting), I think the pretty printing issues boil down to the fact that the Quote instance for Array and Name don't use the current canonical representation of those types (Array uses empty/push instead of toArray and Name uses mkStr instead of a name literal). This could be resolved by either changing the current canonical representation to match Quote or changing Quote to match the current canonical representation.

[Sebastian Ullrich]

Yeah, I'm not satisfied with the pretty printed macro output either. Printing defeq things the same way is not a good idea though since tactics like simp don't work modulo defeq. Probably we should just move List.toArray to Prelude so we can use it in the quotation implementation.

[Mario Carneiro]

Printing defeq things the same way is not a good idea though since tactics like simp don't work modulo defeq.

Also there could be a performance or even behavior difference if one is a implementedBy constant and the other is the lean model (which is the case here re: Array.empty vs List.toArray [])

[Sebastian Ullrich]

List.toArray actually is the faster one here (if everything is inlined) because it uses Array.mkEmpty with an appropriate capacity