Top

Mode Coercion

French

German

Italian

Spanish

Portuguese

Japanese

Korean

Chinese

Type Conversion

Legal Type Casts
Automatic Type Coercion
Polymorphic Predicates

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.

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 term₂ 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):
P(a', b')
integers n:
R(n), -2³¹ < = n < = 2³²-1
Long integers n:
R(n), -2³¹ <= n <= 2³¹-1
Real numbers n:
R(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):
R(n)
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:
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 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 type₂ 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 type₁ is wider than type₂ - that is, that all the elements of type₂ are contained in type₁ - 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 -2³¹ to 2³¹-1?
L	I	Integer from -2³¹ to 2³¹-1?

This section describes the characteristics of all the standard polymorphic predicates. In each section, several different predicate declaration heads are given, each of which corresponds to a particular behaviour of the predicate.

These declarations are really pseudo-code, only to indicate approximately how FormulaOne treats the predicates.

Note: You need FormulaOne compiler release 41C or later for _AllDifferent, _AllAscending, _AllDescending, _Ascending, _Descendig.

Print

Print acts as a procedure with any number of input parameters, of any types Tl to Tn:

proc Print(xl :< Tl, ..., xn :< Tn)

The type information is used by Print to determine how it should print the arguments - as strings, arrays, tuples, etc.

Len

Len acts as each of the following predicates and procedures, for any type T:

proc Len(a :< [0..n]->T, len :> I) 
pred Len(a::[0..n]->T, len :> I)
proc Len(a :< [0..]->T, len :> I) 
pred Len{a::[0..]->T, len :> I)
proc Len(s :< S, len :> I)
proc Len(l :< list T, len :> I)
pred Len(l :: list T, len :: I)

With arrays, Len returns the number of elements in the array (recall that flexible arrays ave a known number of elements at run time, and that while the elements of symbolic arrays may be unknown, the number of elements is always known). With strings, Len returns the length of the string. With lists, Len returns the number of elements in the list, not counting Nil. The symbolic list predicate form of Len behaves exactly as the following predicate, for every T:

pred Len(l :: list T, len :: I) iff
    len = 0 & l =  Nil |
    len > 0 &
    l = (_,t) & Lent(t, len-1)

Append

Append acts as each of the following procedures and predicates, for every T:

proc Append(s1 :< S, s2 :< S, s_out :> S)
proc Append(l1 :< list T, l2 :< list T, l_out :> list T)
pred Append(l1 :: list T, l2 :: list T, l__out :: list T)

Append returns the string or list consisting of the concatenation of the first two parameters in its call. The last version of Append behaves exactly as the following predicate, for every T:

pred Append (l1 :: list T, l2 :: list T, l_out :: list T) iff
    l1 = Nil & l_out = l2 | l1 = (h, t) &
    l_out = (h, l_aux)
    & Append(t, l2, l aux)

in

The in operator is not exactly a predicate, but it behaves in a polymorphic way which is similar to that of the polymorphic predicate. If we think of every formula of the form xl in x2 as being a call to a predicate In(xl, x2), then this predicate In acts as each of the following predicates, for every T:

proc In(x :< T,	l :< list T)
pred In(x :> T,	l :< list T)
pred In(x :: T,	l :: list T)
proc In(pat :< S, s :< S)

The first list predicate form has the effect of testing the membership of x in l. The second form assigns to x each of the members of l on backtracking. The third form behaves exactly as the following predicate, for every T:

pred In(x :: T, l :: list T) iff
    l = (h, t) & ( h = x | In(x, t))

The form with string-typed arguments is a pattern matching form, which matches the wild-card character "*" to any sequence of text (possibly empty), and any other characters to themselves. For instance, all the following formulas should be true: '*a*a' in 'lava' '*a*a' in 'ada' '*a*a' in 'llama' \ '*ula*' in 'FormulaOne' '*log*' in 'Prolog'

Dupl

Dupl acts as a procedure of the following form, for every type T:

proc Dupl(n :< I, x :< T, array :> [0..]->T )

It has the effect of putting into array, an array constructed of n copies of the value x.

_AllDifferent

_AllDifferent acts as a predicate with any number of logical parameters, for every type T:

pred _AllDifferent(x1::T, x2::T, x3::T, ..., xn::T)

The _AllDifferent predicate places n(n-1)/2 binary constraints on n variables, ensuring no two variables can have the same value.

pred _AllDifferent(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 <> x2 & x1 <> x3 & ... x1 <> xn &
               x2 <> x3 & ... x2 <> xn &
                              x3 <> xn

For example, the following query

    all x::[1..2] & y::[1..4] & z ::I[1..2] & _AllDifferent(x,y,z)

will generate the following solutions:

x = 2
y = 3
z = 1
___ Solution: 1 __________________________________

x = 2
y = 4
z = 1
___ Solution: 2 __________________________________

x = 1
y = 3
z = 2
___ Solution: 3 __________________________________

x = 1
y = 4
z = 2
___ Solution: 4 __________________________________
    
Number of solutions: 4   Number of backtracks: 0
Elapsed time: 00:00:00

_AllAscending

_AllAscending acts as a predicate with any number of logical parameters, for every type T which allows comparison constraints for "greater than". These types currently include I, L, R and S. The _AllAscending predicate places n-1 binary constraints on n variables, ensuring the variables have ascending values.

pred _AllAscending(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 < x2 & x1 < x3 & ... x1 < xn

For example, the following query

   all x::[1..2] & y::[1..4] & z ::I[1..4] & _AllAscending(x,y,z)

will generate the following solutions:

x = 1
y = 2
z = 3
___ Solution: 1 __________________________________

x = 1
y = 2
z = 4
___ Solution: 2 __________________________________

x = 1
y = 3
z = 4
___ Solution: 3 __________________________________

x = 2
y = 3
z = 4
___ Solution: 4 __________________________________

Number of solutions: 4   Number of backtracks: 0
Elapsed time: 00:00:00

_Ascending

_Ascending acts as a predicate with any number of logical parameters, for every type T which allows comparison constraints for "greater or equal than". These types currently include I, L, R and S. The _Ascending predicate places n-1 binary constraints on n variables, ensuring the variables have ascending values.

pred _Ascending(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 <= x2 & x1 <= x3 & ... x1 <= xn

For example, the following query

   all x::[1..2] & y::[1..4] & z ::I[1..2] & _Ascending(x,y,z)

will generate the following solutions:


x = 1
y = 1
z = 1
___ Solution: 1 __________________________________

x = 1
y = 1
z = 2
___ Solution: 2 __________________________________

x = 1
y = 2
z = 2
___ Solution: 3 __________________________________

x = 2
y = 2
z = 2
___ Solution: 4 __________________________________

Number of solutions: 4   Number of backtracks: 0
Elapsed time: 00:00:00

_AllDescending

_AllDescending acts as a predicate with any number of logical parameters, for every type T which allows comparison constraints for "greater than". These types currently include I, L, R and S. The _AllDescending predicate places n-1 binary constraints on n variables, ensuring the variables have ascending values.

pred _AllDescending(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 > x2 & x1 > x3 & ... x1 > xn

For example, the following query

all x::[1..3] & y::[1..3] & z ::I[1..3] & _AllDescending(x,y,z)

will generate the following solutions:

x = 3
y = 2
z = 1
___ Solution: 1 __________________________________

Number of solutions: 1   Number of backtracks: 0
Elapsed time: 00:00:00

_Descending

_Descending acts as a predicate with any number of logical parameters, for every type T which allows comparison constraints for "greater or equal than". These types currently include I, L, R and S. The _Descending predicate places n-1 binary constraints on n variables, ensuring the variables have ascending values.

pred _Descending(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 >= x2 & x1 >= x3 & ... x1 >= xn

For example, the following query

all x::[1..2] & y::[1..2] & z ::I[1..2] & _Descending(x,y,z)

will generate the following solutions:

x = 1
y = 1
z = 1
___ Solution: 1 __________________________________

x = 2
y = 1
z = 1
___ Solution: 2 __________________________________

x = 2
y = 2
z = 1
___ Solution: 3 __________________________________

x = 2
y = 2
z = 2
___ Solution: 4 __________________________________

Number of solutions: 4   Number of backtracks: 0
Elapsed time: 00:00:00

Top

BNF Syntax of FormulaOne

Mode Coercion