:- dynamic interpreted/2.


inverse_hInterpreter([th-HeadI],Cla0):- 
	topCla(th-HeadI,Cla0).
inverse_hInterpreter([tb-I|Indexes],NewH):-
	inverse_hInterpreter(Indexes,H),
	topCla(tb-I,Cla),
	resolve(H,Cla,NewH).


tInterpreter(TI,T):- 
	tInterpreter0(TI,T0),
	delete(T0,[],T).

tInterpreter0([],[]).
tInterpreter0([HI|HsIndex],[H|Hs]):-
	tInterpreter0(HsIndex,Hs),
	%claInterpreter(HI,H).
	(claInterpreter(HI,H)->
		Foo=1;
		write('Fail to interpret this one'),write(HI),nl
	).
	



% test: quick interpret when known; assert if unknown --> save next time
claInterpreter(ClaIndex,Cla):- 
	interpreted(ClaIndex,Cla),!.
	%nl,write({ClaIndex,Cla}),nl.%write('---AGAIN').
	%write('Saved Time'),nl.
claInterpreter(ClaIndex,Cla):- 
	hInterpreter(ClaIndex,Cla),
	%nl,write({ClaIndex,Cla}),nl,
	assert(interpreted(ClaIndex,Cla)). %write('---NOT AGAIN---').
	%write('Quicker Next time'),nl.


	
% build up in reversed order
% sequentially, not robust enough, in case the sequence is not correct, may not be able to build
% in the case of horn clauses, only one positive, so the resolvenents are determinestic. 
% have to be top-down, otherwise the two leave nodes at the same level may not be resolved. --- there is a sequence of resolving, although reorder is allowed.


hInterpreter(endNode-Coverage,[]):-!.
hInterpreter(startNode,[]):-!.

hInterpreter([HeadI],Cla0):- 
	topCla(HeadI,Cla0).
hInterpreter([I|Indexes],NewH):-
	Indexes\==[],
	hInterpreter(Indexes,H),
	topCla(I,Cla),
	resolve(H,Cla,NewH).




% assume all Horn-Clauses, so always body literals in Cla1 resolved with Cla2.
% quicker resolving - the record are left-first, so always resolve with the 1st left body.
resolve([Head1|Body1],[Head2|Body2],[Head1|NewBody]):-
	once((append(Body1A,[Atom1|Body1B],Body1),Atom1=Head2)), % ensure left-most/first
		%unify_with_occurs_check(Atom1,Head2),
	concatenateLists([Body1A,Body2,Body1B],NewBody). % It's important that Body1A,Body2,Body1B is arranged in this order!!! not Body1A, Body1B
	
% can be replaced by build-in predicate flattern (list)
concatenateLists([],[]).
concatenateLists([L|Ls],NConnL):-
	concatenateLists(Ls,ConnL),
	nAppend(L,ConnL,NConnL).

%nAppend(Prefix,Suffix,List).
nAppend([],Suffix,Suffix).
nAppend([X|Prefix],Suffix,[X|List]):-
	nAppend(Prefix,Suffix,List).






% ensure it is unique mapping (from Index to Cla)--left-first
testTI(H):-
	%TI=[[1,2,0,6,8,4,1,12,7,3,5,1,11,10]],
	HI=[],%HI=[1,2,0,7,3,5,1,11,6,8,4,1,12,10],
	hInterpreter(HI,H).
	



testHB:-
	%TI=[[1,6,5,2],[1,5,2],[1,4,2]],
	%tInterpreter(TI,T).	
	HI=[[2,5,6,1],[2,5,1],[2,4,1]],
	tInterpreter(HI,H),print_list(H).