nextupprevious
Next:Operational Semantics of Up:The On-demand E-strategyPrevious:Restriction Imposed by

Example Using the On-demand E-strategy

We show an example that needs the on-demand E-strategy.

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.



nextupprevious
Next:Operational Semantics of Up:The On-demand E-strategyPrevious:Restriction Imposed by



Kazuhiro Ogata
Mon Nov 29 13:47:22 JST 1999