% SLDNF Draw
% Produces a LaTeX drawing of an SLDNF tree
% Author: Marco Gavanelli
% http://www.ing.unife.it/docenti/MarcoGavanelli/sldnfDraw/

% Version 1.4
% Does not crash when printing infinite terms
% Uses lib(var_names) for pretty printing the names of variables.

sldnf_version(1.4).

% TODO:
% stop when 1st solution found
% stop negation when 1st solution found
% CLP? Minimize?

:- lib(var_name).

% Note that it does not handle correctly the cut in the resolvent, but only
% in a clause. Please, do not write ?- p,!. but define e new predicate
% callp:- p,!.

% Given a clause a:-b,!,c, we have that:
% 1.the scope of the cut is a:-b, in the sense that it will cut the
%   alternatives to a and b. This is represented with the list
%   of OpenCuts: it contains all the cuts that are in a clause that
%   has been selected.
% 2.The cut has an effect when it is reached, and its effect lasts
%   until the backtracking goes back to a. Thus, the information about
%   reaching a cut is saved with assert(reached(Cut)).
%   Each cut has a unique name, given by a counter.

:- dynamic begin_resolvent/1, end_resolvent/1, begin_binding/1, end_binding/1, counter/1, reached/1, maxdepth/1.
:- dynamic my_clause/2.

set_depth(D):-
    retract(maxdepth(_)),
    assert(maxdepth(D)).

maxdepth(20). % Default max depth: 20

draw_goal(G,FileName):-
    init_file(FileName,write,File),
    term_length(G,Length),
    conv_sq_list(G,GSq),
    init_cuts,
    (draw(GSq,File,Length) ; true),
    close(File).

draw(R,F,Longest):-
    maxdepth(Depth),
    draw(R,F,Longest,Depth,[]).

% draw(+Resolvent,+Stream,MaxLenghtOfResolvent,MaxDepth,OpenCuts)
draw([],F,Longest,_,_):-
    print_string_spaces(F,Longest,"true"),
    fail.
draw(_,F,Longest,0,_):- !,
    print_string_spaces(F,Longest,"..."),
    fail.
draw([not G|R],F,LongestIn,Depth,OpenCuts):-
    Depth1 is Depth-1,
    write(F,"\\begin{bundle}{"),
    print_resolvent(F,[not G|R]),
    writeln(F,"}\n\\chunk{"),
    % NOTA: forse in questo caso non conviene metterlo, cosi` il box diventa giusto.
    %       pero` non si assicura che sia giusto il figlio del box...
    % Compute the maximum length
    term_length([not G|R],ResLen), Length is max(LongestIn,ResLen),
    write(F,"\\begin{bundle}{\\framebox{"),
    (draw([G],F,0,Depth1,[]) ; true),
    write(F,"}}"),
    (vanilla(G)
      ->    print_fail(F,ResLen)
      ;     write(F,"\\chunk{"),
                (draw(R,F,Length,Depth1,OpenCuts); true), write(F,"}")
    ),
    writeln(F,"\\end{bundle}}\\end{bundle}"),
    fail.

% Cut !
draw([!|R],F,LongestIn,Depth,[LastCut|OpenCuts]):- !,
    Depth1 is Depth-1,
    term_length([!|R],ResLen), Length is max(LongestIn,ResLen),
    write(F,"\\begin{bundle}{"),
    print_resolvent(F,[!|R]),
    writeln(F,"}"),
    assert(reached(LastCut)),
    (print_builtin_children(true,R,F,Length,Depth1,OpenCuts);     writeln(F,"\\end{bundle}")), 
    fail.    

% Conjunction of goals: may occur inside another predicate, like not((G1,G2)).
draw([(G1,G2)|R],F,LongestIn,Depth,OpenCuts):-
    draw([G1,G2|R],F,LongestIn,Depth,OpenCuts).

% Built-in Predicate
draw([G|R],F,LongestIn,Depth,OpenCuts):-
    Depth1 is Depth-1,
    not(G = not(_)),
    not(G=(_,_)),
    built_in(G),
    term_length([G|R],ResLen), Length is max(LongestIn,ResLen),
    write(F,"\\begin{bundle}{"),
    print_resolvent(F,[G|R]),
    writeln(F,"}"),
    (print_builtin_children(G,R,F,Length,Depth1,OpenCuts);     writeln(F,"\\end{bundle}")), 
    fail.    

% User defined predicate
draw([G|R],F,LongestIn,Depth,OpenCuts):-
    Depth1 is Depth-1,
    not(G = not(_)),
    not(G=(_,_)),
    not(built_in(G)),
    term_length([G|R],ResLen), Length is max(LongestIn,ResLen),
    write(F,"\\begin{bundle}{"),
    print_resolvent(F,[G|R]),
    writeln(F,"}"),
    (print_children(G,R,F,Length,Depth1,OpenCuts);     writeln(F,"\\end{bundle}")), 
    fail.

print_children(G,R,F,Length,Depth,OpenCuts):-
    Depth1 is Depth-1,
    term_variables(G,Vars),
    vars_names(Vars,VarNames),
    count_children(G,NumChildren),
    (NumChildren = 1 -> Len = Length ; Len=0),
    increase_counter, get_counter(C), 
    % Unique name for the node: if a cut is reached, it will have this name
    % First part: the cut may cut the alternatives for the clause
    retract_cut_on_backtracking(C),
    clausola(G,B),
    (clause_is_not_cut(C)
        ->  true
        ;   write(F,"\\chunk{(cut)}"), fail),
    (check_body_contains_cut(B,OpenCuts,NewCuts,_AddedCut,C)
        ->    % retract_cut_on_backtracking(AddedCut)
              true
        ;     NewCuts=OpenCuts),
    % Second part: takes care of the alternatives of the predicates
    % in the body
    ( (member(Cut,OpenCuts),reached(Cut))
      ->        write(F,"\\chunk{(cut)}"), fail
      ;         write(F,"\\chunk"),
                print_binding(F,VarNames),
                write(F,"{"),
                append(B,R,Ris),
                (draw(Ris,F,Len,Depth1,NewCuts) ; write(F,"}"), fail)
    ).

print_children(G,_,F,Length,_Depth,_):-
    not(clausola(G,_)),
    print_fail(F,Length),
    fail.

print_builtin_children(G,R,F,Length,Depth,OpenCuts):-
    Depth1 is Depth-1,
    term_variables(G,Vars),
    vars_names(Vars,VarNames),
    findall(G,call(G),L),length(L,NumChildren),
    (NumChildren = 1 -> Len = Length ; Len=0),
    call(G),
    write(F,"\\chunk"),
    print_binding(F,VarNames),
    write(F,"{"),
    (draw(R,F,Len,Depth1,OpenCuts) ; write(F,"}"), fail).
print_builtin_children(G,_,F,Length,_Depth,_OpenCuts):-
    not(call(G)),
    print_fail(F,Length),
    fail.

%%%%%%%%%%%%%%%% Predicates fot cut handling %%%%%%%%%%%%%%%%%

%check_body_contains_cut(+Body,++OpenCuts,-NewCuts,-AddedCut,++Counter)
check_body_contains_cut(B,OpenCuts,NewCuts,AddedCut,Counter):-
    memberchk(!,B),push_cut(OpenCuts,NewCuts,AddedCut,Counter).


% A clause is not cut if the cut of the current
% node has not been reached.
clause_is_not_cut(C):-
    not reached(cut(C)).

push_cut(L,[cut(C)|L],cut(C),C).

% On backtracking, remove the information about the reached cuts
% that are not open
retract_cut_on_backtracking(_).
retract_cut_on_backtracking(C):-
    retract(reached(C)), fail.

follows(cut(N),cut(N1)):-
    N>N1.

last_cut([C],C):-!.
last_cut([Cut|Cuts],C):-
    last_cut(Cuts,LastSoFar),
    (follows(LastSoFar,Cut)
        ->  C=LastSoFar
        ;   C=Cut).

init_cuts:- retract_all(reached(_)),
    reset_counter.

increase_counter:-
    counter(C), retract(counter(C)), C1 is C+1,
    assert(counter(C1)).
get_counter(C):- counter(C).
reset_counter:- retract_all(counter(_)),
    assert(counter(0)).

%%%%%%%%%%%%%%% End predicates for cut handling %%%%%%%%%%%%%%

%%%%%%%%%%%%%%% Utilities %%%%%%%%%%%%%%

count_children(G,NumChildren):-
    findall(B,clausola(G,B),L),
    length(L,NumChildren).

vars_names([],[]).
vars_names([X|T],[b(X,N)|TN]):-
    var_name(X,N),
    vars_names(T,TN).

term_to_string(Term,String):-
    open(string(""),write,Stream),
    write(Stream,Term),
    get_stream_info(Stream, name, String),
    close(Stream).

var_name(X,N):-
    get_var_name(X,N),!.
var_name(X,NewName):-
    term_to_string(X,N),
    (var(X)
     -> % if the variable name starts with underscore, set X as its name
        (string_list(N,[95|_]) -> set_var_name(X,'X') 
            ; set_var_name(X,N)),
        get_var_name(X,NewName)
     ;  NewName=N).

print_binding(F,X):-
    write(F,"["),
    (begin_binding(S) -> write(F,S); true),
    print_binding1(F,X),
    (end_binding(Send) -> write(F,Send) ; true),
    write(F,"]").

print_binding1(_F,[]).
print_binding1(F,[b(A,B)|T]):-
    var_name(A,Name),
    Name = B, !,
    % Avoid writing "X=X" as a binding...
    print_binding1(F,T).
print_binding1(F,[b(A,B)|T]):-
    write_var(F,B), write(F,"/"),
    (acyclic_term(A)
      ->    write_term_no_sqbrack(F,A,1000)
      ;     maxdepth(D), write_term_no_sqbrack(F,A,D)
    ), 
    (T=[] -> true
        ; write(F,", "), print_binding1(F,T)).

write_var(F,V):-
    var(V),
    var_name(V,VarName),!,
    split_string(VarName,"#","",[Name,Number]),
    write(F,"$"),
    write(F,Name),
    write(F,"_{"),
    write(F,Number),
    write(F,"}$").
write_var(F,VarName):-
    string(VarName),
    split_string(VarName,"#","",[Name,Number]),!,
    write(F,"$"),
    write(F,Name),
    write(F,"_{"),
    write(F,Number),
    write(F,"}$").

% Writes a term replacing the symbols "[" and "]"
% with \lbrack and \rbrack, because you cannot use "["
% inside a label of an arc.
% Stops at depth Depth
% write_term_no_sqbrack(File,Term,Depth):-
write_term_no_sqbrack(F,_,0):- !,
    write(F,"\\dots").
write_term_no_sqbrack(F,A,_):-
    % Named Variables
    var(A), !,
    write_var(F,A).
write_term_no_sqbrack(F,[],_):- !,
    write(F,"\\lbrack\\rbrack ").
write_term_no_sqbrack(F,[H|T],N):- !,
    write(F,"\\lbrack "),
    print_list_no_sqbrack(F,[H|T],N),
    write(F,"\\rbrack ").
write_term_no_sqbrack(F,T,_):- 
    T =.. [Fun], !,
    write(F,Fun).
% infixed operators
write_term_no_sqbrack(F,T,N):-
    T =.. [Fun,ArgX,ArgY],
    N1 is N-1,
    current_op(_,Associativity,Fun),
    (Associativity = xfy ; Associativity = yfx ; Associativity = xfx),!,
    write_term_no_sqbrack(F,ArgX,N1),
    pretty_write_op(F,Fun),
    write_term_no_sqbrack(F,ArgY,N1).
write_term_no_sqbrack(F,T,N):- !,
    N1 is N-1,
    T =.. [Fun|Arg],
    write(F,Fun),
    write(F,"("),
    print_list_no_sqbrack(F,Arg,N1),
    write(F,")").

% If the list is a difference list, we also have the 
% case in which the rest is a variable.
%print_list_no_sqbrack(File,Term,Depth)
print_list_no_sqbrack(F,V,N):-
    var(V), !,
    write_term_no_sqbrack(F,V,N).
print_list_no_sqbrack(F,[H|T],N):-
    var(T),!,
    write_term_no_sqbrack(F,H,N),
    write(F,"$|$"),
    write_term_no_sqbrack(F,T,N).
print_list_no_sqbrack(F,[H],N):- !,
    write_term_no_sqbrack(F,H,N).
print_list_no_sqbrack(F,[H1,H2|T],N):-
    N1 is N-1,
    write_term_no_sqbrack(F,H1,N1),write(F,","),
    print_list_no_sqbrack(F,[H2|T],N1).

pretty_write_op(F,<):- !,
    write(F,$<$).
pretty_write_op(F,=<):- !,
    write(F,$=<$).
pretty_write_op(F,>=):- !,
    write(F,$>=$).
pretty_write_op(F,>):- !,
    write(F,$>$).
pretty_write_op(F,is):- !,
    write(F," is ").
pretty_write_op(F,\=):- !,
    write(F,"$\\backslash=$").
pretty_write_op(F,Op):- !,
    write(F,Op).

print_resolvent(F,X):-
    (begin_resolvent(S) -> write(F,S); true),
    print_list(F,X),
    (end_resolvent(Send) -> write(F,Send) ; true).

print_list(F,[H]):- !,
    maxdepth(D),
    write_term_no_sqbrack(F,H,D).
print_list(F,[H1,H2|T]):-
    maxdepth(D),
    write_term_no_sqbrack(F,H1,D),write(F,","),
    print_list(F,[H2|T]).

print_fail(F,Longest):-
    write(F,"\\chunk{"),
    print_string_spaces(F,Longest,"false"),
    write(F,"}").

% Prints a string adding "Longest" spaces.
print_string_spaces(F,Longest,String):-
    NumSpace is Longest//2,
    print_n_spaces(F,NumSpace),
    write(F,String), writeln(F,"\n"), 
    print_n_spaces(F,NumSpace).

print_n_spaces(_,0):- !.
print_n_spaces(F,N):-
    number(N), N>0,
    write(F,"~"),
    N1 is N-1,
    print_n_spaces(F,N1).

vanilla([]).
vanilla([A|B]) :- !, vanilla(A), vanilla(B).
vanilla(not X) :- !,
    (vanilla(X) -> fail ; true).
vanilla(X) :-
    built_in(X), call(X).
vanilla(X) :-
    clausola(X,Body),
    vanilla(Body).

term_length(G,Length):-
    term_to_string(G,S), 
    string_length(S,Length).

remove_char(Sin,Char,Sout):-
    split_string(Sin,Char,"",SubStrings),
    concat_string(SubStrings,Sout).

clausola(H,BSq):-
    functor(H,F,A), current_predicate(F/A),
    clause(H,B),
    conv_sq_list(B,BSq).
clausola(H,BSq):-
    my_clause(H,BSq).

conv_sq_list((A,B),[A|Bsq]):- !,
    conv_sq_list(B,Bsq).
conv_sq_list(true,[]):- !.
conv_sq_list(X,[X]).

built_in(G):-
    functor(G,F,A),
    current_built_in(F/A).

init_file(FileName,write,File):-
    open(FileName,write,File),
    write(File,"% File created by SLDNF Draw version "),
    sldnf_version(Ver),
    writeln(File,Ver),
    writeln(File,"% http://www.ing.unife.it/docenti/MarcoGavanelli/sldnfDraw/"),
    nl(File).
