pattern matching in macros

Stream: new members

[Abhinav Menon]

Hello! I was trying to extend the example given here, to include arbitrary sequences of balanced sequences (e.g. {}{}{}). The modified code is

inductive Dyck : Type where
  | seq : List Dyck → Dyck
  | round : Dyck → Dyck
  | curly : Dyck → Dyck
  | leaf : Dyck

declare_syntax_cat brack

syntax "end" : brack
syntax "(" brack ")" : brack
syntax "{" brack "}" : brack
syntax brack "-" brack : brack

syntax "`[Dyck| " brack "]" : term

macro_rules
  | `(`[Dyck| end]) => `(Dyck.leaf)
  | `(`[Dyck| ($b)]) => `(Dyck.round `[Dyck| $b])
  | `(`[Dyck| {$b}]) => `(Dyck.curly `[Dyck| $b])
  | `(`[Dyck| $b-$c]) =>
    match `(`[Dyck| $c]) with
     | `(Dyck.seq brackseq) => `(Dyck.seq (List.cons `[Dyck| $b] brackseq))
     | _ => `(Dyck.seq (List.cons `[Dyck| $b]
                       (List.cons `[Dyck| $c]
                       List.nil)))

However, the match ... line gives the following error:

typeclass instance problem is stuck, it is often due to metavariables

Is this the right way to pattern match on a macro expansion?

[Abhinav Menon]

cc @Jatin Agarwala

[Arthur Paulino]

Here:

inductive Dyck : Type where
  | seq : List Dyck → Dyck
  | round : Dyck → Dyck
  | curly : Dyck → Dyck
  | leaf : Dyck

declare_syntax_cat brack

syntax "end" : brack
syntax "(" brack ")" : brack
syntax "{" brack "}" : brack
syntax brack "-" brack : brack

syntax "`[Dyck| " brack "]" : term

macro_rules
  | `(`[Dyck| end]) => `(Dyck.leaf)
  | `(`[Dyck| ($b)]) => `(Dyck.round `[Dyck| $b])
  | `(`[Dyck| {$b}]) => `(Dyck.curly `[Dyck| $b])
  | `(`[Dyck| $b-$c]) =>
    match c with
     | `(Dyck.seq brackseq) => `(Dyck.seq (List.cons `[Dyck| $b] brackseq))
     | _ => `(Dyck.seq (List.cons `[Dyck| $b]
                       (List.cons `[Dyck| $c]
                       List.nil)))

[Arthur Paulino]

You might want the dollar symbol before brackseq on this line:

| `(Dyck.seq $brackseq) => `(Dyck.seq (List.cons `[Dyck| $b] $brackseq))

Also notice that the code above compiles, but you haven't defined a syntax for sequences of brackets (you probably know this since you literally matched with `(Dyck.seq brackseq))