%==============================================================================
% Project:	An Improved Magic Set Technique
% Version:	0.2
% Module:	sldmagic.pl
% Purpose:	Computation of Conditional Facts and Rewritten Program
% Created:	05.03.1996
% Last Change:	20.03.2000
% Language:	Prolog (ECLiPSe 3.5.1, SWI-Prolog 2.5.0, Quintus-Prolog 3.2)
% Author:	Stefan Brass
% Email:	sbrass@sis.pitt.edu
% Address:	Univ. of Pittsburgh, School of Information Sc., PA 15260, USA
% Copyright:	(C) 1996-2000  Stefan Brass
% Copying:	Permitted under the GNU General Public Licence.
%==============================================================================

%------------------------------------------------------------------------------
%    I wrote this program in a hurry, so:
%    - It probably contains still a number of bugs
%      (I am interested to hear about them if you find them).
%    - No attempt was made to use more efficient data structures.
%    - The programming style and comments are not optimal.
%    I hope that I can improve this program later.
%    Please send me an email if you want to here about future versions.
%
%    This program is free software; you can redistribute it and/or
%    modify it under the terms of the GNU General Public License
%    as published by the Free Software Foundation; either version 2
%    of the License, or (at your option) any later version.
%    
%    This program is distributed in the hope that it will be useful,
%    but WITHOUT ANY WARRANTY; without even the implied warranty of
%    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%    GNU General Public License for more details.
%    
%    You should have received a copy of the GNU General Public License
%    along with this program; if not, write to the Free Software
%    Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
%------------------------------------------------------------------------------

%sldmagic(Filename) :-
sldmagic :-
	sldmagic_clear,
	%load_program(Filename),
	%print_data,
	init_cond,
	%print_cond,
	nl,
	nl,
	write('Partial Evaluation is running ...'),
	nl,
	nl,
	part_eval,
	%print_cond,
	%print_prog,
	optimize.
	%print_opt_prog.

% Uncomment this for ECLiPSe:
%retract_all(Head) :- retractall(Head).

% This is for ECLiPSe and SWI-Prolog:
%write_quote :- write('\'').
% This is for Quintus-Prolog (also understood by SWI-Prolog):
write_quote :- write('''').

%==============================================================================
% Portability Definitions:
%==============================================================================

%------------------------------------------------------------------------------
% list_append(+List1, +List2, -List12):
%------------------------------------------------------------------------------

list_append([], List, List).

list_append([Head|Tail], List, [Head|Tail_List]) :-
	list_append(Tail, List, Tail_List).

%------------------------------------------------------------------------------
% list_member(+Elem, +List):
%------------------------------------------------------------------------------

list_member(Elem, [Elem|_]) :-
	!.

list_member(Elem, [_|Rest]) :-
	list_member(Elem, Rest).

%------------------------------------------------------------------------------
% int_max(+N +M, -Max):
%------------------------------------------------------------------------------

int_max(N, M, N) :-
	N >= M,
	!.

int_max(N, M, M) :-
	N < M.

%==============================================================================
% Dynamic Database:
%==============================================================================

%------------------------------------------------------------------------------
% List of Option Values:
%------------------------------------------------------------------------------

%:- dynamic option/2.
option(derive_idb_literals, yes).
option(use_query_const, yes).

%------------------------------------------------------------------------------
% List of EDB-Predicates:
%------------------------------------------------------------------------------

%:- dynamic edb_pred/2.

%------------------------------------------------------------------------------
% List of IDB-Predicates:
%------------------------------------------------------------------------------

%:- dynamic idb_pred/2.

%------------------------------------------------------------------------------
% List of Program Rules:
%------------------------------------------------------------------------------

%:- dynamic rule/2.

%------------------------------------------------------------------------------
% List of Query Patterns:
%------------------------------------------------------------------------------

% This predicate contains the given query.
% query(Query, Query_Pattern, Cond_Vars, Cond_Vals).
% Query is the query as entered, but with variables bound to terms of the form
% var(i) with a unique number i.
% If use_query_const is yes, Query_Pattern is the same as Query and Cond_Vars
% and Cond_Vals are [].
% If use_query_const is no, Query_Pattern is computed from Query by replacing
% constants also by terms of the from var(i).
% These terms are collected in Cond_Vars, and the corresponding constants are
% collected in Cond_Vals.

%:- dynamic query/4.

%------------------------------------------------------------------------------
% List of Conditional Facts:
%------------------------------------------------------------------------------

:- dynamic cond/2.

%------------------------------------------------------------------------------
% List of Rewritten Rules:
%------------------------------------------------------------------------------

:- dynamic prog/2.

%------------------------------------------------------------------------------
% Seed Fact with query constants:
%------------------------------------------------------------------------------

% If use_query_const is no, and the query contains constants, a fact is
% generated which contains the constants from the query.
% This fact is contained in prog/2, but in order to print a comment for this
% fact, we repeat it here:

:- dynamic query_const/1.

%------------------------------------------------------------------------------
% List of Optimized Rewritten Rules:
%------------------------------------------------------------------------------

:- dynamic opt_prog/2.

%------------------------------------------------------------------------------
% clear:
%------------------------------------------------------------------------------

% This predicate clears the dynamic database, i.e. removes all facts from it.

sldmagic_clear :-
	%retractall(option(_,_)),
	%retractall(edb_pred(_,_)),
	%retractall(idb_pred(_,_)),
	%retractall(rule(_,_)),
	%retractall(query(_,_,_,_)),
	retractall(cond(_,_)),
	retractall(prog(_,_)),
	retractall(query_const(_)),
	retractall(opt_prog(_,_)).

%------------------------------------------------------------------------------
% save_option(+Option, +Value):
%------------------------------------------------------------------------------

% This predicate stores an option setting in the dynamic database.
% Each option must have a unique value, so it first checks whether the
% option is already defined.
% If it is already defined with a different value, it fails.

save_option(Option, Value) :-
	option(Option, Defined_Value),
	!,
	Value = Defined_Value.

save_option(Option, Value) :-
	assert(option(Option, Value)).

%------------------------------------------------------------------------------
% use_option(+Option, ?Value):
%------------------------------------------------------------------------------

% This predicate checks whether a given option has a given value.
% The default for all options is "no", so if no value is defined,
% we check for "no".
% In that case, we store the value "no" in the dynamic database
% in order to exclude that later a different value for the option is defined.

use_option(Option, Value) :-
	option(Option, Defined_Value),
	!,
	Value = Defined_Value.

use_option(Option, Value) :-
	save_option(Option, no),
	Value = no.



%------------------------------------------------------------------------------
% save_cond(+Fact, +Cond):
%------------------------------------------------------------------------------

save_cond(Fact, Cond) :-
	cond(Fact, Cond),
	!.

save_cond(Fact, Cond) :-
	assert(cond(Fact, Cond)).

%------------------------------------------------------------------------------
% save_prog(+Head, Body):
%------------------------------------------------------------------------------

save_prog(Head, Body) :-
	prog(Head, Body),
	!.

save_prog(Head, Body) :-
	assert(prog(Head, Body)).

%------------------------------------------------------------------------------
% save_query_const(+Fact):
%------------------------------------------------------------------------------

save_query_const(Fact) :-
	assert(query_const(Fact)).

%------------------------------------------------------------------------------
% save_opt_prog(+Head, Body):
%------------------------------------------------------------------------------

save_opt_prog(Head, Body) :-
	assert(opt_prog(Head, Body)).

%==============================================================================
% Reserved Words, Generated Predicate Names:
%==============================================================================

%------------------------------------------------------------------------------
% reserved_word(+Pred):
%------------------------------------------------------------------------------

% This predicate is used to check that a predicate in an input program is
% not the name of an option or another command of this program.
% Generated predicate names have the form "pNumber", e.g. p0, p1, etc.
% Therefor all predicate names starting with the letter p and followed by
% a digit are forbidden.

reserved_word(Gen_Pred) :-
	name(Gen_Pred, [112, Digit|_]),   % 112 = ASCII code of 'p'.
	digit(Digit),
	!.
reserved_word(db).
reserved_word(use_query_const).
reserved_word(derive_idb_literals).
reserved_word(call).
reserved_word(params).

%------------------------------------------------------------------------------
% digit(+ASCII):
%------------------------------------------------------------------------------

% This predicate is true when ASCII is the ASCII code of a digit 0-9.

digit(48). % 0
digit(49). % 1
digit(50). % 2
digit(51). % 3
digit(52). % 4
digit(53). % 5
digit(54). % 6
digit(55). % 7
digit(56). % 8
digit(57). % 9

%==============================================================================
% Parser for Input Programs:
%==============================================================================

%------------------------------------------------------------------------------
% Operator for Defining Database Literals:
%------------------------------------------------------------------------------

% E.g. an input line can be:   db edge/2.

%:- op(1000, fy, db).

%------------------------------------------------------------------------------
% Operators for Defining Options:
%------------------------------------------------------------------------------

% E.g. an input line can be:   use_query_const yes.

%:- op(1000, fy, use_query_const).
%:- op(1000, fy, derive_idb_literals).



%------------------------------------------------------------------------------
% parse_yes_or_no(+Yes_Or_No):
%------------------------------------------------------------------------------

% This predicate checks that the value of an option is yes or no.

parse_yes_or_no(yes).

parse_yes_or_no(no).



%------------------------------------------------------------------------------
% replace_vars(+List_of_Atoms):
%------------------------------------------------------------------------------

% This predicate bind all variables occurring in the body of an input rule to
% a term of the form var(i), where i is a unique number starting from 0.
% The body is already transformed into a list of atoms.

replace_vars(List_of_Atoms) :-
	replace_vars(List_of_Atoms, 0).

replace_vars([], _).

replace_vars([Atom|Body], Var_No) :-
	rep_vars_atom(Atom, Var_No, Next_Var_No),
	replace_vars(Body, Next_Var_No).

%------------------------------------------------------------------------------
% rep_vars_atom(+Atom, +Var_No, -Next_Var_No):
%------------------------------------------------------------------------------

% This predicate binds all variables occurring in an atom to a term of the from
% var(i). The atom can have the form pred(args) or call(pred(args)).
% The args are constants or variables (or terms of the form var(i)).
% Var_No is the next variable number which is still unused.
% After all replacements are done, Next_Var_No is returned, which is then
% the next still free variable number.

rep_vars_atom(call(Atom), Var_No, Next_Var_No) :-
	!,
	Atom =.. [_|Args],
	rep_vars_args(Args, Var_No, Next_Var_No).

rep_vars_atom(Atom, Var_No, Next_Var_No) :-
	Atom =.. [_|Args],
	rep_vars_args(Args, Var_No, Next_Var_No).

%------------------------------------------------------------------------------
% rep_vars_args(+Args, +Var_No, -Next_Var_No):
%------------------------------------------------------------------------------

% This predicate implements the loop over the arguments of an atom from the
% input program. It also does the bookeeping for the next free variable number.

rep_vars_args([], Var_No, Var_No).

rep_vars_args([Arg|Args], Var_No_0, Var_No_2) :-
	rep_vars_arg(Arg, Var_No_0, Var_No_1),
	rep_vars_args(Args, Var_No_1, Var_No_2).

%------------------------------------------------------------------------------
% rep_vars_arg(+Arg, +Var_No, -Next_Var_No):
%------------------------------------------------------------------------------

% This predicate binds variable arguments to terms of the form var(i).
% In this case the current variable number i (Var_No) must be increased,
% so that every variable gets a unique number.
% However, an argument can also be a constant or a term of the form var(j)
% which indicates that the same variable appeared already somewhere to the
% left and was there already bound to a term of this form.

rep_vars_arg(Arg, Var_No, Next_Var_No) :-
	var(Arg),
	Arg = var(Var_No),
	Next_Var_No is Var_No + 1.

rep_vars_arg(Arg, Var_No, Var_No) :-
	atomic(Arg).

rep_vars_arg(var(No), Var_No, Var_No) :-
	number(No).



%==============================================================================
% Initialization of Conditional Facts:
%==============================================================================

%------------------------------------------------------------------------------
% init_cond:
%------------------------------------------------------------------------------

% For every edb predicate p, we create a conditional fact of the form
% db(p(X0,...,Xn)) :- p(X0,...,Xn).

init_cond :-
	%edb_pred(Pred, Arity),
	edb_pred(Pred, Types),
	length(Types, Arity),
	make_varlist(Arity, 0, Varlist),
	Atom =.. [Pred|Varlist],
	save_cond(db(Atom), Atom),
	fail.

% For every rule A :- B1, ..., Bm of the input program, we create a conditional
% fact of the form   rule(A, [B1,...,Bm]) :- true.

init_cond :-
	sldmagic_rule(Head, Body),
	save_cond(rule(Head,Body), true),
	fail.

% The query is more tricky because we have to distinguish two cases according
% to whether constants in the query were replaced by variables:

init_cond :-
	query(_, Query_Pattern, Cond_Vars, Cond_Vals),
	init_query_cond(Query_Pattern, Cond_Vars, Cond_Vals),
	fail.

% Ok, all conditional facts created (in the above rules):

init_cond.

%------------------------------------------------------------------------------
% make_varlist(+Num_Vars, +Start_Var_No, +Varlist):
%------------------------------------------------------------------------------

% This predicate produces a variable list in internal format.
% E.g. [var(0), var(1), var(2)].
% This would be the result of the call make_varlist(3, 0, Var_List).

make_varlist(Num_Vars, Num_Vars, []).

make_varlist(Num_Vars, Start_Var_No, [var(Start_Var_No)|Rest_Varlist]) :-
	Start_Var_No < Num_Vars,
	Next_Var_No is Start_Var_No + 1,
	make_varlist(Num_Vars, Next_Var_No, Rest_Varlist).

%------------------------------------------------------------------------------
% init_query_cond(+Query_Pattern, +Cond_Vars, +Cond_Vals):
%------------------------------------------------------------------------------

init_query_cond(Query_Pattern, [], []) :-
	!,
	save_cond(query(Query_Pattern), true).

init_query_cond(Query_Pattern, Cond_Vars, Cond_Vals) :-
	next_pred_no(N),
	save_cond(query(Query_Pattern), params(N,Cond_Vars)),
	save_prog(params(N,Cond_Vals), []),
	save_query_const(params(N,Cond_Vals)).

%==============================================================================
% Unparser (Print All Data):
%==============================================================================

%------------------------------------------------------------------------------
% print_data:
%------------------------------------------------------------------------------

% This predicate is called after the input program is read.
% It shows all the data which are input for the transformation.

print_data :-
	print_all_options,
	print_all_rules,
	print_all_edb,
	print_all_queries.

%------------------------------------------------------------------------------
% print_all_options:
%------------------------------------------------------------------------------

% This predicate prints all option settings in the dynamic database.

print_all_options :-
	nl,
	write('Options:'),
	nl,
	write('======='),
	nl,
	fail.

print_all_options :-
	valid_option(Option),
	use_option(Option, Value),
	write('	'),	% This is a TAB
	write(Option),
	write(': '),
	write(Value),
	nl,
	fail.

print_all_options.

valid_option(use_query_const).
valid_option(derive_idb_literals).

%------------------------------------------------------------------------------
% print_all_rules:
%------------------------------------------------------------------------------

% This predicate prints all input rules stored in the dynamic database.

print_all_rules :-
	nl,
	write('Input Rules:'),
	nl,
	write('==========='),
	nl,
	sldmagic_rule(Head, Body),
	write('	'),	% This is a TAB
	print_rule(Head, Body),
	nl,
	fail.

print_all_rules.

%------------------------------------------------------------------------------
% print_rule(+Head, +Body):
%------------------------------------------------------------------------------

% This predicate is used to print an input rule.

print_rule(Fact, []) :-
	!,
	print_lit(Fact),
	write('.').

print_rule(Head, Body) :-
	print_lit(Head),
	write(' :- '),
	print_goal(Body),
	write('.').

%------------------------------------------------------------------------------
% print_all_edb:
%------------------------------------------------------------------------------

% This predicate prints all edb predicate declarations in the dynamic database.

print_all_edb :-
	nl,
	write('EDB-Predicates:'),
	nl,
	write('=============='),
	nl,
	edb_pred(Predicate, Arity),
	write('	'),	% This is a TAB
	write(Predicate),
	write('/'),
	write(Arity),
	write('.'),
	nl,
	fail.

print_all_edb.

%------------------------------------------------------------------------------
% print_all_queries:
%------------------------------------------------------------------------------

% This predicate prints the query literals in the dynamic database.
% There should be only one.

print_all_queries :-
	nl,
	write('Query:'),
	nl,
	write('====='),
	nl,
	query(Query, _, _, _),
	write('	'),	% This is a TAB
	print_lit(Query),
	write('.'),
	nl,
	fail.

print_all_queries.

%------------------------------------------------------------------------------
% print_goal(+Goal):
%------------------------------------------------------------------------------

print_goal([]) :-
	write('true').

print_goal([Lit|Goal]) :-
	print_lit(Lit),
	print_goal_rest(Goal).

%------------------------------------------------------------------------------
% print_goal_rest(+Goal):
%------------------------------------------------------------------------------

print_goal_rest([]).

print_goal_rest([Lit|Goal]) :-
	write(', '),
	print_lit(Lit),
	print_goal_rest(Goal).

%------------------------------------------------------------------------------
% print_lit(+Atom):
%------------------------------------------------------------------------------

print_lit(params(N, Args)) :-
	!,
	write('p'),
	write(N),
	print_args(Args).

print_lit(Atom) :-
	Atom =.. [Pred|Args],
	write(Pred),
	print_args(Args).

%------------------------------------------------------------------------------
% print_args(+Args):
%------------------------------------------------------------------------------

print_args([]).

print_args([Arg|Args]) :-
	write('('),
	print_arg(Arg),
	print_args_rest(Args),
	write(')').

%------------------------------------------------------------------------------
% print_args_rest(+Args):
%------------------------------------------------------------------------------

print_args_rest([]).

print_args_rest([Arg|Args]) :-
	write(','),
	print_arg(Arg),
	print_args_rest(Args).

%------------------------------------------------------------------------------
% print_arg(+Arg):
%------------------------------------------------------------------------------

print_arg(var(Var_No)) :-
	!,
	write('X'),
	write(Var_No).

print_arg(Const) :-
	atomic(Const),
	!,
	write(Const).

print_arg([First|Rest]) :-
	!,
	write('['),
	print_arg(First),
	print_list_rest(Rest),
	write(']').

print_arg(Term) :-
	Term =.. [Functor|Args],
	write(Functor),
	print_args(Args).

%------------------------------------------------------------------------------
% print_list_rest:
%------------------------------------------------------------------------------

% This is called from print_arg if the argument has a list structure.
% print_arg prints [, first element, and ].

print_list_rest([]).

print_list_rest([First|Rest]) :-
	write(','),
	print_arg(First),
	print_list_rest(Rest).

%------------------------------------------------------------------------------
% print_cond:
%------------------------------------------------------------------------------

% List all conditional facts in the dynamic database.

print_cond :-
	nl,
	write('Conditional Facts:'),
	nl,
	write('================='),
	nl,
	cond(Fact, Cond),
	write('	'), % This is a TAB.
	print_lit(Fact),
	write(' :- '),
	print_lit(Cond),
	write('.'),
	nl,
	fail.

print_cond.

%------------------------------------------------------------------------------
% print_prog:
%------------------------------------------------------------------------------

% This predicate prints all rewritten rules stored in the dynamic database.

print_prog :-
	nl,
	write('Rules after Partial Evaluation:'),
	nl,
	write('=============================='),
	nl,
	prog(Head, Body),
	write('	'),	% This is a TAB
	print_rule(Head, Body),
	print_comment(Head, Body),
	nl,
	fail.

print_prog.

%------------------------------------------------------------------------------
% print_comment(+Head, +Body):
%------------------------------------------------------------------------------

% This prints a comment about a rule in the rewritten program
% (if the rule is special).

print_comment(Head, []) :-
	query_const(Head),
	!,
	write(' % Seed fact with query constants.').

print_comment(_, _).

%------------------------------------------------------------------------------
% print_opt_prog:
%------------------------------------------------------------------------------

% This predicate prints all rewritten rules stored in the dynamic database
% after the "copy-rule" elimination is done.

print_opt_prog :-
	nl,
	write('Rules after Copy Rule Elimination:'),
	nl,
	write('================================='),
	nl,
	opt_prog(Head, Body),
	write('	'),	% This is a TAB
	print_rule(Head, Body),
	nl,
	fail.

print_opt_prog.

%==============================================================================
% The Meta Interpreter:
%==============================================================================

%------------------------------------------------------------------------------
% meta(-Head, -Body):
%------------------------------------------------------------------------------

% These are the input rules for the partial evaluation.

% Initialization (Root Node):
%	node(Query, [Query]) :-
%		query(Query).
%	var(0) = Query.

meta(node(var(0), [var(0)]),
	[query(var(0))]).

% SLD-Resolution:
%	node(Query, Child) :-
%		node(Query, [Lit|Rest]),
%		rule(Lit, Body),
%		append(Body, Rest, Child).
%	var(0) = Query.
%	var(1) = Child.
%	var(2) = Lit.
%	var(3) = Rest.
%	var(4) = Body.

meta(node(var(0), var(1)),
	[node(var(0), [var(2)|var(3)]),
	 rule(var(2), var(4)),
	 sys_eval(append(var(4), var(3), var(1)))]).

% Evaluation of a DB-Literal:
%	node(Query, Rest) :-
%		node(Query, [Lit|Rest]),
%		db(Lit).
%	var(0) = Query.
%	var(1) = Rest.
%	var(2) = Lit.

meta(node(var(0), var(1)),
	[node(var(0), [var(2)|var(1)]),
	 db(var(2))]).

% Turn Proven Query into Answer:
%	answer(Query) :-
%		node(Query, []).
%	var(0) = Query.

meta(answer(var(0)),
	[node(var(0), [])]).

% Set Up Recursive Call (Derive Magic Fact):
%	query(Lit) :-
%		node(_, [call(Lit)|_]).
%	var(0) = Lit.
%	var(1) = _.
%	var(2) = _.

meta(query(var(0)),
	[node(var(1), [call(var(0))|var(2)])]).

% Get Result of Recursive Call:
%	node(Query, Rest) :-
%		node(Query, [call(Lit)|Rest]),
%		answer(Lit).
%	var(0) = Query.
%	var(1) = Rest.
%	var(2) = Lit.

meta(node(var(0), var(1)),
	[node(var(0), [call(var(2))|var(1)]),
	 answer(var(2))]).

%==============================================================================
% Computation of Rewritten Program:
%==============================================================================


%XXX

%==============================================================================
% Maximal Used Variable Numbers:
%==============================================================================

% These predicates return the first free variable number,
% i.e. one above the highest used numbers.

%------------------------------------------------------------------------------
% max_var(+Term, -Max_Var):
%------------------------------------------------------------------------------

max_var(var(I), I_Plus_One) :-
	!,
	I_Plus_One is I + 1.

max_var(Const, 0) :-
	atomic(Const),
	!.

max_var(Term, Max_Var) :-
	Term =.. [_|Args],
	max_var_list(Args, Max_Var).

%------------------------------------------------------------------------------
% max_var_list(+List, -Max_Var):
%------------------------------------------------------------------------------

max_var_list([], 0).

max_var_list([Term|List], Max_Var) :-
	max_var(Term, Term_Max_Var),
	max_var_list(List, List_Max_Var),
	int_max(Term_Max_Var, List_Max_Var, Max_Var).

%==============================================================================
% Fresh Variables:
%==============================================================================

% These predicates renumber variables in such a way that
% the used numbers are disjoint from the numbers in a given node.
% This is important before unification.
% The caller has to compute the offset with max_var (or with these predicates),
% then these predicates simply add the offset to all variables
% occurring in the input term.
% Offset_Out will be one above the highest variable number in the output term,
% or the Offset_In if the term contains no variables.

%------------------------------------------------------------------------------
% fresh_var(+Term_In, +Offset_In, -Term_Out, -Offset_Out):
%------------------------------------------------------------------------------

fresh_var(var(I), Var_Offset, var(I_Plus_Offset), I_Plus_Offset_Plus_One) :-
	!,
	I_Plus_Offset is I + Var_Offset,
	I_Plus_Offset_Plus_One is I_Plus_Offset + 1.

fresh_var(Const, Offset, Const, Offset) :-
	atomic(Const),
	!.

fresh_var(Term_In, Offset_In, Term_Out, Offset_Out) :-
	Term_In =.. [Functor|Args_In],
	fresh_var_list(Args_In, Offset_In, Args_Out, Offset_Out),
	Term_Out =.. [Functor|Args_Out].

%------------------------------------------------------------------------------
% fresh_var_list(+List_In, +Offset_In, -List_Out, -Offset_Out):
%------------------------------------------------------------------------------

fresh_var_list([], Offset, [], Offset).

fresh_var_list([Term_In|List_In], Offset_In, [Term_Out|List_Out], Offset_Out):-
	fresh_var(Term_In, Offset_In, Term_Out, Offset_1),
	fresh_var_list(List_In, Offset_In, List_Out, Offset_2),
	int_max(Offset_1, Offset_2, Offset_Out).

%==============================================================================
% Unification:
%==============================================================================

%------------------------------------------------------------------------------
% unify(+Term1, +Term2, -Subst):
%------------------------------------------------------------------------------

unify(Term1, Term2, Subst) :-
	empty_subst(Empty),
	unify(Term1, Term2, Empty, Subst).

%------------------------------------------------------------------------------
% unify(+Term1, +Term2, +Subst_In, -Subst_Out):
%------------------------------------------------------------------------------

% When we do the unification, we must implicitly dereference the pointers.
% So if one of the two input terms is a bound variable, we replace it by
% the term to which it is bound.
% This may be repeated for reference chains.
% After this is done, we do the real unification step.

unify(var(X), Term2, Subst_In, Subst_Out) :-
	bound(Subst_In, var(X), Term1),
	!,
	unify(Term1, Term2, Subst_In, Subst_Out).

unify(Term1, var(X), Subst_In, Subst_Out) :-
	bound(Subst_In, var(X), Term2),
	!,
	unify(Term1, Term2, Subst_In, Subst_Out).

unify(Term1, Term2, Subst_In, Subst_Out) :-
	unify_step(Term1, Term2, Subst_In, Subst_Out).

%------------------------------------------------------------------------------
% unify_step(+Arg1, +Arg2, +Subst_In, -Subst_Out):
%------------------------------------------------------------------------------

% This is the classical unification step.
% If the two input terms are equal, we are done
% (note that no Prolog unification happens here, since we have replaced all
% Prolog variables by terms of the form var(i).)
% The test for equal input terms is imporaant, so that we dont generate
% cyclic bindings like X/X.
% Otherwise, if one of the two terms is a variable, we replace it by the
% other term.
% Finally, we do the unification recursively for structured terms.
% Of course, the main functor must be the same in this case.

unify_step(Arg, Arg, Subst, Subst) :-
	!.

unify_step(var(X), Val, Subst_In, Subst_Out) :-
	!,
	subst_add(Subst_In, var(X), Val, Subst_Out).

unify_step(Val, var(X), Subst_In, Subst_Out) :-
	!,
	subst_add(Subst_In, var(X), Val, Subst_Out).
	
unify_step(Term1, Term2, Subst_In, Subst_Out) :-
	Term1 =.. [Functor|Args1],
	Term2 =.. [Functor|Args2],
	unify_list(Args1, Args2, Subst_In, Subst_Out).

%------------------------------------------------------------------------------
% unify_list(+List1, +List2, +Subst_In, -Subst_Out):
%------------------------------------------------------------------------------

unify_list([], [], Subst, Subst).

unify_list([Term1|List1], [Term2|List2], Subst_In, Subst_Out) :-
	unify(Term1, Term2, Subst_In, Subst),
	unify_list(List1, List2, Subst, Subst_Out).

%==============================================================================
% Substitutions:
%==============================================================================

% This is an abstract datatype, substitutions should only be constructed and
% applied via these predicates (the implementation may change).
% The current implementation is a list of pairs "map(Var,Val)".
% We do not really compose substitutions, but simply add the replacement at the
% end of the list. This means that we must process the whole list when applying
% a substitution (instead of stopping at the first match).

%------------------------------------------------------------------------------
% empty_subst(-Empty):
%------------------------------------------------------------------------------

empty_subst([]).

%------------------------------------------------------------------------------
% subst_add(+Subst_In, +Var, +Val, -Subst_Out):
%------------------------------------------------------------------------------

% This predicate adds the replacement Var/Val to the given substitution.

subst_add([], Var, Val, [map(Var,Val)]).

subst_add([Map|Subst_In], Var, Val, [Map|Subst_Out]) :-
	subst_add(Subst_In, Var, Val, Subst_Out).

%------------------------------------------------------------------------------
% apply_subst_list(+Goal_In, +Subst, -Goal_Out):
%------------------------------------------------------------------------------

% This predicate applies a substitution to a list of terms (by applying it to
% every list element).
% The list of terms can be a goal (list of literals), but it can also be an
% argument list.

apply_subst_list([], _, []).

apply_subst_list([Term_In|List_In], Subst, [Term_Out|List_Out]) :-
	apply_subst_term(Term_In, Subst, Term_Out),
	apply_subst_list(List_In, Subst, List_Out).

%------------------------------------------------------------------------------
% apply_subst_term(+Term_In, +Subst, -Term_Out):
%------------------------------------------------------------------------------

% This predicate applies a substitution to a given term.
% The three cases are:
% (1) the term is a constant, therefore it is not changed by the substitution.
% (2) the term is a variable, then we check the substitution whether it
%     contains a replacement for this variable,
% (3) the term is structured, then we apply the substitution recursively to its
%     arguments. The functor remains unchanged.

apply_subst_term(Const, _, Const) :-
	atomic(Const),
	!.

apply_subst_term(var(No), Subst, Term_Out) :-
	bound(Subst, var(No), Term),
	!,
	apply_subst_term(Term, Subst, Term_Out).

apply_subst_term(var(No), _, var(No)) :-
	% \+ bound(Subst, var(No), Term),
	!.

apply_subst_term(Term_In, Subst, Term_Out) :-
	Term_In =.. [Functor|Args_In],
	apply_subst_list(Args_In, Subst, Args_Out),
	Term_Out =.. [Functor|Args_Out].

%-------------------------------------------------------------------------------
% bound(+Subst, +Term_In, -Term_Out):
%------------------------------------------------------------------------------

% This predicate replaces bound variables by the term they are bound to.
% It does only one step in following a reference chain.
% So if it is successful, it must be called again.
% If it is not successful, the variable is not bound.

bound([map(Var,Term)|_], Var, Term).

bound([_|Subst], Var, Term) :-
	bound(Subst, Var, Term).

%==============================================================================
% Normalization:
%==============================================================================

% The goal of this predicates is to number variables
% consecutively beginning with 0.
% This is important because otherwise we would not detect that a derived
% conditional fact is equal to one we already have.

%------------------------------------------------------------------------------
% normalize(+Term_In, -Term_Out):
%------------------------------------------------------------------------------

normalize(Term_In, Term_Out) :-
	normalize(Term_In, [], 0, Term_Out, _, _).

%------------------------------------------------------------------------------
% normalize(+Term_In, +Map_In, +Next_Var_In, -Term_Out,-Map_Out,-Next_Var_Out):
%------------------------------------------------------------------------------

normalize(var(I), Map_In, Next_Var_In, var(J), Map_In, Next_Var_In) :-
	map(Map_In, var(I), var(J)),
	!.

normalize(var(I), Map_In, Next_Var, var(Next_Var),
		[map(var(I),var(Next_Var))|Map_In], Next_Var_Out) :-
	% \+map(Map_In, var(I), var(J)),
	!,
	Next_Var_Out is Next_Var + 1.

normalize(Const, Map, Next_Var, Const, Map, Next_Var) :-
	atomic(Const),
	!.

normalize(Term_In, Map_In, Next_Var_In, Term_Out, Next_Var_Out, Map_Out) :-
	Term_In =.. [Functor|List_In],
	normalize_list(List_In, Map_In, Next_Var_In, List_Out, Next_Var_Out,
		Map_Out),
	Term_Out =.. [Functor|List_Out].

%------------------------------------------------------------------------------
% normalize_list(+List_In,+Map_In,+N_Var_In, -List_Out,-N_Var_Out,-Map_Out):
%------------------------------------------------------------------------------

normalize_list([], Map, Next_Var, [], Map, Next_Var).

normalize_list([Term_In|List_In], Map_In, Next_Var_In,
		[Term_Out|List_Out], Map_Out, Next_Var_Out) :-
	normalize(Term_In, Map_In, Next_Var_In, Term_Out, Map, Next_Var),
	normalize_list(List_In, Map, Next_Var, List_Out, Map_Out,Next_Var_Out).

%------------------------------------------------------------------------------
% map(+Map, +Var_In, -Var_Out):
%------------------------------------------------------------------------------

map([map(Var_In,Var_Out)|_], Var_In, Var_Out).

map([_|Rest], Var_In, Var_Out) :-
	map(Rest, Var_In, Var_Out).

%==============================================================================
% Derive Conditional Facts (Partial Evaluation):
%==============================================================================

%------------------------------------------------------------------------------
% part_eval:
%------------------------------------------------------------------------------

% This predicate executes derivation steps as long as possible.
% Each derivation step adds new facts to cond/2.
% This is the standard bottom-up fixpoint computation.

part_eval :-
	derivation_step,
	!,
	part_eval.

part_eval.

%------------------------------------------------------------------------------
% derivation_step:
%------------------------------------------------------------------------------

derivation_step :-
	derive(Fact, Conds),
	remove_true(Conds, Simplified_Conds),
	store_if_new(Fact, Simplified_Conds).

%------------------------------------------------------------------------------
% store_if_new(+Head, +Body):
%------------------------------------------------------------------------------

% This predicate stores a derived conditional fact and partially evaluated
% rule.
% It fails if the state of the computation is not changed,
% i.e. the conditional fact and the rule were already known.
% A rule is only constructed if the body is not true (or the head is an
% answer literal).

store_if_new(Head, []) :-
	cond(Head, true),
	!,
	fail.

store_if_new(Head, []) :-
	Head =.. [Functor|_],
	Functor \== answer,
	!,
	save_cond(Head, true).

store_if_new(Head, Body) :-
	parameters(Head, Body, Var_List),
	construct_encoding(Head, Var_List, Head_Encoding),
	\+ prog(Head_Encoding, Body),
	save_prog(Head_Encoding, Body).

%------------------------------------------------------------------------------
% construct_encoding(+Fact, +Params, -Encoding):
%------------------------------------------------------------------------------

% This predicate checks whether there is already a conditional fact of the form
%	Fact <- pN(Var_List).
% If it is, it returns N.
% Otherwise it creates such a conditional fact with a new N.

construct_encoding(answer(Fact), _, Fact) :-
	use_option(derive_idb_literals, yes),
	make_gen_fact(Fact, Gen_Fact),
	cond(answer(Gen_Fact), Gen_Fact),
	!.

construct_encoding(answer(Fact), _, Fact) :-
	use_option(derive_idb_literals, yes),
	make_gen_fact(Fact, Gen_Fact),
	save_cond(answer(Gen_Fact), Gen_Fact),
	!.

construct_encoding(Fact, Var_List, params(N,Var_List)) :-
	cond(Fact, params(N,Var_List)),
	!.

construct_encoding(Fact, Var_List, params(N,Var_List)) :-
	next_pred_no(N),
	save_cond(Fact, params(N,Var_List)).

%------------------------------------------------------------------------------
% make_gen_fact(Fact, Gen_Fact):
%------------------------------------------------------------------------------

% This predicate replaces all arguments of the given fact by different
% variables. E.g. it replaces sg(var(0),var(0)) by sg(var(0),var(1)).
% It is used currently when derive_idb_literals is yes and we derive
% a fact of the form answer(p(...)).
% We want to use p then as encoding, but it is possible that we will derive
% later another fact of the form answer(p(...)) with different arguments.
% Since we want to use every predicate as an encoding only once,
% we immediately choose the most general arguments.
% I don't know whether this is a good solution, but for the same generation
% example, it produces a better output.

make_gen_fact(Fact, Gen_Fact) :-
	Fact =.. [Pred|Args],
	make_gen_args(Args, 0, Gen_Args),
	Gen_Fact =.. [Pred|Gen_Args].

%------------------------------------------------------------------------------
% make_gen_args(Args, First_Var_No, Gen_Args):
%------------------------------------------------------------------------------

% This produces a list of variables with unique numbers, starting with
% First_Var_No, which has the same length as the list Args.
% Actually, Args is only used for counting (only the list length is important,
% not the list itself).

make_gen_args([], _, []).

make_gen_args([_|Args], First_Var_No, [var(First_Var_No)|Gen_Args]) :-
	Next_Var_No is First_Var_No + 1,
	make_gen_args(Args, Next_Var_No, Gen_Args).

%------------------------------------------------------------------------------
% remove_true(+Body_In, -Body_Out):
%------------------------------------------------------------------------------

% This removes the atom "true" from a rule body.
% It also removes conditional facts which hold unconditionally.

remove_true([], []).

remove_true([true|Body_In], Body_Out) :-
	!,
	remove_true(Body_In, Body_Out).

remove_true([Lit|Body_In], [Lit|Body_Out]) :-
	remove_true(Body_In, Body_Out).

%------------------------------------------------------------------------------
% derive:
%------------------------------------------------------------------------------

derive(Norm_Fact, Norm_Conds) :-
	meta(Head, Body),
	max_var([Head|Body], Max_Var),
	empty_subst(Empty),
	find_match(Body, Empty, Max_Var, Unifier, Conds),
	apply_subst_term(Head, Unifier, Derived_Fact),
	apply_subst_list(Conds, Unifier, Derived_Conds),
	normalize(cond(Derived_Fact,Derived_Conds),
		cond(Norm_Fact,Norm_Conds)).

%------------------------------------------------------------------------------
% find_match(+Body, +Subst_In, +Var_Offset, -Subst_Out, -Conds):
%------------------------------------------------------------------------------

find_match([], Subst_In, _, Subst_In, []).

find_match([sys_eval(Call)|Body], Subst_In, Var_Offset, Subst_Out, Conds) :-
	!,
	apply_subst_term(Call, Subst_In, Real_Call),
	sys_eval(Real_Call, Subst_In, Subst),
	find_match(Body, Subst, Var_Offset, Subst_Out, Conds).

find_match([Atom|Body], Subst_In, Var_Offset, Subst_Out, [Fresh_Cond|Conds]) :-
	cond(Head, Cond),
	fresh_var(cond(Head,Cond), Var_Offset, cond(Fresh_Head,Fresh_Cond),
		Next_Offset),
	unify(Atom, Fresh_Head, Subst_In, Subst),
	find_match(Body, Subst, Next_Offset, Subst_Out, Conds).

%------------------------------------------------------------------------------
% sys_eval(+Call, +Subst_In, -Subst_Out):
%------------------------------------------------------------------------------

sys_eval(append(List1, List2, var(X)), Subst_In, Subst_Out) :-
	list_append(List1, List2, Result),
	subst_add(Subst_In, var(X), Result, Subst_Out),
	!.

sys_eval(Call, Subst, Subst) :-
	nl,
	write('*** SYS_EVAL NOT IMPLEMENTED FOR: '),
	write(Call),
	nl,
	fail.

%------------------------------------------------------------------------------
% next_pred_no(-N):
%------------------------------------------------------------------------------

% This generates a number for the next parameter predicate.
% If there are no parameter predicates in cond/2, it returns 0.
% Otherwise, it returns the largest number occurring plus 1.

next_pred_no(0) :-
	\+ pred_no(_),
	!.

next_pred_no(N_Plus_One) :-
	pred_no(N),
	\+ not_max_pred_no(N),
	N_Plus_One is N + 1.

%------------------------------------------------------------------------------
% pred_no(-N):
%------------------------------------------------------------------------------

% This predicate returns all numbers for the parameter predicates in the
% current set of conditional facts.

pred_no(N) :-
	cond(_,params(N,_)).

%------------------------------------------------------------------------------
% not_max_pred_no(+N):
%------------------------------------------------------------------------------

% This predicate is successful if there is a predicate number which is larger
% than N.

not_max_pred_no(N) :-
	pred_no(M),
	M > N.

%==============================================================================
% Determine Parameters:
%==============================================================================

% Parameters are variables which appear in both, head and body of a conditional
% fact.

%------------------------------------------------------------------------------
% parameters(+Fact, +Conds, -Var_List):
%------------------------------------------------------------------------------

parameters(Fact, Conds, Var_List) :-
	collect_vars(Fact, Vars1),
	collect_vars(Conds, Vars2),
	intersect_vars(Vars1, Vars2, Var_List).

%------------------------------------------------------------------------------
% collect_vars(+Term, -Var_List):
%------------------------------------------------------------------------------

% This predicate builds a list of all variables var(i) which appear in a term.

collect_vars(Term, Var_List) :-
	collect_vars(Term, [], Var_List).

%------------------------------------------------------------------------------
% collect_vars(+Term, +Vars_In, -Vars_Out):
%------------------------------------------------------------------------------


collect_vars(var(X), Vars_In, Vars_Out) :-
	!,
	add_var(Vars_In, var(X), Vars_Out).

collect_vars(Const, Vars, Vars) :-
	atomic(Const),
	!.

collect_vars(Term, Vars_In, Vars_Out) :-
	Term =.. [_|Args],
	collect_vars_list(Args, Vars_In, Vars_Out).

%------------------------------------------------------------------------------
% collect_vars_list(+Vars, -Var_List):
%------------------------------------------------------------------------------

collect_vars_list([], Vars, Vars).

collect_vars_list([Term|List], Vars_In, Vars_Out) :-
	collect_vars(Term, Vars_In, Vars),
	collect_vars_list(List, Vars, Vars_Out).

%------------------------------------------------------------------------------
% add_var(+Vars_In, +Var, -Vars_Out):
%------------------------------------------------------------------------------

add_var([], Var, [Var]).

add_var([Var|Rest], Var, [Var|Rest]) :-
	!.

add_var([Other_Var|Rest_In], Var, [Other_Var|Rest_Out]) :-
	add_var(Rest_In, Var, Rest_Out).

%------------------------------------------------------------------------------
% intersect_vars(+Vars1, +Vars2, -Vars_Out):
%------------------------------------------------------------------------------

intersect_vars([], _, []).

intersect_vars([X|Vars1], Vars2, [X|Vars_Out]) :-
	list_member(X, Vars2),
	!,
	intersect_vars(Vars1, Vars2, Vars_Out).

intersect_vars([_|Vars1], Vars2, Vars_Out) :-
	intersect_vars(Vars1, Vars2, Vars_Out).

%==============================================================================
% Optimizer for Removing Copy Rules:
%==============================================================================

% Partial evaluation produces quite often rules like
%	p2(X0) :- p1(X0).
% If this is the only rule about p2, we might as well replace p2 everywhere
% in the body by p1 and delete this rule.

%------------------------------------------------------------------------------
% optimize:
%------------------------------------------------------------------------------

% This predicate copies all rules from prog to opt_prog except that
% (1) copy rules are deleted (i.e. ignored),
% (2) predicates defined by copy rules are replaced in the body by the original
%     predicate.

optimize :-
	prog(Head, Body),
	\+ copy_rule(Head, Body),
	subst_copy_preds(Body, New_Body),
	save_opt_prog(Head, New_Body),
	fail.

optimize.

%------------------------------------------------------------------------------
% copy_rule(-Head, -Body):
%------------------------------------------------------------------------------

% This predicate returns copy rules which have the form
%	pN(X1,...,Xn) :- pM(X1,...,Xn),
% which are the only rule about pN,
% and where pN is not the answer predicate.

copy_rule(params(N,Args), Body) :-
	candidate_rule(params(N,Args), Body),
	\+ two_rules_about(N),
	\+ cond(answer(_), params(N,_)).

%------------------------------------------------------------------------------
% candidate_rule(-Head, -Body):
%------------------------------------------------------------------------------

% This predicate returns rules of the form p2(X0) :- p1(X0).
% I.e. there is only one body literal, and the argument lists of the predicate
% in head and body are identical, and consist only of variables, and no
% variable occurs more than once.

candidate_rule(params(Head_Pred,Args), [params(Body_Pred,Args)]) :-
	prog(params(Head_Pred,Args), [params(Body_Pred,Args)]),
	check_args(Args).

%------------------------------------------------------------------------------
% check_args(+Args):
%------------------------------------------------------------------------------

check_args([]).

check_args([var(X)|Rest]) :-
	\+ list_member(var(X), Rest),
	check_args(Rest).

%------------------------------------------------------------------------------
% two_rules_about(-Pred_No):
%------------------------------------------------------------------------------

two_rules_about(Pred_No) :-
	prog(params(Pred_No,Args1), Body1),
	prog(params(Pred_No,Args2), Body2),
	pair(Args1,Body1) \== pair(Args2,Body2).

%------------------------------------------------------------------------------
% replace_by(+Pred_No_In, -Pred_No_Out):
%------------------------------------------------------------------------------

replace_by(Pred_No_In, Pred_No_Out) :-
	copy_rule(params(Pred_No_In,_), [params(Pred_No_Out,_)]).

%------------------------------------------------------------------------------
% replace_final(+Pred_No_In, -Pred_No_Out):
%------------------------------------------------------------------------------

% This predicate follows chain of replacements.
% It also succeeds if there is no replacement: In this case it returns the
% input predicate.
% It fails if there are replacement loops:
%	p1(X) :- p2(X).
%	p2(X) :- p1(X).
% If there are no other rules about p1 and p2, both are considered as copy
% rules.
% Obviously, both are false, so it is correct that we also eliminate rules
% having these predicates in body literals.

replace_final(Pred_In, Pred_Out) :-
	replace_final(Pred_In, Pred_Out, []).

replace_final(Pred, Pred, _) :-
	\+ replace_by(Pred, _).

replace_final(Pred_In, Pred_Out, Visited_Preds) :-
	replace_by(Pred_In, Pred),
	\+ member(Pred, Visited_Preds),
	replace_final(Pred, Pred_Out, [Pred|Visited_Preds]).

%------------------------------------------------------------------------------
% subst_copy_preds(+Body_In, -Body_Out):
%------------------------------------------------------------------------------

subst_copy_preds([], []).

subst_copy_preds([params(N,Args)|Rest_In], [params(M,Args)|Rest_Out]) :-
	!,
	replace_final(N,M),
	subst_copy_preds(Rest_In, Rest_Out).

subst_copy_preds([Other_Lit|Rest_In], [Other_Lit|Rest_Out]) :-
	subst_copy_preds(Rest_In, Rest_Out).

