/*%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%	
% generate T for single seeded Example
%	1. get one example by index;
%	2. output a bunch of Ts
%	--only T(ID is useless after reconstruction)
%	--duplicate removed

WORK OR NOT:
Top Theory
DepthLimit (Peano number)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%*/


g(EI,K):-
	%tell('hypothesesGenTest.txt'),
	set(depthLimit,DepthLimit),
	singleE(DepthLimit,EI,Ts),
	%numbersList(From,To,EIs),
	%allEs(DepthLimit,EIs,Ts),
	length(Ts,K), write(K),	
	%remove_duplicates(Ts,Ts1), length(Ts1,K1), write(' Duplicate removed, then remain:  '), write(K1),% in case of no duplicates--then no remove_duplicate to save time
	write(' HYPOSESE have been obtained and they are '),nl,
	nl,print_list(Ts)
	.
	%, told.

all(From,To):-
	%tell('hypothesesGenTest.txt'),
	set(depthLimit,DepthLimit),
	numbersList(From,To,EIs),
	allEs(DepthLimit,EIs,Ts),
	length(Ts,K), write(K),	remove_duplicates(Ts,Ts1), length(Ts1,K1), write(' Duplicate removed, then remain:  '), write(K1),% in case of no duplicates--then no remove_duplicate to save time
	write(' HYPOSESE have been obtained and they are '),nl,
	nl%print_list(Ts1)
	.
	%, told.

/*************** Each Example ***************/

% single E -> Ts
singleE(DepthLimit,EI,RecordAll):-
	findall(OneTr,
		(
			gEx(DepthLimit,EI,OneTr0),
		%write(OneTr),nl,
		OneTr0=OneTr, %remove_duplicates(OneTr0,OneTr),
		tInterpreter(OneTr,T),
		%,write('*** One theory'),nl,
		write(OneTr),nl,	% track the ID of clauses in B
		print_list(T),nl,
		nl
	 
		),
		RecordAll).

multiE(DepthLimit,EIs,RecordAll):-
	findall(OneTr,
		(
		multi_gEx(DepthLimit,EIs,OneTr0),
		remove_duplicates(OneTr0,OneTr)
		%, tInterpreter(OneTr,T),
		%nl,nl,write(OneTr),nl,	% track the ID of clauses in B
		%print_list(T),nl,nl
		),
		RecordAll).




/***************************variable connection (BINDING) ********************************/
% bind to one of the list, no worry whether is ground or not 
binding(Hr,[nt_binding1|Hr],X,[X|_]). % can't have '!', otherwise, won't try the later ones.
binding(HrSoFar,Hr,X,[Y|Rest]):-
	binding([nt_binding2|HrSoFar],Hr,X, Rest).

% just extra control (compared with binding, so the same ID with binding)

% ???? what I was doing? this should be the control of the problem (within) top Theory
nLast_nReBinding([TClause|Hr],[nt_binding1,TClause|Hr],X,[X|Rest]):- 
	notMember(b2-Change-X,Hr),
	write('OK, it is allowed to be attached'),writeq({b2-Change-X,Hr}),nl,
/*
	(notMember(b2-Change-X,Hr)->
		write('OK, it is allowed to be attached'),nl;
		write('NO, can not be attached, it is already there'), writeq({b2-Change-X,Hr}),nl
	),
*/
	Rest\==[]. % at least one element in the Rest
	

nLast_nReBinding(HrSoFar,Hr,X,[Y|Rest]):-
	nLast_nReBinding([nt_binding2|HrSoFar],Hr,X, Rest).

notMember(_,[]).
notMember(b2-_-X,[b2-_-Y|Rest]):-
	X\==Y,
	notMember(b2-_-X,Rest).

bodyVarsUpdate(Hr,[nt_bUpdate1|Hr],NewVar,BodyVars,BodyVars):- member(NewVar,BodyVars),!.
bodyVarsUpdate(Hr,[nt_bUpdate2|Hr],NewVar,BodyVars,[NewVar|BodyVars]).



topCla(nt_bUpdate1,[bodyVarsUpdate(NewVar,BodyVars,BodyVars)]). % not to update since it is there
topCla(nt_bUpdate2,[bodyVarsUpdate(NewVar,BodyVars,[NewVar|BodyVars])]).

topCla(nt_binding1,[binding(X,[X|_])]).
topCla(nt_binding2,[binding(X,[Y|Rest]),binding(X,Rest)]).