Sebastian Ullrich ; Leonardo de Moura - Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages

lmcs:7421 - Logical Methods in Computer Science, April 13, 2022, Volume 18, Issue 2 -
Beyond Notations: Hygienic Macro Expansion for Theorem Proving LanguagesArticle

Authors: Sebastian Ullrich ORCID; Leonardo de Moura

    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.

    Volume: Volume 18, Issue 2
    Published on: April 13, 2022
    Accepted on: February 14, 2022
    Submitted on: April 30, 2021
    Keywords: Computer Science - Programming Languages

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1826 times.
    This article's PDF has been downloaded 1406 times.