RAPT (Rewriting-based Automated Program Transformation system)


Overview

RAPT (Rewriting-based Automated Program Transformation system) is a program transformation system using transformation templates, which implements a framework of program transformation (See References). RAPT transforms many-sorted TRSs according to input correct templates with verification of its correctness.

Download

RAPT is currently implemented by SML#. The followings are archives of execution files, samples and proofs of the correctness of templates.

How to use

RAPT is a command line tool "rapt".

rapt (INPUTFILE)

shows intermediate results and output TRS if the transformation succeed. You can see the list of options by "rapt" or "rapt -h".

The format of input files

Input files of RAPT consist five parts FUNCTIONS, RULES, INPUT, OUTPUT, and HYPOTHESIS, which specify type information of functions, input program, input pattern of template, output pattern of template, and hypothesis of template. Each part is a list divided by ";", pattern variables are preceded by "?", and to distinguish variables from constants, the latter are followed by "()". Sum is an example of input for RAPT.


Experiments

Template 1

This template specifies transformations of recursive programs to iterative programs.

Template 2

This template specifies transformations of recursive programs to iterative programs. (The difference against template1 is the order of arguments in the right-hand side of the second rule.)

Template 3

This template specifies transformations of recursive programs to iterative programs. Template 3 is more general than template 1 and 2.

Template 4

This template specifies fusion transformations, which improves efficiency of programs by eliminating intermediate data.

Template 5

This template also specifies fusion transformations, which improves efficiency of programs by eliminating intermediate data. This template transforms programs with accumulators.

Template 6

This template specifies a tupling transformations, which improves efficiency of programs by eliminating redundant recursive calls. (This template is currently specialized for Fibonacci function :-().

Template 7-9

Templates 7, 8 and 9 are upgraded to the following template 10. So, omitted.

Template 10

This template specifies tupling transformations, which improves efficiency of programs by eliminating redundant recursive calls.


References


Yuki Chiba
chiba