A New Synthesis Tool for Agda

Abstract

Agda is a dependently typed functional programming language and proof assistant based on constructive type theory. Agda programmers spend most of their time working with unfinished programs where uncompleted parts are marked by holes. These holes can stand for anything from the core, complex parts of the program to trivial details. To allow programmers to focus on the complex parts of the program, Agda includes a synthesis tool called Agsy that can automatically fill in simple holes. Alas, the development of Agsy has not kept up with the evolution of Agda. Hence, Agsy fails to fill some trivial holes. This report describes a replacement for Agsy, named Mimer. To explain the methods used by Mimer, it also presents synthesis algorithms for two simple languages with meta-variables. The first is a simply typed A-calculus with products and sums. The second is a dependently typed A-calculus.