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

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

evalTBSFile(File, State) :-
	open(File, read, Stream),
	read(Stream,Prog),
	evalTBS(Prog,State,S,T),
	write_term((S,T), []),
	close(Stream).

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

interestingBS(evalTBS).
%interestingBS(evalA).
%interestingBS(evalB).

latexGoalBS(evalTBS(P,S,S2,T), Tex) :-
	latexAL(S, T1),
	latexAL(S2, T2),
	swritef(Tex, "\\\\langle \\\\texttt{%w}, %w \\\\rangle \\Downarrow_{%w} %w", [P,T1,T,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, evalTBS(Prog,State,_,_)).

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

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