Allow mutually recursive functions

[caterinaurban]

From @mostafa-abdullah on July 20, 2017 12:58

Example

def f(x):
    if x == 0:
        return 1
    return g(x - 1)

def g(x):
    if x == 0:
        return 2
    return f(x - 1)

The approach I plan to take is to pre-analyze all function definitions and store the corresponding z3 types in the context, so when the inferencer encounters the g function call (whose definition didn't appear yet) it will have its type already in the context.

The problem with this is that it will allow some incorrect programs to type, like the following one:

def f(x):
    if x == 0:
        return 1
    return g(x - 1)

f(1)

def g(x):
    if x == 0:
        return 2
    return f(x - 1)

Because by the time f is called, g wouldn't have appeared yet.

What do you think? Do you think the above example is tolerable? Can we consider it as a normal run-time error that is not type-related?

Copied from original issue: caterinaurban/Lyra#43

[mostafa-abdullah]

Implemented in #32