5.4.7 Computations
On this page:
5.4.7.1 Comments
5.4.7.2 Blocks
5.4.7.3 Statements
5.4.7.3.1 const and function
const
function
5.4.7.3.2 return
return
5.4.7.3.3 if
if
else
5.4.7.3.4 switch
switch
case
default
5.4.7.3.5 Block statements
5.4.7.3.6 Try/  Catch & Throw Statements
5.4.7.3.7 Expression statements
5.4.7.4 Expressions
5.4.7.4.1 ’use strict’
5.4.7.4.2 Identifier reference
this
5.4.7.4.3 Function application
new
5.4.7.4.4 Types
Null
Bool
UInt
Bytes
Digest
Address
Token
Fun
Tuple
Object
Struct
Array
Data
Refine
type  Of
is  Type
is
5.4.7.4.5 Literal values
true
false
null
5.4.7.4.6 Operator expression
!
-
+
typeof
void
&&
||
*
/
%
|
&
^
<<
>>
==
!=
===
!==
>
>=
<=
<
and
or
add
sub
mul
div
mod
lt
le
ge
gt
lsh
rsh
band
bior
bxor
poly  Eq
poly  Neq
bool  Eq
type  Eq
int  Eq
digest  Eq
address  Eq
fxeq
ieq
5.4.7.4.7 xor
5.4.7.4.8 Padding
pad
5.4.7.4.9 Parenthesized expression
5.4.7.4.10 Tuples
5.4.7.4.11 array
array
5.4.7.4.12 Element reference
5.4.7.4.13 Array & tuple length:   Tuple.length, Array.length, and .length
length
5.4.7.4.14 Array & tuple update:   Tuple.set, Array.set, and .set
set
5.4.7.4.15 Array element type:   Array.elem  Type and .elem  Type
elem  Type
5.4.7.4.16 Foldable operations
Foldable
5.4.7.4.16.1 Foldable.for  Each && .for  Each
for  Each
5.4.7.4.16.2 Foldable.all && .all
all
5.4.7.4.16.3 Foldable.any && .any
any
5.4.7.4.16.4 Foldable.or && .or
5.4.7.4.16.5 Foldable.and && .and
5.4.7.4.16.6 Foldable.includes && .includes
includes
5.4.7.4.16.7 Foldable.count && .count
count
5.4.7.4.16.8 Foldable.size && .size
size
5.4.7.4.16.9 Foldable.min && .min
min
5.4.7.4.16.10 Foldable.max && .max
max
5.4.7.4.16.11 Foldable.sum && .sum
sum
5.4.7.4.16.12 Foldable.product && .product
product
5.4.7.4.16.13 Foldable.average && .average
average
5.4.7.4.17 Array group operations
5.4.7.4.17.1 Array.iota
iota
5.4.7.4.17.2 Array.replicate && .replicate
replicate
Array_  replicate
5.4.7.4.17.3 Array.concat && .concat
concat
5.4.7.4.17.4 Array.empty
Array_  empty
empty
5.4.7.4.17.5 Array.zip && .zip
zip
5.4.7.4.17.6 Array.map && .map
map
5.4.7.4.17.7 Array.map  With  Index && .map  With  Index
map  With  Index
5.4.7.4.17.8 Array.reduce && .reduce
reduce
5.4.7.4.17.9 Array.reduce  With  Index && .reduce  With  Index
reduce  With  Index
5.4.7.4.17.10 Array.index  Of && .index  Of
index  Of
5.4.7.4.17.11 Array.find  Index && .find  Index
find  Index
5.4.7.4.17.12 Array.find && .find
find
5.4.7.4.17.13 Array.with  Index && .with  Index
with  Index
5.4.7.4.17.14 Array.slice && .slice
slice
5.4.7.4.18 Mapping group operations
5.4.7.4.18.1 Map.reduce && .reduce
5.4.7.4.19 Objects
5.4.7.4.20 Structs
5.4.7.4.21 Field reference
5.4.7.4.22 Object.set
Object_  set
5.4.7.4.23 Object.set  If  Unset
Object_  set  If  Unset
5.4.7.4.24 Object.has
5.4.7.4.25 Data
5.4.7.4.26 Maybe
Maybe
Some
None
from  Maybe
is  None
is  Some
from  Some
maybe
5.4.7.4.27 Either
either
is  Left
is  Right
from  Left
from  Right
5.4.7.4.28 match
match
5.4.7.4.29 Conditional expression
?
ite
5.4.7.4.30 Arrow expression
=>
5.4.7.4.31 make  Enum
make  Enum
5.4.7.4.32 assert
assert
5.4.7.4.33 forall
forall
5.4.7.4.34 possible
possible
5.4.7.4.35 digest
digest
5.4.7.4.36 balance
balance
5.4.7.4.37 last  Consensus  Time
last  Consensus  Time
5.4.7.4.38 make  Deadline
make  Deadline
5.4.7.4.39 implies
implies
5.4.7.4.40 ensure
ensure
5.4.7.4.41 has  Random
has  Random
5.4.7.4.42 has  Console  Logger
has  Console  Logger
5.4.7.4.43 compose
compose
5.4.7.4.44 sqrt
sqrt
5.4.7.4.45 pow
pow
5.4.7.4.46 Signed Integers
Int
Pos
Neg
int
5.4.7.4.47 Fixed-Point Numbers
Fixed  Point
fx
fxint
fxrescale
fxunify
fxdiv
fxpow
fxpowui
5.4.7.4.48 Anybody
Anybody
5.4.7.4.49 Intervals
Interval
Interval  Type
5.4.7.4.49.1 Constructors
5.4.7.4.49.2 Accessors
5.4.7.4.49.3 Relational Operations
5.4.7.4.49.4 Arithmetic Operations
5.4.7.4.49.5 Other Operations
interval  Intersection
interval  Union
interval  Width
interval  Abs
0.1.3
5.4.7 Computations

This section describes the common features available in all Reach contexts.

5.4.7.1 Comments

// single-line comment
/* multi-line
 * comment
 */ 

Comments are text that is ignored by the compiler. Text starting with // up until the end of the line forms a single-line comment. Text enclosed with /* and */ forms a multi-line comment. It is invalid to nest a multi-line comment within a multi-line comment.

5.4.7.2 Blocks

{ return 42; }
{ const x = 31;
  return x + 11; }
{ if ( x < y ) {
    return "Why";
  } else {
    return "Ecks"; } } 

A block is a sequence of statements surrounded by braces, i.e. { and }.

5.4.7.3 Statements

This section describes the statements which are allowed in any Reach context.

Each statement affects the meaning of the subsequent statements, which is called its tail. For example, if {X; Y; Z;} is a block, then X’s tail is {Y; Z;} and Y’s tail is {Z;}.

Distinct from tails are continuations which include everything after the statement. For example, in {{X; Y;}; Z;}, X’s tail is just Y, but its continuation is {Y;}; Z;.

Tails are statically apparent from the structure of the program source code, while continuations are influenced by function calls.

A sequence of statements that does not end in a terminator statement (a statement with no tail), such as a return statement, continue statement, or exit statement is treated as if it ended with return null;.

The remainder of this section enumerates each kind of statement.

5.4.7.3.1 const and function

An identifier definition is either a value definition or a function definition. Each of these introduces one or more bound identifiers.

const DELAY = 10;
const [ Good, Bad ] = [ 42, 43 ];
const { x, y } = { x: 1, y: 2 };
const [ x, [ y ] ] = [ 1, [ 2 ] ];
const [ x, { y } ] = [ 1, { y: 2 } ];
const { x: [ a, b ] } = { x: [ 1, 2 ] };

Valid identifiers follow the same rules as JavaScript identifiers: they may consist of Unicode alphanumeric characters, or _ or $, but may not begin with a digit.

A value definition is written const LHS = RHS;.

LHS must obey the grammar:

 

LHS

 ::= 

id

 

  |  

[ LHS-tuple-seq ]

 

  |  

{ LHS-obj-seq }

 

LHS-tuple-seq

 ::= 

 

  |  

... LHS

 

  |  

LHS

 

  |  

LHS , LHS-tuple-seq

 

LHS-obj-seq

 ::= 

 

  |  

... LHS

 

  |  

LHS-obj-elem

 

  |  

LHS-obj-elem , LHS-obj-seq

 

LHS-obj-elem

 ::= 

id

 

  |  

propertyName : LHS

 

propertyName

 ::= 

id

 

  |  

string

 

  |  

number

 

  |  

[ expr ]

RHS must be compatible with the given LHS. That is, if a LHS is an LHS-tuple-seq, then the corresponding RHS must be a tuple with the correct number of elements. If a LHS is an LHS-obj-seq, then the corresponding RHS must be an object with the correct fields.

Those values are available as their corresponding bound identifiers in the statement’s tail.

function randomBool() {
  return (interact.random() % 2) == 0; }; 

A function definition, written function FUN(LHS_0, ..., LHS_n) BLOCK;, defines FUN as a function which abstracts its function body, the block BLOCK, over the left-hand sides LHS_0 through LHS_n.

Function parameters may specify default arguments. The expressions used to instantiate these parameters have access to any variables in the scope of which the function was defined. Additionally, these expressions may reference previous arguments of the function definition. Parameters with default arguments must come after all other parameters.

function f(a, b, c = a + 1, d = b + c) =>
  a + b + c + d;

The last parameter of a function may be a rest parameter, which allows the function to be called with an arbitrary number of arguments. A rest parameter is specified via ...IDENT, where IDENT is bound to a Tuple containing all the remaining arguments.

All identifiers in Reach programs must be unbound at the position of the program where they are bound, i.e., it is invalid to shadow identifiers with new definitions. For example,

const x = 3;
const x = 4; 

is invalid. This restriction is independent of whether a binding is only known to a single participant. For example,

Alice.only(() => {
  const x = 3; });
Bob.only(() => {
  const x = 3; }); 

is invalid.

The special identifier _ is an exception to this rule. The _ binding is always considered to be unbound. This means means that _ is both an identifier that can never be read, as well as an identifier that may be bound many times. This may be useful for ignoring unwanted values, for example:

const [_, x, _] = [1, 2, 3];

5.4.7.3.2 return

return 17;
return 3 + 4;
return f(2, false);
return; 

A return statement, written return EXPR;, where EXPR is an expression evaluates to the same value as EXPR. As a special case, return; is interpreted the same as return null;.

A return statement returns its value to the surrounding function application.

A return statement is a terminator statement, so it must have an empty tail. For example,

{ return 1;
  return 2; } 

is invalid, because the first return’s tail is not empty.

5.4.7.3.3 if

if ( 1 + 2 < 3 ) {
  return "Yes!";
} else {
  return "No, waaah!"; } 

A conditional statement, written if (COND) NOT_FALSE else FALSE, where COND is an expression and NOT_FALSE and FALSE as statements (potentially block statements), selects between the NOT_FALSE statement and FALSE statement based on whether COND evaluates to false.

Both NOT_FALSE and FALSE have empty tails, i.e. the tail of the conditional statement is not propagated. For example,

if ( x < y ) {
  const z = 3; }
else {
  const z = 4; }
return z; 

is erroneous, because the identifier z is not bound outside the conditional statement.

A conditional statement may only include a consensus transfer in NOT_FALSE or FALSE if it is within a consensus step, because its statements are in the same context as the conditional statement itself.

5.4.7.3.4 switch

const mi = Maybe(UInt).Some(42);
switch ( mi ) {
 case None: return 8;
 case Some: return mi + 10; }
switch ( mi ) {
 case None: return 8;
 default: return 41; } 

A switch statement, written switch (VAR) { CASE ... }, where VAR is a variable bound to a data instance and CASE is either case VARIANT: STMT ..., where VARIANT is a variant, or default: STMT ..., STMT is a sequence of statements, selects the appropriate sequence of statements based on which variant VAR holds. Within the body of a switch case, VAR has the type of variant; i.e. in a Some case of a Maybe(UInt) switch, the variable is bound to an integer.

All cases have empty tails, i.e. the tail of the switch statement is not propagated.

A switch statement may only include a consensus transfer in its cases if it is within a consensus step, because its statements are in the same context as the conditional statement itself.

It is invalid for a case to appear multiple times, or be missing, or to be superfluous (i.e. for a variant that does not exist in the Data type of VAR).

5.4.7.3.5 Block statements

A block statement is when a block occurs in a statement position, then it establishes a local, separate scope for the definitions of identifiers within that block. In other words, the block is evaluated for effect, but the tail of the statements within the block are isolated from the surrounding tail. For example,

const x = 4;
return x; 

evaluates to 4, but

{ const x = 4; }
return x; 

is erroneous, because the identifier x is not bound outside the block statement.

5.4.7.3.6 Try/Catch & Throw Statements

try {
  throw 10;
} catch (v) {
  transfer(v).to(A); }

A try statement, written try BLOCK catch (VAR) BLOCK, allows a block of code to execute with a specified handler should an exception be thrown.

A throw statement, written throw EXPR, will transfer control flow to the exception handler, binding EXPR to VAR. Any value that is able to exist at runtime may be thrown. For example, Ints and Arrays are valid values to throw, but a function is not.

5.4.7.3.7 Expression statements

4;
f(2, true); 

An expression, E, in a statement position is equivalent to the block statement { return E; }.

5.4.7.4 Expressions

This section describes the expressions which are allowed in any Reach context. There are a large variety of different expressions in Reach programs.

The remainder of this section enumerates each kind of expression.

5.4.7.4.1 ’use strict’

'use strict'; 

'use strict' enables unused variables checks for all subsequent declarations within the current scope. If a variable is declared, but never used, there will be an error emitted at compile time.

strict mode will reject some code that is normally valid and limit how dynamic Reach’s type system is. For example, normally Reach will permit expressions like the following to be evaluated:

const foo = (o) =>
  o ? o.b : false;

void foo({ b: true });
void foo(false); 

Reach allows o to be either an object with a b field or false because it partially evaluates the program at compile time. So, without 'use strict', Reach will not evaluate o.b when o = false and this code will compile successfully.

But, in strict mode, Reach will ensure that this program treats o as having a single type and detect an error in the program as follows:

reachc: error: Invalid field access. Expected object, got: Bool

The correct way to write a program like this in strict mode is to use Maybe. Like this:

const MObj = Maybe(Object({ b : Bool }));

const foo = (mo) =>
  mo.match({
    None: (() => false),
    Some: ((o) => o.b)
  });

void foo(MObj.Some({ b : true }));
void foo(MObj.None()); 

5.4.7.4.2 Identifier reference

X
Y
Z 

An identifier, written ID, is an expression that evaluates to the value of the bound identifier.

The identifier this has a special meaning inside of a local step (i.e. the body of an only or each expression), as well as in a consensus step (i.e. the tail of publish or pay statement and before a commit statement). For details, see this and this.

5.4.7.4.3 Function application

assert( amount <= heap1 )
step( moveA )
digest( coinFlip )
interact.random()
declassify( _coinFlip ) 

A function application, written EXPR_rator(EXPR_rand_0, ..., EXPR_rand_n), where EXPR_rator and EXPR_rand_0 through EXPR_rand_n are expressions that evaluate to one value. EXPR_rator must evaluate to an abstraction over n values or a primitive of arity n. A spread expression (...expr) may appear in the list of operands to a function application, in which case the elements of the expr are spliced in place.

new f(a) is equivalent to f.new(a) and is a convenient short-hand for writing class-oriented programs.

5.4.7.4.4 Types

Reach’s types are represented with programs by the following identifiers and constructors:

Object and Data are commonly used to implemented algebraic data types in Reach.

typeOf(x) // type
isType(t) // Bool
is(x, t) // t

The typeOf primitive function is the same as typeof: it returns the type of its argument.

The isType function returns true if its argument is a type. Any expression satisfying isType is compiled away and does not exist at runtime.

The is function returns its first argument if it satisfies the type specified by the second argument. If it is not, then the program is invalid. For example, is(5, UInt) returns 5, while is(5, Bool) is an invalid program. The value returned by is may not be identical to the input, because in some cases, such as for functions, it will record the applied to type and enforce it on future invocations. These applications are considered negative positions for Refine.

5.4.7.4.5 Literal values

10
0xdeadbeef
007
-10
34.5432
true
false
null
"reality bytes"
'it just does' 

A literal value, written VALUE, is an expression that evaluates to the given value.

The null literal may be written as null.

Numeric literals may be written in decimal, hexadecimal, or octal. Numeric literals must obey the bit width of UInt if they are used as UInt values at runtime, but if they only appear at compile-time, then they may be any positive number. Reach provides abstractions for working with Ints and signed FixedPoint numbers. Ints may be defined by applying the unary + and - operators to values of type UInt. Reach provides syntactic sugar for defining signed FixedPoint numbers, in base 10, with decimal syntax.

Boolean literals may be written as true or false.

String literals (aka byte strings) may be written between double or single quotes (with no distinction between the different styles) and use the same escaping rules as JavaScript. Since Bytes types are specialized in their length, literals typically needed to be padded to be useful.

5.4.7.4.6 Operator expression

An operator is a special identifier, which is either a unary operator, or a binary operator.

! a  // not
- a  // minus
+ a  // plus
typeof a
void a

A unary expression, written UNAOP EXPR_rhs, where EXPR_rhs is an expression and UNAOP is one of the unary operators: ! - + typeof void. All the unary operators, besides typeof, have a corresponding named version in the standard library.

It is invalid to use unary operations on the wrong types of values.

When applied to values of type UInt, unary - and + operators will cast their arguments to type Int. The unary - and + operations are defined for values of type: Int, and FixedPoint.

void a evaluates to null for all arguments.

a && b
a || b
a + b
a - b
a * b
a / b
a % b
a | b
a & b
a ^ b
a << b
a >> b
a == b
a != b
a === b
a !== b
a > b
a >= b
a <= b
a < b 

Bitwise operations are not supported by all consensus networks and greatly decrease the efficiency of verification.

A binary expression, written EXPR_lhs BINOP EXPR_rhs, where EXPR_lhs and EXPR_rhs are expressions and BINOP is one of the binary operators: && || + - * / % | & ^ << >> == != === !== > >= <= <. Numeric operations, like + and >, only operate on numbers. Since all numbers in Reach are integers, operations like / truncate their result. Boolean operations, like &&, only operate on booleans. It is invalid to use binary operations on the wrong types of values.

and(a, b)     // &&
or(a, b)      // ||
add(a, b)     // +
sub(a, b)     // -
mul(a, b)     // *
div(a, b)     // /
mod(a, b)     // %
lt(a, b)      // <
le(a, b)      // <=
ge(a, b)      // >=
gt(a, b)      // >
lsh(a, b)     // <<
rsh(a, b)     // >>
band(a, b)    // &
bior(a, b)    // |
bxor(a, b)    // ^
polyEq(a, b)  // ==, ===
polyNeq(a, b) // !=, !==

All binary expression operators have a corresponding named function in the standard library. While && and || may not evaluate their second argument, their corresponding named functions and and or, always do.

polyEq(a, b)    // eq on all types
boolEq(a, b)    // eq on Bool
typeEq(a, b)    // eq on types
intEq(a, b)     // eq on UInt
digestEq(a, b)  // eq on Digest
addressEq(a, b) // eq on Addresses
fxeq(a, b)      // eq on FixedPoint
ieq(a, b)       // eq on Int

Equality functions, like ==, ===, !=, and !==, operate on all types. However, values with different types are always not equal. Both arguments must be of the same type. Specialized functions exist for equality checking on each supported type.

If verifyArithmetic is true, then arithmetic operations automatically make a static assertion that their arguments would not overflow the bit width of the enable consensus networks. If it is false, then the connector will ensure this dynamically.

5.4.7.4.7 xor

xor(false, false); // false
xor(false, true);  // true
xor(true, false);  // true
xor(true, true);   // false 

xor(Bool, Bool) returns true only when the inputs differ in value.

5.4.7.4.8 Padding

Bytes(16).pad('abc');

Bytes are like Arrays in that they fixedly and exactly sized. This means that two Bytes of different lengths are usable in the same contexts.

For example, 'You win!' and 'You lose!' cannot both be provided to an interact function, because the second is one character longer. Most of the time this is good, because it is a signal that you should use a Data type instead, so that the formatting and display logic is entirely controlled by the frontend.

But, sometimes it is necessary and useful to extend one byte string into a larger size. Each Bytes type has a pad field that is bound to a function that extends its argument to the needed size. A byte string extended in this way is called padded, because it is extended with additional NUL bytes.

5.4.7.4.9 Parenthesized expression

(a + b) - c 

An expression may be parenthesized, as in (EXPR).

5.4.7.4.10 Tuples

[ ]
[ 1, 2 + 3, 4 * 5 ] 

A tuple literal, written [ EXPR_0, ..., EXPR_n ], is an expression which evaluates to a tuple of n values, where EXPR_0 through EXPR_n are expressions.

...expr may appear inside tuple expressions, in which case the spreaded expression must evaluate to a tuple or array, which is spliced in place.

5.4.7.4.11 array

const x = array(UInt, [1, 2, 3]); 

Converts a tuple of homogeneous values of the specific type into an array.

5.4.7.4.12 Element reference

arr[3] 

A reference, written REF_EXPR[IDX_EXPR], where REF_EXPR is an expression that evaluates to an array, a tuple, or a struct and IDX_EXPR is an expression that evaluates to a natural number which is less than the size of the array, selects the element at the given index of the array. Indices start at zero.

If REF_EXPR is a tuple, then IDX_EXPR must be a compile-time constant, because tuples do not support dynamic access, because each element may be a different type.

If REF_EXPR is a mapping and IDX_EXPR evaluates to an address, then this reference evaluates to a value of type Maybe(TYPE), where TYPE is the type of the mapping.

5.4.7.4.13 Array & tuple length: Tuple.length, Array.length, and .length

Tuple.length(tup);
tup.length;
Array.length(arr);
arr.length; 

Tuple.length Returns the length of the given tuple.

Array.length Returns the length of the given array.

Both may be abbreviated as expr.length where expr evaluates to a tuple or an array.

5.4.7.4.14 Array & tuple update: Tuple.set, Array.set, and .set

Tuple.set(tup, idx, val);
tup.set(idx, val);
Array.set(arr, idx, val);
arr.set(idx, val); 

Tuple.set Returns a new tuple identical to tup, except that index idx is replaced with val. The idx must be a compile-time constant, because tuples do not support dynamic access, because each element may be a different type.

Array.set Returns a new array identical to arr, except that index idx is replaced with val.

Both may be abbreviated as expr.set(idx, val) where expr evaluates to a tuple or an array.

5.4.7.4.15 Array element type: Array.elemType and .elemType

Array.elemType(arr)
arr.elemType 

Array.elemType Returns the Type of elements that the array contains.

5.4.7.4.16 Foldable operations

The following methods are available on any Foldable containers, such as: Arrays and Maps.

5.4.7.4.16.1 Foldable.forEach && .forEach

c.forEach(f)
Foldable.forEach(c, f)
Array.forEach(c, f)
Map.forEach(c, f) 

Foldable.forEach(c, f) iterates the function f over the elements of a container c, discarding the result. This may be abbreviated as c.forEach(f).

5.4.7.4.16.2 Foldable.all && .all

Foldable.all(c, f)
Array.all(c, f)
Map.all(c, f)
c.all(f) 

Foldable.all(c, f) determines whether the predicate, f, is satisfied by every element of the container, c.

5.4.7.4.16.3 Foldable.any && .any

Foldable.any(c, f)
Array.any(c, f)
Map.any(c, f)
c.any(f) 

Foldable.any(c, f) determines whether the predicate, f, is satisfied by at least one element of the container, c.

5.4.7.4.16.4 Foldable.or && .or

Foldable.or(c)
Array.or(c)
Map.or(c)
c.or() 

Foldable.or(c) returns the disjunction of a container of Bools.

5.4.7.4.16.5 Foldable.and && .and

Foldable.and(c)
Array.and(c)
Map.and(c)
c.and() 

Foldable.and(c) returns the conjunction of a container of Bools.

5.4.7.4.16.6 Foldable.includes && .includes

Foldable.includes(c, x)
Array.includes(c, x)
Map.includes(c, x)
c.includes(x) 

Foldable.includes(c, x) determines whether the container includes the element, x.

5.4.7.4.16.7 Foldable.count && .count

Foldable.count(c, f)
Array.count(c, f)
Map.count(c, f)
c.count(f) 

Foldable.count(c, f) returns the number of elements in c that satisfy the predicate, f.

5.4.7.4.16.8 Foldable.size && .size

Foldable.size(c)
Array.size(c)
Map.size(c)
c.size() 

Foldable.size(c) returns the number of elements in c.

5.4.7.4.16.9 Foldable.min && .min

Foldable.min(c)
Array.min(c)
Map.min(c)
c.min() 

Foldable.min(arr) returns the lowest number in a container of UInts.

5.4.7.4.16.10 Foldable.max && .max

Foldable.max(c)
Array.max(c)
Map.max(c)
c.max() 

Foldable.max(c) returns the largest number in a container of UInts.

5.4.7.4.16.11 Foldable.sum && .sum

Foldable.sum(c)
Array.sum(c)
Map.sum(c)
c.sum() 

Foldable.sum(c) returns the sum of a container of UInts.

5.4.7.4.16.12 Foldable.product && .product

Foldable.product(c)
Array.product(c)
Map.product(c)
c.product() 

Foldable.product(c) returns the product of a container of UInts.

5.4.7.4.16.13 Foldable.average && .average

Foldable.average(c)
Array.average(c)
Map.average(c)
c.average() 

Foldable.average(c) returns the mean of a container of UInts.

5.4.7.4.17 Array group operations

Array is a Foldable container. Along with the methods of Foldable, the following methods may be used with Arrays.

5.4.7.4.17.1 Array.iota

Array.iota(5) 

Array.iota(len) returns an array of length len, where each element is the same as its index. For example, Array.iota(4) returns [0, 1, 2, 3]. The given len must evaluate to an integer at compile-time.

5.4.7.4.17.2 Array.replicate && .replicate

Array.replicate(5, "five")
Array_replicate(5, "five") 

Array.replicate(len, val) returns an array of length len, where each element is val. For example, Array.replicate(4, "four") returns ["four", "four", "four", "four"]. The given len must evaluate to an integer at compile-time.

5.4.7.4.17.3 Array.concat && .concat

Array.concat(x, y)
x.concat(y) 

Array.concat(x, y) concatenates the two arrays x and y. This may be abbreviated as x.concat(y).

5.4.7.4.17.4 Array.empty

Array_empty
Array.empty 

Array.empty is an array with no elements. It is the identity element of Array.concat. It may also be written Array_empty.

5.4.7.4.17.5 Array.zip && .zip

Array.zip(x, y)
x.zip(y) 

Array.zip(x, y) returns a new array the same size as x and y (which must be the same size) whose elements are tuples of the elements of x and y. This may be abbreviated as x.zip(y).

5.4.7.4.17.6 Array.map && .map

Array.map(arr, f)
arr.map(f) 

Array.map(arr, f) returns a new array, arr_mapped, the same size as arr, where arr_mapped[i] = f(arr[i]) for all i. For example, Array.iota(4).map(x => x+1) returns [1, 2, 3, 4]. This may be abbreviated as arr.map(f).

This function is generalized to an arbitrary number of arrays of the same size, which are provided before the f argument. For example, Array.iota(4).map(Array.iota(4), add) returns [0, 2, 4, 6].

5.4.7.4.17.7 Array.mapWithIndex && .mapWithIndex

Array.mapWithIndex(arr, f)
arr.mapWithIndex(f) 

Array.mapWithIndex(arr, f) is similar to Array.map, except it provides f with an additional argument, which is the index of the current element in arr. Unlike Array.map, this function is not generalized to an arbitrary number of arrays; it only accepts one array.

5.4.7.4.17.8 Array.reduce && .reduce

Array.reduce(arr, z, f)
arr.reduce(z, f) 

Array.reduce(arr, z, f) returns the left fold of the function f over the given array with the initial value z. For example, Array.iota(4).reduce(0, add) returns ((0 + 1) + 2) + 3 = 6. This may be abbreviated as arr.reduce(z, f).

This function is generalized to an arbitrary number of arrays of the same size, which are provided before the z argument. For example, Array.iota(4).reduce(Array.iota(4), 0, (x, y, z) => (z + x + y)) returns ((((0 + 0 + 0) + 1 + 1) + 2 + 2) + 3 + 3).

5.4.7.4.17.9 Array.reduceWithIndex && .reduceWithIndex

Array.reduceWithIndex(arr, z, f)
arr.reduceWithIndex(z, f) 

Array.reduceWithIndex(arr, z, f) is similar to Array.reduce, except it provides f with an additional argument, which is the index of the current element in arr. Unlike Array.reduce, this function is not generalized to an arbitrary number of arrays; it only accepts one array.

5.4.7.4.17.10 Array.indexOf && .indexOf

Array.indexOf(arr, x)
arr.indexOf(x) 

Array.indexOf(arr, x) returns the index of the first element in the given array that is equal to x. The return value is of type Maybe(UInt). If the value is not present in the array, None is returned.

5.4.7.4.17.11 Array.findIndex && .findIndex

Array.findIndex(arr, f)
arr.findIndex(f) 

Array.findIndex(arr, f) returns the index of the first element in the given array that satisfies the predicate f. The return value is of type Maybe(UInt). If no value in the array satisfies the predicate, None is returned.

5.4.7.4.17.12 Array.find && .find

Array.find(arr, f)
arr.find(f) 

Array.find(arr, f) returns the first element in the array, arr, that satisfies the predicate f. The return value is of type Maybe. If no value in the array satisfies the predicate, None is returned.

5.4.7.4.17.13 Array.withIndex && .withIndex

Array.withIndex(arr)
arr.withIndex() 

Array.withIndex(arr) returns an array where every element of arr is paired with its index. For example, array(Bool, [false, true]).withIndex() returns array(Tuple(Bool, UInt), [[false, 0], [true, 1]]).

5.4.7.4.17.14 Array.slice && .slice

Array.slice(arr, start, length)
arr.slice(start, length)

Array.slice(arr, start, length) returns a portion of arr, starting from the start index, up to the start + length index.

5.4.7.4.18 Mapping group operations

Map is a Foldable container. Mappings may be aggregated with the following operations and those of Foldable within the invariant of a while loop.

5.4.7.4.18.1 Map.reduce && .reduce

Map.reduce(map, z, f)
map.reduce(z, f) 

Map.reduce(map, z, f) returns the left fold of the function f over the given mapping with the initial value z. For example, m.reduce(0, add) sums the elements of the mapping. This may be abbreviated as map.reduce(z, f).

The function f must satisfy the property, for all z, a, b, f(f(z, b), a) == f(f(z, a), b), because the order of evaluation is unpredictable.

5.4.7.4.19 Objects

{ }
{ x: 3, "yo-yo": 4 }
{ [1 < 2 ? "one" : "two"]: 5 }

An object, typically written { KEY_0: EXPR_0, ..., KEY_n: EXPR_n }, where KEY_0 through KEY_n are identifiers or string literals and EXPR_0 through EXPR_n are expressions, is an expression which evaluates to an object with fields KEY_0 through KEY_n.

Additional object literal syntax exists for convenience, such as:

{ ...obj, z: 5 }

An object splice, where all fields from obj are copied into the object; these fields may be accompanied by additional fields specified afterwards.

{ x, z: 5 }

Shorthand for { x: x, z: 5}, where x is any bound identifier.

5.4.7.4.20 Structs

const Posn = Struct([["x", UInt], ["y", UInt]]);
const p1 = Posn.fromObject({x: 1, y: 2});
const p2 = Posn.fromTuple([1, 2]);

A struct is a combination of a tuple and an object. It has named elements, like an object, but is ordered like a tuple, so its elements may be accessed by either name or position. Structs exist for interfacing with non-Reach remote objects, where both parties must agree to the runtime representation of the values.

A struct instance may be constructed by calling the fromTuple method of a struct type instance (like Posn) with a tuple of the appropriate length.

A struct instance may be constructed by calling the fromObject method of a struct type instance (like Posn) with an object with the appropriate fields.

Structs may be converted into a corresponding tuple or object via the toTuple and toObject methods on the Struct value (as well as struct type instances, like Posn in the example above):

assert(Posn.toTuple(p1)[0] == 1);
assert(Struct.toObject(p2).y == 2);

The names of elements may be restricted to avoid conflicting with reserved words of the specified connectors.

5.4.7.4.21 Field reference

obj.x

An object reference, written OBJ.FIELD, where OBJ is an expression that evaluates to an object or a struct, and FIELD is a valid identifier, accesses the FIELD field of object OBJ.

5.4.7.4.22 Object.set

Object.set(obj, fld, val);
Object_set(obj, fld, val);
{ ...obj, [fld]: val };

Returns a new object identical to obj, except that field fld is replaced with val.

5.4.7.4.23 Object.setIfUnset

Object.setIfUnset(obj, fld, val);
Object_setIfUnset(obj, fld, val);

Returns a new object identical to obj, except that field fld is val if fld is not already present in obj.

5.4.7.4.24 Object.has

Object.has(obj, fld);

Returns a boolean indicating whether the object has the field fld. This is statically known.

5.4.7.4.25 Data

const Taste = Data({Salty: Null,
                    Spicy: Null,
                    Sweet: Null,
                    Umami: Null});
const burger = Taste.Umami();

const Shape = Data({ Circle: Object({r: UInt}),
                     Square: Object({s: UInt}),
                     Rect: Object({w: UInt, h: UInt}) });
const nice = Shape.Circle({r: 5}); 

A data instance is written DATA.VARIANT(VALUE), where DATA is Data type, VARIANT is the name of one of DATA’s variants, and VALUE is a value matching the type of the variant. As a special case, when the type of a variant is Null, the VALUE may be omitted, as shown in the definition of burger in the same above.

Data instances are consumed by switch statements and match expressions.

5.4.7.4.26 Maybe

const MayInt = Maybe(UInt);
const bidA = MayInt.Some(42);
const bidB = MayInt.None(null);

const getBid = (m) => fromMaybe(m, (() => 0), ((x) => x));
const bidSum = getBid(bidA) + getBid(bidB);
assert(bidSum == 42); 

Option types are represented in Reach through the built-in Data type, Maybe, which has two variants: Some and None.

Maybe is defined by

export const Maybe = (A) => Data({None: Null, Some: A}); 

This means it is a function that returns a Data type specialized to a particular type in the Some variant.

Maybe instances can be conveniently consumed by fromMaybe(mValue, onNone, onSome), where onNone is a function of no arguments which is called when mValue is None, onSome is a function of on argument which is called with the value when mValue is Some, and mValue is a data instance of Maybe.

const m = Maybe(UInt).Some(5);
isNone(m); // false
isSome(m); // true

isNone is a convenience method that determines whether the variant is isNone.

isSome is a convenience method that determines whether the variant is isSome.

fromSome(Maybe(UInt).Some(1), 0); // 1
fromSome(Maybe(UInt).None(), 0);  // 0

fromSome receives a Maybe value and a default value as arguments and will return the value inside of the Some variant or the default value otherwise.

const add1 = (x) => x + 1;
maybe(Maybe(UInt).Some(1), 0, add1); // 2
maybe(Maybe(UInt).None(), 0, add1);  // 0

maybe(m, defaultVal, f) receives a Maybe value, a default value, and a unary function as arguments. The function will either return the application of the function, f, to the Some value or return the default value provided.

5.4.7.4.27 Either

Either is defined by

export const Either = (A, B) => Data({Left: A, Right: B}); 

Either can be used to represent values with two possible types.

Similar to Maybe, Either may be used to represent values that are correct or erroneous. A successful result is stored, by convention, in Right. Unlike None, Left may carry additional information about the error.

either(e, onLeft, onRight) 

either(e, onLeft, onRight) For an Either value, e, either will either apply the function onLeft or onRight to the appropriate variant value.

const e = Either(UInt, Bool);
const l = e.Left(1);
const r = e.Right(true);
isLeft(l);  // true
isRight(l); // false
const x = fromLeft(l, 0);      // x = 1
const y = fromRight(l, false); // y = false 

isLeft is a convenience method that determines whether the variant is Left.

isRight is a convenience method that determines whether the variant is Right.

fromLeft(e, default) is a convenience method that returns the value in Left, or default if the variant is Right.

fromRight(e, default) is a convenience method that returns the value in Right, or default if the variant is Left.

5.4.7.4.28 match

const Value = Data({
   EBool: Bool,
   EInt: UInt,
   ENull: Null,
 });
 const v1 = Value.EBool(true);
 const v2 = Value.EInt(200);
 const isTruthy = (v) =>
   v.match({
     EBool: (b) => { return b },
     EInt : (i) => { return i != 0 },
     ENull: ()  => { return false }
   });

 assert(isTruthy(v1));
 assert(isTruthy(v2));

A match expression, written VAR.match({ CASE ... }), where VAR is a variable bound to a data instance and CASE is VARIANT: FUNCTION, where VARIANT is a variant or default, and FUNCTION is a function that takes the same arguments as the variant constructor. If the variant has a type of Null, then the function is allowed to take no arguments. default functions must always take an argument, even if all defaulted variants have type Null.

match is similar to a switch statement, but since it is an expression, it can be conveniently used in places like the right hand side of an assignment statement.

Similar to a switch statement, the cases are expected to be exhaustive and nonredundant, all cases have empty tails, and it may only include a consensus transfer in its cases if it is within a consensus step.

5.4.7.4.29 Conditional expression

choosesFirst ? [ heap1 - amount, heap2 ] : [ heap1, heap2 - amount ] 

A conditional expression, written COND_E ? NOT_FALSE_E : FALSE_E, where COND_E, NOT_FALSE_E, and FALSE_E are expressions, selects between the values which NOT_FALSE_E and FALSE_E evaluate to based on whether COND_E evaluates to false.

ite(choosesFirst, [heap1 - amount, heap2], [heap1, heap2 - amount])

Conditional expressions may also be written with the ite function, however, note that this function always evaluates both of its branches, while the regular conditional expression only evaluates one branch.

5.4.7.4.30 Arrow expression

(() => 4)
((x) => x + 1)
((x) => { const y = x + 1;
          return y + 1; })
((x, y) => { assert(x + y == 3); })(1, 2);
((x, y) => { assert(x + y == 3); })(...[1, 2]);
((x, y = 2) => { assert(x + y == 3); })(1);
((x, y = 2) => { assert(x + y == 2); })(1, 1);
(([x, y]) => { assert(x + y == 3); })([1, 2]);
(({x, y}) => { assert(x + y == 3); })({x: 1, y: 2});
(([x, [y]]) => { assert(x + y == 3); })([1,[2]]);
(([x, {y}]) => { assert(x + y == 3); })([1,{ y: 2 }]);
((...xs) => Foldable.sum(xs))(1, 2, 3)

An arrow expression, written (LHS_0, ..., LHS_n) => EXPR, where LHS_0 through LHS_n are left-hand sides and EXPR is an expression, evaluates to an function which is an abstraction of EXPR over n values compatible with the respective left-hand side. Like function definitions, arrow expressions may use default argument notation and rest parameters.

5.4.7.4.31 makeEnum

const [ isHand, ROCK, PAPER, SCISSORS ] = makeEnum(3); 

An enumeration (or enum, for short), can be created by calling the makeEnum function, as in makeEnum(N), where N is the number of distinct values in the enum. This produces a tuple of N+1 values, where the first value is a Fun([UInt], Bool) which tells you if its argument is one of the enum’s values, and the next N values are distinct UInts.

5.4.7.4.32 assert

assert( claim, [msg] ) 

A static assertion which is only valid if claim always evaluates to true.

The Reach compiler will produce a counter-example (i.e. an assignment of the identifiers in the program to falsify the claim) when an invalid claim is provided. It is possible to write a claim that actually always evaluates to true, but for which our current approach cannot prove always evaluates to true; if this is the case, Reach will fail to compile the program, reporting that its analysis is incomplete. Reach will never produce an erroneous counter-example.

It accepts an optional bytes argument, which is included in any reported violation.

See the guide section on verification to better understand how and what to verify in your program.

5.4.7.4.33 forall

forall( Type )
forall( Type, (var) => BLOCK ) 

The single argument version returns an abstract value of the given type. It may only be referenced inside of assertions; any other reference is invalid.

The two argument version is an abbreviation of calling the second argument with the result of forall(Type). This is convenient for writing general claims about expressions, such as

forall(UInt, (x) => assert(x == x)); 

5.4.7.4.34 possible

possible( claim, [msg] ) 

A possibility assertion which is only valid if it is possible for claim to evaluate to true with honest frontends and participants. It accepts an optional bytes argument, which is included in any reported violation.

5.4.7.4.35 digest

digest( arg_0, ..., arg_n ) 

The digest primitive performs a cryptographic hash of the binary encoding of the given arguments. This returns a Digest value. The exact algorithm used depends on the connector.

5.4.7.4.36 balance

balance();
balance(gil); 

The balance primitive returns the balance of the contract account for the DApp. It takes an optional non-network token value, in which case it returns the balance of the given token.

5.4.7.4.37 lastConsensusTime

lastConsensusTime() 

The lastConsensusTime primitive returns the time of the last publication of the DApp. This may not be available if there was no such previous publication, such as at the beginning of an application where deployMode is 'firstMsg'.

Why is there no thisConsensusTime? Some networks do not support observing the time of a consensus operation until after it has finalized. This aides scalability, because it increases the number of times when an operation could be finalized.

5.4.7.4.38 makeDeadline

const [ timeRemaining, keepGoing ] = makeDeadline(10); 

makeDeadline(deadline) takes an UInt as an argument and returns a pair of functions that can be used for dealing with absolute deadlines. It internally determines the end time based off of the deadline and the last consensus time—at the time of calling makeDeadline. timeRemaining will calculate the difference between the end time and the current last consensus time. keepGoing determines whether the current last consensus time is less than the end time. It is typical to use the two fields for the while and timeout field of a parallelReduce expression. For example:

const [ timeRemaining, keepGoing ] = makeDeadline(10);
const _ = parallelReduce(...)
  .invariant(...)
  .while( keepGoing() )
  .case(...)
  .timeout( timeRemaining(), () => { ... }) 

This pattern is so common that it can be abbreviated as .timeRemaining.

5.4.7.4.39 implies

implies( x, y ) 

Returns true if x is false or y is true.

5.4.7.4.40 ensure

ensure( pred, x ) 

Makes a static assertion that pred(x) is true and returns x.

5.4.7.4.41 hasRandom

hasRandom 

A participant interact interface which specifies random as a function that takes no arguments and returns an unsigned integer of bit width bits. Reach provides a default frontend implementation via hasRandom (Frontend).

5.4.7.4.42 hasConsoleLogger

hasConsoleLogger 

A participant interact interface which specifies log with an unconstrained domain function type that returns Null. Reach provides a default frontend implementation via hasConsoleLogger (Frontend).

5.4.7.4.43 compose

compose(f, g) 

Creates a new function that applies it’s argument to g, then pipes the result to the function f. The argument type of f must be the return type of g.

5.4.7.4.44 sqrt

sqrt(81, 10) 

Calculates an approximate square root of the first argument. This method utilizes the Babylonian Method for computing the square root. The second argument must be an UInt whose value is known at compile time, which represents the number of iterations the algorithm should perform.

For reference, when performing 5 iterations, the algorithm can reliably calculate the square root up to 32 squared, or 1,024. When performing 10 iterations, the algorithm can reliably calculate the square root up to 580 squared, or 336,400.

5.4.7.4.45 pow

pow (2, 40, 10) // => 1,099,511,627,776 

pow(base, power, precision) Calculates the approximate value of raising base to power. The third argument must be an UInt whose value is known at compile time, which represents the number of iterations the algorithm should perform. For reference, 6 iterations provides enough accuracy to calculate up to 2^64 - 1, so the largest power it can compute is 63.

5.4.7.4.46 Signed Integers

The standard library provides abstractions for dealing with signed integers. The following definitions are used to represent Ints:

Int is represented as an object, as opposed to a scalar value, because some platforms that Reach targets do not provide native support for signed integers.

const Int = { sign: Bool, i: UInt };
const Pos = true;
const Neg = false;  

int(Bool, UInt) is shorthand for defining an Int record. You may also use the + and - unary operators to declare integers instead of UInts.

int(Pos, 4); // represents 4
int(Neg, 4); // represents -4
-4;          // represents -4
+4;          // represents 4 : Int
 4;          // represents 4 : UInt 

iadd(x, y) adds the Int x and the Int y.

isub(x, y) subtracts the Int y from the Int x.

imul(x, y) multiplies the Int x and the Int y.

idiv(x, y) divides the Int x by the Int y.

imod(x, y) finds the remainder of dividing the Int x by the Int y.

ilt(x, y) determines whether x is less than y.

ile(x, y) determines whether x is less than or equal to y.

igt(x, y) determines whether x is greather than y.

ige(x, y) determines whether x is greater than or equal to y.

ieq(x, y) determines whether x is equal to y.

ine(x, y) determines whether x is not equal to y.

imax(x, y) returns the larger of two Ints.

abs(i) returns the absolute value of an Int. The return value is of type UInt.

5.4.7.4.47 Fixed-Point Numbers

FixedPoint is defined by

export const FixedPoint = Object({ sign: bool, i: Object({ scale: UInt, i: UInt }) }); 

FixedPoint can be used to represent numbers with a fixed number of digits after the decimal point. They are handy for representing fractional values, especially in base 10. The value of a fixed point number is determined by dividing the underlying integer value, i, by its scale factor, scale. For example, we could represent the value 1.234 with { sign: Pos, i: { scale: 1000, i : 1234 } } or fx(1000)(Pos, 1234). Alternatively, Reach provides syntactic sugar for defining FixedPoint numbers. One can simply write 1.234, which will assume the value is in base 10. A scale factor of 1000 correlates to 3 decimal places of precision. Similarly, a scale factor of 100 would have 2 decimal places of precision.

const scale = 10;
const i = 56;
fx(scale)(Neg, i); // represents - 5.6 

fx(scale)(i) will return a function that can be used to instantiate fixed point numbers with a particular scale factor.

const i = 4;
fxint(-i); // represents - 4.0 

fxint(Int) will cast the Int arg as a FixedPoint number with a scale of 1.

const x = fx(1000)(Pos, 1234); // x = 1.234
fxrescale(x, 100);    // => 1.23 

fxrescale(x, scale) will convert a fixed point number from using one scale to another. This operation can result in loss of precision, as demonstrated in the above example.

const x = fx(1000)(Pos, 824345); // x = 824.345
const y = 45.67;
fxunify(x, y);    // => [ 1000, 824.345, 45.670 ] 

fxunify(x, y) will convert the fixed point numbers to use the same scale. The larger scale of the two arguments will be chosen. The function will return a 3-tuple consisting of the common scale and the newly scaled values.

fxadd(x, y) adds two fixed point numbers.

fxsub(x, y) subtracts two fixed point numbers.

fxmul(x, y) multiplies two fixed point numbers.

fxdiv(34.56, 1.234, 10)     // => 28
fxdiv(34.56, 1.234, 100000) // => 28.0064 

fxdiv(x, y, scale_factor) divides two fixed point numbers. The numerator, x, will be multiplied by the scale factor to provide a more precise answer. For example,

fxmod(x, y) finds the remainder of dividing x by y.

fxfloor(x) returns the greatest integer not greater than x.

fxsqrt(x, k) approximates the sqrt of the fixed number, x, using k iterations of the sqrt algorithm.

const base = 2.0;
const power = 0.33;
fxpow(base, power, 10, 1000); // 1.260
fxpow(base, power, 10, 10000); // 1.2599
fxpow(base, power, 10, 1000000); // 1.259921

fxpow(base, power, precision, scalePrecision) approximates the power of the fixed number, base, raised to the fixed point number, power. The third argument must be an UInt whose value is known at compile time, which represents the number of iterations the algorithm should perform. The scalePrecision argument must be a UInt and represents the scale of the return value. Choosing a larger scalePrecision allows for more precision when approximating the power, as demonstrated in the example below:

fxpowi(base, power, precision) approximates the power of the fixed number, base, raised to the Int, power. The third argument must be an UInt whose value is known at compile time, which represents the number of iterations the algorithm should perform. For reference, 6 iterations provides enough accuracy to calculate up to 2^64 - 1, so the largest power it can compute is 63.

fxpowui(5.8, 3, 10); // 195.112

fxpowui(base, power, precision) approximates the power of the fixed number, base, raised to the UInt, power. The third argument must be an UInt whose value is known at compile time.

fxcmp(op, x, y) applies the comparison operator to the two fixed point numbers after unifying their scales.

There are convenience methods defined for comparing fixed point numbers:

fxlt(x, y) tests whether x is less than y.

fxle(x, y) tests whether x is less than or equal to y.

fxgt(x, y) tests whether x is greater than y.

fxge(x, y) tests whether x is greater than or equal to y.

fxeq(x, y) tests whether x is equal to y.

fxne(x, y) tests whether x is not equal to y.

5.4.7.4.48 Anybody

Anybody.publish(); // race(...Participants).publish()

Reach provides a shorthand, Anybody, which serves as a race between all participants. This shorthand can be useful for situations where it does not matter who publishes, such as in a timeout.

Anybody is strictly an abbreviation of a race involving all of the named participants of the application. In an application with a participant class, this means any principal at all, because there is no restriction on which principals (i.e. addresses) may serve as a member of that class. In an application without any participant classes, Anybody instead would mean only the actual previously-bound participants.

5.4.7.4.49 Intervals

An Interval is defined by

where IntervalType is defined by

export const [ isIntervalType, Closed, Open ] = mkEnum(2);
export const IntervalType = Refine(UInt, isIntervalType);  

5.4.7.4.49.1 Constructors

An interval may be constructed with its tuple notation or by function:

// Representing [-10, +10)
const i1 = [Closed, -10, +10, Open];
const i2 = interval(Closed, -10, +10, Open);
const i3 = intervalCO(-10, +10); 

For convenience, Reach provides a number of functions for constructing intervals:

interval(IntervalType, Int, Int, IntervalType) constructs an interval where the first and second argument represent the left endpoint and whether it’s open or closed; the third and fourth argument represent the right endpoint and whether it’s open or closed.

intervalCC(l, r) constructs a closed interval from two endpoints of type Int.

intervalCO(l, r) constructs a half-open interval from two endpoints of type Int where the left endpoint is closed and the right endpoint is open.

intervalOC(l, r) constructs a half-open interval from two endpoints of type Int where the left endpoint is open and the right endpoint is closed.

intervalOO(l, r) constructs an open interval from two endpoints of type Int.

5.4.7.4.49.2 Accessors

leftEndpoint(i) will return the Int that represents the left endpoint of an interval.

rightEndpoint(i) will return the Int that represents the right endpoint of an interval.

5.4.7.4.49.3 Relational Operations

Intervals may be compared with the following functions:

intervalEq(l, r) tests whether the intervals are equal.

intervalNe(l, r) tests whether the intervals are not equal.

intervalLt(l, r) tests whether the left interval is less than the right interval.

intervalLte(l, r) tests whether the left interval is less than or equal to the right interval.

intervalGt(l, r) tests whether the left interval is greater than the right interval.

intervalGte(l, r) tests whether the left interval is greater than or equal to the right interval.

5.4.7.4.49.4 Arithmetic Operations

intervalAdd(l, r) adds the two intervals.

intervalSub(l, r) subtracts the two intervals.

intervalMul(l, r) multiplies the two intervals.

intervalDiv(l, r) divides the two intervals.

5.4.7.4.49.5 Other Operations

const i1 = intervalOO(+3, +11); // (+3, +11)
const i2 = intervalCC(+7, +9);  // [+7, +9]
intervalIntersection(i1, i2);   // [+7, +11)  

intervalIntersection(x, y) returns the intersection of two intervals.

const i1 = intervalOO(+3, +9);  // (+3, +9)
const i2 = intervalCC(+7, +11); // [+7, +11]
intervalUnion(i1, i2);          // (+3, +11]  

intervalUnion(x, y) returns the union of two intervals.

intervalWidth(intervalCC(+4, +45)); // +41 

intervalWidth(i) returns the width of an interval.

intervalAbs(intervalCC(+1, +10)); // +10 

intervalAbs(i) returns the absolute value of an interval.