A with-clause allows us to use a block (remember that this is a list of sentences in braces) right in the middle of a function definition without introducing an auxilliary function for that purpose.
To give an example of a with-clause, recall the pair ordering function from Chapter 3:
Order { (e1)e2 = <Order1 <Pre (e1)(e2)> (e1)e2>;} Order1 { T (e1)e2 = e1 e2; F (e1)e2 = e2 e1; };
The auxilliary function is unnecessary if we use the full Refal:
Order { (e1)e2, <Pre (e1)(e2)>: { T = (e1)(e2); F = (e2)(e1); }; }
A with-clause starts in the same way as a where-clause: a where-with sign, then a general Refal expression using only bound variables (argument), then the colon for a matching operation. Instead of a pattern, however, the with-clause has a block. The braces enclosing a group of sentences in the block have double significance.
First, they allow us to try to match the argument to several patterns. In our example, <Pre (e1)(e2)> is computed once, after which the Refal machine tries to match it to the consecutive left sides in the block. In the case of a successful match, the replacement is performed as usual.
The second function of the braces in a with-clause is to put an end to the process of matching in the preceding left side and conditions. When control enters a left brace, there is no way back for lengthening e-variables. Whatever values have been assigned to the variables outside the block are going to stay. In case none of the sentences in a block is applicable, an abnormal end will ensue as if it were a function definition.
In fact a block is a function definition, but this function has no name assigned and is called with the argument, (the expression following the where-with sign) as its argument. One can see that the block in the definition of Order is exactly the same as in the auxiliary function Order1 . A with-clause allows us to define an unnamed function right in the place where we need it. The definition of Order in basic Refal can be seen as the semantics of the with-clause in the second definition.
Consider the following definition:
F { e1'+'(e2)e3, <P e2>: T = (e2); e1 = <Prout 'No such term'>; };
This function finds the first parenthesized term following '+' such that the expression inside satisfies the predicate P . If P is defined by:
P { s1'/'s2 = T; eX = F; }the evaluation of:
<F A-B+(C*D)+(C/D)>results in (C/D) . If we put the condition and the right side in braces, so that is becomes a one-sentence block:
F { e1'+'(e2)e3>, <P e2>: { T = (e2) }; e1 = <Prout 'No such term'>; }then the algorithm should be read: find the first parenthesized term following '+' and then check that the enclosed expression satisfies P . If we now evaluate the same call with the modified definition, the result will be an abnormal stop `Recognition impossible'. Indeed, the first term after '+' is (C*D) , and it does not satisfy P . There will be no attempt to lengthen e1: we can only enter the braces around blocks, never exit from them.
Recall the function Sub-a-z which locates a substring starting with 'a' and ending with 'z' . In Chapter 2 we had to introduce an auxilliary function in order to define it efficiently. Now we can include that function as a block:
Sub-a-z { e1'a'e2, e2 : { e3'z'e4 = (e1)'a'e3'z'(e4); e3 = <Prout 'No substring a-z'>; }; e1 = <Prout "No 'a' found">; }After the first 'a' is found, we enter a block, and if there is no single 'z' after it, e1 will not be lengthened; the negative result will be stated instead.
Blocks, like conditions, are implemented through the calls of auxiliary $-functions which are inserted between the argument of the main (calling) functions and the right activation bracket. Auxiliary functions for blocks are even closer to regular functions than those for conditions. Like regular functions, they are computed by trying to match the argument to consecutive sentences of the block; after a successful matching the corresponding right side is used for replacement. However, the call that is replaced is not of the $-function, but that of the main function whose definition includes the with-clause.
Let us trace a call of the function Order above:
1. <Order ('abc')'de'> 2. <Order ('abc')'de'<Order$1 <Pre ('abc')('de')>>>After Pre is computed, which takes four steps, we have:
6. <Order ('abc')'de'<Order$1 T>> 7. ('abc')('de')Exercise 4.3 Redefine the following function to make the definition efficient:
S123 { eA 1 eB 2 eC 3 eD = T; eA = F; }Exercise 4.4 An inverted pair in a sequence of numbers is a pair of adjacent numbers such that the preceding number is greater than the following one.