mix and match matching on Syntax

Stream: lean4

[Damiano Testa]

Below, you can see the two ways in which I typically match on syntax. Is there a way of mixing the two matchings in a single pattern?

import Lean

open Lean Elab Command

-- works and can be extended by more `(...)
example : Syntax →  Syntax
  | s@`(a + b) => s
  | s => s

-- works and can be extended by more .atom, .node, ...
example : Syntax →  Syntax
  | .ident _ _ v _ => mkIdent v
  | s => s

-- does not work
example : Syntax →  Syntax
  | s@`(a + b) => s
  | .ident _ _ v _ => mkIdent v
  | s => s
/-
match (syntax) : unexpected pattern kind .ident _ _ v _
-/

[Eric Wieser]

(and similarly for TSyntax with ⟨.ident _ _ _ _⟩)

[Damiano Testa]

I am comforted that one of the native Lean-speakers does not know of this feature! :smile:

[Eric Wieser]

I'm pretty sure it's just missing, for the same reason that I think you can't match on syntax and other arguments at the same time?

[Damiano Testa]

Ah, that I never tried!

[Eric Wieser]

I bet you can trick it by adding a ~q match to the same match

[Damiano Testa]

I am not sure that I understand what you have in mind, but both of these work:

-- works
example : Syntax → Unit →  Unit
  | s, t => t

-- works
example (s : Syntax) (u : Unit) :  Unit :=
  match s, u with
    | .node .., t => t
    | _, t => t

[Eric Wieser]

Does the one with a syntax antiquotation match work?

[Damiano Testa]

I think so:

-- works
example (s : Syntax) (u : Unit) :  Unit :=
  match s, u with
    | `(a + b), t => t
    | _, t => t

seems to work.

[Damiano Testa]

I wonder what happens if you match on two syntaxes, one with anti-quotations on one with constructors...

[Damiano Testa]

Ok, for completeness, this is what happens:

open Lean

-- does not work
example : Syntax → Syntax → Unit
  | `(a + b), .node .. => ()
  | _, t => ()

-- does not work
example : Syntax → Syntax → Unit
  | .node .., `(a + b) => ()
  | _, _ => ()

-- works
example : Syntax → Syntax → Unit
  | .node .., .node .. => ()
  | _, _ => ()

-- works
example : Syntax → Syntax → Unit
  | `(a * b), `(a + b) => ()
  | _, _ => ()

[Mario Carneiro]

This will require rearchitecting the way match works to fix

[Damiano Testa]

Ok, it is not that important: the constructor matching works, it is just more verbose at times.

[Mario Carneiro]

you can usually refactor it into separate matches to get the desired mix and match

[Eric Wieser]

Eric Wieser said:

I bet you can trick it by adding a ~q match to the same match

Yep:

import Qq
open Lean Qq

-- works
example (s1 : Syntax) (s2 : Syntax) : MetaM Unit :=
  match s1, s2, q(trivial) with
  | `(a + b), .node .., ~q(trivial) => return ()
  | _, t, _ => return ()

-- works
example (s1 : Syntax) (s2 : Syntax) : MetaM Unit :=
  match s1, s2, q(trivial) with
  | .node .., `(a + b), ~q(trivial) => return ()
  | _, _, _ => return ()

[Eric Wieser]

Damiano Testa said:

I think so:

-- works
example (s : Syntax) (u : Unit) :  Unit :=
  match s, u with
    | `(a + b), t => t
    | _, t => t

seems to work.

This fails if you replace t => with () => ()(or any other pattern that actually does work); so I think my original claim is basically correct