Let a function declaration have either of the two forms
$func Fname Farg = Fres;
$func? Fname Farg = Fres;
where
Farg is the input format of the function, i.e. a format expression which
specifies the structure of the function's argument, and Fres is the output
format of the function, i.e. a format expression which specifies the structure of the
function's result. As mentioned previously the variable indices appearing in formats are of no
significance, for which reason, without any loss of generality, they will be supposed to have
been omitted.
Then, to formulate the restrictions imposed by the input and output formats of the function,
we assume the set of format expressions to be equipped with the following partial ordering.
Let F1 and F2 be two formats. Then F2
>> F1 means that the format F1 is an instance of the
format F2. The relation >> is defined by the
following rules.
-
F >> F.
-
If F1' >> F1 and F2' >>
F2 , then F1' F2' >> F1 F2 .
-
If F1 >> F2 , then (F1) >>
(F2) .
-
e >> F .
-
If F is not of the form e e ... e, then v
>> F .
-
t >> Gs , for all symbols Gs.
-
t >> s .
-
t >> (F) .
-
s >> Gs , for all symbols Gs.
Now consider a program written in Refal Plus and the constructs appearing in the program.
Let Re be a result expression appearing in the program. A format expression
F is said to be the format of Re, if F
can be produced from Re by the following transformations.
-
The indices of all variables appearing in Re are discarded.
-
All function calls appearing in Re are replaced with the output
formats of the corresponding functions. In other words, suppose that a function
Fname has been declared as either $func Fname Farg =
Fres; or $func? Fname Farg = Fres; . Then each call
<Fname Re'> is replaced with Fres.
Let P be a pattern appearing in the program. A format expression
F is said to be the format of P, if F can
be produced from P by the following transformations.
-
The indices of all variables appearing in P are discarded.
-
If P has a direction designator, the designator is discarded.
Let He be a hard expression appearing in the program. A format expression
F is said to be the format of He, if F
can be produced from P by discarding the indices of all variables appearing
in He.
Henceforth, the format of a result expression will be denoted by form[Re],
the format of a pattern P by form[P], and the format of a
hard expression He by form[He].
It should be emphasized that not only does the format of a result expression
Re depend on the structure of Re, but it also depends on the
output formats of the functions called in Re. Nevertheless, given a
particular program, the meaning of form[Re] is unambiguously defined.
Now we can formulate the restrictions that must be met by the function definitions. These
restrictions are imposed on the function calls, the input patterns in the function
definitions, and the results returned by the paths.
Suppose the declaration of a function Fname contains the input format
Farg, the output format Fres, whereas the pattern
alternative Palt appearing in the function definition
Fname Palt
has the form \{P1 R1; ... Pn
Rn;}.
Then the following conditions must be satisfied.
The function's input patterns P1, ...,
Pn must satisfy the restriction Farg >>
form[Pj].
The calls to the function Fname in all function definitions must satisfy
the following condition.
Let a call to the function Fname have the form <Fname
Re> . Then there must be satisfied the restriction Farg
>> form[Re].
To describe the restrictions imposed on the results returned by paths, we use the following
notation.
The fact that the results returned by a path Q satisfy a format
F will be written as F |- Q.
Rests, sources, and result expressions may be regarded as particular cases of paths, for
which reason the above notation is applicable to them as well as to paths.
Similarly, the fact that the results returned by a pattern alternative Palt
satisfy a format F will be written as F |- Palt.
Now we can formulate the restrictions imposed on the function definitions by the output
formats of the functions.
Let the definition of a function Fname be Fname Palt, and
the output format Fres. Then there must be satisfied Fres |-
Palt.
The relations F |- Q and F |- Palt are defined by the
following inference rules.
form[] |- S form[He] |- S
F |- R F |- R
------------ ---------------
F |- S R F |- S :: He R
form[He] |- S''
form[He] |- S'
F |- R
-------------------------
F |- S'' $iter S' :: He R
form[] |- S
F |- R F |- Q F |- R
------------- --------- ------------
F |- S : P R F |- , Q F |- # S R
F |- Q F |- Q
---------- ---------- F |- $fail
F |- \? Q F |- \! Q
F |- Q
--------- F |- $error Q
F |- = Q
F |- Q
F |- Palt
------------------------
F |- $trap Q $with Palt
F |- Qj for all j=1,...,n
---------------------------
F |- \{Q1; ... Qn;}
F |- Palt F >> form[Re]
-------------- --------------
F |- S : Palt F |- Re
F |- Rj for all j=1,...,n
---------------------------
F |- \{P1 R1; ... Pn Rn;}