Synthesis of Recursive ADT Transformations from Reusable Templates

摘要: Recent work has proposed a promising approach to improving scalability of program synthesis by allowing the user supply syntactic template that constrains space potential programs. Unfortunately, creating templates often requires nontrivial effort from user, which impedes usability synthesizer. We present solution this problem in context recursive transformations on algebraic data-types. Our relies polymorphic constructs: small but powerful extension language templates, makes it possible define concise and highly reusable manner, while at same time retains benefits conventional templates. This enables end-users reuse predefined library for wide variety problems with little effort. The paper also describes novel optimization further improves performance system. evaluated set benchmarks most notably includes desugaring functions lambda calculus, force synthesizer discover Church encodings pairs boolean operations.