Macros: parse dyck grammar?

Stream: lean4

[Siddharth Bhat]

I'm trying to learn the LEAN4 macro system well enough to parse context-free grammars I'm interested in. I started with trying the dyck grammar / balanced parens.

Here's what I have so far:

inductive Dyck: Type :=
   | Round : Dyck -> Dyck
   | End : Dyck

declare_syntax_cat brack
syntax "End" : brack
syntax "(" brack ")" : brack
syntax "{" brack "}" : brack

macro "End" : term => `(Dyck.End)
macro "(" expr:brack ")" : term => `(Dyck.Round $expr)

syntax "brack" ident "->" brack : command

macro "brack" n:ident "End": command =>
   `(def $n : Dyck := End)

-- | macro that wants `( brack )`
macro "brack" n:ident "->" "(" e:brack ")" : command =>
   `(def $n : Dyck := Dyck.Round $e)

brack foo End
print foo

brack bar ( End )
print bar

Unfortunately, the line that attempts to parse "(" brack ")" fails with:

$ lean macros.lean
macros.lean:19:33: error: expected stx
macros.lean:19:39: error: expected identifier
macros.lean:20:9: error: expected identifier
macros.lean:23:0: error: expected command
macros.lean:25:10: error: expected '->' or 'End'

How should I write the macro such that parse and evaluate the "bracket language" correctly?

I'm on the nightly if it helps:

/home/bollu/work/2-mlir-verif$ ~/work/lean4-contrib/build/stage1/bin/lean --version
Lean (version 4.0.0, commit f4759c9a223f, Release)

[Mario Carneiro]

Your syntax looks like it expects a literal -> but you don't have that in your usage examples

[Mario Carneiro]

also you need #print foo instead of print foo

[Leonardo de Moura]

@Siddharth Bhat Not sure exactly what you are trying to do, but I think the following example may illustrate may idioms we use:

inductive Dyck: Type :=
   | Round : Dyck -> Dyck
   | End : Dyck

declare_syntax_cat brack
syntax "End" : brack
syntax "(" brack ")" : brack
syntax "{" brack "}" : brack

-- auxiliary notation for translating `brack` into `term`
syntax "fromBrack% " brack : term

macro_rules
  | `(fromBrack% End) => `(Dyck.End)
  | `(fromBrack% ( $b )) => `(fromBrack% $b)
  | `(fromBrack% { $b }) => `(Dyck.Round (fromBrack% $b))

-- Remark: after this command `brack` will be a "reserved" keyword, and we will have to use `«brack»`
-- to reference the `brack` syntax category
macro "brack" n:ident "->" e:brack  : command =>
   `(def $n:ident : Dyck := fromBrack% $e)

brack bar -> ( End )
#print bar
/-
def bar : Dyck :=
Dyck.End
-/
brack foo -> ( { { End } } )
#print foo
/-
def foo : Dyck :=
Dyck.Round (Dyck.Round Dyck.End)
-/

[Siddharth Bhat]

Thanks a lot, the example is super helpful! A question: is it possible to learn what the line

macro_rules
  | `(fromBrack% End) => `(Dyck.End)
  | `(fromBrack% ( $b )) => `(fromBrack% $b)
  | `(fromBrack% { $b }) => `(Dyck.Round (fromBrack% $b))

desugars into? I want to understand how to write everything in terms of the low level macro command, and I'm guessing there's a LEAN option to debug print macro expansions?

[Mario Carneiro]

the macro command is not low level, and in fact it desugars to syntax + macro_rules

[Mario Carneiro]

macro_rules desugars to a def with certain attributes

[Mario Carneiro]

and syntax also desugars to def with attributes

[Mario Carneiro]

macro is usable in the special case where the corresponding macro_rules has only one alternative

[Leonardo de Moura]

desugars into? I want to understand how to write everything in terms of the low level macro command, and I'm guessing there's a LEAN option to debug print macro expansions?

Everything Mario wrote is correct. You can see the definition that is sent to the Lean kernel by using the option

set_option trace.Elab.definition true in
macro_rules
  | `(fromBrack% End) => `(Dyck.End)
  | `(fromBrack% ( $b )) => `(fromBrack% $b)
  | `(fromBrack% { $b }) => `(Dyck.Round (fromBrack% $b))

[Leonardo de Moura]

If we use the option before the macro command, we will see two definitions: the parser and the macro expansion function.