%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  This code implements a simple CTR interpreter.  It assumes that  %
%  backtrackable updates are provided.                              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


% Given a goal, execute it by recursively executing hot components one
% at a time until the empty goal (state) is reached.
%
execute(Goal1) :- not(Goal1 = state),
                  oneStep(Goal1,Goal2),
                  execute(Goal2).

execute(state).


% Execute one hot component of Goal1.  In the process, Goal1 is
% transformed into Goal2, which is then simplified to Goal3.
%
oneStep(Goal1,Goal3) :- doOne(Goal1,Goal2), simplify(Goal2,Goal3).


% Execute one hot component of a sequential goal.
%
doOne(seq(G1a,G),seq(G1b,G)) :- !, doOne(G1a,G1b).


% Execute one hot component of a concurrent goal.  After execution,
% reverse the order of the two concurrent goals, to achieve a kind of
% round-robin scheduling.
%
doOne(conc(G1a,G2),conc(G2,G1b)) :- doOne(G1a,G1b).
doOne(conc(G1,G2a),conc(G2b,G1)) :- !, doOne(G2a,G2b).


% conc0 is a form of concurrent conjunction for transactions that
%commute (ie, for transactions for which the order of execution does
%not matter).
%
doOne(conc0(G1a,G2),conc(G2,G1b)) :- !, doOne(G1a,G1b).


% An isolated goal is a hot component, so execute the entire goal, and
% return the empty goal.
%
doOne(isolate(G),state) :- !, execute(G).

% Given a disjunctive goal, begin executing one of its disjuncts.
%
doOne(or(G1a,G2),G1b) :- doOne(G1a,G1b).
doOne(or(G1,G2a),G2b) :- !, doOne(G2a,G2b).


% If "Head" is defined by a rule in the transaction base, then execute
% one hot component of the rule body.  In the process, the rule body
% is transformed from "Body" into "Goal".  Thus, "Head" is unfolded into
% "Body", which is transformed into "Goal".  All rules in the
% transaction base have the form "trans(Head) :- Body".
%
doOne(Head,Goal) :- clause(trans(Head),Body), doOne(Body,Goal).
% doOne(Head,Goal) :- clause(trans(Head),Body), !, fail.


% An empty goal (state) does nothing and always succeeds.
%
doOne(state,state) :- !.


% If the interpreter gets this far, then assume that P is a Prolog
% command and execute it, leaving the empty goal (state).
%
doOne(P,state) :- !, P.


% Simplify a goal by removing any empty hot components.  eg, change
% "state x Phi x Psi" into "Phi x Psi", and change "Phi | state | Psi"
% into "Phi | Psi".  (A single empty hot component is introduced into a
% goal by the predicate "doOne".)
%
simplify(seq(state,G),G) :- !.
simplify(conc(state,G),G) :- !.
simplify(conc(G,state),G) :- !.
simplify(conc0(state,G),G) :- !.
simplify(conc0(G,state),G) :- !.

simplify(seq(G1a,G2),seq(G1b,G2)) :- simplify(G1a,G1b), !.

simplify(conc(G1a,G2a),conc(G1b,G2b)) :-
                         simplify(G1a,G1b), simplify(G2a,G2b), !.

simplify(conc0(G1a,G2a),conc0(G1b,G2b)) :-
                         simplify(G1a,G1b), simplify(G2a,G2b), !.

simplify(G,G) :- !.



% Define monitor(Task).  This command is useful for monitoring the
% execution of the various tasks that make up a program.  It prints a
% message when a task is committed, and prints another message if the
% task is later aborted and undone.  Specifically, when monitor(Task) is
% executed, it prints "committing Task" on the screen.  During
% backtracking, it prints "Aborting and Undoing Task".
%
monitor(Task) :- write('committing '), write(Task), nl, !,
                 onBacktracking(Task).

onBacktracking(Task).

onBacktracking(Task) :- write('aborting and undoing '),
                        write(Task), nl, !, fail.

