5.4.6.4 expression

This section describes the expressions that are available in any Reach scenario. A wide variety of expressions exist in the Reach program.

The rest of this section enumerates each expression.

5.4.6.4.1 Identifier Reference

XYZ

The identifier is written as an ID and is an expression used to calculate the value of the binding identifier.

The identifier this has special meaning in both the local step (that is, the body of the only or each expression) and the consensus step (that is, in a publish or pay statement, before a COMMIT statement). See this and this for details.

5.4.6.4.2 Function Application

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

The format of the function is: EXPR_rator(EXPR_rand_0,… ,EXPR_rand_n), where: EXPR_rator and EXPR_rand_0 to EXPR_rand_n are expressions used to calculate a value; EXPR_rator must evaluate n values of the same type, or parameters of n primitive types; Extended expressions (… Expr may appear in the list of operands to which the function applies, in which case the elements of expr are concatenated in place.

New f(a) is equivalent to f(a).new(), which is a very convenient abbreviation when writing class-oriented programs.

5.4.6.4.3 type

Types in Reach are represented by the following identifiers and constructors:

  • Null.
  • Bool represents a Boolean value.
  • UInt: represents an unsigned integer. Uint. Max is the maximum value that can be assigned to a UInt.
  • Bytes(length) : indicates a string with a maximum length of length Bytes.
  • Digest: indicates a Digest.
  • Address: indicates the Address of an account.
  • Token: indicates a non-network Token.
  • Fun([Domain_0,…, Domain_N], Range), representing a function type.
  • Tuple(Field_0, … , FieldN), representing a tuple (see tuples to Build tuples).
  • Object({key_0: Type_0, … , key_N: Type_N}), representing an object (see Objects to build objects).
  • Struct([[key_0, Type_0],…, [key_N, Type_N]]), represents a Struct(see Struct to build Struct).
  • Array(Type_0,size), representing a fixed-length Array. Type_0 must be a type that can exist at runtime (that is, not a function type) (see Arrays to build arrays).
  • Data({variant_0: Type_0, … , variant_N: Type_N}), indicating a tagged Union (or summary type) (see data to build data instances).
  • Refine(Type_0, Predicate, ? Message, where the Predicate represents the refined type, which is a unary function that returns a Boolean value, that is, instances of Type_0 satisfy the Predicate. It introduces an assert when an elaboration type appears in a passive position (such as in an IS statement, or in a Domain of Fun that acts as an interface to the participant). When it is in an active position (the Range in the function), it introduces a assume. Message is an optional string that is displayed when Predicate validation fails.

For example, if f has the following type: Fun([Refine(UInt, (x => x < 5))], Refine(UInt, (x => x > 10)))

So const z = f(y) is equivalent to: assert(y < 5); const z = f(y); assume(z > 10);

  • Refine(Type_0, PreCondition, PostCondition, ? Messages), where Type_0 is a function type; PreCondition is a unary function that receives the tuple of the field and returns a Boolean value. PostCondition is a binary function that takes a tuple of fields and ranges and returns a Boolean value; Represents a function type with preconditions and postconditions. Preconditions are ensured by assert and postconditions by assume. Message is an optional two-tuple byte. The first message is displayed when the pre-condition verification fails, and the second message is displayed when the post-condition verification fails.

For example, Refine(Fun([UInt, UInt], UInt),([x, y] => x < y),(([x, y], z) => x + y < z)) is a function that requires its second argument to be greater than the first argument and its result to be greater than the input.

Object and Data are commonly used for algebraic Data types in effect in Reach. typeOf(x) // typeisType(t) // Boolis(x, t) // Bool

The typeOf primitive function is the same as typeOf:, which returns the typeOf its argument.

An isType function returns true if its argument is a type. Any expression that satisfies isType is compiled away and does not exist at run time.

Is returns true if the first argument is the type of the second argument. This is called the passive position in Refine.

5.4.6.4.4 literal

100 xdeadbeef007 1034.5432 truefalsenull “reality bytes” ‘it just does’

The literal, written as VALUE, is an expression used to evaluate a given VALUE.

An empty literal can be written as NULL.

Numeric literals can be decimal, hexadecimal, or octal. If used as a UInt value at run time, numeric literals must follow the bit width of UInt; But if they only appear at compile time, they can be any positive number. Reach provides an abstraction for handling ints and signed FixedPoint numbers. Int can be defined by using the unary + and – operators on values of type UInt. Reach provides syntactic sugar for defining signed FixedPoint numbers, which are defined in decimal syntax in base 10.

Boolean literals can be written as true or false.

String literals (also called byte strings) can be written between double or single quotes (there is no difference between styles) and use the same escape rules as JavaScript.

5.4.6.4.5 Operational expressions

An operation is a special identifier that may be unary or binary.

-! A // non-a // minus + a // add typeof avoid A

Unary operations are written as UNAOP EXPR_rhs, where EXPR_rhs is an expression and UNAOP is one of several unary operations:! – + typeof void. All unary operations, except typeof, have corresponding named versions in the standard library.

Unary operations on values of the wrong type are invalid.

When applied to values of type UInt, the unary – and + operators cast their arguments to Int. The unary – and + operators are defined for values of Int and FixedPoint types.

Void in all arguments is equivalent to null.

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

Not all consensus networks support bit arithmetic, and bit arithmetic greatly reduces the efficiency of verification.

Binary expression writing EXPR_lhs BINOP EXPR_rhs, including EXPR_lhs and EXPR_rhs are expressions, BINOP is one of several binary operation: && | | | + – * / % & ^ < < > > = =! = = = =! == > >= <= <. The operators == (and ===) and! = (and! ==) can operate on all atomic values. Numeric operators, such as + and >, operate only on numbers. Because all numbers in Reach are integers, operators such as/intercept their results. Boolean operators, such as &&, operate only on Boolean values. Binary operations on values of the wrong type are invalid.

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 operations have named functions in the standard library. Although && and | | might not count them the second argument, but their corresponding naming functions and and or always calculation.

DigestEq (a, B) // digestEq(a, B) // digestEq(a, B) // digestEq(a, B) // digestEq(a, B) // digestEq(A, B) // digestEq(A, B) // digestEq(A, B) // digestEq(A, B) AddressEq (a, b) // Address equal FXeq (a, b) // FixedPoint equal IEq (a, b) // Int equal

== is a function that operates on all types. The two parameters must be of the same type. For each supported type, there are special functions for equality checking.

— If verifyArithmetic is true, the arithmetic operations automatically make a static assertion that their parameters will not overflow the bitwidths of the available consensus network. If false, the connector ensures this dynamically.

5.4.6.4.6 xor

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

Xor (Bool, Bool) returns true only if the two input values are different.

5.4.6.4.7 Parenthesized expressions

(a + b) – c

Expressions can be enclosed in parentheses, as in (EXPR).

5.4.6.4.8 tuples

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

A tuple, written literally [EXPR_0,…, EXPR_n], is an expression that evaluates a tuple with n values, where EXPR_0 through EXPR_n are expressions.

. Expr may appear inside a tuple expression, in which case the expanded expression must be evaluated as a tuple or an array, and the result is also concatenated to the corresponding expression position.

5.4.6.4.9 array

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

Converts a single type value tuple of a specific type to an array.

5.4.6.4.10 Element References

arr[3]

The reference is written REF_EXPR[IDX_EXPR], where REF_EXPR is an expression used to evaluate an array, a tuple, or a structure. IDX_EXPR is an expression used to compute a natural number that is smaller than the length of the array. References the element at the given index of the selection array. The subscripts start at zero.

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

5.4.6.4.11 Array and Tuple lengths: tupl. length, array. length, and.length

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

Tupl. length returns the length of the given Tuple.

Array.length Returns the length of the given Array.

Both can be shortened to expr. Length, where expr evaluates to a tuple or an array.

5.4.6.4.12 Updates to arrays and tuples: tupl. set, array. set, and.set

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

Tupl. set returns the same new Tuple as tUP, except that the index IDx is replaced by val.

Array.set returns a new Array identical to arr, except that the index IDx is replaced by val.

Both can be abbreviated to expr.set(IDx, val), where expr evaluates to a tuple or array.

5.4.6.4.13 Folding operation

The following methods can be used for any collapsible container, such as arrays and maps.

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

Foldable. ForEach (c, f) iterates over function f on the elements of container C and discards the result. This can be abbreviated to C. Fraser (f).

Foldable. All (c, F) array. all(C, f) map. all(C, f)c. will (f) Foldable.

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

Foldable. Any (C, f) determines if at least one element in container C meets requirement F.

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

Foldable. Or (c) returns the separation of the container as a Boolean value.

Foldable. &&. And Foldable. And (c)Array. And (c)Map. And (c) c.nd () Foldable.

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 contains element X.

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 container C that satisfy requirement f.

Size Foldable. Size Foldable. Size (c) array.size (c) map.size (c)c.size() Foldable.

Foldable.min &&.min Foldable. Min (c) array.min (c) map.min (c) c.Min () Foldable. Min (arr) returns the minimum value in the UInt container.

Foldable. Max &&. Max Foldable. Max (c) array.max (c) map.max (c)c.max() Foldable.

Foldable. Sum &&. Sum Foldable. Sum (c) array.sum (c) map.sum (c)c.sum() Foldable. Sum (c) return the sum in the UInt container.

Product (C)Array. Product (C)Map. Product (C)c.product() Foldable. Product (C Product in containers.

Average (c)c.average() Foldable. Average (c)c.average() Foldable. Average (c The average in the container.

5.4.6.4.14 Group operations on arrays

Arrays are collapsible containers. In addition to the folding method, the following methods can also be used for arrays.

Array.iota array.iota (5) array.iota (len) returns an Array of len length in which each element is equal to its index value. For example, array.iota (4) returns [0,1,2,3]. The given len must be evaluated as an integer at compile time.

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 be evaluated as an integer at compile time.

Concat (x, y)x.concat(y) array. concat(x, y) concatenates arrays X and Y. This can be abbreviated as x.concat of y.

Array.empty array_emptyarray. empty is an Array with no elements. It is the identity element of array. concat, which can also be written as Array_empty.

Array.zip&&.zip array.zip (x,y) x.zip(y) array.zip (x,y) returns a new Array with the same length as x and y (x and y must be the same length). The elements of this new Array are tuples of x and Y elements. This can be abbreviated as x.zip(y).

Array.map &&.map array.map (arr,f) arr.map(f) array.map (arr,f) Returns a new Array arr_mapped, which is of the same length as arr. Arr_mapped [I] = f (arr) [I]. Example: array.iota (4).map(x => x + 1) Returns [1, 2, 3, 4]. This can be abbreviated to arr.map(f).

By analogy, this function can be used for any number of arrays of the same size that are supplied before the f argument. For example, array.iota (4).map(array.iota (4), add) returns 0,2,4,6.

Reduce array. reduce(arr,z,f) arr.reduce(z, f) Array.reduce(arr,z,f) returns the left fold of the function f on the given Array, with an initial value of z. Iota (4).reduce(0,add) Returns (0+1)+2)+3=6. This can be abbreviated as arr. Reduce (z,f).

By analogy, this function can be used for any number of arrays of the same size that are supplied before the z argument. For example: Array. Iota (4). The reduce (Array. Iota (4), 0, (x, y, z) = > (z + x + y)) return ((((0 + 0 + 0) + 1 + 1) + 2 + 2) + 3 + 3).

Array.indexof &&.indexof array.indexof (arr,x) arr.indexof (x) array.indexof (arr,x) returns the indexOf the first element equal to x in a given Array. The return value is of type Maybe(UInt). If there are no eligible elements in the array, None is returned.

5.4.6.4.15 Mapping group operation

Map is a Foldable container. Maps can be aggregated using the following operations and Foldable operations within the constants of the while loop.

Reduce 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 on the given mapping, with the initial value z. For example, M. table (0, add) aggregates the elements of the map. This can be abbreviated to map.reduce(z, f).

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

5.4.6.4.16 object

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

A typical object format is {KEY_0: EXPR_0,… , KEY_n: EXPR_n}, where KEY_0 through KEY_n are identifiers or string literals; EXPR_0 through EXPR_n are expressions. Object is also an expression used to evaluate objects with fields KEY_0 through KEY_n.

For convenience, there are other object literal syntax, such as: {… obj, z: 5 }

Is an object concatenation that copies all fields from OBj into the object; You can then add additional fields in addition to these fields.

{ x, z: 5 }

Is short for {x: x, z: 5}, where x is any binding string.

5.4.6.4.17 structure

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

A structure is a combination of tuples and objects. It has named elements, similar to objects, but sorted like a tuple, so its elements can be accessed by name or location. There is a structure for connecting to non-REACH remote objects, where both parties must agree on what the value should look like at run time.

A struct instance can be constructed by calling the fromTuple method of a struct type instance (such as Posn), plus a tuple of appropriate length.

A struct instance can be constructed by calling the fromObject method of a struct type instance, such as Posn, along with an object with an appropriate field.

Structures can be converted to tuples or objects using toTuple and toObject methods on Struct values (and Struct type instances, such as Posn in the above example) : Assert (posn.totuple (p1)[0] == 1); assert(Struct.toObject(p2).y == 2);

5.4.6.4.16 Field Reference

obj.x

FIELD references are written as obj. FIELD, where OBJ is an expression that evaluates an object or structure, and FIELD is a valid identifier used to access the FIELD FIELD of an OBJ object.

5.4.6.4.19 Object. The set

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

Returns the same new object as obj, except that the field FLD has been replaced with val.

5.4.6.4.20 Object. SetIfUnset

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

Returns a new object identical to obj, but adds a field FLD with the value val if one does not exist in obj.

5.4.6.4.21 Object. From the

Object.has(obj, fld);

Returns a Boolean value indicating whether the object contains the field FLD. This is known statically.

5.4.6.4.22 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 as data.variant (VALUE), where DATA is the DATA type.VARIANT is the name of a variable of DATA, and VALUE is the VALUE matching the variable type. As a special case, when a variable is of type Null, the value can be omitted, as in the burger definition above.

Data instances are used for switch statements.

5.4.6.4.23 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);

The option type is represented in Reach by the built-in Data type Maybe, which has two variables: Some and None.

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

It is therefore a function that returns a Data type specific to a particular type in the Some variable.

Maybe instances can be easily used fromMaybe(mValue, onNone, onSome), where onNone is a no-argument function and onNone is called if mValue is None; OnSome is a function of the on argument. The value of onSome is called when mValue is Some. MValue is a data instance of Maybe.

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

IsNone is a convenient way to determine if a variable is isNone.

IsSome is a convenient way to determine if a variable is isSome.