Nesting let expressions may reveal potential bugs

[gregr]

Hi, Ilya, thanks for sc-mini! I just finished reading the paper and the source, and noticed some things that didn't make sense to me, which may be unintended. By the way, this issue probably isn't a big deal since let expressions don't seem intended for use in the source language, and so won't appear in nested positions.

I noticed a few places where the handling of let expressions would cause problems if they appeared in nested positions (currently, they are only placed in outer positions during decomposition).

Based on how it's used, vnames should be extracting free variables, so should subtract the let parameter from the names retrieved from the body: https://github.com/ilya-klyuchnikov/sc-mini/blob/71388c1add9e76222564dcc8e4f1367626d1aa0a/DataUtil.hs#L56

I don't think you really want to substitute v' for v in e2' here, since v could legitimately be free in e2'. You really want the behavior you'd get from first substituting the argument for the let-bound parameter in both e2 and e2', then computing the renaming. A more efficient way of getting this would be to prime the renaming with [(v, v')] to ensure that other occurrences of v on the left, indicating that renaming v to anything else should fail; then removing this renaming since v is not actually a free variable in e2: https://github.com/ilya-klyuchnikov/sc-mini/blob/71388c1add9e76222564dcc8e4f1367626d1aa0a/DataUtil.hs#L77