Goosifying Recursive Functions

[ismailkuru]

Hi,

I am not sure if it is intended to capture the recursive function translations, but Goose can translate the recursive function in a format that you cannot load it to use Iris for verification. Concretely speaking, you can get a recursive function A translated into

Definition A: val := rec: "A" "n" "m" := .... (A "x" "y");; ..... where the recursive call is not in the format that you can get and use in Iris, i.e. wrapped inside string.

[upamanyus]

We had to fix a related issue, and now recursive functions also translate without the quotes (see c41249e835efe10b9c0a02aee3969101ba7b011f).

[tchajed]

I had not intended to support recursive functions, so thanks @upamanyus! (The translations use rec: so that the interpreter can produce a trace of functions called, which was useful for debugging back when we had more bugs.)

[upamanyus]

Reopening because I was wrong. It's not so straightforward to check when a function call is to the function that's being currently defined (not easy to correctly walk up the tree of ast.Scopes and check if the function shows up somewhere in there). Leaving this issue for later when someone really wants to use recursive functions.