:- module(_,[ackerman/3],[assertions,regtypes, nativeprops]).

% adapded from the `Ackerman` example of the Interproc analyzer
%   http://pop-art.inrialpes.fr/interproc/interprocweb.cgi
%
% proc ack(x:int,y:int) returns (res:int)
% var t:int, t1:int;
% begin
%   assume x>=0 and y>=0;
%   if (x<=0) then /* x<=0 instead of x==0 (more precise) */
%     res = y+1;
%   else
%     if (y<=0) then /* y<=0 instead of x==0 (more precise) */
%       t1 = x-1;
%       t = 1;
%       res = ack(t1,t);
%     else
%       t1 = y-1;
%       t = ack(x,t1);
%       t1 = x-1;
%       res = ack(t1,t);
%     endif ;
%   endif;
% end
%
% var
% a:int, b:int, r:int;
% begin
% r = ack(a,b);
% end

:- entry ackerman(A,B,R) : constraint([A >=0, B >=0]).

ackerman(A,B,C) :- ack(A,B,C).

:- pred ack(A,B,R) : constraint([A >=0, B >=0])
                  => constraint([A >=0, B >=0, R >= A + B + 1]).

ack(X,Y,Res) :-
        X =< 0,
        Res is Y + 1.
ack(X,Y,Res) :-
        X >= 1,
        Y =< 0,
        T1 is X - 1,
        B is 1,
        ack(T1,B,Res).
ack(X,Y,Res) :-
        X >= 1,
        Y >= 1,
        T1 is Y - 1,
        ack(X,T1,T),
        T2 is X - 1,
        ack(T2,T,Res).
