% Operational semantics for L1 
% Sam Staton. February 2011.
% 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.
% [while (deref l >= 1) do ((k := ((deref k) + (deref l))) seq (l := (deref l + -1))),[l := 3, k := 0]] ===> 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] ---> [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
% NB because of prolog syntax we have to use "deref" instead of !
[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
% 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).