[FEATURE] Modify operator inlining for carrying types

[konnov]

Consider the following example:

A(x, y) == x + y

B(x) == A(x, 1) * A(1, y)

The current version of Inliner replaces A in be as follows:

B(x) == (x + 1) * (1 + y)

The new type checker and type inferer give us types before preprocessing. The most important part of the type information is the types of declarations: variable declarations, constant declarations, and operators declarations, including LET-definitions. To be able to carry this type information, we have to modify the inliner in a way that it implicitly introduces constant LET-definitions for the parameters and the result at the call sites:

B(x) ==
  LET A_result1 ==
    LET A_x1 == x IN
    LET A_y1 == 1 IN
    A_x1 + A_y1
  IN
  LET A_result2 ==
    LET A_x2 == x IN
    LET A_y2 == 1 IN
    A_x2 + A_y2
  IN
  A_result1 * A_result2

By doing so, we can define the types of the auxiliary definititions such as A_result1, A_x1, A_y1, ... These types are easily computed from the type contexts that are produced by the type checker. When we have this form, we can apply our usual preprocessing transformations and then re-run the type checker. The types of the auxiliary variables will contain enough information for finding the types of the inlined operator bodies.

[konnov]

As Jure @Kukovec noticed, this format is very similar to a stack machine. It looks like we are moving towards a particular TLA+ structure in our intermediate representation.

[konnov]

Maybe we need the form:

B(x) ==
  LET A_result1 ==
    LET A_x1 == x IN
    LET A_y1 == 1 IN
    A(x1, y1)
  IN
  LET A_result2 ==
    LET A_x2 == x IN
    LET A_y2 == 1 IN
    A(x2, y2)
  IN
  A_result1 * A_result2

[Kukovec]

Closed in #344.