Alpha-renaming documentation / possible bug

[davidweichiang]

Currently alpha-renaming happens twice, right before type inference and right before FGG generation. There's a comment in the first call (written by me) that says that it is needed for type inference but I'm not really sure about that. This should be more clearly documented.

When I remove the first call to alphaRenameProgs, all tests pass except for reverse.ppl, and the error seems to come from a variable collision during derefun. But if derefun requires unique variable names, shouldn't the renaming happen right before derefun?

[davidweichiang]

Commit 7028563fd4e8655034eddec609bcca0122e7a9b7 was the one that made this bug much more likely to happen, by using the very generic name x for automatically-generated local variables.

[davidweichiang]

It seems to me that if show put a type annotation on every variable, then FGG generation would no longer need all variables to be renamed apart.

[colin-mcd]

When I initially wrote the transformation pipeline I decided to be liberal with alpha renaming. We definitely need to do something before type checking (see here), and it's possible we would need to do it before de/refun too. Your idea about adding type annotations to every variable seems right though, I think? Although it would make the rule labels even longer. If we did that, we might want to consider also adding a flag that makes the compiler output FGGs with shorter rule names (e.g. map case n of ... to A, \ x. x to B, etc.)

[davidweichiang]

Leaving this open for further discussion about whether there might be too much or too little alpha-renaming.