/* 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]).