:- module(_,[fact/2],[regtypes,assertions,nativeprops]).

% adapted from the `Factorial` example of the Interproc analyzer
%   http://pop-art.inrialpes.fr/interproc/interprocweb.cgi
%
% /* Multiplication with a loop */
% proc fact1 (a:int) returns (b:int)
% var c:int;
% begin
%   if (a<=1) then
%     b = 1;
%   else
%     c = a - 1;
%     c = fact1(c);
%     b = 0;
%     while (c>0) do
%       b = b+a;
%       c = c-1;
%     done;
%   endif
%   ;
% end

% ----------------------------------------------------------------------
:- entry fact(A,B) : constraint([A >= 0]).
:- pred fact(A,B) : constraint([A >= 0]) => constraint([B >=0, B >= A]).

fact(A,B) :- A =< 1, B = 1.
fact(A,B) :-
        A > 1,
        C0 is A - 1,
        fact(C0,C),
        loop_fact1(C,A,0,B).

loop_fact1(C,_,AccB,B):- C = 0, B = AccB.
loop_fact1(C,A,AccB,B) :-
        C > 0,
        B1 is AccB + A,
        C1 is C - 1,
        loop_fact1(C1,A,B1,B).
