why does this array/list pattern match fail?

Stream: new members

[Alok Singh]

#eval match #[1, 2, 3] with
  | #[a, b, c] => a + b + c
  | #[a, c] => a  + c
  | #[a] => a
  | #[] => 0
  -- | _ => 0
/-
failed to compile pattern matching, stuck at
  remaining variables: [x✝:(Array ℕ)]
  alternatives:
    [a:(ℕ), b:(ℕ), c:(ℕ)] |- [#[a, b, c]] => h_1 a b c
    [a:(ℕ), c:(ℕ)] |- [#[a, c]] => h_2 a c
    [a:(ℕ)] |- [#[a]] => h_3 a
    [] |- [#[]] => h_4 ()
  examples:_

-/
#eval match [1, 2, 3] with
  | [_,_,_,_] => 4
  | [_,   _, _] => 3
  | [_,_] => 2
  | [_] => 1
  | [] => 0
  -- | _ => 0
-- missing cases: (List.cons _ (List.cons _ (List.cons _ (List.cons _ (List.cons _ _)))))

I have an idea of why but wanted to be sure. Is it that the pattern matcher does not have access to any length info, so it assumes any length array/list can be passed, so there needs to be a catchall for arbitrary length cases?

[Edward van de Meent]

yes, that seems right to me.

[Edward van de Meent]

if you want to match an exact number of values, you can use match (1,2,3) with |(a,b,c) => a+ b+ c

[Edward van de Meent]

i.e. match on a tuple, where lean can tell that indeed there is an exact number of items.

[Alok Singh]

makes sense, was curious about specifically array/list after reading that pattern matching supports array literals

[Alok Singh]

slight digression, if i wanted to write a custom pattern matcher, is that possible?

say for

structure Vector (a : Type) (n : Nat) where
  data : Array a
  _len : data.size = n

-- assume some literal syntax like (v[1,2,3] : Vector Nat 3) is defined

match v[1,2,3] with
| v[a,2,b] => b
| v[a,b,c] => 3
-- no catch all needed

[Mario Carneiro]

you are matching on an array here, so of course the longer arrays have to be handled?

[Mario Carneiro]

No, there is no way to extend the pattern language currently, the match compiler is not extensible

[Mario Carneiro]

you can make macros that fire in pattern position though

[Mario Carneiro]

Actually, I bet you could make that example work, although it probably won't generate very good code

[Mario Carneiro]

dang, so close and yet so far

import Batteries.Data.Vector

syntax (name := vecNotation) (priority := high) "#v[" withoutPosition(sepBy(term, ", ")) "]" : term

namespace Batteries.Vector
open Lean Elab Term in
@[term_elab vecNotation]
def elabVectorNotation : TermElab := fun stx ty => do
  match stx with
  | `(#v[ $elems,* ]) =>
    if (← read).inPattern then
      elabTerm (← `(Vector.mk (n := $(quote elems.getElems.size)) ⟨[$elems,*]⟩ _)) ty
    else
      elabTerm (← `(Vector.mk (n := $(quote elems.getElems.size)) ⟨[$elems,*]⟩ rfl)) ty
  | _ => throwUnsupportedSyntax

#check
  match #v[1,2,3] with
  | #v[a,2,b] => b -- invalid pattern
  | #v[a,b,c] => 3

It doesn't work because match only expands macros, not elabs, and macros are not given access to inPattern

[Alok Singh]

i'm very appreciative but a bit apprehensive that you're so nerd-snipable @Mario Carneiro

[Mario Carneiro]

what? that's, like, my thing

[Edward van de Meent]

it is? i thought that was yaels?

[Damiano Testa]

Oh, there are many nerds here...

[Alok Singh]

Damiano Testa said:

Oh, there are many nerds here...

understatement of the year

[Edward van de Meent]

like sniping nerds in a barrel

[Mario Carneiro]

this isn't even full on nerd sniped, it's a few lines of code. Full nerd sniping is writing a fix to lean core, and then belatedly making an RFC for that because that's what you need to do now

[Damiano Testa]

I can see where you are headed, Mario.

[Alok Singh]

well, he had to do it guys

[Edward van de Meent]

at least i never wrote a tool because i felt it was missing... ahem

[Mario Carneiro]

TBH I'm not headed there, it's the part of the process that is not fun

[Mario Carneiro]

the actual way to do this kind of thing now is to hint to FRO members that it's a worthwhile problem and then maybe later it will show up on the lean commit feed

[Edward van de Meent]

transitive nerdsniping?

[Mario Carneiro]

remote sniping