/* *************************************************************
	module for parser 4 
************************************************************** */

initparser :- assert(looplist([])).

% parsing for transaction query
%
parsingcond(Cond,PCond) :-
	PCond = dbase(Cond).

parse_body(sc(B1,B2),PBody,Type) :-
	parse_body(B1,PB1,Type),
	parse_body(B2,PB2,Type),
	PBody = (PB1,PB2).

parse_body(if(then(Cond,else(Alpha,Beta))),if(CList,AList,BList),Type) :-
        parsingcond(Cond,CList),
        parse_body(Alpha,AList,Type),
        parse_body(Beta,BList,Type).

parse_body(if(then(Cond,Alpha)),if(CList,AList,true),Type) :-
        parsingcond(Cond,CList),
        parse_body(Alpha,AList,Type).

parse_body(while(with(Varlist),do(Cond,Body)),LoopPred,Type) :-
	incr_counter(N,1),
	loop_name(N,LoopName),
	LoopPred =.. [LoopName|Varlist],
	new_loop(LoopPred,Type),
	assert(whileclause(LoopPred,Cond,Body,Type)).

parse_body(while(do(Cond,Body)),LoopName,Type) :-
	incr_counter(N,1),
	loop_name(N,LoopName),
	new_loop(LoopName,Type),
	assert(whileclause(LoopName,Cond,Body,Type)).

% translation of for loop statement by giving a new predicate as the loop 
% name; 
% a temperory predicate is declared for holding the loop variant
% the parameters are recorded for later insertion of the translated rules
%
% syntax: with Vars forall possible List in Cond do Body
%
parse_body(forall(with(Vars),possible(do(in(List,Cond),Body))), MainPred, Type) :-
	incr_counter(N,2),
	temp_name(N,TempName),
	loop_name(N,MainName),
	MainPred =.. [MainName|Vars],
	new_loop(MainPred,Type),
	M is N+1,
	loop_name(M,LoopName),
	LoopPred =.. [LoopName,LoopN|Vars],
	new_loop(LoopPred,Type),
	length(List,NArgs),
	Total is NArgs+1,
	TempPred =.. [TempName|List],
	declare(TempName/Total),
	assert(forpossible(MainPred,LoopPred,TempPred,LoopN,Cond,Body,Type)).

parse_body(forall(possible(do(in(List,Cond),Body))),MainName,Type) :-
	incr_counter(N,2),
	temp_name(N,TempName),
	loop_name(N,MainName),
	new_loop(MainName,Type),
	M is N+1,
	loop_name(M,LoopName),
	LoopPred =.. [LoopName,LoopN],
	new_loop(LoopPred,Type),
	length(List,NArgs),
	Total is NArgs+1,
	TempPred =.. [TempName,LoopN|List],
	declare(TempName/Total),
	assert(forpossible(MainName,LoopPred,TempPred,LoopN,Cond,Body,Type)).



% syntax: with Vars forall List in Cond do Body
%
parse_body(forall(with(Vars),unique(do(in(List,Cond),Body))), MainPred, Type) :-
	incr_counter(N,2),
	loop_name(N,MainName),
	MainPred =.. [MainName|Vars],
	new_loop(MainPred,Type),
	M is N+1,
	loop_name(M,LoopName),
	assert(forunique(MainPred,Vars,LoopName,List,Cond,Body,Type)).

parse_body(forall(unique(do(in(List,Cond),Body))), MainName, Type) :-
	incr_counter(N,2),
	loop_name(N,MainName),
	new_loop(MainName,Type),
	M is N+1,
	loop_name(M,LoopName),
	assert(forunique(MainName,[],LoopName,List,Cond,Body,Type)).

% syntax: with Vars forall List in Cond do Body
%
parse_body(forall(with(Vars),do(in(List,Cond),Body)), MainPred, Type) :-
	incr_counter(N,2),
	loop_name(N,MainName),
	MainPred =.. [MainName|Vars],
	new_loop(MainPred,Type),
	M is N+1,
	loop_name(M,LoopName),
	assert(forclause(MainPred,Vars,LoopName,List,Cond,Body,Type)).

parse_body(forall(do(in(List,Cond),Body)), MainName, Type) :-
	incr_counter(N,2),
	loop_name(N,MainName),
	new_loop(MainName,Type),
	M is N+1,
	loop_name(M,LoopName),
	assert(forclause(MainName,[],LoopName,List,Cond,Body,Type)).


parse_body(':='(ToPred,FromPred),Steps,_) :-
	ToPred =.. [Name|Args],
	length(Args,NArgs),
	keyed(Name,NArgs,NKeys),
	( 
	(NArgs = NKeys) -> Steps = 
				( deleting(tr),
				  getlist(weakins(ToPred),FromPred,List),
				  retractall(ToPred),
				  call_all(List),
				  inserting(tr) )	
	;
	NVal is NArgs-NKeys,
	createpreds(NVal,Vals),
	separate_key_val(Args,NKeys,Keys,_),
	append(Keys,Vals,DupArgs),
	DupPred =.. [Name|DupArgs],
	Steps = ( deleting(tr),
		  getlist((not(DupPred),weakins(ToPred)),FromPred,List),
		  retractall(ToPred),
		  call_all(List),
		  inserting(tr)) ).


parse_body(set(Pred),SPred,_) :-
	Pred =.. [Name|Args],
	length(Args,NArgs),
	keyed(Name,NArgs,NKeys),
	NArgs > NKeys,
	NVal is NArgs-NKeys,
	separate_key_val(Args,NKeys,Keys,_),
        createpreds(NVal,OldVals),
	append(Keys,OldVals,OldArgs),
	OldPred =.. [Name|OldArgs],
	SPred = (retract(OldPred), assert(Pred)) .

parse_body(create(Pred),CPred,_) :-
	Pred =.. [Name|Args],
	length(Args,NArgs),
	keyed(Name,NArgs,NKeys),
	(
	NKeys = NArgs -> CPred = ins(Pred)
	;
	NVal is NArgs-NKeys,
	separate_key_val(Args,NKeys,Keys,_),
        createpreds(NVal,OldVals),
	append(Keys,OldVals,OldArgs),
	OldPred =.. [Name|OldArgs],
	CPred = (not(OldPred), assert(Pred)) ).


parse_body(destroy(Pred),DPred,_) :-
	DPred = retract(Pred).

parse_body(Body,Body,_) :-
	not(Body = sc(_,_)),
	not(Body = while(_,_)),
	not(Body = while(_)),
	not(Body = for(_)),
	not(Body = for(_,_)),
	not(Body = if(_)),
	not(Body = else(_,_)),
	not(Body = conj(_,_)),
	not(Body = ':='(_,_)),
	not(Body = create(_)),
	not(Body = destroy(_)),
	not(Body = set(_)).

% translate to:
% forallloop(Z) :- setof([X,Y],alpha(X,Y,Z),List), loop(List,Z).
% loop([[X,Y]|List],Z) :- beta(X,Y,Z), loop(List,Z).
% loop([],Z).
write_forall(MainPred,Vars,LoopName,List,Cond,Body,query) :-
	LoopPred =.. [LoopName,LoopList|Vars],
	LoopHead =.. [LoopName,[List|LoopList]|Vars],
	LoopTerm =.. [LoopName,[]|Vars],
	new_loop(LoopPred,query),
	parse_body(Body,PBody,query),
	assert((MainPred :- getbag(List,Cond,LoopList), LoopPred)),
	assert((LoopHead :- PBody, !, LoopPred)),
	assert((LoopTerm)).

write_forall(MainPred,Vars,LoopName,List,Cond,Body,transaction) :-
	LoopPred =.. [LoopName,LoopList|Vars],
	LoopHead =.. [LoopName,[List|LoopList]|Vars],
	LoopTerm =.. [LoopName,[]|Vars],
	new_loop(LoopPred,transaction),
	parse_body(Body,PBody,transaction),
	write_canonical((MainPred :- tr, getbag(List,Cond,LoopList), LoopPred)),
	write('.'), nl,
	write_canonical((LoopHead :- tr, PBody, !, LoopPred)),
	write('.'), nl,
	write_canonical((LoopTerm)),
	write('.'), nl.

write_forunique(MainPred,Vars,LoopName,List,Cond,Body,query) :-
	LoopPred =.. [LoopName,LoopList|Vars],
	LoopHead =.. [LoopName,[List|LoopList]|Vars],
	LoopTerm =.. [LoopName,[]|Vars],
	new_loop(LoopPred,query),
	parse_body(Body,PBody,query),
	assert((MainPred :- getlist(List,Cond,LoopList), LoopPred)),
	assert((LoopHead :- PBody, !, LoopPred)),
	assert((LoopTerm)).
write_forunique(MainPred,Vars,LoopName,List,Cond,Body,transaction) :-
	LoopPred =.. [LoopName,LoopList|Vars],
	LoopHead =.. [LoopName,[List|LoopList]|Vars],
	LoopTerm =.. [LoopName,[]|Vars],
	new_loop(LoopPred,transaction),
	parse_body(Body,PBody,transaction),
	write_canonical((MainPred :- tr, getlist(List,Cond,LoopList), LoopPred)),
	write('.'), nl,
	write_canonical((LoopHead :- tr, PBody, !, LoopPred)),
	write('.'), nl,
	write_canonical((LoopTerm)),
	write('.'), nl.


% insert the translated rules for for-loops according to the input parameters
write_forpossible(MainPred,LoopPred,TempPred,LoopN,Cond,Body,query) :-
	parse_body(Body,PBody,query),
	assert((MainPred :- incr_counter(LoopN,1), (bulk_ins(Cond,TempPred), LoopPred))),
	assert((LoopPred :- TempPred, retract(TempPred), PBody, !, LoopPred)),
	assert((LoopPred :- not(TempPred))).

write_forpossible(MainPred,LoopPred,TempPred,LoopN,Cond,Body,transaction) :-
	parse_body(Body,PBody,transaction),
	write_canonical((MainPred :- tr, incr_counter(LoopN,1), (bulk_ins(Cond,TempPred), LoopPred))),
	write('.'), nl,
	write_canonical((LoopPred :- tr, TempPred, retract(TempPred), PBody, !, LoopPred)),
	write('.'), nl,
	write_canonical((LoopPred :- tr, not(TempPred))),
	write('.'), nl.



write_whileloop(LoopPred,Cond,Body,query) :-
	parsingcond(Cond,PCond),
	parse_body(Body,PBody,query),
	assert((LoopPred :- PCond, PBody, !, LoopPred)),
	assert((LoopPred :- not(PCond))).

write_whileloop(LoopPred,Cond,Body,transaction) :-
	parsingcond(Cond,PCond),
	parse_body(Body,PBody,transaction),
	write_canonical((LoopPred :- tr, PCond, PBody, !, LoopPred)),
	write('.'), nl,
	write_canonical((LoopPred :- tr, not(PCond))),
	write('.'), nl.

% write new rules for while loop, and for loop
%
write_new_rules :-
	retract(whileclause(LoopPred,Cond,Body,Type)),
	write_whileloop(LoopPred,Cond,Body,Type),
	write_new_rules.

write_new_rules :-
	retract(forpossible(MainPred,LoopPred,TempPred,LoopN,Cond,Body,Type)),
	write_forpossible(MainPred,LoopPred,TempPred,LoopN,Cond,Body,Type),
	write_new_rules.

write_new_rules :-
	retract(forclause(MainPred,Vars,LoopName,List,Cond,Body,Type)),
	write_forall(MainPred,Vars,LoopName,List,Cond,Body,Type),
	write_new_rules.
write_new_rules :-
	retract(forunique(MainPred,Vars,LoopName,List,Cond,Body,Type)),
	write_forunique(MainPred,Vars,LoopName,List,Cond,Body,Type),
	write_new_rules.

write_new_rules.




new_loop(_,transaction).
new_loop(Pred,query) :-
	retract(looplist(L)),
	assert(looplist([Pred|L])).

