%==============================================================================
% Project:	Course "Logic Programming and deductive Databases"
% Version:	Summer 2017, University of Halle
% Module:	sld.pl
% Purpose:	SLD-Metainterpreter with nice output
% Last Change:	02.06.2017
% Language:	LaTeX
% Authors:	Stefan Brass
% Email:	brass@informatik.uni-halle.de
% Address:	Universitaet Halle, Inst. f. Informatik, D-06099 Halle, Germany
% Copyright:	(c) 2017 by Stefan Brass
% Copying:	Do with it what you want, but do not make me responsible.
%		The code might contain bugs! There is no warranty.
%==============================================================================


%------------------------------------------------------------------------------
% Example data for given logic program:
%------------------------------------------------------------------------------

% Test for output of disinct variables with the same name:
%rule(ptest(X), [q(X)], [var('X',X)]).
%rule(q(Y), [r(X,Y)], [var('X',X),var('Y',Y)]).
%rule(r(a,b), [], []).

rule(p(X), [q1(X), q2(X,c)], [var('X', X)]).
rule(p(X), [q3(X,Y), q4(Y)], [var('X', X), var('Y', Y)]).
rule(q1(X), [r1(X), r2(X)], [var('X', X)]).
rule(q1(X), [r3(X)], [var('X', X)]).
rule(q2(X,Z), [s1(X), s2(X,Z)], [var('X', X), var('Z', Z)]).
rule(q3(d,e), [], []).
rule(q4(e), [], []).
rule(r1(a), [], []).
rule(r1(b), [], []).
rule(r2(b), [], []).
rule(r3(c), [], []).
rule(s1(b), [], []).
rule(s2(b,c), [], []).

%------------------------------------------------------------------------------
% Example Query:
%------------------------------------------------------------------------------

goal([p(X)], [var('X',X)]).

%------------------------------------------------------------------------------
% Meta-Interpreter for SLD-Resolution:
%------------------------------------------------------------------------------

sld :-
	goal(Goal, Vars),
	sld(Goal, Vars).

sld(Goal, Vars) :-
	write_sld_node(Goal, 0, Vars),
	sld(Goal, 1, Vars).

sld([], _, _).
sld([Lit|Rest], Depth, Vars) :-
	rule(Head, Body, RuleVars),
	Lit = Head,
	append(Body, Rest, Child),
	append(Vars, RuleVars, NewVars),
	write_sld_node(Child, Depth, NewVars),
	NewDepth is Depth + 1,
	sld(Child, NewDepth, NewVars).

% Output for goals without child nodes (no matching rule):
sld([Lit|_], Depth, _Vars) :-
	\+ rule(Lit, _, _),
	write_fail(Depth),
	fail.

%------------------------------------------------------------------------------
% Indentation:
%------------------------------------------------------------------------------

indent(0).

indent(I) :-
	I > 0,
	write('    '),
	NextI is I - 1,
	indent(NextI).

%------------------------------------------------------------------------------
% Output of a node in the SLD-tree (proof goal):
%------------------------------------------------------------------------------

write_sld_node(Child, Depth, VarList) :-
	indent(Depth),
	write_goal(Child, VarList),
	nl.

write_goal([], _) :-
	write('TRUE.').
write_goal([Lit], VarList) :-
	write_lit(Lit, VarList),
	write('.').
write_goal([Lit1,Lit2|MoreLits], VarList) :-
	write_lit(Lit1, VarList),
	write(', '),
	write_goal([Lit2|MoreLits], VarList).

write_lit(Lit, VarList) :-
	Lit =.. [Pred|Args],
	write(Pred),
	write_arg_list(Args, VarList).

write_arg_list([], _VarList).
write_arg_list([Arg|MoreArgs], VarList) :-
	write('('),
	write_arg(Arg, VarList),
	write_args_rest(MoreArgs, VarList),
	write(')').

write_args_rest([], _VarList).
write_args_rest([Arg|MoreArgs], VarList) :-
	write(', '),
	write_arg(Arg, VarList),
	write_args_rest(MoreArgs, VarList).

write_arg(Arg, _VarList) :-
	atomic(Arg),
	write(Arg).

write_arg(Arg, VarList) :-
	var(Arg),
	write_var(Arg, VarList).

%------------------------------------------------------------------------------
% Printing of Variables:
%------------------------------------------------------------------------------

write_var(Var, VarList) :-
	% First find variable name:
	find_var(Var, VarList, VarName),
	% Then do another pass through the variable list to check
	% how many variables before this one have the same name:
	write_var_suffix(Var, VarName, 0, VarList).

find_var(Var, [var(VarName, SameVar)|_], VarName) :-
	% Cannot use standard unification here, because we compare variables:
	Var == SameVar,
	% The variable might appear with different names,
	% because originally distinct variables might have been unified.
	% We must decide for one variable name:
	!. 

find_var(Var, [_|VarList], VarName) :-
	find_var(Var, VarList, VarName).

% There might be more than one variable with the name.
% Output additional number for all but the first occurrence of the variable:

% Found Variable:
write_var_suffix(Var, VarName, Suffix, [var(VarName,SameVar)|_VarList]) :-
	Var == SameVar,
	write(VarName),
	write_suffix(Suffix).

% Different Variable, but same Variable Name - must increase suffix:
write_var_suffix(Var, VarName, Suffix, [var(VarName,OtherVar)|VarList]) :-
	Var \== OtherVar,
	NextSuffix is Suffix + 1,
	write_var_suffix(Var, VarName, NextSuffix, VarList).

% Different variable, different name - continue searching:
write_var_suffix(Var, VarName, Suffix, [var(DifferentName,_)|VarList]) :-
	VarName \= DifferentName,
	write_var_suffix(Var, VarName, Suffix, VarList).

% The suffix 0 is not printed:
write_suffix(0).

% All other suffixes are printed to distinguish variables:
write_suffix(Suffix) :-
	Suffix > 0,
	write('['),
	write(Suffix),
	write(']').

%------------------------------------------------------------------------------
% Output for goals without child nodes (no matching rule):
%------------------------------------------------------------------------------

write_fail(Depth) :-
	indent(Depth),
	write('FAIL (no matching rule)'),
	nl.