/* *************************************************************
	parser module
************************************************************** */

:- export parse_body/3, initparser/0, write_new_rules/0, ':='/2.
:- import length/2 from basics.
:- import assert/1, retract/1 from assert.
:- import separate_key_val/4, declare/1, keyed/3 from keys_basics3.
:- import bulk_ins/2, incr_counter/2, call_all_list/1 from keys_appl3.
:- import createpreds/2, dbase/1 from tr_basics3.
:- import getlist/3, deletebase/1, insertbase/1 from basic_funs3.
:- import create_name/3, destroy_name/3, set_name/3, index_list/2, key_name/3,
	  temp_name/2, loop_name/2 from naming3.
:- op(900,xfy,':=').

initparser :- assert(templist([])), 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).

% translate if- then- and else- statement and put into the predicate if/3
%
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).

% translation of while loop statement by giving a new predicate as the loop 
% name; 
% the parameters are recorded for later insertion of the translated rules
%
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),
	insertbase(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),
	insertbase(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,
	new_temp(TempName,Total,Type),
	declare(TempName/Total),
	insertbase(forpossible(MainPred,LoopPred,LoopN,TempName,List,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,
	new_temp(TempName,Total,Type),
	declare(TempName/Total),
	insertbase(forpossible(MainName,LoopPred,LoopN,TempName,List,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),
	insertbase(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),
	insertbase(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),
	insertbase(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),
	insertbase(forclause(MainName,[],LoopName,List,Cond,Body,Type)).

parse_body(':='(ToPred,FromPred), Steps, Type) :-
	ToPred =.. [ToName|Args],
	length(Args,NArgs),
	index_list(NArgs,IdList),
	keyed(ToName,NArgs,NKeys),
	createpreds(NArgs,FreeArgs),
	destroy_name(ToName,IdList,DesName),	
	DesPred =.. [DesName|FreeArgs],	
	create_name(ToName,IdList,CName),
	CPred =.. [CName|Args],
	AllPred =.. [ToName|FreeArgs],
	(
	NArgs = NKeys -> Steps = (getlist(CPred,FromPred,CList),
				  getlist(DesPred,AllPred,DList),
		 		  call_all_list(DList),
		 		  call_all_list(CList) )
	;
	% add new rule
	% loop_N(X,Y) :- key_2_p(X), !, true
	%	    	 ;
	%	    	 create_2_p(X,Y).
	% getlist(create_2_p(X,Y),q(X,Y,Z),CList)
	% destroy_all(destroy_2_p(X,Y))
	% call_all_list(CList)
	incr_counter(N,1),
	loop_name(N,LoopName),
	LPred =.. [LoopName|Args],
	new_loop(LPred,Type),
	separate_key_val(Args,NKeys,Keys,_),
	key_name(ToName,IdList,KName),
	KPred =.. [KName|Keys],
	assert((LPred :- KPred, !, true ; CPred)),
	Steps = ( getlist(LPred,FromPred,LList),
		  getlist(DesPred,AllPred,DList),
		  call_all_list(DList),
		  call_all_list(LList) )).


% translation to create predicate
parse_body(create(Pred),CPred,_) :-
	Pred =.. [Name|Args],
	length(Args,NArgs),
	index_list(NArgs,IdList),
	create_name(Name,IdList,CName),
	CPred =.. [CName|Args].

% translation to destroy predicate
parse_body(destroy(Pred),DPred,_) :-
	Pred =.. [Name|Args],
	length(Args,NArgs),
	index_list(NArgs,IdList),
	destroy_name(Name,IdList,DName),
	DPred =.. [DName|Args].

% translation to set predicate
parse_body(set(Pred),SPred,_) :-
	Pred =.. [Name|Args],
	length(Args,NArgs),
	index_list(NArgs,IdList),
	set_name(Name,IdList,SName),
	SPred =.. [SName|Args].

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,LoopN,TempName,Args,Cond,Body,query) :-
	length(Args,NArgs),
	Total is NArgs + 1,
	index_list(Total,IdList),
	destroy_name(TempName,IdList,DName),
	DPred =.. [DName,LoopN|Args],
	TempPred =.. [TempName,LoopN|Args],
	parse_body(Body,PBody,query),
	assert((MainPred :- incr_counter(LoopN,1), (bulk_ins(Cond,TempPred), LoopPred))),
	assert((LoopPred :- TempPred, DPred, PBody, LoopPred)),
	assert((LoopPred :- not(TempPred))).

write_forpossible(MainPred,LoopPred,LoopN,TempName,Args,Cond,Body,transaction) :-
	length(Args,NArgs),
	Total is NArgs+1,
	index_list(Total,IdList),
	destroy_name(TempName,IdList,DName),
	DPred =.. [DName,LoopN|Args],
	TempPred =.. [TempName,LoopN|Args],
	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, DPred, PBody, LoopPred)),
	write('.'), nl,
	write_canonical((LoopPred :- tr, not(TempPred))),
	write('.'), nl.


% insert the translated rules for while loop according to the input parameters
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.


% retract the asserted parameters for the loops and assert the required
% translated rules by calling appropriate subroutine
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,LoopN,TempName,Args,Cond,Body,Type)),
	write_forpossible(MainPred,LoopPred,LoopN,TempName,Args,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.

% put the name of new loop to the looplist if query
new_loop(_,transaction).
new_loop(Pred,query) :-
	deletebase(looplist(L)),
	insertbase(looplist([Pred|L])).

% put the name of new temp predicate to the templist if query
new_temp(_,_,transaction).
new_temp(TempName,NArgs,query) :-
	createpreds(NArgs,Args),
	Pred =.. [TempName|Args],
	deletebase(templist(L)),
	insertbase(templist([Pred|L])).

not(X) :- call(X), !, fail
	  ;
	  true.