I'm looking for a tool that implements the source code transformation "replace recursion by catamorphism" (fold etc.).
My application is that if the transformation succeeds, it implies that the program terminates. (roughly)
I don't want to make a big research project out of this, rather I think of quickly putting together a prototype that proves the concept.
Have you considered another approach? E.g. the Coq papers define its elimination constructs either as a catamorphism, or as a combination of case&fix, where the recursive calls are appropriately restricted to pass subterms as arguments. See for example Eduardo Gimenez's "Codifying guarded definition with recursive schemes". This paper also shows how to turn such a case&fix into a call to a catamorphism. Stefan