#!/usr/bin/pl -q -t main -f
%%%%
%%%% Usage:
%%%%
%%%% proofs_to_dot [-tTYPE] [-dOUT_DIR] [-fOUT_BASENAME] FILE
%%%%
%%%% FILE contains Prolog readable Goal-Proof statements. For each
%%%% statement a graph file is written in directory OUT_DIR (default /tmp).
%%%% Depending on the format a dot file (TYPE dot, default) or a gif image
%%%% (TYPE gif) is written. Filenames are of the form OUT_BASENAMENNNNN.dot or
%%%% OUT_BASENAMENNNNN.gif, where NNNNN is a zero padded number,
%%%% starting from 1. OUT_BASENAME defaults to 'proof_'.
%%%%
%%%% Modified version, adapted to E-KRHyper.
%%%%

:- use_module('../contrib/pl/dotgraph').
:- use_module('../contrib/pl/swilib/pretty').
:- use_module('../contrib/pl/swilib/onto_atom').
:- use_module('../contrib/pl/swilib/fromonto').
:- use_module('../contrib/pl/swilib/err').

:- op(900, fy, ~).

node_color(_, _, false, '#ffb0b0') :- !.
node_color(branch, _, _, '#ffffa0') :- !.
node_color(split, _, _, '#ffffa0') :- !.
node_color(_, input_fact, _, '#b0ffb0') :- !.
node_color(_, input_clause, _, '#8fca02') :- !.
node_color(_, hyper(_), _, '#b0e0ff') :- !.
node_color(_, _, _, '#e0e0e0').
% node_color(X, _, '#ffffa0').

edge_color(complement, '#e00000') :- !.
edge_color(branch, '#909000') :- !.
edge_color(_, black) :- !.

proof_to_dotgraph(Proof, Dotgraph) :-
	Dotgraph =
	dotgraph(proof,
		 [graph_attributes([]),
		  edge_defaults([]),
		  node_defaults([fontsize=12, fontname='Arial'])|
		 NodesAndEdges]),
	proof_to_dotgraph_1(Proof, std, Nodes, [], Edges, []),
	append(Nodes, Edges, NodesAndEdges).
	
proof_id(node(Id, _, _, _, _), Id) :- !.
proof_id(split(Id, _, _, _), Id) :- !.
proof_id(branch(Id, _, _), Id) :- !.
proof_id(ref(Id), Id) :- !.
proof_id(P, _) :-
	( nonvar(P) -> functor(P, F, N) ; true ),
	err('Bad proof term with functor: ~q/~q.', [F,N]).

node_avs(Mode, Rule, Term, [style=filled, fillcolor=Color|AVs]) :-
	node_color(Mode, Rule, Term, Color),
        ( Mode == split ->
	  AVs = [shape='record', label=RuleA],	    
          pp_rule(Rule, RuleA)
        ; Mode == branch ->
	  AVs = [shape=ellipse, label=TermA],	    
	  onto_atom(write(Term), TermA)
        ; AVs = [shape=record, label=rec(rec(TermA, RuleA))],
	  onto_atom(write(Term), TermA),
	  pp_rule(Rule, RuleA)
	).

strip_trailing_newline(Atom, Atom1) :-
	sub_atom(Atom, B, 1, 0, '\n'),
	!,
	sub_atom(Atom, 0, B, _, Atom1).
strip_trailing_newline(Atom, Atom).

pp_rule(hyper(Clause), RuleA) :-
	!,
	onto_atom(pp_clause(Clause), ClauseA),
	strip_trailing_newline(ClauseA, ClauseA1),
	RuleA = rec(hyper, ClauseA1).
pp_rule(Rule, RuleA) :-
	onto_atom(write(Rule), RuleA).

map_edge([X|Xs], Id, Mode,
	 [edge(Id, Id1, [color=Color|AVs])|Xs1], Xs2) :-
	edge_color(Mode, Color),
	( Mode == branch ->
	  AVs = [dir=none, style=bold]
	; AVs = [dir=back]
	),
	proof_id(X, Id1),
	map_edge(Xs, Id, Mode, Xs1, Xs2).
map_edge([], _, _, Xs, Xs).

proof_to_dotgraph_1(ref(_), _, Ns, Ns, Es, Es) :-
	!.
proof_to_dotgraph_1(node(Id, Term, Rule, Subproofs, NegSubproofs),
		    Mode, Ns, Ns1, Es, Es1) :-
	!,
	map_edge(Subproofs, Id, Mode, Es, Es2),
	map_edge(NegSubproofs, Id, complement, Es2, Es3),
	node_avs(Mode, Rule, Term, AVs),
	Ns = [node(Id, AVs)|Ns2],
	map_proof_to_dotgraph(Subproofs, Ns2, Ns3, Es3, Es4),
	map_proof_to_dotgraph(NegSubproofs, Ns3, Ns1, Es4, Es1).
proof_to_dotgraph_1(split(Id, Rule, Subproofs, NegSubproofs),
		    _Mode, Ns, Ns1, Es, Es1) :-
	!,
	proof_to_dotgraph_1(node(Id, null, Rule, Subproofs, NegSubproofs),
			    split, Ns, Ns1, Es, Es1).
proof_to_dotgraph_1(branch(Id, Term, Subproof), _Mode, Ns, Ns1, Es, Es1) :-
	!,
	proof_to_dotgraph_1(node(Id, Term, null, [Subproof], []),
			    branch, Ns, Ns1, Es, Es1).
proof_to_dotgraph_1(P, _, _, _, _, _) :-
	( nonvar(P) -> functor(P, F, N) ; true ),
	err('Bad proof term with functor: ~q/~q.', [F,N]).

map_proof_to_dotgraph([P|Ps], Ns, Ns1, Es, Es1) :-
	proof_to_dotgraph_1(P, std, Ns, Ns2, Es, Es2),
	map_proof_to_dotgraph(Ps, Ns2, Ns1, Es2, Es1).
map_proof_to_dotgraph([], Ns, Ns, Es, Es).

proofs_to_dot(File, OutDir, OutBasename, Mode) :-
	ensure_dir(OutDir),
	open(File, read, Stream),
	( repeat,
	  read_term(Stream, Term, [double_quotes(atom)]),
	  ( Term == end_of_file ->
	    !,
	    close(Stream),
	    true
	  ; ( Term = _-Proof -> true
	    ; Term = node(_, _, _, _, _) ->
	      Proof = Term
	    ; Term = branch(_, _, _) ->
	      Proof = Term
	    ) ->
	    flag(count, N, N+1),
	    sformat(Filename, '~w~`0t~d~11|', [OutBasename, N]),
	    concat_atom([OutDir, '/', Filename, '.', Mode], Pathname),
	    proof_to_dot(Proof, Mode, Pathname),
	    fail
	  ; err('Unexpected input statement: ~q.', [Term])
	  )
	  ; true
	).

proof_to_dot(Proof, Mode, Pathname) :-
	format(user_error, 'Writing ~w.\n', [Pathname]),
	proof_to_dotgraph(Proof, Dotgraph),
	( Mode = gif ->
	  write_gif_dotgraph(Dotgraph, Pathname)
	; onto_file(print_dotgraph(Dotgraph), Pathname)
	).

process_argv :-
	current_prolog_flag(argv, Argv), 
	append(_, [--|Args], Argv),
	!,
	get_option(t, Args, dot, Type),
	get_option(d, Args, '/tmp', Dir),
	get_option(f, Args, 'proof_', Basename),
	flag(count, _, 1),
	( enum_regular_arg(Args, File),
	  format(user_error, 'Processing ~w.\n', [File]),	
	  proofs_to_dot(File, Dir, Basename, Type),
	  fail
	; true
	).

enum_regular_arg(Args, Arg) :-
	member(Arg, Args),
	\+ sub_atom(Arg, 0, 1, _, '-').

get_option(Option, Args, _, Value) :-
	member(Arg, Args),
	sub_atom(Arg, 0, 1, _, '-'),
	sub_atom(Arg, 1, 1, _, Option),
	!,
	sub_atom(Arg, 2, _, 0, Value).
get_option(_, _, Default, Default).
	
ensure_dir(Dir) :-
        exists_directory(Dir), !.
ensure_dir(Dir) :-
        file_directory_name(Dir, Parent),
        ensure_dir(Parent),
	format(user_error, 'Creating directory ~w.\n', [Dir]),
        make_directory(Dir).

main :-
        catch(process_argv, E, (print_message(error, E), fail)),
        halt.                                           
main :-
        halt(1).