:- consult(common).
:- consult(derivTree).

/* Bigstep-Semantics for WHILE */
evalBS(skp, S, S) :-
	name('Skip').
evalBS((P1;P2), S1, S3) :-
	name('Seq'),
	evalBS(P1, S1, S2),
	evalBS(P2, S2, S3).
evalBS(Var := Aexp, S1, S2) :-
	name('Ass'),
	evalA(S1, Aexp, Value),
	set(S1, Var, Value, S2).
evalBS(cond(Bexp, P1, _), S1, S2) :-
	name('IfTT'),
	evalB(S1, Bexp, tt),
	evalBS(P1, S1, S2).
evalBS(cond(Bexp, _, P2), S1, S2) :-
	name('IfFF'),
	evalB(S1, Bexp, ff),
	evalBS(P2, S1, S2).
evalBS(while(Bexp,_), S1, S1) :-
	name('WhileFF'),
	evalB(S1, Bexp, ff).
evalBS(while(Bexp,P), S1, S3) :-
	name('WhileTT'),
	evalB(S1, Bexp, tt),
	evalBS(P, S1, S2),
	evalBS(while(Bexp,P), S2, S3).

evalBSFile(File, State) :-
	open(File, read, Stream),
	read(Stream,Prog),
	evalBS(Prog,State,S),
	write_term(S, []),
	close(Stream).

evalBSFile(File) :- evalBSFile(File, []).

interestingBS(evalBS).
%interestingBS(evalA).
%interestingBS(evalB).

latexGoalBS(evalBS(P,S,S2), Tex) :-
	latexAL(S, T1),
	latexAL(S2, T2),
	swritef(Tex, "\\\\langle \\\\texttt{%w}, %w \\\\rangle \\Downarrow %w", [P,T1,T2]).
latexGoalBS(evalA(S,Ex,V),Tex) :-
	latexAL(S,T),
	swritef(Tex,"\\\\mathcal A \\\\llbracket \\\\texttt{%w} \\\\rrbracket %w = %w", [Ex,T,V]).
latexGoalBS(evalB(S,Ex,V),Tex) :-
	latexAL(S,T),
	swritef(Tex,"\\\\mathcal B \\\\llbracket \\\\texttt{%w} \\\\rrbracket %w = \\\\mathbf{%w}", [Ex,T,V]).

bsGoal(State, Prog, evalBS(Prog,State,_)).

evalBSToTex(File, State) :-
	derivTreeFromFile(File, interestingBS, latexGoalBS, call(bsGoal, State)).

evalBSToTex(File) :- evalBSToTex(File, []).