% ----- Use dot and ghostview/gv to display the search tree -----

% Added by Hans Leiss (HL), CIS, Uni-Muenchen, 2012.
% Added 10.2.2013: branch for disjunctions and show unifier for equations

why(Goal) :-  % show search tree for goal
    sld(Goal),
    shell('dot -T ps -o sld.ps sld.dot'),
    shell('gv sld.ps &').

why2(Goal) :- % show search tree for goal with substitutions at edges
    sld2(Goal),
    shell('dot -T ps -o sld.ps sld.dot'),
    shell('gv sld.ps &').

show(Term) :-  
    term(Term),
    shell('dot -T ps -o term.ps term.dot'),
    shell('gv term.ps &').

why2(Goal,_Depth) :-
    var(Goal),!,
    write('Error: the first argument of why/2 must not be a variable!\n'),
    write('Usage: why(+Goal,+Depth bound for search tree)'),
    fail.
why2(_Goal,Depth) :-
    var(Depth),!,
    write('Error: the second argument of why/2 must be a nonnegative number!\n'),
    write('Usage: why(+Goal,+Depth bound for search tree)'),
    fail.
why2(Goal,Depth) :-
    sld2(Goal,Depth),
    shell('dot -T ps -o sld.ps sld.dot'),
    shell('gv sld.ps &').    
    
% See sld2 added at the end of the file.

% ----------------------------------------------------------------------
% Source: http://www.cs.bris.ac.uk/Teaching/Resources/COMS30106/graphviz/ 

%%% Plotting terms as trees using Graphviz %%%

term_list_linear(false).	% change to true for plotting lists linearly

term(Term):-
	gv_start('term.dot'),
	Term =.. [Functor|Subterms],
	gv_root(Functor,0),
	term_list(Subterms,0),
	gv_stop.

term(Term,N):-
	var(Term),!,
	gv_node(N,Term,_).
term(Term,N):-
	term_list_linear(true),
	list(Term),!,
	gv_node(N,Term,N1),
	term_list(Term,N1).
term([],N):-!,
	gv_node(N,'$empty_list',_).
term(Term,N):-
	Term =.. [Functor|Subterms],
	gv_node(N,Functor,N1),
	term_list(Subterms,N1).

term_list([],_).
term_list([Term|Terms],N):-
	term(Term,N),
	term_list(Terms,N).

% testing
term1:-term([a,b,b,a]).
term2:-term(
html(head(title('Peter A. Flach')),
	body([img([align=right,src='logo.jpg']),
		img([align=left,src='peter.jpg']),
		h1('Peter Flach\'s homepage'),
		h2('Research interests'),
		ul([li('Learning from structured data'),
			bla,
			li(a([href='CV.pdf'],'Full CV'))]),
		h2('Current activities'),
		bla,
		h2('Past activities'),
		bla,
		h2('Archives'),
		bla,
		hr,address(bla)
	    ])
         )
).


%%% Meta-interpreter plotting (part of) the SLD-tree using Graphviz %%%

:-op(1100,fx,sld).	% can write ?-sld Goal instead of ?-sld(Goal)

sld(Goal):-
	sld(Goal,10).	% default depth bound % HL: raised from 5 to 10

sld(Goal,D):-
	gv_start('sld.dot'),
	gv_root((?-Goal),0),
	prove_d(Goal,Goal,0,D),
	fail.	% failure-driven loop to get all solutions
sld(_,_):-
	gv_stop.

% meta-interpreter with complete resolvent and depth bound
prove_d(true,Goal,N,_):-!,
	gv_answer(N,Goal).
prove_d(_,_Goal,N,D):- % HL
        D=0, !, gv_stop(N).
prove_d((A,B),Goal,N,D):-!,
	D>0, D1 is D-1,
	resolve(A,C),
	conj_append(C,B,E),
	gv_node(N,(:-E),N1),
	prove_d(E,Goal,N1,D1).
prove_d(_,_Goal,N,D):- % HL
	D=0,!, gv_stop(N).
prove_d(A,Goal,N,D):-
	D>0, D1 is D-1,
	resolve(A,B),
	gv_node(N,(:-B),N1),
	prove_d(B,Goal,N1,D1).

resolve(A,true):-
	predicate_property(A,built_in),!,
	call(A).
resolve(A,B):-
	clause(A,B).

% testing
student_of(X,T):-follows(X,C),teaches(T,C).
follows(paul,computer_science).
follows(paul,expert_systems).
follows(maria,ai_techniques).
teaches(adrian,expert_systems).
teaches(peter,ai_techniques).
teaches(peter,computer_science).

brother_of(paul,peter).
brother_of(peter,adrian).
brother_of(X,Y):-brother_of(X,Z),brother_of(Z,Y).
brother_of(X,Y):-brother_of(Y,X).

sld1:-sld student_of(_,peter).
sld2:-sld brother_of(paul,_).


%%% Utilities %%%

list([]).
list([_|T]):-list(T).

conj_element(X,X):-	% single-element conjunction
	X \= true,
	X \= (_,_).
conj_element(X,(X,_)).
conj_element(X,(_,Ys)):-
	conj_element(X,Ys).

conj_append(true,Ys,Ys).
conj_append(X,Ys,(X,Ys)):-	% single-element conjunction
	X \= true, 
	X \= (_,_).
conj_append((X,Xs),Ys,(X,Zs)):-
	conj_append(Xs,Ys,Zs).

writes([]):-!,nl.
writes([H|T]):-!,writes(H),writes(T).
writes((A,B)):-!,writes(A),write(',\\n'),writes(B).	% break up conjunctions
writes({}) :- !, write({}).               % HL
writes({A,B}) :- !,                       % HL
    write('{'),writes((A,B)),writes('}'). % HL
writes(:-A):-!,write(':-'),writes(A).
writes(?-A):-!,write('?-'),writes(A).
writes('$empty_list'):-!,write([]).
writes(A):-write(A).	% catch-all

	
%%% Graphviz utilities %%%

gv_max_id(1000).	% max number of nodes in the graph

% open file and start new graph
gv_start(FileName):-
	tell(FileName),
	writes(['digraph {']),
	%writes(['graph [size="4,6"];']),
	writes(['edge [shape=plaintext, fontname=Courier, fontsize=12]']), % HL
	writes(['node [shape=plaintext, fontname=Courier, fontsize=12]']).

% next graph
gv_next:-
	writes(['}']),
	writes(['digraph {']),
	writes(['node [shape=plaintext, fontname=Courier, fontsize=12]']).

% finish graph and close file
gv_stop:-
	writes(['}']),
	told.

% start new subgraph
gv_cluster_start:-
	( retract('$gv_cluster'(N)) -> N1 is N+1
	; otherwise -> N1=0
	),assert('$gv_cluster'(N1)),
	writes(['subgraph cluster_',N1,' {']),
	writes(['[style=filled, color=lightgrey];']),
	writes(['node [style=filled,color=white];']).

% finish subgraph 
gv_cluster_stop:-
	writes(['}']).

% write the root of a tree and initialise node IDs
gv_root(L,N):-
	writes([N,' [label="',L,'"];']),
	gv_init_ids(N).

% add a node with label L and parent N0
gv_node(N0,L,N):-
	gv_id(N),
	writes([N,' [label="',L,'"];']),
	writes([N0,' -> ',N,';']).

% add a specially formatted leaf
gv_answer(N0,L):-
	gv_id(N),
	writes([N,' [label="Answer:\\n ',L,'", shape=ellipse, style=dotted, fontsize=10];']),
	writes([N0,' -> ',N,' [style=dotted, arrowhead=none,length=0];']).
	% writes(['{rank=same;',N0,';',N,';}']).

% generate a new node ID
gv_id(N):-
	retract('$gv_id'(N0)),
	gv_max_id(M),
	N0 < M,	% don't generate infinite graphs
	N is N0+1,
	assert('$gv_id'(N)).

% initialise node IDs, next free ID is N+1
gv_init_ids(N) :-
	retractall('$gv_id'(_)),
	assert('$gv_id'(N)).

% -----------------------------------------------------------------------------
% Added by HL:

%%% Meta-interpreter plotting (part of) the SLD-tree using Graphviz %%%

sld2(Goal):-
	sld2(Goal,10).	% default depth bound

sld2(Goal,D):-
	gv_start('sld.dot'),
	gv_root((?-Goal),0),
	prove_d2(Goal,Goal,0,D),
	fail.	% failure-driven loop to get all solutions
sld2(_,_):-
	gv_stop.

% -------- modify graphviz to show the substitions -------

% meta-interpreter with complete resolvent and depth bound

prove_d2(true,Goal,N,_):-!,
	gv_answer(N,Goal).
prove_d2((A,B),Goal,N,D):-!,
	(D=0 -> gv_stop(N)
        ; D>0, D1 is D-1,
            resolve(A,C,S),
            conj_append(C,B,E),
            gv_node2(N,(:-E),N1,S),
            prove_d2(E,Goal,N1,D1)
        ).
prove_d2(A,Goal,N,D):-
	(D=0 -> gv_stop(N)
        ; D>0, D1 is D-1,
            resolve(A,B,S),
            gv_node2(N,(:-B),N1,S),
            prove_d2(B,Goal,N1,D1)
        ).

% add a node with label L and parent N0
gv_node2(N0,L,N,S):-
	gv_id(N),!,
	writes([N0,' -> ',N,' [label="',S,'"]',';']),
        % now apply S to N and L
        applySubst(S),
	writes([N,' [label="',L,'"];']). 
gv_node2(_N0,_L,_N,_S):-
	write(user,'Maximal number 1000 of tree nodes reached!'),
        fail.

resolve((A;B),E,{}) :-
    !, (E=A;E=B).      % branch to two subnodes
resolve(A,true,Subst):-
    predicate_property(A,built_in),!,
    (functor(A,(=),2)  
    -> unify(A,Subst)  % show the unifying substitution
    ; solve(A,Subst)). % hide the unification with fresh vars of heads
resolve(Goal,B,Subst) :-
    copy_term(Goal,GoalCopy),
    clause(GoalCopy,B),
    Goal =.. [F|Args],
    GoalCopy =.. [F|ArgsCopy],
    pairs(Args,ArgsCopy,Pairs),
    (Pairs = true -> Subst = {} ; Subst = {Pairs}).
    
solve(Goal,Subst) :-
    copy_term(Goal,GoalCopy),
    call(GoalCopy),
    Goal =.. [F|Args],
    GoalCopy =.. [F|ArgsCopy],
    pairs(Args,ArgsCopy,Pairs),
    (Pairs = true -> Subst = {} ; Subst = {Pairs}).

pairs([X|Xs],[Y|Ys],Pairs) :-
    (compound(X), compound(Y) ->
        X =.. [_|XArgs], Y =.. [_|YArgs],
        append(XArgs,Xs,XS),
        append(YArgs,Ys,YS),
        pairs(XS,YS,Pairs)
    ; % X,Y lead to at most one substitution pair X/Y or Y/X
        pairs(Xs,Ys,XsYs),
        % don't use copied variables in the result
        (var(X), var(Y) -> X=Y ; true), 
        (var(X) -> (X==Y -> Pair=true ; Pair=Y/X) % can be simplified
        ; (var(Y) -> Pair=X/Y ; Pair=true)    % if we don't use copied
        ),                                    % variables
        (XsYs = true -> Pairs=Pair
        ; Pair=true -> Pairs=XsYs ; Pairs = (Pair,XsYs)
        )
    ).
pairs([],[],true).

unify((S = T),Subst) :-
    (\+ \+ (S = T)), % S and T are unifiable
    unify([S],[T],Subst).
unify([X|Xs],[Y|Ys],Subst) :- 
    (compound(X), compound(Y) ->
        X =.. [_|XArgs], Y =.. [_|YArgs], 
        append(XArgs,Xs,XS),
        append(YArgs,Ys,YS),
        unify(XS,YS,Subst)
    ; (var(X) -> (X==Y -> Sub={} ; Sub={Y/X}) 
      ; (var(Y) -> Sub={X/Y} ; Sub={})    
      ),                                   
        ( Sub={} -> unify(Xs,Ys,Subst)
        ; apply_to_all(Sub,Xs,XsP),
            apply_to_all(Sub,Ys,YsP),
            unify(XsP,YsP,SubstP),
            compose(Sub,SubstP,Subst)
        )
    ).
unify([],[],{}).

apply_to_all(_Subst,[],[]) :- !.
apply_to_all(Subst,[T|Ts],[R|Rs]) :-
    apply(Subst,T,R),
    apply_to_all(Subst,Ts,Rs).

apply({S/Y, Pairs},T,R) :-
    var(T), !, (Y == T -> R=S ; apply({Pairs},T,R)).
apply({S/Y},T,ST) :-
    var(T), !, (Y == T -> ST=S ; ST=T).
apply({},T,T) :- !.
    
apply(_Subst,T,T)  :-
    atomic(T), !.
apply(Subst,T,R) :-
    T =.. [F|Args],
    apply_to_all(Subst,Args,RArgs),
    R =.. [F|RArgs].

% assume disjoint domains
compose({},Subst,Subst) :- !.
compose(Subst,{},Subst) :- !.
compose({S/X},{Pairs},Subst) :-
    !, apply({Pairs},S,T),
    Subst = { T/X, Pairs }.
compose({S/X,Pairs},Subst,Composed) :-
    compose({Pairs},Subst,CompSubst),
    apply(Subst,S,R),
    Composed = { R/X,CompSubst }.
    

applySubst({}).
applySubst({X/Y}) :- X=Y.
applySubst({X/Y,Subst}) :- X=Y, applySubst({Subst}).

% add a specially formatted leaf to indicate depth-bound % HL
gv_stop(N):-
	writes([N,' [label="Stopped\\n (max.depth)",
               shape=ellipse, style=dotted, fontsize=10];']).

% ----------------------------------------------------------------------
