macro v/s typeclass resolution

Stream: lean4

[Siddharth Bhat]

How do I write a macro which captures something like "x" + "y" into an abstract syntax tree? Currently, it appears to cause a typeclass lookup for the HAdd typeclass. Here's a minimal example of what I want:

-- Controlling typeclass resolution versus macros
inductive Arith: Type :=
   | Add : Arith -> Arith -> Arith
   | Symbol : String -> Arith

declare_syntax_cat arith
syntax term : arith
syntax  arith "+" arith : arith

syntax "fromArith% " arith : term

macro_rules
  | `(fromArith% $sym:term) => `(Arith.Symbol $sym)
  | `(fromArith% $x:arith + $y:arith ) => `(Arith.Add (fromArith% $x) (fromArith% $y))

macro "arith" n:ident "->" e:arith  : command =>
   `(def $n:ident : Arith := fromArith% $e)

arith baz -> "x" + "y"
#print baz

I would like the answer to be:

def baz : Arith :=
Arith.Add (Arith.Symbol "x") (Arith.Symbol "y")

I currently get the error:

add.lean:19:13: error: failed to synthesize instance
  HAdd String String ?m.1645
def baz : Arith :=
Arith.Symbol (sorryAx String)

[Mario Carneiro]

I think you have to specify the precedence here, because in the expression fromArith% "x" + "y" it could mean either fromArith% ("x" + "y") or (fromArith% "x") + "y", and it seems lean is going for the latter interpretation, which is not what you want

[Mario Carneiro]

Additionally, you have an ambiguity due to the syntax term : arith rule, since then even fromArith% ("x" + "y") can be interpreted as fromArith% ("x" + "y" : term)

[Mario Carneiro]

Testing reveals that this latter version is how it is actually getting interpreted

[Mario Carneiro]

The simplest fix is something like this:

declare_syntax_cat arith
syntax strLit : arith
syntax arith "+" arith : arith

syntax:max "fromArith% " arith : term

macro_rules
  | `(fromArith% $sym:strLit) => `(Arith.Symbol $sym)
  | `(fromArith% $x:arith + $y:arith ) => `(Arith.Add (fromArith% $x) (fromArith% $y))

macro "arith" n:ident "->" e:arith  : command =>
   `(def $n:ident : Arith := fromArith% $e)

arith baz -> "x" + "y"
#print baz

[Siddharth Bhat]

Ah, strLit is handy to know. I wonder if there's a place to find all of the core syntax categories?

[Leonardo de Moura]

If you want to use identifiers, you can add the following lines after Mario's example above.

syntax ident : «arith»  -- Have to use french quotes since `arith` is now a keyword

macro_rules
  | `(fromArith% $x:ident) => `(Arith.Symbol $(Lean.quote (toString x.getId)))

arith foo -> x + y + z
#print foo

syntax "{" term "}" : «arith» -- escape for embedding terms into `Arith`

macro_rules
  | `(fromArith% { $e }) => e

arith boo -> x + y + {foo}
#print boo