sldnf.1.1.pl

Contenuto del file

% TODO: Cut !
% stop when 1st solution found
% stop negation when 1st solution found
% CLP? Minimize?s

% Version 1.1: stops at a given depth

:- dynamic begin_resolvent/1, end_resolvent/1, begin_binding/1, end_binding/1.

draw_goal(G,FileName):-
    open(FileName,write,File),
    term_length(G,Length),
    conv_sq_list(G,GSq),
    (draw(GSq,File,Length) ; true),
    close(File).

draw(R,F,Longest):-
    draw(R,F,Longest,30).  % Default Max depth: 30

% draw(+Resolvent,+Stream,MaxLenghtOfResolvent,MaxDepth)
draw([],F,Longest,_):-
    NumSpace is Longest//2,
    print_n_spaces(F,NumSpace),
    write(F,"true\n"), 
    print_n_spaces(F,NumSpace),
    fail.
draw(_,F,Longest,0):- !,
    NumSpace is Longest//2,
    print_n_spaces(F,NumSpace),
    write(F,"...\n"), 
    print_n_spaces(F,NumSpace),
    fail.
draw([not G|R],F,LongestIn,Depth):-
    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); true), write(F,"}")
    ),
    writeln(F,"\\end{bundle}}\\end{bundle}"),
    fail.

draw([G|R],F,LongestIn,Depth):-
    Depth1 is Depth-1,
    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_builtin_children(G,R,F,Length,Depth1);     writeln(F,"\\end{bundle}")), 
    fail.    

draw([G|R],F,LongestIn,Depth):-
    Depth1 is Depth-1,
    not(G = not(_)),
    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);     writeln(F,"\\end{bundle}")), 
    fail.

print_children(G,R,F,Length,Depth):-
    Depth1 is Depth-1,
    term_variables(G,Vars),
    vars_names(Vars,VarNames),
    count_children(G,NumChildren),
    (NumChildren = 1 -> Len = Length ; Len=0),
    clausola(G,B),
    write(F,"\\chunk"),
    print_binding(F,VarNames),
    write(F,"{"),
    append(B,R,Ris),
    (draw(Ris,F,Len,Depth1) ; write(F,"}"), fail).
print_children(G,_,F,Length,_Depth):-
    not(clausola(G,_)),
    print_fail(F,Length),
    %write(F,"\\chunk{fail}"),
    fail.

print_builtin_children(G,R,F,Length,Depth):-
    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) ; write(F,"}"), fail).
print_builtin_children(G,_,F,Length,_Depth):-
    not(call(G)),
    print_fail(F,Length),
    %write(F,"\\chunk{fail}"),
    fail.

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).
%print_binding(F,X):-
%    write(F,"[$"),
%    writeln(F,X),
%    write(F,"$]").

var_name(X,N):-
    open(string(""),write,Stream),
    write(Stream,X),
    get_stream_info(Stream, name, N),
    close(Stream).

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(F,B), write(F,"/"), write_term_no_sqbrack(F,A), 
    (T=[] -> true
        ; write(F,", "), print_binding1(F,T)).

% Writes a term replacing the symbols "[" and "]"
% with \lbrack and \rbrack, because you cannot use "["
% inside a label of an arc.
write_term_no_sqbrack(F,A):-
    var(A), !, write(F,A).
write_term_no_sqbrack(F,[]):- !,
    write(F,"\\lbrack\\rbrack ").
write_term_no_sqbrack(F,[H|T]):- !,
    write(F,"\\lbrack "),
    print_list_no_sqbrack(F,[H|T]),
    write(F,"\\rbrack ").
write_term_no_sqbrack(F,T):- 
    T =.. [Fun], !,
    write(F,Fun).
write_term_no_sqbrack(F,T):- !,
    T =.. [Fun|Arg],
    write(F,Fun),
    write(F,"("),
    print_list_no_sqbrack(F,Arg),
    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(F,V):-
    var(V), !,
    write_term_no_sqbrack(F,V).
print_list_no_sqbrack(F,[H|T]):-
    var(T),!,
    write_term_no_sqbrack(F,H),
    write(F,"$|$"),
    write_term_no_sqbrack(F,T).
print_list_no_sqbrack(F,[H]):-
    write_term_no_sqbrack(F,H).
print_list_no_sqbrack(F,[H1,H2|T]):-
    write_term_no_sqbrack(F,H1),write(F,","),
    print_list_no_sqbrack(F,[H2|T]).


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]):- !,
    write_term_no_sqbrack(F,H).
print_list(F,[H1,H2|T]):-
    write_term_no_sqbrack(F,H1),write(F,","),
    print_list(F,[H2|T]).

print_fail(F,Longest):-
    NumSpace is Longest//2,
    write(F,"\\chunk{"),
    print_n_spaces(F,NumSpace),
    write(F,"false\n"), 
    print_n_spaces(F,NumSpace),
    write(F,"}").

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_string(G,S), string_length(S,Length).

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).