Software engineers should be able to apply massive code refactorings to maintain large legacy code bases. A key aspect of developing restructurings is matching and transforming code snippets using abstract syntax trees (ASTs). Matching on ASTs is typically done through AST patterns with holes. AST patterns can be extended to become metapatterns, which increase their expressivity. Metapattern examples include disjunctions, descendant patterns, and patches where we inline transformations into the pattern itself. Despite their expressivity, abstract syntax (meta)patterns can become verbose and require restructuring engineers to be intimately familiar with the data types that define the AST. A better approach is to use concrete syntax patterns, which allows us to denote our patterns in the syntax of the object language. Previous work has shown that we can use external black-box parsers of the object language to compile concrete syntax patterns for arbitrary languages. In this paper, we scale this compilation method to support concrete syntax metapatterns, which allows for a more declarative way of expressing restructurings. We evaluate this method through an implementation written in Kotlin.

The goal of automated refactoring is to reduce maintenance effort. To realize this, programmers need to be able to trust or manually check that refactorings actually preserve behavior. To allow programmers to focus on such checks, automated refactorings should preserve program well-typedness. However, historically automated refactorings in popular IDEs could break well-typedness. The reason is that modern languages have complex name binding semantics which makes it hard to guarantee well-typedness in general. In recent work, scope graphs have been proposed as a uniform model for name binding. The model supports complex name binding patterns, and its uniformity makes it attractive to consider for verifying that refactorings preserve well-typedness. This paper explores how to prove that refactorings preserve well-typedness, using scope graphs. We consider a simple refactoring for merging modules in a toy module language, and prove that this refactoring preserves well-typedness. We give a generic template for proving well-typedness preservation using scope graphs, and discuss how this template relates to refactorings more generally.