Top Database Files Miscellaneous Advanced Topics
French French German German ItalianItalian SpanishSpanish PortuguesePortuguese JapaneseJapanese KoreanKorean ChineseChinese

Collecting Solutions with "all"


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


Top Database Files Miscellaneous Advanced Topics