Code duplication in mutually recursive functions

[lastland]

Issue by trommler
Thursday Aug 13, 2020 at 14:13 GMT
Originally opened as antalsz/hs-to-coq#162

---

When translating mutually recursive functions hs-to-coq generates one Definition, which contains a fix, for each of the mutually recursive functions. Each of those definitions must contain code for all functions in the mutual fixed point leading to code duplication linear in the number of mutually recursive functions in the mutual fixed point.

A small reproducer for this issue is the testcase for mutual recursion. In the generated file Mutrec.v note the two definitions that differ only in the for clause at the end.

Code duplication can be avoided by translating to a Fixpoint as follows:

Fixpoint f1 (arg_0__: list T) : list T
        := match arg_0__ with
           | nil => nil
           | cons x xs => (cons x (f2 xs))
           end with f2 (arg_0__ : list T) : list T
                      := match arg_0__ with
                         | nil => nil
                         | cons y ys => (cons y (f1 ys))
                         end.