Example fun_trans-1.0-0  is from 
www.ai.univie.ac.at/~markus/home/publications.html#mscthesis


  It contains code used in the MSc thesis of Markus Mottl.  Haven't
had time to study it very carefully.  It does program transformations.
It uses both second and third order constructs (see modules
let_ext.mod and tp_let_ext.mod).  It is non-Llambda and uses both
first order unification (for type inference) and higher order
unification (see below).

To run tests, do as in:

./main tests/poly.dat

poly.dat can be replaced by any other file name in the tests subdirectory.

Run all tests with

./testscript


data from poly.dat

Total number of calls to head_norm = 20432
Total number of calls to hnormOC = 333
Number of choice points between Beta and BetaPrime : 478
Number of Beta reductions : 865
Number of Beta-prime reductions : 478
Number of calls to lazy_read from head_norm : 2738
Number of iterations of lazy_read loop : 3158
Number of nested suspensions in lazy_read loop : 0
Adjusted number of lazy_read iterations : 3158
Number of calls to lread_withoc from hnormOC : 0
Number of calls to head_norm from lazy_read : 0

The following figures counts the number of substitutions,
i.e.: [[#1,ol,nl,(t,l)::e]] --> [[t,0,nl-l,nil]]:
R5-only occurrences (t is not a suspension, nl>l): 41
R5->R12 occurrences (t is a suspension, nl>l): 33
R5->R13 occurrences (nl = l): 660
Total number of these substitutions: 734
Cases of R5-only and R5->R12 where the skeleton is compound: 3
Cases of R5-only and R5->R12 where the skeleton is a bound variable: 37
Cases of R5->R13 where skeleton is not a free variable or constant (and not closed if annotations apply): 194
Cases of reindexing of compound term avoided because nl=0: 171
Cases of reindexing of compound term avoided because term is closed (no intersection with above case): 24
Number of times indices were adjusted: 63

Note the 3 instances of non-trivial reindexing.  

The reindexing cases do not appear to come from eta-expansion.  A quick
examination of the code leads me to believe that they're probably from
the following module.  This module contains explicit abstraction (as
opposed to pi goals).  It has embedded abstractions (inside the "lam"
structure), non-beta0 patterns, and the requisite open terms.
The second "curry" clause is the culprit.

module trafo.

accumulate terms.

curry (lam (x\ F (fst x) (snd x)))
      (lam (x1\ lam (x2\ F x1 x2))).

curry (rec (f\ x\ F (fst x) (snd x) (p1\ p2\ app f (pair p1 p2))))
      (rec (f\ x1\ lam (x2\ F x1 x2 (y1\ y2\ app (app f y1) y2)))).



Note that unification here is beyond second order, since F must have
an abstraction over an abstraction.

This is a very interesting example.  I wouldn't have written things
this way.  I don't believe that the use of third order unification
here is necessary.  It should also lead to needless non-determinism,
unless he's doing something like biasing projections over
imitations.

--- 
Data from testscript:  (Mottl's thesis examples)

Total number of calls to head_norm = 132331
Total number of calls to hnormOC = 1739
Number of choice points between Beta and BetaPrime : 4485
Number of Beta reductions : 5640
Number of Beta-prime reductions : 4485
Number of calls to lazy_read from head_norm : 18990
Number of iterations of lazy_read loop : 24290
Number of nested suspensions in lazy_read loop : 369
Adjusted number of lazy_read iterations : 23921
Number of calls to lread_withoc from hnormOC : 0
Number of calls to head_norm from lazy_read : 0

The following figures counts the number of substitutions,
i.e.: [[#1,ol,nl,(t,l)::e]] --> [[t,0,nl-l,nil]]:
R5-only occurrences (t is not a suspension, nl>l): 644
R5->R12 occurrences (t is a suspension, nl>l): 795
R5->R13 occurrences (nl = l): 5935
Total number of these substitutions: 7374
Cases of R5-only and R5->R12 where the skeleton is compound: 19
Cases of R5-only and R5->R12 where the skeleton is a bound variable: 910
Cases of R5->R13 where skeleton is not a free variable or constant (and not closed if annotations apply): 1908
Cases of reindexing of compound term avoided because nl=0: 1628
Cases of reindexing of compound term avoided because term is closed (no intersection with above case): 358
Number of times indices were adjusted: 979



---