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


:- export execute/1, oneStep/3, monitor/1.

:- import append/3 from basics.


% TRANSACTIONAL EXECUTION.  The CTR interpreter executes a goal
% as a transaction, that is, atomically and in isolation.  The
% execution is atomic since it is completely undone in case of
% failure.  It is isolated since it is not interleaved with any
% other processes.
%
% At present, a goal may have any of the following forms:
%
%   - an atom,
%   - seq(List),
%   - conc(List) or conc1(List),
%   - or(List),
%   - isolate(List) or isolate1(List),
%
% where G is a goal, and List is a list of goals.  A goal may
% also be a sequence of Prolog commands inside round brackets,
% such as (Y is X+1, Z is Y-3).
%
% To execute a goal, the user types execute(goal).  As the
% following rule shows, execute/1 is essentially a user interface
% to execute/2, which is the main entry point into the CTR
% interpreter.

execute(Goal) :- execute(all,Goal).


% The predicate execute(Flag,Goal) executes Goal as a
% transaction, where Flag affects the treatment of concurrency
% and the response to transaction failure.
% 
% Specifically, given a set of concurrent processes, Flag
% specifies how many different interleavings of these processes
% should be checked.  The value of Flag (and thus the treatment
% of concurrency) is fixed within the scope of each isolation
% operator.  At present, regardless of the value of Flag, the
% first interleaving to be checked is always based on round-robin
% scheduling.
%
% At present, Flag can take two values, "all" and "one."  When Flag=all,
% the interpreter checks all possible interleavings of the processes until
% one is found that succeeds.  When Flag=one, the interpreter checks
% only one interleaving.  This is useful for commutative transactions,
% where all interleavings give the same result.  In this case, if one
% interleaving fails, then they all fail, so there is no point of
% checking more than one interleaving.  The value of flag is initially
% "all" (see above), and can be changed by an isolation operator (see
% below).
%
% THE INTERPRETER: The two rules below define the predicate
% execute(Flag,Goal).  They execute Goal by recursively executing
% hot components one at a time until the empty goal (state) is
% reached.  Whenever there is a choice of hot components to
% execute, the choice is made non-deterministically.  (The other
% hot components may be chosen during backtracking, in case of
% transaction failure.)

execute(Flag,Goal1) :- not(Goal1 = state),
                       oneStep(Flag,Goal1,Goal2),
                       execute(Flag,Goal2).

execute(Flag,state).



% ONE-STEP EXECUTION: The predicate oneStep(Flag,Goal1,Goal3)
% executes one hot component of Goal1.  In the process, Goal1 is
% transformed into Goal2, which is then simplified to Goal3.  The
% CTR interpreter calls this predicate repeatedly, reducing the
% goal one step at a time.

oneStep(Flag,Goal1,Goal3) :- doOne(Flag,Goal1,Goal2),
                             simplify(Goal2,Goal3).


% The predicate doOne(Flag,Goal1,Goal2) is the main workhorse
% of the CTR interpreter.  It executes one hot component of
% Goal1, transforming it into Goal2 in the process.  This
% predicate is defined by a number of rules.  The rule that is
% invoked depends on the structure of Goal1, and on the value of
% Flag.

% SEQUENTIAL COMPOSITION: Execute one step of a sequential goal.  The
% value of Flag is irrelevant.

doOne(Flag,seq([]),state) :- !.
                  % Special case.  Do nothing, but simplify the goal.

doOne(Flag,seq([G1|Goals]),seq([G2|Goals])) :- !, oneStep(Flag,G1,G2).



% DISJUNCTIVE GOALS: A disjunctive goal is a list of processes.  To
% execute the goal, we must execute one of its disjuncts, chosen
% non-deterministically.  The rules below first choose a disjunct,
% then execute one step, and then return the rest.  (More precisely,
% the rules choose the first disjunct, and on backtracking, they
% choose other disjuncts.)  The value of Flag is irrelevant.

doOne(Flag,or([]),G) :- !, fail.            % No disjuncts.  Fail.

doOne(Flag,or([G1]),G2) :- !, oneStep(Flag,G1,G2). 
                        % Only 1 disjunct to choose from.  This special case
			% gets special treatment in order to reduce backtracking.

doOne(Flag,or([G1|Goals]),G2) :- oneStep(Flag,G1,G2).
                              % Many disjuncts: choose the first one.

doOne(Flag,or([G1|Goals]),G2) :- !, doOne(Flag,or(Goals),G2).
                              % Choose another one.


% CONCURRENT COMPOSITION: A concurrent goal is a list of
% processes.  To execute one step of the goal, we choose some
% process in the list, and execute one step of it.

doOne(Flag,conc([]),state) :- !.
                   % Special case.  Do nothing, but simplify the goal.


% If Flag=one, then choose the first process in the goal list,
% execute one step of this process, and then rotate the goal list
% by 1 position.  This assures round robin scheduling of concurrent
% processes.

doOne(one,conc(Goals1),conc(Goals4)) :- !,
        [Ga|Goals2] = Goals1,      % Extract the first process.
        oneStep(one,Ga,Gb),        % Execute one step of the process.
        Goals3 = [Gb|Goals2],      % Put first process back into the list.
        rotate1(Goals3,Goals4).    % Rotate list by 1 position.


% If Flag=all, then on backtracking, we should eventually choose every
% process in the goal list.  (This guarantees that all interleavings of
% the processes are eventually generated.)  To choose a process, we
% rotate the list by some amount, and select the first process in the
% rotated list.  More precisely, we initially rotate the list by 0
% positions; then, on backtracking, we rotate it by 1 position, 2
% positions, 3 positions, etc.  In this way, every process is eventually
% rotated to the front of the list.  Moreover, in the absense of
% backtracking, the first process in the list is always chosen.
% In addition, after one step of the chosen process is executed,
% we rotate the list again, by 1 position, to assure round-robin
% scheduling.

doOne(all,conc(Goals1),conc(Goals5)) :- !,
        rotate(Goals1,Goals2),     % Rotate the list of processes.
        [Ga|Goals3] = Goals2,      % Extract the first process.
        oneStep(all,Ga,Gb),        % Execute one step of the process.
        Goals4 = [Gb|Goals3],      % Put first process back into the list.
        rotate1(Goals4,Goals5).    % Rotate list by 1 position.


% Rotate a list by 1 position.  If the first list element is state,
% then simply chop it off (this is an optimization.)
%
rotate1([state|Goals],Goals) :- !.
rotate1([G|Goals1],Goals2) :- !, append(Goals1,[G],Goals2).


% Rotate list L1 by some amount, to give list L2.
%
rotate(L1,L2) :- split(L1,L1a,L1b),
                 not(L1b = []),
                 append(L1b,L1a,L2).


% Split list L into two sublists, L1 and L2.
%
split(L,L1,L2) :- append(L1,L2,L).



% conc1 provides a form of concurrent conjunction for
% transactions that commute (ie, for transactions for which the
% order of execution does not matter).  In this case, the
% interpreter tries only one interleaving.
% 
doOne(Flag,conc1(Goals1),conc1(Goals2)) :- !,
                   doOne(one,conc(Goals1),conc(Goals2)).
                   


% ISOLATION: An isolated goal is a hot component; so, to execute one
% step, the entire goal is executed, and the empty goal is returned.
%
% There are two modalities of isolation, isolate(G) and isolate1(G),
% which affect the interleaving of concurrent processes in G.
% isolate(G) causes all interleavings to be checked, while isolate1(G)
% causes only one interleaving to be checked.

doOne(Flag,isolate(G),state) :- !, execute(all,G).

doOne(Flag,isolate1(G),state) :- !, execute(one,G).



% ATOMIC GOALS.  Search the transaction base for rules of the
% form Goal<-Body.  If such a rule is found, then, to execute one
% step of Goal, we simply execute one step of Body.  (This
% transforms Body into Body2, which we return.)  Note that the
% CTR rule Goal<-Body is implemented as the Prolog rule
% trans(Goal):-Body.  The value of Flag is irrelevant.

doOne(Flag,Goal,Body2) :- clause(trans(Goal),Body),
                          oneStep(Flag,Body,Body2).



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



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




% SIMPLIFICATION: Here are some basic rules for simplifying a goal
% after a single step has been executed.  Intuitively, simplify(G1,G2)
% means that goal G2 is equivalent to but syntactically simpler than
% goal G1.

simplify(seq([]),state) :- !.
simplify(seq([Goal]),Goal) :- !.
simplify(seq([state,Goal]),Goal) :- !.
simplify(seq([state|Goals]),seq(Goals)) :- !.
simplify(seq([seq(Goals1)|Goals2]),seq(Goals3)) :- !,
                           append(Goals1,Goals2,Goals3).

simplify(conc([]),state) :- !.
simplify(conc([Goal]),Goal) :- !.
simplify(conc([state,Goal]),Goal) :- !.
simplify(conc([state|Goals]),conc(Goals)) :- !.
simplify(conc([conc(Goals1)|Goals2]),conc(Goals3)) :- !,
                           append(Goals1,Goals2,Goals3).

simplify(conc1([]),state) :- !.
simplify(conc1([Goal]),Goal) :- !.
simplify(conc1([state,Goal]),Goal) :- !.
simplify(conc1([state|Goals]),conc1(Goals)) :- !.
simplify(conc1([conc1(Goals1)|Goals2]),conc1(Goals3)) :- !,
                           append(Goals1,Goals2,Goals3).

simplify(isolate(isolate(Goal)),isolate(Goal)) :- !.
simplify(isolate1(isolate1(Goal)),isolate1(Goal)) :- !.

simplify(G,G) :- !.



% MONITORING EXECUTION: The command monitor(Task) helps a user to
% monitor the execution of the various tasks that make up a CTR program.
% It prints a message when a task is executed, and then prints another
% message if the task is later rolled back and undone.  Specifically,
% when monitor(Task) is executed, it prints "executing Task" on the
% screen.  During backtracking, it prints "undoing Task".

monitor(Task) :- write(' completed '), write(Task), nl, !,
                 onBacktracking(Task).

onBacktracking(Task).

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

