Stratego -- Strategies for Program Transformation
tfof-deforest is a small demo package around a case study into transformation of functional programs, more specifically: on eliminating intermediate trees by deforestation.


Deforestation Theory

Based on Philip Wadler's paper: P. L. Wadler. Deforestation: transforming programs to eliminate trees. Theoretical Computer Science, 73(2):231--248, 1990.

Type Inferencing Theory

Tiny First-Order Functional language (TFOF)

TFOF Syntax

TFOF Tools


Listing of example tfof-files

TFOF Modules (*.tfmd)

  • datatypes.tfmd
    • Definition of basic datatypes (Tree and List)

  • basic-operators.tfmd
    • For typing purposes only: the standard arithmetic, relational and boolean operators.

  • list-basic.tfmd
    • A treeless definition of append (appending two lists).
    • Some list-flattening functions. flatten0 is not treeless, flatten1 and its helper flatten1' are treeless.

  • tree-basic.tfmd
    • A treeless definition of flip (at each Branch node, flip the two branches.
    • A non-treeless definition of fleaves (collect all leaves in a list)

  • int-arith.tfmd
    • Some basic integer computations.

  • list-arith.tfmd
    • Some computations on lists (sum, sequares, etc.)

  • tree-arith.tfmd
    • Some computations on trees (sum, sequares, etc.)

TFOF Example files (*.tfof)

  • append.tfof
    • term1a and term1b are two distinct nested FunApps? but should transform to the same resulting term and helper functions.
    • term2 is not linear, only inlining should occur.
    • term3 is just ok. Nothing should happen.

  • flatten.tfof
    • term1a calls the nontreeless flatten0 and should transform to two helper functions that are identical to flatten1 and flatten1'.
    • term1b does in fact the same, but now by literally containing the body of flatten0 already. Now only an equivalent of flatten1' should be generated.

  • flip.tfof
    • term1 is the example from Wadler's article, p.9.

  • leaves.tfof
    • t0 .. t4 only work if a separate rule for simple expressions is added, such that e.g. `(+) v 0' does not lead to additional inlining and deforestation.
    • t5 and t6 fail, since fleaves itself is non-treeless

  • nestedcase-renaming.tfof
    • Tests whether transformation of two nested case-statements correctly handles renaming (to prevent undesirable re-binding of variables)

  • typetest-*.tfof
    • Small tests for the type-inferencer.

  • test-1.tfof
    • Initially used as a parser test.
    • No valid input for deforestation.

  • test-2.tfof
    • Initially used as a parser test.
    • term1 is already treeless.

-- ArthurVanDam - 22 Mar 2004