% Prolog implementation of SOS rules for our simple imperative language.

% We represent an environment as a list of terms `x=v`.
% Thus, the following predicate implements the lookup in an environment:
lookup([Y=W|E],X,V) :- X=Y -> V=W ; lookup(E,X,V).

% This predicate implements an update of an environment, i.e.,
% update(S,X,V,S1) holds if S1 = S[X/V]:
update([]     ,X,V,[X=V]).
update([Y=W|S],X,V,S1) :- X=Y -> S1=[X=V|S] ; update(S,X,V,S2), S1=[Y=W|S2].

% We define the evaluation of expressions as a predicate
% where the clauses are just the translation of the natural semantics rules:
eval(_,N,N) :- number(N).
eval(S,X,V) :- atom(X), lookup(S,X,V).
eval(S,E1+E2,V) :- eval(S,E1,V1), eval(S,E2,V2), V is V1+V2.
eval(S,E1-E2,V) :- eval(S,E1,V1), eval(S,E2,V2), V is V1-V2.
eval(S,E1*E2,V) :- eval(S,E1,V1), eval(S,E2,V2), V is V1*V2.
eval(S,E1<E2,V) :- eval(S,E1,V1), eval(S,E2,V2), (V1<V2 -> V=true ; V=false).
eval(S,E1>E2,V) :- eval(S,E1,V1), eval(S,E2,V2), (V1>V2 -> V=true ; V=false).
eval(S,E1=E2,V) :- eval(S,E1,V1), eval(S,E2,V2), (V1=V2 -> V=true ; V=false).

% The predicate step(S1,Sigma1,S2,Sigma2) represents an SOS step.
step((X = E)   ,Sigma,skip,SigmaV) :- eval(Sigma,E,V), update(Sigma,X,V,SigmaV).
step(if(E,S,_) ,Sigma,S,Sigma)     :- eval(Sigma,E,true).
step(if(E,_,S) ,Sigma,S,Sigma)     :- eval(Sigma,E,false).
step(while(E,_),Sigma,skip,Sigma)  :- eval(Sigma,E,false).
step(while(E,S),Sigma,(S ; while(E,S)),Sigma) :- eval(Sigma,E,true).
step((skip ; S),Sigma,S,Sigma).
step((S1 ; S)  ,Sigma,(S2 ; S),Sigma1) :- step(S1,Sigma,S2,Sigma1).

% Computing sequences of steps (until skip) and return final environment:
exec(skip,Sigma,Sigma) :- !. % final state reached
exec(S1,Sigma1,R) :- step(S1,Sigma1,S2,Sigma2), exec(S2,Sigma2,R).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Examples: compute factorial of variable n:
%
% ?- P = (p=1; while(n>0, (p=p*n ; n=n-1))), exec(P,[n=6],R).