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

:- export parse_body/3, initparser/0, write_new_rules/0.
:- import length/2 from basics.
:- import retract/1, assert/1 from assert.
:- import declare/1, separate_key_val/4, keyed/3 from keys_basics4.
:- import incr_counter/2 from keys_appl4.
:- import ins/1, del/1, createpreds/2, dbase/1 from tr_basics4.
:- import call_all/1, append/3, dynpred/1 from basic_funs4.
:- import loop_name/2, temp_name/2 from naming4.


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) :-
	parse_body(forall(with(Vars),unique(do(in(List,Cond),Body))),MainPred,Type).

parse_body(forall(possible(do(in(List,Cond),Body))),MainName,Type) :-
	parse_body(forall(unique(do(in(List,Cond),Body))),MainName,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, Type) :-
        ToPred =.. [ToName|Args],
        length(Args,NArgs),
        keyed(ToName,NArgs,NKeys),
        createpreds(NArgs,FreeArgs),
        AllPred =.. [ToName|FreeArgs],
        (
        NArgs = NKeys -> Steps = (getbag(weak_ins(ToPred),FromPred,CList),
                                  retractall(AllPred),
                                  call_all(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],
	CPred =.. [ToName|Args],
        new_loop(LPred,Type),
        separate_key_val(Args,NKeys,Keys,_),
	NVal is NArgs - NKeys,
	createpreds(NVal,FreeVal),
	append(Keys,FreeVal,KArgs),
        KPred =.. [ToName|KArgs],
        assert((LPred :- KPred, !, true ; ins(CPred))),
        Steps = ( getbag(LPred,FromPred,LList),
                  retractall(AllPred),
                  call_all(LList) )).



/*
parse_body(':='(ToPred,FromPred),Steps,_) :-
	ToPred =.. [Name|Args],
	Temp =.. [temp|Args],
	length(Args,NArgs),
	keyed(Name,NArgs,NKeys),
	NVal is NArgs-NKeys,
	createpreds(NVal,Vals),
	separate_key_val(Args,NKeys,Keys,_),
	append(Keys,Vals,DupArgs),
	DupPred =.. [temp|DupArgs],
	dynpred(DupPred),
	Steps = ( deleting(tr),
		  copy((FromPred,not(DupPred)),Temp),
		  retractall(ToPred),
		  move(Temp,ToPred),
		  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.

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(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])).


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