% Runtime Repeated Recursion Unfolding Implementation and Benchmarks
% copyright Thom Fruehwirth October 5, 2020 to July 4, 2023

% SWI Prolog started with -O command line option to compile in optimised mode. 
% /opt/local/lib/swipl-6.2.1/bin/i386-darwin10.8.0/swipl -O
% Currently optimised compilation implies compilation of arithmetic

:- use_module(library(chr)).

:- chr_option(check_guard_bindings, off).
:- chr_option(optimize, off).
:- chr_option(debug, off).


% RUNTIME REPEATED RECURSION UNFOLDING 

% recursive constraint call
% query below corresponds to rec_unfold
% ?- unf(RecursiveCall, [RecursiveRule,BaseCaseRule], RuleList),
%    mip(RecursiveCall,RuleList).


% UNFOLDER -------------

% unf(+RecursiveCall, +Rules, -RuleList)
% unf/2 runtime repeated recursion unfolder with rule simplification

:- chr_constraint unf(+,+,-).

unf(R, [RR|LR], LO) <=>               % unfold current rule
   RR = (Ro <=> Co | _),        
   copy_term_nat((Ro <=> Co), (R <=> C)), 
   call(C)
   |
   simp_unf(RR, RRl),
   unf(R, [RRl,RR|LR], LO).
unf(_R, [_RR|LR], LO) <=> LR=LO.      % no more recursion to unfold


% META_INTERPRETER -------------

% mip(+RecursiveCall, +RuleList)
% mip/2 specialised CHR meta-interpreter, rules used only at most once

:- chr_constraint mip(+,+).  

mip(true,_LR) <=> true.  % base case reached
mip(R,[RR|LR]) <=>       % apply current rule
   copy_term_nat(RR, (R <=> C | B, Rl, RCl)),  
   call(C)
   |
   call(B),
   mip(Rl,LR),
   call(RCl).  
mip(R,[_RR|LR]) <=>      % current rule not applicable
   mip(R,LR).


% SUMMATION EXAMPLE -------------

% original version summation
:- chr_constraint s(+,-).

s(A, C)<=>A>1| B is A-1, s(B, D), C is A+D.
s(A, B)<=>A=1| B=1.

% unfolding scheme with rule template

simp_unf((s(A,C) <=> A>V | (B is A-V, s(B,D), C is V*A-W+D)), 
         (s(Al,Cl) <=> Al>Vl | (Bl is Al-Vl, s(Bl,Dl), Cl is Vl*Al-Wl+Dl))) :-
    Vl is 2*V, Wl is 2*W+V*V.

% BENCHMARKS
 
% original version, 100 runs
% ?- between(15,22,K), sumtesto(K).
sumtesto(K):-
I is 2^K, 
T0 is cputime, 
(between(1,100,_), s(I,_), fail ; 
T1 is 10*(cputime-T0), format('$2^{~d}$ & ~0f \\\\~n',[K,T1]), fail).

% unfolded version, 1000 runs
% ?- member(K,[25,50,100,200,400,800,1600]), sumtestr(K).
sumtestr(K):- 
(I is 2^K,format('$2^{~d}$ &',K);
 I is 2^K+1,format('$2^{~d}+1$ &',K)),
T0 is cputime, 
(
(between(1,1000,_),
unf(s(I,_), [(s(A,C) <=> A>1 | (B is A-1, s(B,D), C is 1*A-0+D)),
            (s(Ib,Ob) <=> Ib=1 | Ob=1, true, true)], _),
fail);
T1 is cputime-T0, format(' ~2f &',T1),
unf(s(I,_), [(s(A,C) <=> A>1 | (B is A-1, s(B,D), C is 1*A-0+D)),
            (s(Ib,Ob) <=> Ib=1 | Ob=1, true, true)], LO), 
T11 is cputime,
(between(1,1000,_),mip(s(I,_),LO),
fail;
T2 is cputime-T11, format(' ~2f &',T2),
T3 is T1+T2, format(' ~2f \\\\~n',T3)),
fail
).


% LIST REVERSAL EXAMPLE -------------

% original version list reversal
:- chr_constraint r(+,-).

r(A, E) <=> A=[D|B] | r(B, C), append(C, [D], E).
r([], A) <=> A=[].

% unfolding scheme with rule template

simp_unf((r(A, B) <=> A=X1XnC | true, r(C, D), append(D, XnX1, B)), 
         (r(Al, Bl) <=> Al=X1X2nCl | true, r(Cl, Dl), append(Dl, X2nX1, Bl))) :-
    copy_term_nat((X1XnC,C,XnX1),(X1X2nCl,Cc,XnX1c1)), 
    copy_term_nat((X1XnC,C,XnX1),(Cc,Cl,XnX1c2)), 
    append(XnX1c2,XnX1c1,X2nX1).  

% BENCHMARKS

% original version
% ?- between(9,15,K), revtesto(K).
revtesto(K):- 
J is 2^K,format('$2^{~d}$ &',K),
length(I,J),
garbage_collect,
T1 is cputime,
r(I,_O),
T2 is cputime-T1, 
format(' ~2f \\\\~n',T2),
!,fail.

% unfolded version
% ?- revtestr(19,0) ; between(13,19,K), revtestr(K,-1) ; between(13,19,K), revtestr(K,0).
revtestr(K,W):- 
(W=(-1), !, J is 2^K-1,format('$2^{~d}-1$ &',K);
 W=0, !, J is 2^K,format('$2^{~d}$ &',K);
 W=1, !, J is 2^K+1,format('$2^{~d}+1$ &',K);
 W=m, !, J is 2^K+2^(K-1),format('$2^{~d}*1.5$ &',K)),
length(I,J),
garbage_collect,
T0 is cputime, 
unf(r(I,_), [(r(L, D) <=> L=[C|A] | true, r(A, B), append(B, [C], D)),
            (r([], B) <=> true | B=[], true, true)], LO),
T1 is cputime-T0, 
mip(r(I,_),LO),
T2 is cputime-T0-T1, T3 is T1+T2,  
format(' ~2f &',T1), format(' ~2f &',T2), format(' ~2f \\\\~n',T3),
!,fail.


% SORTING EXAMPLE  -------------

% original version
:- chr_constraint o(+,-).

o([], B) <=> B=[].
o(L, D) <=> L=[C|A] | o(A, B), m([C],B, D). 

   % merge m/3
   m([A|S1],[B|S2],[A|S]) :-  A=<B, !, m(S1,[B|S2],S).
   m([A|S1],[B|S2],[B|S]) :-  !, m([A|S1],S2,S).
   m(S,[],S):- !.
   m([],S,S). 
		
% unfolding scheme with rule template

simp_unf(
   Rule,
  (o(Ll, Dl) <=> Ll=X1X2nAl | MGlc, o(Ac, Bc), m(Dx,Bc,Dl))
        ):-     
    copy_term_nat(Rule,
                  (o(Ll, Dl) <=> Ll=X1X2nAl | MGl, o(Al, Bl), m(Cl,Bl,Dl))), 
    copy_term_nat(Rule,
                  (o(Al, Bl) <=> Al=X1XnAc | MGc, o(Ac, Bc), m(Cc,Bc,Bl))),
    clean((MGl, MGc, m(Cc,Cl,Dx)), MGlc),
    Al=X1XnAc.

   % remove superfluous 'true' from goals
   clean((true,C),D):- !, clean(C,D).
   clean(C,C).

% BENCHMARKS

% original version
% ?- between(9,14,K), sorttesto(K).
sorttesto(K):- 
J is 2^K,format('$2^{~d}$ &',K),
numlist(1,J,Is), 
random_permutation(Is,I),
garbage_collect,
T1 is cputime,
o(I,_),
T2 is (cputime-T1), 
format(' ~2f \\\\~n',T2),
!,fail.

% unfolded version
% ?- between(12,19,K), sorttestr(K,-1).
% ?- between(12,19,K), sorttestr(K,0).
sorttestr(K,W):- 
(W=(-1), !, J is 2^K-1,format('$2^{~d}-1$ &',K);
 W=0, !, J is 2^K,format('$2^{~d}$ &',K);
 W=1, !, J is 2^K+1,format('$2^{~d}+1$ &',K)),
numlist(1,J,Is), 
random_permutation(Is,I), 
garbage_collect,
T0 is cputime, 
unf(o(Is,_), [(o(L, D) <=> L=[C|A] | true, o(A, B), m([C],B, D)),
             (o([], B1) <=> true | B1=[], true, true)], LO), 
T1 is cputime-T0,
mip(o(I,_),LO),
T2 is cputime-T0-T1, T3 is T1+T2,  
format(' ~2f &',T1), format(' ~2f &',T2), format(' ~2f \\\\~n',T3),
!,fail.