FormulaOne Programmer's Manual

This file documents the use of the Formula One compiler.
Copyright © 2003, 2004, 2005, 2006, 2007, 2008 K2 Software Corp.

About This Document
Preface
What Is Formula One
FormulaOne and Other Languages

Formulas and Queries
  • Simple Arithmetic Queries
  • Some Formal Definitions
  • "How It Does It"
  • The Print Formula

Predicates
  • Predicates and Modules
  • A Simple Predicate Definition
  • Reading Predicate Calls
  • Variables
  • Calling Predicates in Predicates
  • More Formal Definitions

Data Types
  • Why Types?
  • Variable Declarations
  • Integers
  • Long Integers
  • Real Numbers
  • Strings
  • The Pairing Operation
  • The FormulaOne Universe
  • Subranges
  • Lists

Modes
  • Symbolic Mode
  • Input Mode
  • Output Mode
  • Mode Clash

Control Structures
  • The if Formula
  • Alternate Forms of if
  • The case Formula
  • Iteration

Procedures, Subroutines and Functions
  • Predicate Classes
  • Procedures
  • Subroutines
  • Input/Output Mode
  • Queries Revisited
  • Functions

Building Types
  • Type Declarations
  • Tuples
  • Field Selection Terms and Deconstructors
  • Enumerated Types
  • Unions
  • The Universal Type
  • Type Conversions
  • Arrays
  • Array Constants and Initializing
  • Flexible Arrays

Database Files
  • Database Files in FormulaOne
  • Files as Variables
  • Reading Database Files
  • Positioning the File Pointer
  • Altering Database Files
  • Database Files as Predicates
  • Index Files
  • Manipulating Files

Collecting Solutions with "all"
  • The all Formula
  • all, one, min and max Formulas
  • The Standard Order for Sorting
  • The Whole Truth about Queries
  • Query Output to Database Files

Miscellaneous Advanced Topics
  • Constant Declarations
  • The Anonymous Variable
  • Scope of Variables
  • The local Keyword
  • Unnamed tuples
  • Injections, Relations, and Unknown Indices
  • Injections
  • Relations
  • Unknown Indices
  • Construction and Deconstruction of Arrays, Tuples, Lists and Unions
  • Tail Recursion Elimination
  • Negation
  • More About if-then-else Formulas
  • Opening and Closing of Files
  • Cross Modular Consistency Checks
  • Heap Management
  • External Modules

Queries

FormulaOne Language Definition
  • Comments
  • Identifiers
  • Reserved Words
  • Queries
  • Overall Module Structure
  • Type Declarations
  • Constant Declarations
  • Predicate and Variable Declarations
  • Predicate Declarations
  • Variable Declarations
  • Types
  • Tuples
  • Unions
  • Array Types
  • Subrange Types
  • List Types
  • Relation Types
  • File Types
  • Terms
  • Complex Terms
  • Constant Terms
  • Integer Constants
  • Real Constants
  • String Constants
  • Character Constants
  • Array Constants
  • Declared Constants
  • Variables
  • Extended Variables
  • Array Element Selection
  • Field Selection
  • Anonymous Variable
  • Union Terms
  • Function Calls
  • Type Casts
  • Formulas
  • Truth Values
  • Logical Connectives
  • if Formulas
  • case Formulas
  • all Formulas
  • Relational Operators
  • Assignment Formulas
  • Predicate Calls
  • Variable Declarations as Formulas

BNF Syntax of FormulaOne

Type Conversion
  • Legal Type Casts
  • Automatic Type Coercion
  • Polymorphic Predicates
    • Print
    • Len
    • Append
    • in
    • Dupl
    • _AllDifferent
    • _AllAscending
    • _Ascending
    • _AllDescending
    • _Descending

Mode Coercion
  • Identities
  • Predicate Calls

Constraints
Runtime Library
  • RtlSystem
  • RtlLtoS
  • RtlStoL
  • RtlLtoSx
  • RtlStoLx
  • RtlReverse
  • RtlSortAscending
  • RtlSortDescending
  • RtlToUpperString
  • RtlToLowerString
  • RtlParseString
  • RtlGetCommandLine
  • RtlGetCommandArguments
  • RtlGetCutPoint
  • RtlSetCutPoint
  • TTYSetTitleBar
  • TTYKeyHit
  • TTYKeyWait
  • TTYKeyGet
  • TTYGetString
  • TTYShow
  • TTYHide
  • DbGet
  • DbAccess
  • DbSkip
  • DbRewind
  • DbDelete
  • DbEof
  • DbEofSet
  • DbTruncate
  • DbFlush
  • DbSeek
  • DbSeekGt
  • DbSeekLt
  • DbSeekNext
  • DbSeekNextEq
  • DbSeekPrev
  • DbSeekPrevEq
  • DbSeekFirst
  • DbSeekLast

About This Document

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.

Preface

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.

What Is FormulaOne?

FormulaOne is a computer programming language, but it's also a complete programming environment that gives programmers the ability to efficiently develop, test and run their programs. At the heart of FormulaOne is the language itself, which can be viewed as a successor to the procedural language of the third generation Pascal, extended to cover the paradigms of database languages (fourth generation) and logic languages (fifth generation).
FormulaOne has the readability and efficiency of third-generation languages like BASIC, C, and Pascal, and the database update and query capabilities of fourth-generation systems. These features are all brought together by the powers of symbolic computing and logic programming with backtracking search - the same power as in fifth-generation languages like Prolog. Along with the FormulaOne language comes a complete visually oriented IDE environment. In the FormulaOne system, users can edit, compile, and run programs; build, query, and update database files; and create interlocking structures of program modules and databases of any desired complexity.

FormulaOne and Other Languages

FormulaOne is a new programming language, so it's useful to compare and contrast it to other popular programming languages. The foundations of FormulaOne are most like those of Prolog. Both languages:
  • Are based on mathematical logic, and have a precise declarative semantics (a static, clearly-defined meaning for every component of the language)
  • Have programs which are run by asking questions rather than giving commands;
  • Are able to handle symbolic variables, whose values are determined by backtracking search.
  • However, FormulaOne recognizes the deficiencies of Prolog in areas where languages like Pascal do better.

Both FormulaOne and Pascal:
  • Have a clear but concise nested program structure, rather than the difficult-to-read clauses of Prolog;
  • Have if and case constructs that improve readability;
  • Can produce fast, compact, non-backtracking code when desired.

But the type structure of FormulaOne is more like that of C than the loose structure of most prologs or the rigid one of Pascal or Turbo Prolog. In FormulaOne, you can build arrays, structures, lists, and unions which are implemented as efficiently as they are in C. And as in C, terms of one type can be recast into terms of another type, when possible. FormulaOne also has many advanced features which are not found in either Prolog, Pascal or C. These include:
  • A leading-edge decision procedure for systems of constraints composed of arithmetic formulas, built into the language itself;
  • A database file query system which is fully integrated with programs;
  • Variable modes, which allow the language to check the data flow in programs for correctness;
  • Useful data types not found in most languages, such as relations and injections;
  • A module system which supports incremental compilation, linking, and loading of program modules.

In addition to all this, FormulaOne is firmly grounded in its underlying logic. Instead of the non-declarative, extra logical features of Prolog, like "cut", there are features like "if" which are more powerful, readable, and logically valid. There is not a single extra logical feature in FormulaOne.

Formulas and Queries

FormulaOne is different from other programming languages, and systems, in many ways. In well-known languages like Basic and Pascal, we order the computer to perform some task for us, and watch the results. In FormulaOne, we ask the computer questions and get responses.
The basic unit of programming in FormulaOne is the formula. A formula is a statement about the world, phrased in a language similar to mathematical logic. When we enter a formula into the query window of the FormulaOne system, it is interpreted as a query; the system will respond by stating whether the query is true, or by stating the conditions under which it's true.

Simple Arithmetic Queries

The simplest example of a query formula is an arithmetic statement. When we say 2 + 2 = 4 or x = 3, we are making a statement about the numbers and variables involved. In general, a formula is a statement, which says something about objects (like numbers), variables, and the relationships they hold to one another.
When we type in an arithmetic formula as a query to FormulaOne, we are asking it to tell us whether the formula is true or false, according to what it knows about arithmetic. For instance, you can ask FormulaOne whether 2 + 2 = 4 by the following steps:
  • Start up the FormulaOne and open project 'Tutorial'.

  • Open query tab pressing [image] and type 2 + 2 = 4 into the query window.
  • Compile and run the query by pressing [image] button.

Note: Newer compilers can determine an expression to be true or false at compile time and subsequently issue a corresponding warning. Additionally, newer compilers can also treat warnings as errors. If this happens, go to "Project->Settings" and uncheck "Treat warnings as errors".

The result will be displayed in the window:

that is, FormulaOne believes it to be true, which is of course correct. Now try to run 2 + 2 = 5 query instead, it will give us Failure result instead of Success. After the Success, or Failure comes some statistics on how long the query took to run.
FormulaOne can tell you whether an arithmetic formula is true or not. But more importantly, if you pose a query containing variables, FormulaOne will try to find values for those variables which will make the query true, and will report to you what those values are. Consider the following example:

The phrase all res indicates to the system that we want to see all the solutions for the unknown variable we are calling. res::L is a variable declaration; we can consider it to mean res is a number. The & symbol means and. So the full meaning of this query is "show all values for res such that res is a number equal to (3 + 33) multiplied by (4 + 44)".
Instead of indicating Success or Failure for this query, FormulaOne will give you a solution that looks like following:

FormulaOne has found one solution to the query, one value for res which will make the query formula true. That value is 1728, (3 + 33) * (4 + 44).
Actually, you would get the same result even if you omitted everything in the query up to and including the &. The complete set of circumstances in which you can do this will be explained later. For now, we will precede all our queries containing unknown variables with an all phrase and a variable declaration.
Now let's consider a slightly more complex example.

This query has a new symbol, |, which means or. Translation into English of this query is "show all values for x and y meeting the condition that x and y are numbers, x is equal to either 4 or 5, and y is equal to 64 + x". You can see for yourself that this query has more than one solution, and that the solutions will involve both variables. FormulaOne has found two combinations of values for the variables, and each combination satisfies the formula. If we had said all x instead of all x,y, we would have gotten only the solutions for x, and similarly for y. If we had said simply all, omitting the list of variables entirely, it would have defaulted to all variables; that is, the same thing as all x,y.
It's worth noting here that the same solutions would have been found to the above query if we had said (x > 3 & x < 6) instead of (x = 4 | x = 5). FormulaOne has considerably more knowledge of arithmetic, than every other widely-used programming language, including all current Prolog implementations. It can use this knowledge to figure out that the first formula has the same effect as the second.

Here are some more examples of arithmetic queries that you can try out:
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 = 46
We 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 = 46
And now we get the results we wanted, as shown

A brief check will show that these are all the combinations of spiders and beetles that will give forty-six legs in the box. Note the section of the results screen which states Number of backtracks: 0. This phrase means that FormulaOne has found these solutions not by trying all possible alternatives, as all current Prolog implementations would have done, but by applying a decision procedure for solving arithmetic queries. This decision procedure avoids having to test the many possible solutions which fail to satisfy the formula.

Some Formal Definitions

Let's look a little more formally at the syntax of simple arithmetic formulas and queries in FormulaOne.
  • A variable identifier is:
    • a string of letters, numbers, and underscores, starting with a lower-case letter.
      A variable identifier cannot be one of the FormulaOne reserved words.
      Examples: res, x, fahr_Temp, xyzzy _
  • A term can be:
    • a variable identifier;
    • an integer constant (a string of digits, possibly preceded by a minus sign);
    • two terms separated by a +, -, *, / (quotient without remainder), or mod (modulo, or remainder upon division);
    • a term surrounded by parentheses, ( ).
      Examples: (3 + 33), f + 32, (c*9) mod 5
  • A formula can be:
    • an expression of the form var::L, where var is some variable identifier;
    • two terms separated by a =, <, >, <= (less than or equal to), >= (greater than or equal to), or <> (not equal to);
    • two formulas separated by a & (and) or | (or);
    • a formula surrounded by parentheses,( ).
      Examples: sec::L, 8*s + 6*b = 46, (x = 4 | x = 5)
  • A query can be:
    • a formula containing no variables;
    • a formula preceded by all and an optional list of variables.

This is just a small subset of the whole FormulaOne language. The rest of this tutorial will be concerned largely with what the "other things", terms, formulas, and queries can be. A complete and comprehensive description of the language can be found in the Programmer's Manual section.

"How It Does It"

We can trust FormulaOne to solve arithmetic queries correctly without needing to know how it manages to solve them. But when we write programs, we will have to know more about this, in order to predict the course of events in our programs. The way it actually solves a query is very complex, but this section will give a simplified version of the process that will be all that's needed to understand it.
We'll describe the process using a fairly simple example:
all x  x::L & (x<4 | x>6) & x = 10
We'll explain how other kinds of formulas are handled as we get to them.
We can think of FormulaOne as having a query pointer which points to the current position in the query that it is considering. The query pointer will be denoted below by the symbol (DownArr). The system will advance the query pointer through the formula, building up an environment which contains the information it has so far about the values of variables. Occasionally, it will set up backtrack points (o) which it will return to if it encounters inconsistencies. Each backtrack point will be associated with a skip point later in the query. When the system gets to the end of the query without getting any inconsistent information about the values of variables, it will try to print a solution.
  1. The first thing the system will do is to store the fact that the user is requesting values of x with the expression all x. Then it will start the processing of the main part of the query, with an empty environment, the query pointer at the start of the query formula, and no backtrack or skip points set up.
    x::L & (x<4 | x>6) & x = 10 & (Env: empty)
  2. The query pointer will be advanced through the first formula, with the information that x is a number being stored in the environment. The next formula the system encounters will be an or (|) formula; it will set up a backtrack point at the or, and a skip point after the second part of the formula. It will then advance the pointer to the first part of the formula.
    x::L & ( x<4 | x>6 ) & x = 10 & (Env: x::L)
  3. The pointer will be advanced through x<4, with that information going to the environment. When the pointer reaches the backtrack point, it will skip over to the skip point. The system is following the rationale that if 'A or B' is true, we can first assume A, and then come back to B later.
    x::L & ( x<4 | x>6 ) & x = 10 & (Env: x<4)
  4. Now the system encounters an inconsistency. It knows from the environment that it has assumed x<4, but now it faces the information that x = 10 as well. This is an inconsistency; a failure occurs, causing a backtrack operation. The system moves the pointer to the last backtrack point set up. As it does this, it removes the backtrack point, its associated skip point, and all information that it put into the environment since the backtrack point was set up. The system is essentially saying 'Assuming x<4 didn't work after all, so let's try assuming x>6.
    x::L & ( x<4 | x>6 ) & x =10 & (Env: x<4)
  5. Now, the system can advance the pointer through the rest of the query to the end, without setting up backtrack points or encountering inconsistencies. When it reaches the end, it will print out the value of x taken from its environment (as requested by the all clause at the start of the query).
    x::L & ( x<4 | x>6 ) & x = 10 & (Env: x=10)
There are no backtrack points set up at the time the pointer reaches the end of the query, so processing ends there. However, if some backtrack point had remained, the system would have made a backtrack after printing the solution, to see if there were more possible solution. It would have kept on doing backtracks after finding solutions until no backtrack points remained. Figure 2.5 shows the result of this query. Note the Number of fails statistic, which lists the number of times the system had to make a backtrack due to a failure (in this case, one, the failure noted in point 4 above). This statistic is a good measure of how complex the query was to solve. All of our previous examples have had 0 fails, so they have not been very complicated by FormulaOne standards.

Queries with explicit or-s in them will always cause backtrack points to be set up. But implicit backtracks can also occur; for instance, in the query
all x  x::L & x > 10 & x < 20
the 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.

Another example of implicit backtracking is the 'spiders and beetles' query from earlier mentioned earlier. There, the decision procedure for integers caused a single backtrack to occur which caught the other solution to the puzzle. That particular example is too complex to go into, but you should be able to trace through all the other examples without too much trouble.

The Print Formula

The Print formula is a useful tool for tracing the execution of queries, and doing simple output to the screen. A formula of the form Print('xxxx'), where xxxx is any text, can be used anywhere any other formula can. (In fact, Print is just a predefined predicate in FormulaOne) When the FormulaOne query pointer is advanced to such a formula, it has the effect of just printing out the text within the two single quotation marks. For instance, the query
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.

So the query
Print('ABC\n') & Print((3 + 33) * (4 + 44))
would cause the output

Print arguments can also be strung together within the parentheses, if they are separated by commas. So the query
Print('ABC','\n',(3 + 33) * (4 + 44))
would have exactly the same effect as the query above.

Print can be used effectively in helping us follow the course of computation of a formula. Any backtrack that causes a Print to be re-evaluated will cause the text in it to be printed again. We can insert a Print formula into our extended example above:
all x  x::L & (x < 4 | x > 6) & Print('Here\n') & x = 10
Then the output of the query will look like

As an exercise, you might want to trace through the execution of this query just to see that the result above makes sense.

Summary

  • The basic unit of programming in FormulaOne is the formula.
  • If a formula with no variables is entered as a query, FormulaOne will tell whether it is true or false; if a formula with variables is entered, FormulaOne will give values for the variables which will make the formula true.
  • FormulaOne solves a query by stepping through it from left to right, sometimes skipping over parts of it and coming back to them later through backtrack operations.
  • The Print formula can be used to get the system to print things on the screen.


F1: Predicates

 Top [image] Preface [image] Data Types

Predicates

  • Predicates and Modules
  • A Simple Predicate Definition
  • Reading Predicate Calls
  • Variables
  • Calling Predicates in Predicates
  • More Formal Definitions
  • Summary

So far, we have seen formulas used only as queries. But formulas can also be named and stored away for later use. A formula which is named in this way is called a predicate, and predicates are the basic building-blocks of FormulaOne programs. They correspond roughly to the procedures, functions, and subroutines of languages such as Pascal and Basic.

Predicates and Modules

A predicate definition must be stored in a FormulaOne entity called a module. Basically, a module is just a group of predicate definitions and associated information, stored in a file.

A Simple Predicate Definition

Previously we learned how to solve puzzles of the form
8*s + 6*b = 46
We 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....".

Installation of the FormulaOne compiler also installs the Tutorial project with the module called Tutorial. It contains most of the predicates discussed in this tutorial. 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 the first time. Another possibility is to create your own module, type in the text of the Puzzle_soln predicate so that it appears exactly as above and compile the module afterwards.
Now you can pose the following query.
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.
This is how FormulaOne handles all predicate calls (as we call such formulas - logicians would call them predicate applications). It substitutes the predicate call by the predicate body, in the process substituting arguments (the terms given in the call, like s, b, and 46) for the formal parameters (the variables in the predicate declaration, like x, y, and z). If we posed the query Puzzle_soln(s, b, 48), it would substitute 48 for z instead of 46, and we would get the expected response.

Reading Predicate Calls

A predicate is something which expresses some property, quality, or relationship possessed by a term or a group of terms. It's important that we name predicates in such a way that the property they express is clear, even given the terse syntax of logic they are phrased in.
Above, we have defined a predicate which expresses the property that x spiders and y beetles have a total of z legs. We have called it Puzzle_soln so that we can read a call such as Puzzle_soln(a, b, 46) as 'one puzzle solution is a and b when the total is 46 '. Since it's not always clear what the intended reading of the predicate is, it's a good idea to put a comment in the program text immediately after the first line of a predicate declaration, to tell how a call to it is supposed to be read:
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.

Variables

Unlike in the C programming language where a variable can be declared as local or global, in FormulaOne we have only so-called "local" variables. What variables can a predicate "see"?. It can only see
  • the variables which are in its parameter list, or
  • variables which are defined in the body of the predicate itself, or
  • variables which are implicitly defined in a predicate call made by this predicate. An example is the Sum predicate.

All these variables are local variables. No other predicate can use, alter or refer to a local variable unless it is given access to it by having the variable passed to it as a parameter. This restriction can cause a loss of efficiency on some occasions but to counterbalance that is the great benefit that whole classes of programming errors are eliminated.
For example, we could define a predicate Divis, which expresses the property that one number is divisible by another, by the following:
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:
'The number x is divisible by the number y if and only if there is some number z such that z multiplied by y results in x.'
This is exactly how a mathematician would define it. The variable z, which appears only in the body of the predicate, is a local variable, and the predicate is true only if FormulaOne can find some value for z which satisfies z*y = x. For example, the query
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.
Constants, types and predicates can be designated with the local keyword, but this must not be confused with the concept of 'local' variable.

Calling Predicates in Predicates

Predicate definitions can, of course, refer to other predicates:
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.
Predicates can even refer to themselves. Such predicates are called recursive, and are used to allow FormulaOne to perform some action repeatedly. The following predicate will find the greatest common divisor of two numbers x and y by an algorithm known since Euclid's time: keep changing the numbers by subtracting the smaller number from the larger, and when the smaller number is zero, the larger number will be the GCD.
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

More Formal Definitions

A predicate name is a sequence of letters, numbers, and underscores, beginning with a capital letter. A predicate definition is of the following form:
pred Name(varl::typel,var2::type2,...varn::typen) iff formula

Each of the vari above is a variable identifier, and Name is a predicate name.

Summary

  • Predicate definitions allow us to compute the same formula many times with different parameters .
  • Predicate definitions must appear in program modules, and the modules must be compiled before FormulaOne is able to use those definitions in queries.
  • FormulaOne expands a defined predicate call into the body of its definition, substituting arguments for parameters.
  • Predicate definitions should include comments to help readers understand what they signify.
  • Predicates can refer to local variables not appearing in their list of parameters.
  • Predicates can call other predicates, including themselves. Predicates which call themselves are called recursive.

 Top [image] Preface [image] Data Types


F1: Data Types

 Top [image] Predicates [image] Modes

Data Types

  • Why Types?
  • Variable Declarations
  • Integers
  • Long Integers
  • Real Numbers
  • Strings
  • The Pairing Operation
  • The FormulaOne Universe
  • Subranges
  • Lists
  • Summary

So far, the only objects we have worked with have been what we have referred to as simply numbers. But in fact, FormulaOne programs can work with several different kinds of numbers, and there are other non-numeric objects they can manipulate, such as strings and lists of other objects. All these objects form the FormulaOne universe. Types, in FormulaOne, are just subsets of this universe. When we declare a variable to be of a certain type, we are saying that its value can come from that type's subset of the universe.
Here we should point out the distinction between objects and terms. A term is a FormulaOne expression, a purely linguistic sequence of symbols. An object is an abstract entity that some term refers to. For example, '22 + 3' and '25' are two different and distinct terms, but they both denote the same object, that is the number twenty-five.

Why Types?

Most conventional languages, such as Pascal and C, have some notion of the type of a variable. Some other languages, like LISP and some Prologs, have no such notion. Variables in these languages are just variables, and can take on any kind of value. Why does FormulaOne have types?
There are several reasons. Types make our programs more readable, because we can tell more easily what a variable represents. They also let us pass off to the compiler some of the work of checking arguments in predicate calls. And when the compiler knows what type a variable is, a program can represent it more compactly and access its value more efficiently.
Finally, giving types to variables allows FormulaOne to use decision procedures such as the one it uses for integer arithmetic. Languages which have no types, such as some dialects of Prolog, can't possibly do that because they can't distinguish between integers and any other kind of variable. These decision procedures involve the notion of constraint. Constraints are the pieces of information that FormulaOne places in the environment as it is computing the solution to a query. A constraint can be something as simple as the information that a variable has a certain fixed value, or the information that the sum of a group of variables is equal to another variable. We'll tell you what kinds of constraints can be put on each type of variable as we describe them.

Variable Declarations

As we have seen, variable declarations (such as x::L) can appear as formulas in queries or in the bodies of predicates, or as parameter declarations in predicate definitions. The most simple form of a variable declaration is the following:

var::type

In this template, var is a variable identifier. This can be any string of letters, numbers, and underscores, as long as it starts with a lower-case letter, and is not one of the FormulaOne reserved words. type is the name of a FormulaOne type, such as L, specifying what kind of variable it is. The four basic types in FormulaOne are L, I, R, and S.
  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.

Integers

I is the type of integers. Variables declared to be of this type are represented within the computer by the standard representation for integers (a block of 32 bits), which allows them to take on values from (-2,147,483,648 to 2,147,483,647). I variables can be compared to other I variables, and to integer constants (integers spelled out as sequences of digits). However, any constants which I variables are compared to must be in the above L range. The constraints that can be put on an I variable, say x, are of the format

x op n

or of the format

x op var + n

where op is one of the arithmetic relational operators ( = , <=, etc.), var is some other I variable, and n is some fixed integer value.
Whenever a formula with integers and a relational operator is processed by the query processor, it tries to put it into one of these forms by the laws of algebra. If it cannot, it will try to compute a value for some variable, if that is possible, or raise an exception ('Too many backtracks...') if it is not. So queries like
all s::I & b::I & s = 40 & b = 3*s + 9
work with integers, because the value of s is known at the time the last formula is encountered.
All the previous queries will also work with I variables, up to the spiders and beetles example. But the query
all s::I & b::I & s>0 & b>0 & 8*s + 6*b = 46
should give an exception, because FormulaOne cannot convert the last formula to the proper format for an I variable constraint.

Long Integers

L is the type of long integers of unlimited bit-precision.
The constraints that can be put on L variables are of the following form:

tlvl + t2v2 +....tnvn op m

where the ti's and m are long integer values, the vi's are long integer variables, and the op is an arithmetic relational operator (one of =, <, <=, <>, >, and >=).
In particular, the spiders-and-beetles formula
8*s + 6*b = 46
is 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.
For example, consider the query
all x::L & y::L & x > 0 & y > 0 & x * y = 46
This 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 = 46
Then, FormulaOne could solve the equation by testing all values of y between 0 and 50 (not inclusive).
Your own knowledge and programming skills can be brought to bear on a problem. In this example, considerations of basic mathematics would lead you to an optimized query:
all x::L & y::L & x > 0 & y > 0 & y < 24 & x * y = 46
FormulaOne will only test for y from 1 to 23 (obviously 24 or greater will not divide evenly into 46).
It might seem that you could optimize the query further by adding in y > x as another constraint. However when x is fixed then y is fixed as equal to 46/x so the additional constraint yields no benefit. You might wish that FormulaOne could solve problems like this in a better way. FormulaOne has taken the approach of being able to internally solve a very useful subset of possible queries, and that's a lot more than other logic or declarative languages do. A famous result of mathematical logic, Godel's Incompleteness Theorem, has as a consequence that there is no procedure or algorithmic problem-solver which will satisfy everybody. Nevertheless, your own problem solving method can be encapsulated into a predicate which will have the effect of acting as a constraint in the manner you desired. In any case, if you don't think you need the additional power or additional range of long integers in your problems, we would recommend that you use integers. They take up less memory in the computer, and because they can have fewer kinds of constraints on them, their decision procedure is more efficient.

Real Numbers

R is the type of real numbers. These are the numbers with fractional parts as well as integer parts. They are represented in memory by the conventional 64-bit representation of such numbers. Mathematically speaking, we can represent only rational numbers in this way, so these numbers might better be called rational (in both FormulaOne and other programming languages!). But in later versions of FormulaOne, R variables will stand for actual real numbers (roots of polynomial equations), and will have their own decision procedure, so we will call them reals.
Real-number constants are of the form
[-]<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.
Real-number constants can also be followed by an optional expression of the form
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.
A full decision procedure for real-number variables exists, but is very complex. The only constraints you can put on real variables in FormulaOne are of the format

x op n

or of the format

x op var + n

the same as for integers. Note, again, that this doesn't mean that you can't do arithmetic operations with real variables. You can do any addition, subtraction, multiplication, and division you want with them, as long as their values are known at the time the expression gets evaluated.

Strings

The type S is the type of character strings. This is the first non-numeric type we have encountered. A character string is just a sequence of characters, of any length. An S variable can have any string as value, regardless of length.
Constant terms of type S consist of the characters of the string, enclosed in single quotes. For example:
'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.
For instance, the query
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 is a predicate which takes three string arguments, and succeeds if the third string is the concatenation of the first two. The first two arguments to Append, however, must have values, so it can really only be used to find the concatenation of two given strings.
Append('foo','bar',str)
will result in str = 'foobar', while
Append('foo ','bar', str)
will result in str = 'foo bar'.
Single characters can be extracted from strings by direct indexing. The first character has the index 0. The query
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".
Here is a predicate which will allow us to take a string and pad it with periods (".") to 10 characters, if it is not that long.
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.

The Pairing Operation

The four basic types in the FormulaOne universe are integers and long integers, reals, and strings. But from those four basic types can be made many more data structures, by using the pairing operator, ",". When you place a comma in-between two terms, the whole thing forms a new term, the pair containing those terms. Some examples:
(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)

The FormulaOne Universe

The complete set of objects - the things that terms can represent in FormulaOne - consists of all the real numbers, all the strings, and all possible pairs that can be made from applying the pairing operation to them any number of times. The long integers are a subset of the real numbers, and the integers are a subset of the long integers. This set of objects is called the universe of FormulaOne.

Every term we will encounter will refer to some object in this universe. Types are just subsets of this universe. The type consisting of the entire universe is called the universal type. U. R and S are basic types, but also subsets of the universal type; I and L are subsets of R, and so subsets of the universal type U too.
This means that when a term of one type is given as an argument to a parameter of another type (the situation usually referred to as a type clash in other languages), it doesn't necessarily cause a problem. Say we had the following predicate defined and compiled:
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.
The basic types of the universe are all referred to by name identifiers. But you can also use more complex type expressions to refer to many different useful types. The forms of type expressions have been chosen to represent the kinds of types that programmers frequently want.

Subranges

Recall our original spiders-and-beetles query. Since we can guess that there must be between 1 and 10 of both spiders and beetles, we could have phrased that query in the following way:
all s::[1..10] & b::[1..10] & 8*s + 6*b = 46
We 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 = 46
Expressions of the form

[n..m]

for any numbers n and m, stand for the type containing all the integers from n to m. They act just like the type names I, S, and so on, and can be used in parameter and local variable declarations just like them. Some examples:
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

L[n..m];

for example
ftemp::L[-32..212]

Lists

We can declare a variable, say x, as being a list of integers by the declaration x::list I. This declaration has a precise technical meaning in FormulaOne. All the following terms are constants of type list I and can therefore be compared to x:
(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:
  • Nil is of type list I;
  • The pair (h, t) is of type list I if h is of type I and t is of type list I;
  • Nothing else is of type list I.

Nil stands for the list with no elements. It is an empty list which cannot be represented by a pair (head,tail). Every list must be terminated with the term Nil (this also allows the compiler to distinguish a list from a pair). Nil is really just another term representing the object 0 in the universe; but FormulaOne will not let you give the term 0, or any arithmetic expression equivalent to it, as a list. It allows only the term Nil itself.
We can use lists of other types too, for instance list L, list S, and list [-32..212]. Here is a predicate that may come in handy for processing lists of long integers.
{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.
The formula l = (head,tail) is a deconstructor of a list. This deconstructor decomposes l for your convenience (but does not destroy it) and in the process implicitly defines two new variables which we will call head and tail:
head::L tail::list L
For 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.
The predicate Sum, simple as it is, illustrates important concepts and so it is worthwhile to go through it with an example.
In computing the query all Sum ((3,44,Nil),x), lines 3 and 4 have no effect because l = (3,44,Nil) and so l <> Nil (i.e. l is not equal to Nil). Line 5 deconstructs l into a head of 3 and a tail of (44,Nil). Line 6 recursively calls Sum with new arguments tail and tailsum.

We go back to line 1 and replace l by tail and sum by tailsum. Note that sum and tailsum have not yet received any value. Again, lines 3 and 4 have no effect but line 5 deconstructs l into head = 44 and tail = Nil.

The next recursive call in line 6 in Sum(Nil, tailsum). This is a new tailsum but the compiler is aware of that and keeps track of the versions of tailsum. In this call lines 3 and 4 are finally executed and this time tailsum gets a value, which is 0.

Control passes "back up one level" and line 7 is executed: sum = 44 + 0 = 44.

Next control passes up to the first recursive call where head was 3 and line 7 executes and gives a final sum = 3 + 44 = 47.

There are other and better ways to achieve what Sum accomplishes, but you should have a clear idea of its mechanism because Sum incorporates critical ideas about lists, recursion and declarative programming in general.
Lists are recursive data structures, so recursive predicates fit them well. You will frequently encounter recursive predicates, and the need for them, when you work with lists. There are several predefined predicates for lists. Len and Append, which we encountered for strings, also work with any kind of list type as well as strings. (They are, technically, polymorphic predicates - they can take many types of terms as arguments.) Len gives the number of elements in the list, and Append makes a list out of the elements of the first list, followed by the elements of the second.

There is also a list membership operator, in, which you can use to test or assert that a term is in a given list. The following query should succeed:
all x::I & z::list I & x = 2 & z = (3, 2, Nil) & x in z
the 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 z
should give you two solutions, one with x = 3 and the other with x = 2.

Summary

  • The four basic types of FormulaOne are I (integers), L (long integers), R (real numbers), and S (strings).
  • Types are subsets of the FormulaOne universe. I is a subset of L, which is a subset of R.
  • L integers can have more general and powerful constraints put on them than I integers.
  • Subrange type expressions allow you to assert that an integer variable is in a given range.
  • Variables of a list type expression can have values consisting of lists of values of a given type, terminated by Nil.
  • There are several predefined predicates in the FormulaOne Runtime Library (F1RTL), which make working with strings and lists easier.

 Top [image] Predicates [image] Modes


F1: Modes

 Top [image] Data Types [image] Control Structures

Modes

  • Symbolic Mode
  • Input Mode
  • Output Mode
  • Mode Clash
  • Summary

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.

Symbolic Mode

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.

Input Mode

Consider the Sum predicate. Its first parameter is a list of I values, and the second is the sum of that list. Now, a query such as
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.

Output Mode

Here's something that happens quite often in all computer programs: a routine is called, and the value of one of its parameters is fully computed and then passed back to the calling routine. If we have parameters which are handled like this in FormulaOne programs, we would like to be able to tell the compiler to use the efficient, constraint-free representation for the parameter. But we can't declare it to be an input parameter then, because we specifically don't know the parameter's value until it is computed.

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.
The only space allocated for an output variable in memory is, as for an input variable, enough space for its value. Constraints are not used for output variables either, because FormulaOne makes sure that the output variable is not used before its value is known. This means, for instance, that in Sum1, implicitly declared local variable tailsum is known to have a value after the recursive call to Sum1, so the addition operation immediately after is compiled as a simple addition, with no checks or constraints. The speed-up in this new version of Sum1 is very noticeable (just look at the time FormulaOne reports that it took to compute the sum of a list under the old and the new versions of the predicate).

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

Mode Clash

We have seen some examples of what happens when a term of one type is used as an argument corresponding to a parameter of another type. What happens when an argument does not match its parameter because of incompatibility in modes?

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 = 6
With 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 query
all 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.

Summary

  • Input mode parameters must have a value at the time a call is made to the predicate.
  • Output mode parameters and local variables must not have a value at the start of the predicate, but must be given one on their first use.
  • Using input and output mode can make your programs faster and more readable, and help you find bugs in them.
  • Any mode of variable may be given as an argument to an input or output parameter. But if a symbolic or output variable is given to an input parameter, FormulaOne will try to "backtrack out" its value if possible.

 Top [image] Data Types [image] Control Structures


F1: Control Structures

 Top [image] Modes [image] Procedures, Subroutines and Functions

Control Structures

  • The if Formula
  • Alternate Forms of if
  • The case Formula
  • Iteration

The if and case formulas of FormulaOne correspond to similar features of other programming languages. We can use these types of formulas to make common patterns of logic more readable, because they have a syntax and structure which is closer to what we are thinking when these patterns appear in our programs. Another reason to use if and case is that the FormulaOne compiler can compile them into very efficient object code.

The if Formula

We can rewrite Fib_prevl predicate by using an 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:

if A then B else C end

where A, B, and C are all formulas.

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.

Alternate Forms of if

There are two main alternate forms of the if formula. The formula

if A then B end

is equivalent to the formula

if A then B else true end

For example, we might want our Fibonacci number predicate to print a warning message if we try to give it an index less than one, but to go on nevertheless:
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

The case Formula

The case formula is similar to the if formula, in that it causes formulas to be evaluated based on the outcome of a test. Consider the following rewriting of the Sum1 predicate.
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:

case term of
term1 => formula1;
term2 => formula2;
.................;
termn => formulan;
end

The first term is called the subject term, and the others are called case terms; the formulas are called case conclusions. The subject term must be full-value, as is the case with variables in if condition formulas. One condition on the case terms must be met for the compiler to accept the case formula: they must, between them, cover all the possible forms that the subject term can take.

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

Iteration

Most programming languages provide an explicit method of allowing iteration, or looping, where a segment of a code can be executed repeatedly. FormulaOne provides this facility by recursion.

Top [image] Modes [image] Procedures, Subroutines and Functions


F1: Procedures, Subroutines and Functions

 Top [image] Control Structures [image] Building Types

Procedures, Subroutines and Functions

  • Predicate Classes
  • Procedures
  • Subroutines
  • Input/Output Mode
  • Queries Revisited
  • Functions
  • Summary

Usually there is a trade off between logic programming languages and other programming languages. If you use logic programming, you get the power of built-in backtracking search and symbolic variables, but the programs you write are not very efficient. If you use conventional languages such as Pascal or Basic, the programs are very efficient, but you have very limited search and symbolic capabilities.
One very important aspects of FormulaOne is that it gives you the power of logic programming yet allows you to write predicates and programs which are compiled with the efficiency of conventional programs.

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.

Predicate Classes

A predicate can be declared with either the proc or subr keyword in the place of pred keyword. Each of these keywords asserts that the predicate is in a different class of predicate, the three classes being pred (true predicate), proc (procedure) and subr (subroutine).

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

Only true predicates can do backtracking through symbolic variables and or-s but only procedures and subroutines can have input/output (I/O) variables.

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.

Procedures

The major source of power in logic programs is the backtracking mechanism. But sometimes this can also be a source of inefficiency. To control backtrack, a logic program has to keep a lot of data around concerning where the next backtrack location is, what the old values of variables were, and so on. When you declare a predicate to be an FormulaOne procedure, you are asserting that it is never going to backtrack. (This is what's called a "deterministic predicate" in Prolog terminology.)

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.

The following procedure would not compile, because the input/output variable has had its value modified to 2 in the left argument of the or:
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.

Subroutines

A subroutine is a special kind of procedure which can access data external to the FormulaOne environment, such as input from the user or the computer's date and time. In fact, the only reason we would declare something to be a subroutine rather than a procedure is to access this kind of data through the existing system-defined subroutines.

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.

Input/Output Mode

Now that we have covered procedures and subroutines, we can discuss the fourth and last variable mode. This is input/output mode. An input/output (i/o) mode variable is like a simple input or output variable in that no constraints are ever recorded for it, just its value. But unlike input and output variables, i/o variables can have their values reassigned. Consider the following version of our Sum procedure.
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.

For instance, given the procedure Incr
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.

Queries Revisited

Up to now, we have been using the all keyword at the beginnings of queries, followed by an optional list of variables. In fact, the all clause is sometimes not necessary, and sometimes unusable. A query is executed as if it were a formula which is the body of a predicate. By default, the predicate whose body it is, is of class subr, and so cannot do any of the things listed in section 7.2; however, it can call subroutines and use i/o variables.

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:

  • If your query contains logical variables, "or"s, or calls to true predicates, use an all.
  • If your query contains i/o variables or calls to subroutines, don't use an all.
  • Otherwise, it's your choice. Since the formula can act as the body of any of the three classes of predicate, it doesn't matter whether you use an all clause or not; but using one will allow you to select which variables' values you want reported.

Functions

In mathematics, a function is an object which maps a set of parameters onto a single, uniquely-determined value. In FormulaOne, a function is much the same thing: a procedure which determines one parameter from several others, without backtracking.

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.

Summary

  • The three predicate classes, pred, proc, and subr, have different capabilities and restrictions.
  • preds, or true predicates, are the only class which can do backtracking.
  • procs and subrs are the only classes which can use i/o variables, subrs are the only class which can access external data, but they can be called only from queries or other subrs.
  • Input/output, or i/o, variables can be assigned one value, and then reassigned a different value, with the : = operator.
  • You need to precede a query formula with an all expression only when the query formula cannot be the body of a proc or subr.
  • If all the parameters of a procedure are input except for the last, which is output, then the procedure is also a function and can be called using functional notation.

 Top [image] Control Structures [image] Building Types


F1: Building Types

 Top [image] Procedures, Subroutines and Functions [image] Database Files

Building Types

  • Type Declarations
  • Tuples
  • Field Selection Terms and Deconstructors
  • Enumerated Types
  • Unions
  • The Universal Type
  • Type Conversions
  • Arrays
  • Array Constants and Initializing
  • Flexible Arrays

Type Declarations

FormulaOne has a facility which allows you to give names to types you define, so that they can be used more readably and clearly. These types must be declared before any predicate declarations which use them. Some simple examples of type declarations:
Posint_t =[1..]
Digit_t = [0..9]
Stringlist_t = list S
Weight_t = I
Notice 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.

Tuples

Consider the following type declaration.
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

(var1:type1, var2:type2,...., varn:typen)

The variable names declared within the parentheses are called Fields, and can be of predefined types themselves:
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.

Field Selection Terms and Deconstructors

The fields of the Date_t type, year, month, and day, can be referred to individually. With the variable declaration in the last section,
birthday:>Date_t
the 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

Enumerated Types

Enumerated types are a way for programmers to introduce their own names for terms 3 a program.
Gender_t = Male | Female
Colour_t = Red | Yellow | Green | Blue
These 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.

Unions

Enumerated types are actually just a special case of type expressions called unions. Union type expressions are much like C unions, or Pascal case variant types.
Vehicle_t = Tricycle | Car(doors:I, engine_size:I) | Bicycle(gears:I) | Motorcycle
The 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 Universal Type

We have indicated before that a universal type U exists, a type of which every member of the FormulaOne universe is a member. Up to now, we have not studied how to use this universal type in programs, because it's implemented as a union type. Now we can study it.

The name of the universal type is U, and it looks to programs as if it has been defined with the following recursive definition:

U = R(r:R) | P(h:U, t:U)

Clearly, this definition is not a valid FormulaOne type definition, since R is used as a variant name as well as a type. But U is treated in a special way, so an exception is made for it. U is special because any object, of no matter what type, is also an object of type U. The structure of U is exactly the structure of the FormulaOne universe: all real numbers, and all pairs that can be built up from them. Thus, if a predicate parameter is of type U, any term can be given as an argument to that parameter in a predicate call.

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.

Type Conversions

But what exactly is the mechanism by which terms are converted from one type (say list I) to another (say U)? There are actually two different ways this kind of type conversion is done in FormulaOne programs: type coercion, which happen automatically, and type casts, which are explicitly specified by the programmer. A term of the form

term : type

is a type cast term. Its value, if it exists, is the given term converted to the given type. Logically, the effect of a type cast is to insert a test before whatever formula it appears in, checking that the term is a member of the given type. If the test fails, the formula containing the cast fails.

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.

Arrays

It's often useful for us to store a number of variables of the same type together in a single variable, and to use another index variable to pick out which one we are referring to. This data structure is called an array, and appears in most programming languages (though not in most Prologs). An array can be seen as a data structure which associates one value of a given element type with each value of an index type. So in FormulaOne, array types are declared using the standard mathematical "mapping" notation:
P_data_at = [0..3] -> P_data_t
This 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] -> I
The 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.

Array Constants and Initializing

An array variable can be assigned a value, like any other variable. But because of the nature of arrays, we have to use a special syntax to denote a value assigned to an entire array. An array constant is just a list of constants of the element type, separated by commas and enclosed by square brackets.
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 = Theresa
An 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
     ...

Flexible Arrays

The arrays we have been considering up to now are fixed arrays: we know how many elements are in them from their declarations. Arrays can also be flexible, however, in that the number of elements in them is set only at the time a query is run.

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..] -> I
declares 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 typical use of the procedure Asum would be with arrays which have fixed upper bounds:
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.
There are three basic methods of assigning values to flexible arrays. The first one uses an explicit array constructor:
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:Flex
Here 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.
Top [image] Procedures, Subroutines and Functions [image] Database Files


F1: Database Files

 Top [image] Building Types [image] Collecting Solutions with "all"

Database Files

  • Database Files in FormulaOne
  • Files as Variables
  • Reading Database Files
  • Positioning the File Pointer
  • Altering Database Files
  • Database Files as Predicates
  • Index Files
  • Manipulating Files
  • Summary

A FormulaOne database file is a list of values of a given type, stored in an efficient binary format. In the following discussion, we'll use the term database file to refer to the concept of a FormulaOne file, and external file to refer to the files as they appear in OS file system. When there's no possibility of confusion, we'll just use file. This section will discuss how files interact with, and are manipulated by, programs.

Database Files in FormulaOne

A database file, in the FormulaOne world, is like something in-between a module, a predicate, and a variable. It's defined like a module, but can be accessed in programs like a predicate and passed in queries like a variable. The actual contents of a database file is a set of records stored in a file on secondary storage, such as hard disk. Each record is a value of a FormulaOne type associated with the file by the programmer.

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_ft
The 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.

Files as Variables

A file such as P_data can be referred to in the FormulaOne query processor as an input/output variable, which can be passed to procedures in queries. We can think of its structure as being a list of values of the file type, along with a file pointer, which points to some value within that list. When we pass a file to a procedure in a query, initially the file pointer points to the beginning of the file.
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:

  • DbAccess
  • DbGet
  • DbSkip
  • DbEof
  • DbRewind
  • DbEofSet
  • DbPut
  • DbInsert
  • DbDelete
  • DbTruncate

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.

Reading Database Files

The predefined procedures DbAccess and DbSkip can be used to read database files, within procedures.
{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).
Typical output from this query might be
'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

Positioning the File Pointer

Two procedures are provided for positioning the file pointer within the file, DbRewind and DbEofSet. DbRewind takes an input/output file variable as its only argument,
proc DbRewind(f:.file T)

It has the effect of simply setting the pointer back to the beginning of the file, before the first record.
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.

Altering Database Files

So far, we have dealt only with procedures which alter the file pointer, if they alter anything at all. But it is also possible to alter the contents of the file, inserting and deleting records. The DbPut, DbInsert, DbDelete, and DbTruncate procedures perform these actions.

DbPut

DbPut takes two arguments, an input/output file variable and a value of the file's record type.
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.
The following code demonstrates the usage of DbRewind, DbTruncate and DbPut:
 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.

DbInsert

DbInsert is an alternative to DbPut. DbInsert uses the same arguments as DbPut. Using DbInsert creates a database file in sorted order. Consider the routine CreateP_dataFile1:
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.

DbDelete

DbDelete has one argument, the input/output file variable,
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

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 DbTruncate:
start->|A|....|P|Q|R|....|Z|<-end
           ptr->|
After DbTruncate:
start->|A|....|P|<-end
           ptr->|

Database Files as Predicates

We have seen how database files can be accessed as variables, for the purposes of explicit reading and updating. But a program can also refer to a database file as a predicate, using the file name as a predicate name. To do this, the program module must use both the files module and the database file itself. In the module header include both as used. Once you have done this, each file in the list of used modules can be referred to in the program as if it were a predicate whose arguments were the fields of the tuple which is the file record type.
The file effectively acts as a module containing one predicate, which is named the same as the file. For example, say we had declared P_data as above, and were writing a module which used P_data. Then we could include the following predicates in the module:
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.
For example, if P_data contained the 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')
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).
Note that in the predicate definition above, the string parameters and gender appear as symbolic parameters, while the two Date_t parameters appear as output. This is the general case with all files being used as predicates. Parameters of type S, I, L, R, or enumerated types (that is, the basic types) are symbolic, while those of all other types (including tuple types) are output. This means that any kind of argument can be given to parameters of basic types, whereas symbolic arguments cannot be given to parameters of non-basic types.
A database file predicate is treated as just another predicate in most ways. Within procedures, all arguments to database file predicates must be full-value. File predicates may also appear as if formula conditions, or preceded by the "not" connective (~), if all arguments are full-value.

Index Files

To search a database file sequentially can be prohibitably inefficient for large files. Index files allow to avoid time-consuming searches through an entire database file in order to find a particular record. FormulaOne implements a set of routines to allow fast database searches of a database record of any type. Prior to creating a database, a decision should be made about the database record fields we are likely to search. Let's consider a database of records of type P_data, defined previously as
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_ft2
several 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.
To illustrate the usage of various index file routines, le us first create a simple indexed database:
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.
Although the records in the database file are in no particular order, the index files allow us to browse all records in an ordered way. The order can be either ascending, or descending, using pairs of routines DbSeekFirst and DbSeekNext or DbSeekLast and DbSeekPrev respectively. For example, the code in DumpAllNames will print out all records sorted in ascending order based on the filed name:
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

Manipulating Files

Files other than database files can be also manipulated from procedures in much the same way as database files can be. Two other file types have been predefined: Bin and Ascii. An Ascii file is interpreted as a standard text file, consisting of lines of printable text. Each string record in the file corresponds to one of the lines, so that DbGet routine (for instance) gets lines of the file in sequence, from first line to last line. For example, the following code will read and print out a text file:
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.

Summary

  • File format can be database, Ascii or Bin
  • Database files can be used as variables or as predicates.
  • A file used as a variable has a file pointer associated with it, which indicates the location at which operations will take place within the file.
  • The file predicates DbAccess, DbSkip, DbGet, and DbEof can be used to read a file.
  • DbRewind and DbEofSet can be used to position the file pointer at the beginning or end of the file.
  • DbPut, DbInsert, DbDelete, and DbTruncate are the only file predicates that change the contents of a file.
  • Ascii and Bin files can be manipulated in procedures as if they were database files.
  • For large databases use index files.
  • Index file search operations are significantly faster then sequential database file search.

 Top [image] Building Types [image] Collecting Solutions with "all"


F1: Collecting Solutions with "all"

 Top [image] Database Files [image] Miscellaneous Advanced Topics

Collecting Solutions with "all"

  • The all Formula
  • all, one, min and max Formulas
  • The Standard Order for Sorting
  • The Whole Truth about Queries
  • Query Output to Database Files
  • Summary

The keyword all can be used in various places to collect all solutions to a given formula - that is, all assignments of values to a set of variables under which the formula is true. We have already seen its use in queries; following section describes its use in procedures and subroutines, and fully explains its use in queries.

The all Formula

The all formula is a special construct which allows you to call predicates from within procedures and subroutines, and sort all possible solutions to the predicate in a list or file. Say we wanted to collect all the records about men from our P_data file. We could do so with the following procedure:
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.
Here's another example. Recall the predicate Even, which is true for any even integer.
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:

all var1, var2,...,varn in listvar formula end

In this format,
  • listvar is a declared variable which can be assigned a value directly; that is, an input/output variable or an output variable on its first use. It must be of type list T or file T, where T is a tuple type or a simple type (such as L or S).
  • var1... varn are variables not declared outside the all formula. They may be declared within the body of the formula; if not, they are implicitly declared according to the declaration of the listvar. If there is more than one variable in the list, they stand for the various fields of the elements of listvar (in this case the element type of listvar must be a tuple type). If there is only one variable, then the variable stands for an entire element.
  • The formula is computed as the body of a true predicate, so there can be no input/output variables declared in it, nor any calls to subrs. It can refer to variables which have values (such as input variables or initialized output or input/output variables), but not change their values or put constraints on them.

Logically, the all formula means that for all values of the vari's, the tuple term comprised of the entire set of vari's is in the listvar if and only if the values of the vari's satisfy the formula; and listvar is the unique list which satisfies this property and is also sorted in ascending order with no duplicates. The listvar will generally be a list, but it can also be an input/output file variable. In this case, the file's contents are emptied, and the solutions are placed in the file, sorted and with duplicates removed, each as a separate record. See section below for more details on output to database files.

all, one, min and max formulas

It is not possible to call predicates, or to backtrack in the procedures or subroutines, except through the all/one/min/max formulas. The syntax of all/one/min/max formulas is as follows

all var1, var2, ..., varn in var form end

min var1, var2, ..., varn form end

max var1, var2, ..., varn form end

one var1, var2, ..., varn form end
All four formulas try to find the values of variables 'var1,...,varn' satisfying the formula form. All n-tuples of values satisfying the formula form of an all formula are collected into the list variable var . All n-tuples of values satisfying the formula form of a min and max formulas are generated and compared among themselves. The minimal or maximal n-tuple (in the ordering of the universal type U) is left as the value of the variables varl,...,varn at the end of the execution of the min or max formula. The first n-tuple of values found to satisfy the formula form of an one formula is left as the value of the variables var1,...,varn at the end of the execution of the one formula. When the formula form cannot be satisfied the all formula returns an empty list, and min, max and one formulas fail.
All four kinds of formulas can be used only in procedure or subroutine contexts. Formula form is always evaluated in the predicate context. There are certain restrictions on the non-local variables used in an all/one/min/max formula but declared outside the formula. The restrictions are necessary in order to uphold the logic of FormulaOne. Non-local variables can be either input or input/output variables. It is impossible to change the values of non-local input/output variables within an all/one/min/max formula. The following example demonstrates what would happen if non-local output variables were permitted:
y :> I & one xy = 3 & x=l | x = 2 end & y = 2
y :> I & y = 2 & one xy = 3 & x = l | x = 2 end
According 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.
The variables vari of min, max and one formulas are both local and global to the formulas. Actually they are two different sets of variables. For instance:
x :> I & min x & x::L & T(x) end
The 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 the variable varl of a min and max formula is a symbolic variable (as in the above example or in the modules containers and warehouses), then before the next solution to the formula form is generated, the variable is constrained to varl <= val, (varl =>val for max) where val is the value of the variable in the previous solution. All four kinds of formulas admit arbitrary local variables. Variables declared as local to the formulas are thought to be implicitly existentially quantified (see the section Scope of Variables of Addendum).

The Standard Order for Sorting

Since the all formula must sort the elements of the list, there must be some standard order in which they are sorted. Recall that the universe of FormulaOne is made up of the reals (including the integers), the strings, and all pairs built up from reals and strings.
Reals are sorted according to the usual order (lowest before highest). Strings are sorted in lexicographic order - that is, the order in which they would be found in a dictionary. Pair terms, including tuples, arrays, and unions, are sorted recursively as follows:

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.
The idea behind this procedure is that the user provides a Key function, which will return a key for any list element; the elements of the list will be sorted in ascending order on their keys. A "key code", given to the Sort procedure and passed on to the Key function, is a code telling what kind of key is to be extracted. This enables Sort to handle different kinds of lists and different keys.
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

The Whole Truth about Queries

Now, we finally have the tools to explain the true significance of the all keyword in queries. The complete syntax of a query is shown below, with square brackets indicating optional elements.

[all [ varl [, ...., varn]] [in outspec]] formula [end]
varl....varn are variables which appear in the formula. If an all clause is included, but no variable list, the variable list is assumed to consist of all the variables. outspec is one of two things:
  • a string constant containing the DOS file name of a standard ASCII file (for example, 'query.out' or '\\misc\\results.txt'), in which case the solutions are printed on that file in the same format as they would in the results screen; or
  • a database file name (see the next section for details).

If no outspec is given the solutions are printed (unsorted and with duplicates) in the familiar solution format, in the results screen on the terminal; As previously mentioned, if the formula can only be the body of a procedure, an all clause must be included; and if it can only be the body of a predicate or subroutine, an all clause must not be included. If no all clause is included, the solution is output to the results screen. The end keyword is completely optional, and has no significance. It is only allowed for compatibility with the all formula.
So we can see a query with an all clause as being a variant of the all formula of procedures and subroutines. Just as an all formula allows backtracking to go on within a procedure or subroutine, an all clause allows the query formula to backtrack within the query. (Recall that a query is executed by default as a subroutine body.) Instead of summarizing all solutions and sorting, however, it just outputs solutions one at a time. The in variable, can be a database file which collects all solutions. But it can also be a regular Ascii file, in which case the file gets the output that would normally go to the screen. This feature is very useful for storing lists of solutions and then viewing them by using the editor for external files. For example, the following query will redirect all output into a text file all_pdata.txt:
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.

Query Output to Database Files

When manipulating databases, we often find it useful to be able to fill a database file with the results of queries (possibly involving other database files). The all formula, and the all clause in queries, allow us to do this easily. Consider the following query:
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_ft
Say 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.
We can do the same kind of thing from within a procedure. We could define a procedure Get_men as follows:
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.

Summary

  • The all formula allows all solutions to a backtracking formula to be collected and sorted within a procedure or subroutine.
  • Output of solutions can be done to either a list variable or a file variable.
  • Calling predicates (pred) or to backtrack in the procedure or subroutine can be done only by mean of the all/one/min/max formulas.
  • There is a standard order by which all elements in the FormulaOne universe are sorted.
  • The syntax of a query is really just a variant of the syntax of the all formula.
  • A query's output can be redirected to a DOS file in the same format as it appears in the results window.
  • The all construct can be used to fill a database file with records corresponding to solutions to a backtracking formula, either from the query level or from within a procedure.

Top [image] Database Files [image] Miscellaneous Advanced Topics


F1: Miscellaneous Advanced Topics

 Top [image] Collecting Solutions with "all" [image] Queries

Miscellaneous Advanced Topics

  • Constant Declarations
  • The Anonymous Variable
  • Scope of Variables
  • The local Keyword
  • Unnamed tuples
  • Injections, Relations, and Unknown Indices
  • Injections
  • Relations
  • Unknown Indices
  • Construction and Deconstruction of Arrays, Tuples, Lists and Unions
  • Tail Recursion Elimination
  • Negation
  • More About if-then-else Formulas
  • Opening and Closing of Files
  • Cross Modular Consistency Checks
  • Heap Management
  • External Modules

Constant Declarations

You can associate a name with a certain constant value by putting a constant declaration at the start of your program, along with any type declarations you may have. Here are some examples:
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:

Name :< type = term

This declaration causes Name to act as a constant term whose value is term. The type of the new term is the given type; needless to say, the term must be of that type as well.
Constant declarations are useful for several purposes. If we want to refer to the same value several times in a program, but we think we might want to change it later, we can instead use a constant declaration which gives a name to the value. Then, if we do want to change it, we need only change the constant declaration. Constants are also used for giving a name which is more easily remembered to an important constant, such as Pi above. They also come in handy when giving a brief, concise name to a long tuple constant, as in the case of Princess above. The full syntax of a FormulaOne program (that is, the contents of a program module) is:

tcdecli
.
.
tcdecln
pdecli
.
.
pdeclm

where each tcdecli is a type or constant declaration, and each pdecli is a predicate declaration. FormulaOne permits declaration of constants, types and predicates to be given in any order, with the following restrictions:
  • Constants must be always declared before they are used for the first time.
  • Non-recursive types must be declared before they are used.
  • Recursive types can be used in a type expression before they are declared.
  • Both the non-recursive and recursive types must be declared before they are used in constant or predicate declarations.
  • Predicates can be declared and called in any order.

In FormulaOne, the declarations of constants, types and predicates are processed before starting the compilation of predicate bodies. This allows for logical grouping of declarations. Declarations of constants and types used globally can be placed at the beginning of a module; constants and types used only in certain predicates can be declared later, before they are used in the predicates. For instance:
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
    ...

The Anonymous Variable

The anonymous variable is the term which consists of a single underscore (_). It is like a variable which is new every time it is referred to, so that two occurrences of it do not refer to the same variable. It is used as a placeholder for terms which we want to match and then discard. Consider the procedure from earlier in the book:
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.

Scope of Variables

Variables in FormulaOne are always local variables. Not only may a variable be local to a particular predicate, but it may even be local to a particular part or structure in that predicate. Look at this example:
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.
Variables which are defined, explicitly or implicitly, within an all/one/min/max formula are local to that formula. From the point of view of mathematical logic, the arguments of predicates can be considered as universally quantified:
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...".

The local Keyword

When we specify in FormulaOne that a module uses other modules, we (by default) give that module access to all the constant, type, and predicate declarations in the used modules. But sometimes this is not what we want. Occasionally we will want to hide all but a few declarations from modules that use a given module, so that the interface between modules is as small as possible.
The keyword local gives us the ability to do this hiding. Preceding a constant, type, or predicate declaration by local makes that declaration inaccessible from other modules, even modules which are specified as 'using' the declaration's module. For instance, say we wanted to put our Eratosthenes' Sieve algorithm in a module, say Sieve. We have three procedure declarations, Print_primes, Sift_print_from, and Multiples_marked. The only ones of these that it makes much sense for some other procedure to call is Print_primes. So it would be logical to put the declarations in Sieve this way:
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])

Unnamed tuples

We have seen how tuple types normally have fields which can be accessed by field selection expressions (e.g., parent.b_date.month). But as well as these named tuples, there can also be unnamed tuples, which have no field names in them. These are more compact and convenient when you know you are always going to disassemble terms of that type by matching them with variable terms.
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.

Injections, Relations, and Unknown Indices

Injection variables, relation variables, and the unknown index capability are features of FormulaOne which are important for complex constraint-satisfaction applications. They are fairly interdependent, and so will be illustrated together with some simple examples.
The examples are taken from the world of logic puzzles, of the kind found in crossword puzzle magazines. These puzzles are usually simple constraint-satisfaction problems. One such puzzle runs as follows.
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.

Injections

The first new feature you will notice is the use of a double arrow (->>) instead of a single arrow (->) in the declaration of Name_t and Occ_t. This double arrow signifies an injection type in the same way as a single arrow signifies an array type.
In mathematics, an injection is a function which never has the same value for two different sets of arguments. In FormulaOne, where arrays are like functions, an injection is an array in which no two elements are the same. Here are some more examples of injection types:
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) = Grey
then 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.
FormulaOne handles the entire mechanism of propagating the constraints to fill each element of the injection with its appropriate value.

Relations

A predicate expresses the fact that some relation holds between several objects; a relation variable expresses the same kind of thing, and is accessed with a similar notation. The difference is that a predicate is fixed at compile time, whereas a relation variable is built during the execution of the program. In the Hackers example above, the declarations
likesMac::rel Last_t & guest::rel Last_t
declare 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).
The sole purpose of guest in this example is to propagate these inequality constraints through the original constraint ~ lastname(Tim) in guest. The likesMac variable is used in a similar way.
The effect of both of these relation variables could have been achieved with explicit inequality formulas, but the resultant code would not have been as clear. As it is, the relations, together with the injections, make the FormulaOne code an almost exact transcription of the original puzzle into logical notation. A relation variable never has a fixed value; it is represented completely by constraints. However, it may be useful to think of it as a list containing the elements asserted to be in it, and carrying constraints about the elements asserted not to be in it.

Unknown Indices

We'll illustrate the use of unknown indices with another logic puzzle example. It's a puzzle by R. L. Whipkey, taken from the Dell Champion Variety Puzzle magazine, May 1987.
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)) + 1
This 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).
In general, the beauty of constraints is that the system determines which way information will flow through the variables, and all you have to do as a programmer is to state the conditions of the problem. The reason this last example is not impressive on first glance is that it is so natural. But no current implementation of Prolog, for example, could solve this problem with anywhere near the readability of FormulaOne, without an exhaustive enumeration of the values of all the variables involved.

Construction and Deconstruction of Arrays, Tuples, Lists and Unions

Data structures such as arrays, n-tuples, lists, or unions are created by the use of constructors. For instance, assume the following type and variable declarations:
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',56000
Comma 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.
Deconstruction of lists and union values always generates a test to check whether a list is non-empty or whether a union value has the correct tag:
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',56000
and
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.

Tail Recursion Elimination

FormulaOne is a language firmly based on logic. Like other declarative languages, FormulaOne does not contain explicit loop statements. Each loop has to be written as a recursive procedure. It is possible to optimize the recursion by placing the recursive call as the very last action before leaving the body of the procedure. Such recursive calls are called tail recursion. FormulaOne recognizes tail recursion in procedures (proc) and subroutines (subr), and generates a loop instead. This saves both space and time, as there are no stack frames to be allocated, and no arguments passed for the tail-recursive calls.
Consider the Pascal loop computing the factorial of n:
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.
The 'standard' recursive form of the factorial function as found in the textbooks is not tail-recursive:
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.
Note that because of constraints, FormulaOne is much more powerful than Prolog. In Prolog it is impossible to assert that tmax > = h when both of the variables are not instantiated. Consequently the implicit quantifiers in Prolog do not have to be eliminated and it is possible to perform tail recursion optimization on arbitrary predicates of Prolog.

Negation

FormulaOne has implemented a logically sound form of negation, called negation by failure. The formula ~A is computed by computing A. If A succeeds then ~A fails and vice-versa.
Negation by failure works as expected from the logical point of view only under certain restrictions on the formula which has been negated. The FormulaOne compiler must process the formula A in the procedure context and no situations which give rise to backtracking may occur within A. So, no true predicates can be called in A and symbolic variables cannot be used unless they are enclosed within an all/one/min/max formula.
Here is a very simple example of what would happen if a backtracking predicate were negated:
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.
In the first case P(x) succeeds in setting x to 1 and the formula fails because x cannot equal 1 and 2.
In the second case x is given the value 2, and P(2) is of course false so that ~P(x) succeeds and therefore the whole formula succeeds.
In a negated formula you are free to test or refer to input, output or i/o variables which are non-local to (i.e. defined outside of) the formula, but you may not modify them. You may enclose the formula which you are negating with parentheses to make it clear what the scope of the negation is. Within the scope of the negation you may define local variables as you wish. These variables are subject to the scope of variables, and their implicit existential quantification.
Take for instance the procedure Lookup looking up a salary of a specific person in a list of persons:
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.
In other words, the FormulaOne formula ~A with local variables x,...,z has the logical meaning of ~ exist x,...,z A. A legal FormulaOne formula ~A has the same meaning as the formula ~A of predicate logic only if the formula A does not contain any local variables.
As a result of the restrictions on the formulas within a negation operator, as well as because of the implicit existential quantification of local variables, the formula a <> b is not necessarily equivalent to the formula ~a = b.
For instance, if a were a symbolic variable the first formula is a constraint, whereas the second one is illegal.

More about if-then-else formulas

FormulaOne performs extensive checks in if-then-else constructs. The if-then-else formula if A then B else C end has the same meaning and the same restrictions as the formula
A & B | ~A & C
The 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.
Under the restrictions on conditions, at most one branch of an if formula can hold. Once the condition A has succeeded the else branch cannot be satisfied. Thus the compiler of FormulaOne can generate efficient test and jump code for if-then-else formulas without a double evaluation of conditions and without backtracking. Note that the condition would be evaluated twice if we had used the or (|) form instead of the if-then-else formula. Once the condition A has succeeded there can be no backtrack to the else part. Hence FormulaOne can permit assignments to the non-local output and input/output variables in the formulas B and C. Actually without this it would be impossible to write procedures returning values:
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.
On the other hand, it is impossible to lookup a person in two lists either by the procedure
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.
A backtrack is needed to search the second list. The situation can be corrected by turning the first procedure P4 to a backtracking predicate:
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.
However, the meaning of this procedure is not the same as the meaning of the first version of P4. The difference is subtle and lies in the implicit existential quantification of the local variable ss. The body of the last procedure is equivalent to the formula
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.
The meaning of more complex if-then-else formulas reduces to the above general case. The formula
if A then B end
has the same meaning as the formula
if A then B else true end
or as the formula
A & B | ~A
The 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)

Opening and Closing of Files

Ascii, Bin as well as FormulaOne's database files are opened and closed automatically without any explicit action on the part of the programmer. A file can be opened only in the subroutine context of a query or within a subroutine. This restriction is necessary from the point of view of logic because the mapping of a file name to the physical location of the file requires a hidden environment argument describing the current state of the file system of an OS.
A FormulaOne database file is automatically opened whenever its filename is converted to an input/output file argument. Consider the procedure Printfile which reads and prints a file:
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.
The file names of Ascii and Bin files are specified by strings (S). The query
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)

Cross Modular Consistency Checks

FormulaOne can automatically detects changes made to the modules and files which could render other modules using the changed modules inexecutable. This automatic cross-modular checking is a sophisticated version of the utility known as MAKE in the C-based environments.
A module is said to export all non-local constants, types, and predicates defined in it. These are collected in the so called export list, sometimes referred to as a symbol table. The information from an export list can be generated into the code of modules using the given module. When the export list of a module is changed the object code of modules using this module might become invalid.
FormulaOne automatically disables the execution of all modules compiled before a used module changes its export list. If the changes to the export list were not extensive it might be enough just to recompile all modules using the changed module. If, for instance, a parameter to a predicate changed its type, all modules using the changed module must be manually modified before they can be recompiled. FormulaOne keeps a time stamp with symbol table. The time stamp records the time of the last change to the export list. The automatic cross-modular consistency checks refer to the time stamps. For this reason it is essential that your computer system clock is always set with the current date and time.

Heap Management

During the execution of programs in symbolic languages like FormulaOne, Prolog, or Lisp, data structures are created dynamically on the heap. It is impossible to predict the pattern of heap allocation during the compile time. Consequently, there should be a mechanism for dynamically removing the unused data structures from the heap, once the heap is exhausted. This is called garbage collection. In logic programming languages such as Prolog and FormulaOne it is relatively easy to manage the heap allocation when a predicate backtracks (there are ors in the program). When a Prolog predicate is deterministic, or when we have a procedure or a subroutine in FormulaOne, there is no backtracking and the heap can quickly overflow.

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.
FormulaOne has a simple yet surprisingly powerful scheme for the garbage collection of the heap. The heap in FormulaOne is cleared automatically whenever a procedure or subroutine returns without passing (through its arguments) to its caller objects allocated to the heap during the execution of the procedure call. The procedures and predicates called during the processing of this call can allocate objects on the heap, but since the heap-allocated objects cannot be passed up it is possible to cut the heap to the state it was in the moment of the procedure call.
The automatic heap cut occurs when a procedure or a subroutine observes the following restrictions to its arguments:
  • there can be input arguments of arbitrary type; and
  • all output arguments are of the types I, L, R, file T, or enumerated types; and
  • all input/output arguments are of a fixed size.

An argument is of a fixed size whenever it is of
  • type I, L, R, file T, or enumerated type; or
  • n-tuple type (Tl, T2,...,Tn) where all types Ti are themselves of a fixed size; or
  • array type [0..n]->T or [0..n]->> T with the fixed upper bounds where the type T is of a fixed size.

External Modules

Sometimes it is necessary to invoke a subroutine written in a language other than FormulaOne. The FormulaOne compiler creates modules, which are essentially DLLs. It is possible to use DLLs created by other third party tools; we refer to these as external DLLs; or external modules. However, these DLLs do not contain all the information necessary for the FormulaOne compiler to use them correctly. In particular, the number of arguments, their types and the calling convention are necessary to correctly call the external API. This information is provided in FormulaOne source code as part of the external API; declaration:

proc ExtName({ arguments }) iff external [_cdecl |_stdcall] 'dllname':'procname'

subr ExtName({ arguments }) iff external [_cdecl |_stdcall] 'dllname':'procname'

The actual code for the external APIs does not reside in the FormulaOne module itself but in the in the external DLL. All calls to the external module are forwarded to this module. A few notes:
  • To declare the external API proc or subr is the up to the software writer.
  • ExtName can be different than procname. (FormulaOne programs will only refer to ExtName)
  • dllname is case insensitive
  • Calling convention _cdecl or _stdcall must match the calling convention of the actual code in the external DLL. If none is specified, the compiler will assume _stdcall.
  • procname: the FormulaOne compiler will attempt to do exact match, if it fails it will try to match with a decorated name. For _stdcall APIs, some limited argument checking is performed. Name decoration is assumed to be the one used by Microsoft compilers.
  • The external API must return non-0 value if it succeeds, 0 value otherwise. The return value is expected in the register EAX.

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 = &timest;
    return TRUE;
    }

Top [image] Collecting Solutions with "all" [image] Queries


F1: Queries

 Top [image] Miscellaneous Advanced Topics [image] FormulaOne Language Definition

Queries

A FormulaOne query can act as anything from a question about the truth of a simple arithmetic statement, to a request to find values of variables satisfying a formula, to the running of a program, to an access or update of a database file.

Moving to the Query Window

The first step in entering a query is to get to the query window. From the toolbar, press the Query, [image] button.

Entering and Running a Query

You enter a query by typing its text. However, most queries will be only one line. You can copy queries from your code and paste them in the query window using predefined keys, such as Ctrl-C and Ctrl-V, you specify in your preferences under Customize menu.
To run a query press Compile, [image] or Compile and Run, [image] toolbar buttons.

Compiler Errors in Queries

Result of code compilation will be displayed in the Message window. To toggle the view of Message window press [image] toolbar button.

The Results Window

Results of queries are displayed in the Result window.

Top [image] Miscellaneous Advanced Topics [image] FormulaOne Language Definition


F1: FormulaOne Language Definition

 Top [image] Queries [image] BNF Syntax of FormulaOne

FormulaOne Language Definition

  • Comments
  • Identifiers
  • Reserved Words
  • Queries
  • Overall Module Structure
  • Type Declarations
  • Constant Declarations
  • Predicate and Variable Declarations
  • Predicate Declarations
  • Variable Declarations
  • Types
  • Tuples
  • Unions
  • Array Types
  • Subrange Types
  • List Types
  • Relation Types
  • File Types
  • Terms
  • Complex Terms
  • Constant Terms
    • Integer Constants
    • Real Constants
    • String Constants
    • Character Constants
    • Array Constants
    • Declared Constants
    • Declared File Constants

  • Variables
  • Extended Variables
  • Array Element Selection
  • Field Selection
  • Anonymous Variable
  • Union Terms
  • Function Calls
  • Type Casts
  • Formulas
    • Truth Values
    • Logical Connectives
      • And
      • Or
      • Not

    • if Formulas
    • case Formulas
    • all Formulas
    • Relational Operators
    • Assignment Formulas
    • Predicate Calls
    • Variable Declarations as Formulas

In listing the format of syntactic elements, we use the notation var to mean a variable identifier. Similarly, we use Name to mean a name identifier, and type, term, and formula to mean those syntactic elements.

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.

Comments

Any text in-between a left { and right } brace is treated as a comment, and is equivalent to white space in the program. Comments can be nested; that is, a comment can appear inside another comment.
Additionally, a whole or a part of a single text line can be commented out by using a line comment. Line comment starts with a double forward slash character //. Text that has been commented out by a single line comment is completely ignored by the preprocessor.
{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

Identifiers

An identifier is a sequence of letters, numbers, and underscores (_) beginning with a letter. The last character of an identifier is the one before any character which is not one of these. Variable identifiers (which can take the place of any occurrence of the word var in the following syntax) must begin with a lower-case letter. Name identifiers (which can take the place of Name) must begin with an upper-case letter.

Reserved Words

The following identifiers have special meaning to FormulaOne and cannot be used by programmers.

Variable identifiers:
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 |  |

Name identifiers:
Nil | Print | Dupl | Pause | Len | Append
I | L | R | S | P | U

In addition, all variables with a leading underscore are reserved for the use by the compiler/preprocessor. Currently used are the following:
  • _pred : replaced during compilation with the name of the pred/proc/subr being compiled (as a string).
  • _file : replaced during compilation with the name of the file containing the code (as a string).
  • _line : replaced during compilation with the current line number (as an integer constant).
  • _addessof(Identifier) : replaced at runtime with the address of the specified identifier (as an integer constant).

Queries

General Format:

[ results [ var1, ...,varn] [ in output ] ] formula [ end ]

Where:
  • results is either all, one, min or max
  • output is either the Name of a database file, or a string constant which is the external name of a DOS file

The first, optional clause of a query is called the results clause or all/one/min/max clause. A results clause must be included if the formula can be the body of a true predicate only (that is, if it contains ors ( | ), symbolic variables, or calls to true predicates). No results clause can be included if the formula cannot be the body of a true predicate (that is, if it contains input/output variables or calls to subroutines).

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:

all [var1,...varn] [ in 'Ascii-file' ] form [end]
all [var1,...varn] [ in 'Database-file' ] form [end]
one [var1,...varn] [ in 'Ascii-file' ] form [end]
min [var1,...varn] [ in 'Ascii-file' ] form [end]
max [var1,...varn] [ in 'Ascii-file' ] form [end]
[var1,...varn] [ in 'Ascii-file' ] form [end]

The first five forms evaluate the formula form in the predicate mode. The last one evaluates the formula form in the subroutine mode. If the in clause is omitted the results go to the screen, otherwise the results of all can be redirected either to a FormulaOne database file or to an Ascii file. The remaining forms of the query allow only redirection to an Ascii file.

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'.

Overall Module Structure

General Format:

[local] typeconstdecll
.
.
.
[local] typeconstdecln
[local] preddecln
.
.
.
[local] typeconstdeclm

Where:
  • typeconstdecll ..... typeconstdecln are type or constant declarations (see below)
  • preddecll ..... preddeclm are predicate declarations (see below)

The type and constant declarations in a program can be intermixed, but all predicate declarations must come after all type and constant declarations.

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.

Type Declarations

General Format:

Namel = type

The type called Name is declared to be equivalent to the type expression to the right of the equality sign. In a program which uses Name, it acts exactly as the given type would.

Examples:

Weight_t = I
Complex_t = (R, R)
Tree_t =  Nulltree | Node(val:I, l:Tree_t, r:Tree_t)

Constant Declarations

General Format:

Name :< type = term

The constant called Name is declared to be equivalent to the term to the right of the equality sign. The term must be constant; that is, it must contain no variables, although it can contain previously-defined constants. The term must also be of the given type, and Name will be treated as a term of that type whenever it is mentioned. Examples:
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

Predicate and Variable Declarations

Predicate Declarations

General Format:

class Name(vdecl1, vdecl2 , . . . , vdecln) iff body

Where:
  • class is either pred, proc, or subr
  • vdecl1 ... vdecln are variable declarations (the formal parameters of the predicate), and
  • body is either a formula (the body or defining formula of the predicate, or the keyword external

If class is pred (the class of true predicates), then the body cannot be external; none of the formal parameter declarations can have input/output mode; may not contain calls to subrs.

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.

Variable Declarations

Format 1:

var :< type

var is declared to be an input variable of the given type. The variable has a value as soon as it is declared.

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 :> type

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 :: type

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 :. type

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.

Types

Tuples

Format 1:

var1 : type1, var2 : type2 ,...., varn : typen

Format 2:

type1, type2, ...., typen

The first kind of tuple is called a named tuple, and the second an unnamed tuple. A term of either kind of type is just a term of the form term1, term2, ...... termn where each numbered term is of the corresponding type.

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)

Unions

General Format:

Name1 [(tuple1)] | Name2 [(tuple2)] | ... | Namen [(tuplen)]

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)

Array Types

Format 1:

type1 -> type2

Where:
  • type1 is an index type (that is, an enumerated type, or a subrange type with lower bound 0)

Format 2:

type1 ->> type2

Where:
  • type1 is an index type

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]

Subrange Types

General Format:

[L] [[term1]..[term2]]

Where:
  • term1, term2 are constant terms of type L, I, or an enumerated type, and term1 is less than term2

The given subrange type expression represents the type containing all the elements from the original ordered type which are greater than or equal to term, (if given), and less than or equal to term2 (if given). If the optional L appears, elements of the new type are represented by long integers; otherwise, they are represented by integers. Examples:
Posint_t = [1..] Digit_t = [0..9]
Water_liquid_t = [-32..212]

List Types

General Format:

list type

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)

Relation Types

General Format:

rel type

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

File Types

General Format:

file type

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

Terms

Terms can be simple terms, or complex terms, which are built up from simpler terms with unary or binary operators.

Complex Terms

Format 1:

term1 oper term2

Where:
  • oper is one of the following operators: *, /, mod, +, -, and ,.

Format 2:

-term

The six binary operators and the unary operator above have the properties shown in the operators and their properties table:

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, - 5
is 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, 99
is 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')

Constant Terms

Integer Constants

An integer constant is any sequence of digits, terminated by a non-digit, which is not a part of an identifier. It can be preceded by a minus sign (-) to indicate the negative of the integer.

The constant is of type I if it is between -2147483648 to 2147483647, and of type L otherwise.

Examples:
-32760
1066
10000000000000000000000000000

Real Constants

A real constant consists of a sequence of one or more digits, possibly preceded by a minus sign (-); a decimal point; one or more digits; and possibly the letter e followed by an integer constant. Real constants are of type R.

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

String Constants

A string constant is a sequence of characters enclosed by single quotation marks ('). It has type S. Single quotation marks themselves are represented in a string by a sequence of two single quotation marks. Examples:
'A   B   C   D    '
'The word  ''word'''
'10.aaa99'

Character Constants

A character constant consists of any Ascii character, surrounded by double quotation marks ("). The double quotation mark itself is represented by an inner pair of double quotation marks within the outer pair. Character constants are of type I. Examples:
"Q"
"t1
"""""""
"j"

Array Constants

General Format:

[term1, term2, . .., termn]

Where:

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 type
term2 -> term1
or
term2 ->> term1

That 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]]

Declared Constants

A named constant declared with the constant declaration

Name :< type = term

is considered a constant term of the given type, and can be used wherever a variable of that type can be used.

Examples:
Fib200 :< L = 280571172992510140037611932413038677189525
Beatle :< S = 'John Lennon'
Pi :< R = 3.14159

Declared File Constants

General Format:

file type

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

If a variable has been declared as being of a given type, then it is a term of that type whenever it appears after that, to the end of the query or predicate body. If a variable name is used without being explicitly declared, FormulaOne will in some cases implicitly declare it: when it is being compared to a term of a definite type, or when it appears as an argument in a predicate call.

Extended Variables

Variables and declared constants of certain types have parts which can be referred to by using the element selection and field selection operators.

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.

Array Element Selection

General Format:

extvar (term)

Where:
  • extvar is an extended variable of type S, or of a type of the form type1 -> type2 or type1 - >> type2
  • term is a term of type type1

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)

Field Selection

General Format:

extvar.var

Where:
  • extvar is an extended variable whose type is a named tuple containing var as one field name, or a union type containing such a tuple as a variant tuple

If extvar is of a tuple type, one of its fields must be of the form var:type. The resulting extended variable is of that type, and refers to the field in that position in extvar. Otherwise, extvar must be of a union type. The tuple of some one of the variants of that type, with variant tag Name, must contain a field of the form vantype.

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 = 0
would be equivalent to
extvar= Name(x) & x.var = 0.
Examples:
p_data.name
p_data.b_date.month
curr vehicle.doors

Anonymous Variable

The term _ acts just like an undeclared variable: its intended type is obtained from the context in which is used and it is implicitly declared. However, each time it is used it refers to a different variable; so once used, the value it obtained cannot be referred to again because there is no "handle" for it. For this reason, _ is called the anonymous variable.

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.

Union Terms

Format 1:

Name

Where Name has been declared to be one variant of some declared union type utype

Format 2:

Name(term)

Where:
  • Name(type) for some type, has been declared to be one variant of some declared union type utype
  • term is a term of that type

In both formats, the new term is of type utype. The first format is also a constant term. Since the second format can contain variables in the contained term, it is not a constant term unless term is constant.

Examples:

Tricycle
Nulltree
Node(0, left_tree, Nulltree)
P(R(0), S('wacka'))

Function Calls

General Format:

Name(term1, term2, ..., termn-1)
Where:
  • Name is the name of a procedure or subroutine with a parameter list of the following form:
    (var1 :< type1, var2 :< type2, ..., varn-l :< typen-l, varn :> typen)
  • term1, term2, ...., termn-1.are full-value terms of type type1, type2, ..., typen-1,respectively

The resultant term is of type typen.

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):

Name(term1, term2, ..., termn-1,z)

The usual rules apply about values which can appear as arguments to the original procedure; see Variable Declarations.

Examples:
x = Sum((3, 7, 3, 2, 6, 87, 4, Nil))
y = Fib(GCD(42, 6*9) + 4)
z = Youngest(pers, arr)

Type Casts

General Format:

term:type
Where:
  • term is any full-value term

This form of term represents the term, converted into the given type. The resulting term is of that type.

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 I
the string 'abcd' is directly typecasted into the type list I, resulting in the list of integers
97,98,99,100,Nil
In 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,Nil
Consider 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.
It is important to realize, that if conversion is possible one way, it may not necessarily possible to convert it the other way, i.e. na integer can always be converted to real number but converting a real number into an integer may, or may not fail.

Formulas

In addition to giving the syntactic format of formulas in this section, we give the meaning of the formula (the conditions under which it is true or false), and a description of how the formula is processed. The meaning is intended to be a static, declarative reading of the formula. The description of processing is intended to help users trace the execution of their programs.

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.

Truth Values

Format 1:
true
Format 2:
false
Meaning:

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.

Logical Connectives

The connectives & (and), | (or), and ~ (not), can be used to build up more complex formulas from simpler ones. ~ binds more strongly than &, and & binds more strongly than |; parentheses can be used to group formulas with the desired connectives.

Thus, the formula

  P & Q | ~P & ~Q
would be treated exactly like
  (P & Q) | ((~P) & (~Q))

And

General Format:

formula1 & formula2
Meaning:

formula1 & formula2 is true if and only if both formula1 and formula2 are true.

Processing:

When the query pointer reaches A & B, it is advanced through A normally and then through B normally.

Examples
x :: L & x = 3
Fib(3, x) & Print (x)

Or

General Format:

formula1 | formula2
Meaning:

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.

Examples
x = 4 | x = 5
(x <= 1 & y = 1) | (x > 1 & y = x*Fact(x-l))

Not

General Format:

~formula
Meaning:

~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)

if formulas

Format 1:
if condformula then
thenformula
else
elseformula
end

Where:
  • condformula is a formula containing no terms which are not full-value

Meaning:

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

if condformula then
thenformula
end

This format is completely equivalent to the formula
if condformula then
thenformula
else
true
end

Format 3

if condformula then
thenformula
elsif elsifformula1 then
thenformula1
elsif elsifformulan then
thenformulan
else
elseformula
end

This format is completely equivalent to the formula

if condformula then
thenformula
else
if elsifformula1 then
thenformula1
else
if elsifformulan then
thenformulan
else
elseformula
end
end
end

Note that the else part can be omitted in this format as well.

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

case Formulas

General Form:

case term of
case-expression1 => formula1;
case-expression2 => formula2;
.
.
case-expressionn => formulan[;]
else elseformula
end

Where:

  • case-expressioni for each i, is either a term, or an expression of the form term1 | .... | termn, where each termi is a term

The first term is called the subject term; the terms in the case expressions are called case terms; and the formulas corresponding to each case expression are called case conclusions.

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 formula
subjectterm = caseterm
were 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

all Formulas

General Form:

all var1,,...., varn in listvar
formula
end

Where:
  • listvar is an output or input/output variable of a list type, or an input/output variable of a file type
  • formula is a formula which can be the body of a true predicate

listvar must be of type list type or file type for some type; type is called the element type. There must be at least one vari. If there is only one, it must be of the element type; otherwise the tuple (var1,...., varn) must be of the element type. The single variable, or the tuple of the list of variables, is called the element term.

Meaning:

An all formula is true if
  • For each set of values for vari's satisfying the formula, the value of the element term (with the variables given those values) is in the listvar;
  • Nothing else is in the listvar; and
  • The listvar is the unique such value which is in sorted order and has no duplicates. The elements of the listvar are sorted by the order on the type U, as if they had been cast into that type.

Processing:

The 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

Relational Operators

General Format:

term1 op term2
Where:
  • op is a relational operator

The relational operators are < (less than),> (greater than), <= (less than or equal to), >= (greater than or equal to), <> (not equal to), = (equal to), and in (relation, list, or file inclusion).

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

Assignment Formulas

General Format:

extvar := term

Where:
  • extvar is an extended variable which starts with a variable of input/output mode
  • term is a full-value term of the same type as the var

Meaning:

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

Predicate Calls

General Format:

Name(term1, term2,..., termn)
Where:
  • Name is a declared predicate with n formal parameters, of types type1, type2, ...,typen
  • term1, term2, ..., termn are terms of those types, called the arguments, or actual parameters, of the predicate call

If the formal parameter in position i in the declaration of Name is of input mode, the argument in that position must normally be full-value. If the parameter is of a finite type (that is, a subrange type with both bounds fixed or an enumerated type), values can be generated for it automatically if needed. Some implicit type coercions can be made to allow an argument of one type to be given to a parameter of a different type.

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)

Variable Declarations as Formulas

A variable declaration can also be used as a formula. Normally, variable declarations appear at the start of a predicate body or at the start of a query, but they can appear anywhere any formula can appear.

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

Top [image] Queries [image] BNF Syntax of FormulaOne


F1: BNF Syntax of FormulaOne

 Top [image] FormulaOne Language Definition [image] Type Conversion

BNF Syntax of FormulaOne

In the following BNF-format syntax of FormulaOne:
  • Bars ( | ) separate alternatives.
  • BNF elements in braces ({}) can be repeated zero or more times. (Braces { and } in the language itself designate the beginning and end of a comment. Comments can be nested).
  • BNF elements in square brackets ( [ , ] ) are optional.
  • "[", "|", and "]" mean those single characters, taken literally.
  • Capitalized identifiers are lexical elements.
  • Uncapitalized identifiers, and all other sequences of symbols, are tokens to be taken literally.
Query     ::= [ all | one | min | max ]
              [ Var { , Var } ] [ in [ Ident | String ] ] Formula [ end ]

Prog      ::= { Typedecl | Constdecl } { Pred }

Formula   ::= Formula2 { "|" Formula2 }
Formula2  ::= Formula3 { & Formula3 }
Formula3  ::= If | Case | All | false | true | ~Formula3 |
              Call | Term Oper Term  | ( Formula ) | Vdecl

Oper      ::= < | > | <= | >= | <> | = | := | in

Call      ::= Ident ( Term )

If        ::= if Formula then Formula
              {elsif Formula then 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 | subr
Body      ::= Formula | Forwarded
Forwarded ::= external [_cdecl | _stdcall] String : String

Top [image] FormulaOne Language Definition [image] Type Conversion


F1: Type Conversion

 Top [image] BNF Syntax of FormulaOne [image] Mode Coercion

Type Conversion

  • Legal Type Casts
  • Automatic Type Coercion
  • Polymorphic Predicates

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

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

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

Legal Type Casts

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

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

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

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

  • Pairs (a, b):
    P(a', b')
  • integers n:
    R(n), -231 <= n <= 232-1
  • Long integers n:
    R(n), -231 <= n <= 231-1
  • Real numbers n:
    R(n)
  • Tuples (a1, ..., an):
    P(a1', P( ..., P(an-1' an')...))
  • Union terms A, where A is the n^th alternative of the union (numbered from 0):
    R(n)
  • Union terms A(a1, ..., am), where A is the n^th alternative of the union (numbered from):
    P(R(n), P(a1', P(..., P(am-l', am')...)))
  • Arrays with n elements, [a1, ..., an] and strings with Len(string)= n:
    P(R(n), P(a1', P(..., P(an', R(0))...)))
  • Injections with n elements, [al, ..., an]:
    P(R(n), P(a1', P(..., P(an', R(0))...))), where no two ai' are the same.
  • Terms n of subrange type [a.. b]:
    R(n), where a <= n <= b
  • The list element Nil:
    R(0)
  • Lists (h, t):
    P(h', t')
  • Relations containing al, ..., an:
    P(a', P(..., P(an-1', P(an', R(0)))...))
  • Files containing records rl, ..., rn, with file pointer after ri:
    P(P(r1', ..., P(ri-1', ri')...),
    P(ri + 1', ...,P(rn-1', rn')...))

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

Automatic Type Coercions

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

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

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

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

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

Type coercion table. T represents any type.
Wider Type | Narrower Type | Test
U | T | Fits T?
[0..]->T | [0..n]->T | Upper bound n?
[0..n]->T | [0..n]->>T | All elements different?
R | L | Unlimited Integer
R | I | Integer form -231 to 231-1?
L | I | Integer from -231 to 231-1?

Polymorphic Predicates

  • Print
  • Len
  • Append
  • in
  • Dupl
  • _AllDifferent
  • _AllAscending
  • _Ascending
  • _AllDescending
  • _Descending

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

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

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

Print

Print acts as a procedure with any number of input parameters, of any types Tl to Tn:
proc Print(xl :< Tl, ..., xn :< Tn)
The type information is used by Print to determine how it should print the arguments - as strings, arrays, tuples, etc.

Len

Len acts as each of the following predicates and procedures, for any type T:
proc Len(a :< [0..n]->T, len :> I)
pred Len(a::[0..n]->T, len :> I)
proc Len(a :< [0..]->T, len :> I)
pred Len{a::[0..]->T, len :> I)
proc Len(s :< S, len :> I)
proc Len(l :< list T, len :> I)
pred Len(l :: list T, len :: I)
With arrays, Len returns the number of elements in the array (recall that flexible arrays ave a known number of elements at run time, and that while the elements of symbolic arrays may be unknown, the number of elements is always known). With strings, Len returns the length of the string. With lists, Len returns the number of elements in the list, not counting Nil. The symbolic list predicate form of Len behaves exactly as the following predicate, for every T:
pred Len(l :: list T, len :: I) iff
    len = 0 & l =  Nil |
    len > 0 &
    l = (_,t) & Lent(t, len-1)

Append

Append acts as each of the following procedures and predicates, for every T:
proc Append(s1 :< S, s2 :< S, s_out :> S)
proc Append(l1 :< list T, l2 :< list T, l_out :> list T)
pred Append(l1 :: list T, l2 :: list T, l__out :: list T)
Append returns the string or list consisting of the concatenation of the first two parameters in its call. The last version of Append behaves exactly as the following predicate, for every T:
pred Append (l1 :: list T, l2 :: list T, l_out :: list T) iff
    l1 = Nil & l_out = l2 | l1 = (h, t) &
    l_out = (h, l_aux)
    & Append(t, l2, l aux)

in

The in operator is not exactly a predicate, but it behaves in a polymorphic way which is similar to that of the polymorphic predicate. If we think of every formula of the form xl in x2 as being a call to a predicate In(xl, x2), then this predicate In acts as each of the following predicates, for every T:
proc In(x :< T,	l :< list T)
pred In(x :> T,	l :< list T)
pred In(x :: T,	l :: list T)
proc In(pat :< S, s :< S)
The first list predicate form has the effect of testing the membership of x in l. The second form assigns to x each of the members of l on backtracking. The third form behaves exactly as the following predicate, for every T:
pred In(x :: T, l :: list T) iff
    l = (h, t) & ( h = x | In(x, t))
The form with string-typed arguments is a pattern matching form, which matches the wild-card character "*" to any sequence of text (possibly empty), and any other characters to themselves. For instance, all the following formulas should be true: '*a*a' in 'lava' '*a*a' in 'ada' '*a*a' in 'llama' \ '*ula*' in 'FormulaOne' '*log*' in 'Prolog'

Dupl

Dupl acts as a procedure of the following form, for every type T:
proc Dupl(n :< I, x :< T, array :> [0..]->T )
It has the effect of putting into array, an array constructed of n copies of the value x.

_AllDifferent

_AllDifferent acts as a predicate with any number of logical parameters, for every type T:
pred _AllDifferent(x1::T, x2::T, x3::T, ..., xn::T)
The _AllDifferent predicate places n(n-1)/2 binary constraints on n variables, ensuring no two variables can have the same value.
pred _AllDifferent(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 <> x2 & x1 <> x3 & ... x1 <> xn &
               x2 <> x3 & ... x2 <> xn &
                              x3 <> xn
For example, the following query
    all x::[1..2] & y::[1..4] & z ::I[1..2] & _AllDifferent(x,y,z)
will generate the following solutions:
x = 2
y = 3
z = 1
___ Solution: 1 __________________________________

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

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

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

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

_AllAscending

_AllAscending acts as a predicate with any number of logical parameters, for every type T which allows comparison constraints for "greater than". These types currently include I, L, R and S. The _AllAscending predicate places n-1 binary constraints on n variables, ensuring the variables have ascending values.
pred _AllAscending(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 < x2 & x1 < x3 & ... x1 < xn
For example, the following query
   all x::[1..2] & y::[1..4] & z ::I[1..4] & _AllAscending(x,y,z)
will generate the following solutions:
x = 1
y = 2
z = 3
___ Solution: 1 __________________________________

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

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

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

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

_Ascending

_Ascending acts as a predicate with any number of logical parameters, for every type T which allows comparison constraints for "greater or equal than". These types currently include I, L, R and S. The _Ascending predicate places n-1 binary constraints on n variables, ensuring the variables have ascending values.
pred _Ascending(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 <= x2 & x1 <= x3 & ... x1 <= xn
For example, the following query
   all x::[1..2] & y::[1..4] & z ::I[1..2] & _Ascending(x,y,z)
will generate the following solutions:

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

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

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

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

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

_AllDescending

_AllDescending acts as a predicate with any number of logical parameters, for every type T which allows comparison constraints for "greater than". These types currently include I, L, R and S. The _AllDescending predicate places n-1 binary constraints on n variables, ensuring the variables have ascending values.
pred _AllDescending(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 > x2 & x1 > x3 & ... x1 > xn
For example, the following query
all x::[1..3] & y::[1..3] & z ::I[1..3] & _AllDescending(x,y,z)
will generate the following solutions:
x = 3
y = 2
z = 1
___ Solution: 1 __________________________________

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

_Descending

_Descending acts as a predicate with any number of logical parameters, for every type T which allows comparison constraints for "greater or equal than". These types currently include I, L, R and S. The _Descending predicate places n-1 binary constraints on n variables, ensuring the variables have ascending values.
pred _Descending(x1::T, x2::T, x3::T, ..., xn::T) iff
    x1 >= x2 & x1 >= x3 & ... x1 >= xn
For example, the following query
all x::[1..2] & y::[1..2] & z ::I[1..2] & _Descending(x,y,z)
will generate the following solutions:
x = 1
y = 1
z = 1
___ Solution: 1 __________________________________

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

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

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

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

Top [image] BNF Syntax of FormulaOne [image] Mode Coercion


F1: Mode Coercion

 Top [image] Type Conversion [image] Constraints

Mode Coercion

  • Identities
  • Predicate Calls

When a variable of one mode is given in a position where a variable of another mode is expected, mode coercion goes on in much the same way as type coercion does.

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.

Identities

In processing the identity formula a = b, the action actually performed depends on the modes of the terms a and b. For the purposes of the following table, we can consider output variables after their first assignment as input variables.

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.

  • a input, b input: a and b are compared.
  • a input, b output: at compile time, b is made to refer to the same value (in memory) as a.
  • a input, b symbolic: if b has a value, it is compared with a; otherwise, b gets the value of a if compatible with the constraints on b.
  • a input, b input/output: a and b are compared.
  • a output, b output: b is backtracked out if possible, and the values are assigned to a.
  • a output, b symbolic: if b has a value, it is assigned to a; otherwise, it is backtracked out if possible, and the values are assigned to a.
  • a output, b input/output: a is assigned a copy of the value of b.
  • a symbolic, b symbolic: an equality constraint is put between the two variables.
  • a symbolic, b input/output: if a has a value, it is compared with b; otherwise, a gets a copy of the value of b if compatible with the constraints on a.
  • a input/output, b input/output: a and b are compared.
The operation of "backtracking out" a variable a is possible when the type of a has a small finite number of elements (i.e., an enumerated type, a subrange type with fixed upper and lower bounds, or a finite array type etc,); or when a is a symbolic variable of some other integral type (L, I, or a non-fixed subrange type) which is constrained to be in a small finite range.

If the system attempts to backtrack out a variable and fails, it raises the "too many backtracks" run-time error.

Predicate Calls

We can illustrate the mode coercion actions associated with predicate calls by a simple example. We have a predicate declared by
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)

Mode coercion on predicate table summarizes these actions. Usually, if the modes do not agree an auxiliary variable of the correct mode is implicitly declared. Most of the work of mode coercion is then passed off to the mechanism for resolving identity formulas (see previous section). The identity formula is computed either before or after the predicate call with the auxiliary variable, as appropriate.
Top [image] Type Conversion [image] Constraints


F1: Constraints

 Top [image] Mode Coercion [image] Runtime Library

Constraints

When a relational operator formula involving symbolic variables is computed, it may cause a constraint to be placed on the environment. The kinds of constraints that can be placed there are summarized in this section.

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 <>).

  • Sum constraint of long integers with coefficients:
    al*xl + a2*x2 + . . . + an*xn  rel a
    where al, a2, ..., an, a are long integer values, and xl, x2, ..., xn are symbolic variables of type L.
  • Constant value constraint:
    x rel a
    where x is a symbolic variable of type I, R, S, or a subrange type, and a is some value of the same type.
  • Numeric variable constraint:
    x rel y + a
    where x and y are symbolic variables of type I, R, or a subrange type, and a is a numeric value of the same type.
  • Array index constraint:
    z(x+a) = y
    where 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.
  • Relation variable constraints:
    b in x
~b in x
    where 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.
  • Simple equality or inequality constraints:
    x = b
x <> b
    where 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.

Top [image] Mode Coercion [image] Runtime Library


F1: Runtime Library

 Top [image] Constraints

Runtime Library

  • RtlSystem
  • RtlLtoS
  • RtlStoL
  • RtlLtoSx
  • RtlStoLx
  • RtlReverse
  • RtlSortAscending
  • RtlSortDescending
  • RtlToUpperString
  • RtlToLowerString
  • RtlParseString
  • RtlGetCommandLine
  • RtlGetCommandArguments
  • RtlGetCutPoint
  • RtlSetCutPoint
  • TTYSetTitleBar
  • TTYKeyHit
  • TTYKeyWait
  • TTYKeyGet
  • TTYGetString
  • TTYShow
  • TTYHide
  • DbPut
  • DbGet
  • DbAccess
  • DbSkip
  • DbRewind
  • DbDelete
  • DbEof
  • DbEofSet
  • DbTruncate
  • DbFlush
  • DbSeek
  • DbSeekGt
  • DbSeekLt
  • DbSeekNext
  • DbSeekNextEq
  • DbSeekPrev
  • DbSeekPrevEq
  • DbSeekFirst
  • DbSeekLast

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.

RtlSystem

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.

RtlLtoS

Convert an integer number to a decimal string.

Syntax:

    RtlLtoS(x:<L, s:>S)

Note: Conversion implicitly assumes a decimal number.

RtlLtoSx

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.

RtlStoL

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.

RtlStoLx

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

RtlReverse

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]

RtlSortAscending

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’.
Sorted list 3,1,5,4,7,9,3,2, Nil becomes 1,2,3,3,4,5,7,9,Nil.
Sorted array [2,1,5,6,0] becomes [0,1,2,5,6]

RtlSortDescending

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’.
Sorted list 3,1,5,4,7,9,3,2, Nil becomes 9,7,5,4,3,3,2,1,Nil.
Sorted array [2,1,5,6,0] becomes [6,5,2,1,0]

RtlToUpperString

Convenience API. Convert an ASCII string to upper case.

Syntax:

    RtlToUpperString(sin:<S, out:>S)

RtlToLowerString

Convenience API. Convert an ASCII string to lower case.

Syntax:

    RtlToLowerString(sin:<S, out:>S)

RtlParseString

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]

RtlGetCommandLine

Retrieve the command line string.

Syntax:

    RtlGetCommandLineString(cmdline:>S)

Note: Routine typically used by standalone executables.

RtlGetCommandArguments

Routine parses the command line string and returns an array of strings.

Syntax:

    RtlGetCommandArguments(cmdars:>[0..]->S)

Note: Routine typically used by standalone executables.

RtlGetCutPoint
RtlSetCutPoint

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.

TTYSetTitleBarText

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.

TTYKeyHit

Check if any user key input present.

Syntax:

    proc TTYKeyHit()

Note: Succeeds if the keyboard buffer is not empty, fails otherwise.

TTYKeyWait

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”.

TTYKeyGet

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.

TTYGetString

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.

TTYShow

Show the console window.

Syntax:

    proc TTYShow()

Note: The call allows to display the console previously hidden.

TTYHide

Hide the console window.

Syntax:

    proc TTYHide()

Note: The call allows to hide the console at runtime.

DbPut

Store a record at the current position.

Syntax:

    proc DbPut(f:.file T, x:<T)

DbGet

Current record is accessed and the file is advanced by one record.

Syntax:

    proc DbGet(f:.file T, rec:>T)

DbAccess

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

DbDelete

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.

DbSkip

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.

DbRewind

Position the file at the beginning, always succeeds.

Syntax:

    proc DbRewind(f:.file T)

DbEof

Test for end of file. Call succeeds if there are no more records left after the current position.

Syntax:

    proc DbEof(f:.file T)

DbEofSet

Positions the file at the end, always succeeds.

Syntax:

    proc DbEofSet(f:.file T)

DbTruncate

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.

DbFlush

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)

DbSeek

Position the DB file pointer to the record containing the key value.

Syntax:

    proc DbSeek(f:.IndexFile,keyvalue:<T)

DbSeekNext

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.

DbSeekNextEq

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.

DbSeekGt

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.

DbSeekPrev

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.

DbSeekPrevEq

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.

DbSeekLt

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.

DbSeekFirst

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)

DbSeekLast

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)

Top [image] Constraints