% = portray_graph(+Graph)
%
% GraphViz output

:- module(portray_graph_tikz, [portray_graph/1,graph_header/0,graph_footer/1,latex_graph/1]).

:- dynamic '$GRAPH_NO'/1.

graph_header :-
      ( exists_file('graph.tex') -> delete_file('graph.tex') ; true),
	open('graph.tex', write, _, [alias(graph)]),
	format(graph, '\\documentclass{article}~2n', []),
	format(graph, '\\usepackage[a3paper]{geometry}~n', []),
	format(graph, '\\usepackage{amsmath}~n', []),
	format(graph, '\\usepackage{cmll}~n', []),
	format(graph, '\\usepackage{tikz}~n', []),
	format(graph, '\\usetikzlibrary{graphs, graphdrawing}~n', []),
	format(graph, '\\usetikzlibrary{quotes}~n', []),
	format(graph, '\\usegdlibrary{layered}~2n', []),
	format(graph, '\\begin{document}~n', []),
	format(graph, '\\begin{center}~n', []),
	retractall('$GRAPH_NO'(_)),
	assert('$GRAPH_NO'(0)).

graph_footer(P) :-
	'$GRAPH_NO'(N),
	write_graphs(N),
	write_proofs(P),
	format(graph, '\\end{center}~n', []),
	format(graph, '\\end{document}~n', []),
	close(graph),
    (
	access_file('graph.tex', read)
    ->
	/* it is recommended to comment out the following line */
	/* for larger proofs, since lualatex slows down */
	/* considerably for a trace consisting of several */
        /* larger graphs */    
        /* find lualatex in the user's $PATH */
%	absolute_file_name(path(lualatex), LuaLaTeX, [access(execute)]),
%	process_create(LuaLaTeX, ['graph.tex'], [stdout(null)]),
	format('LaTeX graphs ready~n', [])
     ;
        format('LaTeX graph output failed~n', [])
     ).


write_proofs(P) :-
   (
       P =:= 0
   ->
       format(graph, 'No proofs found!~n', [])
   ;
       P =:= 1
   ->
       format(graph, '1 proof found.~n', [])
   ;
       format(graph, '~p proofs found.~n', [P])
   ).

write_graphs(N) :-
   (
       N =:= 0
   ->
       format(graph, 'No graphs output!~n', [])
   ;
       N =:= 1
   ->
       format(graph, '1 graph output.~n', [])
   ;
       format(graph, '~p graphs output.~n', [N])
   ).

latex_graph(G0) :-
	copy_term(G0, G),
 	graph_header,
 	graph_numbervars(G, 0, _),
        format(graph, '{\\tikz \\graph [multi, layered layout, level distance=1.3cm] {~n', []),
        portray_vertices(G, -1, Max),
        portray_edges(G, Max),
        format(graph, '};~2n', []),
	format(graph, '\\end{center}~n', []),
	format(graph, '\\end{document}~n', []),
	told,
    (
	access_file('graph.tex', read)
    ->
        /* find lualatex in the user's $PATH */
	absolute_file_name(path(lualatex), LuaLaTeX, [access(execute)]),
	process_create(LuaLaTeX, ['graph.tex'], [stdout(null)]),
	format('LaTeX graphs ready~n', [])
     ;
        format('LaTeX graph output failed~n', [])
     ).

portray_graph(G) :-
        '$GRAPH_NO'(N0),
	retractall('$GRAPH_NO'(_)),
	N is N0 + 1,
	assert('$GRAPH_NO'(N)),
        /* do temporary numbervars */
\+ \+ ( graph_numbervars(G, 0, _),
        format(graph, '{\\flushleft ~p\\hfill}~2n\\tikz \\graph [multi, layered layout, level distance=1.3cm] {~n', [N]),
        portray_vertices(G, -1, Max),
        portray_edges(G, Max),
        format(graph, '};~2n', [])).

graph_numbervars([], N, N).
graph_numbervars([vertex(_,As,_,_)|Rest], N0, N) :-
	atoms_numbervars(As, N0, N1),
	graph_numbervars(Rest, N1, N).

atoms_numbervars([], N, N).
atoms_numbervars([A|As], N0, N) :-
	atom_numbervars(A, N0, N1),
	atoms_numbervars(As, N1, N).

atom_numbervars(neg(_, _, Vars), N0, N) :-
    numbervars(Vars, N0, N).
atom_numbervars(pos(_, _, Vars), N0, N) :-
    numbervars(Vars, N0, N).
atom_numbervars(neg(_, _, _, _, Vars), N0, N) :-
    numbervars(Vars, N0, N).
atom_numbervars(pos(_, _, _, _, Vars), N0, N) :-
    numbervars(Vars, N0, N).

portray_vertices([], Max, Max).
portray_vertices([vertex(N,As,FVs,_Ps)|Rest], Max0, Max) :-
	format(graph, '~w/{$', [N]),
	portray_fvs(FVs),
	write(graph, '\\ '),
	portray_atoms(As),
	format(graph, '$};~n', []),
	Max1 is max(Max0,N),
	portray_vertices(Rest, Max1, Max).

portray_edges([], _).
portray_edges([vertex(N,_As,_FVs,Ps)|Rest], Max0) :-
	portray_links(Ps, N, Max0, Max),
	portray_edges(Rest, Max).


portray_links([], _, Max, Max).
portray_links([P|Ps], N, Max0, Max) :-
	portray_link(P, N, Max0, Max1),
	portray_links(Ps, N, Max1, Max).

portray_link(univ(A,P), N, Max0, Max) :-
	Max is Max0 + 1,
	format(graph, '~w/{$\\!~@\\!$} [shape=circle,draw];~n', [Max,portray_var(A)]), 
	format(graph, '~w <- ~w;~n~w <- ~w;~n', [N,Max,Max,P]).
portray_link(par(P,Q), N, Max0, Max) :-
	Max is Max0 + 1,
	format(graph, '~w/{$\\!\\parr\\!$} [shape=circle,draw];~n', [Max]),
	format(graph, '~w <- ~w;~n', [N,Max]),
   (
        P =:= Q
   ->
        format(graph, '~w <-[bend left] ~w;~n~w <-[bend right] ~w;~n', [Max,P,Max,Q])
   ;
        format(graph, '~w <- ~w;~n~w <- ~w;~n', [Max,P,Max,Q])
   ).

portray_atoms([]) :-
    write(graph, '\\emptyset').
portray_atoms([A|As]) :-
    write(graph, '\\{'),
    portray_atoms1(As, A).

portray_atoms1([], A) :-
    portray_atom(A),
    write(graph, '\\}').
portray_atoms1([B|Bs], A) :-
    portray_atom(A),
    write(graph, ','),
    portray_atoms1(Bs, B).

portray_atom(neg(A,_,Vars)) :-
    format(graph, '\\overset{-}{~@}',[portray_atom1(Vars, A)]).
portray_atom(pos(A,_,Vars)) :-
    format(graph, '\\overset{+}{~@}',[portray_atom1(Vars, A)]).
portray_atom(neg(A,_,_,_,Vars)) :-
    format(graph, '\\overset{-}{~@}',[portray_atom1(Vars, A)]).
portray_atom(pos(A,_,_,_,Vars)) :-
    format(graph, '\\overset{+}{~@}',[portray_atom1(Vars, A)]).

portray_fvs([]).
portray_fvs([V|Vs]) :-
  (
      var(V)
   ->
      true
   ;
      V = var(N)
   ->
      portray_var(N)
   ;
      true
  ),
  portray_fvs(Vs).

portray_atom1([], Atom) :-
    write(graph, Atom).
portray_atom1([V|Vs], Pred) :-
    format(graph, '~w(~@)', [Pred,portray_vars(Vs,V)]).
    
portray_vars([], V) :-
	portray_var1(V).
portray_vars([V|Vs], W) :-
	portray_var1(W),
	write(graph, ','),
	portray_vars(Vs, V).

portray_var1(Int) :-
	integer(Int),
	!,
	print(graph, Int).
portray_var1(var(N)) :-
	!,
	portray_var(N).
portray_var1('$VAR'(N)) :-
	!,
	print(graph, '$VAR'(N)).
portray_var1(Term) :-
	Term =.. [F0|Args],
	atomic_list_concat(List, '_', F0),
	atomic_list_concat(List, '\\_', F),
	format(graph, '\\textit{~w}', [F]),	
	latex_arguments(Args).

portray_var(N) :-
    VI is N mod 5,
    VN is N//5,
    var_name(VN),
    format(graph, '_{~w}', [VI]).

var_name(0) :-
    write(graph, x).
var_name(1) :-
    write(graph, y).
var_name(2) :-
    write(graph, z).
var_name(3) :-
    write(graph, v).
var_name(4) :-
    write(graph, w).

% = latex_arguments(+ListOfArguments)
%
% write a list of arguments to a predicate ie. (t_1, t_2, t3) sending
% each t_i to print and outputing nothing for a proposition (ie. the
% empty list of arguments.

latex_arguments([]).
latex_arguments([A|As]) :-
	write(graph, '('),
	latex_arguments(As, A),
        write(graph, ')').

latex_arguments([], A) :-
   (
        var(A)
    ->
	format(graph, '\\_', [])
    ;		  
        format(graph, '~@', [portray_var1(A)])
    ).
latex_arguments([A|As], A0) :-
   (
        var(A0)
    ->
	format(graph, '\\_, ', [])
    ;		  
        format(graph, '~@, ', [portray_var1(A0)])
    ),
	latex_arguments(As, A).