3. Metaprogramming I: Syntax

‘Or else what?’ said Alice, for the Knight had made a sudden pause.
‘Or else it doesn’t, you know. The name of the song is called “Haddocks’ Eyes.”’
‘Oh, that’s the name of the song, is it?’ Alice said, trying to feel interested.
‘No, you don’t understand,’ the Knight said, looking a little vexed. ‘That’s what the name is called. The name really is “The Aged Aged Man.”’
‘Then I ought to have said “That’s what the song is called”?’ Alice corrected herself.
‘No, you oughtn’t: that’s quite another thing! The song is called “Ways and Means”: but that’s only what it’s called, you know!’
‘Well, what is the song, then?’ said Alice, who was by this time completely bewildered.
‘I was coming to that,’ the Knight said. ‘The song really is “A-sitting On A Gate”: and the tune’s my own invention.’

The last two chapters built a pipeline: strings into trees, trees through a checker into a core language, with definitional equality decided by evaluation. This chapter's reveal is that Lean has been running the same pipeline underneath us all along. A Lean file is parsed into a tree called Syntax, which is chapter 1 with a grown-up grammar; elaboration turns Syntax into a core term type called Expr, which is chapter 2 with metavariables; and a small trusted kernel replays the result, which is the checker again, stripped of convenience. Elaboration is the deterministic completion of everything humans leave out: implicit arguments, universe levels, instances, coercions. This chapter learns to hold the first tree in our hands; chapter 4 takes the second.

Syntax as data

A value of type Syntax is an ordinary inductive tree, and its shape would fit in chapter 1: a node carries a kind and an array of children; the leaves are atoms for keywords and literals, identifiers as their own leaf flavor, and a missing constructor for error recovery. The kind is just a name, auto-generated from the grammar rule that produced the node, and it is how every later stage dispatches. Grammar rules live in syntax categories: term for everything with a value, command for the top level, tactic inside by, and any number of user categories. The elaboration boundaries follow the categories: what stands after := is elaborated as a term, what begins a line at the top level as a command.

Nothing stops us from building the tree for 1 + 1 by hand, kind names, atoms, and all. A small macro splices the result into term position, and the #guard confirms the built tree elaborates and computes:

def onePlusOneSyntax : Syntax :=
  Syntax.node .none `«term_+_» #[
    Syntax.mkNumLit "1",
    Syntax.atom .none "+",
    Syntax.mkNumLit "1"
  ]

macro "onePlusOneRaw" : term =>
  pure ⟨onePlusOneSyntax⟩

#guard onePlusOneRaw == 2

The metaprogramming book, reaching this exact point, remarks: "If you don't like this way of creating Syntax at all you are not alone." The relief is quotation: inside `(...), write the surface syntax itself and the quoted tree is produced for you, kinds and positions included.

macro "onePlusOneQuoted" : term =>
  `(1 + 1)

#guard onePlusOneQuoted == 2

Syntax patterns

The same notation runs backwards, and the pair of directions deserves one name: these lectures call `(...) in all its forms a syntax pattern. In term position it constructs; in match position it destructs, with $x binding subtrees. One macro, two rules, and the rewriting of x + 0 happens during macro expansion, before the elaborator ever assigns the zero a meaning:

syntax "dropZero(" term ")" : term

macro_rules
  | `(dropZero($x + 0)) => `($x)
  | `(dropZero($x)) => `($x)

#guard dropZero(5 + 0) == 5
#guard dropZero(2 * 3) == 6

For a category other than term, the pattern names it explicitly: `(coin| heads) is a syntax pattern in the category coin. A fresh category is a closed grammar, disconnected from the rest of the language until a bridge rule embeds it. Both facts are visible in miniature, and so is something else: the syntax declarations below are BNF that runs. Set them next to the grammar they denote,

and the correspondence is line by line:

declare_syntax_cat coin

syntax "heads" : coin
syntax "tails" : coin

def coinToBool : TSyntax `coin -> MacroM (TSyntax `term)
  | `(coin| heads) => `(true)
  | `(coin| tails) => `(false)
  | _ => Macro.throwUnsupported

macro "flip " c:coin : term => coinToBool c

#guard flip heads == true
#guard flip tails == false

The function destructs coins by syntax pattern and constructs terms the same way; the bridge rule flip carries the closed category into term position. This shape, a category, its productions, a bridge, and pattern-driven translation, is exactly how chapter 5 makes the object language of these lectures resident in Lean, grammar and all.

What does one line of that running BNF cost without the sugar? A production is really a parser value registered to its category by an attribute, and even one layer down the ceremony shows; further layers down sit the parser state machines, which is chapter 1 built by hand all over again. Here is a third face for the coin, added the raw way:

open Lean.Parser in
@[coin_parser] def shiny : Parser :=
  leading_parser "shiny"

macro_rules
  | `(flip shiny) => `(true)

#guard flip shiny == true

One line of grammar became a definition, an attribute, and a macro rule. Multiply by every production in a real language, and that multiplication is why the syntax command exists.

Every metaprogramming object has three parts

The raw coin face just showed the pattern once, and it holds throughout Lean: every metaprogramming object is three declarations wearing one trench coat.

• the syntax: a parser for the new form, declared by a syntax rule, named with syntax (name := ...) or left to a generated kind name;
• the semantics: an ordinary function saying what the new form means;
• the registration: an attribute binding the function to the parser's kind.

All three, spelled out for a macro:

syntax (name := twiceStx) "twice! " term : term

def expandTwice : Macro
  | `(twice! $x) => `($x + $x)
  | _ => Macro.throwUnsupported

attribute [macro twiceStx] expandTwice

#guard (twice! 21) == 42

Everything else is bundling, and the bundle can be watched expanding. A macro_rules block is the same three declarations at a higher altitude: Lean derives the function from the match arms, registers it under the rule's kind, and quietly appends one more arm, | _ => Macro.throwUnsupported, so that anything the stated rules do not match falls through to any other macro registered for the same syntax:

syntax "thrice! " term : term

macro_rules
  | `(thrice! $x) => `($x + $x + $x)

#guard (thrice! 14) == 42

The macro command goes one step further and declares the syntax too, all three parts in one line; and the same trench coat fits elaborators, where the attribute says term_elab or command_elab instead of macro, and delaborators, tactics, and the rest of the zoo; the monads they all live in are chapter 4's subject. Knowing the three parts is what turns the sugar from magic into abbreviation.

To see that the coat really fits, here it is worn once by an elaborator: the semantics is an ordinary function of type TermElab, a shape the boundary section below spells out, and only the attribute name changes.

syntax (name := unitStx) "unit!" : term

open Lean Elab Term in
@[term_elab unitStx] def elabUnit : TermElab := fun _ _ =>
  return .const ``Unit.unit []

#guard unit! == ()

The coat comes in more sizes than the two just worn, and it is worth seeing the whole rack at once. Every kind of metaprogramming object in Lean is the same triple, a parser, a function, an attribute, and the kinds differ only in the function's type: what flows in, what flows out, and which monad carries the crossing. The registry, at a glance:

The shapes are not asserted, they are printed from the library, and two of them repay a closer look. The delaborator takes no argument at all: it reads the Expr under scrutiny from its monad's context rather than from a parameter. And the unexpander is the macro's mirror image, syntax to syntax on the way out, undoing at display time the sugar a macro spent at parse time; the monads these functions live in are chapter 4's subject, where the tactic row also stops being a mention and becomes code:

#print Lean.Macro

#print Lean.Elab.Term.TermElab

#print Lean.Elab.Command.CommandElab

#print Lean.Elab.Tactic.Tactic

#print Lean.PrettyPrinter.Delaborator.Delab

#print Lean.PrettyPrinter.Unexpander

Hygiene

A macro that introduces a binder ought to worry anyone who has substituted by hand. The constFn macro wraps its argument in fun x => ...; the argument mentions a global x; and nothing goes wrong:

macro "constFn " e:term : term => `(fun x => $e)

def x : Nat := 42

#guard (constFn x) 10 == 42

The user's x means 42 even inside a binder that spells its variable x, because quotation-introduced names carry macro scopes, invisible marks distinguishing them from anything the user wrote. The mechanism, hygienic macro expansion, is the subject of the Beyond Notations paper under Further reading. The marks cut both ways: a macro that wants to introduce a name visible to the user must strip them deliberately, with mkIdent, and chapter 5 meets the same issue from the other side when object-language binders arrive as Lean identifiers.

Macros and elaborators

Everything on this page so far is a macro: a function from syntax to syntax, run in a loop until the tree stops changing, before meaning is assigned. The other species is the elaborator, a function from syntax to meaning, Expr for terms. The division of labor is a design decision every metaprogram makes, and the community's rule of thumb is blunt: macros are for translations a human could write out by hand but is too lazy to; as soon as types or control flow are involved, it should be an elaborator. The #check_dtt command of chapter 2 was an elaborator for exactly that reason: it ran a parser and a checker, not a rewrite.

Laid end to end, the objects of the table above are one pipeline, and the overview chapter of the metaprogramming book draws the same round trip. The macro stage is a loop from Syntax to Syntax, running until no macro matches the tree; only then does an elaborator assign the meaning. The return leg runs whenever a term is shown back: every #check and #print on this site came through delaboration and the formatter, while a plain #eval answers with its value's Repr instance and skips the leg entirely.

The boundary deserves one more degree of precision. A syntax tree does not carry its meaning: the tactic assumption, written twice in one proof, closes two different goals, because what it does depends on where elaboration finds it, and the literal 1 + 1 becomes different core terms at type Nat and at type Int. A TSyntax `term is not an Expr, and nothing short of elaboration turns one into the other. The core term, by contrast, is deterministic: universes, instances, and binding structure are all explicit in an Expr, and it means the same thing wherever it stands. The functions that cross the boundary form a family whose types tell the whole story:

#check @Lean.Elab.Term.elabTerm
#check @Lean.Elab.Term.elabTermEnsuringType
#check @Lean.Elab.Command.elabCommand

For terms, Syntax goes in and Expr comes out, and the crossing happens inside TermElabM, the monad carrying everything that makes a meaning determinate: the expected type, the local context, the open namespaces. Life inside that monad is the subject of chapter 4.

Qq, one level down

The quotation ladder has a third rung. Syntax patterns quote Syntax; the Qq library quotes Expr, the elaborated core, and its quotations carry the object-level type in the meta-level type: a value of type Q(Nat) is an Expr known to denote a Nat.

def natTypeExpr : Q(Type) := q(Nat)

#guard natTypeExpr == .const ``Nat []

def onePlusOneExpr : Q(Nat) := q(1 + 1)

The knowledge is checked, not asserted. Quote an addition of naturals at type Q(Bool) and the mismatch is caught while compiling the metaprogram, long before it runs:

/--
error: failed to synthesize instance of type class
  HAdd Nat Nat Bool

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
def mismatch : Q(Bool) := q(1 + 1)

These lectures show Qq and reach for it once more, in chapter 4's closing exhibit; the backend there constructs its Exprs with the raw API precisely so that the reader feels what the library abstracts away. The ladder is the lesson: raw constructors, then syntax patterns, then typed quotation, each rung trading ceremony for a stronger guarantee.

A template cheat sheet

Antiquotations inside syntax patterns follow a small template language, and it is the same language in both directions: what binds in a match splices in a construction. The forms, at a glance:

Two footnotes to the table. An extra dollar, $$x, escapes one quotation level, the tool of macros that write macros; and a splice's separator must be the one the production declared, so a sepBy on semicolons is spliced with ;*, not with ,*. The three entries of the earlier block exercised the workhorse rows; the remaining rows, each checked:

syntax "first[" term ", " term "]" : term

macro_rules
  | `(first[$x, $_]) => pure x

#guard first[5, 6] == 5

syntax "mylet " ident (" : " term)? " := " term " in " term : term

macro_rules
  | `(mylet $x $[: $ty]? := $v in $b) => `(let $x $[: $ty]? := $v; $b)

#guard (mylet n : Nat := 4 in n + 1) == 5
#guard (mylet n := 4 in n + 1) == 5

syntax "incAll[" term,* "]" : term

macro_rules
  | `(incAll[$[$x:term],*]) => `([$[$x + 1],*])

#guard incAll[1, 2, 3] == [2, 3, 4]

syntax "lams " ident* " => " term : term

macro_rules
  | `(lams $xs* => $b) => do
    let body <- xs.foldrM (fun x (acc : Lean.TSyntax `term) => `(fun $x => $acc)) b
    pure body

#guard (lams a b => a - b) 7 3 == 4

syntax "here!" : term

macro_rules
  | `(here!%$tk) => `($(Lean.quote tk.getPos?.isSome))

#guard here! == true

The promissory note from chapter 0 can now be cashed: its comprehension box is a fresh category, one production, a bridge into term, and two macro rules, the recursive one splicing the remaining clauses with the comma-separated sequence of this cheat sheet.

Lists in the grammar

Templates are one of two list-shaped things, and they are worth telling apart. The bracketed lemma lists of simp [h1, h2] and rw [h1, h2] are not templates but grammar: Lean's postfix sugar turns a production p,* into sepBy, with p,+ for nonempty and p,*,? allowing a trailing separator, and each tactic then wraps its own brackets around the result. There is no single shared bracket production to import; the reusable part is the separator combinator, and the handler side destructs with the table's $rs,* row and getElems. A miniature in the house style, with a sub-rule per element exactly as rw has its rwRule, a trailing comma allowed, and elements told apart by matching on the sub-rule:

syntax bumpRule := ("!")? num

syntax "bump[" bumpRule,*,? "]" : term

macro_rules
  | `(bump[$rs,*]) => do
    let terms <- rs.getElems.mapM fun r => match r with
      | `(bumpRule| !$n) => `(($n + 10 : Nat))
      | `(bumpRule| $n:num) => `(($n + 1 : Nat))
      | _ => Lean.Macro.throwUnsupported
    `([$terms,*])

#guard bump[1, 2] == [2, 3]
#guard bump[!1, 2,] == [11, 3]

#check @Lean.Syntax.TSepArray.getElems

The Qq templates

Qq mirrors the template language one level down, with a shorter table. In construction, $x interpolates a typed Expr into a q(...) quotation and $(e) a computed one; in destruction, ~q(...) matches up to definitional equality, which is why the match runs in MetaM. A capture $a is a fresh name whose type is inferred, never ascribed; a universe splices as Sort $u, a level rather than a term.

def double (n : Q(Nat)) : Q(Nat) := q($n + $n)

def isZero (e : Q(Nat)) : Lean.MetaM Bool := do
  match e with
  | ~q(0) => return true
  | _ => return false

/-- info: true -/
#guard_msgs in
#eval show Lean.MetaM Bool from isZero q(0)

/-- info: false -/
#guard_msgs in
#eval show Lean.MetaM Bool from isZero (double q(1))

Two things distinguish the level below. First, there are no list templates in Qq at all: no $xs,*, no groups, no optional splices; repetition happens through ordinary application. Second, destruction reaches further than syntax ever could: a pattern may apply a capture to bound variables, as in ~q(∃ x, $p x), and matching solves for the function p. That shape is exactly the pattern fragment of chapter 2's cliff, met here as a working tool rather than a boundary:

open Lean Meta Qq in
/-- info: true -/
#guard_msgs in
#eval show MetaM Bool from do
  let e : Q(Nat) := q(1 + 2)
  match e with
  | ~q($a + $b) => return (<- isDefEq a q(1)) && (<- isDefEq b q(2))
  | _ => return false

open Qq in
set_option linter.constructorNameAsVariable false in
def pushForall (e : Q(Prop)) : Lean.MetaM (Option Q(Prop)) := do
  match e with
  | ~q(∃ x, $p x) => return some q(∀ x, $p x)
  | _ => return none

open Lean Meta Qq in
/-- info: true -/
#guard_msgs in
#eval show MetaM Bool from do
  let some r := (<- pushForall q(∃ n, n = 0)) | return false
  isDefEq r q(∀ n, n = 0)

Further reading

• The Lean 4 Metaprogramming Book: its Syntax and Macros chapters cover this ground at full width; the book pins an older toolchain, so expect small drifts from what these lectures display. <- back
• Ullrich and de Moura, Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages: the hygiene mechanism behind the constFn demo. <- back
• quote4: the Qq library, typed quotation for Expr. <- back