Top BNF Syntax of FormulaOne Mode Coercion
French French German German ItalianItalian SpanishSpanish PortuguesePortuguese JapaneseJapanese KoreanKorean ChineseChinese

Type Conversion

There are three basic situations in which a term of a certain type is expected in a FormulaOne program.
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.

Legal Type Casts

Every term has corresponding to it a term', which is the mapping of that term into the universal type, U. The type cast term term:type is defined whenever there is some term2 such that term' is the same as term2' - in which case the type cast term represents term2.

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.

When the type cast term is defined, it stands (computationally) for the given term, represented in the representation of the given type. When the type cast term is undefined, the formula containing it is false (computationally, it fails causing a backtrack).

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

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 Ascii, Bin or a database file type.

Automatic Type Coercions

In some cases, a term of some type can be given where a term of some other type2 is expected. In other words, term:type2 is assumed where just term is given.

Most of the cases in which this can happen have the property that type1 is wider than type2 - that is, that all the elements of type2 are contained in type1 - or vice versa. These cases are summarized in Type coercion table.

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.

One other class of coercion not shown in the table is done: between subrange terms and I, L, or other subrange terms. In this kind of coercion, the value is simply checked to see if it is in the proper range.

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

Type coercion table. T represents any type.
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 -231 to 231-1?
L I Integer from -231 to 231-1?

Top BNF Syntax of FormulaOne Mode Coercion