:- import append/3 from basics.

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

% THE INTERPRETER: The predicate execute(Flag,Goal) executes Goal by

% recursively executing hot components one at a time until the empty

% goal (state) is reached.

%

% The variable Flag affects concurrency.  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 each isolation operator (see below).

execute(Flag,Goal1) :- not(Goal1 = state),

oneStep(Flag,Goal1,Goal2),

execute(Flag,Goal2).

execute(Flag,state).
 

% Execute one hot component of Goal1.  In the process, Goal1 is

% transformed into Goal2, which is then simplified to Goal3.

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

simplify(Goal2,Goal3).

 

% 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).
 

% 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.

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.

% conc1 is 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)).

% CONCURRENT COMPOSITION: A concurrent goal is a list of processes.

% To execute one step of the goal, we execute one step of some process

% in the list.  After execution, we rotate the list by 1 position, which

% assures round-robin scheduling in the absense of backtracking.

doOne(Flag,conc([]),state) :- !.

% Special case.  Do nothing, but simplify the goal.

% If Flag=one, then we always choose the first process in the goal list.

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.

% Rotate a list by 1 position.  If the first list element is state,

% then simply chop it off.

rotate1([state|Goals],Goals) :- !.

rotate1([G|Goals1],Goals2) :- !, append(Goals1,[G],Goals2).

% If Flag=all, then on backtracking, we will 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.

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 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).

% TRANSACTION BASE: Search the transaction base for rules of the form

% Head<-Body.  If such a rule is found, then, to execute one step of

% "Head", we execute one step of "Body".  This transforms "Body" into

% "Goal".  Note that the CTR rule Head<-Body is implemented as the

% Prolog rule trans(Head):-Body.  The value of Flag is irrelevant.

doOne(Flag,Head,Goal) :- clause(trans(Head),Body),

oneStep(Flag,Body,Goal).

% doOne(Flag,Head,Goal) :- clause(trans(Head),Body), !, fail.

% STATE: An empty goal does nothing and always succeeds.

%

doOne(Flag,state,state) :- !.

% PROLOG COMMANDS in CTR formulas: If the interpreter gets this far,

% then assume that P is a Prolog command and execute it, leaving 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([state]),state) :- !.

simplify(seq([state|Goals]),seq(Goals)) :- !.

simplify(conc([]),state) :- !.

simplify(conc([state]),state) :- !.

simplify(conc([state|Goals]),conc(Goals)) :- !.

simplify(conc1([]),state) :- !.

simplify(conc1([state]),state) :- !.

simplify(conc1([state|Goals]),conc1(Goals)) :- !.

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 committed, and then prints another

% message if the task is later rolled back and undone.  Specifically,

% when monitor(Task) is executed, it prints "committing Task" on the

% screen.  During backtracking, it prints "Undoing Task".

monitor(Task) :- write('committing '), write(Task), nl, !,

onBacktracking(Task).

onBacktracking(Task).

onBacktracking(Task) :- write('undoing '),

write(Task), nl, !, fail.