| Summary: | 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.
|
|---|