Home Downloads Sample Code Screenshots Getting Started FAQ Support
This file documents the use of the Formula One compiler.
Copyright © 2003, 2004, 2005, 2006 K2 Software Corp.
This file documents the use of the FormulaOne compiler. The screenshots in this document are based on the FormulaOne Release 40 IDE (Integrated Development Environment).
Other releases may have different look and feel and a different method of invoking queries. This should be rather irrelevent, as this document focuses on the programming language itself.
Installation of the FormulaOne Compiler Release 40 also installs the Tutorial project with the module called Tutorial. It
contains most of the predicates discussed in this manual. You can use this module if you do not plan to type the
predicates yourself. The module must be compiled before it can be used. Once the module is compiled it can be used by various queries
without a recompilation, unless, of course, it has been modified.
FormulaOne a language which integrates procedural, declarative and database programming into one
highly efficient language.
Since the early 1980's micro-computers have won an important place in science, education, entertainment and industry.
Procedural programming,
which details how computing is performed, has lighten the drudgery of repetitive calculation for many people.
However, procedural programming
shows weakness when faced with problems concerning logic, reasoning or the evaluation of complex data relations.
One answer to this impasse is declarative programming, which lies at the very heart of AI (artificial intelligence).
Using this approach, the relation between information and objects is the matter of scrutiny and many of the programming
details can be left to the compiler.
With declarative programming, the inference engine organizes information and then finds a way to logically interpret or process that information,
when queried with respect to a given problem.
Expert systems place exceptional demands on such information processing, and great programming effort must be
expended to meet the challenge when using procedural languages such as C, Fortran or Pascal. On the other hand,
declarative languages such as Prolog and FormulaOne (which are very high-level languages) have the needed tools
built into their inferences engines.
At the start of the 1990's it is apparent that new development in computer languages has lagged behind hardware
development.
The transition to declarative programming may still be lengthy for the software industry.
Certainly for the individual, time is required to switch over to new languages and to learn the new styles,
philosophies and techniques they require. Complex and flexible applications will require both declarative and
procedural programming. Prolog is the widest known of declarative languages but it suffers from the flaw of
lacking procedural and program control features and must simulate them. FormulaOne has overcome this stumbling
block and has elegantly integrated both programming philosophies into one unit.
FormulaOne can be learned by a beginner but will be most appreciated by experienced programmers. If you are a problem solver, FormulaOne's truly unique implementation of constraints will be invaluable. Constraints enable numeric problems to be solved more rapidly, by orders of magnitude - in real time. And they work readily with FormulaOne's highly structured and modular nature to produce better code. "Better" code means more readable, more error-free and easier to maintain and change. This is another reason why FormulaOne is superior to any other declarative programming language.
and type 2 + 2 = 4 into the query window.
button.
6*9 = 42
all sec sec::L & sec = 60 * 60 * 24
all f f::L & f-32 = (20 * 9)/5
We can put FormulaOne's knowledge of arithmetic to good use in solving problems of arithmetic which humans can't solve easily. Consider the following puzzle.
Some spiders and some beetles are in a box. The box contains forty-six legs. How many spiders and how many beetles are in the box?Since we know that spiders have eight legs and beetles have six legs, we can make a first stab at the puzzle by posing the query:
all s, b s::L & b::L & 8*s + 6*b = 46We are using s and b to stand for the number of spiders and the number of beetles, respectively, so 8*s + 6*b must be equal to 46. It seems that it should work; but when we issue this as a query, the system pops up the following error message:
This corresponds to a very large number of solutions (more than 1G).
There are an infinite number of values for s and b because the way we declared them, they can have either positive or negative numbers as their values. So because there can't be a negative number of either spiders or beetles, and the problem indicates that there is at least one of each in the box, we can add a restriction:all s::L & b::L & s > 0 & b > 0 & 8*s + 6*b = 46And now we get the results we wanted, as shown
all x x::L & (x<4 | x>6) & x = 10We'll explain how other kinds of formulas are handled as we get to them.
x::L & (x<4 | x>6)& x = 10 & (Env: empty)
x::L & ( x<4 | x>6 ) & x = 10 & (Env: x::L)
x::L & ( x<4 | x>6 ) & x = 10 & (Env: x<4)
x::L & ( x<4 | x>6 ) & x =10 & (Env: x<4)
x::L & ( x<4 | x>6 ) & x = 10 & (Env: x=10)
all x x::L & x > 10 & x < 20the variable x does not have a single value by the end of the query, so the system enumerates all the possible values between the bounds that it knows. It should give each integer between 11 and 19 inclusive as possible solutions.
Print('ABC')
will just cause FormulaOne to print the line ABC in the results
window, followed by Success. The query
Print('A') & Print('BC')
would have exactly the same effect, since the Print formula does
not put any space between successive printed text. Other things besides quoted
strings can appear as arguments to Print (the things inside the parentheses).
Any term can be an argument, causing its value to be printed; and if the
special term '\n' is printed, it causes a carriage return.
Print('ABC\n') & Print((3 + 33) * (4 + 44))
would cause the output
Print('ABC','\n',(3 + 33) * (4 + 44))
would have exactly the same effect as the query above.
all x x::L & (x < 4 | x > 6) & Print('Here','\n') & x = 10
Then the output of the query will look like
8*s + 6*b = 46We took the variables to be the numbers of spiders and beetles in a box, but they could just as easily be the numbers of 8-inch and 6-inch pieces that could be cut from 46 inches of dowel. Say that we wanted to solve this kind of problem a lot, but sometimes with numbers other than 46 on the right-hand side. We could do this by defining the following predicate:
pred Puzzle_soln(x::L, y::L, z::L) iff
x > 0 & y > 0 & 8*x + 6*y = z
An English translation of this definition is the following:
The predicate Puzzle_soln is true of x, y, and z if and only if x>0, y >0, and 8*x + 6*y = z
Even better, we could say"x spiders and y beetles' is a solution to the spiders-and-beetles puzzle for z legs if and only if....".
all Puzzle_soln(s, b, 46)No variable declarations are necessary in this case, because FormulaOne can deduce that s and b are numbers from the definition of the predicate Puzzle_soln. Also note, that we are omitting a list of variables after the all, so that all variables will be printed. We should get the same answer as before. FormulaOne has computed this query by replacing it with the predicate body (the part following the iff), after substituting the variables s for x and b for y, and the number 46 for z. It has solved the resulting query, s > 0 & b > 0 & 8*s + 6*b = 46, just like a regular query.
pred Puzzle_soln(x::L, y::L, z::L) iff
{ There are 'x' spiders and 'y' beetles if there are 'z'legs }
x > 0 & y > 0 & 8*x + 6*y = z
A comment, in general, is any text enclosed by an open brace {, and close brace }. Comments can appear anywhere
in program text, and can appear on a single line or be split across any number of lines:{There are 'x' spiders and 'y' beetles if there are 'z'legs}
Comments can be nested, so that{Level 1 {Level 2 {} {} }
Level 1 again}
is a single comment. All the text within a comment is ignored; it is there to help us read and understand program text.
This is especially useful for indicating how a predicate is to be read.
pred Divis(x::L, y::L) iff
{'x' is divisible by 'y'}
z::L & z*y = x
An English translation of this definition is the following:all Divis(6,3)is successful (z is 2), and so is
all Divis(69,3)(z is 23), but
all Divis(25,6)fails because there is no z which, when multiplied by 6, will result in 25.
pred Even(x::L) iff
{'x' is even}
Divis(x ,2)
"The number x is even if and only if it is divisible by 2." When a call to Even appears in a query, it would
be expanded into the Divis call, and then that would be expanded into the body of Divis.pred GCD(x::L, y::L, n::L) iff
{ The greatest common divisor of 'x' and 'y' is 'n' Uses the Euclidean algorithm }
y = 0 & n = x
| x = 0 & n = y
| y > 0 & x >= y & GCD(x-y, y, n)
| x > 0 & x < y & GCD(x, y-x, n)
We'll see a more readable version of GCD when we get to if formulas. Let's see how this predicate would work on a query like this:
all GCD(6, 9, z)The predicate call would be expanded, replacing 6 for x, 9 for y, and z for n:
6=0 & z=9 | 9=0 & z=6 | 9>0 & 6>=9 & GCD(6-9, 9, z) | 6>0 & 6<9 & GCD(6, 9-6, z)The first three parts of this formula obviously fail, but 6 is indeed greater than 0 and less than 9, so the query is essentially reduced to GCD(6, 3, z). This call expands into
6=0 & z=3 3=0 & z=6 3>0 & 6>=3 & GCD(6-3,3,z) 6>0 & 6<3 & GCD(6, 3-6, z)which is reduced to GCD(3, 3, z), and from there, it is reduced to GCD(0, 3, z). This last call will be reduced to z = 3, and we will have the solution. (There will be some backtrack formulas, but all of them will fail; so this will be the only solution.) Here are some more examples of simple recursive arithmetic predicates. Later we will learn how to make these predicates a little more readable with the use of the if formula; but they work perfectly as listed.
pred Factorial(x::L, f::L) iff
{'x'-factorial is 'f}
x<2 & f=l
| x>=2 & Factorial(x-1, sub) & f=x*sub
{note that 'sub' will be declared implicitly, as sub::L}
pred Fib(index::L, number::L) iff
{'number' is the 'index'-th Fibonacci number}
index<=2 & number=l
| index>2 &
Fib(index-l, last) & Fib(index-2, prev) & number = last + prev
This last predicate could be made a lot more efficient. Each call makes two recursive calls, one for the previous
number and one for the number before that.
So a call like Fib(5, x) will generate one call for the fourth Fibonacci number, two calls for the third, three
calls for the second, and so on.
A better way to program Fib is for it to pass off most of the work to an auxiliary predicate which is recursive.
pred Fib1(index::L, number::L) iff
{'number' is the 'index'-th Fibonacci number} Fib_prev(index, prev, number)
pred Fib_prev(index::L, prev::L, number::L) iff
{'prev' and 'number' are two Fibonacci numbers
in sequence, with 'number' being the 'index'-th}
index<=2 & prev=l & number=l | index>2 &
Fib_prev(index-1, befprev, prev) & number = befprev + prev
x::L declares x to be a long integer x::I declares x to be an integer, having slightly different properties from the long ones x::R declares x to be a real number, that is, a number with a decimal part; and x::S declares x to be a string of characters.We'll cover some other type expressions that can come after the "::" in due course, and even symbols that can go in place of the "::". At this point we will concentrate mainly on these four basic types.
all s::I & b::I & s = 40 & b = 3*s + 9work with integers, because the value of s is known at the time the last formula is encountered.
all s::I & b::I & s>0 & b>0 & 8*s + 6*b = 46should give an exception, because FormulaOne cannot convert the last formula to the proper format for an I variable constraint.
8*s + 6*b = 46is in this format already, and will be accepted as a long integer constraint. So as we have seen, the example from the last section will work if we have L variables instead of I. This gives L variables much more power than integers, quite apart from their wider range. However, FormulaOne will still not be able to solve some problems that humans can solve.
all x::L & y::L & x > 0 & y > 0 & x * y = 46This query is very similar to the spiders-and-beetles query, but it has one important difference: two variables, whose values are not known, are being multiplied together. Now we know that the pairs of possible values for x and y are 1 and 46, 2 and 23, 23 and 2, or 46 and 1. But FormulaOne does not know how to solve queries involving the multiplication of two unknown L variables, because it cannot convert it into a constraint of the proper form. An error condition would therefore be raised. One solution to this problem would be to put an upper bound on the value of one of the variables, by (for instance) changing the query to
all x::L & y::L & x > 0 & y > 0 & y < 50 & x * y = 46Then, FormulaOne could solve the equation by testing all values of y between 0 and 50 (not inclusive).
all x::L & y::L & x > 0 & y > 0 & y < 24 & x * y = 46FormulaOne will only test for y from 1 to 23 (obviously 24 or greater will not divide evenly into 46).
[-]<digits>.<digits>where <digits> is a sequence of one or more digits. (Note that there must be at least one digit before and after the decimal point.) For example, 232.45, -9999.0, 0.8937432, and 3.14 are all real constants, and can be compared to variables of type R.
e<digits>or
e-<digits>indicating an exponent of 10 by which the constant will be multiplied. For instance, 2.17el0 represents the real number 21,700,000,000, and 314.15e-02 represents 3.1415.
'Maple Leaf' ' $22.34 US' ' 'That last one is the null string, string containing no characters. If you want a string to contain the single quote character itself, you must represent it within the string by two single quotes. The string constant
'The word ''word''.'contains only the characters in the following line:
The word 'word'.You might now recognize that the Print formula is just a predefined predicate that can take strings as arguments:
Print('wacka wacka')
Print('3.1415', 'nine')
Print('A B C ')
The term '\n', which you can print to cause Print to start a new line, is actually a string constant containing
the carriage-return/line-feed (CR/LF) sequence. There are several other predefined predicates that work with strings.
Len is a predicate with two arguments, the first of type S and the second of type I. A call to Len is true if
and only if the length of the string is equal to the integer.Len('Prolog', 6)
succeeds because the string 'Prolog' contains six characters; but the query
Len('four', 7)
fails. Of course, Len can be used to find the length of a given string. The query
all Len('$22.34 Cdn', length)
should give the single solution 'length = 10 '. The first argument to Len must have a value; x::S & Len(x, 5) will cause an error.Append('foo','bar',str) will result in str = 'foobar', while
Append('foo ','bar', str)
will result in str = 'foo bar'.all s = 'Vancouver' & s(3) = ch & ch = "c"should succeed and give the solution ch = 99 for the variable ch. Characters are in FormulaOne represented by their Ascii codes taken as integers. The Ascii code for the character c is 99. The same integer is denoted by the character constant "c".
pred Dotpadded(string::S, outstring::S) iff
{'string', padded to at least 10 characters, is 'outstring'}
Len(string, x) &
(x >= 10 & outstring = string |
x < 10 & Append(string, '.', newstring) & Dotpadded(newstring, outstring))
With these predicates declared, the following queries should all succeed:
all Dotpadded('Chapter 9', 'Chapter 9.')
all Dotpadded('Andrews', 'Andrews...')
all Dotpadded('Srivallipurandan', 'Srivallipurandan')
x and newstring, it should be noted, can be used without a declaration because FormulaOne can tell from the context that
they are supposed to be of type I and type S, respectively. When FormulaOne can do this, it declares the variables implicitly.
(22,3)
('Dixie',0)
(x,(929.29,last))
As you can see, any two terms, be they integer, real or string, constant or variables, can be paired. The last example above
even contains a pair as one element of a bigger pair. The comma operator, like an arithmetic operator, constructs a new term
from two other terms on either side of it. The difference is that (22,3) is not equal to any other simpler term, whereas (22+3)
is just another expression for 25. The type that every pair term belongs to is the type U, which we will encounter later. But
they can also be used as constants of many other important types. The parentheses are not really necessary in the above examples;
they are simply included for clarity. Pairing is right-associative, so the term
(x, 929.29, last)is equivalent to
(x, (929.29, last))and not to
((x, 929.29), last)
pred Determ(a::R, b::R, c::R, det::R) iff
det = ( (b*b) - (4*a*c) )
Then we could run the following query with no problems:
all det x::R & x=2 & Determ(x, 3, 4, det)even though the terms 2, 3, and 4 are integer constants, not real constants. Computationally, of course, FormulaOne has to convert the value of x from a 32-bit integer into a 64-bit real number, but it does so automatically because the value is logically a valid member of the type R.
all s::[1..10] & b::[1..10] & 8*s + 6*b = 46We could read this, in English, as "s and b are between 1 and 10, and 8*s + 6*y is equal to 46." It is equivalent to saying
all s::I & s>=0 & s<=10 & b::I & b>=0 & b<=10 & 8*s + 6*b = 46Expressions of the form
ftemp::[-32..212] delta:[-1..1] son:[1..7]These type expressions are called subranges, and will become particularly important when we talk about arrays. But even here, they have the effect of making the program code more compact and readable, which is always a benefit. Normally the variables declared as being of subrange types are represented as I variables, with the associated capabilities and constraints. If you want them to be represented as L variables, with their more powerful constraints, you can use the form
ftemp::L[-32..212]
(1, 1, 2, 3, 5, 8, Nil) Nil (32767, Nil)The set of all objects of type list I can be defined recursively as follows:
{Line 1} pred Sum(l::list L, sum::L) iff
{Line 2} {The sum of the list 'l' is 'sum'}
{Line 3} l = Nil &
{Line 4} sum = 0
{Line 5} | l = (head, tail) &
{Line 6} Sum(tail, tailsum) &
{Line 7} sum = head + tailsum
Sum is a recursive predicate (i.e. one which calls itself, that is, self-referential). If the list is Nil, the sum computed is
0; otherwise, the list is broken into a head and tail.head::L tail::list LFor example, if l = (3,44,Nil) then head = 3 and tail = (44,Nil). Another implicit definition of a symbolic variable occurs in line 6.:
Sum(tail,tailsum)tailsum is implicitly defined as a symbolic variable of type L, in agreement with the definition of the variable sum in line 1.
all x::I & z::list I & x = 2 & z = (3, 2, Nil) & x in zthe test x in z succeeds since 2 is a term of z. The similar query
all x::I & z::list I & z = (3, 2, Nil) & x in zshould give you two solutions, one with x = 3 and the other with x = 2.
One power of the variables we have worked with so far has been that they can be used and referred to without our knowing what their values are, or indeed whether they have values at all. But that power is sometimes not necessary, and in fact sometimes it gets in the way of writing efficient, readable programs.
You can specify, if you want, that a parameter or a local variable definitely has a value, or that it definitely does not have a value, when the predicate is entered. This is called the mode of the variable. The first kind of mode is called input mode, and is denoted by using the symbols " :< " instead of " :: " in the variable declaration; the second kind is called output mode, and is denoted by " :> ". The mode we have been using so far, denoted by " :: ", is called symbolic mode. Variables of this mode are often called logical variables in the terminology of Prolog.
Choosing variable mode specifications wisely can make your programs more readable. The compiler can also use this information to make compiled programs have the great efficiency of compiled Pascal or C programs, and to check for erroneous predicate calls which you have put into your program code by mistake.
The variables we have been working with so far are in symbolic mode. (The symbols " :: " between the variable name and the type are what indicate that.) With symbolic mode, the FormulaOne compiler can't tell, at the time the program is being compiled, whether the variable has a value or not. That fact is, however, known at run time. In the representation of the variable in memory, along with the space for its value is space for constraints that have been put on the variable. By the nature of these constraints, the running program can tell whether the variable has a full value.
If the constraints so far have determined a unique value for the variable, it acts just like a variable in other programming languages like Pascal or BASIC.
Formulas which compare the variable to other terms by relational operators (" = ", " < ", etc.) act just like tests. But if a unique value is not known, such formulas put new constraints on the variable, which may result in finding a unique value, or (if the new constraint is incompatible) causing a failure and a backtrack. FormulaOne has to check which of these conditions holds every time it encounters any relational operator formula.
l::list I & Sum(l,3)
would be ridiculous, since there are an infinite number of lists of integers whose elements sum to 3. It may well be, in fact, that for any purpose you are going to use Sum for, neither the first variable nor any part of it will ever be unknown. That is, you may want to use Sum exclusively to find the sum of a known list, or to confirm that some number is the sum of a known list.
If this is the case, you could specify that the first parameter always has a value by declaring it to be an input mode parameter.pred Sum1(l :< list I, s :: I) iff
{The sum of the integers in 'l' is 's'}
l = Nil & s = 0 |
l = (head, tail) & Sum1(tail, tailsurn) &
s = head + tailsum
The only thing that has changed here is that the first parameter is declared with the symbols
:< separating the variable name from the type. The only effect
this has is that the new Sum1 predicate can take only full-value terms in its first parameter; that is, terms built up from constant
terms or variables which have values at the time of the predicate call.
But this is a decrease in power from what we had with the old Sum predicate. Why should we ever want to do such a thing? There are three main reasons.
The first is that input variables are more efficient than symbolic variables (those declared with ::). Since FormulaOne knows that an input variable must have a fixed value, it doesn't need to store information about its value, such as constraints. It need only allocate enough memory for the value itself. And of course it doesn't need to take the time to check whether the variable has a value when it performs a comparison.The second reason is that it makes it clearer what the predicate is intended to do. If you explicitly state that, for instance, the
first Sum1 parameter always has a value, it makes it clear that it is to be used to find the sum of a given list. This makes your programs
more readable.
The third reason to use input mode declarations is that such declarations help the FormulaOne compiler help you to debug your programs.
A query such as
all z::list I & Sum(z, 3)would soon cause a "Too many backtracks" error with the old version of Sum, after having returned one solution. But in a larger program, a variable with no value which should have a value can often work its way through many predicate calls before it causes a problem. Most programmers would prefer to be able to detect such mistakes at chosen points, than to have them come up in difficult-to-detect ways later in a running program.
An input variable has the significant property that it cannot be reassigned, i.e. given a new value. It can be referred to, deconstructed if it is a list or some other composite term, used as a parameter, anything as long as it is not reassigned.
Thus the following is a test, not a reassignment of:pred Test_x (x :< I) iff
x = 3
The query Text_x(3) will succeed. Test_x(4) will fail but it will not modify x in the process.
This property makes for a sort of safety valve. In the case where you have nested predicates (that is, one predicate calls another
which may call more in turn) you can pass a value on to greater "depths" of nesting and know that the value cannot be accidently
corrupted. This value prevents many hard-to-find program bugs.
Just as there is a way of telling the compiler that a parameter has a value, there is a way of telling it that a parameter does not have a value, but will receive one by the end of the predicate call processing. This kind of parameter is called an output mode parameter, and is denoted by the symbols ":> ", output between the variable name and the type.
The second parameter in our Sum1 predicate is a good candidate. We can declare it to be an output-mode variable by using the following as the first line in the predicate declaration:pred Sum1(l :< list I, s :> I)This declaration tells the FormulaOne compiler to make sure that the parameter s receives a value in any call to Sum1. That information helps FormulaOne to compile calls to Sum1 more efficiently.
FormulaOne imposes two restrictions on output variables. The first use of an output variable must assign a full value to that variable; and the variable must be used at some time in any call to that predicate, no matter which set of conditions has caused the predicate body to be true.
For instance, if we omitted the last line from the definition of Sum1, the new definition would not even be accepted by the compiler:
pred Sum1(l :< list I, s :> I) iff
l = Nil & s = 0 | l = (head, tail) &
Sum1(tail, tailsum)
If s had been declared as symbolic mode, there would have been no problem with this definition. But as it stands, if l
is not Nil, s is never assigned a value. FormulaOne cannot guarantee that s has a value at the end of the
processing of any call to Sum1, so it refuses to accept the definition.
Here's another example of how input and output variables interact. It's just the Fibonacci number predicates from earlier in the book, modified by using integers and input and output annotations. Try to follow how data flows through the predicates as computation goes on.
pred Fib2(index :< I, number :> I) iff
{The 'index'-th Fibonacci number is 'number'}
Fib prevl(index, prev, number)
pred Fib_prevl(index :< I, prev :> I, fib :> I) iff
{'prev' and 'fib' are two Fibonacci numbers in sequence, where 'fib' is the 'index'-th}
index <= 2 & prev = 1 & fib = 1 | index > 2 &
Fib_prevl(index-1, befprev, prev) &
fib = befprev + prev
With output parameters, the answer is simple enough. While the usual thing to use as an argument to an output-mode parameter is another output variable, FormulaOne will accept symbolic or input variables, constants, or complex terms made up of a mixture of variables and constants. The way it handles the situation is to implicitly declare an invisible local output variable, use that in place of the original term, and then compare the result that comes back with the original term. For example, the query
all Sum1((3, 2, 1, Nil), 6)would be handled in the same way as would
all Sum1((3, 2, 1, Nil), aux) & aux = 6With input parameters, the situation is more complex. Normally FormulaOne allows only terms made up of constants, input variables, and output variables which have been assigned values to be used as input arguments. But it does not forbid the use of symbolic variables in input arguments, because sometimes, in the course of a program, symbolic variables do have definite values.
This means that symbolic variables are allowed, but a check is put into the compiled code to make sure that the variable has a value. If it does not, one of two things can happen. If the variable can take on a finite number of values, such as a variable of a subrange type, then the call is preceded by a formula enumerating all those possible values.
For instance, the queryall i::[0..3] & Fib2(i, x)would be handled in exactly the same way as the following query.
all i::[0..3] & (i=0 | i=l | i=2 | i=3) & Fib2(i, x)This clearly causes the query to backtrack to get all solutions, even though no explicit or-s, (|) were in it.
The other possibility is that the symbolic variable can take on an infinite or very large number of values, due to being of a type such as I or list S. In this case, FormulaOne sees that trying to "backtrack out" a value for the variable would cause it to keep backtracking indefinitely. This is the source of the familiar "Too many backtracks" help message on such errors. FormulaOne would like to be able to generate all the values for the variable, but cannot because the number of values is infinite.
There is one more mode of a variable, input/output (":."), which is explained separately since it can appear only in procedures and subroutines, special cases of predicates.if Formula
pred Fib_prev2(index :< I, prev :> I, fib :> I) iff
{'fib' is the 'index'-th Fibonacci number, and prev is the one before it}
if index <= 2 then
fib = 1 & prev = 1
else
Fib_prev2(index-1, befprev, prev) & fib = prev + befprev
end
The general form of an if formula is:
Formally, the if formula is true if both the A and the B are true, or if the A is false and the C is true. However, you can think about it in terms of instructions to the system in the following way:
If the condition holds, then evaluate the then formula; otherwise, evaluate the else formula. So using an if formula of the form given above is equivalent to using(A & B) | (~A & C)where ~A expresses the opposite condition to A (for instance, index > 2 and index <=2). There is a restriction on A, the condition formula, namely that all the terms that appear there must be full value.
A is meant to be a test, not a constraint. There is no such restriction on B or C however.
Thus the following is valid and will compile properly:
pred Rex (x :< L,z :: L) iff
if x < 3 then z < x else z > x+12 end
Normally the restriction on A is one you can live with. Often it helps to isolate your "if" in its own predicate, like pred Rex above,
or its own procedure and pass it all the parameters it needs to function correctly and collect any or all calculated values as output parameters.
However, if you must use symbolic variables in A, your condition formula, then you can - directly in your predicate - embed code of the form (( A & B ) | C ) where A, B and C are formulas. Recall that this is logically equivalent to "if A then B else C end".
As an example, look at the following pseudo-code:
x::L & y::L & z::L &
if x < y then
z >= 6
else
z < x+y+2
end
This test can be expressed in FormulaOne as
(( x < y & z >= 6) | z < x+y+2 )If and its close relative case are rather deterministically oriented structures. The procedural approach to them described in the next section is often more readable and efficient.
if
pred Fib3(index :< I, fib :> I) iff
{'fib' is the 'index'-th Fibonacci number}
if index < 1 then
Print('Warning: Fib index less than 1!')
end &
Fib_prev2(index, prev, fib)
If you tried to program this kind of thing without an if formula, you would get something like this:
pred Fib4(index :< I, fib :> I) iff
( index < 1 & Print('Warning: Fib index less than 1!') | index >= 1 ) &
Fib_prev2(index, prev, fib)
Clearly, the version with the if is more understandable. You may often have several if formulas strung together by the else clauses like this:
if A then
B
else
if C then
D
else
if E then
F
....
end
end
end
In this case, you can use the elsif construct to make the conditions a little more readable:
if A then
B
elsif C then
D
elsif E then
F
end
Note that only one end keyword is necessary at the end of the sequence. This makes more sense in cases where the conditions are really
equal possibilities, rather than some being subordinate to others. Consider this version of the greatest-common-divisor predicate, GCD1.
pred GCD1(x :< L, y :< L, n :> L) iff
{the greatest common divisor of 'x' and 'y' is 'n'}
if y = 0 then
n = x
elsif x = 0 then
n = y
elsif x < y then
GCD1(x, y-x, n)
else
GCD1(x-y, y, n)
end
Here's another example of an elsif predicate. We'll see a better version of this below, in the section on case formulas.
pred Digit_name(x :< [0..3], name :> S) iff
{the English name of 'x' is 'name'}
if x = 0 then
name = 'zero'
elsif x = 1 then
name = 'one'
elsif x = 2 then
name = 'two'
else
name = 'three'
end
pred Sum2(l :< list I, s :> I) iff
{the sum of the members of '!' is 's'}
case l of
Nil => s = 0;
(head, tail) => Sum2(tail, tailsum) & s = head + tailsum
end
The terms to the left of the arrows (=>) in the case formula are the various different forms l can take; and the formulas to
the right of them are the conditions which must hold true, in each of those cases, for the predicate to be true. The general
format of the case formula is:
This means, among other things, that only certain types of variables can be subject terms. (Subject terms are usually going to be variables, because if the structure of the term were explicit, you would not need to know what structure it had!). Only variables of list types, subrange types, and union types (which we'll discuss later) can be subject terms; all others, such as those of type I, cannot.
For example, say you wanted to write a predicate to give the English names of the digits, like the example in the last section. The following definition would work:
pred Digit_name1(digit :< [0..9], name :> S) iff
{'digit' has the English name 'name'}
case digit of
0 => name = 'zero';
1 => name = 'one';
2 => name = 'two';
3 => name = 'three';
4 => name = 'four';
5 => name = 'five';
6 => name = 'six';
7 => name = 'seven';
8 => name = 'eight';
9 => name = 'nine'
end
However, if we had declared digit to be of type I, it would not have been acceptable, since the given case statement would not have
covered all possible values of the variable.
FormulaOne allows two kinds of variants to the case statement which streamline them in many instances. After a list of cases, which may not cover all possible forms, there can be a final clause, just before the end, of the form else formula.
This works in the same way as the else part of a long if ... .... elsif statement. It catches all other cases not covered by the previous case terms. So if we wanted to consider all digits over 3 to be 'many', we could modify our Digit_name predicate as follows:
pred Digit_name2(digit :< [0..9], name :> S) iff
case digit of
0 => name = 'zero';
1 => name = 'one';
2 => name = 'two';
3 => name = 'three'
else
name = 'many'
end
The other streamlining variant FormulaOne allows is to group more than one case term before the arrow when all their case conclusion
formulas are the same. The case terms are separated by or "|" symbols.
pred Digit_name3(digit :< [0..9], name :> S) iff
case digit of
0 => name = 'zero';
1 => name = 'one';
2 => name = 'two';
3 => name = 'three';
4 | 5 | 6 => name = 'several'
else
name = 'many'
end
These predicates are called procedures because they are so much like the procedures of Pascal and C programming languages. Certain kinds of procedures can also be called functions. FormulaOne also facilitates subroutines, procedures that can access system information and variables.
| Class | Backtracking | I/O variables | External Data | Call pred | Call proc | Call subr |
| pred | yes | no | no | yes | yes | no |
| proc | no | yes | no | yes(*) | yes | no |
| subr | yes | yes | yes(*) | yes | yes | yes |
In addition, subroutines can access data external to the FormulaOne system such as user input and system date and time information. Any class of predicate can call a procedure but only a subroutine can call other subroutine (because external data are being passed implicitly from one subroutine to another). Also the procedures and subroutines cannot call predicates except in context of all/one/min/max formulas, though any predicate can call another predicate.
With that knowledge, FormulaOne can compile it into an efficient form that never keeps or refers to this backtrack data. You declare a procedure exactly the way you declare a true predicate, except that you use the keyword proc where you would normally use pred.
proc Sum3(l:<list I, sum:>I) iff
{the sum of the members of '!' is 's'}
case l of
Nil => sum = 0;
(head, tail) => Sum3(tail, tailsum) & sum = head + tailsum;
end
proc Powers(first :< I, last :< I) iff
{ prints square and cube of integers from 'first' to 'last' }
square = first*first &
Print(first,' ', square,' ', first*square, '\n') &
if first < last then
Powers(first+1, last)
end
So a procedure is like a predicate which is entered, does its job, and exits, after which it can be completely forgotten about.
Although a procedure can't call a predicate directly, a predicate can call a procedure, because it's effectively just a special kind of predicate.
A procedure can fail, just like a regular predicate. A procedure like the following could be expected to fail if the first argument were not an even number.
proc Half(x :< I, y :> I) iff
{'y' is half of 'x'}
x mod 2 = 0 & y = x / 2
Procedure can use if and case formulas. In fact, these two types of formulas were defined partly with procedures
in mind. Since the possible outcomes in if's and case's do not overlap, no backtrack is ever needed for them, even in true
predicates. Also, because they cannot backtrack, procedure calls with output variables can be themselves used in the conditions of if formulas:
... &
Sum3(ilistl, s1) &
if Sum3(ilist2) = s1 then
Print('Sums the same\n')
end &
....
The if condition can be written even in the following form:
. &
Sum3(ilistl, si) &
if Sum3(ilist2,s1) then
Print('Sums the same\n')
end &
....
where Sum3(ilist2,s1) is actually test of the outcome of procedure Sum3 with input parameter ilistl, and previously obtained value s1.
In FormulaOne it is possible to use or-s, ("|") in the subroutine context of a query or in the bodies of procedures and subroutines. Or-s behave similarly as the boolean or in Pascal or C. For instance:
proc Test(x :< I) iff
x = 1 | x = 5
The procedure call Test(x) tests whether the argument x is 1 or 5.
The or-s within procedures and subroutines are efficiently compiled by the tests and jumps just as in Pascal or C. This is possible because there is no backtracking in the procedure/subroutine context. In contrast to this, or-s within predicates permit backtracking, and require a more complicated implementation mechanism called choice points.
FormulaOne performs an extensive data analysis to make sure that procedures do not backtrack. If a non-local output or input/output variable is to be modified within an or in a procedure context, the logic of FormulaOne calls for the use of backtracking. Consequently the compiler of FormulaOne prohibits non-local assignments within or-s. For instance the following procedure is not accepted:proc Gen(x :> I) iff
x = 1 | x = 2
This is because the procedure Gen generates a value for its output argument x from within the or. The query Gen(2)
should logically succeed but since it is compiled as Gen(z) & z = 2, and the value returned from the call is z = 1, the
test z = 2 fails. It is impossible to generate the correct value 2 without backtracking. Similarly, input/output variables
non-local to an or can only be referred to (i.e. can be tested). Assignments to such variables are not permitted.proc P1(x :< I) iff
y:=1 & (y := y + l & x = 2 | y = 1) & T(y,x)
In the call P1(1) the first branch of or fails the test x = 2 and the second one should succeed.
If your problem calls for non-local assignments to the output or input/output variables you will have to use predicates.
Assignments to local output and input/output variables within the procedures are permitted. For instance the procedure:
proc P2(x :< I) iff
y = 1 & T(x,y) | z := 5 & Q(x,z)
is a legal one because the effect of the assignment of 1 to the output variable y is localized to the left argument of the or.
Similarly, the input/output variable z can be modified within the scope of the right argument of the or. See the section Scope of Variables.
For instance, imagine a subroutine Dates(date string) defined with the following declaration:
subr Dates(date_string :> S) iff ...A query to this subroutine would look like this:
Dates(date)(Note the absence of the all keyword in this query, which we'll explain later.) The result of the query would be date = '06/11/2001', or whatever the current date was.
The restrictions on the bodies of subroutines are exactly the same as those on the bodies of procedures. But there is an important restriction on the use of subroutines: they can be called only from other subroutines, or from queries.
This restriction has to do with how we explain logically what is going on in subroutines. Subroutines have to access data which come from outside the parameters they have been given. This means that two calls of a subroutine, with exactly the same parameters, could give two different results at different times.FormulaOne explains this logical anomaly by considering there to be an "imaginary first parameter" to every subroutine. The imaginary parameter contains all the external data that will ever be requested by the subroutine, including user input. (This is just an abstract concept, and has nothing to do with how subroutines are actually computed. Clearly the value of the imaginary parameter is impossible to predict at the time the subroutine is called.)
The value of the parameter is "known" to the top-level query processor and is "passed down" from subroutine to subroutine as an input/output variable, being modified as various subroutines take what they need from it. So the distinction between procedure and subroutine is necessary in order to explain logically such things as user input. But it's also very useful to programmers, because it makes a clear distinction between predicates whose behavior cannot be predicted due to different user inputs, and those whose behavior is predictable only from their parameters.
proc Sum4(l :< list I, s :> I) iff
iosum :. I &
iosum := 0 &
Sum_io(l, iosum) &
s = iosum
proc Sum_io(l :< list I, sofar :. I) iff
case l of
Nil => true;
(head, tail) => sofar := sofar + head & Sum_io(tail, sofar);
end
Notice the new symbol in these procedures, ":= ". This can be read as "is assigned"; for instance, "sofar is assigned the
value of the expression sofar + head". It means that whatever value the variable to the left of the := was, it now will
take on the value of the expression to the right of it.
We can think of the sofar parameter in the above program as being like a pair of parameters, one input and one output, with an intermediate variable local to the procedure to hold the new value. Similarly, we can think of the iosum local variable as being an initial variable and another variable to hold its final value. If we rewrite the program in this way, it would look like this:
proc Sum5(l :< list I, s :> I) iff
iosum_first :> I &
iosum_last :> I &
iosum_first = 0 &
Sum_io1(l, iosum_first, iosum_last) &
s = iosum_last
proc Sum_io1(l :< list I, sofar_first :< I, sofar_last :> I) iff
case l of
Nil => sofar_last = sofar_first;
(head, tail) => sofar_med :> I &
sofarjmed = sofar_first + head & Sum_io1(tail, sofarjmed, sofar_last);
end
Of course, the reason we wrote it with input/output, i/o variables in the first place was that all these different
variables were collapsed into one. No new storage is ever allocated for the new versions of iosum or sofar; they all
use the same area of memory for their value.
Old values of i/o variables are overwritten with new ones, so no backtracking can be done on them because their old value has been lost. In procedures and subroutines, no backtracking is ever done, so there is no problem. In FormulaOne, it is possible to use input/output variables in the predicates. For instance:
pred P3(x :. I) iff
x := x + 1 | x := x + 2
The query
all x := 2 & P3(x)will give two answers x = 3 and x = 4. Note that the assignment x := x + 1 is automatically undone when backtracking occurs, and the original value x = 2 is restored. The i/o variables are used with great advantage in many situations within a predicate context. See the modules maze and containers for the examples of i/o arrays to record the state of traversal through a graph. The module schuses i/o variables in a predicate context in order to satisfy a constraint which is not expressible by the standard constraints.
When backtracking occurs the previous values of i/o variables are automatically restored. This is done by remembering (trailing) the value of an i/o variable just before an assignment changes its value.
Procedures cannot backtrack and they are compiled without saving the previous values of i/o variables. This increases the efficiency of generated code. For this reason the procedures with i/o arguments cannot be called from within the predicate (backtracking) context.
proc Incr(x:.I) iff
x := x + 1
the query
all x := 6 & (Incr(x) & x = 7 | x = 6)is not permitted because the procedure Incr destroys the old value of the variable x. In this particular case, it would be quite simple to remember the value of x just before the procedure Incr was called. In general, saving the current value could be expensive if, for instance the i/o variable passed to a procedure were an array. The procedure could change only one element of the array but the compiler cannot know this and would have to generate the code saving the whole array.
For the same reason it is impossible to use i/o files in the predicate context. File operations make changes to the files which cannot be undone upon backtracking.
Local i/o variables must be initialized on their first use, just like local output variables. This is because FormulaOne would rather enforce such a standard than to be unable to know whether an i/o variable had a true value or just the random value found in the memory allocated for it.I/O variables are especially useful as error condition and return code parameters, which are usually set to something other than a standard value only in special circumstances:
{ loop on the subroutine Get_process_command, until a fatal error
occurs or user requests termination}
subr Main_command_loop() iff
e:.I & e := 0 &
Get_process_command(e) &
if e > 1 then {error condition; fail}
Print('Fatal error\n') & false
elsif e = 1 then {normal termination}
Print('End of command loop\n')
else
Main_command_loop()
end
subr Get_process_command(e :. I) iff
Print('Enter q to quit, a to abort ') &
Print('or anything else to continue') &
TTYKeyGet(x) &
if x = "q" then
e := 1
elsif x = "a" then
e := 2
else
Print('...processing')
end &
Print('\n')
I/O variables provide for the in-place modification of values. Each i/o variable is from a logical point of view a pair of variables: one
input variable holding the old value and the output variable holding the new modified value. The implementation, of course, is st as in Pascal or C.
Since FormulaOne is a programming language firmly based on logic, there are certain restrictions on the use of the i/o variables which make the variables different from the Pascal or C variables. Consider, for instance, the following predicate declarations:
proc P7(x:.[0..3]->[0..3]->I) iff .... proc P8(x:.[0..3]->I) iff .....The procedure P7 takes an i/o matrix of integers and the procedure P8 takes an i/o vector of integers. The predicates are used in the following contexts:
proc P9(x:.[0..3]->[0..3]->I) iff x = [_,r2,_] & P7(x) & P8(r2) proc P10(x:.[0..3]->[0..3]->I) iff P7(x) & P8(x(l))The predicate P9 deconstructs the array x in a Prolog-like fashion, whereas the predicate uses Pascal-like indexing. The compiler of FormulaOne must assume that the procedure P7 will modify the array x. In order to preserve the logical reading of P9, the compiler must deconstruct the array x in its body by copying the second row of x to the implicitly declared i/o variable r2. This is necessary to preserve the value unchanged across the call to P7. Consequently, any changes in P8 to the row r2 cannot affect the value of the matrix x. On the other hand, by passing to the predicate P8 in the body of P10, the second row of x selected by the indexing x(l), we achieve the same effect as in Pascal. Only a pointer is passed; the changes to the row are done directly in the matrix x.
When you want to use (and modify) a component of an i/o structure, you should use Pascal-like deconstructors of indexing or field selection. In this way, you make sure that pointers to components of data structures are passed. Because of the considerations dictated by logic, the Prolog-like deconstruction of i/o variables always results in the copying of components.
If the Pascal-like selection from fixed-size i/o variables is used, the compiler of FormulaOne can generate efficient code. Fixed-size data structures are, for instance, fixed-size arrays of integers (or of other fixed-size arrays). See Heap Management for the definition of the term fixed-size.A word of caution is needed here. FormulaOne is a logic programming with an integrated procedural part which is reminiscent of Pascal. It would be easy to implement input/output variables in the same manner as Pascal or C. Unfortunately, this is unacceptable because things could happen to variables in the course of program execution which then violate the basic concepts of logic. These same side-effects or unintended effects are also the ones that give rise to bugs and plague programs. Certainly it is possible to have bugs in a FormulaOne program, but in general if your program will compile at all then you have few bugs left to find and they are much easier to ferret out than in older languages.
By sticking to logic we get better programs. There may be some loss of efficiency but usually FormulaOne makes up for that elsewhere. Also, any program that works is better than one that doesn't.The all keyword makes the formula into a simplified form of the all formula and thus makes it able to contain backtracking formulas. So the exact guidelines for deciding whether to put an all in front of your queries are:
A function is declared as a procedure. But for a given procedure to be a function, the last parameter must be of output mode, and all the others must be of input mode. So, for instance, the SumS procedure is a function, and so is the following version of the Fib predicate:
proc Fib5(index :< I, number :> I) iff
{The 'index'-th Fibonacci number is 'number'}
Fib_prev3(index, prev, number)
proc Fib_prev3(index :< I, prev :> I, fib :>I) iff
{'fib' is the 'index'-th Fibonacci number, and prev is the one before it}
if index <= 2 then
fib = 1 & prev = 1
else
Fib_prev3(index-1, befprev, prev) & fib = prev + befprev
end
Note that the Fib_prev3 predicate is not a function because it has two output arguments.
So if functions are just procedures, why do we care about them? Because we can refer to them in a much more compact and easy-to-read format. We can define the following predicate:
pred Largesum(ilist :< list I) iff
{the sum of 'ilist' is greater than 10}
Sum5(ilist)>10
The expression Sum5(l) is here used as a term. This is functional notation: we are calling Sum5 with all its parameters except
the last one, and the value of the term is what the value of the last parameter would have been if it had been included. So the above
predicate definition is completely equivalent to the following:
pred Largesum1(ilist :< list I) iff
{the sum of 'ilist' is greater than 10}
Sum5(ilist, sum) & sum > 10
Functional notation is useful because we can make our programs more readable and compact with it (this is something that we consider
natural in languages like Pascal and C, but it's disallowed in Prologs). For instance, the final version of the procedure Sum can be
naturally coded as follows:
proc Sum6(l :< list I, sum :> I) iff
{the sum of the members of 'l' is 's'}
case l of
Nil => sum = 0;
(head, tail) => sum = head + Sum6(tail);
end
We usually write functions with the idea of using them as functions, and name them so that function calls read nicely. In the above
example, we can read the first definition of Largesum as "a list has a large sum if the sum of the list is greater than 10."
The second definition's reading is more complex, and slightly obscures its real meaning.
A function call can appear anywhere any other term can, including inside other function calls. The type of the function call term is the type of the last parameter which it stands for. So with Fib5 declared as a procedure, we can issue the following query:
x = Fib5(Fib5(Sum6((2,4,Nil))))The sum of the list is 6, the sixth Fibonacci number is 8, and the eighth Fibonacci number is 21; so we would expect the query to give us the answer x = 21.
Posint_t =[1..] Digit_t = [0..9] Stringlist_t = list S Weight_t = INotice that the names of the types are capitalized, like the names of predicates. As with predicates, this is because they each refer to a definite, static object, the kind of thing we would give a capitalized name to in English.
In this manual, we use the convention that type names end with the characters _t, to distinguish them from other names; but this is not required.
The first three declarations name the subranges of integers which correspond to the positive integers, the ten digits, and the lists of strings. After these declarations have been made, we can use the new names in place of the old. For example, declaring a variable to be of type Posint_t would have exactly the same effect as declaring it to be of type [1..].The last declaration may seem a little strange; why should we want to declare the type name Weight_t to be something for which we already have a shorter name, I? We may be doing this because we are not sure what kind of variables we want to be weights (integers, long integers, reals, etc.), and we want to get on with writing the rest of the program without deciding it yet. This way, if we change our mind about what a weight is, we'll only have to change one declaration in the whole program.
Date_t = (year:I,month:[1..12],day:[1..31])The expression on the right hand side of the equality formula, looks like a pair term with three parts, but it has things that look like variable declarations in the place of the three terms. This expression is called a tuple, and will act as a template for terms of type Date_t.
If a variable is declared to be of type Date_t, the only terms that can be assigned to it of the form (a, b, c), where a is an integer, b is from 1 to 12, and c is from 1 to 31. The parentheses around the term can be omitted when there is no possibility of confusion.
pred ... iff
birthday :> Date_t &
yr :> I &
... &
yr = 1961 &
birthday = yr, 7, (41-39) &
...
The general form of a named tuple type expression is
Date_t = (year:I,month:[1..12],day:[1..31]) Person_t = (name:S,age:I,birthdate:Date_t)Each type expression represents some subset of the universal type, U. The declared type Date_t represents all the terms which have the form of values for variables of type Date_t, just as the type list I represents all the pair terms which are Nil-terminated lists of integers.
However, the representation of tuple type values within the program's memory is a different story. While list terms are represented as separate elements connected by pointers into a linked list, the values representing tuple fields are stored in contiguous memory locations.
So in many respects, such terms are implemented like the records of Pascal and the structures of C. They also have the efficiency that goes along with them.birthday:>Date_tthe year field of the birthday variable can be referred to by the term birthday.year, and similarly for birthday.month and birthday.day. Such terms are called field selection terms. We can continue the example of the last section as follows:
... & birthday2:>Date_t & birthday2 = (birthday.year - 1, birthday.month, 1) & ... &Note that an output variable of a tuple type must be initialized all at once, not field-by-field. Before the whole variable is initialized, its individual fields cannot be referred to.
Another way you can refer to fields of a tuple variable is to use a deconstructor term. This is a term of the same "shape" as the tuple variable, but with variables in places corresponding to fields you want to match.
... & birthday2 = (yr2, mo2, dy2) & Print(mo2, dy2) & ... &After the equality formula, the variable yr2 will act exactly as the term birthdayl.year, and similarly for mo2 and dy2. This means not only that these variables have the same value, but that they refer to the same location in computer memory. Deconstructors are handled by the FormulaOne compiler in such a way that no extra memory is allocated for them.
Here are two versions of a predicate which succeeds if and only if its first parameter is a date which is before its second parameter. The first uses field selection terms and or ( | ), while the second uses deconstructors and if; you can decide for yourself which you prefer.
pred Before(datel :< Date_t, date2 :< Date_t) iff
{'datel' is before 'date2'}
datel.year < date2.year |
(datel.year = date2.year &
(datel.month < date2.month |
(datel.month = date2.month & datel.day < date2.day)))
proc Before1(datel :< Date_t, date2 :< Date_t) iff
{'datel' is before 'date2'}
datel = (yl, ml, dl) &
date2 = (y2, m2, d2) &
if yl > y2 then
false
elsif yl = y2 then
if ml > m2 then
false
elsif ml = m2 then
dl < d2
end
end
The following queries should succeed with either version of this predicate:
all Before((1987, 8, 8), (2001, 1, 1))
Before1((1961, 7, 2), (1961, 10, 29))Field-selection operators can be chained together to go as deep as you want into a tuple's structure. The following example makes use of the Person_t type, which we used to illustrate nested tuples above.
proc Same_birthday(p1 :< Person_t, p2 :< Person_t) iff
p1.birthdate.month = p2.birthdate.month &
p1.birthdate.day = p2.birthdate.day
Gender_t = Male | Female Colour_t = Red | Yellow | Green | BlueThese declarations mean that variables of type Gender_t can have only Male and male as values, and that those of type Colour_t can have only Red, Yellow, Green, and Blue. Note that this is not the same as saying that Gender_t variables can have the strings 'Male' and 'Female' as values. Male and Female are actually declared as new constant terms (with name identifiers because they are static objects), just as Gender_t itself is declared as a new type name.
Enumerated types are used extensively to tailor data types to be more readable. Here's example of a structure for a genealogical database.
Gender_t = Male | Female
P_data_t = (name:S, {person's name}
gender:Gender_t,
b_date:Date_t, {date of birth}
d_date:Date_t, {date of death}
comment:S)
Enumerated type values are really just new names for the integers starting at 0; for instance, Red is just 0,
Yellow is 1, Green is 2, and Blue is 3. This is also how they are represented internally. However, FormulaOne
enforces syntactic restrictions on programs which ensure that variables of an enumerated type get assigned only
terms of that type. So enumerated types give no extra programming power, just increased readability.
Vehicle_t = Tricycle | Car(doors:I, engine_size:I) | Bicycle(gears:I) | MotorcycleThe above declaration defines Tricycle and Motorcycle as new constant terms of type Vehicle_t (represented by 0 and 3), as with enumerated types. But it also defines all expressions of the form Car (a, b) and Bicycle(a), where a and b are integer terms, to be terms of type Vehicle_t.
pred ... iff
v1 :> Vehicle & v2 :> Vehicle &
... &
(v1 = Motorcycle | v1 = Car(4, 4000)) &
v2 = Bicycle(v1.doors) &
...
Note the use of the field-selection feature in the last formula above. When we refer to a field of a union type,
we do it without referring to the variant name (like Motorcycle or Car). Whenever we select fields of a union
variable, FormulaOne inserts an implicit test just before the formula containing the field term, to make sure
that the variant name is the one containing the field name. So the formula
v2 = Bicycle(v1.doors)acts just like the formula
v1 = Car(d,s) & v2 = Bicycle(d)The field names appearing in different variants of a union type expression must therefore be different, so that FormulaOne can tell which variant a union variable field is in. Since union type definitions can be recursive, we can create important data structures in FormulaOne, such as trees.
Tree_t = Nulltree | Node(node_val:I, left:Tree_t, right:Tree_t)Recursively-defined types lend themselves naturally to recursive procedures. Consider this one for inserting a leaf into a structure of type Tree:
proc Insert_tree(x :< I, tree :. Tree_t) iff
case tree of
Nulltree => tree := Node(x, Nulltree, Nulltree);
Node(nv, l, r) => if x = nv then {x is already there}
true
elsif x < nv then
Insert_tree(x, tree.left)
else
Insert_tree(x, tree.right)
end;
end
The following queries insert different values into the tree x:
x := Node(5,Node(2,Nulltree,Nulltree),Nulltree) & Insert_tree(7,x)
x := Node(5,Node(2,Nulltree,Nulltree),Nulltree) & Insert_tree(3,x)
x := Node(5,Node(2,Nulltree,Nulltree),Nulltree) & Insert_tree(4,x)The results in the same order are:
x = Node(5,Node(2,Nulltree,Nulltree), Node(7,Nulltree,Nulltree)) x = Node(5,Node(2,Nulltree,Node(3,Nulltree,Nulltree)), Nulltree) x = Node(5,Node(2,Nulltree,Node(4,Nulltree,Nulltree)), Nulltree)Note the use of tree.left and tree.right in the recursive calls to Insert_tree. When a formula like
tree = Node(nv, l, r)is processed, if the variable on the left is of any mode except input/output, the compiler would consider the parts of the union term on the right to be just synonyms for the fields of the variable. That is, the compiler would have associated the variable nv with the exact storage location assigned to tree.nodeval, I with tree.left, and so on.
But when the variable is of input/output mode, a formula like this causes FormulaOne to make a separate copy of the fields of the tree, and assign the new variables to those copies. So if we had used l and r instead of tree.left and tree.right, we would have been referring to copies of the subtrees of tree, instead of the actual parts that we need to replace in the recursive calls.
In the case of input/output tuple or union types, only field selection terms refer to parts the of the original structures.The name of the universal type is U, and it looks to programs as if it has been defined with the following recursive definition:
Consider the following definition, of a procedure which "reverses" any list.
proc Reverse(x :< U, y :> U) iff
Revl(x, Nil, y)
proc Revl(x :< list U, sofar :< list U, y :> list U) iff
case x of
Nil => y = sofar;
(h, t) => Revl(t, (h, sofar), y);
end
We have given the Reverse procedure parameters of type U so that any term can be given as a parameter.
However, a procedure call like Reverse(a,b) will fail if a is not of some list type, because when it is
passed along as an argument to Revl, it will fail to be converted into a list. So the query
x :> I & x = 10 & Reverse(x, y)should fail, while the query
x :> list I & y :> list I & x = (3,2,1,Nil) & Reverse(x,y)should return y = (1, 2, 3, Nil). Note the automatic conversion from the type list I to the universal type U and back inserted by the FormulaOne compiler.
Computationally, however, the type cast term has the effect of taking the value of the term and deriving a term in the
representation of the type; this new term is the term used.
For instance, if v is of the type Vehicle declared earlier, then the formula
Fib5(v:I, y)will pass a version of v to Fib5, in the representation of integers - if v can be so represented. As it turns out, the only terms of type Vehicle which can be represented as integers are Tricycle and Motorcycle, which have the values 0 and 3. If v has any other value, the type cast will fail and so the call to FibS will fail.
Similarly, if v is of type I, then the term v:L will stand for the value of v, represented in the unlimited precision-bit representation of L variables rather than the 32-bit representation of I variables. But in fact it's unnecessary to give a type cast term in this case, because this cast is one of the many that are done automatically by type coercion. Type coercion are done automatically between U and any type, and between L, I, R, and subranges. That is, if a variable of type L is assigned a value of type I, or a parameter of type L gets an argument of type I, no explicit type cast is necessary. FormulaOne does some other coercion, too.
The automatic coercion between U and other types is particularly important, because it allows programmers to write predicates (like Reverse above) which take any term as a parameter. Languages with strict type structures, like Pascal or Turbo Prolog, would totally disallow such predicates, because there is no notion of universal type in those languages.P_data_at = [0..3] -> P_data_tThis declaration says that a variable of type P_data_at is an array with elements of type P_data_t, indexed by elements of type [0..3]; that is, a set of 4 elements of the P_data_t type. The following type is an array of three arrays of four integers each:
Matrix_t = [0..2] -> [0..3] -> IThe arrows are right-associative, so that the indices of an array of type Matrix_t are of type [0..2] and the elements are of type [0..3] -> I.
The syntax for selecting elements of the array is the one that most programming languages have. The expression v(i), where v is a term of an array type, and i is a term whose value is of the index type of v, stands for the i-th element of the array v. (For nested arrays, such as Matrix_t above, the index expressions can be grouped within the parentheses; for example, m(l,2) means the same thing as m(l)(2).)
proc Youngest(pers_arr :< P_data_at, y_name :> S) iff
{the name of the youngest person in 'pers_arr' is 'y_name'}
Youngest1(pers_arr, 1, pers_arr(0), y_name)
proc Youngest1(pers_arr :< P_data_at,curr :< I ,y_sofar :< P_data_t, y_name :> S) iff
{ The youngest in 'pers_arr' before index 'curr' is 'y_sofar' and the name of the
youngest overall is 'y_name' }
if curr >= Len(pers_arr) then
{we have reached the end of the array}
y_name = y_sofar.name
elsif
Before1(pers_arr(curr).b_date, y_sofar.b_date)
then
{current is older than youngest so far}
Youngest1(pers_arr, curr+1, y_sofar, y_name)
else
{current is youngest}
Youngest1(pers_arr, curr+1, pers_arr(curr), y_name)
end
See next section for a query using the predicate Youngest1.
The expression pers_arr(curr) above refers to the curr-th element of the pers_arr array, which is a term of type P_data_t. Since it is a term of type P_data_t, fields can be selected from it like any other such term; so pers_arr(curr).name is its name, etc.
The elements of the array are represented side-by-side in computer memory, and there can obviously be only a finite number of them for any one array. So the type expression that appears to the left of the -> in an array type expression cannot be just any type; it normally must be a finite type, except in the cases noted in flexible arrays below. A finite type is defined as being an enumerated type, a subrange of the integers ([m..n]), or any defined type whose definition is a finite type. For now, an array index type which is a subrange must start with 0; but this restriction may be lifted in later versions of FormulaOne.
pred Wackafoo(ca :< I, cb :< Date_t) iff
parents:>[0..l]->Person &
matrix:>[0..2]->[0..2]->I &
... &
parents = [('Charles', ca, cb),('Diana', 26, (1961, 7, 1))] &
matrix = [[8, 1, 6], [3, 5, 7], [4, 9, 2]] &
...
Note that these array constants can be nested, as in the matrix example above. We can construct an array of type P_data_at by the
following predicate
proc Construct_arr(pers_arr :> P_data_at) iff
pers_arr = [('Johann',Male,(1800,5,15),(1887,2,10),'friend of Wagner and Liszt'),
('Theresa',Female,(1897,2,1),(1979,8,14), 'moved to USA in 1920'),
('Dagmar',Female,(1834,4,29),(1915,9,23),
'had twins twice in a row'), ( 'Thomas',Male,(1889,7,11),(1971,1,28) ,
'was FDR s personal physician') ]
Now we can determine the youngest person by running the query
Construct_arr(pers) & Youngest(pers,name)which should find the solution
name = TheresaAn array output or input/output variable must be initialized on its first use, like any other variable of those modes. This may pose some problems. Some arrays have so many elements, or elements which are so complex, that the array constants we can use as values for them can become excessively large. So FormulaOne has a predefined procedure, Dupl, that can make such initializations easier. It takes three arguments: the number of elements in the array; the value to duplicate; and the variable to receive the value. Dupl is a function, so functional notation can be used with it too.
pred ... iff
parents:.[0..39]->Person &
row:>[0..9]->I & matrix:.[0..9]->[0..9]->I &
... &
Dupl(40, ("Null", 0, (1900, 0, 0)), parents) &
row = Dupl(10, 0) & Dupl(10, row, matrix) &
...
Dupl is a polymorphic procedure because it accepts different types of parameters. For all types T, Dupl acts like a
procedure with the following declaration:
proc Dupl(len :< I, val :< T, arr :> [0..]->T) iff
...
A flexible array is any array whose index type is [0..]. This is the only exception to the rule that an array index type must be finite. The variable declaration
x :> [0..] -> Ideclares an output flexible array with element type I. The length of the array will be known only at the time x is initialized; the initializing formulas
x = [9, 99, 999] Dupl(10, 0, x)would initialize x to have 3 elements and 10 elements, respectively. Flexible arrays are most often used as types of formal arguments for predicates which can process actual argument arrays of arbitrary length. The following procedure Asum adds together elements of a flexible array:
Flex = [0..]->I
proc Asum(a :< Flex, sum :> I) iff
Asum1(a,Len(a)-1,0,sum)
proc Asum1(a :< Flex, index :< I, accum :< I, sum :> I) iff
if index >= 0 then
Asum1(a,index-1,accum + a(index),sum)
else
sum = accum
end
Note the use of the length predicate Len to determine the upper bound of the flexible array a, which is then
passed to the auxiliary procedure Asum1. Incidentally, the procedure Asum1 is written in the so-called accumulator style where
the sum is being accumulated via the input argument accum and is returned through the argument sum at the end of the recursion.
This, rather than the conceptually simpler and more straightforward recursion, has the advantage of being tail-recursive.
The compiler of FormulaOne compiles the procedure Asuml as a loop. See the section Tail Recursion Elimination for more information.a:>[0..99]->I & Initialize(a) & sum = Asum(a)The array a is declared to contain 100 elements, it is assigned a value by the procedure Initialize and it is then passed to the procedure Asum.
a :> Flex & a = [2,3,4,5]The variable a is given a four element array as a value. This method works when the size of the array is small and the length of the array is known during the compile time. Flexible arrays are used most often in dynamic situations where the size of the array is given by a variable rather than by a constant.
The second method of creating flexible arrays uses input/output array variables:
...
a:.Flex & Dupl(n,0,a) & Set(a,0)
...
proc Set(a :. Flex, index :< I) iff
if index < Len(a) then
a(index) := index & Set(a,index + 1)
end
The input/output array a is first allocated to contain n elements (all initialized to zeros). The elements are then set
by the procedure Set. This method of incremental assignment of element values works with input/output arrays
(where it is possible to change a single element) or with symbolic arrays (where constraints can be set to the arbitrary elements).
Flexible output arrays must be given full values at one time. This is possible by the third method of using a cast to convert a list to an array:
a = lst:FlexHere lst is an already constructed list of integers.
The standard procedure Dupl which allocates flexible arrays is used mostly to initialize input/output arrays. FormulaOne allows the use of the standard predicate Len as a constraint to set the length of a flexible symbolic array:
a::Flex & Len(n,a)Here the input integer variable n gives the size to the flexible symbolic array a.
Let's look at a typical definition of a file, to see how it links to programs and to secondary storage. Say we had defined the type P_data_t. Then we could define the type of file with records of type P_data_t as follows:
P_data_ft = file P_data_t(In this document, we use the convention that file types end with the characters '_ft'.) The file is treated as a data structure of the given type, which must be a file type. For example, if the database file storing the actual records is c:\Database\pdata.dbs, we can define P_data
P_data :< P_data_ft = 'c:\\Database\\pdata.dbs':P_data_ftThe record type of a file does not have to be a tuple; it can be a union expression or basic type (such as S), and it can even be a recursively-defined tuple, like Tree_t. So an entire tree structure can be stored on a disk file for later recovery into another run of a query.
start->|A|....|P|Q|R|....|Z|<-end ptr->|Then, as we advance the file pointer, it points to records further and further on in the file.
start->|A|....|P|Q|R|....|Z|<-end
ptr->|
Records are deleted or inserted by deleting them from or inserting them into the list at the point to which the file pointer is pointing.
In the program, however, we cannot refer to file variables as lists with pointers. We can only pass them as arguments to predicates and procedures.
Several predefined procedures exist for manipulating files and file pointers. They are:
The first six change the file pointer without affecting the contents of the file, while the last three change the contents. These procedures are not accessible automatically. They reside in the standard module files, that comes with the FormulaOne package. If one of your modules uses the file procedures, you must therefore specify that your module uses the file module. When you create or update the module you should enter names of used modules into the module header.
{prints each record in 'f'}
proc Printall(f:.P_data_ft) iff
if DbAccess(f, person) then
Print(person,'\n') & DbSkip(f,1) & Printall(f)
end
If we have the above procedure in a compiled module, and the P_data database file defined as above, we can issue the query
Printall(P_data)and expect it to print all the records in the file (if there are any).
'Heather',Female,(1961,7,2),(0,1,1),'Musician' 'Isadora',Female,(1924,3,22),(0,1,1),'Homemaker' 'Steven',Male,(1921,9,20),(0,1,1),'Engineer'DbAccess file predicates, takes two arguments, a file and an output variable of the record type of the file. If T is the record type, then DbAccess can act as a procedure with the following declaration.
proc DbAccess(f:<file T, rec:>T)DbAccess, like all the other file procedures, is polymorphic. It can act as a procedure with the given types of parameters for any type T. It has the effect of setting the output variable to the next record in the file after the file pointer. For instance, if the file is in the following state, the record read into the second argument will be Q.
start->|A|....|P|Q|R|....|Z|<-end ptr->|If the pointer is pointing after the last record in the file - that is, if there are no records to fetch - DbAccess fails. DbAccess never actually changes the file pointer, even after it has copied the record into its output parameter. That is the job of DbSkip. DbSkip takes two arguments, a file and an integer containing the number of records to skip.
proc DbSkip(f:.file T, n :<L)It has the effect of advancing the file pointer past the record it is currently pointing to, by the given number of records. Before DbSkip(f, 1):
start->|A|....|P|Q|R|....|Z|<-end
ptr->|
After DbSkip(f, 1):
start->|A|....|P|Q|R|....|Z|<-end
ptr->|
If the number of records in the file is less than the number requested to skip, DbSkip moves the pointer after the last record.
This includes the case in which the pointer is at the end of the file (0 records left). DbSkip never fails unless its second argument
is less than 0. So in the processing of the query above, DbAccess gets into variable person the next record after the file pointer, and
each call to DbSkip advances the file pointer by one record. DbAccess fails when the end of the file is reached, causing the
recursion to "bottom out".
DbAccess is a procedure with no input/output parameters, so it can be used in if formulas. In circumstances where you don't need to
test whether or not a record is there, you may more likely use the DbGet procedure predicate than DbAccess in your programs.
proc DbGet(f:.file T, rec:>T)DbGet(f,x) has exactly the same effect as DbAccess(f,x) & DbSkip(f,l); that is, it gets the current record into x and advances the pointer by one record - unless the pointer is at the end of the file, in which case the DbGet fails. DbGet works well in combination with the procedure DbEof, which succeeds if and only if its argument is a file positioned at the end.
proc DbEof(f :<file T)DbEof also has no input/output parameters, and can be used in ifs. Using DbGet and DbEof, we can write an alternative version of our earlier Printall procedure.
{prints each record in 'f'}
proc Printall1(f:.P_data_ft) iff
if DbEof(f) then
Print('End of file')
else
DbGet(f,person) & Print(person,'\n') & Printall1(f)
end
proc DbRewind(f:.file T)
start->|A|....|P|Q|R|....|Z|<-end ptr->|DbEofSet also takes an input/output file as its argument.
proc DbEofSet(f:.file T)It has the effect of setting the pointer to the end of the file, after the last record.
start->|A|....|P|Q|R|....|Z|<-end
ptr->|
DbEofSet is not very useful when reading a file, and is usually used in conjunction with file-writing routines. However,
DbRewind can come in handy when reading, as in this Read_circ routine which treats the
file as a circular list of records:
{ read 'pers' from 'f', rewinding to the start if end-of-file }
proc Read_circ(f:.P_data_ft, pers:>P_data_t) iff
if DbEof(f) then
DbRewind(f)
end & DbGet(f,pers)
Note that in the above procedure, if the file is empty, the DbGet call will fail, so the procedure will fail. This behavior is
probably consistent with what we want from it.
proc DbPut(f:.file T, x:<T)It inserts a record, with given value, before the next record after the file pointer, and then skips past the inserted record. Say the file is in the following state.
start->|A|....|P|Q|R|....|Z|<-end
ptr->|
If a record - we'll call it V - is inserted with DbPut, the new state of the file will be the following.
start->|A|....|P|V|Q|R|...|Z|<-end
ptr->|
DbPut skips the inserted record automatically, so that repeated DbPuts insert records in sequence.
proc CreateP_dataFile(f:.P_data_ft) iff
DbRewind(f) & DbTruncate(f) & {delete any existing records first}
DbPut(f,('Heather',Female,(1961,7,2),(0,1,1),'Musician')) &
DbPut(f,('Isadora',Female,(1924,3,22),(0,1,1),'Homemaker')) &
DbPut(f,('Steven',Male,(1921,9,20),(0,1,1),'Engineer'))
Note the code line containing DbRewind(f) & DbTruncate(f). These two calls in effect delete all previously
existing records from the file. Without this line, multiple calls to CreateP_dataFile would keep adding the same
three records to the database file with each call.
proc CreateP_dataFile1(f:.P_data_ft) iff
DbInsert(f,('Isadora',Female,(1924,3,22),(0,1,1),'Homemaker')) &
DbInsert(f,('Heather',Female,(1961,7,2),(0,1,1),'Musician')) &
DbInsert(f,('Steven',Male,(1921,9,20),(0,1,1),'Engineer')) &
DbInsert(f,('Isadora',Female,(1924,3,22),(0,1,1),'Homemaker')) &
DbInsert(f,('Steven',Male,(1921,9,20),(0,1,1),'Engineer'))
The routine creates a database file that contains only the following records:
'Heather',Female,(1961,7,2),(0,1,1),'Musician' 'Isadora',Female,(1924,3,22),(0,1,1),'Homemaker' 'Steven',Male,(1921,9,20),(0,1,1),'Engineer'Unlike using DbPut, DbInsert places the records within the database file based on the actual records content. The records are inserted in standard order for sorting. Standard order of sorting basically specifies a method to determine which record is "smaller". If a record of the same value already exists, the record in not inserted again, otherwise the record is inserted after the first record of a "smaller" value. To keep the whole database file in sorted order, do not mix DbPut and DbInsert.
proc DbDelete(f:.file T)It removes the record after the pointer, as if doing a DbSkip and deleting whatever it encountered on the way. As with DbSkip, if the pointer is at the end of the file, DbDelete fails. Before DbDelete:
start->|A|....|P|Q|R|....|Z|<-end
ptr->|
After DbDelete:
start->|A|....|P|R|....|Z|<-end
ptr->|
DbTruncate also takes a single input/output file, proc DbTruncate(f:.file U)It has the effect of deleting every record in the file from the current record on, that is, "truncating" the file at the current file pointer location. Before DbTrunk:
start->|A|....|P|Q|R|....|Z|<-end
ptr->|
After DbTrunk:
start->|A|....|P|<-end
ptr->|
pred Man(person_name::S) iff
P_data(person_name, Male, b, d, c)
pred Woman(person_name::S) iff
P_data(person_name, Female, b, d, c)
The queries:
all Man('Steven')
all Woman('Steven')
will succeed and fail respectively. P_data, when used in this way, acts as a predicate
which matches its arguments with any of the records in the file.
('Heather',Female,(1961,7,2),(0,1,1),'Musician')
('Isadora',Female,(1924,3,22),(0,1,1),'Homemaker')
('Steven',Male,(1921,9,20),(0,1,1),'Engineer')
then P_data as a predicate would be equivalent to the following:
pred P_data_pred(tuple:>P_data_t) iff
tuple = ('Heather', Female,(1961,7,2),(0,1,1),'Musician')
| tuple = ('Isadora', Female,(1924,3,22),(0,1,1),'Homemaker')
| tuple = ('Steven', Male,(1921,9,20),(0,1,1),'Engineer')
P_data can also be accessed in queries, as any regular predicate can; for instance,
all P_data(x)
all P_data_pred(x)will list all the records in the P_data file, and
all n P_data(n, g, b, d, c)
all n P_data_pred(n, g, b, d, c)will list just the names (the expression in the parentheses being a "deconstructor" term which gets the value of the output parameter as it comes out).
P_data_t = (name:S, {person's name}
gender:Gender_t,
b_date:Date_t, {date of birth}
d_date:Date_t, {date of death}
comment:S)
Let us also assume we will want to search the database for a specific name, birthday date b_date, gender and the year
of birth b_date.year. For this purpose we define the following database file type:
P_data_ft2 = file P_data_t[gender,name,b_date,b_date.year]Creating a database file of the type P_data_ft2 will not only create a database file containing the actual records of type P_data_t, but also index files corresponding to the record fields name, birthday date b_date, gender and the year of birth b_date.year. There will be one separate index file for each index. Note that the order of indeces is irrelevant, but two file types with the same indeces but with the indeces in a different order are considered two different types. So when we create a database file pdataIx.dbs using the following declaration:
P_data2 :< P_data_ft2 = 'pdataIx.dbs':P_data_ft2several files will be created: pdataIx.dbs, pdataIx.dbs.000, pdataIx.dbs.001, pdataIx.dbs.002, pdataIx.dbs.003. Inserting or deleting a record in the database file will automatically update all index files, so modifying an indexed database files can be significantly slower than modifying a database file without indeces, however searching the indexed database will be significantly faster than searching a database file without indeces.
proc CreateIndexFile(f:.P_data_ft2) iff
DbRewind(f) & DbTruncate(f) & {delete any existing records first}
DbPut(f,('Heather',Female,(1961,7,2),(0,1,1),'Musician')) &
DbPut(f,('Isadora',Female,(1924,3,22),(0,1,1),'Homemaker')) &
DbPut(f,('Steven',Male,(1921,9,20),(0,1,1),'Engineer')) &
DbPut(f,('Alexa',Female,(1973,10,11),(0,1,1),'Student')) &
DbPut(f,('Douglas',Male,(1992,5,14),(0,1,1),'Student')) &
DbPut(f,('Lukas',Male,(1989,6,28),(0,1,1),'Student')) &
DbPut(f,('Megan',Female,(1992,5,14),(0,1,1),'Student')) &
DbPut(f,('Boris',Male,(1955,7,25),(0,1,1),'Programmer')) &
DbPut(f,('John',Male,(1945,7,15),(0,1,1),'Trucker')) &
DbPut(f,('Ernest',Male,(1955,7,25),(0,1,1),'Programmer')) &
DbPut(f,('Patrick',Male,(1955,2,17),(0,1,1),'Programmer')) &
DbPut(f,('Jimmy',Male,(1955,2,17),(0,1,1),'')) &
DbPut(f,('Emanuella',Female,(1955,12,25),(0,1,1),'born on Christmas Day!')) &
DbPut(f,('Ella',Female,(1924,3,1),(0,1,1),'Retired'))
Note that in the code above we did not bother to keep the database file records in any particular sorted order.
To create the database file and all index files, run the query
CreateIndexFile(P_data2)Having successfully created the files, now we can easily search the database for various records. For example, the code in DumpAllBirthdayYear will print out all records with the given year of birth:
proc DumpAllBirthdayYear(f:.P_data_ft2,year:<I) iff
DbSeek(f.b_date.year,year) & DumpAllBirthdayYear1(f)
proc DumpAllBirthdayYear1(f:.P_data_ft2) iff
if DbAccess(f,y) then
Print(y,'\n') &
DbSeekNextEq(f.b_date.year) & DumpAllBirthdayYear1(f)
else
Print('<EOF>')
end
For example, we can find all records with the year of birth 1955 by issuing the query
DumpAllBirthdayYear(P_data2,1955)Given the records as entered in the routine CreateIndexFile, the results will be
'Boris',Male,(1955,7,25),(0,1,1),'Programmer' 'Ernest',Male,(1955,7,25),(0,1,1),'Programmer' 'Patrick',Male,(1955,2,17),(0,1,1),'Programmer' 'Jimmy',Male,(1955,2,17),(0,1,1),'' 'Emanuella',Female,(1955,12,25),(0,1,1),'born on Christmas Day!' <EOF>It is easy to create similar routines to search records using different record fields.
proc DumpAllNames(f:.P_data_ft2) iff
DbSeekFirst(f.name) & DumpAllNames1(f)
proc DumpAllNames1(f:.P_data_ft2) iff
if DbAccess(f,y) then
Print('\nname:', y) &
DbSeekNext(f.name) & DumpAllNames1(f)
else
Print('<EOF>')
end
There are several additional runtime index file seek routines, they all either find the corresponding record and position
the database file pointer to point to the record or position the file pointer to the end of the file. Once the file pointer has been
set to point to a record, you can use DbAccess, or DbGet to read the record or DbDelete to delete the record.
Deleting the record will delete all corresponding index file entries for the record automatically. Once a record has been deleted,
any record comparisons are ill defined; therefore start a new search with an absolute DbSeek instead of relative seeks such as DbSeekNextEq,
DbSeekNextGt etc.
The various seek routines are described in more detail in the section describing the Runtime Library:
DbSeek, DbSeekNext, DbSeekNextEq,
DbSeekPrev, DbSeekPrevEq, DbSeekFirst,
DbSeekLast, DbSeekLt, DbSeekGt
proc DumpAscii(f:.Ascii) iff
if DbAccess(f,y) then
Print(y,'\n') & DbSkip(f,1) & DumpAscii(f)
end
DumpAscii can be called to print out a particular text file using the file name (keep in mind the file names are case insensitive):
DumpAscii('c:\\Temp\\License.txt')
Records, i.e. lines, cannot be deleted from an Ascii file, and no record can be
inserted in the middle. If either of these operations is attempted, an error condition is raised. However, records can be
appended to the end of the file with the DbPut procedure.
A Bin file is interpreted simply as a sequence of bytes. Each DbGet operation will get the next byte in the file,
regardless of whether the file is in text format, database file format, or any other format. These one-byte records cannot
be deleted, nor can any records be inserted in the middle. The DbPut procedure, however, has a special behavior with
Bin files: instead of inserting a byte, it overwrites the current byte, therefore doing the equivalent of a DbDelete followed by a DbPut.
proc All_men(m:>list P_data_t) iff
{'m' is the list of all men from the P_data file}
all rec in m
P_data(rec) & rec = (n, Male, b, d, c)
end
The body of this procedure consists of an all formula. It asserts that the list m is made up of elements
rec, each of which has the property that it is in the P_data file (used as a predicate) and has gender Male.
The all formula has the effect of collecting all the solutions for rec, and putting them in m in sorted order,
with duplicate elements removed.proc All_evens(x:<list L, x_evens:>list L) iff
{ 'x_evens' is a sorted list of all the even elements of 'x'}
all n in x_evens
n in x & Even(n)
end
The all formula, which again happens to form the entire body of the procedure, means that for each member n
of the list x_evens, the formula within the parentheses holds. For this procedure, the query
all All_evens((1, 7, 3, 6, 9, 6, 2, 5, 7, 4, Nil), x)would result in the single solution
x = (2, 4, 6, Nil)FormulaOne has extracted the even elements of the list (6, 6, 2, and 4), sorted them, and removed duplicates. all is for those cases when you need to refer to a predicate, or do some kind of backtracking, within a procedure or subroutine. The general format of an all formula is as follows:
y :> I & one xy = 3 & x=l | x = 2 end & y = 2 y :> I & y = 2 & one xy = 3 & x = l | x = 2 endAccording to the logic both formulas should yield the same result y = 2 & x = 2. The first formula fails because of the non-local assignment y = 3 within the one formula. The variable var of an all formula is a variable of type list (Tl,T2,...,Tn) where the type of the variable vari is Ti. If the variable var does not have an explicit declaration then it is implicitly declared to be an output variable of the above list type. The variables vari are local to the all formulas.
x :> I & min x & x::L & T(x) endThe variable x is a symbolic variable within the min and max formulas and output variable outside of it. If the variable vari of a min, max or one formula does not have an explicit declaration outside of the formula then it is implicitly declared to be an output variable of the same type as inside the formula.
if a < b, or if a = b and c < d, then (a, c) < (b, d) . if a = b and c = d, then (a, c) = (b, d). Otherwise,(a, c) > (b, d).
All reals (including integers) are less than all strings, which are less than all pairs. FormulaOne thus provides the programmer with a general sorting facility. We can use this fact to program an inefficient, but working general sorting procedure.proc Sort(x :< list U, key_code :< I, sx :> list U) iff
{ 'sx' is 'x' sorted by the Key function by the given 'key_code', with duplicates removed }
ksx :> list (U, U) & {keyed, sorted x}
all key, xe in ksx { get elements of x, pair with keys, sort }
xe in x & Key(xe, key_code, key)
end &
Unkeyed_list(ksx, sx) { take off keys }
proc Unkeyed_list(ky :< list (U, U), y :> list U) iff
{ 'ky' is a list of elements paired with their keys; 'y' is the list of just the elements }
case ky of
Nil => y = Nil;
((key, elt), tail) => y = (elt, Unkeyed_list(tail));
end
{sample Key function}
proc Key(x :< U, key_code :< I, key :> U) iff
case key_code:[0..4] of
0 => {P_data_t, sort by name}
y = (x:P_data_t) & key = y.name;
1 => {P_data_t, sort by birthdate}
y = (x:P_data_t) & key = y.b_date;
2 => {Date_t, sort by month}
y = (x:Date_t) & key = y.month;
3 => {Real or other number, sort in descending order}
x = R(n) & key = -n;
else {sort by standard order; use 0 as key}
key = 0
end
all n, g, b, d, c in 'all_pdata.txt'
P_data(n, g, b, d, c)
A query which can only be a subroutine or procedure body cannot have an all clause, so it can do its output only to the screen.
This is not much of a restriction, since at most one solution will ever come back, and since subroutines and procedures can do
whatever i/o they want to files.
all n, g, b, d, c in Men_data
P_data(n, g, b, d, c) & g = Male
This query has the effect that the output of the query proper (the part on the second line) is not displayed on the screen,
but re-routed to the file Men_data, one record per solution. Before this query will work
Men_data must be defined within a FormulaOne module in the same way as P_data was, for example using the following
definition:
Men_data :< P_data_ft = 'mendata.dbs':P_data_ftSay P_data contained the following records before the query:
'Heather',Female,(1961,7,2),(0,1,1),'Musician' 'Isadora',Female,(1924,3,22),(0,1,1),'Homemaker' 'Steven',Male,(1921,9,20),(0,1,1),'Engineer'Then Men_data will contain only the record
'Steven',Male,(1921,9,20),(0,1,1),'Engineer'after the query. The records that met the conditions in the query will have been copied over in a sorted order.
proc Get_men(f:.P_data_ft) iff
{get all men from P_data into f}
all n, g, b, d, c in f
P_data(n, g, b, d, c) & g = Male
end
Then the query
Get_men(Men_data)would have exactly the same effect as the query at the start of this section.
Maxnames :< I = 20
Pi :< R = 3.14159
Princess :< P_data_t = ('Diana', Female, (1961, 7, 1),(0, 1, 1), 'Spencer')
Declared constants are objects whose value remains static throughout programs, so they are given capitalized name identifiers.
The general form of a constant declaration is:
Maxsize :< I = 100
Table = [0..Maxsize-l]->S
proc Tabulate(table :< Table,f:.Ascii) iff
...
Actions = Delete | Add | Modify
Mylist :< list S = 'Smith','Jones','Meredith',Nil
proc Crosstab(table :< Table, action:< Actions) iff
Process(Mylist) &
...
proc Process(s :< list S) iff
...
proc All_men(m :> list P_data_t) iff
{'m' is the list of all men from the P_data file}
all rec in m
P_data(rec) & rec = (n, Male, b, d, c)
end
We really don't care what the values of n, b, d, and c are in this procedure; we just put them there to take
the place of the parts of the record. So we could re-code this procedure as:
proc All_men1(m:>list P_data_t) iff
{'m' is the list of all men from the P_data file}
all rec in m
P_data(rec) & rec = (_, Male, _, _, _)
end
The anonymous variables in the equation mean less overhead for the compiler in remembering variable names, and they also indicate
clearly that we don't care what the values of those parts of rec are.
pred ListLook(x :< list L]) iff
x = (h,t) & Print(h)
| x = Nil & h :> S & h = 'Nil' & Print(h)
This works because of the or ( | ).
The compiler knows that the variables h on each side or branch of the or are different local variables. This is an interesting
feature of FormulaOne, but it must be used with caution: the variables have meaning or scope only within the branch where they are defined.
To attempt to reference h later in ListLook will result in an error because the compiler will not know which h is being referred to.
Also, the duplicate definition of h would not be accepted if we had used & instead of |. This is prevented by the laws of logic.
If we had used &, we would be saying that h must be defined as a long integer L and as a string S at the same time.
Many local variables in FormulaOne have the property of being implicitly existentially quantified. An example which we encountered very
early on was the Sum predicate in this line:
Sum(tail,tailsum)In plain English we can restate this as "there exists a variable tailsum such that Sum(tail,tailsum) is true". Quantifiers and quantification are topics of mathematical logic beyond the purpose of this text. However it is useful to be able to convert in your own mind from FormulaOne code to the natural language equivalent. When you encounter a variable like tailsum, realize that it has this implicit existential quantification which extends over its scope; that is, over the portion of the program wherever the variable is to be found.
pred Sum(l::list L,sum::L) iff
...
can be read as "for all variables which are lists of long integers and for all variables sum which are long integers, the predicate
Sum is true if and only if the following conditions hold...".
Number_type = Prime | Composite
Sieve_type = [0..] -> Number_type
proc Print_primes(max :< I) iff
...
local proc Sift_print_from(sieve :. Sieve_type, first :< I, max :< I) iff
...
local proc Multiples_marked(sieve :. Sieve_type, prime :< I, multiple :< I ,max :< I) iff
...
Now, if any module uses Sieve, the only procedure it will be able to "see" will be Print_primes. If the using module refers to
one of the local procedures, it will get an 'identifier undefined' error message.
This means less overhead for the system when loading the Sieve module; less chance of error by a predicate mis-using the two auxiliary procedures;
and an explicit description of which procedures are intended to be called from other modules.
The local keyword also works for constant and type declarations. Some examples:
local Pi :< R = 3.14159 local Number_type = Prime | Composite local Date = (year:I, month:[1..12], day:[1..31])
Complex = (R, R)
proc Complex_product(x:<Complex, y:<Complex, prod:>Complex) iff
x = (xre, xim) & y = (yre, yim) &
prod = ( (xre*yre - xim*yim), (xre*yim + yre*xim) )
Unnamed tuples involve a little less overhead for the system. They are no less efficient to use, because the "disassembling"
operations x = (xre, xim), for instance, is implemented by associating the variables xre and xim
with the appropriate parts of the term x.
Four friends, including Tim, gathered at Tim's home on a Sunday afternoon to compare the Apple Macintosh and the IBM PC. From the clues that follow, determine each person's last name (one is Brown) and occupation (one is a teacher). 1. Two of Tim's guests were Ann and the doctor. 2. Jack, whose last name is not Blue, prefers the IBM PC. 3. Ann is not the dentist. 4. Grey, a keen Macintosh user, went home before the benchmarks were finished. 5. Jill and Green were both delighted when the Macintosh finished the last test before the PC. 6. The lawyer was the last person to go home. 7. Blue is not the doctor.One brute-force solution to this problem would be to just generate all 4!*4!*4!= 13824 combinations of first name, last name, and occupation, and test them to see whether they meet all the conditions. This is what most Prolog implementations would have to do, unless some constraint-satisfaction code were written specifically for the problem. Here is a FormulaOne solution to the puzzle that makes use of injections and relations.
First_t = Tim | Ann | Jack | Jill
Last_t = Green | Brown | Blue | Grey
Job_t = Doctor | Dentist | Lawyer | Teacher
Name_t = First_t ->> Last_t
Occ_t = Job_t ->> Last_t
pred Hackers(lastname::Name_t, occ::Occ_t) iff
likesMac::rel Last_t & guest::rel Last_t &
~lastname(Tim) in guest &
{1} lastname(Ann) in guest & occ(Doctor) in guest & lastname(Ann) <> occ(Doctor) &
{2} lastname(Jack) <> Blue & ~lastname(Jack) in likesMac &
{3} lastname(Ann) <> occ(Dentist) &
{4} Grey in likesMac & Grey in guest &
{5} lastname(Jill) in likesMac & Green in likesMac &
lastname(Jill) <> Green & Grey <> lastname(Jill) &
{6} occ(Lawyer) in guest & occ(Lawyer) <> Grey &
{7} Blue <> occ(Doctor)
We'll describe the new features used in this example in the sections below.
ID_inj_t = [0..9] ->> I Reordering_t = [0..15] ->>[0..15]An injection works just like an array which has had constraints put on it specifying that no two elements of it are equal to one another. So in the Hackers example predicate,the variable lastname, of type Name_t, is an array of last names, indexed by first names, in which no two of the last names are the same. When the system encounters further constraints on lastname, like
lastname(Jack) <> Blue & lastname(Ann) <> occ(Doctor)it puts additional constraints on the variables involved. If there were any equality constraints, like
lastname(Jack) = Greythen the fact that the other three elements of lastname could not be Grey would have been propagated through the injection. But even without any equality constraints, eventually there are so many things that a particular element of each injection cannot be that there is only one thing that each element can be.
likesMac::rel Last_t & guest::rel Last_tdeclare likesMac and guest to be relation variable. Once a variable has been declared to be a relation, you can assert that values of the element type of the relation (like Last_t) are either in or not in the relation. A constraint formula on guest, like ~ lastname(Tim) in guest, asserts that the variable lastname(Tim) is not in the relation guest. If later information comes along that, for instance, occ(Doctor) in guest, the system will automatically deduce that lastname(Tim) and occ(Doctor) are not the same; that is, that lastname(Tim) <> occ(Doctor).
Islandtown, the main town on Cozy Island, is the crossroads for the island's four roads, each of which goes in a different direction (north, south, east, west) to one of the four outlying Cozy Island villages. Given this information and the clues, find each village's direction and distance from Islandtown, and the road that goes to that village. 1. The village on Ocean Road is 1 mile farther from Islandtown than Summerport is. 2. The closest village is 2 miles from Islandtown; no two villages are the same distance from Islandtown. 3. Winterharbor is a total of 6 miles by road from the village on Island Road. 4. The town on Conch Road is a total of 9 miles by road from Autumnbeach. 5. Springcove is twice as far by road from Islandtown as the village west of the main town. 6. The village on Bay Road, which doesn't go west, is 4 miles from Islandtown. 7. The village south is twice as far from Islandtown as the village north.The solution of this puzzle in FormulaOne is an elegant example of the use of long integer arithmetic constraints, injections, and the unknown index feature.
Road = Ocean_Road | Conch_Road | Bay_Road | Island_Road
Village = Winterharbor | Autumnbeach | Springcove | Summerport
Dir = North | East | South | West
pred Island(dist :: Road->>L[2..], dir :: Dir->>Road, vill::Village->>Road) iff
{1} dist(Ocean_Road) = dist(vill(Summerport)) + 1 &
{3} dist(vill(Winterharbor)) + dist(Island_Road) = 6 &
{4} dist(Conch_Road) + dist(vill(Autumnbeach)) = 9 &
{5} dist(vill(Springcove)) = 2 * dist(dir(West)) &
{6} Bay_Road <> dir(West) & dist(Bay_Road) = 4 &
{7} dist(dir(South)) = 2 * dist(dir(North))
This may look like a straightforward example of a puzzle with arithmetic constraints and
injections, but if you look more closely you'll see an interesting thing. The array element
term vill(Summerport), although its value is as yet unknown, is itself being used as an index to
the array dist. The same thing happens six more times in the course of the predicate.
When you give an array or injection index which is itself a symbolic variable, its value
may or may not be known at the time the system processes it. So FormulaOne essentially
declares an auxiliary variable of the type of the indexed array term, and sets a
constraint on the array that its element at the unknown index is equal to that new
variable.
For instance, take the formula
dist(Ocean_Road) = dist(vill(Summerport)) + 1This formula is equivalent to the formula
dist(Ocean_Road) = aux + 1 & aux = dist(vill(Summerport))Later, if it becomes known what dist(Ocean_Road) is, the value of aux will become known. That will have the effect of constraining vill(Summerport) to be, for instance, not equal to Ocean_road(otherwise aux would be equal to aux+1!). Similarly, if the value of vill(Summerport) becomes known, it may cause the value of aux to become known, and thus propagate back to the value of dist(Ocean_road).
A = [0. .2]->I B = S,L Bb = s:S,i:L C = list Bb D = E | F(I,D,D) Dd = Ee | Ff(i:I,l:Dd,r:Dd) ... a:>A & b:>Bb & c:>C & d:>D & dd:>Dd ...The array a can be constructed either by an array constructor
a = [5,6,7]or by the duplication predicate:
Dupl(3,4,a)or
a = Dupl(3,4)The last two formulas are equivalent to:
a = [4,4,4]Both n-tuple types B and Bb are the same, the type Bb includes the field names. The pair b is constructed with the help of the pairing operator ',':
b = 'Smith',56000Comma is also used to construct lists:
c = b,('Jones',20000),Nil
Union values are constructed by using the union tags:
d = E dd = Ff(6,Ee,Ee)The types D and Dd are not recognized by FormulaOne as the same types. Data structures of FormulaOne can be broken down into their constituents by the use of deconstructors. FormulaOne offers two types of deconstructors: Prolog-like and Pascal-like. Prolog-like deconstructors are similar to the constructors but they use explicitly or implicitly declared output (symbolic) variables:
a = [al,a2,a3]The implicitly declared output variables al, a2, and a3 obtain as their values the corresponding elements of the array a. Arrays can be deconstructed also by a Pascal-like indexing. For instance a(0) = a1, a(1) = a2. The tuple b can be deconstructed either in the Prolog style: b = x,y or by the use of Pascal-like field selectors (provided that the tuple type, i.e. Bb in this case, contains named fields). We have b.i = y.
c = v,w d = F(_,_,_) dd = Ff(i,p,q)The list c is non-empty, so, after deconstruction, we have (v = b)
v = 'Smith',56000and
w = ('Jones',20000),Nil
The tag of d is not F so the second deconstructor fails, the third one succeeds setting i = 6 and p = q = Ee.
The standard field names h (for the head) and t (for the tail) can be used to deconstruct lists in a Pascal-like fashion.
We have the following:
c.h = v c.t = w c.t.h.s = 'Jones'It is also possible to use the field names of components of lists directly, without the selectors h and t:
c.i = c.h.i = v.i = 56000.If the components of a union value are named we can deconstruct the value by selecting the component name in a Pascal-like fashion:
dd.l = p = Ee.
fact := 1;
while n >= 1 do begin
fact := n*fact;
n := n - 1;
end
Note that the variable fact is used as an accumulator to store the partial results of the computation. This loop can be
programmed with Pascal's efficiency in FormulaOne by a call to the tail-recursive procedure Fact:
fact = Fact(n,l)The tail-recursive procedure Fact is defined as follows:
proc Fact(n :< L,ace :< L,fact :> I) iff
if n >= 1 then
Fact(n - 1, n*acc, fact)
else
fact = ace
end
Note that the recursive call to Fact in its body is the last action performed in the body. Immediately after the
return from the recursion the procedure exits.proc Fact(n :< L, fact :> L) iff
if n >= 1 then
fact = n*Fact(n-l) {i.e. Fact(n-l,aux) & fact = n*aux }
else
fact = 1
end
This is because after the recursive call returns, the result must yet be computed by a multiplication.
There is no tail recursion optimization performed for the predicates (pred). The following example illustrates the reasons for it:
pred Maxlist(l::list [1..], max::I) iff
l = Nil & max = 0
| l = h,t & tmax::I & (tmax >= h & max = tmax | tmax < h & max = h) &
Maxlist(t,tmax)
The predicate Maxlist finds the maximum of a symbolic list of positive integers. After the seemingly tail-recursive call to find the maximum
of t returns, FormulaOne still has to make sure that there exists a value for the variable tmax such that the
constraint tmax >= h or tmax < h holds. In logic this situation is called
quantifier elimination. There is an implicit existential quantifier binding the variable tmax.pred OneThree (x :: I) iff
x = l | x = 3
Logically speaking, these two queries are identical:
~P(x) & x=2 x=2 & ~P(x)and must yield the same result - but they don't.
Person = name:S, salary:L
proc Lookup(persons :< list Person,name :< S,salary :> L) iff
persons = person,rest &
if person.name = name then
salary = person.salary
else
Lookup(rest,name,salary)
end
The call :
~Lookup(persons,'Smith',_)which is the same as the call
~Lookup(persons,'Smith', s)with a local variable s, succeeds iff (if and only if) it is not the case that there is a salary s such that Lookup(persons,'Smith',s) holds, i.e. iff the name 'Smith' does not occur in the list persons.
A & B | ~A & CThe formula A is called the condition of the if formula. Since the conditions of if formulas are negated the same restrictions as with negations apply. Conditions are processed in the procedure context without backtracking. No symbolic variables and no assignments to non-local output and input/output variables are allowed within the conditions. Note that the if-then-else formulas can occur in a predicate, procedure, or subroutine context, and the formulas B and C are evaluated in the same context.
proc Fact(x :< L,y :> L) iff
if x > 0 then
y = 1
else
y = x*Fact(x-l)
end
The output variable y is non-local to the if, yet the procedure cannot possibly backtrack.
The following assignment to the variable s is also legal:
if Lookup(persons,'Smith',s) then
Print(s)
else
Print('no such person')
end
The reason for this can be seen from the equivalent formula:
Lookup(persons,'Smith',s) & Print(s) |
~Lookup(persons,'Smith',s) & Print('no such person')
Note that the assignment to s remains local both to the left argument of the or and to the negation.
This kind of assignment is used to advantage in many search situations.proc P4(personsl :< list Person, persons2 :< list Person, s :> L) iff
Lookup(personsl,'Smith',s) | Lookup(persons2,'Smith',s)
or by the procedure
proc P4(personsl :< list Person, persons2 :< list Person, s :> L) iff
if Lookup(personsl,'Smith',s) then
true
else
Lookup(persons2,'Smith',s)
end
Neither of these procedures is accepted by FormulaOne because of the non-local assignments to the output
variable s which occurs within conditions. Such assignments generally call for a backtrack.
Consider the logically true predicate call:
P4((('Smith',45000),Nil),(('Smith',56000),Nil),56000)
The call is compiled as:
P4((('Smith',45000),Nil),(('Smith',56000),Nil),s) & s = 56000
Backtracking is required in order for the formula to succeed. This is because the call
returns s = 45000 which fails the test.pred P4(personsl :< list Person, persons2 :< list Person, s :> L) iff
Lookup(personsl,'Smith',s) | Lookup(persons2,'Smith',s)
The second procedure P4 cannot be turned into a predicate because the conditions of
the if-then-else formula are processed in the procedural mode without non-local assignments.
Note that the seemingly equivalent procedure
proc P4(personsl :< list Person, persons2 :< list Person, s :> L) iff
if Lookup(personsl,'Smith',ss) then
s = ss
else
Lookup(persons2,'Smith',s)
end
is accepted by the compiler of FormulaOne as perfectly legal. This is because the variable ss is local to
the first branch of if. Non-local assignments to the variable s occur in situations after the
condition has been either positively or negatively evaluated and there is no possibility of backtracking.Lookup(personsl,'Smith',ss) & s = ss | ~Lookup(personsl,'Smith',ss) & Lookup(persons2,'Smith',s)The call
P4((('Smith',45000),Nil),(('Smith',56000),Nil),s) & s = 56000
cannot succeed because the Smith in the first list does not make 56000, and the branch
searching the second list cannot succeed because the formula ~Lookup(personsl,'Smith',ss) is false,
i.e. there is a Smith in the first list.if A then B endhas the same meaning as the formula
if A then B else true endor as the formula
A & B | ~AThe formula
if A then
B
elsif C then
D
else
E
end
has the same meaning as the formula
if A then
B
else
if C then
D
else
E
end
end
or as the formula
A & B | ~A & (C & D | ~C & E)
proc Printfile(f:.Ascii) iff
if DbAccess(f,s) then
Print(s,'\n') & DbSkip(f,1) & Printfile(f)
else
Print ('---- EOF -----')
end
Let us assume that the file Myfile is to be of type Ascii. The
query Printfile(Myfile) automatically opens the file Myfile before the file is passed to
the procedure Printfile for the printing.Printfile('sys\\textfile.doc')
prints the Ascii file textfile.doc in the directory sys. The compiler inserts automatically the conversion
from a string constant to the file typed argument. If the file name is given by a variable of type S
then an explicit cast to the type Ascii is required:
subr Printfiles(fs :< list S) iff
if fs = f,fs2 then
Print('-------- ',f,' ---------\n') &
Printfile(f:Ascii) & Printfiles(fs2)
end
The subroutine Printfiles prints the contents of the Ascii files specified by a list of strings as
the argument. The compiler of FormulaOne automatically inserts a call in the body of Printfiles
to open and close the Ascii file:
{open the file f} Printfile(f:Ascii) {close the file f}
Note that the conversion between a file name and a file typed value always means the insertion of the
opening and closing code. In the following query the file text.txt is opened twice:
f = 'text.txt' & Printfile(f:Ascii) & Printfile(f:Ascii)The query
Printfile2('text.txt') calling the subroutine Printfile2 should be used instead:
subr Printfile2(f:.Ascii) iff
Printfile(f) & Printfile(f)
All implementations of Prolog (except Turbo-Prolog) use the so-called tagged architecture for the data structures. This means that every object manipulated by the interpreter (even a simple integer) must be supplemented by a tag giving the type of object. Tagged architecture slows down the execution of programs because the run-time system must constantly test the tags. On the other hand the tagged architecture makes it easy to implement garbage collectors.
Turbo-Prolog and FormulaOne are typed languages and there are no run-time tags on the data structures. Turbo Prolog has no garbage collector.
Example:
Create and call an external API returning the current system time.
FormulaOne code:
Time = hour:[0..23],minute:[0..60],second:[0..60],millisecond:[0..1000]
subr PrintTime() iff TimeGetTime(t) & Print('TimeGetTime returned: ',t)
subr TimeGetTime(t:>Time) iff external _cdecl 'extf1.dll':'GetTime'
External module ‘extf1.dll’ code:
#include <windows.h>
typedef struct
{
int hour;
int minute;
int second;
int millisecond;
} TIMEST,*TIMEPT;
__declspec(dllexport) int __cdecl GetTime(TIMEPT *timept)
{
static TIMEST timest;
SYSTEMTIME SystemTime;
GetLocalTime(&SystemTime);
timest.hour = SystemTime.wHour;
timest.minute = SystemTime.wMinute;
timest.second = SystemTime.wSecond;
timest.millisecond = SystemTime.wMilliseconds;
*timept = ×t;
return TRUE;
}
button.
or Compile and Run, toolbar buttons.
toolbar button.
We also use the convention that anything enclosed within roman-font square brackets ([...]) is an optional element, that can be left out. This is not to be confused with the typewriter-font square brackets ([...]), which indicate actual square brackets as typed into a program.
See BNF-format for precise syntax of FormulaOne. BNF-format presents the syntax less formally for purposes of readability.
{Examples of comments: }
{This is a multiline comment:
line 1
line 2
// } this end of comment not visible by the preprocessor!
} // This is the real end of the multiline comment
// This line is commented out
Pi = 3.14158 // We need to fix this
| all | one | min | max | in | true | false |
| list | pred | if | then | else | elsif | end |
| iff | file | local | pred | proc | subr | mod |
| rel | use | external | case | of |
| Nil | Dupl | Pause | Len | Append | |
| I | L | R | S | P | U |
The output of the query is a list of the possible values of the vars listed. If no results clause is given, or no vars are listed, then the values of all variables appearing in the query are listed.
If results is all, all solutions are listed; if it is one, only the first solution found is listed; if it is min, only the solution of the minimal value is listed; if it is max, only the solution of the maximum value is listed.If output is a database file name, the output is written to the database file; whatever was in the file before is destroyed. Otherwise, output is in results-window format. If output is a string constant, that string is taken as a file name and the output is written to a file. If no in clause is given, or the entire results clause is omitted, output is to the results window.
FormulaOne permits redirection of results of a query to a database file or to an Ascii file in the predicate mode; and to an Ascii file in the subroutine mode. The complete syntax of queries is as follows:If the list of variables vari is given, only the variables specified in the list are displayed on the screen or are redirected to the file. If the list is not given, all the variables occurring in the query are displayed or redirected.
In the following example, the query does not contain a list of variables:in 'myfile' Process()The procedure Process can contain calls to other procedures (such as Print) and the output will be redirected to the Ascii file called 'myfile'.
Each type, constant, and predicate declared is visible to the entire program module. Each is also visible to other program modules which use the module, unless the declaration has been preceded by the keyword local.
Examples:
Weight_t = I Complex_t = (R, R) Tree_t = Nulltree | Node(val:I, l:Tree_t, r:Tree_t)
Pi :< R = 3.14159265358979 Answer :< I = 42 One_tree :< Tree_t = Node(Answer, Nulltree, Nulltree) Name :< S = 'Call me Ishmael' Fact10 :< I = 10*9*8*7*6*5*4*3*2*1 List10 :< list I = 1,2,3,4,5,6,7,8,9,10,Nil
If class is proc (procedure) or subr (subroutine), then none of the formal parameter declarations can have symbolic mode; if the body is a formula, it cannot contain any symbolic variables, or's, or calls to true predicates, except within an all formula. In addition, if class is proc and the body is a formula, it cannot contain any calls to subrs.
In a local variable, the possible values for the variable are generated automatically by backtracking at the point of declaration, if it can have only a small finite number of values. Local input variables can therefore appear only in true predicates.
Format 2:var is declared to be an output variable of the given type. The parameter or variable has no value when the predicate is entered, but must obtain a value before it is exited, at the time of its first use. If it is given a value in one branch of an if, case, or or formula, then it must be given a value in branches of that formula. If the first use of the variable is not as an argument to another predicate in the position of an output parameter, or in an equality formula in which it is assigned a full value, then the possible values are generated automatically at its first use, if it has a small finite number of possible values.
Format 3:var is declared to be an symbolic variable of the given type. It is not known at compile time whether the parameter or variable has a value at any particular point in the predicate, although at run time this is known. If a symbolic variable has no value, the running program will keep track of all the constraints put on that variable by previous formulas, such as that it is equal to another variable, that it is less than some expression, etc. If it can deduce from the constraints that it can have only one value, the program will assign it that value; if it can deduce that it cannot have a value, the program will make a failure backtrack.
Format 4:var is declared to be an input/output variable of the given type. In a parameter, this means that the variable has a value when the procedure is entered (in the same way that an input variable does). However, an input/output parameter can be assigned a new value during the course of the predicate, by the := operator (see section 21.6, Formulas), or by passing it as an argument to an output or input/output parameter. The new value, if one has been given, is returned to the calling predicate at the end of the predicate execution. A local input/output variable acts as an output variable in that it must be assigned a value on its first use. But it can also be passed as an output or input/output argument, and reassigned with the : = operator.
If a variable var is declared to be of a named tuple type, then the terms var.var1 through var.varn are valid terms, and refer to the particular parts of the value of var.
Examples:Date_t = (year:I, month:[1..12], day:[1..31]) Complex_t = (R, R) Person_t = (name:S, age:I, birthdate:Date_t)
A union type expression is a series of two or more variant type expressions, separated by bars. Each variant represents one structure which a variable of that type can have. The Name of the variant is called the variant tag, and the tuple in the variant, if it exists, is called the variant tuple. A term of the type above is a term of the form Name, if Name is one of the variants with no tuple, or of the form Name(term), if Name is one of the variants with a tuple and term is of that tuple type.
The variant tuples can contain fields of the type being declared. Such unions are called recursive unions. Unions with no tuples in any of their variants are called enumerated types.Examples:
Colour_t = Red | Yellow | Green | Blue Vehicle_t = Tricycle | Car (doors: I, engine_size: I ) | Bicycle(gears: I ) | Motorcycle Tree_t = Nulltree | Node(I, Tree_t, Tree_t)
Format 2:
A variable of an array type is a set of values of type type2 indexed by members of type type1. The first form given above is called a simple array; the second form is called an injection. If type1 is [0..], then the array is flexible, meaning that its number of elements is determined only at execution time; otherwise, the array has a fixed number of elements.
An array constant of either of the array types above is of the form [term1term2, ...,termn]. Unless the array is flexible, n must equal the number of elements in type1.If a variable, say x, is declared to be of one of the array types above, then the term x(term), where term is of type type1; is a valid term. This term is of type type2. An injection is identical in use to a simple array; however, variables declared to be injections have the additional constraint that no two members of the array can have the same value.
Examples:Persarr_t = [0..33] -> Person_t Matrix_t = [0..2] -> [0..3] -> I Wavelength_t = Colour_t -> R Dperm_t = [0..9] ->> [0..9]
Posint_t = [1..] Digit_t = [0..9] Water_liquid_t = [-32..212]
A variable of the list type above can take on the value Nil, or any value consisting of a term of the given type paired with another term of the list type; that is, Nil or any term of the form (term1, term2,..., termn, Nil) where term1 .... termn are terms of the given type. Nil is a special reserved name which has no fixed type of its own, but can be used as a term of any list type.
Examples:Guests_t = list Person Sum_t = list I Csum_t = list (R, R)
A variable var declared to be of the above relation type stands for a property of terms of the type. It can be used in declared relation formulas of the form [~] term in var, where term is a term of the given type. This denotes that a term of the given type has the property represented by var.
A variable of a relation type can only be passed as a parameter and used in declared relation formulas. There are no terms of any relation type, except variables declared to be of that type. Examples:Ismale_t = rel Person_t Isprime_t = rel I
A parameter of the above type stands for an ordered list of the given type, represented on external storage. Such a variable can be passed to the file procedures, or used as a predicate.
Constant terms of the file types . Also, any string containing a file name is a file constant, which can be passed as an argument to a parameter of type Ascii, pr Bin. This latter kind of file constant can be coerced into type Ascii or Bin when being passed to the various database polymorphic procedures in F1RTL (FormulaOne Run Time Library). File constants can appear only in queries. Examples:P_data_ft = file P_data_t Marriage_ft = file (husb:P_data_t, wife:P_data_t) Lasttag_ft = file Tag_t
| Operator | Precedence | Associativity |
| * | 4 | Left |
| / | 4 | Left |
| mod | 4 | Left |
| + | 3 | Left |
| - (binary) | 3 | Left |
| - (unary) | 2 | Left |
| , | 1 | Right |
Here integral means L, I, or a subrange type; and arithmetic means either integral or R. Most of these operators have the obvious meanings. "-" can be used both as a binary operator, meaning the difference between the two terms, or as a unary operator, meaning the negative of the term, mod is the modulo or remainder operation, which results in the remainder upon division of the left-hand term by the right-hand term.
The "," operator is the data constructor operator of pairing. It is analogous to the CONS function of LISP. If term1 is of type1 and term2 is of type2, then the pair term (term1, term2) can be of type (type1, type2).We encourage programmers to use parentheses in terms with many operators, to make it clear which operators go with which terms. However, if no parentheses are supplied, FormulaOne parses terms by rules of precedence.
Each operator has a precedence and an associativity, given by the table above.If a term is flanked by two operators of unequal precedence, it is bound more strongly by the higher-precedence one; thus
x + y * z, - 5is parsed as
((x + (y * z)), (-5))If a term is flanked by two operators of equal precedence, it is bound more strongly by the left-hand one if they are left-associative, the right-hand one if they are right-associative; thus
x * y * z, a - b + c, 99is parsed as in the Operators and Their Syntactic Properties table below.
(((x * y) * z), (((a - b) + c), 99))
| Operator | Meaning | Arity | Argument Type | Resultant Type |
| * | multiplication | binary | arithmetic | arithmetic |
| / | division | binary | arithmetic | arithmetic |
| mod | modulo | binary | integral | integral |
| + | Addition | binary | arithmetic | arithmetic |
| - | Subtraction | binary | arithmetic | arithmetic |
| - | Unary minus | unary | arithmetic | arithmetic |
| , | pairing | binary | any | any |
Examples:
8*s + 6*b
('Heather', Female,
(1921 + 40, 7, 2), (0, 1, 1), 'Musician')
The constant is of type I if it is between -2147483648 to 2147483647, and of type L otherwise.
Examples:-32760 1066 10000000000000000000000000000
The e part of a real constant stands for the exponent of the power of 10 by which the numeric part is to be multiplied. For example, the constant -9.99e50 stands for -9.99 * 1050, and the constant 0.0005e-6 stands for 0.0005 * 10-6.
Examples:3.1415926 -22.0 -9.99e50 0.0005e-6
'A B C D ' 'The word ''word''' '10.aaa99'
"Q" "t1 """"""" "j"
term1, term2,...., termn are terms of the same type type.
If type2 is an array index type with n elements, then the given term can be used as a term of typeThat is, the term stands for an entire array, each termi standing for the element of the array subscripted by one of the n terms of type2.
Examples:['Sally','Heather','Isadora'] [0,0,0,0,7] [[7,6],[3,5,9],[4,8,2],[1,2,3,4]]
Fib200 :< L = 280571172992510140037611932413038677189525 Beatle :< S = 'John Lennon' Pi :< R = 3.14159
A parameter of the above type stands for an ordered list of the given type, represented on external storage. Such a variable can be passed to the file procedures, or used as a predicate.
Constant terms of the file types. Also, any string containing a file name is a file constant, which can be passed as an argument to a parameter of type Ascii, pr Bin. This latter kind of file constant can be coerced into type Ascii or Bin when being passed to the various database polymorphic procedures in F1RTL (FormulaOne Run Time Library). File constants can appear only in queries. Examples:P_data :< P_data_ft = 'pdata.dbs':P_data_ft Marriage_ft = file (husb:P_data_t, wife:P_data_t) Lasttag_ft = file Tag_t
Variables or constants followed by a sequence of zero or more such operators are called extended variables. Note that the term 'extended variable' includes all variables and constants themselves.
The term, in this kind of extended variable, is called the index of the array. If the index is not of the index type of the array, and cannot be coerced into that type, the formula containing the term will fail. The resulting extended variable is of type typej, and refers to the term-th element of the array extvar.
Strings can also be indexed. The index must be an integer greater than or equal to 0 and less than the length of the string. Such an extended variable stands for the term-th character in the string (numbered starting at zero), and is of type I.If extvar is also an array element term, the consecutive index expressions (x)(y) can be grouped together in a single set of parentheses, separated by a comma, as (x, y).
Examples:pers_arr(0) sieve(curr) matrix(i)(j) matrix(i, j)
Again, the resulting extended variable is of that type, and refers to that field. When such an extended variable is used, a test is implicitly inserted that the variant named by Name is the one in the value of extvar.
For example,extvar.var = 0would be equivalent to
extvar= Name(x) & x.var = 0.Examples:
p_data.name p_data.b_date.month curr vehicle.doors
The anonymous variable is useful in matching parts of a larger term which the programmer does not need to refer to later. It acts as a placeholder whose matched value is immediately discarded.
Examples:
Tricycle
Nulltree
Node(0, left_tree, Nulltree)
P(R(0), S('wacka'))
All but the last of the formal parameters to the procedure must be of input mode, and the last must be of output mode. The value of the term is the value that z would have after the following procedure call (assuming that z had not been assigned a value before):
x = Sum((3, 7, 3, 2, 6, 87, 4, Nil)) y = Fib(GCD(42, 6*9) + 4) z = Youngest(pers, arr)
Since different types represent different subsets of the universal type U, it may not always be possible to cast a given term into a given type. If it is not, the formula containing the term will fail and cause a backtrack.
Examples:curr_colour :L Print(foo:U) 'abcd':list I [4, 5, 6]:[0..]->I:list Ithe string 'abcd' is directly typecasted into the type list I, resulting in the list of integers
97,98,99,100,NilIn the last example term [4, 5, 6] is first typecasted into an array of integers and subsequently typecasted into a type list I. Result would be a list of integers:
4,5,6,NilConsider the following code fragment
AR = [0..]->[0..]->R
LS = list (list I)
LCONST :< LS = (1,2,3,4,Nil),(5,6,7,Nil),(15,Nil),Nil
proc Cast(x :< LS) iff
y = x:AR & Print(y)
Running the query
Cast(LCONST)
will result in printing
y = [[1.,2.,3.,4.],[5.,6.,7.],[15.]]
thus converting a list of list I into an array of arrays of R. Several conversions were carried out simultaneously.
First, each element of the list LCONST, itself a list I, was converted into an array of I, and subsequently each
element of the array was converted into a real number, R. This conversion was repeated for each element of the list LCONST.
At this point a list of arrays of R was constructed, and the list was then converted into an array of arrays, the
final value being assigned to y.In the Processing sections, we assume the existence of a query pointer pointing to the current position in the formula being processed, and an environment containing all constraints and other information about the current values of variables. Backtrack points and their corresponding skip points are sometimes set up during the course of processing.
When the query pointer is advanced to a backtrack point, it is skipped to the corresponding skip point. The operation of backtrack is assumed to mean the following: the query pointer is reset to the last backtrack point set up, it and its corresponding skip point are deleted, and everything in the environment from the time the backtrack point was set up is removed.true is always true; false is always false.
Processing:When the query pointer reaches true, it passes over it with no change to the environment. When it reaches false, a backtrack is performed.
Thus, the formula
P & Q | ~P & ~Qwould be treated exactly like
(P & Q) | ((-P) & (-Q))
When the query pointer reaches A & B, it is advanced through A normally and then through B normally.
Examplesx :: L & x = 3 Fib(3, x) & Print (x)
formula1 | formula2 is true if either formula1 or formula2 are true.
Processing:When the query pointer reaches A | B, a backtrack point is set up just before B, with the corresponding skip point just after B. Then the query pointer is advanced normally through A.
Examplesx = 4 | x = 5 (x <= 1 & y = 1) | (x > 1 & y = x*Fact(x-l))
~formula is true only if formula is false.
Processing:~formula is completely equivalent to the following if formula:
if formula then
false
else
true
end
Examples:
~Longname('Smith')
~DbEof(p_data_file)
An if formula is true if both its condformula and its thenformula are true, or if its condformula is false and its elseformula is true.
Processing
When the query pointer reaches an if formula, the condformula is tested, as if it were a separate query. If it succeeds, the entire if formula is effectively replaced by the thenformula, and the query pointer is set to the beginning of that formula; if it fails, the formula is replaced by the elseformula and the pointer is set there.Format 2
Format 3
Examples
if l = Nil then
sum = 0
else
l = (h, t) & sum = h + Sum(t)
end
...
if n < 0 then
f = 0
elsif n <= 1 then
f = l
else
f = n * Fact(n-l)
end
Where:
The FormulaOne compiler must be able to deduce that at least one case term must match the subject term. For example, if the subject term is of a union type, the case terms must include all members of that type, unless an else clause is included. The case terms must be mutually exclusive: no two case terms can be such that a subject term can match both of them.
The subject term must be full-value, and must be of a union, subrange, string or list type. The case term must be of the same type as the subject term, but can contain variables.Meaning:
A case formula is true if the subject term is equal to one of the case terms, and the corresponding case conclusion is true; or if the subject term is not equal to any of the case terms, and the else formula is true.Processing:
When the query pointer reaches a case formula, the subject term is matched against each of the case terms, as if the formulasubjectterm = casetermwere being evaluated. When one of these matchings succeeds (possibly altering the environment), the entire case formula is effectively replaced by the corresponding case conclusion formula, and the pointer is set to the beginning of that formula.
Examples:
case digit of
0 => name = 'zero';
1 => name = 'one';
2 => name = 'two';
3 => name = 'three';
4 | 5 | 6 => name = 'several'
else name = 'many'
end
case string of
'John' => name = 'Lennon';
'George' => name = 'Harrison';
'Paul' => name = 'McCartney';
'Ringo' => name = 'Starr';
else name = 'not a Beatle'
end
Meaning:
An all formula is true ifThe formula is processed as a sub-query. Each solution of the var^s is obtained in turn and inserted into the file (or into memory, for lists) in sorted order.
Examples:
all x in men_file
P_data(x) &
x = (_, Male, _, _, _)
end
all x, square, cube in triple
x::[1..20] &
square = x * x &
cube = x * square
end
The two terms related by the first six operators must normally be of the same type, though they can sometimes be different; see the section on automatic mode coercion. The right-hand term of an in formula must be of a relation, list, or file type; the left-hand term must be of the element type of the right-hand term.
The first four relational operators can be used only between terms of a type which is ordered (that is, I, L, R, S, or a subrange or enumerated type).Meaning:
The first six relational operators have the obvious meaning: that the left-hand term is in the given relation with the right-hand term, in means that the left-hand term is a member of the right-hand term (if it is of a relation or list type) or is a record in the right-hand term (if it is of a file type).Processing:
When the query pointer reaches a relational operator formula, the system tries to integrate the information in the formula into the information in the environment. If the new formula is inconsistent with the environment (for example, x = 1 when the environment contains x = 0), a backtrack is performed.If all the variables in the formula are full-value, the formula will act as a simple test. Otherwise, the new formula may act as an assignment of a value to a variable, or it may cause new constraints to be put into the environment. This may in turn cause previous constraints to be eliminated, or cause symbolic, or output variables to obtain values where they had none before.
Examples:
name = 'zero'
8*3 + 6*b <= 46
p_data = ('Sally', Female, (1957, 10, 6), (0, 1, 1),'')
sally_p_data in guests_r
No matter what the value of the extvar was beforehand, its value becomes the value of term. If extvar is a field-selection or element-selection term, only that part of the variable is changed. Syntactically, if a formula contains var := term, all references to var after it in the formula will effectively refer to an auxiliary variable which has the value of term.
Processing:The value of the extended variable in the environment is reassigned to the value of the term.
Examples:vehicle_arr(3).doors := Default_doors iosum := iosum + 5 error_s := 2
Database files which are declared as being used by a module can be used as predicates within the module. In this case, the formal parameters are the fields of the tuple which was used to define the records in the file.
Meaning:For program predicates, the predicate call is true if and only if the defining formula of the predicate is true when the formal parameters are given the values of the arguments. For database-file predicates, the call is true if and only if the list of arguments is equal to one of the records in the file. If only one argument is given, it must be a tuple variable equal to one of the records.
Processing:When the query pointer reaches a predicate call, the call is expanded into the defining formula of the predicate, with each parameter replaced by the corresponding argument. Every local variable of the predicate which has the same name as a variable already in the environment, is renamed to some new name throughout the expanded formula. For database-file predicates, a call is processed by scanning the file and trying to match the argument list to a record.
Examples:Sum((3, 2, 6, Nil), s) Print( 'Foo' ) DbInsert(x, tree. left) P_data(rec)
Meaning:
A variable declaration is true if the variable has a value which is of the type given in the declaration.Processing:
When the query pointer reaches a variable declaration, information about the type and mode of the variable is put into the environment. It is also used extensively by the FormulaOne compiler in checking programs and queries for correct format.Examples:
x :< I tree :. Tree reversed :> list U
Query ::= [ all | one | min | max ]
[ Var { , Var } ]
[ in [ Ident ] String ] ]
Formula
[end]
Prog ::= { Typedecl | Constdecl } { Pred }
Formula = Formula2 { "|" Formula2 }
Formula2 = Formulas { & Formulas }
Formula3 = If | Case | Else | false | true | ~Formula3 |
Call | Term Oper Term | ( Formula ) | Vdecl
Oper = < | > | <= | >= | <> | = | := | in
Call = Ident ( Term ) |
If = if Formula then Formula
{elsif Formula ->Formula} }
[ else Formula ]
end
Case : = case Term of
Term { "|" Term } => Formula
{ ; Term { "|" Term } => Formula } [ ; ]
[ else Formula ]
end
all ::= all Var { , Var } in Var Formula end |
[ one | min | max ] Var { , Var } Formula end
Term ::= Term1 [ ,Term ]
Terml ::= [ - ] Term2 {Addop Term2 }
Addop ::= + | -
Term2 ::= Term3 { Multop Term3 }
Multop ::= * | / | mod
Term3 ::= _ | Ident | Call | Number | String | Charconst |
Selection | ( Term ) | Array | Term3 : Type
Selection ::= [ Var | Ident ] { . Var | ( Term ) }
Array ::= "[" [Term ] "]"
Number ::= DecimalDigit { DecimalDigit } | Radix RadixDigit {RadixDigit}
Radix ::= 0x | 0b | 0o | 0d
String ::= 'Char { Char }'
Charconst ::= " Char "
Type ::= Ptype [ Arrows Type ]
Arrows ::= -> | ->>
Ptype ::= ( Tuple ) | [ Ident ] "[" [ Term ]..[Term] "]" |
list Ptype | rel Ptype | file Ptype | Ident
Tuple ::= Named | Unnamed
Named ::= Var : Type { , Unnamed }
Unnamed ::= Type { , Unnamed }
Vdecl ::= Var Mode type
Mode ::= :< | :> | :.
Typedecl ::= [ local ] Ident = Td
Td ::= Tuple | Union
Constdecl ::= [ local ] Ident :< Type = Term
Union ::= Unionelem "|" Unionelem { "|" Unionelem }
Unionelem = Ident | Ident ( Tuple )
Pred ::= [ local ] Kind Ident ( Vdecl { , Vdecl } ) iff Body
Kind ::= pred | proc
Body ::= Formula | Forwarde
Forwarded ::= external [_cdecl | _stdcall] String : String
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.
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.
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.
These declarations are really pseudo-code, only to indicate approximately how FormulaOne treats the predicates.
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.
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? |
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)
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)
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'
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.
There are two basic places in which mode coercion happens: in identity formulas and in predicate calls. In the descriptions that follow, we assume that all necessary type conversion has already taken place.
Any full-value term (any term made up only of constant terms, input variables, initialized output variables, initialized input/output variables, and symbolic variables whose values are fixed as full-value terms) can also be considered an input variable.
If the system attempts to backtrack out a variable and fails, it raises the "too many backtracks" run-time error.
class P(x mode T) iff ...where class is pred, proc, or subr, as appropriate, and mode is the mode of the parameter x. Given a call to this predicate, P(y), what action is actually performed by the call?
Mode coercion on predicate calls table:
| Mode of x (parameter) | Mode of y (parameter) | Action performed |
| input | input | P(y) |
| input | output | z :> T & z = y & P(z) |
| input | symbolic | z :> T & z = y & P(z) |
| input | i/o | z :> T & z = y & P(z) |
| output | input | z :> T& P(z) & y = z |
| output | output | P(y) |
| output | symbolic | z :> T & P(z) & y = z |
| output | i/o | z :> T & P(z) & y := z |
| symbolic | input | z :: T & z = y & P(z) |
| symbolic | output | z :: T & P(z) & y = z |
| symbolic | symbolic | P(y) |
| symbolic | i/o | z :: T& z = y & P(z) |
| i/o | input | z :. T & z = y & P(z) |
| i/o | output | z :. T & z := y & P(z) |
| i/o | symbolic | z :. & z := y & P(z) |
| i/o | i/o | P(y) |
If the relational operator formula is not in the format of a constraint to begin with, it is transformed according to the rules of algebra so that it is. This may require coercing the mode of some symbolic variables to input by backtracking out those variables. If the backtracking-out fails, a run-time error, "Too many backtracks..." is raised, as usual.
The setting of a constraint will cause the relational operator formula to fail if the constraint is not compatible with constraints already in the environment; for instance, x < 3 where x > 4 is already in the environment.The following list summarizes the formats of all possible constraints that can be in the environment, rel here always refers to one of the relational operators (< , > , < =, >=, =,or <>).
al*xl + a2*x2 + . . . + an*xn rel awhere al, a2, ..., an, a are long integer values, and xl, x2, ..., xn are symbolic variables of type L.
x rel awhere x is a symbolic variable of type I, R, S, or a subrange type, and a is some value of the same type.
x rel y + awhere x and y are symbolic variables of type I, R, or a subrange type, and a is a numeric value of the same type.
z(x+a) = ywhere z is a symbolic array, x is a symbolic variable of the index type of z, a is a integer value, and y is a symbolic variable of the element type of z. If a term of the form z(x+a) is used in a relational operator formula, y is implicitly declared, and a constraint of this form is set up. Then y is used in place of the original term in any further constraints.
b in x ~b in xwhere x is a symbolic variable of a relation type, and b is either a value of the element type of x, or a symbolic variable of the element type of x.
x = b x <> bwhere x is a symbolic variable of any type, and b is either a value of the same type, or another symbolic variable of the same type.
The runtime library (F1RTL.DLL) contains routines used directly by the FormulaOne compiler, but also several user accessible APIs. Available APIs can be viewed by expanding the F1RTL.DLL tree in the "Modules" tab.
Execute a system call.
Syntax:
RtlSystem(cmd:<S)
Example:
RtlSystem(‘dir c:’)
Note: use with caution. The system output is redirected to the TTY. Do not use for system calls requiring user input.
Convert an integer number to a decimal string.
Syntax:
RtlLtoS(x:<L, s:>S)
Note: Conversion implicitly assumes a decimal number.
Convert an integer number to a string with specified base.
Syntax:
RtlLtoSx(x:<L,base:<I[2..36], s:>S)
Note: Binary numbers use base 2, decimal numbers use base 10, hexadecimal numbers base 16 etc.
Convert a string in decimal base to a number.
Syntax:
RtlStoL(s:<S, x:>L)
Note: The string must contain only digits 0..9. There is no limit on the string length.
Convert a string representing a number in arbitrary base [2..36] to a number.
Syntax:
RtlStoL(s:<S, base:<I[2..36], x:>L)
Note: The string must contain only alphanumerical characters valid for the required base
Convenience polymorfic API. Reverse a string, array or a list.
Syntax:
RtlReverse(in:<S, out:>S)
RtlReverse(in:<list X, out:>list X)
RtlReverse(in:<[0..]->X, out:>[..]->X)
Note: X can be of any type.
Examples:
Reversed string ‘abcd’ becomes ‘dcba’.
Reversed list el, e2, e3, e4, Nil becomes e4, e3, e2, e1, Nil.
Reversed array [a1,a2,a3,a4,a5] becomes [a5,a4,a3,a2,a1]
Convenience polymorfic API. Sort a string, array or a list in ascending order.
Syntax:
RtlSortAscending(in:<S, out:>S)
RtlSortAscending(in:<list X, out:>list X)
RtlSortAscending(in:<[0..]->X, out:>[..]->X)
Note: X can be of any type.
Examples:
Sorted string ‘bozo’ becomes ‘booz’.Convenience polymorfic API. Sort a string, array or a list in descending order.
Syntax:
RtlSortDescending(in:<S, out:>S)
RtlSortDescending(in:<list X, out:>list X)
RtlSortDescending(in:<[0..]->X, out:>[..]->X)
Note: X can be of any type.
Examples:
Sorted string ‘bozo’ becomes ‘zoob’.Convenience API. Convert an ASCII string to upper case.
Syntax:
RtlToUpperString(sin:<S, out:>S)
Convenience API. Convert an ASCII string to lower case.
Syntax:
RtlToLowerString(sin:<S, out:>S)
Parse a string into individual tokens. The token separators are passed as a string.
Syntax:
RtlParseString(sin:<S, separators:<S, output:>[0..]->S)
Example:
y = RtlParseString('OK,parse this string 1, 2, 3 ,4, 5\n6\t7\t8\n', ' ,\n\t')
Returs:
y = [OK,parse,this,string,1,2,3,4,5,6,7,8]
Retrieve the command line string.
Syntax:
RtlGetCommandLineString(cmdline:>S)
Note: Routine typically used by standalone executables.
Routine parses the command line string and returns an array of strings.
Syntax:
RtlGetCommandArguments(cmdars:>[0..]->S)
Note: Routine typically used by standalone executables.
By using these routines we are able to prematurely terminate any predicate, explicitly cutting off the predicate backtracking branches.
Syntax:
RtlGetCutPoint(cp:>I)
RtlSetCutPoint(cp:<I)
The following code snippet illustrates the typical usage of these routines: terminate
collecting of all results of the predicate MyPredicate if the proc
WantNextSolution fails.
all x in l
RtlGetCutPoint(cp) &
MyPredicate(x) &
if ~WantNextSolution() then
RtlSetCutPoint(cp)
end
end
Note: Use caution when using these routines, as there is no proper argument validation. Incorrect usage will lead to bizarre program behaviour.
Specify the title of the TTY window.
Syntax:
proc TTYSetTitleBar(title:<S)
Note: Typically meant for standalone applications. Replaces the default TTY title as it appears in the TTY window title bar.
Check if any user key input present.
Syntax:
proc TTYKeyHit()
Note: Succeeds if the keyboard buffer is not empty, fails otherwise.
Wait for the user the press a key. The call always succeeds.
Syntax:
proc TTYKeyWait()
Note: This is a blocking call. The procedure will not return until the user presses a key. Since the actual key value is not retrieved, TTYKeyWait is declared as “proc”.
Wait for the user the press a key.The call always succeeds.
Syntax:
subr TTYKeyGet(key:>I)
Note: This is a blocking call. The procedure will not return until the user presses a key. The key value is retrieved.
Wait for the user the enter a string. The call always succeeds.
Syntax:
subr TTYGetString(string:>S)
Note: This is a blocking call. The procedure will not return until the user presses the ENTER key.
Show the console window.
Syntax:
proc TTYShow()
Note: The call allows to display the console previously hidden.
Hide the console window.
Syntax:
proc TTYHide()
Note: The call allows to hide the console at runtime.
Store a record at the current position.
Syntax:
proc DbPut(f:.file T, x:<T)
Current record is accessed and the file is advanced by one record.
Syntax:
proc DbGet(f:.file T, rec:>T)
Retrieve the current record.
Syntax:
proc DbAccess(f:.file T, rec:>T)
Note: fails at EOF, otherwise succeeds returning the current record, does not change the file position
Delete the current record.
Syntax:
proc Delete(f:.file T)
Note: Fails at EOF, otherwise succeeds removing the current record. Aborts when used with Bin or Ascii files.
Syntax:
DbSkip(f:.file T, n:<I)
Fails if n negative, succeeds otherwise advancing the current position by n records or to the end of file if there are not n records left in the file.
Position the file at the beginning, always succeeds.
Syntax:
proc DbRewind(f:.file T)
Test for end of file. Call succeeds if there are no more records left after the current position.
Syntax:
proc DbEof(f:.file T)
Positions the file at the end, always succeeds.
Syntax:
proc DbEofSet(f:.file T)
Truncate the file at the current position.
Syntax:
proc DbTruncate(f:.file T)
Note: for database files, calling this function after DbRewind will delete all database records and indeces, otherwise this call will fail if index files exist.
Flush all modified blocks from the cache-buffers. This procedure is to be used from time to time as a safeguard against a hardware or software malfunction.
Syntax:
proc DbFlush(f:.file T)
Position the DB file pointer to the record containing the key value.
Syntax:
proc DbSeek(f:.IndexFile,keyvalue:<T)
Position the DB file pointer to the record with a greater or equal key value then the current record.
Syntax:
proc DbSeekNext(f:.IndexFile)
Note: Assumes a previous call to one of DbSeekFirst, DbSeekLast, DbSeek.
Position the DB file pointer to the next record containing the same key value as the current record.
Syntax:
proc DbSeekNextEq(f:.IndexFile)
Note: Assumes a previous call to one of DbSeekFirst, DbSeekLast, DbSeek.
Position the DB file pointer to the record with a greater key value then the current record.
Syntax:
proc DbSeekGt(f:.IndexFile)
Note: Assumes a previous call to one of DbSeekFirst, DbSeekLast, DbSeek.
Position the DB file pointer to the record with a lesser or equal key value then the current record.
Syntax:
proc DbSeekPrev(f:.IndexFile)
Note: Assumes a previous call to one of DbSeekFirst, DbSeekLast, DbSeek.
Position the DB file pointer to the previous record containing the same key value as the current record.
Syntax:
proc DbSeekPrevEq(f:.IndexFile)
Note: Assumes a previous call to one of DbSeekFirst, DbSeekLast, DbSeek.
Position the DB file pointer to the record with a lesser key value then the current record.
Syntax:
proc DbSeekLt(f:.IndexFile)
Note: Assumes a previous call to one of DbSeekFirst, DbSeekLast, DbSeek.
Position the DB file pointer to the first record (leftmost node) as sorted by the index file. DB file pointer position is set to the record containing the smallest value of the index file key.
Syntax:
proc DbSeekFirst(f:.IndexFile)
Position the DB file pointer to the last record (rightmost node) as sorted by the index file. DB file pointer position is set to the record containing the largest value of the index file key.
Syntax:
proc DbSeekLast(f:.IndexFile)
Last updated: August 14, 2006