:- export init/0.
:- export instrans/1.
:- export tracking/0, track/1.
:- export conj/2, if/3.
:- export dbase/1, cleanup/0, key/1.
:- export database/1.
:- export inserteq/2.
:- export inserted/1, deleted/1.
:- export loadtran/1 , loadbase/1.
:- import assert/1, retract/1 from assert.
:- import initkey/0 from keys_basics2.
:- import init_keyappl/0 from keys_appl2.
:- import initdbmode/0 from parser2.
:- import getfreetemp/1 from upload2.
:- import on_backtracking/1, insertbase/1, deletebase/1, dynpred/1, init_basic/0
	  from basic_funs2.

:- op(1150,fx,[instrans,insbase,delbase]).

init :- 
	reconsult(tr_basics2),
	reconsult(tr_appl2),
	reconsult(query2),
	reconsult(keys_basics2),
	reconsult(keys_appl2),
	reconsult(dbmode2),
	reconsult(basic_funs2),
	reconsult(upload2),
	dynpred(tracking), dynamic(tr),
	dynpred(track([])), 
	init_basic, initkey, initdbmode, init_keyappl.


/* ***************************************************************** 
	Insert clause to transaction base
 ***************************************************************** */

instrans('<-'(Lhs,Rhs)) :-
	dotransbody(Rhs,Pro),
	assert((Lhs :- (tr, Pro))),
	checknewrule.

instrans( Pred ) :-
	not(Pred = '<-'(_,_)),
	assert((Pred :- tr)).

dotransbody(sc(A,B),(Pro1,Pro2)) :-
	dotransbody(A,Pro1),
	dotransbody(B,Pro2).
dotransbody(while(with(Varlist),do(Cond,Body)),Temp) :-
	getfreetemp(TempName),
	Temp =.. [TempName|Varlist],
	dotransbody(Body,BPro),
	insertbase(whileclause(Temp,Cond,BPro)).

dotransbody(while(do(Cond,Body)),Temp) :-
	getfreetemp(Temp),
	dotransbody(Body,BPro),
	insertbase(whileclause(Temp,Cond,BPro)).

dotransbody(for(with(Varlist),do(in(List,Cond),Body)),Temp) :-
	getfreetemp(TempName),
	getfreetemp(LoopName),
	Temp = ((assign_to(TempName,from(List,dbase(Cond))), LoopName)),
	LoopBuffer =.. [TempName|List],
	LoopPred =.. [LoopName|Varlist],
	dotransbody(Body,BPro),
	insertbase(forclause(LoopPred,LoopBuffer,BPro)).

dotransbody(for(do(in(List,Cond),Body)),Temp) :-
	getfreetemp(TempName),
	getfreetemp(LoopName),
	Temp = ((assign_to(TempName,from(List,Cond)), LoopName)),
	LoopBuffer =.. [TempName|List],
	dotransbody(Body,BPro),
	insertbase(forclause(LoopName,LoopBuffer,BPro)).

dotransbody(if(then(Cond,else(Alpha,Beta))),VarName) :-
	scan3(Cond,Alpha,Beta,Varlist),
	getfreetemp(Temp),
	VarName =.. [Temp|Varlist],
	dotransbody(Alpha,AlphaPro),
	dotransbody(Beta,BetaPro),
	insertbase(ifthenelse(VarName,Cond,AlphaPro,BetaPro)).

dotransbody(if(then(Cond,Alpha)),VarName) :-
	scan3(Cond,Alpha,true,Varlist),
	getfreetemp(Temp),
	VarName =.. [Temp|Varlist],
	dotransbody(Alpha,AlphaPro),
	insertbase(ifthenelse(VarName,Cond,AlphaPro,true)).

dotransbody(Body,Body) :-
	not Body = sc(_,_),
	not Body = if(_,_),
	not Body = else(_,_),
	not Body = while(_),
	not Body = while(_,_),
	not Body = for(_,_),
	not Body = for(_).

checknewrule :-					% check while loop
	deletebase(whileclause(Temp,Cond,BPro)),
	insertbase((Temp :- tr, dbase(Cond),BPro,Temp)),
	insertbase((Temp :- tr, not(dbase(Cond)))),
	checknewrule.
checknewrule :- checknewrulefor.
checknewrulefor :-
	deletebase(forclause(Loopname,Temp,BPro)),
	insertbase((Loopname :- tr, dbase(Temp), del(Temp), BPro, Loopname)),
	insertbase((Loopname :- tr, not(dbase(Temp)))),
	checknewrulefor.
checknewrulefor :- checknewruleif.
checknewruleif :-
	deletebase(ifthenelse(VarName,Cond,AlphaPro,BetaPro)),
	insertbase((VarName :- tr, dbase(Cond), AlphaPro)),
	insertbase((VarName :- tr, not(dbase(Cond)), BetaPro)),
	checknewruleif.
checknewruleif.

scan3(Phi,Alpha,Beta,VarList) :-
	Phi =.. [_|PhiVars],
	Alpha =.. [_|AlphaVars],
	Beta =.. [_|BetaVars],
	scanVars(PhiVars,[],List1),
	scanVars(AlphaVars,List1,List2),
	scanVars(BetaVars,List2,VarList).

scanVars([],X,X).
scanVars([X|L],InList,OutList) :-
	var(X),
	checkrepeat(X,InList,InList,NewList),
	scanVars(L,NewList,OutList).
scanVars([X|L],InList,OutList) :-
	atomic(X), nonvar(X),
	scanVars(L,InList,OutList).
scanVars([X|L],InList,OutList) :-
	not(atomic(X)), 
	X =.. [_|MoreArgs],
	scanVars(MoreArgs,InList,NewList),
	scanVars(L,NewList,OutList).

checkrepeat(X,[],List,[Y|List]) :-
	Y = X.

checkrepeat(X,[Y|_],List,List) :-
	X == Y.
checkrepeat(X,[Y|L],List,List2) :-
	X \== Y, 
	checkrepeat(X,L,List,List2).


/* ***************************************************************** */

conj(A,B) :-	totrack, 
		A, forceback(Tr),
		B, track(Tr2), compare(Tr,Tr2), endconj.


totrack	 :- assert(tracking), on_backtracking(retract(tracking)),
	    assert(track([])), on_backtracking(retract(track([]))).

forceback(X) :- retract(track(X)),
		undotrack(X),  assert(track([])).

endconj :-	
	retract(tracking), on_backtracking(assert(tracking)),
	retract(track(X)), on_backtracking(assert(track(X))).

undotrack([]).
undotrack([(i,Data)|Tr]) :-
	deletebase(Data), undotrack(Tr).
undotrack([(d,Data)|Tr]) :-
	insertbase(Data), undotrack(Tr).

compare([],[]).

compare([(X,D)|Tr1],[(X,D)|Tr2]) :-
		compare(Tr1,Tr2).

if(X,Y,_) :- call(X) , call(Y).
if(X,_,Z) :- not(X),   call(Z).