Resugaring: Lifting Evaluation Sequences Through Syntactic Sugar

Syntactic sugar is pervasive in language technology. It is used to shrink the size of a core language; to define domain-specific languages; and even to let programmers extend their language. Unfortunately, syntactic sugar is eliminated by transformation, so the resulting programs become unfamiliar to authors. Thus, it comes at a price: it obscures the relationship between the user's source program and the program being evaluated.We address this problem by showing how to compute reduction steps in terms of the surface syntax. Each step in the surface language emulates one or more steps in the core language. The computed steps hide the transformation, thus maintaining the abstraction provided by the surface language. We make these statements about emulation and abstraction precise, prove that they hold in our formalism, and verify part of the system in Coq. We have implemented this work and applied it to three very different languages.