% A reversible interpreter for the JANUS reversible programming language
% (C) 2009 Adrian Prantl <adrian@complang.tuwien.ac.at>

:- use_module(library(clpfd)).
:- op(600, xfx, [ +=, -=, <=> ]).
:- op(804, fx, [call, uncall, if]).
:- op(803, yfx, [then]).
:- op(802, yfx, [else]).
:- op(801, yfx, [fi]).

ptrace(S0, P, S1, Dir) :- format('~w ~w ~w ~w ~w~n', [S0, Dir, P, Dir, S1]).

reval(S, _, [], S). % Speedup hack, reverse blocks
reval(S0, P, [Z|Zs], Sn) :-
  length(Sn, N), length(Sn_min1, N), % Skip useless backtracking
  eval(Sn_min1, P, Z, Sn),
  ptrace(Sn_min1, Z, Sn, '<--'),
  reval(S0, P, Zs, Sn_min1).
eval(S0, P, L, Sn) :- % This is the only special case for reverse execution
  is_list(L), \+ ground(S0), reverse(L, Lr), reval(S0, P, Lr, Sn).

eval(S0, _, [], Sn) :- permute(S0, Sn).
eval(S0, P, [Z|Zs], Sn) :-
  eval(S0, P, Z, S1), ptrace(S0, Z, S1, '-->'), eval(S1, P, Zs, Sn).

eval(S, _, procedure(_, _), S).

eval(S0, P, uncall F, Sn) :- eval(Sn, P, call F, S0).
eval(S0, P, call F, Sn) :- member(procedure(F, Body), P), eval(S0, P, Body, Sn).
  
eval(S0, P, if Cond then A else B fi Assert, Sn) :-
  freeze(Sn, eval1(Assert, Sn, Yes)), % Reduce useless backtracking
  eval1(Cond, S0, Yes),
  ( Yes = true -> eval(S0, P, A, Sn) ; eval(S0, P, B, Sn) ).
  
eval(S0, _, X <=> Y, Sn) :- % Swap
  select(X=Vx, S0, S1),
  select(Y=Vy, S1, S2),
  select(X=Vy, S3, S2),
  select(Y=Vx, Sn, S3).

eval(S0, _, Stmt, Sn) :-  % Expression Statements
  Stmt =.. [Op, X, Y],
  eval1(Y, S0, Vy),
  select(X=Vx,  S0, S1),
  select(X=Vx1, Sn, S1),
  eval1(Op, Vx1, Vx, Vy).

% Subexpressions
eval1(I, _, I) :- integer(I).
eval1(A, S, Va) :- atom(A), member(A=Va, S).
eval1(X=Y, S, true)  :- eval1(X, S, V),  eval1(Y, S, V).
eval1(X=Y, S, false) :- eval1(X, S, Vx), eval1(Y, S, Vy), Vx #\= Vy.
eval1((+=), R, X, Y) :- R #= X + Y.
eval1((-=), R, X, Y) :- R #= X - Y.

finalize(_=X) :- indomain(X).

% TESTS
test(S, P) :-
  sort(S, S0),
  eval(S0, P, P, S1),
  eval(S2, P, P, S1),
  maplist(finalize, S2),
  sort(S2, S0),
  format('~w ---> ~w ---> ~w ~n~n', [S0, P, S1]), !.

:- 
  test([x1=2,x2=0], [x1 += 3, x2 -= x1]),
  test([x1=2,x2=0], x1 <=> x2),
  test([x1=2], if x1=0 then x1+=42 else x1-=1 fi x1=42), 
  test([x1=0,x2=0,n=4],
       [procedure(fib,
		  [if n=0 then [x1 += 1,
				x2 += 1]
		  else [n -= 1,
			call fib,
			x1 += x2,
			x1 <=> x2]
		  fi x1=x2]
		 ),
	x1 += 5,
	x2 += 8,
	n -= 4,
	uncall fib
       ]),
  !.