Composite types

Search…
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!
Conversions
Basic containers
Last modified 8mo ago
Export as PDF
Copy link
Edit on GitHub
Contents
Options
Tuples
Records