% nat-sem.pl
%
% The Natural Semantics of Statements of While programs
% reconsult('nat-sem').

 :- ['expr'].

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Stm : Statements
%   S ::= skip | ass(X, A) | seq(S1, S2) | cond(B, S1, S2) | while(B, S)
%
% Executing statements in Natural Semantics
% exec_ns(+Statement, +State, -State)

% Rule skip_ns
exec_ns(skip, State, State).

% Rule ass_ns
exec_ns(ass(X, A), State, State1) :-
   eval_AExp(A, State, Z),
   update(State, X, Z, State1).

% Rule comp_ns
exec_ns(seq(S1, S2), State, State1) :-
   exec_ns(S1, State, State2),
   exec_ns(S2, State2, State1).

% Rule if_tt_ns
exec_ns(cond(B, S1, S2), State, State1) :-
   eval_BExp(B, State, tt), !,
   exec_ns(S1, State, State1).

% Rule if_ff_ns
exec_ns(cond(B, S1, S2), State, State1) :-
   exec_ns(S2, State, State1).

% Rule while_tt_ns
exec_ns(while(B, S), State, State1) :-
   eval_BExp(B, State, tt), !,
   exec_ns(S, State, State2),
   exec_ns(while(B, S), State2, State1).

% Rule while_ff_ns
exec_ns(while(B, S), State, State).

% Test Queries:
%
% ?- exec_ns(seq(ass(z, num(0)), while(leq(var(y), var(x)), seq(ass(z, add(var(z), num(1))), ass(x, sub(var(x), var(y)))))), [val(x, 17), val(y, 5), val(z, -3)], X).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%