% SOS-Implementierung in Prolog.

% Repräsentation von Zuständen als Liste von "="-Termen (z.B.: [=(x,2),b=true])
% Prädikat zum Nachschlagen in einem Zustand: lookup(Sigma,Var,Value)
lookup([Y=W|E],X,V) :- X=Y -> V=W ; lookup(E,X,V).

% Prädikat zum Aktualisieren eines Zustand:
% update(Sigma,X,V,Sigma1) entspricht "Sigma1 = Sigma[X/V]"
update([]         , X, V, [X=V] ).
update([Y=W|Sigma], X, V, Sigma1) :-
  X = Y -> Sigma1 = [X=V|Sigma]
         ; update(Sigma, X, V, Sigma2), Sigma1 = [Y=W|Sigma2].

% Auswertung von Ausdrücken nach den Regeln der natürlichen Semantik:
% eval(Sigma,E,V) enspricht "Sigma |- E : V"
eval(_    , N    , N) :- number(N).
eval(Sigma, X    , V) :- atom(X), lookup(Sigma, X, V).
eval(Sigma, E1+E2, V) :- eval(Sigma,E1,V1), eval(Sigma,E2,V2), V is V1 + V2.
eval(Sigma, E1-E2, V) :- eval(Sigma,E1,V1), eval(Sigma,E2,V2), V is V1 - V2.
eval(Sigma, E1*E2, V) :- eval(Sigma,E1,V1), eval(Sigma,E2,V2), V is V1 * V2.
eval(Sigma, E1<E2, V) :- eval(Sigma,E1,V1), eval(Sigma,E2,V2), (V1 < V2 -> V = true; V = false).
eval(Sigma, E1>E2, V) :- eval(Sigma,E1,V1), eval(Sigma,E2,V2), (V1 > V2 -> V = true; V = false).
eval(Sigma, E1=E2, V) :- eval(Sigma,E1,V1), eval(Sigma,E2,V2), (V1 = V2 -> V = true; V = false).

% Berechnungsschritte nach Regeln der SOS:
% step(S1,Sigma1,S2,Sigma2) entspricht "<S1,Sigma1> -> <S2,Sigma2>"
step((X=E)      , Sigma, skip, SigmaV) :- eval(Sigma, E, V), update(Sigma,X,V,SigmaV).
step(if(E,S1,S2), Sigma, S1, Sigma) :- eval(Sigma, E, true).
step(if(E,S1,S2), Sigma, S2, 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), Sigma2) :- step(S1, Sigma, S2, Sigma2).

% Druchführen einer Berechnung:
% exec(S, Sigma, FinalSigma) entspricht "<S, Sigma> -> ... -> <skip, FinalSigma>""
exec(skip, Sigma, Sigma     ) :- !.
exec(S   , Sigma, FinalSigma) :- step(S, Sigma, S2, Sigma2), exec(S2, Sigma2, FinalSigma).

% Beispiel: Berechnung der Fakultät einer Variable n
% ?- P = (p=1; while(n>0, (p=p*n; n=n-1))), exec(P, [n=6], R).
