declare X Y {Test f(X b Y)}
It waits for x1, y1 to bind and then depending upon the bindings it'll print 'case'(1) if we bind X->a and Y->b else 'case'(2)
declare X Y {Test f(a Y d)}
It fails immediately because a=a, Y=Y (no matter what the binding is) and d is never equal to c.
declare X Y {Test f(X Y d)}
It waits for X to bind and then eventually will fail as c is not equal to d.and will print 'case'(2)
Note: I cheated in giving the above answers, I ran the code and then tried to come up with these answers. I am still not sure what is the exact pattern matching algorithm used by the case statement. I hope someone will provide better explainations.
declare X Y
if f(X Y d)==f(a Y c) then {Browse 'case '(1)}
else {Browse 'case'(2)} end
It fails immediately, because "==" uses entailment algorithm which is smart enough to find out that this matching is gonna fail no matter what X binds to.
Subscribe to:
Post Comments (Atom)
This has puzzled me as well ...
ReplyDeleteHowever, when I tried
declare X Y {Test f(d Y X)}
it selected case 2.
So I suspect, this may have something to do with pattern matching algorithm sticking to a strict order of evaluation, whereas (for some reason) entailment algorithm can be more flexible.