Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages

Beyond Notations

Sebastian Ullrich1 () Leonardo de Moura2

S. Ullrich L. de Moura

Karlsruhe Institute of Technology, Germany
<EMAIL_ADDRESS>Microsoft Research, USA

In interactive theorem provers (ITPs), extensible syntax is not only crucial to lower the cognitive burden of
manipulating complex mathematical objects, but plays a critical role in developing reusable abstractions in libraries.
Most ITPs support such extensions in the form of restrictive “syntax sugar” substitutions and other ad hoc mechanisms,
which are too rudimentary to support many desirable abstractions. As a result, libraries are littered with unnecessary
redundancy. Tactic languages in these systems are plagued by a seemingly unrelated issue: accidental name capture,
which often produces unexpected and counterintuitive behavior. We take ideas from the Scheme family of programming
languages and solve these two problems simultaneously by proposing a novel hygienic macro system custom-built for ITPs. We further
describe how our approach can be extended to cover type-directed macro expansion resulting in a single, uniform system
offering multiple abstraction levels that range from supporting simplest syntax sugars to elaboration of formerly
baked-in syntax. We have implemented our new macro system and integrated it into the new version of the Lean
theorem prover, Lean 4. Despite its expressivity, the macro system is simple enough that it can easily be integrated into
other systems.

This is an extended version of 22, with the most significant changes being the addition of <ref> and <ref>.

§ INTRODUCTION

Mixfix notation systems have become an established part of many modern ITPs for attaching terse and familiar syntax
to functions and predicates of arbitrary arity.

_⊢_:_ = Typing
Notation "Ctx ⊢ E : T" := (Typing Ctx E T).
notation typing ("_ ⊢ _ : _")
notation Γ `⊢` e `:` τ := Typing Γ e τ

Lean 3

As a further extension, all shown systems also allow binding names inside mixfix notations.

syntax ∃ A (λ x → P) = ∃[ x ∈ A ] P
Notation "∃ x , P" := (exists (fun x => P)).
notation exists (binder "∃")
notation `∃` binder `,` r:(scoped P, Exists P) := r

Lean 3

While these extensions differ in the exact syntax used, what is true about all of them is that at the time
of the notation declaration, the system already, statically knows what parts of the term are bound by the newly
introduced variable. This is in stark contrast to macro systems in Lisp and related languages where the
expansion of a macro (a syntactic substitution) can be specified not only by a template expression with placeholders like above, but also by
arbitrary syntax transformers, i.e. code evaluated at compile time that takes and returns a syntax
tree.[These two macro declaration styles are commonly referred to as pattern-based vs. procedural] As we
move to more and more expressive notations and ideally remove the boundary between built-in and user-defined
syntax, we argue that we should no more be limited by the static nature of
existing notation systems and should instead introduce syntax transformers to the world of ITPs.

However, as usual, with greater power comes greater responsibility. By using arbitrary syntax transformers, we lose the
ability to statically determine what parts of the macro template can be bound by the macro input (and vice versa). Thus
it is no longer straightforward to avoid hygiene issues (i.e. accidental capturing of identifiers; [13]) by automatically
renaming identifiers. We propose to learn from and adapt the macro hygiene systems
implemented in the Scheme family of languages for interactive theorem provers in order to obtain more general but still well-behaved
notation systems.

After giving a practical overview of the new, macro-based notation system we
implemented in Lean 4 [6] in <ref>, we describe the
issue of hygiene and our general hygiene algorithm, which should be just as applicable to other ITPs, in
<ref>. <ref> gives a detailed description of the implementation of this algorithm, and macros in general, in Lean 4. In
<ref>, we extend the use case of macros from mere syntax substitutions to type-aware elaboration
[By “elaboration”, we mean the transformation of surface-level syntax into the explicit kernel term/declaration representation, including type and typeclass inference.].
Finally, we have already encountered hygiene issues in the current version of Lean in a different part of the system:
the tactic framework. We discuss how these issues are inevitable when implementing reusable tactic scripts and how our
macro system can be applied to this hygiene problem as well in <ref>.

Contributions. We present a system for hygienic macros optimized for theorem proving languages as implemented[<https://github.com/leanprover/lean4/blob/IJCAR20-LMCS/src/Lean/Elab>] in
the new version of the Lean theorem prover, Lean 4.

* We describe a novel, efficient hygiene algorithm
to employ macros in ITP languages at large: a combination
of a white-box, effect-based approach for detecting newly introduced identifiers and an efficient encoding of scope

* We show how such a macro system can be seamlessly integrated into existing elaboration designs to support
type-directed expansion even if they are not based on homogeneous source-to-source transformations.

* We show how hygiene issues also manifest in tactic languages and how they can be solved with the same
macro system. To the best of our knowledge, the tactic language in Lean 4 is the first tactic language in an
established theorem prover that is automatically hygienic in this regard.

§ THE NEW MACRO SYSTEM

Lean's previous notation system as shown in <ref> is still supported in Lean 4, but based on a much more general
macro system; in fact, the notation command[A Lean file is made up of a sequence of commands, which are processed in turn and can extend the environment with new declarations or metadata (such as custom parsers)] itself has been reimplemented as a macro, more specifically as a
macro-generating macro making use of our tower of abstraction levels. The corresponding Lean 4
command[All examples including full context can be found in the supplemental material at
for the example from the previous section
expands to the macro declaration

macro Γ:term "⊢" e:term ":" τ:term : term => `(Typing $Γ $e $τ)
\end{lstlisting}
where the \emph{syntactic category} (\lstinline{term}) of placeholders and of the entire macro is now specified explicitly.
The right-hand side uses an explicit \emph{syntax quasiquotation} to construct the syntax tree,
with syntax placeholders (\emph{antiquotations}) prefixed with \lstinline{$}. As suggested by the
explicit use of a quotation, the right-hand side may now be an arbitrary Lean term computing a syntax object; in other words,
there is no distinction between pattern-based and procedural macros in our system. We can now use this abstraction level to
implement simple macros in syntactic categories other than \lstinline{term}, such as for commands.
\lstinputlisting[linerange=defthunk-end]{supplement/Examples.lean}
\lstinline{macro} itself is another command-level macro that, for our \lstinline{notation} example, expands to two commands
\begin{lstlisting}
syntax term "⊢" term ":" term : term
| `($Γ ⊢ $e : $τ) => `(Typing $Γ $e $τ)
\end{lstlisting}
that is, a pair of parser extension (which we will not further discuss in this paper) and syntax transformer.
Our reason for ultimately separating these two concerns is that we can now obtain a well-structured syntax tree pre-expansion, i.e.\ a
\emph{concrete} syntax tree, and use it to implement source code tooling such as auto-completion, go-to-definition, and
refactorings. Implementing even just the most basic of these tools for the Lean 3 frontend that combined parsing and
notation expansion meant that they had to be implemented right inside the parser, which was not an extensible or even
maintainable approach in our experience.

Both \lstinline{syntax} and \lstinline{macro_rules} are in fact further macros for regular Lean definitions encoding
procedural metaprograms, though users should rarely need to make use of this lowest abstraction level explicitly. Both
commands can only be used at the top level; we are not currently planning support for local macros.

%The main remaining restriction of \lstinline{notation} compared to using \lstinline{syntax}/\lstinline{macro} directly
%is that it is specific to
There is no more need for the complicated \lstinline{scoped} syntax since the desired translation can now be specified
naturally, without any need for further annotations.
\lstinputlisting[linerange=exists-end]{supplement/Examples.lean}
The lack of static restrictions on the right-hand side ensures that this works just as well with custom binding notations,
even ones whose translation cannot statically be determined before substitution.
\lstinputlisting[linerange=union-end]{supplement/Examples.lean}
Here we explicitly make use of the \lstinline{macro_rules} abstraction level for its convenient syntactic pattern matching syntax. \lstinline{macro_rules} are ``open'' in the sense that multiple transformers for the same \lstinline{syntax} declaration can
be defined; they are tried up to the first match, starting with the newest declaration (though this can be customized
using explicit priority annotations).
Thus the following extension will not be shadowed by the \lstinline{$b} default case above:
\lstinputlisting[linerange=le-end]{supplement/Examples.lean}

As a final example, we present a partial reimplementation of the arithmetic ``bigop'' notations found\footnote{\url{https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/bigop.v}} in Coq's
Mathematical Components
library~[14] such as
\begin{lstlisting}
\sum_ (i <- [0, 2, 4] | i != 2) i
\end{lstlisting}
for summing over a filtered sequence of elements. The
specific bigop notations are defined in terms of a single \verb!\big_! fold operator; however, because Coq's notation
system is unable to abstract over the indexing syntax, every specific bigop notation has to redundantly repeat every
specific index notation before delegating to \verb!\big_!. In total, the 12 index notations for \verb!\big_! are duplicated for 3 different bigops in the file.\\
\begin{minipage}{1.0\linewidth}
\begin{lstlisting}
Notation "\sum_ ( i <- r ) F"     := (\big[addn/0]_(i <- r) F).
Notation "\sum_ ( i <- r | P ) F" := (\big[addn/0]_(i <- r | P) F).
Notation "\prod_ ( i <- r ) F"     := (\big[muln/1]_(i <- r) F).
Notation "\prod_ ( i <- r | P ) F" := (\big[muln/1]_(i <- r | P) F).
\end{lstlisting}
\end{minipage}
In contrast, using our system,
we can introduce a new syntactic category for index notations, interpret it once in \verb!\big_!, and define new
bigops on top of it without any redundancy.
\lstinputlisting[linerange=declare_syntax_cat-end,belowskip=0pt]{supplement/Bigop.lean}
\begin{lstlisting}[aboveskip=0pt,belowskip=0pt,showlines=true]

\end{lstlisting}
\lstinputlisting[linerange=Sum-end,aboveskip=0pt]{supplement/Bigop.lean}
\lstinputlisting[linerange=Prod-end,aboveskip=0pt]{supplement/Bigop.lean}
The full example is included in the supplement.
We reiterate that this is not merely a showcase of a parsing extension, but that abstracting over binding syntax in this manner is fundamentally incompatible with any static approach of ensuring hygiene.
The dynamic nature of Scheme-like macros allows us to always apply such factorings without being burdened by static restrictions while still preserving hygiene.

%Here the ``quotation kind'' \lstinline{:command} is used to disambiguate the syntax quotation's content
%For a simple example that is not expressible in the old system, we present the definition of a \emph{destructuring
%  lambda}, which combines an anonymous function with matching its parameter against an \emph{anonymous constructor}
%pattern. The list of identifiers introduced in the new syntax can be used without further annotations in the pattern
%match in the macro's right-hand side.
%-- syntax may overlap previous syntax; the longest parse wins
%syntax "fun" "⟨" (sepBy "," term) "⟩" "=>" term : term
%macro `(fun ⟨$e*⟩ => $f) => `(fun x => match x with ⟨$e*⟩ => $f)
%\todo{Does this example still make sense?}

%We had decided early on that these examples were the minimum of generality the new macro system should support. What was
%less clear was how to do so in a hygienic manner. Clearly the tricks of Lean 3 that depended on statically knowing the
%full binding structure were not applicable anymore. Instead we looked at the Scheme family of languages and in
%particular Racket's new \emph{Sets of Scopes}~[12] hygiene algorithm, which is described by its author
%as being both simpler and more uniform than previous algorithms based on explicit renaming.
%While the Lean and Racket languages hardly look similar, the Sets of Scopes algorithm is for the most part directly
%applicable to our macro system sketched above.
%%To see this, we give an embedding of the relevant parts of the Lean language into the simplified formal language described in~12.
%The biggest difference between the two languages is that Lean (top-level) definitions are strictly ordered as in most
%theorem proving languages while Racket
%definitions (including macros) live in a mutually recursive ``definition context'' (which is a source of significant
%complication in the hygiene algorithm that we can ignore)\footnote{While Lean allows mutual definitions in a
%  special \lstinline{mutual} block, these are rare enough that not supporting macro declarations inside of them is not a
%significant restriction in practice.}. Thus the Racket equivalent of our first \lstinline{macro}
%example would be a locally-bound macro
%%(let-syntax [(const
%%              (syntax-rules ()
%%              [(_ e) (lambda (a) e)]))]
%%   (const a))
%(let-syntax [(-⊢-:- (syntax-rules ()
%              [(-⊢-:- Γ e τ) (typed Γ e τ)]))]
%   ...remainder of module...)
%Here we use a Racket identifier \lstinline{-⊢-:-} where the Lean code used the notation's syntax, which is resolved
%prior to macro expansion. Indeed, we assume that every Lean macro is resolved not by dynamic name resolution during
%macro expansion but statically associated with a syntax production (identified by a globally unique name) and is
%triggered whenever this production is encountered in the syntax tree produced by the parser. In other words, we can
%think of our new macro system as a subset of Racket's where all identifiers bound by \verb!let-syntax! are known to
%be mutually distinct and thus do not need to participate in macro hygiene.

\section{Hygiene Algorithm}
\label{sec:hygge}

In this section, we will give a mostly self-contained description of our algorithm for automatic hygiene applied to a
simple recursive macro expander; we postpone comparisons to existing hygiene algorithms to \cref{sec:related}.

Hygiene issues occur when transformations such as macro expansions lead to an unexpected capture (rebinding) of
identifiers. For example, we would expect the notation
\begin{lstlisting}
notation "const" e => fun x => e
\end{lstlisting}
to always produce a constant function regardless of the specific \lstinline{e}.
We would not expect the term \lstinline{const x} to be the identity function because intuitively there is no
\verb!x! in scope at the argument position of \lstinline{const}; that the implementation of the macro
makes use of the name internally should be of no concern to the macro user.

Thus hygiene issues can also be described as a \emph{confusion of scopes} when syntax parts are removed from their
original context and inserted into new contexts, which makes name resolution strictly after macro expansion (such as in a compiler preceded
by a preprocessor) futile. Instead we need to track scopes \emph{as metadata} before and during macro expansion so as
not to lose information about the original context of identifiers. Specifically,
\begin{enumerate}
\item when an identifier captured in a syntax quotation matches one or more\footnote{Lean allows overloaded
top-level bindings whereas local bindings are shadowing}
top-level symbols, the identifier is annotated with a list of these symbols as
\emph{top-level} scopes to
preserve its \emph{extra-macro} context (which, because of the lack of local macros, can only contain top-level
bindings), and
\item when a macro is expanded, all identifiers freshly introduced by the expansion are annotated with a new \emph{macro} scope
to preserve the \emph{intra-macro} context.
In particular, different expansions of the same macro introduce different annotations.
Macro scopes are appended to a list, i.e.\ ordered by expansion time.
This full ``history of expansions'' is necessary to treat macro-producing macros correctly, as we shall see in \cref{sec:hygge:ex}.
\end{enumerate}
Thus, the expansion of the above term \lstinline{const x} should be (an equivalent of)
\lstinline{fun x.1 => x}
where \verb!1! is a fresh macro scope appended to the macro-introduced \verb!x!, preventing it from capturing the
\verb!x! from the original input. In general, we will present hygienic identifiers in the following as \texttt{n.msc$_1$.msc$_2$.$\ldots$.msc$_n$\{tsc$_1$,$\ldots$,tsc$_n$\}}
where \verb!n! is the original name, \verb!msc! are macro scopes, and \verb!tsc! top-level scopes, eliding the braces if
there are no top-level scopes as in the example above. We use the dot
notation to suggest both the ordered nature of macro scopes and their eventual implementation in \cref{sec:impl}.
We will now describe how to implement these operations in a standard macro expander.

%In contrast to ``black box'' approaches that find identifiers introduced by a macro by annotating its input, then
%flipping the scope on its output, we follow a more efficient ``white box'' approach in which the macro expander passes a
%fresh scope to the syntax transformer, which applies it to all identifiers captured in syntax quotations. These
%approaches are obviously equivalent for pattern-based macros that never synthesize identifiers outside of syntax
%quotations; procedural macros on the other hand may need to make explicit use of the fresh scope passed by the expander.

\subsection{Expansion Algorithm}
\label{sec:algo}

A Scheme-style macro expander takes a syntax tree as input and produces a fully expanded tree, that is, where all macro uses have been reduced to \emph{core forms} that cannot be described as macros and are instead handled by the later stages, such as an elaborator.
The expander should furthermore rename bindings where necessary to avoid hygiene issues such that later stages do not have to know anything about the implementation of hygiene, or indeed that it was applied at all.

Given a \emph{global context} (a set of symbols), our expansion algorithm does so by a conventional top-down expansion, keeping
track of an initially-empty \emph{local context} (another set of symbols).
When a binding core form is encountered, the local context is extended with the bound symbol(s); existing top-level
scopes on bindings are discarded at this step since they are only meaningful on references.
Thus we will formally define a symbol as an identifier together with a list of macro scopes, such as \verb!x.1! above.
As we shall see in \cref{sec:impl}, this definition of symbol is covered by the existing one in Lean, so later stages indeed do not have to concern themselves with it.

When a reference (another core form), i.e.\ an identifier not
in binding position, is encountered, it is resolved according to the following rules:
\begin{enumerate}
\item If the local context has an entry for the same symbol, the reference binds to
the corresponding local binding; any top-level scopes are again discarded.
\item Otherwise, if the identifier is annotated with one or more top-level scopes or matches one or more symbols in the
global context, it binds to all of these (to be disambiguated by the elaborator).
%  \todo{I deleted the following sentence since it is not true for the ``or'' part. Not sure if we need it in any way.
%Here macro scopes are ignored
%  instead since for a top-level scope to be present the identifier must have matched the corresponding symbol exactly at
%  some point.}
\item Otherwise, the identifier is unbound and an error is generated.
\end{enumerate}

In the common incremental compilation mode of ITPs, every command is fully processed before subsequent commands.
Thus, an expander for such a system will never extend the global context by itself, but pass the fully expanded command
to the next compilation stage before being called again with the next command's unexpanded syntax tree and a possibly
extended global context.

Notably, our expander does not introduce macro scopes by itself, either, much in contrast to other expansion algorithms. We
instead delegate this task to the macro's implementation, though in a completely transparent way for all pattern-based and for
many procedural macros. We claim that a macro should in fact be interpreted as an \emph{effectful} computation since two
expansions of the same identifier-introducing macro should not return the same syntax tree to avoid unhygienic
interactions between them. Thus,
as a \emph{side effect}, it should apply a fresh macro scope to each newly introduced identifier. In particular, a syntax quotation
should not merely be seen as a datum, but as an effectful value that obtains and applies this fresh scope to
all the identifiers captured by it to immediately ensure hygiene for pattern-based macros. Procedural macros producing
identifiers not originating from syntax quotations might need to obtain and make use of the fresh macro scope
explicitly. Note that forgoing to do so is not sufficient to reliably implement \emph{anaphoric} or other hygiene-bending macros
that make an identifier (conventionally \lstinline{it} in Lisp languages) available in the scope of the macro caller, as discussed in 3.
Instead, we believe that the correct translation of anaphoric macros to Lean is to change such identifiers to \emph{keywords} that
do not participate in hygiene at all, analogous to the \emph{syntax parameters} of 3.
An example for this is the \lstinline{this} keyword introduced by tactics such as \lstinline{have}
that can be used to refer to the just-proved fact.\footnote{\url{https://github.com/leanprover/lean4/blob/6d0c91c/src/Init/Notation.lean\#L204-L207}}

We give a specific monad-based~[17]
implementation of effectful syntax quotations as a regular macro in \cref{sec:impl}.
For the remainder of this section, we will simply assume that macros have been implemented in this way and observe their interaction with the expansion algorithm described above.
%as further described in \cref{sec:hygge:limit}.

\subsection{Examples}
\label{sec:hygge:ex}

Given the following input,
\begin{lstlisting}
def x := 1
def e := fun y => x
notation "const" e => fun x => e
def y := const x
\end{lstlisting}
a Lean-like system using the presented expansion algorithm should incrementally parse, expand, and elaborate each declaration before advancing to the next one.
For a first, trivial example, let us
focus on the expansion of the second line. At this point, the global context contains the symbol \verb!x! (plus any
default imports that we will ignore here). Descending into the right-hand side of the definition, the expander first adds \verb!y! to the
local context. The reference \verb!x! does not match any local definitions, so it binds to the matching top-level

In the next line, the built-in \lstinline{notation} macro expands to the definitions
\begin{lstlisting}
syntax "const" term : term
| `(const $e) => `(fun x => $e)
\end{lstlisting}
%\todo{which might be confusing because the second definition can't be parsed before the first one is elaborated, but
%  these are only \emph{pretty-printed} representations of the actual expanded syntax objects that will not be parsed again}
When a top-level macro application unfolds to multiple declarations, we expand and elaborate these
incrementally as well to ensure that declarations are in the global context of subsequent declarations from the same expansion. When
recursively expanding the \lstinline{macro_rules} declaration (we will assume for this example that \lstinline{macro_rules} itself is
a core form) in the global context \verb!{x, e}!, we first visit the syntax quotation on the left-hand side. The
identifier \verb!e! inside of it is in an antiquotation and thus not captured by the quotation. It is in binding
position for the right-hand side, so we add \verb!e! to the local context.
Visiting the right-hand side, we find the quotation-captured identifier \verb!x! and annotate it with the matching
top-level definition of the same name; we do not yet know that it is in a binding position. When visiting the reference
\verb!e!, we see that it matches a local binding and do not add top-level scopes.
\begin{lstlisting}
| `(const $e) => `(fun x{x} => $e)
\end{lstlisting}
Visiting the last line
\begin{lstlisting}
def y := const x
\end{lstlisting}
with the global context \verb!{x, e}!, we descend into the right-hand side. We
expand the \lstinline{const} macro given a fresh macro scope \verb!1!, which is applied to any captured identifiers.
\begin{lstlisting}
def y := fun x.1{x} => x
\end{lstlisting}
We add the symbol \verb!x.1! (discarding the top-level scope \verb!x!) to the
local context and finally visit the reference \verb!x!. The reference does not match the local binding \verb!x.1! but
does match the top-level binding \verb!x!, so it binds to the latter.
\begin{lstlisting}
def y := fun x.1 => x
\end{lstlisting}

Now let us briefly look at a more complex macro-macro example demonstrating use of the macro scopes stack:
\lstinputlisting[linerange=hygiene_example2-end]{supplement/Examples.lean}
If we use this macro as in \lstinline{m f}, we apply a fresh macro scope \verb!1! to all captured identifiers, then incrementally process
the two new declarations.
\begin{lstlisting}
def f.1 := 1
macro "mm" : command => `(
def f := f.1{f.1} + 1
def f.1{f.1} := f + 1)
\end{lstlisting}
If we use the new macro \lstinline{mm}, we apply one more macro scope \verb!2!.
\begin{lstlisting}
def f.2 := f.1.2{f.1} + 1
def f.1.2{f.1} := f.2 + 1
\end{lstlisting}
When processing these new definitions, we see that the scopes ensure the expected name resolution.
\begin{lstlisting}
def f.1 := 1
def f.2 := f.1 + 1
def f.1.2 := f.2 + 1
\end{lstlisting}
In particular, we now
have global declarations \lstinline{f.1}, \lstinline{f.2}, and \lstinline{f.1.2} that show that storing only a single
macro scope would have led to a collision.

%Now that we have described the workings of hygiene in our macro system, we can explore how to circumvent it; while rare,
%there is a class of \emph{hygiene-bending} macros for which this behavior is useful. One example is the Lean 3 built-in
%syntax \lstinline{have} that makes the proof of a subgoal available to further chaining as the special identifier

%We have developed this particular hygiene algorithm with the explicit goal of greatly improving the expressivity of
%notation systems for ITPs while keeping additional book-keeping overhead as low as possible so as not to jeopardize
%overall efficiency of the system. Thus we have explicitly excluded some features that users of other macro-based
%languages might expect but that we did not deem necessary for the application to ITPs:
%% not an intrinsic limitation?
%%\item \textbf{Lexical macro resolution.} As shown above, every macro in our system is preceded by and tied to a syntax
%%  declaration. Even identifier-like tokens like \verb!const! are declared as \emph{keywords} by the syntax declaration,
%%  thus it is the parser and not regular name resolution that determines the macros to be executed.
%\item \textbf{Local macros}.

\section{Implementation}
\label{sec:impl}

Syntax objects in Lean 4 are represented as an inductive type of \emph{nodes} (or nonterminals), \emph{atoms} (or
terminals), and, as a special case of terminals, \emph{identifiers}.
\begin{lstlisting}
inductive Syntax where
| node  (kind : Name) (args : Array Syntax)
| atom  (info : SourceInfo) (val : String)
| ident (info : SourceInfo) (rawVal : String) (val : Name) (preresolved : List (Nat × List String))
| missing
\end{lstlisting}
An additional constructor represents \emph{missing} parts from syntax error recovery.
Atoms and identifiers are annotated with source location metadata unless generated by a macro.
Identifiers carry macro scopes inline in their \verb!Name! while top-level scopes are held in a
separate list. The additional \verb!Nat! is an implementation detail of Lean's hierarchical name resolution.

The type \verb!Name! of hierarchical names precedes the implementation of the macro system and is used throughout Lean's
implementation for referring to (namespaced) symbols.
\begin{lstlisting}
inductive Name where
| anonymous
| str (base : Name) (s : String)
| num (base : Name) (n : Nat)
\end{lstlisting}
The syntax \lstinline{`a.b} is a literal of type \lstinline{Name} for use in meta-programs. The numeric part of
\lstinline{Name} is not accessible from the surface syntax and reserved for internal names; similar designs are found in
other ITPs. By reusing \lstinline{Name} for storing
macro scopes, but not top-level scopes, we ensure that the new definition of \emph{symbol} from \cref{sec:algo}
coincides with the existing Lean type and no changes to the implementation of the local or global context are necessary
for adopting the macro system.

\begin{figure}[tb]
\lstinputlisting[linerange=expand-end,numbers=left,firstnumber=0,belowskip=0pt]{supplement/Expander.lean}
\begin{lstlisting}[aboveskip=0pt,showlines=true,numbers=left,firstnumber=17]
| ...  -- other core forms
| _ => do
let t ← getTransformerFor stx.getKind
let stx ← withFreshMacroScope (t stx)
expand stx
\end{lstlisting}
\caption[]{Abbreviated implementation of a recursive expander for our macro system}
\label{fig:expander}
\end{figure}
A Lean 4 implementation of the expansion algorithm described in the previous section is given in
\cref{fig:expander}; the full implementation including examples is included in the supplement.
As a generalization,
syntax transformers in the full implementation have the type \lstinline{Syntax → TransformerM Syntax} where the \lstinline{TransformerM} monad gives access to
the global context and a fresh macro scope per macro expansion. The expander itself uses an extended \lstinline{ExpanderM} monad
based on \lstinline{TransformerM} that also stores the local context and the set of registered macros.
We use the Lean equivalent of Haskell's \verb!do! notation~[15] to program in these monads.

As described in \cref{sec:algo}, the expander in \cref{fig:expander} has built-in
knowledge of some ``core forms'' (lines 2-16) with special expansion behavior, while all other forms are assumed to
be macros and expanded recursively (lines 19-21). Identifiers form one base case of the recursion. As described in
the previous section, they are first looked up in the local context (recall that the \lstinline{Name} of an identifier includes macro scopes),
then as a fall back in the global context plus its own top-level scopes. \lstinline{mkIdent : Name → Syntax}
creates an identifier without source information or top-level scopes, which are not needed after expansion.
\lstinline{mkOverloadedIds} implements the Lean special case of overloaded symbols to be disambiguated by
elaboration; systems without overloading support should throw an ambiguity error instead in this case.

As an example of a core binding form, the expansion of a single-parameter \lstinline{fun} is shown in lines 12-16 of \cref{fig:expander}. It
recursively expands the given parameter type, then expands the body in a new local context extended with the value of
\lstinline{id}. Here \lstinline{getIdentVal : Syntax → Name} in particular
implements the discarding of top-level scopes from binders.

Finally, in the macro case, we fetch the syntax transformer for the given node kind, run it in a new context with
a fresh current macro scope, and recurse.

\begin{figure}
\lstinputlisting[linerange=quoteSyntax-end,numbers=left,firstnumber=0]{supplement/Expander.lean}
\caption[]{Simplified syntax transformer for syntax quotations}
\label{fig:quote}
\end{figure}
Syntax quotations are given as one example of a macro: they do not have built-in semantics but transform into code that
constructs the appropriate syntax tree~(\lstinline{expandStxQuot} in \cref{fig:quote}).
%The produced code has type \lstinline{TransformerM Syntax} to obtain the current macro scope and apply it to all captured identifiers.
More specifically, a syntax quotation will, at run time (of the surrounding macro), query the current
macro scope \lstinline{msc} from the surrounding \lstinline{TransformerM} monad (code generated by \lstinline{expandStxQuot}) and apply it to all captured identifiers (code generated by \lstinline{quoteSyntax}).
\lstinline{quoteSyntax} recurses
through the quoted syntax tree, reflecting its constructors. Basic datatypes such as \lstinline{String} and
\lstinline{Name} are turned into \lstinline{Syntax} via the typeclass method \lstinline{quote}. For antiquotations,
we return their contents unreflected. In the case
of identifiers, we resolve possible global references at compile time and reflect them, while \lstinline{msc} is
applied at run time. Thus a quotation
\lstinline{`(a + $b)} inside a global context where the symbol \lstinline{a} matches declarations \lstinline{a.a} and \lstinline{b.a} is transformed to the equivalent of\\
\begin{minipage}{1.0\linewidth}
\begin{lstlisting}
do let msc ← getCurrMacroScope
pure (Syntax.node `plus [
Syntax.ident SourceInfo.none "a" (addMacroScope `a msc)
[`a.a, `b.a],
Syntax.atom SourceInfo.none "+",
\end{lstlisting}
\end{minipage}

This implementation of syntax quotations itself makes use of syntax quotations for simplicity
and thus is dependent on its own
implementation in the previous stage of the compiler. Indeed, the helper variable \lstinline{msc} must be renamed should
the name already be in scope and used inside an antiquotation.\footnote{As long as no such case exists, a hygienic implementation of syntax quotations can be bootstrapped from an unhygienic one, which is what we did in the case of Lean.} Note that \lstinline{quoteSyntax} is
allowed to reference the same \lstinline{msc} as
\lstinline{expandStxQuot} because they are part of the same macro call and the current macro scope is unchanged between them.
While alternative approaches that use fresh macro scopes on function calls \emph{within} a macro are thinkable, we prefer the presented behavior, which matches that of the Scheme family, because it preserves referential transparency: if \lstinline{quoteSyntax} is inlined into \lstinline{expandStxQuot}, the behavior is unchanged.

\subsection{Extended Quasiquotations}
\label{sec:quot}

Automatic hygiene can greatly simplify development of macros, but a convenient way for con- and destructing syntax is at least as important.
Before we get to more complex macro examples below, we want to describe some syntactic extensions to quotations and antiquotations we have
implemented that will come in useful.

A first obvious such extension is to allow quotations including antiquotations as patterns such as after \lstinline{match} or \lstinline{fun}.
\begin{lstlisting}
| `(())       => ...
| `(($e))     => ...
| `(($e, $f)) => ...
\end{lstlisting}
Because every use of patterns eventually unfolds to a \lstinline{match} in Lean, this is in fact implemented as a macro that expands \lstinline{match} terms with quotation patterns into ones without such patterns.
Note also that because no new syntactic identifiers are generated while matching against a quotation, there is no issue of hygiene in this case.

For syntax with repeated parts, quotation \emph{splices} enable us to match or introduce these parts as a whole.
For example, a recursive macro for $n$-tuple syntax can be written as
\begin{lstlisting}
| `(())          => `(Unit.unit)
| `(($e))        => e
| `(($e, $es,*)) => `(Prod.mk $e ($es,*))
\end{lstlisting}
Here \lstinline{$es,*} matches/introduces the remaining elements of the tuple, including its separators.
Analogous splicing syntax exists for other separators, as well as \lstinline{$x*} for separator-less iteration.
At most one splice can be used per sequence, but it can be pre- and suffixed with an arbitrary (but fixed) number of other elements.

In \lstinline{$x*}, \lstinline{x} has type \lstinline{Array Syntax}, the same type as the second argument of the \lstinline{node} constructor.
For \lstinline{$x,*} and similar we instead use the dependent wrapper type \lstinline{SepArray ","} that provides convenience access functions for the sequence both with and without separator elements.
Finally, we also provide implicit coercions between these types that automatically insert/remove/replace the separators accordingly.

While exposing splices as typed values in this way ensures that we can comfortably process or synthesize them procedurally as well, it is often more convenient to inspect splice contents immediately as part of the quotation.
For this we support extended splices \lstinline{$[...]*} etc.\ where the splice content is parsed like an element of the sequence and can contain nested antiquotations.
If used as a pattern, the match succeeds if and only if the nested pattern matches every element, in which case the contained antiquotations are each bound to an \lstinline{Array} of all corresponding element-wise matches.
\begin{lstlisting}
match stx with
| `(match $discr with $[| $patss,* => $branches]*) =>
-- discr : Syntax
-- patss : Array (SepArray ",")
-- branches : Array Syntax
\end{lstlisting}

By default, quotations are parsed as either terms or top-level commands, since these syntactic categories are both commonly used and should usually be disjoint.
Other syntactic categories, e.g.\ the category of universe \lstinline{level}s that heavily overlaps with \lstinline{term}, can be specified explicitly at the beginning of a quotation.
Similarly, antiquotations can be suffixed with a colon followed by a category or named parser where otherwise ambiguous.
\begin{lstlisting}
match levelStx with
| `(level| $id:ident) => ...  -- a universe variable
| `(level| _)         => ...  -- a universe placeholder
| `(level| $l)        => ...  -- any (other) universe term
\end{lstlisting}

For a full example of using these and other features, we can look at a macro rule unfolding syntax such as
\begin{lstlisting}
| some a, some b => some (a + b)
| _,      _      => none
\end{lstlisting}
\begin{minipage}{\linewidth}
\begin{lstlisting}
fun x.1 x.2 =>
match x.1, x.2 with
| some a, some b => some (a + b)
| _,      _      => none
\end{lstlisting}
\end{minipage}

\begin{figure}[tb]
\begin{lstlisting}[aboveskip=0pt,showlines=true,numbers=left]
| `(fun
| $ps1,* => $rhs1
$alts:matchAlt*) => do
let discrs ← ps1.getElems.mapM (fun _ => withFreshMacroScope `(x))
`(fun $discrs* =>
match $[$discrs:ident],* with
| $ps1,* => $rhs1
\end{lstlisting}
\caption[]{A macro rule for expanding a combined fun-match syntax.}
\label{fig:fun-match}
\end{figure}
The macro rule (\cref{fig:fun-match}) derives the number of \emph{discriminants} (\lstinline{x.1, x.2} in the example) from the number of patterns of the first alternative; if other alternatives have differing number of patterns, it will lead to an elaboration error in \lstinline{match} later on. The macro then introduces a lambda abstraction over a sequence of fresh variable names of this number and subsequently matches on them using the given patterns.

It does so by matching on the first alternative of the match in detail, then capturing the remaining ones in \lstinline{alts : Array Syntax}.
The left-hand side \lstinline{ps1} of the first alternative is a \lstinline{SepArray ","}, so we use \lstinline{getElems} to access its elements and generate a fresh variable for each of them, which we do by running the single quotation \lstinline{`(x)} repeatedly under \lstinline{withFreshMacroScope}, annotating the variable with a unique macro scope each time\footnote{This is comparable to a call to the \lstinline{gensym} function found in many Lisp systems.}.

With \lstinline{discrs : Array Syntax} generated, we insert it into the final quotation, once as a straight sequence after \lstinline{fun} and once separated by commas after \lstinline{match}, followed by the alternatives copied from the input without changes.
Note that \lstinline{$discrs:ident*} would not have worked in this case because identifiers are merely a special case of the more general \lstinline{match} discriminant syntax that allows prefixing a discriminant with \lstinline{h:}, where the identifier \lstinline{h} will then hold the proof that the discriminant matched the corresponding pattern.
Thus there is no direct identifier sequence to insert and we have to instead say that we insert a sequence of general discriminants, each one built up of an identifier without a proof variable prefix, which internally will wrap each element in an additional syntax tree node of the \lstinline{matchDiscr} kind.
This necessary disambiguation of overlapping syntax sadly is a price we have to pay for our preference of such syntax over more regular but verbose one such as S-expressions.

Finally, for the sake of completeness we will mention the \emph{token antiquotation} \lstinline{%$x} that any token can be suffixed with to extract/set its \lstinline{SourceInfo} metadata.
This kind of antiquotation is mostly useful for displaying errors on specific tokens and preserving metadata in transformations. \\
\begin{minipage}{\linewidth}
\begin{lstlisting}
| `(tactic| case $tag =>%$arrTk $tac) => do
reportUnsolvedGoalsAt arrTk

case cons => skip
--^ unsolved goals displayed here
\end{lstlisting}
\end{minipage}

\section{Integrating Macros into Elaboration}
\label{sec:elab}

The macro system as described so far can handle most syntax sugars of Lean 3 except for ones requiring type information.
For example, the \emph{anonymous constructor} \lstinline{⟨e, ...⟩} is sugar for \lstinline{(c e ...)} if the expected type
of the expression is known and it is an inductive type with a single constructor \lstinline{c}. While trivial to parse,
there is no way to implement this syntax as a macro if expansion is done strictly prior to elaboration. A more complex
example is the \emph{structure instance notation} \lstinline!{ field1 := e, ...}! that must analyze the definition of the
given or inferred structure type in order to expand to the correct constructor call. To the best of
our knowledge, none of the ITPs listed in the introduction support hygienic elaboration extensions of this kind, but we
will show how to extend their common elaboration scheme in that way in this section.

Elaboration\footnote{at the term level; elaboration of other syntactic categories work analogously but with different output types} can be thought of
as a function \lstinline{elabTerm : Syntax → ElabM Expr} in an appropriate monad \lstinline{ElabM}\footnote{or some
other encoding of effects} from a (concrete or abstract) surface-level syntax tree type \lstinline{Syntax} to a fully-specified core
term type \lstinline{Expr}~[18]. We have presented the (concrete) definition of \lstinline{Syntax} in Lean
4 in \cref{sec:impl}; the particular definition of \lstinline{Expr} is not important here.
While such an elaboration system could readily be composed with a type-insensitive macro expander such as the one presented in \cref{sec:hygge}, we would
rather like to \emph{intertwine} the two to support type-sensitive but still hygienic-by-default macros (henceforth
called \emph{elaborators}) without having to reimplement macros of the kind discussed so far. Indeed, these can automatically
be adapted to the new type given an adapter between the two monads, similarly to the adaption of macros to
\emph{expanders} in [8]:
\begin{lstlisting}
def transformerToElaborator (t : Syntax → TransformerM Syntax) :
Syntax → ElabM Expr :=
fun stx => do
let stx' ← (transformerMToElabM t) stx
elabTerm stx'
\end{lstlisting}
Because most parts of our hygiene system are implemented by the expander for syntax quotations, the only changes to an
elaboration system necessary for supporting hygiene are storing the current macro scope in the elaboration monad (to be passed
to the expansion monad in the adapter) and allocating a fresh macro scope whenever a macro or elaborator is invoked. Thus elaborators immediately benefit from hygiene
as well whenever they use syntax quotations to construct unelaborated helper syntax objects to pass to \verb!elabTerm!.
In order to support syntax quotations in these two and other monads, we generalize their implementation to a new monad
typeclass implemented by both monads.
\begin{lstlisting}
class MonadQuotation (m : Type → Type) where
getCurrMacroScope : m MacroScope
withFreshMacroScope : m α → m α
\end{lstlisting}
The second operation is not used by syntax quotations directly, but can be used by procedural macros and elaborators to manually enter
new macro call scopes.

As an example, the following is a simplified implementation of the anonymous constructor syntax mentioned above.
\begin{lstlisting}
@[termElab anonymousCtor] def elabAnonymousCtor : Syntax → ElabM Expr
| `(⟨$args,*⟩) => do
let expectedType ← getExpectedType
match Expr.getAppFn expectedType with
| Expr.const constName _ _ => do
let ctors ← getCtors constName
match ctors with
| [ctor] => do
let stx ← `($(mkCIdent ctor) $args*)
elabTerm stx
...  -- error handling
\end{lstlisting}
The \lstinline{[termElab]} attribute registers this elaborator for the given syntax node kind.
The function \lstinline{mkCIdent : Name → Syntax}
synthesizes a hygienic reference to the given constant name by storing it as a top-level scope and applying a reserved
macro scope to the constructed identifier.
Note the monadic binding of the syntax quotation, and that the separators of \lstinline{$args,*} are implicitly discarded when it is used as a plain sequence \lstinline{$args*}.

This implementation fails if the
expected type is not yet sufficiently known at this point. The actual implementation\footnote{\url{https://github.com/leanprover/lean4/blob/IJCAR20-LMCS/src/Lean/Elab/BuiltinNotation.lean\#L16}} of this elaborator extends the code
by \emph{postponing} elaboration in this case. When an elaborator requests postponement,
the system returns a fresh metavariable as a placeholder and associates the input syntax tree with it. Before
finishing elaboration of a command, postponed elaborators associated with unsolved metavariables are retried until they all
ultimately succeed, or else elaboration is stuck because of cyclic dependencies and an error is signed.

%We originally
%planned to implement it as such and compose it with a type-insensitive macro expander, implementing type-sensitive
%syntax like anonymous constructors directly in the elaborator rather than as hygienic macros as a simple compromise.
%However, after being made aware of the \textsc{Turnstile} metalanguage~\cite{turnstile}, we became convinced that it is
%indeed possible to express elaboration of a nontrivial language via macro expansion in a sufficiently general system.
%Moreover, the Hackett project~\cite{hackett} provided not only another demonstration of Turnstile's approach, but also
%combined that with a \emph{multi-pass macro expansion}
%In Hackett's case, this was used to postpone typeclass inference to a second pass. Typeclass inference is not expressed
%via expansion in Lean 4 for performance reasons, but we are still making use of multi-pass expansion to relax Lean 3's
%strict left-to-right elaboration order. For example, Lean 4 can elaborate both of the following applications by one or
%two passes of left-to-right elaboration, respectively.
%foldl f ⟨a, b⟩ xs                   -- type flows from `f` to anon. constructor
%foldl (fun ⟨a, b⟩ c => ...) init xs  -- type flows from `init` to anon. constructor
%The multi-pass elaborating expander is an extension of the basic expander described in \cref{sec:impl}. The
%\lstinline{ExpanderM} monad is extended with new metadata such as the expected type and the metavariable context. In
%order to support multi-pass expansion, transformers take and return partially-expanded syntax objects of type
%\lstinline{Syntax Expr} where \lstinline{Expr} subtrees represent fully resolved and type-checked subterms. We embed
%this less general, optimized type instead of e.g.\ reflecting it into \lstinline{Syntax} because partial results from
%external parts like the aforementioned typeclass inference or tactic execution can quickly reach massive size.
%\todo{figure out the rest when we get there}

\section{Tactic Hygiene}
\label{sec:tactic}

Lean 3 includes a tactic framework that, much like macros, allows users to write custom automation either procedurally
inside a tactic monad or ``by example'' using tactic language quotations, or in a mix of both~[11].
For example, Lean 3 uses a short tactic block to prove injection lemmas for data constructors.
\begin{lstlisting}
def mkInjEq : TacticM Unit :=
`[intros; apply propext; apply Iff.intro; ...]
\end{lstlisting}
Unfortunately, this code unexpectedly broke in Lean 3 when used from a library for homotopy type theory that defined its own
\lstinline{propext} and \lstinline{Iff.intro} declarations;\footnote{\url{https://github.com/leanprover/lean/pull/1913}} in other
words, Lean 3 tactic quotations are unhygienic and required manual intervention in this case. Just like with
macros, the issue with tactics is that binding structure in such embedded terms is not known at declaration time. Only
at tactic run time do we know all local variables in the current context that preceding tactics may have added or
removed, and therefore the scope of each captured identifier.

Arguably, the Lean 3 implementation also exhibited a lack of hygiene in the handling of tactic-introduced identifiers:
it did not prevent users from referencing such an identifier outside of the scope it was declared in.
\begin{lstlisting}
def myTac : TacticM Unit := `[intro h]
lemma triv (p : Prop) : p → p := begin myTac; exact h end
\end{lstlisting}

Coq's similar Ltac tactic language~[7] exhibits the same issue and users are advised not to introduce
fixed names in tactic scripts but to generate fresh names using the \lstinline{fresh} tactic
first,\footnote{\url{https://github.com/coq/coq/issues/9474}} which can be considered a manual hygiene solution.

Lean 4 instead extends its automatically hygienic macro implementation to tactic scripts by allowing regular macros in the place of
tactic invocations.
\lstinputlisting[linerange=myTac-end]{supplement/Examples.lean}
By the same hygiene mechanism described above, introduced identifiers such as \lstinline{h} are renamed so as not to be
accessible outside of their original scope, while references to global declarations are preserved as top-level scope
annotations. Thus Lean 4's tactic framework resolves both hygiene issues discussed here without requiring manual
intervention by the user. Expansion of tactic macros in fact does not precede but is integrated into the \emph{tactic
evaluator} \lstinline{evalTactic : Syntax → TacticM Unit} such that recursive macro calls are expanded lazily,
allowing for combinators like \lstinline{repeat} that would otherwise lead to infinite recursion during expansion.
\begin{lstlisting}
syntax "repeat" tactic : tactic
| `(tactic| repeat $t) => `(tactic| try ($t; repeat $t))
\end{lstlisting}
Note that \lstinline{macro} cannot be used here because the parser for \lstinline{repeat} would not yet be available
in the right-hand side. When \lstinline{$t} eventually fails, the recursion is broken without visiting and expanding the
subsequent \lstinline{repeat} macro call. The \lstinline{try} tactical is used to ignore this eventual failure.

While we believe that macros will cover most use cases of Lean 3's tactic quotations in Lean 4, their use
within larger \lstinline{TacticM} metaprograms can be recovered by passing such a quotation to \lstinline{evalTactic}:
\lstinputlisting[linerange=myTac2-end]{supplement/Examples.lean}
\lstinline{TacticM} implements the \lstinline{MonadQuotation} typeclass for this purpose.

\section{Best-Effort Eager Name Analysis in Macros}
\label{sec:eager}

The dynamic nature of binding in macros has enabled us to implement many Lean language features as macros, with hygiene guaranteeing that bindings within the macro do not interfere with ones outside of it.
However, while knowing that a mistyped identifier in a macro will not be accidentally be bound by bindings at the use site is great in theory, in practice it would be even better to be told about the typo immediately while writing the macro!
This is especially true when renaming a declaration, either manually where we might accidentally miss an occurrence of it inside a macro and then must track name binding errors at use sites back to the responsible macro, or automatically where refactoring tools must treat macros as black boxes.
After all, a static view of a notation's binding structure is exactly what we gave up in \cref{sec:intro} in exchange for the ability to arbitrarily abstract over bindings.
For example, there is no general way to statically analyze whether \lstinline{x} inside the following quotation is well-scoped given an arbitrary computation resulting in \lstinline{stx}:
\begin{lstlisting}
let stx ← ...
`(fun $stx => x)
\end{lstlisting}
With this theoretical limitation in mind, and given that this is more of a practical issue of maintenance, perhaps a practical, best-effort solution is sufficient as long as we retain all hygiene guarantees.
We have done so with an \emph{opt-in}, partial but extensible approach to eager name resolution in macros based on a variant of our quotation syntax.
\begin{lstlisting}
``(fun x => x + $y + id z)  -- error: unknown identifier 'z'
\end{lstlisting}
A \emph{double-backtick} quotation eventually unfolds to the basic, single-backtick version and thus retains all its semantics.
Before that, however, it recursively checks for identifiers that can statically be assumed to be unbound using the following heuristics:
\begin{enumerate}
\item If there is a special \emph{precheck} hook registered for the syntax kind in question, we use it.
Precheck hooks can signal binding errors as well as recursively continue the precheck on nested syntax, possibly with an extended (untyped) \emph{quotation context}, which is initially empty.
For example, we provide a precheck hook for \lstinline{fun x => e} that recurses into \lstinline{e} after adding \lstinline{x} to the quotation context.
The central \emph{identifier} precheck hook ultimately raises an error if an identifier is reached that is neither in the global, extra-macro context, nor in the quotation context.
Other examples for precheck hooks we have added are for \lstinline{match} and function application.
\item Otherwise, if there are no identifiers in the quoted syntax, we assume that there is no risk of unbound ones, and the check succeeds.
In particular, antiquotations (which contain \emph{unquoted} identifiers only) are always skipped.
\item Otherwise, if the quoted syntax is a macro, we unfold it and precheck the result.
Here we assume that the macro is sufficiently good-natured: while macros are pure functions by definition in Lean, their behavior and in particular binding structure could in theory change drastically enough in the presence of antiquotations that it could lead to false positives of this analysis.
If that is the case, the user either has to provide a custom precheck hook for it, or fall back to the basic quotation syntax.

In contrast to macros, we cannot typically run elaborators directly during this check because they usually depend on type information that is not yet available, and are not guaranteed to be pure.
\item Otherwise the check fails since we do not know how to analyze the syntax at hand.
Again, users would either have to provide a precheck hook, or use to the single-backtick quotation syntax.
\end{enumerate}
This approach is clearly best-effort with many opportunities for unhandled cases.
However, since it is guaranteed that after the check the semantics are the same as for the basic quotation syntax, including unchanged hygiene guarantees, we believe that the practical advantages of using the syntax where possible are significant.
In particular, we have observed that quotations capturing global identifiers, which are most at risk of breaking during refactorings, are usually quite simple while complicated quotations that are used to translate one syntax into a more general one often do not reference any identifiers at all, and thus would not benefit from the additional check anyway.

This is especially true for notations, which are usually exceedingly simple in structure, most often consisting of nothing but an application of a global function symbol to the notation arguments, which is covered by the identifier and application precheck hooks.
Thus we have modified the \lstinline{notation} macro to use double-backtick quotations by default in order to make users immediately aware of any unbound identifiers inside of them, restoring its Lean 3 behavior (where the absence of macros naturally allowed for such a check).
\begin{lstlisting}
notation "∃" x "," e => Exits.intro (fun x => e)  -- error: unknown identifier 'Exits.intro'
\end{lstlisting}
We provide an option to disable this change, though all notations in the standard library passed the additional check without modification.
The check did on the other hand find a notation example in our documentation that contained an accidentally unbound identifier.

\section{Related Work}
\label{sec:related}

The main inspiration behind our hygiene implementation was Racket's new \emph{Sets of Scopes}~[12]
hygiene algorithm. Much like in our approach, Racket annotates identifiers both with scopes from their original context
as well as with additional macro scopes when introduced by a macro expansion. However, there are some significant
differences: Racket stores both types of scopes in a homogeneous, unordered set and does name resolution via a maximum-subset
check. For both simplicity of implementation and performance, we have reduced scopes to the bare minimal
representation using only strict equality checks, which we can easily encode in our existing \lstinline{Name}
implementation. In particular, we only apply scopes to matching identifiers and only inside syntax quotations. This
optimization is of special importance because top-level declarations in Lean and other ITPs are not part of a single,
mutually recursive scope as in Racket, but they each open their own scope over all subsequent declarations, which would
lead to a total number of scope annotations quadratic in the number of declarations using the Sets of Scopes algorithm.
Finally, Racket detects macro-introduced identifiers using a ``black-box'' approach without the
macro's cooperation following the marking approach of~13: a fresh macro scope is applied to all
identifiers in the macro input, then inverted on the macro output.
% The result is that the scope is left on all identifiers newly introduced by the macro.
While elegant, a naive implementation of this approach can again result in
quadratic runtime compared to unhygienic expansion and requires further optimizations in the form of lazy scope
propagation 9, which is difficult to implement in a pure language like Lean.
Our ``white-box'' approach based on the single primitive of an effectful syntax quotation, while slightly easier to escape
from in procedural syntax transformers, is simple to implement, incurs minimal overhead, and is equivalent for pattern-based

The idea of automatically handling hygiene in the macro, and not in the expander, was introduced in~[5], though only for
pattern-based macros. MetaML~[21] refined this idea by tying hygiene more specifically to syntax
quotations that could be used in larger metaprogram contexts, which Template Haskell~[20]
interpreted as effectful (monadic) computations requiring access to a fresh-names generator, much like in our design.
However, both of the latter systems should perhaps be characterized more as metaprogramming frameworks than Scheme-like macro
systems: there are no ``macro calls'' but only explicit splices and so only built-in syntax with known binding semantics
can be captured inside syntax quotations. Thus the question of which captured identifiers to rename becomes trivial
again, just like in the basic notation systems discussed in \cref{sec:intro}.

While the vast majority of research on hygienic macro systems has focused on S-expression-based languages, there have
been previous efforts on marrying that research with non-parenthetical syntax, with different solutions for combining syntax tree
construction and macro expansion. The Dylan language requires macro syntax to use predefined terminators
and eagerly scans for the end of a macro call using this knowledge~[2], while in Honu~[19] the syntactic structure of
a macro call is discovered during expansion by a process called ``enforestation''. The Fortress~[1] language
strictly separates the two concerns into grammar extensions %(described as Parsing Expression Grammars~\cite{peg})
and transformer declarations, much like we do. Dylan and Fortress are restricted to pattern-based macro declarations and
thus can make use of simple hygiene algorithms while Honu uses the full generality of the Racket macro expander. On the
other hand, Honu's authors ``explicitly trade expressiveness for syntactic simplicity''~[19]. In order to express the full
Lean language and desirable extensions in a macro system, we require both unrestricted syntax of macros and procedural

Many of the antiquotation extensions presented in \cref{sec:quot} have been inspired by similar syntax in Rust's pattern-based macro language, though we have opened their use to procedural macros as well, using appropriate type representations.

Many theorem provers such as Agda, Coq, Idris, and Isabelle not already based on
a macro-powered language provide restricted syntax extension mechanisms,
circumventing hygiene issues by statically determining binding as seen in \cref{sec:intro}. Extensions
that go beyond that do not come with automatic hygiene guarantees.
Agda's macros,\footnote{\url{https://agda.readthedocs.io/en/v2.6.0.1/language/reflection.html\#macros}} for example,
operate on the De Bruijn index-based core term level and are not
The ACL2 prover in contrast uses a subset of Common Lisp as its input language and adapts the hygiene algorithm of
9 based on renaming~[10]. The experimental Cur~[4] theorem prover is a
kind of dual to our approach: it takes an established language with hygienic macros, Racket, and extends it with a
dependent type system and theorem proving tools. ACL2 does not support tactic scripts, while in Cur they can be defined
via regular macros. However, this approach does not currently provide tactic hygiene as defined in
\cref{sec:tactic}.\footnote{\url{https://github.com/wilbowma/cur/issues/104}}
The Eisbach~[16] proof method language for Isabelle is notable in that while it allows for
reusable proof methods (comparable to Lean's tactics) to be abstracted over terms, these terms are analyzed and typechecked
before being passed to the proof method, and there is no interaction between names in different proof methods either
when using the ``structured'' proof style, so the question of hygiene is moot.
Using the ``unstructured'' proof style, the same hygiene issue as noted for other system can be triggered.
\begin{lstlisting}[morekeywords={method,apply}]
method my_allI =
rule_tac allI, rename_tac escaped

lemma "∀ x. x = x"
apply my_allI
apply (rule_tac t = escaped in refl)
\end{lstlisting}

%While we used Racket's hygiene algorithm~[12] as a basis for our adapted algorithm, parts of the optimized
%algorithm may appear similar to other hygiene approaches. The idea of storing a list of matching top-level definitions
%in particular is reminiscent of Clojure's automatic ``namespace qualification'' of quoted identifiers~\cite{clojure}.
%However, it should be noted that Clojure ``does not implement a full solution to hygienic macros'' in general and
%requires macro-local references to be marked explicitly for renaming.

\section{Conclusion}

We have proposed a new macro system for interactive theorem provers that enables syntactic abstraction and reuse far
beyond the usual support of mixfix notations. Our system is based on a novel hygiene algorithm designed with a focus on
minimal runtime overhead as well as ease of integration into pre-existing codebases, including integration into standard
elaboration designs to support type-directed macro expansion. Despite that, the algorithm is general enough to provide
a complete hygiene solution for pattern-based macros and provides flexible hygiene for procedural macros. We have also demonstrated
how our macro system can address unexpected name capture issues that haunt existing tactic frameworks. We have
implemented our method in the new version of the Lean theorem prover, Lean 4; it should be sufficiently attractive and
straightforward to implement to be adopted by other interactive theorem proving systems as well.

\paragraph{Acknowledgments.}
We are very grateful to
the anonymous reviewers,
David Thrane Christiansen,
Gabriel Ebner,
Matthew Flatt,
Sebastian Graf,
Alexis King,
Daniel Selsam,
Max Wagner
%and the anonymous reviewers
for extensive comments, corrections, and advice.

%% Bibliography
\bibliographystyle{splncs04}
\begin{thebibliography}{10}
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\urlprefix}{URL }
\providecommand{\doi}[1]{https://doi.org/#1}

[1]
Allen, E., Chase, D., Hallett, J., Luchangco, V., Maessen, J.W., Ryu, S.,
Steele~Jr, G.L., Tobin-Hochstadt, S., Dias, J., Eastlund, C., et~al.: The
{Fortress} language specification. Sun Microsystems  \textbf{139}(140), ~116

[2]
Bachrach, J., Playford, K., Street, C.: {D-expressions: Lisp power, Dylan
style}. Style DeKalb IL  (1999)

[3]
Barzilay, E., Culpepper, R., Flatt, M.: Keeping it clean with syntax
parameters. Proc. Wksp. Scheme and Functional Programming  (2011)

[4]
Chang, S., Ballantyne, M., Turner, M., Bowman, W.J.: Dependent type systems as
macros. Proceedings of the ACM on Programming Languages  \textbf{4}(POPL),
1--29 (2019)

[5]
Clinger, W., Rees, J.: Macros that work. In: Proceedings of the 18th ACM
SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 155--162

[6]
De~Moura, L., Ullrich, S.: The {Lean} 4 theorem prover and programming
language. In: International Conference on Automated Deduction. pp. 625--635.
Springer (2021)

[7]
Delahaye, D.: A tactic language for the system {Coq}. In: Logic for Programming
and Automated Reasoning, 7th International Conference, {LPAR} 2000,
Proceedings. pp. 85--95 (2000)

[8]
Dybvig, R.K., Friedman, D.P., Haynes, C.T.: Expansion-passing style: Beyond
conventional macros. In: Proceedings of the 1986 ACM conference on LISP and
functional programming. pp. 143--150 (1986)

[9]
Dybvig, R.K., Hieb, R., Bruggeman, C.: Syntactic abstraction in {Scheme}. Lisp
and symbolic computation  \textbf{5}(4),  295--326 (1993)

[10]
Eastlund, C., Felleisen, M.: Hygienic macros for {ACL2}. In: International
Symposium on Trends in Functional Programming. pp. 84--101. Springer (2010)

[11]
Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de~Moura, L.: A metaprogramming
framework for formal verification. Proc. ACM Program. Lang.  \textbf{1}(ICFP)
(Sep 2017). \doi{http://dx.doi.org/10.1145/3110278}

[12]
Flatt, M.: Binding as sets of scopes. In: Proceedings of the 43rd Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp.
705--717. POPL '16, ACM, New York, NY, USA (2016).
\doi{10.1145/2837614.2837620},
\url{http://doi.acm.org/10.1145/2837614.2837620}

[13]
Kohlbecker, E., Friedman, D.P., Felleisen, M., Duba, B.: Hygienic macro
expansion. In: Proceedings of the 1986 ACM conference on LISP and functional
programming. pp. 151--161 (1986)

[14]
Mahboubi, A., Tassi, E.: Mathematical components,
\url{https://math-comp.github.io/mcb/}

[15]
Marlow, S., et~al.: Haskell 2010 language report  (2010),
\url{https://www.haskell.org/onlinereport/haskell2010}

[16]
Matichuk, D., Murray, T., Wenzel, M.: Eisbach: A proof method language for
isabelle. Journal of Automated Reasoning  \textbf{56}(3),  261--282 (2016)

[17]
Moggi, E.: Notions of computation and monads. Information and computation
\textbf{93}(1),  55--92 (1991)

[18]
de~Moura, L., Avigad, J., Kong, S., Roux, C.: Elaboration in dependent type
theory (2015)

[19]
Rafkind, J., Flatt, M.: Honu: syntactic extension for algebraic notation
through enforestation. In: ACM SIGPLAN Notices. vol.~48, pp. 122--131. ACM

[20]
Sheard, T., Jones, S.P.: Template meta-programming for {Haskell}. In:
Proceedings of the 2002 ACM SIGPLAN workshop on Haskell. pp. 1--16. ACM

[21]
Taha, W., Sheard, T.: {MetaML} and multi-stage programming with explicit
annotations. Theoretical computer science  \textbf{248}(1-2),  211--242

[22]
Ullrich, S., de~Moura, L.: Beyond notations: Hygienic macro expansion for
theorem proving languages. In: International Joint Conference on Automated
Reasoning. pp. 167--182. Springer (2020)

\end{thebibliography}

\end{document}