Composite types

Options

An option is convenient when a variable may or may not have a value of a given type.

Declare

some andnone are the 2 operators to build an option value.
1
variable receiver : option<address> = none // to be set later ...
2
3
variable message : option<string> = some("there is a message")
Copied!

Test

issome and isnone are the 2 operators to test whether an option value is none or is some.
1
entry testopt (a : option<int>) {
2
requires {
3
r1 : issome(a);
4
}
5
failif {
6
f1 : isnone(a);
7
}
8
effect {
9
...
10
}
11
}
Copied!

Get

opt_get is the operator to extract the value from a some option value. It fails if the value is none.
1
effect {
2
var a = some("a string");
3
if issome(a) then (
4
if opt_get(a) = "a string" then transfer 1tz to coder;
5
);
6
}
Copied!

Tuples

Tuples are like vectors of values. For example, the following declares a tuple of three values, an integer on the first dimension, a string on the second and a bytes on the third:
1
variable t : int * string * bytes = (2020, "is the year of", 0x050100000009617263686574797065)
Copied!
The tuple type is built with * and the tuple value with (,) syntax.
The [ ] operator is used to project the tuple to one specific dimension:
1
effect {
2
var t = (2020, "is the year of", 0x050100000009617263686574797065);
3
var y = t[0]; /* 2020 */
4
var s = t[1]; /* "is the year of" */
5
var b = t[2]; /* 0x050100000009617263686574797065 */
6
}
Copied!
Projection fails if the dimension index is invalid.
The dimension index must be a straightforward literal of integer. It does not support any expression, even an expression that would reduce to an integer value. For example, the following does not compile:
1
var y = t[1-1]; /* does NOT compile! */
Copied!

Records

A record is a list of named values. For example, the following declares a record of two values:
1
record geoloc {
2
longitude : rational;
3
latitude : rational;
4
}
Copied!
It is possible to read and assign values to the fields of a record:
1
var r : geoloc = { /* Eiffel tower's location */
2
longitude = 48.8583701;
3
latitude = 2.2944813
4
};
5
var lo = r.longitude; /* lo = 48.8583701 */
6
var la = r.latitude; /* la = 2.2944813 */
7
/* let's go to another Eiffel's construction! */
8
r.longitude := 40.6892494;
9
r.latitude := 74.04;
Copied!
Last modified 8mo ago
Export as PDF
Copy link
Edit on GitHub