Top
Database Files
Miscellaneous Advanced Topics
French
German
Italian
Spanish
Portuguese
Japanese
Korean
Chinese
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 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.
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).
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
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.
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
Database Files
Miscellaneous Advanced Topics