Automatic refactoring for Agda

Abstract

The task of making changes to an existing code base to improve performance, legibility, or extensibility while preserving behaviour is important to virtually any program. Many times this involves making changes requiring a great deal of typing in various places, which is tedious and error-prone. Consequently, programs known as refactoring engines are used to take over the predictable parts of this task. However, although common for imperative and object-oriented languages, refactoring engines for functional languages like Haskell are rare and those for dependently typed languages are nonexistent. This project lays the groundwork for a refactoring engine for Agda by describing useful refactorings and a handful of implementation strategies.