To assist programmers in developing and maintaining software, modern IDEs provide integrated support for refactoring code automatically. Implementing sound automated refactorings for modern programming languages is difficult, as refactorings may introduce name-binding errors or cause references to inadvertently resolve to wrong declarations. To prevent these problems, previous work by Schäfer et al. introduced locked references to separate binding preservation from transformation. Before transformation, all references are replaced by locked references, which vacuously resolve to a particular declaration. After transformation, these locked references must be replaced by concrete references that must resolve to the intended declaration. To synthesize these references, a faithful inverse of the name lookup functions of the underlying language must be defined.

Manually implementing such inverse lookup functions is challenging, however, as modern programming languages exhibit complex name-binding features to provide developers with fine-grained control over how to structure code. To solve this problem, we present an approach to derive these lookup functions automatically, based on type system specifications written in the Statix meta-DSL. Statix specifications consist of inference rules that describe well-typed programs. To cover name binding constraints, Statix uses queries over scope graphs, which are graphs representing the binding structure of a program. We use these queries to infer the names, and inference rules to discover the syntactical structure when synthesizing qualified references.

We evaluate our approach by applying our algorithm to a toy language that illustrates many name binding features, as well as 2159 Java refactoring tests used by IntelliJ. Together, this yields a principled approach to synthesizing references, which is sound by construction, automatic, and broadly applicable.