Janus is a programming language that was designed to support both forward and backward execution. So I decided that it would be an interesting project to design an interpreter for such a language that is itself reversible. By choosing Prolog as implementation language this was easily doable, although I have to acknowledge that only a subset of the language was implemented. The feature set includes recursion, arithmetic and un-calling of functions.
Throughout the interpreter reversability is implemented using unification and (sometimes) backtracking. There are two implementations for basic blocks, depending on the direction of control flow. All other language elements are implemented with only one bidirectional predicate.
The syntax is recognized with a funny combination of infix operators. Check out the if-then-else-fi construct!
Arithmetic was implemented with constraints, as the is predicate does not support logical variables on the right-hand side..
The test-predicate starts from an initial state and executes the program yielding a new state. From the new state, the program is the un-computed yielding the final state. The sorted initial and final states are then compared,a s they should be identical.
The program was tested with SWI-Prolog. Download the file instead.
% A reversible interpreter for the JANUS reversible programming language
% (C) 2009 Adrian Prantl
:- 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).
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).
test(S, P) :-
eval(S0, P, P, S1),
eval(S2, P, P, S1),
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),
[if n=0 then [x1 += 1,
x2 += 1]
else [n -= 1,
x1 += x2,
x1 <=> x2]
x1 += 5,
x2 += 8,
n -= 4,