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