*Example 3 (Lazy lists and related functions).*
** mod!** *TEST2*
{

[*S*]
**
op** *cons* : *S* *S* -> *S* { **strat:** (1 -2
0) }
**
op** *tp* : *S* -> *S*
**
op** *tl* : *S* -> *S*
**
op** *2nd* : *S* -> *S*
**
op** *3rd* : *S* -> *S*
**
ops** *a* *b* *c* *nil* : -> *S*
**
eq** *tp*(*cons*(*X*:*S*,*L*:*S*)) = *X*
.
**
eq** *tl*(*cons*(*X*:*S*,*L*:*S*)) = *L*
.
**
eq** *2nd*(*cons*(*X*:*S*,*cons*(*Y*:*S*,
*L*:*S*))) = *Y* .
**
eq** *3rd*(*cons*(*X*:*S*,*cons*(*Y*:*S*,
*cons*(*Z*:*S*,*L*:*S*)))) = *Z* .

}

Let us think of evaluating the term *2nd*(*cons*(*a*,*
tl*(*cons*(*b*, *cons*(*c*,* nil*))))) with
respect to
*TEST2*. The argument *cons*(*a*,* tl*(*cons*(*b*,*
cons*(*c*,* nil*)))) is first evaluated because of the local
strategy of *2nd*. Although no rewrite occurs while the argument is
evaluated, all the subterms in the second argument are marked with on-demand
flags owing to the local strategy (1 -2 0) of *cons*. After that the
input term is tried to be matched with the left sides of the rewrite rules.
While a pattern matcher tries to match the term with the left side of the
third rewrite rule, it finds that the second one of the term's argument
(i.e. *tl*(*cons*(*b*,* cons*(*c*,* nil*))))
cannot be matched with the corresponding sub-pattern but it has been marked
with an on-demand flag. Hence the pattern matcher has a reducer evaluate
the subterm marked with the on-demand flag and retries to match the evaluated
subterm with the corresponding sub-pattern. In this case the pattern match
succeeds because the result of evaluating the subterm *tl*(*cons*(*b*,*
cons*(*c*,* nil*))) is
*cons*(*c*,* nil*).
Consequently the input term is replaced by
*c* that is the final result
of rewriting the original term.

Mon Nov 29 13:47:22 JST 1999