%------------------------------------------------------------------------------
% This holds a new, unused rule identifyer number to be assigned to parsed
% rules.
%------------------------------------------------------------------------------

:- dynamic rule_no/1.


%------------------------------------------------------------------------------
% List of Query Patterns: (Stefan Brass)
%------------------------------------------------------------------------------

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

%------------------------------------------------------------------------------
% sldmagic_rule(Head, Body)
%------------------------------------------------------------------------------
% The rules of the program, furnished with calls in the rule body, as input
% for the sldmagic transformation. Head is the rule head, Body the list of
% body literals, possibly as argument of a call predicate.
%------------------------------------------------------------------------------

%:- dynamic sldmagic_rule/2.

%------------------------------------------------------------------------------
% numbered_rule(Head, Body)
%------------------------------------------------------------------------------
% Intermediate rules for a query-oriented, tail-recursion-optimizing 
% program transformation. 
% First argument is the rule head,
% second argument is a list of the body literals,
% third argument is a unique number.
%------------------------------------------------------------------------------
:- dynamic numbered_rule/3.

:- dynamic num/1.

%------------------------------------------------------------------------------
% intermediate_rule(Head, Body)
%------------------------------------------------------------------------------
% Intermediate rules for a query-oriented, tail-recursion-optimizing 
% program transformation. 
% First argument is a unique number,
% second argument is the rule head,
% third argument is a list of the body literals,
% the fourth argument is a number of the program rule used in the body, or
% sometimes [].
%------------------------------------------------------------------------------
:- dynamic intermediate_rule/4.

:- dynamic intermediate_no/1.

%------------------------------------------------------------------------------
% This holds the transformed rules.
% The first argument is the list containing the first body literal, empty if the
% body is empty.
% The second argument is a unique rule number.
% The third argument gives the position of the literal of the first argument
% in the body; this will be relevant later for variants of the rule where
% other (idb) body literals are stored in the first argument (for bottom-up
% evaluation).
% The fourth argument is a list of all the body literals.
% The fifth argument is the rule head.
% The sixth argument is the line in the input program where this rule begins
% (for error messages). Now I realized that this is superfluous, since
% a program transformation might destroy the original program structure. Code
% should not use this argument.
%------------------------------------------------------------------------------

:- dynamic transformed_rule/6.

:- dynamic pred_prefix/1.

clear :-
    retractall(rule_no(_)),
	retractall(transformed_rule(_,_,_,_,_,_)),
	retractall(query(_,_,_,_)),
	retractall(sldmagic_rule(_,_)),
	retractall(intermediate_rule(_,_,_,_)),
	retractall(intermediate_no(_)),
	retractall(numbered_rule(_,_,_)),
	retractall(num(_)),
	retractall(pred_prefix(_)).

%------------------------------------------------------------------------------
% transform(+TransformationType)
%------------------------------------------------------------------------------
% In its standard form (TransformationType = standard), 
%transform simply changes the format of the input rules
% and adds rule numbers. This predicate could also be used to transform the
% input rules with sldmagic or magic sets transformation.
%------------------------------------------------------------------------------
transform(standard) :-
	clear,
	assertz(rule_no(1)),
	findall(rule(Head,Body,Line),rule(Head,Body,Line),RuleList),
	transform_rules(standard, RuleList).

%------------------------------------------------------------------------------
% transform(+TransformationType)
%------------------------------------------------------------------------------
% With TransformationType = query_oriented, 
% transform does a very simple and naive (but fast) query-oriented rule transformation. 
% All predicates that cannot be reached from the query, ignoring bound arguments,
% are discarded.
%------------------------------------------------------------------------------		
transform(query_oriented) :-
	clear,
	assertz(rule_no(1)),
	findall(rule(Head,Body,Line),(answer_pred(AnswerPred), idb_pred(AnswerPred, Arity), functor(Head,AnswerPred,Arity), rule(Head,Body,Line)),RuleList),
	(RuleList == [] ->
	    write('Error: No rules defining answer predicate found.'),nl, fail
	;
	    transform_rules(query_oriented, RuleList)
	)
	.	

%------------------------------------------------------------------------------
% transform(+TransformationType)
%------------------------------------------------------------------------------
% With TransformationType = sldmagic, 
% transform does a rule transformation with the SLDMagic method.
%------------------------------------------------------------------------------	
transform(sldmagic) :-
    clear,
	assertz(rule_no(1)),
	(answer_pred(AnswerPred) -> 
	    idb_pred(AnswerPred,AnswerArity),
	    functor(Query, AnswerPred, AnswerArity),
	    numbervars(Query, 0,_, [functor_name(var)]),
	    assertz(query(Query, Query, [], [])),
	    findall(rule(Head,Body,Line),rule(Head,Body,Line),RuleList),
	    (RuleList == [] ->
	        write('Warning: No rules defining answer predicate found.'),nl
	    ;
	        true
	    ),
	    transform_rules(sldmagic, RuleList),
	    sldmagic,
	    % and transform the output rules to transformed_rule facts
	    findall(opt_rule(Head,Body,0),opt_prog(Head,Body),RuleList1),
	    translate_opt_rules(RuleList1,RuleList2),
	    	transform_rules(standard, RuleList2)
	;
	    write('Error: No answer predicate defined.'), nl, fail
	)
    .
    
%------------------------------------------------------------------------------
% transform(+TransformationType)
%------------------------------------------------------------------------------
% With TransformationType = qotr, 
% transform does a query oriented and tail-recursion optimizing rule
% transformation. This is still experimental.
%------------------------------------------------------------------------------
transform(qotr) :-
	clear,
	assertz(rule_no(1)),
	assertz(intermediate_no(1)),
	findall(rule(Head,Body),rule(Head,Body,_), NumberList),
	
	number_rules(1,NumberList),!,
	compute_pred_prefix('p_'),!,
	findall(rule(Head,Body, Number),(answer_pred(AnswerPred), idb_pred(AnswerPred, Arity), functor(Head,AnswerPred,Arity), numbered_rule(Head,Body,Number)),RuleList),
	(RuleList == [] ->
	    write('Error: No rules defining answer predicate found.'),nl, fail
	;
		store_intermediate_rules(1,RuleList),
	    transform_rules_qotr(1),!
	),!
	.
	
transform_rules(standard, []).
	
transform_rules(standard, [rule(Head,Body,Line)|RuleList]) :-
	rule_no(No),
	
	(Body = [First|_] ->
		assertz(transformed_rule([First], No, 1, Body, Head, Line))
		;
		assertz(transformed_rule([], No, 0, Body, Head, Line))
	),!,
	No2 is No+1,
	retract(rule_no(No)),
	assertz(rule_no(No2)),
	transform_rules(standard,RuleList).
	
transform_rules(query_oriented, []).

transform_rules(query_oriented, [rule(Head,Body,Line)|RuleList]) :-
    (%\+transformed_rule(_,_,_,Body, Head, Line) -> % Dieser Test auf Existenz ist nicht ausreichend, siehe Parser
    copy_term((Head, Body), (NewHead, NewBody)),
	transformed_rule(_,_,_,NewBody,NewHead, Line),
	(Head, Body) =@= (NewHead, NewBody) ->	% rule already exists
        RuleListOut = RuleList
    ;
        rule_no(No),
	
	    (Body = [First|_] ->
		    assertz(transformed_rule([First], No, 1, Body, Head, Line))
		    ;
		    assertz(transformed_rule([], No, 0, Body, Head, Line))
	    ),!,
	    No2 is No+1,
	    retract(rule_no(No)),
	    assertz(rule_no(No2)),
	    find_called_rules(Body,CalledRules),
    	append(CalledRules,RuleList,RuleListOut)
    ),
    
    transform_rules(query_oriented,RuleListOut)
    .
    
transform_rules(sldmagic, []).

transform_rules(sldmagic, [rule(Head, Body, _)|RuleList]) :-
    add_calls(Body, Body2),
    numbervars(Body2,0,_,[functor_name(var)]),
    assertz(sldmagic_rule(Head, Body2)),
    transform_rules(sldmagic, RuleList).
    
transform_rules_qotr(Ino) :-
	\+intermediate_rule(Ino,_,_,_).
	
transform_rules_qotr(INo) :-
	intermediate_rule(INo,Head, Body, Number),
	append(PreBody, [Last], Body),
	functor(Last, Pred, Arity),
	%
	length(PreBody,PBL),
	(idb_pred(Pred, Arity), Number\=[]->
		pred_prefix(Prefix),
		%copy_term((Head, Body), (NewHead, NewBody)),
		%(intermediate_rule(_,NewHead, NewBody,Number2), 
		%	(Head, Body,Number) =@= (NewHead, NewBody, Number2) ->	% rule already exists
		%	Rules2 = Rules
		%;
			
			
			(%(PBL > 1;PreBody=[EDBLit],functor(EDBLit,EDBPred,_),edb_pred(EDBPred,_)) ->
			%(PBL > 1; PreBody=[Lit],functor(Lit,LitPred,_),\+atom_concat(Prefix,_,LitPred))->
			PBL > 1 ->	
				
				find_common_vars(PreBody,[Head,Last],CommonVars),
				
				length(CommonVars,CVL),
				Head =.. [HeadPred|HeadArgs],
				Last =.. [Pred|LastArgs],
				binding_pattern(HeadArgs, CommonVars, BPHead),
				binding_pattern(LastArgs, CommonVars, BPLast),
				atomic_list_concat(BPHead,BPH),
				atomic_list_concat(BPLast,BPL),
				atomic_list_concat([Prefix,HeadPred,'_',BPH,'__',Pred,'_',BPL,'_',CVL],GenHeadPred),
				%atomic_list_concat([Prefix,Pred,'_',BPL,'_',CVL],GenHeadPred),
				%atomic_list_concat([Prefix,Number,'_',CVL],GenHeadPred),
				!,
				%write(save_idb(GenHeadPred,CVL)),
				
				GenHead =.. [GenHeadPred|CommonVars],
				save_idb(GenHead,0),
				%find_resolution_rules(Last, RRules),
				make_new_rules(Head, [GenHead],Last, NewRules),
				
				%append([rule(GenHead, PreBody,[])|NewRules],Rules,Rules2)
				intermediate_no(IntNo),
				store_intermediate_rules(IntNo,[rule(GenHead, PreBody,[])|NewRules])
				%append(NewRules,Rules3,Rules2)
			;
			%(PreBody=[Lit],functor(Lit,LitPred,_),atom_concat(Prefix,_,LitPred) ->
			%	%find_called_numbered_rules(PreBody,CalledRules),
			%	%find_resolution_rules(Last, RRules),
			%	make_new_rules(Head, PreBody, Last, NewRules),
			%	%append(NewRules, CalledRules, Rules3),
			%	%append(Rules3, Rules, Rules2),
			%	intermediate_no(IntNo),
			%	store_intermediate_rules(IntNo,NewRules)
			%;
			
				%find_resolution_rules(Last, RRules),
				make_new_rules(Head, PreBody, Last, NewRules),
				intermediate_no(IntNo),
				store_intermediate_rules(IntNo,NewRules)
				%append(NewRules, Rules, Rules2)
			%)
			)
			
			
			
		%)
	;
		 copy_term((Head, Body), (NewHead, NewBody)),
		(transformed_rule(_,_,_,NewBody,NewHead, _), 
			(Head, Body) =@= (NewHead, NewBody) ->	% rule already exists
			true
		;
		
			rule_no(No),
		    (Body = [First|_] ->
			    assertz(transformed_rule([First], No, 1, Body, Head, 0))
			    ;
			    assertz(transformed_rule([], No, 0, Body, Head, 0))
		    ),!,
		    No2 is No+1,
		    retract(rule_no(No)),
		    assertz(rule_no(No2)),
			find_called_numbered_rules(Body,CalledRules),
			%append(CalledRules, Rules, Rules2)
			intermediate_no(IntNo),
			store_intermediate_rules(IntNo,CalledRules)
		)
		
	),
	INo2 is INo+1,
	transform_rules_qotr(INo2).

translate_opt_rules([],[]).
    
translate_opt_rules([opt_rule(Head,Body,Line)|OptRules],[rule(Head2,Body2,Line)|Rules]) :-
	translate_opt_rule_lits([Head|Body], [Head2|Body2],[]),
	
	translate_opt_rules(OptRules,Rules).

translate_opt_rule_lits([],[],_).
	
translate_opt_rule_lits([Lit|Lits],[LitOut|LitsOut],Vars) :-
	(Lit = params(N, Args) ->
		atom_concat(p,N,Pred2),
		translate_opt_rule_args(Args, Args2,Vars, Vars2)
	;
		Lit =.. [Pred|Args],
		Pred2 = Pred,
		translate_opt_rule_args(Args, Args2,Vars, Vars2)
	),
	LitOut =.. [Pred2|Args2],
	translate_opt_rule_lits(Lits, LitsOut, Vars2).
	
translate_opt_rule_args([],[],Vars,Vars).

translate_opt_rule_args([Arg|Args], [Arg2|ArgsOut], VarsIn, VarsOut) :-
	(Arg=var(X),\+member((var(X),_),VarsIn) ->
		VarsIn2 = [(var(X),Arg2)|VarsIn]
	;
		(Arg=var(X),member((var(X),Arg2),VarsIn) ->
			VarsIn2 = VarsIn
		;
			Arg=Arg2,
			VarsIn2 = VarsIn
		)
	),
	translate_opt_rule_args(Args, ArgsOut, VarsIn2, VarsOut).

binding_pattern([], _, []).

binding_pattern([Arg|Args], Vars, [P|Pat]) :-
	(mymember(Arg,Vars) ->
		P=b
	;
		P=f
	),
	binding_pattern(Args, Vars, Pat).

find_called_rules([],[]).
    
find_called_rules([Goal|GoalList], RuleListOut) :-
    findall(rule(Head,Body,Line),(rule(Head,Body,Line), unifiable(Goal,Head,_)),FoundRules),
    
    find_called_rules(GoalList, RuleList),
    append(FoundRules,RuleList,RuleListOut)
    .

%find_resolution_rules(Goal, FoundRules) :-
%    findall(rule(Goal,Body,Number),numbered_rule(Goal,Body,Number),FoundRules)
%    .

find_called_numbered_rules([],[]).

find_called_numbered_rules([Goal|GoalList], RuleListOut) :-
	%copy_term(Goal,NewGoal),
    findall(rule(NewGoal,Body,Number),(numbered_rule(NewGoal,Body,Number), unifiable(Goal, NewGoal,_)),FoundRules),
    %findall(rule(NewGoal,Body,Number),(numbered_rule(NewGoal,Body,Number)),FoundRules),
    find_called_numbered_rules(GoalList, RuleList),
    append(FoundRules,RuleList,RuleListOut)
    .

add_calls([],[]). 
   
add_calls([Lit|Body], [Lit2|Body2]) :-
    functor(Lit, Pred, _),
    ((edb_pred(Pred, _); Body == [])->
        Lit2 = Lit
    ;
        Lit2 = call(Lit)
    ),
    add_calls(Body, Body2).

number_rules(_,[]).

number_rules(N,[rule(Head,Body)|Rules]) :-
	assertz(numbered_rule(Head, Body, N)),
	N2 is N+1,
	number_rules(N2,Rules).
	

compute_pred_prefix(Pref) :-
	((edb_pred(Pred,_);idb_pred(Pred,_)),atom_concat(Pref,_,Pred) ->
		atom_concat(Pref,'_',Pref2),
		compute_pred_prefix(Pref2)
	;
		assertz(pred_prefix(Pref))
	).
	
mymember(X, List) :-
    nonvar(List),
    List = [Y|_],
    X == Y.
    
mymember(X, List) :- 
    nonvar(List),
    List = [Y|Rest],
    X \== Y,
    mymember(X, Rest)
    .
	
find_common_vars(LitList1, LitList2, CommonVars) :-
	term_variables(LitList1, Vars1),
	term_variables(LitList2, Vars2),
	common_members(Vars1, Vars2, CommonVars).
	
common_members([], _, []).

common_members([Var|Vars1], Vars2, CommonVarsOut) :-
	(mymember(Var, Vars2) ->
		CommonVarsOut = [Var|CommonVars]
	;
		CommonVarsOut = CommonVars
	),
	common_members(Vars1, Vars2, CommonVars).

%make_new_rules(_,_,_,[],[]).
	
make_new_rules(Head, NewHead,Last,NewRules) :-
%rule(RuleHead,CalledBody,Number),
%rule(CopyHead,NewBody,Number)
	
	findall(rule(CopyHead,NewBody,Number),(copy_term((Head,NewHead,Last), (CopyHead,CopyNewHead,CopyLast)),numbered_rule(CopyLast,CalledBody,Number), append(CopyNewHead,CalledBody,NewBody)),NewRules).
	%make_new_rules(Head,NewHead, Last,CRules, NewRules).
	
store_intermediate_rules(IntNo, []) :-
	retractall(intermediate_no(_)),
	assertz(intermediate_no(IntNo)).
	
store_intermediate_rules(IntNo, [rule(Head, Body,Number)|Rules]) :-
	copy_term((Head, Body), (NewHead, NewBody)),
	(intermediate_rule(_,NewHead, NewBody,Number2), 
		(Head, Body,Number) =@= (NewHead, NewBody, Number2) ->	% rule already exists
		IntNo2 = IntNo
	;
		assertz(intermediate_rule(IntNo,Head, Body,Number)),
		IntNo2 is IntNo+1
	),
	store_intermediate_rules(IntNo2, Rules).