/* This file provides ways to visualize the derivation that led to a goal to be
considered true. */

/*
 * This clause is always true, but can be used to annotate a clauses with a
 * name, by giving it as the first goal, e.g.
 * child(X) :- name('ChildSon'), son(X,P).
 */
name(_).

/*
 * solve(isinteresting,goal,proof)
 * is true if goal can be shown, and proof is a tree that shows why goal is
 * true, but includes only goals P(x) where interesting(P) is true.
 */
solve(_,true,fact).
solve(_,name(X),name(X)).
solve(Interesting,Call,Proof) :- /* Treat calls transparently. */
	Call =.. [call | Args],
	!,
	Term =.. Args,
	solve(Interesting, Term, Proof).
solve(Interesting,(A,B),(ProofA,ProofB)):-
	solve(Interesting, A, ProofA),
	solve(Interesting, B, ProofB).
solve(Interesting,A,A-ProofB) :-
	functor(A,F,_),
	call(Interesting, F),
	!,
	clause(A,B),
	solve(Interesting, B,ProofB).
solve(_, A,fact) :-
	call(A).

/*
 * latexTree(latexGoal, proof, TEX)
 * takes a proof tree as generated by solve and prints it to a latex string,
 * using the predicate latexGoal to print the actual goals.
 */
latexTree(_, fact, Tex) :-
	swritef(Tex, '').
latexTree(LG, Goal-(name(Name)), Tex) :-
	once(call(LG, Goal, Tex1)),
	swritef(Tex,"\\inferrule*[left=%w]{ }{%w}",[Name,Tex1]),
	!.
latexTree(LG, Goal-(name(Name),Proof2), Tex) :-
	once(call(LG, Goal, Tex1)),
	latexTree(LG, Proof2,Tex2),
	swritef(Tex,"\\inferrule*[left=%w]{%w }{%w}",[Name,Tex2,Tex1]),
	!.
latexTree(LG, Goal-Proof2, Tex) :-
	once(call(LG, Goal, Tex1)),
	latexTree(LG, Proof2,Tex2),
	swritef(Tex,"\\inferrule*{%w }{%w}",[Tex2,Tex1]).
latexTree(LG,(Proof1,Proof2), Tex) :-
	latexTree(LG, Proof1,Tex1),
	latexTree(LG, Proof2,Tex2),
	swritef(Tex,"%w \\\\\\\\ %w",[Tex1,Tex2]).

/*
 * latexGoalPlain is a possible choice for the first argument to latexTree
 */
latexGoalPlain(Goal, Tex) :-
	swritef(Tex, "%w", [Goal]).

/*
 * Helper function to pretty-print an associative list using smallmatrix
 */
latexAL([], Tex) :-
	swritef(Tex, "()"),!.
latexAL(L, Tex) :-
	pairs_keys_values(L, Ks, Vs),
	intersperse(" & ", Ks, KsStr),
	intersperse(" & ", Vs, VsStr),
	swritef(Tex, "{(\\begin{smallmatrix}%w \\\\\\\\ %w\\end{smallmatrix})}", [KsStr, VsStr]).

intersperse(_, [], "").
intersperse(_, [X],Str) :- swritef(Str,"%w",[X]).
intersperse(M, [X|XS],Str) :- intersperse(M,XS,Str2), swritef(Str,"%w %s %w",[X,M,Str2]).

/*
 * derivTreeFromFile(filename, interesting, latexGoal, goal)
 * Reads a term from filename,
 * turns it into a goal G using goal(term,G),
 * solves it while generating a proof tree including the interesting goals,
 * renders the proof tree with latexTree and the given latexGoal,
 * writes it to "filename.tex",
 * runs pdflatex on it.
 */
derivTreeFromFile(File,Interesting,LG,Goal) :-
	open(File, read, Stream),
	read(Stream,Input),
	close(Stream),
	call(Goal,Input,TheGoal),
	solve(Interesting,TheGoal,D),
	!, /* Do not backtrace into solve if something else goes wrong now */
	latexTree(LG, D,T),
	completeFile(T,T2),
	swritef(LFile,"%w.tex",[File]),
	open(LFile, write, LStream),
	write_term(LStream,T2, []),
	close(LStream),
	swritef(CMD,"pdflatex %w.tex",[File]),
	ignore(shell(CMD)).

completeFile(Env,Text) :-
	swritef(Text,"\\documentclass[varwidth=300cm,class=article]{standalone}\\usepackage{amsmath,stmaryrd,mathpartir}\\begin{document}\\[%w\\]\\end{document}", [Env]).