Hi Amoss,
:- entry mem(X,[1,2,3]) : (ground(X)). mem(X,[X|_]). mem(X,[_|Y]) :- member(X,Y).
This code specialises to what I would expect, namely three clauses, one for each success case.
Good!
If I try a similar code that uses some basic arithmetic then I don't get the same results :
:- entry loop(1,10). loop(X,L) :- X>=L. loop(X,L) :- X<L, write(dude), X2 is X+1, loop(X2,L).
This code specialises to:
:- entry loop(1,10). loop(1,10) :- user:write(dude), A is 1+1, user:loop(A,10).
This isn't actually correct as it will write 'dude' once and then fail, where-as the original will write 'dude' nine times and then succeed. But also, I would expect the loop to be unfolded to yield something (close to):
loop(1,10) :- write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude).
How can I get ciaopp to unfold arithmetic expressions like this? Is it a different set of menu options to the one that I am using to select a different type of analysis, or is it a different local-control rule?
I am afraid the problem is not in the arithmetic predicates but rather on the predicate write/1. Since it has side effects, it cannot be executed at specialization time. Then the only solution is to perform non-leftmost unfolding. For this you have to select
Select Computation Rule: [leftmost, local_builtin, local_emb, jump_builtin] (leftmost) ? jump_builtin
all the other flags you can leave with the default value.
This will generate your expected output:
%%%%%%%%%%%%% :- module( _loop, [loop/2], [assertions] ).
:- entry loop(1,10).
loop(1,10) :- write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude). %%%%%%%%
German
P.S. I have added your program to CVS, under CVS:Projects/Asap/Deliverables/Tests/loop.pl so that we always speak about exactly the same code. Note I have added a module declaration.