% Operational semantics for L1 
% Sam Staton. March 2011.
% Tested with SWI Prolog.


% Examples

% To load this file, type [l1].

% Slide 14 in the notes:
% [(l2 := 0) seq while (deref l1 >= 1) do ((l2 := ((deref l2) + (deref l1))) seq (l1 := (deref l1 + -1))),[l1 := 3, l2 := 0]] ===> X.
% [l2 := 0 seq (while (deref l1 >= 1) do ((l2 := ((deref l2) + (deref l1))) seq (l1 := (deref l1 + -1)))),[l1 := 3, l2 := 0]] ---> X.
% In swipl, you can step through a run like this.
% $X ---> X.

:-op(700, xfx, --->).
:-op(700, xfx, --->*).
:-op(700, xfx, ===>).
:-op(250, xfx, >=).
:-op(300, xfx, :=).
:-op(200, fx, deref).
:-op(650, xfx, seq ).
:-op(650, xfx, do ).
:-op(660, xfx, then ).
:-op(665, xfx, else ).
:-op(670, fx, if ).
:-op(670, fx, while ).

value(N) :- integer(N).
value(true).
value(false).
value(skip).

% Rule OP + 
[N1 + N2,S] ---> [N,S] :- integer(N1) , integer(N2) , N 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
[V1 + E2,S] ---> [V1 + E2a,Sa] :- [E2,S] ---> [E2a,Sa], value(V1).
[V1 >= E2,S] ---> [V1 >= E2a,Sa] :- [E2,S] ---> [E2a,Sa], value(V1).

% Rule deref
% NB because of prolog syntax we have to use "deref" instead of !
[deref L,S] ---> [N,S] :- member((L := N),S).

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

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

% Rule SEQ1
% NB because of prolog syntax we have to use "seq" instead of semicolon
[skip seq E2,S] ---> [E2,S].

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

% RULE IF1
[if true then E2 else _,S] ---> [E2,S].

% RULE IF2
[if false then _ else E3,S] ---> [E3,S].

% RULE IF3
[if E1 then E2 else E3,S] ---> [if E1a then E2 else E3,Sa] 
  :- [E1,S] ---> [E1a,Sa].

% RULE WHILE
[while E1 do E2,S] ---> [if E1 then (E2 seq (while E1 do E2)) else skip,S].

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