10.7 Type expressions	10 C++ translator	10.9 Bindings
10.8 Value expressions

10.8 Value expressions

10.8.1 Evaluation order

The evaluation order in RSL is left-to-right. In C++ it is often not specified. So we need to be careful when translating expressions that are not readonly. For example, if any of the expressions e1, e2, or e3 is not readonly, then the application f(e1, e2, e3) is translated as if it had been written

This will translate in C++ to something like

t1 x1 = e1;
t2 x2 = e2;
f(x1, x2, e3)

As well as function applications, a similar approach is taken for enumerated sets, lists and maps.

10.8.2 Value literals

A value literal of type Text translates to the corresponding string.

A value literal of type Unit is ignored, or translated as the empty statement, or not accepted, depending on the context.

10.8.3 Names

10.8.4 Pre names

10.8.5 Basic expressions

10.8.6 Product expressions

10.8.7 Set expressions

static RSL_sI init_ranged_set(const int l_, const int r_){
RSL_sI s_;

s_ = RSL_sI();
for (int i_ = r_;
 i_ >= l_; i_--) {
s_ = RSL_sI(i_, s_);
}
return s_;
}

Note that the translator can only translate a set expression if its type can be uniquely determined from the context, i.e. it is not possible to translate the expression {} = {} without some disambiguation.

Comprehended set expressions

where b is a binding, T is a type, e is a translatable expression, slm is a translatable expression of set, list, or map type, and p is a translatable expression of type Bool.

For example, the expression { 2*i | i : Int • i ∈ s /\ i > 0 }, where s is of type Int-set, translates to

namespace RSL_Temp_3 {
// namespace for comprehended set
int RSL_Temp_4(const int i_3F1){
return 2 * i_3F1;
}

bool RSL_Temp_5(const int i_3F1){
return i_3F1 > 0;
}

} // end of namespace RSL_Temp_3

RSL_sI RSL_test_case_RSL_Temp_2(){
return RSL_compss<int, int>(RSL_Temp_3::RSL_Temp_4, RSL_Temp_3::RSL_Temp_5, s);
}

RSL_compss is a template function defined in a standard RSL library files to generate a set from a set. Its first two parameters are functions, one to generate the expression e in the comprehended set (here RSL_Temp_4), and one to evaluate the predicate p (here RSL_Temp_5). The third parameter is the expression slm (here the set s).

C++ does not allow functions to be defined locally to other functions or expressions, so RSL_Temp_4 and RSL_Temp_5 have to be defined externally, and they are placed in their own namespace. The use of a namespace is not essential, but the approach is close to that used for local expressions described in section 10.8.23. This results in a restriction that comprehended set expressions may not occur in recursive functions where the recursion is through the expression e or the predicate p. There are similar restrictions for comprehended lists and maps, for quantified expressions, and for implicit let expressions.

The reason for this restriction is that the extra functions needed for the expression e and the predicate p must be placed out of their original scope. But they may refer, for example, to the parameters of the function they are used in. So function parameters, and other locally defined names like let bindings, have to be copied to the namespace in which the extra functions are defined. But this technique is essentially static, and recursive calls of the same function would result in these copied variables being changed unpredictably.

10.8.8 List expressions

RSL_C++ includes ranged list expressions and enumerated list expressions, and some comprehended list expressions. A ranged list expression, such as 〈2 .. 7〉, translates to init_ranged_list(2, 7), where init_ranged_list is defined by

static RSL_sI init_ranged_list(const int l_, const int r_){
RSL_lI lst_;

lst_ = RSL_lI();
for (int i_ = r_;
 i_ >= l_; i_--) {
lst_ = RSL_lI(i_, lst_);
}
return lst_;
}

An enumerated list expression, such as 〈1,4,7〉, translates to
RSL_lI(1, RSL_lI(4, RSL_lI(7, RSL_lI()))).

Note that the translator can only translate a list expression if its type can be uniquely determined from the context, i.e. it is not possible to translate the expression 〈〉 = 〈〉 without some disambiguation.

A comprehended list expression can only be translated if it takes one of the forms

where b is a binding, e is a translatable expression, l is a translatable expression of list type, and p is a translatable expression of type Bool. The translation is very similar to that for comprehended sets: see section 10.8.7. Therefore comprehended list expressions may not occur in recursive functions where the recursion is through the expression e or the predicate p.

10.8.9 Map expressions

[ false ↦ 0, true ↦ 1 ] translates to
RSL_BmI(false, 0, RSL_BmI(true, 1, RSL_BmI())).

Note that the translator can only translate map expressions if their type can be uniquely determined from the context, i.e. it is not possible to translate the expression {} = dom [] without some disambiguation.

A comprehended map expression can only be translated if it takes one of the forms

where b is a binding, e1 and e2 are translatable expressions, T is a type, slm is a translatable expression of set, list, or map type, and p is a translatable expression of type Bool. The translation is very similar to that for comprehended sets: see section 10.8.7. Therefore comprehended map expressions may not occur in recursive functions where the recursion is through either of the expressions e1 or e2 or the predicate p.

10.8.10 Function expressions

10.8.11 Application expressions

A function application translates to a function call. This includes calls of constructors, destructors and reconstructors. Note that as a destructor translates into an inline function an application will translate directly into a C++ class member access.

A list application translates to an element selection: l(i) translates to l[i]. A map application translates to an element selection: m(b) translates to m[b]

10.8.12 Quantified expressions

where b is a binding, T is a type, slm is a translatable expression of set, list or map type, and p and q are translatable expressions of type Bool.

The translation involves generating functions which must be defined at the top level. Like the translation of comprehended expressions (section 10.8.7), this means that quantified expressions may not occur in recursive functions where the recursion is through the predicates p or q.

This restriction can require the user to rewrite functions involving quantifiers. For example, consider the common case of a map used to model a relation which may be transitive but should not be cyclic. A particular instance is the "bill of materials" where the map models the "parts" relation. We use natural numbers to model part identifiers.

The function parts gives the "explosion" of a part to give all its sub-parts.

The function part_of contains a quantified expression, and is also recursive through its predicate. So we must rewrite it for translation.

A standard technique is to replace the quantified expression with a separate function that uses a loop to calculate the same result. We can redefine part_of using a second function:

The two part_of functions are mutually recursive, but this recursion is bound to terminate (even if the relation is circular). Each recursive call of part_of (through part_of1) reduces the Bom parameter (and it must terminate when this parameter is empty, since the first conjunct in its definition will be false). Each recursive call of part_of1 reduces the set parameter, and it terminates when this set is empty.

10.8.13 Equivalence expressions

10.8.14 Post expressions

10.8.15 Disambiguation expressions

10.8.16 Bracketed expressions

10.8.17 Infix expressions

An axiom infix expression translates as the equivalent if expression, as shown below.

10.8.18 Prefix expressions

An axiom prefix expression translates to an expression: ~ translates to !.

A universal prefix expression (□) is not accepted by the translator.

A value prefix expression translates to a function call, using the function names below.

10.8.19 Initialise expressions

10.8.20 Assignment expressions

Additional code, included if RSL_pre is defined, is generated if the type of x is a subtype, to check that e isin the subtype.

10.8.21 Input expressions

10.8.22 Output expressions

10.8.23 Local expressions

Local expressions that only declare variables and constant values are translated with the corresponding C++ definitions in-line.

Local expressions that declare functions need a special treatment, as functions may not be declared inside statements or expressions in C++.

So the C++ definitions arising from the declarations of a local expression that include functions are placed outside the definition in which it occurs. In fact they are placed inside their own namespace, as we shall see below.

Moving the declarations out of their original scope means that local bindings, in particular formal function parameters, will no longer be visible. To counter this, formal function parameters are defined as variables in the namespace and initialised from the original position of the local expression. Local explicit values are defined as variables and assigned their defining values after the parameter variables. Local variables are then assigned their initial values. This allows local values to depend on parameters, and the initial values of local variables to depend on parameters and local values.

As with comprehended expressions (section 10.8.7) this technique is essentially static and cannot deal with recursive functions. So recursive functions that contain local expressions defining functions are not accepted.

10.8.24 Let expressions

A simple let expressions like

translates to

int x_123 = 1;
k = x_123 + 1;

In the scope of

translates to

double i_B00 = z.RSL_f1;
double j_B02 = z.RSL_f2;
k = RSL_int(i_B00 * i_B00) + RSL_int(j_B02 * j_B02);

If the type Complex were a variant type rather than a record, the translation would be

if (!(z.RSL_tag == RSL_mk_Complex_tag))
{
RSL_fail("X.rsl:m:n: Let pattern does not match")
}
double i_B00 = (((RSL_mk_Complex_type*)z.RSL_ptr)->RSL_f1);
double j_B02 = (((RSL_mk_Complex_type*)z.RSL_ptr)->RSL_f2);
k = RSL_int(i_B00 * i_B00) + RSL_int(j_B02 * j_B02);

RSL_fail is a function that writes a message to standard output (if RSL_io is set) and then aborts.

In a record pattern such as used in (1), the function (here mk_Complex) must be the constructor of a record or variant.

An implicit let expression can only be translated if it has one of the forms

where b is a binding, T a type, slm a translatable expression of set, list, or map type, and p a translatable expression of type Bool.

For example,

(where s is a set) translates to

namespace RSL_Temp_16 {
// namespace for implicit let
bool RSL_Temp_15(const int x_B59){
return x_B59 > 0;
}
} // end of namespace RSL_Temp_16

int RSL_test_case_RSL_Temp_14(){
int x_B59 = RSL_chooses<int>(RSL_Temp_16::RSL_Temp_15, s);
k = x_B59;
}

If no suitable value can be found the RSL_chooses function will fail with the message "Choose from empty set".

The translation is similar to that for quantified expressions described in section 10.8.12, and for the same reason an implicit let cannot occur in a recursive function where the recursion is through the predicate p.

10.8.25 If expressions

An if expression translates to an if statement or an if expression. An if expression is used if there are no elsif branches and the then and else expressions translate without generating any statements.

Elsif branches translate to nested if statements.

10.8.26 Case expressions

A case pattern translates in general to a condition that the case expression matches the pattern, and one or more variable declarations (for the identifiers introduced in the pattern). The conditions are generally more complicated than can be handled by switch statements, and so if statements are used instead.

A temporary variable is used to ensure the expression being cased on is evaluated first and only once.

For example,

translates to

int RSL_Temp_18 = x;

int RSL_Temp_19;

if (RSL_Temp_18 == 2)
{
RSL_Temp_19 = 0;
}
else
{
if (RSL_Temp_18 == 1)
{
RSL_Temp_19 = 1;
}
else
{
RSL_Temp_19 = 2;
}
}
k = RSL_Temp_19;

In the scope of

the case expression

translates to

V RSL_Temp_1 = v;

if (RSL_Temp_1 == Vconst)
{
j = 5;
}
else
{
if (RSL_Temp_1.RSL_tag == RSL_Vrec_tag)
{
int a_454 = (((RSL_Vrec_type*)RSL_Temp_1.RSL_ptr)->RSL_f1);
j = a_454;
}
else
{
RSL_fail("X.rsl:m:n: Case exhausted");
}
}

RSL_fail is a function that writes a message to standard output (if RSL_io is set) and then aborts.

In a record pattern the function must be the constructor of a record or variant.

10.8.27 While expressions

translates to

for ( ; ; ) {
if (!(j >= k))
{
break;
}
j = j - 1;
}

10.8.28 Until expressions

translates to

do {
j = j + 1;
} while (!(j > k));

10.8.29 For expressions

translates to

{
for (int i_25D = 2;
 i_25D <= 5; i_25D++) {
if (i_25D >= 4)
{
k = k + i_25D;
}
}
}

Note that the scope of a for expression in RSL is not the same as the scope of a for statement in C++: care needs to be taken if the right limit is not pure, when it could be affected by the body of the loop. For example, if j is a variable,

translates to

{
int RSL_Temp_0 = j + 5;

for (int i_2C1 = j;
 i_2C1 <= RSL_Temp_0; i_2C1++) {
if (i_2C1 >= 4)
{
j = j + i_2C1;
}
}
}

If the list expression is an enumerated list expression, the translation introduces an array variable to hold the values.

translates to

{
int i_325;

int RSL_Temp_0[3];

RSL_Temp_0[0] = 1;
RSL_Temp_0[1] = 3;
RSL_Temp_0[2] = 5;
for (int x_ = 0;
 x_ < 3; x_++) {
i_325 = RSL_Temp_0[x_];
if (i_325 >= 4)
{
k = k + i_325;
}
}
}

If the list expression is neither a ranged list expression nor an enumerated list expression, it translates in the obvious way.

translates to

{
int i_389;

RSL_lI list_ = l;

int len_ = len(list_);

for (int x_ = 1;
 x_ <= len_; x_++) {
i_389 = list_[x_];
if (i_389 >= 4)
{
k = k + i_389;
}
}
}

An auxiliary variable list_ is always introduced to contain the list expression. This ensures the list expression is evaluated first and only once.

10.8 Value expressions
10.7 Type expressions	10 C++ translator	10.9 Bindings