% Supported types:
% integer (int), float (float), atom (id), string (string)
% The types are the same as the corresponding Prolog types.

% start_rule(RuleNumber)
% Stores the numbers of rules 
% with which bottom-up evaluation can be started.
%
:- dynamic start_rule/1.

% cursor(Pred, RuleNumber, BodyLiteralNumber, BindingPattern, Types)
% Stores information about required cursors.
% Pred: The predicate for the cursor.
% RuleNumber: Rule number of the rule for the cursor.
% BodyLiteralNumber: Body literal number within the rule of the literal
% for which the cursor is created.
% BindingPattern: a list consisting of b and f, representing a binding
% pattern for calling the cursor.
% Types: Types of the columns of the cursor.
%
%%%%%% IMPROVEMENT %%%%%%
% TODO: If the cursor literal contains constants, these can be hard-coded into 
% the cursor and need not be transferred via a call. 
%
:- dynamic cursor/5.

% idb_pred_types(Predicate, Types)
% Stores type information for idb predicates.
% Predicate: the idb predicate name.
% Types: a list of types for the predicate arguments.
%
:- dynamic idb_pred_types/2.

% variable(RuleNumber, VariableNumber, Type)
% Stores information about variables.
% RuleNumber: The rule number for the variable.
% VariableNumber: a number/identifier that identifies the variable within the
% rule.
% Type: The type of the variable.
%
:- dynamic variable/3.

% application_edge(input_fact([InputFact], [ModifiedInputFact], InputEquations, InputAssignments),
% EdgeNumber, 
%	app_rule(RuleNumber, LitNumber, Line), NewRuleHead, CursorCalls, 
%	Equations, Assignments)
%
% Stores an edge of the rule application graph with information for code
% generation.
% InputFact: Input fact for the rule as it is generated by rule application.
% EdgeNumber: An identifying number for this edge. Helps to later associate
% jump labels to edges.
% It is stored as a list so that the empty list can be used for "no input".
% ModifiedInputFact: In certain cases, e.g. when there are variable conflicts,
% the input fact needs to be modified before it can be used with a rule.
% This argument stores the modified fact.
% InputEquations: This is a list of equal/2 facts that store information about
% conditions that have to hold for runtime unification
% InputAssignments: A list of assign/2 facts that store the
% information how the modified fact can be obtained from the input fact.
% RuleNumber: The number of the rule with which the input fact is used.
% LitNumber: The number of the body literal that unifies with the input fact.
% Line: The line of the source program where the code for this rule started;
% for error messages.
% NewRuleHead: The head of the rule after it has been used with the input fact
% and the cursors
% CursorCalls: A list of facts 
% cursor_call(Pred, RuleNumber, BodyLitNumber, BindingPattern, CallArgs) where 
% RuleNumber is the same as before, BodyLitNumber is the number of the
% body literal for the cursor, BindingPattern is a list of b and f describing
% the binding pattern of the cursor; and CallArgs is a list of atomics 
% or facts v(No, Id, Type) that describe the arguments for calling the cursor.
% Equations: A list of facts equal/2 that describe conditions on the cursor
% arguments; cursor arguments have the form c(RuleNumber, LitNo, ArgNo, BindingPattern, Type) where
% RuleNumber is the same as before, LitNo is the literal number of the cursor
% literal, ArgNo is the argument number of the literal/the cursor column,
% and Type is the type of the argument/cursor column.
% Assignments: Similar in form to Equations, only with facts 
% assign/2. Stores information about assignments to the variables that are used
% in the rule head, which have the form v(No, Id, Type).
% 
:- dynamic application_edge/7.

% Identifying numbers for application edge facts. Used as counter.
:- dynamic application_edge_number/1.

% Stores the number of an application edge that leads to recursion.
:- dynamic recursive/1.

% Stores the name of a recursive predicate.
:- dynamic recursive_pred/1.

% Arg1: Prediate name
% Arg2: List of argument types
:- dynamic derivable_pred/2.

:- dynamic rule_application_db/2.
:- dynamic recursion_history_id/1.
:- dynamic recursion_history_entry/2.
:- dynamic recursion_history_edge/2.

%-------------------------------------------------------------------------------
% define_undefined
%
% Define every undefined body predicate as edb predicate with id argument 
% types
%-------------------------------------------------------------------------------

define_undefined :-
	
    findall(undefined(Pred, Arity), body_pred(Pred,Arity),Undefined),
    
    to_edb(Undefined).

to_edb([]).
    
to_edb([undefined(Pred,Arity)|Undefined]) :- 
	length(List, Arity),
    fill_type_list(List, id),
    save_edb(Pred, List),
    to_edb(Undefined).

fill_type_list([],_).    

fill_type_list([Type|Rest], Type) :-
    fill_type_list(Rest, Type).

%-------------------------------------------------------------------------------
% rule_variants
%
% For every rule, store variants so that every idb body literal is in a first 
% position (for efficient access).
% If there is no idb body literal, the first position becomes the empty list.
%-------------------------------------------------------------------------------

rule_variants :-
    findall((First,No, FirstNo, Body,Head,Line),transformed_rule(First,No, FirstNo, Body, Head,Line), RuleList),
    make_variants(RuleList).

    
% if the first body predicate is edb, check if the other predicates are also
% edb. Then, this is a starting rule. Remove this rule, and replace it with 
% a rule where First is empty, but Body contains all body literals.

make_variants([]).

make_variants([(First,No,FirstNo, Body,Head, Line)|RuleList]) :-
    %if
    (First=[] ->
        true;
        First = [Elem], functor(Elem,Pred,_),
        %if
        (edb_pred(Pred,_) ->
            retract(transformed_rule(First,No, FirstNo, Body,Head, Line)),
            
            %if
            (check_edb_body(Body) ->
                assertz(transformed_rule([],No, 0, Body,Head, Line))
                ;
                make_idb_variants(transformed_rule(First,No, FirstNo, Body,Head, Line))
            )
            ;
            %else : idb_pred(Pred,_)
            make_idb_variants(transformed_rule(First,No, FirstNo, Body, Head,Line))
        )
    ),!,
    make_variants(RuleList).
    
check_edb_body([]).
    
check_edb_body([First|Body]) :-
    functor(First,Func,_),
    edb_pred(Func,_),
    check_edb_body(Body).

% is always called with first argument not the empty list!    
make_idb_variants(transformed_rule([First],No, _FirstNo, [First|Body], Head,Line)) :-
    findall(transformed_rule([Elem], No, ElemNo2, [First|Body], Head,Line),(nth1(ElemNo, Body,Elem), functor(Elem,Func,_),idb_pred(Func,_), ElemNo2 is ElemNo+1),VariantList),
    store_rule_variants(VariantList).
    

store_rule_variants([]).

store_rule_variants([Rule|VariantList]) :-
    % at this point it is checked whether we have generated
    % an already existing rule, but this case should be very rare
    copy_term(Rule, Rule2),
    call(Rule2),
    Rule =@= Rule2,
    !,
    store_rule_variants(VariantList).
	
store_rule_variants([Rule|VariantList]) :-
    assertz(Rule),
    store_rule_variants(VariantList).
    

%-------------------------------------------------------------------------------
% abstract_bu_eval
%
% Abstract bottom-up evaluation. 
% Generates data for code generation.
%-------------------------------------------------------------------------------

abstract_bu_eval :-
	retractall(start_rule(_)),
	retractall(cursor(_,_,_,_,_)),
	retractall(idb_pred_types(_,_)),
	retractall(variable(_,_,_)),
	retractall(application_edge(_,_,_,_,_,_,_)),
	retractall(application_edge_number(_)),
	retractall(recursive(_)),
	retractall(recursive_pred(_)),
	retractall(derivable_pred(_,_)),
	retractall(rule_application_db(_,_)),
	retractall(recursion_history_id(_)),
	retractall(recursion_history_entry(_,_)),
	retractall(recursion_history_edge(_,_)),
	%retractall(rule_application_counter(_)),
	assertz(application_edge_number(1)),
	assertz(recursion_history_id(0)),
	%assertz(rule_application_counter(0)),
	collect_start_rules(StartRules),
	compute_app_start_rules(StartRules, AppStartRules),
	add_rule_applications(0, AppStartRules, Counter),
	rule_application_step(Counter)
	.
	
collect_start_rules(StartRules) :-
    findall(r([], No, 0, Body,Head,Line),transformed_rule([], No, 0, Body,Head,Line), StartRules).


compute_app_start_rules([], []).

compute_app_start_rules([r([], No, 0, Body,Head,Line)|Rules], [app_rule(input_fact([],[],[], _InAssignments), 0, [], No, 0, Body, Head, Line)|AppRules]) :-
	compute_app_start_rules(Rules, AppRules).
	
	
rule_application_step(0).
rule_application_step(Counter) :-      %[app_rule(InputFact, RecursionHistory, First, No, FirstNo, Body,Head,Line)|RuleList]
    integer(Counter), Counter>0,
    (Counter<50000 ->
    	true;
    	write('Error: too many rule application steps'),nl
    ),
    !,
    rule_application_db(Counter, app_rule(InputFact, RecursionHistoryID, First, No, FirstNo, Body,Head,Line)),
    nonvar(No), % Just testing if something went wrong at unification, avoid generating endless lists
    !,
    apply_rule(app_rule(InputFact, RecursionHistoryID, First, No, FirstNo, Body,Head,Line), AppResultList),
	(nonvar(AppResultList), AppResultList = [OldHead, CursorCalls, Equations, NewHead, Assignments]->
	    
	    store_results(app_rule(InputFact, First, No, FirstNo, Body,NewHead,Line), RecursionHistoryID, NewRecursionHistoryID, CursorCalls, Equations, Assignments),
		
		%OldHead: original rule head with unbound variables
		find_next_rules(OldHead, NewHead, NewRecursionHistoryID, NextRules)
		
		%buildNewRuleList(NextRules, RuleList, NewRuleList)
		%NewRuleList=RuleList
		
		
		;
		AppResultList = [],
		NextRules = []
		%NewRuleList=RuleList
	),
	retractall(rule_application_db(Counter,_)),
	Counter2 is Counter -1,
	add_rule_applications(Counter2, NextRules, CounterNew),
    %(Counter2 == CounterNew ->
    %    CounterNext is Counter2-1
    %    ;
    %    CounterNext = CounterNew
    %),
    %write(NextRules),nl,
	rule_application_step(CounterNew).
	
rule_application_step(Counter) :-
    Counter >= 500000, write('Too many rule applications.'),fail.
	
apply_rule(app_rule(input_fact(_InFact, ModifiedInFact, _InEquations, InAssignments), _RecursionHistory, First, No, FirstNo, Body,Head,_Line), AppResultList) :-
    %bu_method(push),!,
	% apply input fact, which is a list of a literal (possibly empty)
	copy_term(Head, OldHead),
    	First = ModifiedInFact,
    	%%% HIER HERLEITBARE PRÄDIKATE SUCHEN UND ÜBERGEBEN %%%
    	create_apply_cursors(No, First, FirstNo, Body, 1, CursorResultList),
    	(nonvar(CursorResultList), CursorResultList = [CursorCalls, Equations] ->
    	    Head =.. [HeadPred|HeadArgs],
    	    replace_head_args(HeadArgs, HeadArgs, No, 1, NewHeadArgs, HeadTypes, ModifiedInFact, InAssignments, Assignments),
	        !,
	        store_new_idb(HeadPred, HeadTypes),
	        store_head_vars(NewHeadArgs),
	        store_inAssign_vars(InAssignments),
	        NewHead =.. [HeadPred|NewHeadArgs],
	        AppResultList =[OldHead, CursorCalls, Equations, NewHead, Assignments]
    	;
    	    (CursorResultList == [] ->
    	    
	        AppResultList = []
	    ;
	    	writ('Error at a rule application step'), nl,
	    	fail
	    )
	)
	.
    
create_apply_cursors(_,_,_,[],_, [[], []]).
        
create_apply_cursors(No, First, FirstNo, [Lit|Body], BodyLitCount, CursorResultListOut) :-
    %nl,write('entering '), write(create_apply_cursors(No, First, FirstNo, [Lit|Body], BodyLitCount, CursorResultList)),nl,
	%bu_method(push),!,
	% First always contains IDB literal, if not empty (((First =..[PredFirst|ArgsFirst],length(ArgsFirst,LFirst),length(TypesFirst,LFirst),edb_pred(PredFirst,TypesFirst));FirstNo \= BodyLitCount) ->
    (FirstNo \= BodyLitCount ->
    	Lit =.. [Pred | Args],
        length(Args, N),
        length(Types,N),
        
        ((edb_pred(Pred,Types); idb_pred_types(Pred, Types); derivable_pred(Pred, Types)) ->
            %%% HIER TEST EINFÜGEN %%%
            
            %nl,write('call '), write(create_cursor_args(No,BodyLitCount, 1, Args, Types, BindingPattern, BindingPattern, CallArgs, Eq)),nl,
            create_cursor_args(No,BodyLitCount, 1, Args, Types, BindingPattern, BindingPattern, CallArgs, Eq),
            %write('after '), write(create_cursor_args(No,BodyLitCount, 1, Args, Types, BindingPattern, BindingPattern, CallArgs, Eq)),nl,
            
            %EquationsOut = [Eq|Equations],
            
            store_cursor(cursor(Pred, No, BodyLitCount, BindingPattern, Types)),
            BLC is BodyLitCount+1,
            create_apply_cursors(No, First, FirstNo, Body, BLC, CursorResultList),
            (nonvar(CursorResultList), CursorResultList = [CursorCalls, Equations] ->
                CursorCallsOut = [cursor_call(Pred, No, BodyLitCount, BindingPattern, CallArgs)|CursorCalls],
                append(Eq, Equations, EquationsOut),
                CursorResultListOut = [CursorCallsOut, EquationsOut]
            ;
                CursorResultListOut = []
            )
        ;
            %write('Hi'),nl,
            CursorResultListOut = []
        )
        
    ;
	    
	    BLC is BodyLitCount+1,
        create_apply_cursors(No, First, FirstNo, Body, BLC, CursorResultList),
        (nonvar(CursorResultList), CursorResultList = [CursorCalls, Equations] ->
            CursorCallsOut = CursorCalls,
	        EquationsOut = Equations,
            CursorResultListOut = [CursorCallsOut, EquationsOut]
        ;
            CursorResultListOut = []
        )
    )
    %write('returning '), write(create_apply_cursors(No, First, FirstNo, [Lit|Body], BodyLitCount, CursorResultList)),nl
    .
    %append(Eq, Equations, EquationsOut).

create_cursor_args(_No,_BodyLitCount, _ArgCount, [], [], [], _, [], []).
	
create_cursor_args(No,BodyLitCount, ArgCount, [Arg|Args], [Type|Types], BindingPattern, FinalBindingPattern, CallArgsOut, EquationsOut) :-
    %if
	(var(Arg) ->
		B = f,
		Arg = c(No, BodyLitCount, ArgCount, FinalBindingPattern, Type),		
		EquationsOut = Equations,
		CallArgsOut = CallArgs
		;
		%if
		(Arg = v(_,_,VType) ->
		    %if
			(Type = VType ->
				B = b,
				EquationsOut = Equations,
				CallArgsOut= [Arg|CallArgs]
				;
				write('Error: Rule '),
				write(No),
				write('Body Literal '),
				write(BodyLitCount),
				write(' Argument '),
				write(ArgCount),
				write(': Type mismatch: Found '),
				write(VType),
				write(', required '),
				write(Type),nl,
				fail
			)
			;
			%if
			(Arg = c(_,_,_,_, CType) ->
			
				%if
				(CType = Type ->
					B = b, %this could also be f
					(Arg = c(No, BodyLitCount, _, _, _) ->
					    EquationsOut = [equal(Arg,c(No, BodyLitCount,ArgCount, FinalBindingPattern, Type))|Equations],
					    CallArgsOut = CallArgs
					    ;
					    EquationsOut = Equations,
					    CallArgsOut = [Arg|CallArgs]
					)
					
					;
					write('Error: Rule '),
					write(No),
					write('Body Literal '),
					write(BodyLitCount),
					write(' Argument '),
					write(ArgCount),
					write(': Type mismatch: Found '),
					write(CType),
					write(', required '),
					write(Type),nl,
					fail
				)
				;
				%if
				(atomic(Arg) ->
				
					B=b,
					
					CallArgsOut = [Arg|CallArgs],
					%if
					(integer(Arg), Type=int ->
						%EquationsOut = [equal(Arg,c(No, BodyLitCount,ArgCount,FinalBindingPattern, Type))|Equations]
						EquationsOut = Equations
						;
						(float(Arg), Type=float ->
							%EquationsOut = [equal(Arg,c(No, BodyLitCount,ArgCount,FinalBindingPattern, Type))|Equations]
							EquationsOut = Equations
							;
							%%% else
							%if
							(atom(Arg), Type=id ->
								%EquationsOut = [equal(Arg,c(No, BodyLitCount,ArgCount,FinalBindingPattern, Type))|Equations]
								EquationsOut = Equations
								;
								%if
								(string_codes(_,Arg),Type=string ->
									%EquationsOut = [equal(Arg,c(No, BodyLitCount,ArgCount,FinalBindingPattern, Type))|Equations]
									EquationsOut = Equations
									;
									write('Error: Rule '),
									write(No),
									write('Body Literal '),
									write(BodyLitCount),
									write(' Argument '),
									write(ArgCount),
									write(': Type mismatch: Found '),
									write(Arg),
									write(', required '),
									write(Type),nl,
									fail
								)
							)
						)
					)
					;
					write('Error: Rule '),
					write(No),
					write('Body Literal '),
					write(BodyLitCount),
					write(' Argument '),
					write(ArgCount),
					write(': No matching possible: '),
					write(Arg),nl,
					fail
				)
				
			)
		)		
	),
	ArgCount2 is ArgCount+1,
	BindingPattern = [B|BP],
	create_cursor_args(No,BodyLitCount, ArgCount2, Args, Types, BP, FinalBindingPattern, CallArgs, Equations)
	.

replace_head_args([],_,_,_,[], [],_, [],[]).
	
replace_head_args([Arg|HeadArgs], AllHeadArgs, No, ArgCounter, [NewArg|NewHeadArgs], [Type|HeadTypes], ModifiedInFact,InAssignmentsOut, EquationsOut) :-
    bu_method(push),!,
    transformed_rule(_,No,_,_,Head,_),
		functor(Head,Pred,_),
	%if
	(Arg = c(No,_LitNo,_LitArgNo, _BindingPattern, Type) ->
		(bu_method(old_push) ->
	        NewArg = v(Pred,ArgCounter,Type)
	    ;
	        NewArg = v(No,ArgCounter,Type)
		    
	    ),
		
		InAssignmentsOut = InAssignments,
		
		%EquationsOut = [assign(NewArg,Arg)|Equations]
		append(Equations, [assign(NewArg,Arg)], EquationsOut)
	;
		%if
		(Arg = v(ArgOne,Count,Type) -> %%% im else-Teil die Variable No irgendwie durch ArgOne ersetzen bzw. Fehlermeldungen verbessern
		    (\+bu_method(old_push),ArgOne==No,ModifiedInFact = [ModFact], ModFact =.. [_ModPred|ModArgs], member(Arg,ModArgs),integer(Count),nth1(Count,AllHeadArgs,c(No,_,_,_,_)) ->
		        atomic_concat(old,Count,Count2),
		        NewArg =.. [v,No,Count2,Type],
		        InAssignmentsOut = [assign(NewArg,Arg)|InAssignments],
		        EquationsOut = Equations
		        ;
		        (bu_method(old_push) ->
		            (ArgOne==Pred ->
	                    (Count==ArgCounter ->
	                    	NewArg = Arg,
		                    EquationsOut = Equations,
	                    	InAssignmentsOut = InAssignments
	                    ;
	                    	%atomic_concat(old,Count,Count2),
	                        %IntermediateArg =.. [v,Pred,Count2,Type],
	                        %InAssignmentsOut = [assign(IntermediateArg,Arg)|InAssignments],
	                        InAssignmentsOut = InAssignments,
	                        NewArg = v(Pred,ArgCounter,Type),
	                        %EquationsOut = [assign(NewArg,IntermediateArg)|Equations]
	                        EquationsOut = [assign(NewArg,Arg)|Equations]
	                    )
	                ;
	                    NewArg = v(Pred,ArgCounter,Type),
                    	EquationsOut = [assign(NewArg,Arg)|Equations],
                    	InAssignmentsOut = InAssignments
	                )
		            
		        ;    
		            NewArg = Arg,
			        EquationsOut = Equations,
		            InAssignmentsOut = InAssignments
		            
		        )
		    )
			
		;
			%if
			(atomic(Arg) ->
				NewArg=Arg,
				EquationsOut = Equations,
				InAssignmentsOut = InAssignments,
				%if
				(integer(Arg) ->
					Type = int
					;
					(float(Arg) ->
						Type = float
						;
						(atom(Arg) ->
							Type = id
							;
							(string_codes(Arg,_) ->
								Type = string;
								write('Error: Cannot match type for argument '),
								write(ArgCounter),
								write(' of head of rule.'),
								%write(No),
								nl,fail
							)
						)
					)
				)
				;
				write('Error: Invalid argument for head of rule.'),
				%write(No),
				nl,
				fail
			)
		)
	),
	ArgCounter2 is ArgCounter+1,
	replace_head_args(HeadArgs,AllHeadArgs,No,ArgCounter2,NewHeadArgs,HeadTypes,ModifiedInFact,InAssignments, Equations)
	.
	
% transformed_rule([], No, 0, Body,Head,Line)	
% app_rule(InputFact, First, No, FirstNo, Body,Head,Line)

%find_next_rules(NextFirst, NewHead, RecursionHistoryID, NextRulesOut) :-
%    
%	findall(r(NewHead, NextFirst, NewNo, NewFirstNo, NewBody, NextHead, RecursionHistoryID, NewLine), transformed_rule([NextFirst], NewNo, NewFirstNo, NewBody, NextHead, NewLine) , NextRules),
%	%write('NextRules '),write(NextRules),nl,
%	remove_existing_next_rules(NextRules, NextRulesOut)
%	%write('NextRulesOut '),write(NextRulesOut),nl
%	.
	
%find_next_rules(_OldHead, NewHead, RecursionHistoryID, NextRulesOut) :-
find_next_rules(OldHead, NewHead, RecursionHistoryID, NextRulesOut) :-
	findall(r(NewHead, NextFirst, NewNo, NewFirstNo, NewBody, NextHead, RecursionHistoryID, NewLine), (transformed_rule([NextFirst], NewNo, NewFirstNo, NewBody, NextHead, NewLine), unifiable(NextFirst, OldHead,_)) , NextRules),
	%write('NextRules '),write(NextRules),nl,
	
	remove_existing_next_rules(NextRules, NextRulesOut),
	NewHead =.. [NewHeadPred|_],
	idb_pred_types(NewHeadPred, NewHeadTypes),
	NewHeadPred2 =.. [NewHeadPred|NewHeadTypes],
	(\+ derivable_pred(NewHeadPred, NewHeadTypes) ->
	    assertz(derivable_pred(NewHeadPred, NewHeadTypes))
	;
	    true
	),
	find_derivable([NewHeadPred2], [])
	
	.
	
buildNewRuleList(NextRules, RuleList, NewRuleList) :-
	bu_method(push),!,
	append(NextRules, RuleList, NewRuleList).

%---------------------------------------------------------------
% remove_existing_next_rules/2
% 
% This predicate name is not good, the predicate does more than
% only removing existing rule applications from the rule list
%---------------------------------------------------------------
	
remove_existing_next_rules([],[]).

% app_rule(InputFact, First, No, FirstNo, Body,Head,Line)
% application_edge(InputFact, Nr, app_rule(No,FirstNo,Line), NewHead, CursorCalls, Equations, Assignments)
remove_existing_next_rules([r(NewHead, NextFirst, NewNo, NewFirstNo, NewBody, NextHead, RecursionHistoryID, NewLine)|NextRules], NextRulesOut) :-

		
	(application_edge(input_fact([NewHead],_, _Eq, _Ass),OldAppEdgeNr,app_rule(NewNo,NewFirstNo,NewLine),_,_,_,_) ->
		NextRulesOut = NR,
		(tag_recursive(OldAppEdgeNr, RecursionHistoryID) ->
		    true
		    ;
		    true
		)
		;
		NewHead =.. [NextFirstPred|NewHeadArgs],
		NextFirst =.. [NextFirstPred|NextFirstArgs],
		NextHead =..[_|NextHeadArgs],
		copy_term((NextFirstArgs, NextHeadArgs), (ModifiedArgs, CopyNextHeadArgs)),
		(
		apply_new_head(NewHeadArgs, NewNo, ModifiedArgs, Equations, Assignments, CopyNextHeadArgs) ->
			Modified =.. [NextFirstPred|ModifiedArgs],
			NextRulesOut = [app_rule(input_fact([NewHead], [Modified],Equations, Assignments), RecursionHistoryID, [NextFirst], NewNo, NewFirstNo, NewBody, NextHead, NewLine)|NR]
			;
			%apply_new_head should always succeed (?)
			%NextRulesOut = NR
			
			fail
		)
	),
	remove_existing_next_rules(NextRules,NR).

apply_new_head([],_,[], [], _,_).
	
apply_new_head([NewArg|NewHeadArgs], NextNo, [ModArg|ModifiedArgs], Equations, Assignments, NextHeadArgs) :-
	
		
	% Fall Arg=String auch behandeln! \+atomic(Arg), string_codes(Arg,_),Type=string
    (var(ModArg) ->
	    %(nonvar(NewArg),NewArg=v(NextNo,Count ,Type), mymember(ModArg,NextHeadArgs)->
	    %    (integer(Count) ->
	    %        atomic_concat(old,Count,Count2),
		%        ModArg = v(NextNo,Count2,Type),
		%        
		%        %Variable speichern
		%        store_head_vars([v(NextNo,Count2,Type)]),
		%        Assignments = [assign(v(NextNo,Count2,Type),NewArg)|Assignments2],
		%        Equations = Equations2
		%        ;
		%        write('Error: Danger of infinite variable creation:'),nl,
		%        write('Rule '), write(NextNo), write('Variable '), write(v(NextNo,Count ,Type)),
		%        nl, write('Trying to make it even older.'),!,
		%        fail		        
		%    )
		%    ;
	    %    ModArg=NewArg,
	    %    Equations = Equations2,
	    %    Assignments = Assignments2
	        
	        ModArg=NewArg,
	        Equations = Equations2,
	        Assignments = Assignments2
	    
	    ;
	    (atomic(ModArg) ->
	    
	        (nonvar(NewArg),NewArg=v(_,_,Type) ->
		        %Typen muessen uebereinstimmen!
		        ((integer(ModArg), Type=int;float(ModArg),Type=float;atom(ModArg),Type=id) -> %Fall String auch behandeln!\+atomic(ModArg), string_codes(ModArg,_),Type=string
				    Equations = [equal(NewArg,ModArg)|Equations2],
				    Assignments = Assignments2
				;
					write('Error: Type mismatch in rule '), nl,
					transformed_rule(_, NextNo, _, RuleBody, RuleHead,_), write(RuleHead), write(' :- '), write(RuleBody),nl,fail
				)
		        %
		        ;
		        NewArg=ModArg,
		        Equations = Equations2,
		        Assignments = Assignments2
	        )
	        ;
	        
	        (nonvar(ModArg),ModArg = v(_,_,Type) ->
                ((NewArg=v(_,_,Type);integer(NewArg), Type=int;float(NewArg),Type=float;atom(NewArg),Type=id) ->
		            Equations = [equal(NewArg,ModArg)|Equations2],
		            Assignments = Assignments2
		        ;
		        	write('Error: Type mismatch in rule '), write(NextNo),nl,fail
		        )
		            
                ;
                string_codes(ModArg,_) ->
                (nonvar(NewArg),NewArg=v(_,_,Type) ->
                    Type=string,
                    Equations = [equal(NewArg,ModArg)|Equations2],
	                Assignments = Assignments2
                    ;
                    NewArg=ModArg,
	                Equations = Equations2,
	                Assignments = Assignments2
                )
                ;
                write('Error in rule '), write(NextNo), nl, fail
            )
	    )
	),!,
	apply_new_head(NewHeadArgs, NextNo, ModifiedArgs, Equations2, Assignments2, NextHeadArgs).

derivable_body([]).

derivable_body([Lit|Body]) :-
    Lit =.. [Pred|Args],
    (edb_pred(Pred, Args); idb_pred_types(Pred, Args); derivable_pred(Pred, Args)),
    derivable_body(Body).

derive_derivable_ruleList([], []).

derive_derivable_ruleList([der_rule(NextHead, NextBody)|DerivedList], DerivedPreds) :-
    (derivable_body(NextBody) ->
        DerivedPreds = [NextHead|DerivedPreds2]
    ;
        DerivedPreds = DerivedPreds2
    ),
    derive_derivable_ruleList(DerivedList, DerivedPreds2).

find_derivable([], DerivedPreds) :-
	!,
    store_derivable(DerivedPreds, NewPreds),
    (NewPreds \= [] -> 
        find_derivable(NewPreds, [])
    ;
        true
    )
    .

find_derivable([PredIn|PredList], DerivedPredsIn) :-
	copy_term(PredIn, Pred),
	%Pred =.. [PredName|_],
	%idb_pred_types(PredName, ArgTypes),
	%Pred2 =.. [PredName|ArgTypes],
	findall(der_rule(NextHead, NextBody), transformed_rule([Pred], _NextNo, _NextFirstNo, NextBody, NextHead, _NewLine), DerivedList),
	derive_derivable_ruleList(DerivedList, DerivedPreds),
	
	append(DerivedPredsIn, DerivedPreds, DerivedPreds2),
	find_derivable(PredList, DerivedPreds2).
	
store_derivable([], []).

store_derivable([Pred| PredList], NewPreds) :-
    Pred =.. [PredName|ArgTypes],
	(\+derivable_pred(PredName,_) ->
		assertz(derivable_pred(PredName, ArgTypes)),
		NewPreds = [Pred|NewPreds2]
	;
		(derivable_pred(PredName,ArgTypes2), ArgTypes \= ArgTypes2 ->
			write('Error: Type clash for IDB predicate '),
			write(PredName), 
			write(': '),nl,
			write('Types present: '),
			write(ArgTypes2),
			write(', Types to store: '),
			write(ArgTypes),
			nl,
			fail
		;
			NewPreds = NewPreds2
		)
	),
	store_derivable(PredList, NewPreds2).

store_start_rules([]).
	
store_start_rules([app_rule(_InputFact, [], No, 0, _Body,_Head,_Line)|Rules]) :-
	bu_method(push),!,
	assertz(start_rule(No)),
	store_start_rules(Rules)
	.
	
store_cursor(cursor(Pred, No, BodyLitCount, BindingPattern, Types)) :-
	    
	%if
	cursor(Pred, No, BodyLitCount, BindingPattern, Types2) ->
		%if
		(Types = Types2 ->
			true;
			write('Error in rule '),
			write(No),
			write(': Cursor '),
			write(cursor(Pred, No, BodyLitCount, BindingPattern)),
			write(' already exists with types '),
			write(Types2),
			nl,
			fail
		)
		;
		assertz(cursor(Pred, No, BodyLitCount, BindingPattern, Types)).
		
store_new_idb(Pred, Types) :-
	idb_pred_types(Pred,Types), !.
	
store_new_idb(Pred, Types) :-
	\+idb_pred_types(Pred,_) ->
		assertz(idb_pred_types(Pred,Types))
		;
		(idb_pred_types(Pred,Types) ->
			true
			;
			write('Error: idb predicate '),
			write(Pred),
			write(' already exists with types '),
			write(Types),
			nl,
			fail
		).
	
store_head_vars([]).
	
store_head_vars([Var|NewHeadArgs]) :-
	(Var=v(ArgOne,No,Type) ->
		(
		variable(ArgOne,No,Type) ->
			true
			;
			\+variable(ArgOne,No,_) -> 
				assertz(variable(ArgOne,No,Type))
				;
				write('Error: variable '),
				write(variable(ArgOne,No,Type)),
				write(' already exists.'),nl,
				fail
				
		)
		;
		true
	),
	store_head_vars(NewHeadArgs).
	
store_inAssign_vars([]).	

store_inAssign_vars([assign(Var1, _)|InAssignments]) :-
    (Var1=v(ArgOne,No,Type) ->
        (
		variable(ArgOne,No,Type) ->
			true
			;
			\+variable(ArgOne,No,_) -> 
				assertz(variable(ArgOne,No,Type))
				;
				write('Error: variable '),
				write(variable(ArgOne,No,Type)),
				write(' already exists.'),nl,
				fail
				
		)
    ;
        write('Error: Left side of assignment is not a variable.'),nl
    ),
    store_inAssign_vars(InAssignments).
	
%(member(No, RecursionHistory), \+ recursive(No) ->
		%    assertz(recursive(No))
		%    ;
		%    true
		%),	
%store_results(app_rule(InputFact, _First, No, FirstNo, _Body,NewHead,Line), RecursionHistory, [(AppEdgeNr,No)|RecursionHistory], CursorCalls, Equations, Assignments):-
store_results(app_rule(InputFact, _First, No, FirstNo, _Body,NewHead,Line), RecHistID1, NewRecursionHistoryID, CursorCalls, Equations, Assignments):-
    (application_edge(InputFact,OldEdgeNr, app_rule(No,FirstNo,Line), NewHead, CursorCalls, Equations, Assignments) ->
	    %AppEdgeNr = OldEdgeNr
	    recursion_history_id(RecursionHistoryID),
	    NewRecursionHistoryID is RecursionHistoryID +1,
	    retractall(recursion_history_id(_)),
	    assertz(recursion_history_id(NewRecursionHistoryID)),
	    assertz(recursion_history_entry(NewRecursionHistoryID,OldEdgeNr))
	    
	    ;
	    
	    application_edge_number(AppEdgeNr),
	    (AppEdgeNr >= 4000000 -> 
	        write('Too many application edges.'),fail
	        ;
	        assertz(application_edge(InputFact, AppEdgeNr, app_rule(No,FirstNo,Line), NewHead, CursorCalls, Equations, Assignments)),
	        retract(application_edge_number(AppEdgeNr)),
	        AppEdgeNr2 is AppEdgeNr+1,
	        
	        assertz(application_edge_number(AppEdgeNr2)),
	        (is_recursive(No, RecHistID1), \+recursive(AppEdgeNr) ->
	            
	            assertz(recursive(AppEdgeNr)),
	            functor(NewHead,HeadPred,_),
	            (\+ recursive_pred(HeadPred) -> assertz(recursive_pred(HeadPred));true)
	            ;
	            true
	        ),
	        recursion_history_id(RecursionHistoryID),
	        NewRecursionHistoryID is RecursionHistoryID +1,
	        retractall(recursion_history_id(_)),
	        assertz(recursion_history_id(NewRecursionHistoryID)),
	        assertz(recursion_history_entry(NewRecursionHistoryID,AppEdgeNr))
	    )
	    
	),
	assertz(recursion_history_edge(NewRecursionHistoryID, RecHistID1))
	.
	
add_rule_applications(CounterIn, [], CounterIn).

add_rule_applications(CounterOld, [Rule|RuleList], Counter2) :-
    
    add_rule_applications(CounterOld, RuleList, CounterNew),
    Counter2 is CounterNew + 1,
    assertz(rule_application_db(Counter2, Rule)).
  
% application_edge(InputFact,EdgeNr, app_rule(No,FirstNo,Line), NewHead, CursorCalls, Equations, Assignments)     
is_recursive(RuleNr, RecHistID) :- 
    recursion_history_entry(RecHistID,AppEdgeNr),
    application_edge(_,AppEdgeNr,app_rule(RuleNr,_,_),_,_,_,_),
    !.
       
is_recursive(RuleNr, RecHistID) :-
    recursion_history_entry(RecHistID,AppEdgeNr),
    application_edge(_,AppEdgeNr,app_rule(RuleNr2,_,_),_,_,_,_),
    RuleNr \= RuleNr2,
    recursion_history_edge(RecHistID, RecHistID2),
    is_recursive(RuleNr, RecHistID2).

%tag_recursive(AppEdgeNr, RecHistId) :- 
%    recursion_history_entry(RecHistId,AppEdgeNr),
%    (\+ recursive(AppEdgeNr) ->
%        assertz(recursive(AppEdgeNr)),
%        application_edge(_InputFact, AppEdgeNr, app_rule(_No,_FirstNo,_Line), NewHead, _CursorCalls, _Equations, _Assignments),
%        functor(NewHead,HeadPred,_),
%	    (\+ recursive_pred(HeadPred) -> assertz(recursive_pred(HeadPred));true)
%        ;
%        true
%    ),
%    !.
       
%tag_recursive(AppEdgeNr, RecursionHistoryIDIn) :-
%    recursion_history_entry(RecursionHistoryIDIn,AppEdgeNr2),
%    AppEdgeNr \= AppEdgeNr2,
%    recursion_history_edge(RecursionHistoryIDIn, RecHistIDNext),
%    tag_recursive(AppEdgeNr, RecHistIDNext)
%    
%    .
       
tag_recursive(AppEdgeNr, RecHistId) :- 
    recursion_history_entry(RecHistId,AppEdgeNr),
    (\+ recursive(AppEdgeNr) ->
        assertz(recursive(AppEdgeNr)),
        application_edge(_InputFact, AppEdgeNr, app_rule(_No,_FirstNo,_Line), NewHead, _CursorCalls, _Equations, _Assignments),
        functor(NewHead,HeadPred,_),
	    (\+ recursive_pred(HeadPred) -> assertz(recursive_pred(HeadPred));true)
        ;
        true
    ),
    !.
       
tag_recursive(AppEdgeNr, RecursionHistoryIDIn) :-
    recursion_history_entry(RecursionHistoryIDIn,AppEdgeNr2),
    AppEdgeNr \= AppEdgeNr2,
    recursion_history_edge(RecursionHistoryIDIn, RecHistIDNext),
    tag_recursive(AppEdgeNr, RecHistIDNext),
    (\+ recursive(AppEdgeNr2) ->
        assertz(recursive(AppEdgeNr2)),
        application_edge(_InputFact, AppEdgeNr2, app_rule(_No,_FirstNo,_Line), NewHead, _CursorCalls, _Equations, _Assignments),
        functor(NewHead,HeadPred,_),
	    (\+ recursive_pred(HeadPred) -> assertz(recursive_pred(HeadPred));true)
        ;
        true
    )
    .


    

