Pattern matching syntax for Array.last/Array.pop

Stream: Is there code for X?

[Joachim Breitner]

I just changed some very elegant code using lists (with pattern matching) to implement a stack to slightly less elegant code using Arrays (with Array.last, Array.pop). I would be less sad if I could still use pattern matching syntax, something like

def foo : Array a  → …
  | #[] -> …
  | #[as... a] → …

Could that be made to work somehow? I noticed that empty and fixed-length arrays already work in patterns.

[Joachim Breitner]

And maybe related: How does #[] in patterns even work? I see

syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term

macro_rules
  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])

and I understand how that works in terms, but for this to work in patterns it seems that lean has to support the function callList.toArray [ x ] in a pattern position…

Ah, maybe its related to the match_pattern attribute at

@[inline, match_pattern, export lean_list_to_array]
def List.toArray (as : List α) : Array α :=

where the docs say

When identifiers are marked with the [match_pattern] attribute, the equation compiler unfolds them in the hopes of exposing a constructor. For example, this makes it possible to write n+1 and 0 instead of Nat.succ n and Nat.zero in patterns.

Hmm, but this attribute probably cannot be used to implement the “view patterns” I would like to see. Too bad.

[Mario Carneiro]

Joachim Breitner said:

And maybe related: How does #[] in patterns even work?

A dirty hack

[Mario Carneiro]

If #[...] was syntax for Array.mk [...] instead of List.toArray [...] the hack wouldn't even be necessary

[Mario Carneiro]

this also messes up exhaustiveness checking:

example : Array Nat → Unit
  | #[] => ()
  | ⟨a :: as⟩ => ()

failed to compile pattern matching, stuck at
  remaining variables: [x✝:(Array Nat)]
  alternatives:
    [] |- [#[]] => h_1 ()
    [a:(Nat), as:(List Nat)] |- [(Array.mk (List.cons a as))] => h_2 a as
  examples:_