BNF Syntax of FormulaOne
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.
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.
- Pairs (a, b):
- integers n:
R(n), -231 <= n <= 232-1
- Long integers n:
R(n), -231 <= n <= 231-1
- Real numbers n:
- Tuples (a1, ..., an):
P(a1', P( ..., P(an-1' an')...))
- Union terms A, where A is the n^th alternative of the union (numbered from 0):
- Union terms A(a1, ..., am), where A is the n^th alternative of the union (numbered from):
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:
- Lists (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 Ascii, Bin or a database file type.
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.
||Upper bound n?
||All elements different?
||Integer form -231 to 231-1?
||Integer from -231 to 231-1?
BNF Syntax of FormulaOne