% Operational semantics for L1 Plus the Par operation from Lecture 12.
% Sam Staton. November 2010.
% Tested with GNU Prolog.


% Examples

% To load this file, type [l1].

% Slide 14 in the notes:
% [while(deref l >= 1,(k := (deref k + deref l)) seq (l := (deref l + -1))),[l := 3, k := 0]] ===> X.

% Page 98 in the notes:
% [l := (1 + deref l) par l := (7 + deref l),[l := 0]] ===> X.


:-op(700, xfx, --->).
:-op(700, xfx, --->*).
:-op(700, xfx, ===>).
:-op(250, xfx, add).
:-op(250, xfx, >=).
:-op(300, xfx, :=).
:-op(650, xfx, par).
:-op(200, fx, deref).
:-op(650, xfx, seq ).

value(N) :- integer(N).
value(true).
value(false).
value(skip).
value(V1 par V2) :- value(V1), value(V2).

% Rule OP + 
[N1 + N2,S] ---> [M,S] :- integer(N1) , integer(N2) , M is (N1+N2) .

% Rule OP >=
[N1 >= N2,S] ---> [true,S] :- integer(N1) , integer(N2) , N1 >= N2 .
[N1 >= N2,S] ---> [false,S] :- integer(N1) , integer(N2) , N1 < N2 .

% Rule OP1
[E1 + E2,S] ---> [E1a + E2,Sa] :- [E1,S] ---> [E1a,Sa].
[E1 >= E2,S] ---> [E1a >= E2,Sa] :- [E1,S] ---> [E1a,Sa].

% Rule OP2
[N1 + E2,S] ---> [N1 + E2a,Sa] :- [E2,S] ---> [E2a,Sa], value(N1).
[N1 >= E2,S] ---> [N1 >= E2a,Sa] :- [E2,S] ---> [E2a,Sa], value(N1).

% Rule DEREF
[deref L,S] ---> [N1,S] :- member((L := N1),S).

% Rule ASSIGN1
[L := N1,S] ---> [skip,[(L := N1)|Saa]] :- value(N1), member((L := N2), S), delete(S,(L := N2),Saa).

% Rule ASSIGN2
[L := E1,S] ---> [L := E1a,Sa] :- [E1,S] ---> [E1a,Sa].

% Rule SEQ1
[skip seq E2,S] ---> [E2,S].

% Rule SEQ2
[E1 seq E2,S] ---> [E1a seq E2,Sa] :- [E1,S] ---> [E1a,Sa].

% (NB I am not using infix notation for if and while.)

% RULE IF1
[ifthenelse(true,E2,_),S] ---> [E2,S].

% RULE IF2
[ifthenelse(false,_,E3),S] ---> [E3,S].

% RULE IF3
[ifthenelse(E1,E2,E3),S] ---> [ifthenelse(E1a,E2,E3),Sa] :- [E1,S] ---> [E1a,Sa].

% RULE WHILE
[while(E1,E2),S] ---> [ifthenelse(E1,(E2 seq while(E1,E2)),skip),S].

% RULE PARALLEL1
[E1 par E2,S] ---> [E1a par E2,Sa] :- [E1,S] ---> [E1a,Sa].

% RULE PARALLEL2
[E1 par E2,S] ---> [E1 par E2a,Sa] :- [E2,S] ---> [E2a,Sa].

% Multi-steps
[E,S] --->* [E,S].
[E,S] --->* [Ea,Sa] :- [E,S] ---> [Eaa,Saa], [Eaa,Saa] --->* [Ea,Sa].

% Evaluation
% (reduce until you get a value)
[E,S] ===> [Va,Sa] :- [E,S] --->* [Va,Sa], value(Va).