11.5.5.1. The macro_rules Command🔗
syntax
The Lean.Parser.Command.macro_rules : commandmacro_rules command takes a sequence of rewrite rules, specified as syntax pattern matches, and adds each as a macro.
The rules are attempted in order, before previously-defined macros, and later macro definitions may add further macro rules.
command ::= ...
| A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.
A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. Syntax quotation for terms. p : ident
The patterns in the macros must be quotation patterns.
They may match syntax from any syntax category, but a given pattern can only ever match a single syntax kind.
If no category or parser is specified for the quotation, then it may match terms or (sequences of) commands, but never both.
In case of ambiguity, the term parser is chosen.
Internally, macros are tracked in a table that maps each syntax kind to its macros.
The Lean.Parser.Command.macro_rules : commandmacro_rules command may be explicitly annotated with a syntax kind.
If a syntax kind is explicitly provided, the macro definition checks that each quotation pattern has that kind.
If the parse result for the quotation was a choice node (that is, if the parse was ambiguous), then the pattern is duplicated once for each alternative with the specified kind.
It is an error if none of the alternatives have the specified kind.
If no kind is provided explicitly, then the kind determined by the parser is used for each pattern.
The patterns are not required to all have the same syntax kind; macros are defined for each syntax kind used by at least one of the patterns.
It is an error if the parse result for a quotation pattern was a choice node (that is, if the parse was ambiguous).
The documentation comment associated with Lean.Parser.Command.macro_rules : commandmacro_rules is displayed to users if the syntax itself has no documentation comment.
Otherwise, the documentation comment for the syntax itself is shown.
As with notations and operators, macro rules may be declared scoped or local.
Scoped macros are only active when the current namespace is open, and local macro rules are only active in the current section scope.
Idiom Brackets
Idiom brackets are an alternative syntax for working with applicative functors.
If the idiom brackets contain a function application, then the function is wrapped in pure and applied to each argument using <*>. Operator hyperlinking to docs
Lean does not support idiom brackets by default, but they can be defined using a macro.
syntax (name := idiom) "⟦" (term:arg)+ "⟧" : term
macro_rules
| `(⟦$f $args*⟧) => do
let mut out ← `(pure $f)
for arg in args do
out ← `($out <*> $arg)
return out
This new syntax can be used immediately.
def addFirstThird [Add α] (xs : List α) : Option α :=
⟦Add.add xs[0]? xs[2]?⟧
none#eval addFirstThird (α := Nat) []
none#eval addFirstThird [1]
some 4#eval addFirstThird [1,2,3,4]
Scoped Macros
Scoped macro rules are active only in their namespace.
When the namespace ConfusingNumbers is open, numeric literals will be assigned an incorrect meaning.
namespace ConfusingNumbers
The following macro recognizes terms that are odd numeric literals, and replaces them with double their value.
If it unconditionally replaced them with double their value, then macro expansion would become an infinite loop because the same rule would always match the output.
scoped macro_rules
| `($n:num) => do
if n.getNat % 2 = 0 then Lean.Macro.throwUnsupported
let n' := (n.getNat * 2)
`($(Syntax.mkNumLit (info := n.raw.getHeadInfo) (toString n')))
Once the namespace ends, the macro is no longer used.
end ConfusingNumbers
Without opening the namespace, numeric literals function in the usual way.
(3, 4)#eval (3, 4)
When the namespace is open, the macro replaces 3 with 6.
open ConfusingNumbers
(6, 4)#eval (3, 4)
It is not typically useful to change the interpretation of numeric or other literals in macros.
However, scoped macros can be very useful when adding new rules to extensible tactics such as trivial that work well with the contents of the namespaces but should not always be used.
Behind the scenes, a Lean.Parser.Command.macro_rules : commandmacro_rules command generates one macro function for each syntax kind that is matched in its quote patterns.
This function has a default case that throws the unsupportedSyntax exception, so further macros may be attempted.
A single Lean.Parser.Command.macro_rules : commandmacro_rules command with two rules is not always equivalent to two separate single-match commands.
First, the rules in a Lean.Parser.Command.macro_rules : commandmacro_rules are tried from top to bottom, but recently-declared macros are attempted first, so the order would need to be reversed.
Additionally, if an earlier rule in the macro throws the unsupportedSyntax exception, then the later rules are not tried; if they were instead in separate Lean.Parser.Command.macro_rules : commandmacro_rules commands, then they would be attempted.
One vs. Two Sets of Macro Rules
The arbitrary! macro is intended to expand to some arbitrarily-determined value of a given type.
syntax (name := arbitrary!) "arbitrary!" term:arg : term
macro_rules
| `(arbitrary! ()) => `(())
| `(arbitrary! Nat) => `(42)
| `(arbitrary! ($t1 × $t2)) => `((arbitrary! $t1, arbitrary! $t2))
| `(arbitrary! Nat) => `(0)
Users may extend it by defining further sets of macro rules, such as this rule for Empty that fails:
macro_rules
| `(arbitrary! Empty) => throwUnsupported
(42, 42)#eval arbitrary! (Nat × Nat)
If all of the macro rules had been defined as individual cases, then the result would have instead used the later case for Nat.
This is because the rules in a single Lean.Parser.Command.macro_rules : commandmacro_rules command are checked from top to bottom, but more recently-defined Lean.Parser.Command.macro_rules : commandmacro_rules commands take precedence over earlier ones.
macro_rules
| `(arbitrary! ()) => `(())
macro_rules
| `(arbitrary! Nat) => `(42)
macro_rules
| `(arbitrary! ($t1 × $t2)) => `((arbitrary! $t1, arbitrary! $t2))
macro_rules
| `(arbitrary! Nat) => `(0)
macro_rules
| `(arbitrary! Empty) => throwUnsupported
(0, 0)#eval arbitrary! (Nat × Nat)
Additionally, if any rule throws the unsupportedSyntax exception, no further rules in that command are checked.
macro_rules
| `(arbitrary! Nat) => throwUnsupported
redundant alternative #2| `(arbitrary! Nat) => `(42)
macro_rules
| `(arbitrary! Int) => `(42)
macro_rules
| `(arbitrary! Int) => throwUnsupported
The case for Nat fails to elaborate, because macro expansion did not translate the arbitrary! : termarbitrary! syntax into something supported by the elaborator.
#eval elaboration function for 'arbitrary!' has not been implemented
arbitrary! Natarbitrary! Nat
elaboration function for 'arbitrary!' has not been implemented
arbitrary! Nat
The case for Int succeeds, because the first set of macro rules are attempted after the second throws the exception.
42#eval arbitrary! Int
11.5.5.2. The macro Command🔗
The Lean.Parser.Command.macro : commandmacro command simultaneously defines a new syntax rule and associates it with a macro.
Unlike Lean.Parser.Command.notation : commandnotation, which can define only new term syntax and in which the expansion is a term into which the parameters are to be substituted, the Lean.Parser.Command.macro : commandmacro command may define syntax in any syntax category and it may use arbitrary code in the MacroM monad to generate the expansion.
Because macros are so much more flexible than notations, Lean cannot automatically generate an unexpander; this means that new syntax implemented via the Lean.Parser.Command.macro : commandmacro command is available for use in input to Lean, but Lean's output does not use it without further work.
syntax
command ::= ...
| A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.
A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`.
syntax
A macro's arguments are either syntax items (as used in the Lean.Parser.Command.syntax : commandsyntax command) or syntax items with attached names.
macroArg ::=
stxmacroArg ::= ...
| ident:stx
In the expansion, the names that are attached to syntax items are bound; they have type TSyntax for the appropriate syntax kinds.
If the syntax matched by the parser does not have a defined kind (e.g. because the name is applied to a complex specification), then the type is TSyntax Name.anonymous.
The documentation comment is associated with the new syntax, and the attribute kind (none, local, or scoped) governs the visibility of the macro just as it does for notations: scoped macros are available in the namespace in which they are defined or in any section scope that opens that namespace, while local macros are available only in the local section scope.
Behind the scenes, the Lean.Parser.Command.macro : commandmacro command is itself implemented by a macro that expands it to a Lean.Parser.Command.syntax : commandsyntax command and a Lean.Parser.Command.macro_rules : commandmacro_rules command.
Any attributes applied to the macro command are applied to the syntax definition, but not to the Lean.Parser.Command.macro_rules : commandmacro_rules command.