French German Italian Spanish Portuguese Japanese Korean Chinese

There are three basic situations in which a term of a certain type is expected in a FormulaOne program.

- When a variable is being assigned a value, either by an identity formula (=) or by an explicit assignment (:=), the type of the variable must be the same as the type of its value.
- In a term containing a binary operator (such as a + b) or an arithmetic relational operator (such as a < b) the types of the two operands must be the same.
- In a predicate call, the type of each argument must be the same as the type of the formal parameter in the same position in the predicate declaration.

If you wish to give a term of one type where a term of another type is expected, some type conversion must be done. This can be an explicit type cast of the form term:type, where type is the desired type. But in some cases, it can be an automatic type coercion, in which the term is converted to the desired type by the system without a type cast operation being needed.

Some system-defined predicates are polymorphic; that is, they act as procedures with different parameter types and modes in different situations. This section describes the legal type casts, the automatic coercions done by FormulaOne, and the characteristics of all the polymorphic predicates.

This means not just that the shape of the **term** is the same, but that the **term'** is a member of the subset
of **U** corresponding to type; for instance, the term R(3.14159)
is not a member of the type [2..4] because it does not stand for an integer in that range.

Terms are mapped into elements of the type U as follows, a' stands for the mapping of a into the universal type U, etc.

- Pairs
**(a, b)**:

**P(a', b')** - integers
**n**:

**R(n), -2**^{31}<= n <= 2^{32}-1 - Long integers
**n**:

**R(n), -2**^{31}<= n <= 2^{31}-1 - Real numbers
**n**:

**R(n)** - Tuples
**(a1, ..., an)**:

**P(a1', P( ..., P(an-1' an')...))** - Union terms
**A**, where**A**is the**n**alternative of the union (numbered from 0):^{^th}

**R(n)** - Union terms
**A(a1, ..., am)**, where**A**is the**n**alternative of the union (numbered from):^{^th}

**P(R(n), P(a1', P(..., P(am-l', am')...)))** - Arrays with
**n**elements,**[a1, ..., an]**and strings with**Len(string)= n**:

**P(R(n), P(a1', P(..., P(an', R(0))...)))** - Injections with
**n**elements,**[al, ..., an]**:

**P(R(n), P(a1', P(..., P(an', R(0))...)))**, where no two**ai'**are the same. - Terms
**n**of subrange type**[a.. b]**:

**R(n), where a <= n <= b** - The list element
**Nil**:

**R(0)** - Lists
**(h, t)**:

**P(h', t')** - Relations containing
**al, ..., an**:

**P(a', P(..., P(an-1', P(an', R(0)))...))** - Files containing records
**rl, ..., rn**, with file pointer after**ri**:

**P(P(r1', ..., P(ri-1', ri')...),**

**P(ri + 1', ...,P(rn-1', rn')...))**

The FormulaOne compiler disallows any cast of a relation term into any type; and the only file terms which can be cast into different types are the DOS file name constants, which can be cast into the types

Most of the cases in which this can happen have the property that **type _{1}** is wider than

A widening coercion (for instance, from **I** to **L** or from any type to **U**) always succeeds; but a narrowing coercion can sometimes fail. The cases in which a narrowing coercion will succeed are those in which the term passes the test shown in the third column of the Type coercion table.

As with type casts, if a type coercion fails, it causes the formula containing the coerced term to fail.

Wider Type | Narrower Type | Test |

U | T | Fits T? |

[0..]->T | [0..n]->T | Upper bound n? |

[0..n]->T | [0..n]->>T | All elements different? |

R | L | Unlimited Integer |

R | I | Integer form -2^{31} to 2^{31}-1? |

L | I | Integer from -2^{31} to 2^{31}-1? |

Top BNF Syntax of FormulaOne Mode Coercion