Writing a Macro
New syntax for a term, tactic, command can be easily added in Lean. The easiest way to do this is to write a macro that transforms the new syntax into existing syntax. In this recipe, we show how to write macros for new syntax for terms and commands.
We will start with a simple example of parsing Python exponentiation syntax and then move on to the more complex example of parsing Python for loop syntax.
Syntax for Python exponentiation
We will start with a simple example for parsing Python exponentiation syntax in Lean. The following macro declaration tells Lean how to parse something of the form 2**4 and expands it into Lean's exponentiation syntax.
macro n:num "**" m:num : term => `($n^$m)
#eval 2**3 --8
Here, num is a parser that accepts strictly numeric literals and rejects everything else.
Syntax for Python for loop
In Python, list comprehensions provide a concise way to create lists. For example, the expression [x^2 for x in [1,2,3,4,5]] generates a list of the squares of the first five natural numbers. We will define similar syntax in Lean and then implement the logic to evaluate it.
In Lean, this can be accomplished by using the List.map function.
#eval List.map (fun x => x * x) [1, 2, 3, 4]
A macro that parses Python-like for loop
Next, we define a macro that lets us write syntax similar to Python syntax in Lean. It parses expressions of the form [<term> pyfor <ident> in <term>] and transforms them into a standard Lean expression using List.map. The ident is a placeholder for the variable name used in the comprehension, and the two term placeholders represent the expression being generated and the collection being iterated over. To avoid conflicts with the for keyword in Lean, we use pyfor instead.
macro "[" t:term "pyfor" x:ident "in" l:term "]": term => do
let fn ← `(fun $x => $t)
`(List.map $fn $l)
#eval [x * 2 pyfor x in [1, 2, 3, 4]] --> [2, 4, 6, 8]
If you prefer to separate the syntax declaration from the macro expansion, Lean also lets you define the syntax first with syntax and then add macro rules separately.
syntax "[" term "pyfor'" ident "in" term "]" : term
macro_rules
| `([ $t:term pyfor' $x:ident in $l:term ]) => do
let fn ← `(fun $x => $t)
`(List.map $fn $l)
The macro_rules command is used to pattern-match on our custom syntax and define exactly how it should be translated (or "expanded") into standard Lean code. In this case, we take the term t, the identifier x, and the list l from our custom syntax and construct a new expression that applies List.map to a lambda function fn(created from t and x) and the list l.
Macros only act as syntactic sugar and are only expanded to a different "already-existing" syntax. In a later recipe, An elaborator that parses Python-like for loop, we will see how to write an elaborator that parses the same syntax and performs additional checks during elaboration.