Introduce support for recursive functions

[Kukovec]

Currently, a at.forsyte.apalache.tla.lir.UnexpectedLanguageError is thrown if a recursive function is used. See #83 for an example specification.

[konnov]

It should be easy to do, as recursive functions -- in contrast to recursive operators -- do not require fixpoint computation.

[konnov]

Recursive functions seem to be harder to encode than we expected. There are a few problems to think about:

• We have to know the function co-domain, in order to define the function first and then constrain it with the function definition. Essentially, a function definition f[x \in S] == body becomes CHOOSE f \in S -> T: \A x \in S: body.
• Another problem is that it is way too easy to define a recursive function of an infinite domain, e.g., Fact[n \in Int] == (* factorial *). Although this function would terminate on every argument, it would require a quantified encoding.

[konnov]

To handle recursive functions differently from recursive operators, we have changed the intermediate representation of recursive functions. From now on, a recursive function is defined with a nullary operator whose body consists of the application of the operator TlaFunOper.recFunDef. The arguments of recFunDef are similar to those of a normal function constructor funDef, that is, the constructor for [x \in S |-> e]. The only difference is that the recursive function definition may refer to the function by applying the operator TlaFunOper.recFunRef.

Details to be added in #125.

[konnov]

We have added limited support for recursive functions, see the manual.