% remove the alternative
/*
1. include depthbound
2. another case for deductively proving
3. 
*/


ggg:- generalise.

generalise:-
	findall(EI,ex(EI,Ex,1),PosEIs),%write(EIs),nl,
	findall(EI,ex(EI,Ex,0),NegEIs),
	generalise(PosEIs,NegEIs,H),
	nl,write(H),nl,print_list(H).


generalise(PosEIs0,NegEIs0,FinalH):- 
	reorder_examples(PosEIs0,PosEIs,NegEIs0,NegEIs),
	write('Learning Order: '),write(PosEIs),write(NegEIs),
	generalise0(PosEIs,[],FinalH,[],NewNTs),
	prune_by_negEx(NegEIs,FinalH).




% depth limit is put into part of the program -- the depth bound on member will be jungled 
generalise0([],Tr,Tr,NumNT,NumNT).
generalise0([EI|EIs],TrSofar,Tr,NumNTSofar,NumNT):-
	accessarySeed([TrSofar,NewTrSofar,NumNTSofar,NewNumNTSofar0],EI,ArgumentedEx),	
	ArgumentedEx,addTemplate(NewNumNTSofar0,NewNumNTSofar),
	generalise0(EIs,NewTrSofar,Tr,NewNumNTSofar,NumNT).


prune_by_negEx([],FinalH).
prune_by_negEx([NegEI|NegEIs],FinalH):-
	accessaryDeductiveEx(FinalH,NegEI,ArgumentedEx),
	not(ArgumentedEx),
	prune_by_negEx(NegEIs,FinalH).



addTemplate(NewNumNTSofar0,[X|NewNumNTSofar0]).
addTemplate(NewNumNTSofar0,[X,Y|NewNumNTSofar0]).
addTemplate(NewNumNTSofar0,[X,Y,Z|NewNumNTSofar0]).