Top Queries BNF Syntax of FormulaOne
French French German German ItalianItalian SpanishSpanish PortuguesePortuguese JapaneseJapanese KoreanKorean ChineseChinese

FormulaOne Language Definition

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.


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 


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:


General Format:

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

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

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.


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

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.



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.

Date_t = (year:I, month:[1..12], day:[1..31])
Complex_t = (R, R)
Person_t = (name:S, age:I, birthdate:Date_t)


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.


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


Format 2:

type1 ->> type2


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.

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

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.

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

Format 2:


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


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.


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.

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

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:

Array Constants

General Format:

[term1, term2, . .., termn]


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


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.

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


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)


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

matrix(i, j)

Field Selection

General Format:


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


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

Format 2:


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.


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

Function Calls

General Format:

Name(term1, term2, ..., termn-1)
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.

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:

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.

curr_colour :L
'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
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:
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
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.


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:
Format 2:

true is always true; false is always false.


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


General Format:

formula1 & formula2

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


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

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


General Format:

formula1 | formula2

formula1 | formula2 is true if either formula1 or formula2 are true.


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.

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


General Format:


~formula is true only if formula is false.


~formula is completely equivalent to the following if formula:

if formula then

if formulas

Format 1:
if condformula then


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.


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

This format is completely equivalent to the formula
if condformula then

Format 3

if condformula then
elsif elsifformula1 then
elsif elsifformulan then

This format is completely equivalent to the formula

if condformula then
    if elsifformula1 then
        if elsifformulan then

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


if l = Nil then
    sum = 0
    l = (h, t) & sum = h + Sum(t)


if n < 0 then
    f = 0
elsif n <= 1 then
    f = l
    f = n * Fact(n-l)

case Formulas

General Form:

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


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.


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.


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.


case digit of
    0 => name = 'zero';
    1 => name = 'one';
    2 => name = 'two';
    3 => name = 'three';
    4 | 5 | 6 => name = 'several'
    else name = 'many'

case string of
    'John'   => name = 'Lennon';
    'George' => name = 'Harrison';
    'Paul'   => name = 'McCartney';
    'Ringo'  => name = 'Starr';
    else name = 'not a Beatle'

all Formulas

General Form:

all var1,,...., varn in listvar

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.


An all formula is true if

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.

    all x in men_file
        P_data(x) &
        x = (_, Male, _, _, _)
    all x, square, cube in triple
        x::[1..20] &
        square = x * x &
        cube = x * square

Relational Operators

General Format:

term1 op term2
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).


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


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.

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


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.


The value of the extended variable in the environment is reassigned to the value of the term.

vehicle_arr(3).doors := Default_doors
iosum := iosum + 5
error_s := 2

Predicate Calls

General Format:

Name(term1, term2,..., termn)
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.


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.


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.

Sum((3, 2, 6, Nil), s)
Print( 'Foo' )
DbInsert(x, tree. left)

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.


A variable declaration is true if the variable has a value which is of the type given in the declaration.


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.


x :< I
tree :. Tree
reversed :> list U

Top Queries BNF Syntax of FormulaOne