Top
Queries
BNF Syntax of FormulaOne
French
German
Italian
Spanish
Portuguese
Japanese
Korean
Chinese
We also use the convention that anything enclosed within roman-font square brackets ([...]) is an optional element, that can be left out. This is not to be confused with the typewriter-font square brackets ([...]), which indicate actual square brackets as typed into a program.
See BNF-format for precise syntax of FormulaOne. BNF-format presents the syntax less formally for purposes of readability.
{Examples of comments: }
{This is a multiline comment:
line 1
line 2
// } this end of comment not visible by the preprocessor!
} // This is the real end of the multiline comment
// This line is commented out
Pi = 3.14158 // We need to fix this
| all | one | min | max | in | true | false |
| list | pred | if | then | else | elsif | end |
| iff | file | local | pred | proc | subr | mod |
| rel | use | external | case | of |
| Nil | Dupl | Pause | Len | Append | |
| I | L | R | S | P | U |
The output of the query is a list of the possible values of the vars listed. If no results clause is given, or no vars are listed, then the values of all variables appearing in the query are listed.
If results is all, all solutions are listed; if it is one, only the first solution found is listed; if it is min, only the solution of the minimal value is listed; if it is max, only the solution of the maximum value is listed.If output is a database file name, the output is written to the database file; whatever was in the file before is destroyed. Otherwise, output is in results-window format. If output is a string constant, that string is taken as a file name and the output is written to a file. If no in clause is given, or the entire results clause is omitted, output is to the results window.
FormulaOne permits redirection of results of a query to a database file or to an Ascii file in the predicate mode; and to an Ascii file in the subroutine mode. The complete syntax of queries is as follows:If the list of variables vari is given, only the variables specified in the list are displayed on the screen or are redirected to the file. If the list is not given, all the variables occurring in the query are displayed or redirected.
In the following example, the query does not contain a list of variables:in 'myfile' Process()The procedure Process can contain calls to other procedures (such as Print) and the output will be redirected to the Ascii file called 'myfile'.
Each type, constant, and predicate declared is visible to the entire program module. Each is also visible to other program modules which use the module, unless the declaration has been preceded by the keyword local.
Examples:
Weight_t = I Complex_t = (R, R) Tree_t = Nulltree | Node(val:I, l:Tree_t, r:Tree_t)
Pi :< R = 3.14159265358979 Answer :< I = 42 One_tree :< Tree_t = Node(Answer, Nulltree, Nulltree) Name :< S = 'Call me Ishmael' Fact10 :< I = 10*9*8*7*6*5*4*3*2*1 List10 :< list I = 1,2,3,4,5,6,7,8,9,10,Nil
If class is proc (procedure) or subr (subroutine), then none of the formal parameter declarations can have symbolic mode; if the body is a formula, it cannot contain any symbolic variables, or's, or calls to true predicates, except within an all formula. In addition, if class is proc and the body is a formula, it cannot contain any calls to subrs.
In a local variable, the possible values for the variable are generated automatically by backtracking at the point of declaration, if it can have only a small finite number of values. Local input variables can therefore appear only in true predicates.
Format 2:var is declared to be an output variable of the given type. The parameter or variable has no value when the predicate is entered, but must obtain a value before it is exited, at the time of its first use. If it is given a value in one branch of an if, case, or or formula, then it must be given a value in branches of that formula. If the first use of the variable is not as an argument to another predicate in the position of an output parameter, or in an equality formula in which it is assigned a full value, then the possible values are generated automatically at its first use, if it has a small finite number of possible values.
Format 3:var is declared to be an symbolic variable of the given type. It is not known at compile time whether the parameter or variable has a value at any particular point in the predicate, although at run time this is known. If a symbolic variable has no value, the running program will keep track of all the constraints put on that variable by previous formulas, such as that it is equal to another variable, that it is less than some expression, etc. If it can deduce from the constraints that it can have only one value, the program will assign it that value; if it can deduce that it cannot have a value, the program will make a failure backtrack.
Format 4:var is declared to be an input/output variable of the given type. In a parameter, this means that the variable has a value when the procedure is entered (in the same way that an input variable does). However, an input/output parameter can be assigned a new value during the course of the predicate, by the := operator (see section 21.6, Formulas), or by passing it as an argument to an output or input/output parameter. The new value, if one has been given, is returned to the calling predicate at the end of the predicate execution. A local input/output variable acts as an output variable in that it must be assigned a value on its first use. But it can also be passed as an output or input/output argument, and reassigned with the : = operator.
If a variable var is declared to be of a named tuple type, then the terms var.var1 through var.varn are valid terms, and refer to the particular parts of the value of var.
Examples:Date_t = (year:I, month:[1..12], day:[1..31]) Complex_t = (R, R) Person_t = (name:S, age:I, birthdate:Date_t)
A union type expression is a series of two or more variant type expressions, separated by bars. Each variant represents one structure which a variable of that type can have. The Name of the variant is called the variant tag, and the tuple in the variant, if it exists, is called the variant tuple. A term of the type above is a term of the form Name, if Name is one of the variants with no tuple, or of the form Name(term), if Name is one of the variants with a tuple and term is of that tuple type.
The variant tuples can contain fields of the type being declared. Such unions are called recursive unions. Unions with no tuples in any of their variants are called enumerated types.Examples:
Colour_t = Red | Yellow | Green | Blue Vehicle_t = Tricycle | Car (doors: I, engine_size: I ) | Bicycle(gears: I ) | Motorcycle Tree_t = Nulltree | Node(I, Tree_t, Tree_t)
Format 2:
A variable of an array type is a set of values of type type2 indexed by members of type type1. The first form given above is called a simple array; the second form is called an injection. If type1 is [0..], then the array is flexible, meaning that its number of elements is determined only at execution time; otherwise, the array has a fixed number of elements.
An array constant of either of the array types above is of the form [term1term2, ...,termn]. Unless the array is flexible, n must equal the number of elements in type1.If a variable, say x, is declared to be of one of the array types above, then the term x(term), where term is of type type1; is a valid term. This term is of type type2. An injection is identical in use to a simple array; however, variables declared to be injections have the additional constraint that no two members of the array can have the same value.
Examples:Persarr_t = [0..33] -> Person_t Matrix_t = [0..2] -> [0..3] -> I Wavelength_t = Colour_t -> R Dperm_t = [0..9] ->> [0..9]
Posint_t = [1..] Digit_t = [0..9] Water_liquid_t = [-32..212]
A variable of the list type above can take on the value Nil, or any value consisting of a term of the given type paired with another term of the list type; that is, Nil or any term of the form (term1, term2,..., termn, Nil) where term1 .... termn are terms of the given type. Nil is a special reserved name which has no fixed type of its own, but can be used as a term of any list type.
Examples:Guests_t = list Person Sum_t = list I Csum_t = list (R, R)
A variable var declared to be of the above relation type stands for a property of terms of the type. It can be used in declared relation formulas of the form [~] term in var, where term is a term of the given type. This denotes that a term of the given type has the property represented by var.
A variable of a relation type can only be passed as a parameter and used in declared relation formulas. There are no terms of any relation type, except variables declared to be of that type. Examples:Ismale_t = rel Person_t Isprime_t = rel I
A parameter of the above type stands for an ordered list of the given type, represented on external storage. Such a variable can be passed to the file procedures, or used as a predicate.
Constant terms of the file types . Also, any string containing a file name is a file constant, which can be passed as an argument to a parameter of type Ascii, pr Bin. This latter kind of file constant can be coerced into type Ascii or Bin when being passed to the various database polymorphic procedures in F1RTL (FormulaOne Run Time Library). File constants can appear only in queries. Examples:P_data_ft = file P_data_t Marriage_ft = file (husb:P_data_t, wife:P_data_t) Lasttag_ft = file Tag_t
| Operator | Precedence | Associativity |
| * | 4 | Left |
| / | 4 | Left |
| mod | 4 | Left |
| + | 3 | Left |
| - (binary) | 3 | Left |
| - (unary) | 2 | Left |
| , | 1 | Right |
Here integral means L, I, or a subrange type; and arithmetic means either integral or R. Most of these operators have the obvious meanings. "-" can be used both as a binary operator, meaning the difference between the two terms, or as a unary operator, meaning the negative of the term, mod is the modulo or remainder operation, which results in the remainder upon division of the left-hand term by the right-hand term.
The "," operator is the data constructor operator of pairing. It is analogous to the CONS function of LISP. If term1 is of type1 and term2 is of type2, then the pair term (term1, term2) can be of type (type1, type2).We encourage programmers to use parentheses in terms with many operators, to make it clear which operators go with which terms. However, if no parentheses are supplied, FormulaOne parses terms by rules of precedence.
Each operator has a precedence and an associativity, given by the table above.If a term is flanked by two operators of unequal precedence, it is bound more strongly by the higher-precedence one; thus
x + y * z, - 5is parsed as
((x + (y * z)), (-5))If a term is flanked by two operators of equal precedence, it is bound more strongly by the left-hand one if they are left-associative, the right-hand one if they are right-associative; thus
x * y * z, a - b + c, 99is parsed as in the Operators and Their Syntactic Properties table below.
(((x * y) * z), (((a - b) + c), 99))
| Operator | Meaning | Arity | Argument Type | Resultant Type |
| * | multiplication | binary | arithmetic | arithmetic |
| / | division | binary | arithmetic | arithmetic |
| mod | modulo | binary | integral | integral |
| + | addition | binary | arithmetic | arithmetic |
| - | subtraction | binary | arithmetic | arithmetic |
| - | unary minus | unary | arithmetic | arithmetic |
| , | pairing | binary | any | any |
Examples:
8*s + 6*b
('Heather', Female,
(1921 + 40, 7, 2), (0, 1, 1), 'Musician')
The constant is of type I if it is between -2147483648 to 2147483647, and of type L otherwise.
Examples:-32760 1066 10000000000000000000000000000
The e part of a real constant stands for the exponent of the power of 10 by which the numeric part is to be multiplied. For example, the constant -9.99e50 stands for -9.99 * 1050, and the constant 0.0005e-6 stands for 0.0005 * 10-6.
Examples:3.1415926 -22.0 -9.99e50 0.0005e-6
'A B C D ' 'The word ''word''' '10.aaa99'
"Q" "t1 """"""" "j"
term1, term2,...., termn are terms of the same type type.
If type2 is an array index type with n elements, then the given term can be used as a term of typeThat is, the term stands for an entire array, each termi standing for the element of the array subscripted by one of the n terms of type2.
Examples:['Sally','Heather','Isadora'] [0,0,0,0,7] [[7,6],[3,5,9],[4,8,2],[1,2,3,4]]
Fib200 :< L = 280571172992510140037611932413038677189525 Beatle :< S = 'John Lennon' Pi :< R = 3.14159
A parameter of the above type stands for an ordered list of the given type, represented on external storage. Such a variable can be passed to the file procedures, or used as a predicate.
Constant terms of the file types. Also, any string containing a file name is a file constant, which can be passed as an argument to a parameter of type Ascii, pr Bin. This latter kind of file constant can be coerced into type Ascii or Bin when being passed to the various database polymorphic procedures in F1RTL (FormulaOne Run Time Library). File constants can appear only in queries. Examples:P_data :< P_data_ft = 'pdata.dbs':P_data_ft Marriage_ft = file (husb:P_data_t, wife:P_data_t) Lasttag_ft = file Tag_t
Variables or constants followed by a sequence of zero or more such operators are called extended variables. Note that the term 'extended variable' includes all variables and constants themselves.
The term, in this kind of extended variable, is called the index of the array. If the index is not of the index type of the array, and cannot be coerced into that type, the formula containing the term will fail. The resulting extended variable is of type typej, and refers to the term-th element of the array extvar.
Strings can also be indexed. The index must be an integer greater than or equal to 0 and less than the length of the string. Such an extended variable stands for the term-th character in the string (numbered starting at zero), and is of type I.If extvar is also an array element term, the consecutive index expressions (x)(y) can be grouped together in a single set of parentheses, separated by a comma, as (x, y).
Examples:pers_arr(0) sieve(curr) matrix(i)(j) matrix(i, j)
Again, the resulting extended variable is of that type, and refers to that field. When such an extended variable is used, a test is implicitly inserted that the variant named by Name is the one in the value of extvar.
For example,extvar.var = 0would be equivalent to
extvar= Name(x) & x.var = 0.Examples:
p_data.name p_data.b_date.month curr vehicle.doors
The anonymous variable is useful in matching parts of a larger term which the programmer does not need to refer to later. It acts as a placeholder whose matched value is immediately discarded.
Examples:
Tricycle
Nulltree
Node(0, left_tree, Nulltree)
P(R(0), S('wacka'))
All but the last of the formal parameters to the procedure must be of input mode, and the last must be of output mode. The value of the term is the value that z would have after the following procedure call (assuming that z had not been assigned a value before):
x = Sum((3, 7, 3, 2, 6, 87, 4, Nil)) y = Fib(GCD(42, 6*9) + 4) z = Youngest(pers, arr)
Since different types represent different subsets of the universal type U, it may not always be possible to cast a given term into a given type. If it is not, the formula containing the term will fail and cause a backtrack.
Examples:curr_colour :L Print(foo:U) 'abcd':list I [4, 5, 6]:[0..]->I:list Ithe string 'abcd' is directly typecasted into the type list I, resulting in the list of integers
97,98,99,100,NilIn the last example term [4, 5, 6] is first typecasted into an array of integers and subsequently typecasted into a type list I. Result would be a list of integers:
4,5,6,NilConsider the following code fragment
AR = [0..]->[0..]->R
LS = list (list I)
LCONST :< LS = (1,2,3,4,Nil),(5,6,7,Nil),(15,Nil),Nil
proc Cast(x :< LS) iff
y = x:AR & Print(y)
Running the query
Cast(LCONST)
will result in printing
y = [[1.,2.,3.,4.],[5.,6.,7.],[15.]]
thus converting a list of list I into an array of arrays of R. Several conversions were carried out simultaneously.
First, each element of the list LCONST, itself a list I, was converted into an array of I, and subsequently each
element of the array was converted into a real number, R. This conversion was repeated for each element of the list LCONST.
At this point a list of arrays of R was constructed, and the list was then converted into an array of arrays, the
final value being assigned to y.In the Processing sections, we assume the existence of a query pointer pointing to the current position in the formula being processed, and an environment containing all constraints and other information about the current values of variables. Backtrack points and their corresponding skip points are sometimes set up during the course of processing.
When the query pointer is advanced to a backtrack point, it is skipped to the corresponding skip point. The operation of backtrack is assumed to mean the following: the query pointer is reset to the last backtrack point set up, it and its corresponding skip point are deleted, and everything in the environment from the time the backtrack point was set up is removed.true is always true; false is always false.
Processing:When the query pointer reaches true, it passes over it with no change to the environment. When it reaches false, a backtrack is performed.
Thus, the formula
P & Q | ~P & ~Qwould be treated exactly like
(P & Q) | ((~P) & (~Q))
When the query pointer reaches A & B, it is advanced through A normally and then through B normally.
Examplesx :: L & x = 3 Fib(3, x) & Print (x)
formula1 | formula2 is true if either formula1 or formula2 are true.
Processing:When the query pointer reaches A | B, a backtrack point is set up just before B, with the corresponding skip point just after B. Then the query pointer is advanced normally through A.
Examplesx = 4 | x = 5 (x <= 1 & y = 1) | (x > 1 & y = x*Fact(x-l))
~formula is true only if formula is false.
Processing:~formula is completely equivalent to the following if formula:
if formula then
false
else
true
end
Examples:
~Longname('Smith')
~DbEof(p_data_file)
An if formula is true if both its condformula and its thenformula are true, or if its condformula is false and its elseformula is true.
Processing
When the query pointer reaches an if formula, the condformula is tested, as if it were a separate query. If it succeeds, the entire if formula is effectively replaced by the thenformula, and the query pointer is set to the beginning of that formula; if it fails, the formula is replaced by the elseformula and the pointer is set there.Format 2
Format 3
Examples
if l = Nil then
sum = 0
else
l = (h, t) & sum = h + Sum(t)
end
...
if n < 0 then
f = 0
elsif n <= 1 then
f = l
else
f = n * Fact(n-l)
end
Where:
The FormulaOne compiler must be able to deduce that at least one case term must match the subject term. For example, if the subject term is of a union type, the case terms must include all members of that type, unless an else clause is included. The case terms must be mutually exclusive: no two case terms can be such that a subject term can match both of them.
The subject term must be full-value, and must be of a union, subrange, string or list type. The case term must be of the same type as the subject term, but can contain variables.Meaning:
A case formula is true if the subject term is equal to one of the case terms, and the corresponding case conclusion is true; or if the subject term is not equal to any of the case terms, and the else formula is true.Processing:
When the query pointer reaches a case formula, the subject term is matched against each of the case terms, as if the formulasubjectterm = casetermwere being evaluated. When one of these matchings succeeds (possibly altering the environment), the entire case formula is effectively replaced by the corresponding case conclusion formula, and the pointer is set to the beginning of that formula.
Examples:
case digit of
0 => name = 'zero';
1 => name = 'one';
2 => name = 'two';
3 => name = 'three';
4 | 5 | 6 => name = 'several'
else name = 'many'
end
case string of
'John' => name = 'Lennon';
'George' => name = 'Harrison';
'Paul' => name = 'McCartney';
'Ringo' => name = 'Starr';
else name = 'not a Beatle'
end
Meaning:
An all formula is true ifThe formula is processed as a sub-query. Each solution of the var^s is obtained in turn and inserted into the file (or into memory, for lists) in sorted order.
Examples:
all x in men_file
P_data(x) &
x = (_, Male, _, _, _)
end
all x, square, cube in triple
x::[1..20] &
square = x * x &
cube = x * square
end
The two terms related by the first six operators must normally be of the same type, though they can sometimes be different; see the section on automatic mode coercion. The right-hand term of an in formula must be of a relation, list, or file type; the left-hand term must be of the element type of the right-hand term.
The first four relational operators can be used only between terms of a type which is ordered (that is, I, L, R, S, or a subrange or enumerated type).Meaning:
The first six relational operators have the obvious meaning: that the left-hand term is in the given relation with the right-hand term, in means that the left-hand term is a member of the right-hand term (if it is of a relation or list type) or is a record in the right-hand term (if it is of a file type).Processing:
When the query pointer reaches a relational operator formula, the system tries to integrate the information in the formula into the information in the environment. If the new formula is inconsistent with the environment (for example, x = 1 when the environment contains x = 0), a backtrack is performed.If all the variables in the formula are full-value, the formula will act as a simple test. Otherwise, the new formula may act as an assignment of a value to a variable, or it may cause new constraints to be put into the environment. This may in turn cause previous constraints to be eliminated, or cause symbolic, or output variables to obtain values where they had none before.
Examples:
name = 'zero'
8*3 + 6*b <= 46
p_data = ('Sally', Female, (1957, 10, 6), (0, 1, 1),'')
sally_p_data in guests_r
No matter what the value of the extvar was beforehand, its value becomes the value of term. If extvar is a field-selection or element-selection term, only that part of the variable is changed. Syntactically, if a formula contains var := term, all references to var after it in the formula will effectively refer to an auxiliary variable which has the value of term.
Processing:The value of the extended variable in the environment is reassigned to the value of the term.
Examples:vehicle_arr(3).doors := Default_doors iosum := iosum + 5 error_s := 2
Database files which are declared as being used by a module can be used as predicates within the module. In this case, the formal parameters are the fields of the tuple which was used to define the records in the file.
Meaning:For program predicates, the predicate call is true if and only if the defining formula of the predicate is true when the formal parameters are given the values of the arguments. For database-file predicates, the call is true if and only if the list of arguments is equal to one of the records in the file. If only one argument is given, it must be a tuple variable equal to one of the records.
Processing:When the query pointer reaches a predicate call, the call is expanded into the defining formula of the predicate, with each parameter replaced by the corresponding argument. Every local variable of the predicate which has the same name as a variable already in the environment, is renamed to some new name throughout the expanded formula. For database-file predicates, a call is processed by scanning the file and trying to match the argument list to a record.
Examples:Sum((3, 2, 6, Nil), s) Print( 'Foo' ) DbInsert(x, tree. left) P_data(rec)
Meaning:
A variable declaration is true if the variable has a value which is of the type given in the declaration.Processing:
When the query pointer reaches a variable declaration, information about the type and mode of the variable is put into the environment. It is also used extensively by the FormulaOne compiler in checking programs and queries for correct format.Examples:
x :< I tree :. Tree reversed :> list U
Top
Queries
BNF Syntax of FormulaOne