Matchin on syntax with group

Stream: lean4

[Joachim Breitner]

I have

syntax (name := find_theorems)
  withPosition("#find_theorems" (colGt (strLit <|> ident <|> term:max))+) : command

and it works, and I want to extend it to

syntax (name := find_theorems)
  withPosition("#find_theorems" (colGt (strLit <|> ident <|> ("⊢ " term:max) <|> term:max))+) : command

This is accepted, but if I then use

#find_theorems ⊢ (tsum _ = _) (_ * _ ^ _)

I get

elaboration function for 'group' has not been implemented
  [Error pretty printing syntax: unknown constant 'group'. Falling back to raw printer.]
  (group "⊢" (Term.paren "(" («term_=_» (Term.app `tsum [(Term.hole "_")]) "=" (Term.hole "_")) ")"))

I am parsing the argument list like this so far:

    for s in stx[1].getArgs do
      match s with
      | `($ss:str) => do
        let str := Lean.TSyntax.getString ss
        name_pats := name_pats.push str
      | `($i:ident) => do
        let n := Lean.TSyntax.getId i
        unless (← getEnv).contains n do
          throwErrorAt i "Name {n} not in scope"
        idents := idents.push n
      | `(group "⊢" $st:term) => do
        let t ← Lean.Elab.Term.elabTerm st none
        terms := terms.push (true, t)
      | _ => do
        let t ← Lean.Elab.Term.elabTerm s none
        terms := terms.push (false, t)

where the second-to-last clause is new. I found in the docs of <|> that it adds a group node if necessary, but I am unsure how to match it, or if I am approaching this the wrong way.

[Joachim Breitner]

I think I figured it out.

[Chris Bailey]

I'm running into this "match on group" thing now, was there a good solution? I would have thought an extra set of parens in the match would do the trick, but no cigar.

[Eric Wieser]

Do you have a mwe? I think Joachim's is too old to reflect the current state of Lean.

[Chris Bailey]

Sure, in this example I want to process a list of tuples/products. The repeated part is grouped in the syntax part as tuples:(..),*. When I go to try and match on the elements of the TSepArray, they present with this additional group wrapper that I can't seem to figure out how to match on, as evidenced by neither of the match arms hitting.

import Lean
open Lean Elab Command

elab "#goMany" "[" tuples:("(" num "," str ")"),* "]" : command => do
  for tuple in tuples.getElems do
    match tuple with
     | `(($a, $b)) => logInfo s!"OK 0"; return
     | `((($a, $b))) => logInfo s!"OK 1"; return
     | stx => throwError s!"failed to match: {stx}"


-- failed to match: (group "(" (num "0") "," (str "\"x\"") ")")
#goMany [
  (0, "x"),
  (1, "y")
]

[Aaron Liu]

You can also always just access the children directly

import Lean
open Lean Elab Command

elab "#goMany" "[" tuples:("(" num "," str ")"),* "]" : command => do
  for tuple in tuples.getElems do
    logInfo tuple.raw[1]
    logInfo tuple.raw[3]

#goMany [
  (0, "x"),
  (1, "y")
]

[Sebastian Ullrich]

Note that the default category of quotations is term, which is definitely incorrect here. So you need to specify the quotation parser, at which point you need to name it.

syntax pair := "(" num "," str ")"
elab "#goMany" "[" tuples:pair,* "]" : command => do
  for tuple in tuples.getElems do
    match tuple with
     | `(pair| ($a, $b)) => logInfo s!"OK 0"; return
     | stx => throwError s!"failed to match: {stx}"

[Chris Bailey]

Thanks, I didn't know you could now shortcut the declare_syntax_cat foo with just syntax foo either.