:- module(transform,[	xcif/2,			%transform to Xtended-CIF
			rewrite/2,		%rewrite negated quantification
			negate/2,
			fill_miss/2,		%fill missing quantification in a flatten manner
			fillmissing/2,		%fill missing quantification in a nested manner
			push_negation/2,
			simplify/2,
			skolemise/2,
			promote/2
		]).


:- use_module('../../prolog/util/prolog_detect').

:- prolog_detect:prolog(Prolog),
	(	(	Prolog=sicstus,
			use_module(library(lists))
		);
		true
	).
:- use_module('../../prolog/util/cif_util').
:- use_module('../../prolog/util/is_daplex_variable').





xcif(Cif,Xcifed) :-
	push_negation(Cif,Pushed),		%push negation down
	rewrite(Pushed,Rewritten),		%rewrite negated quantification
	fill_miss(Rewritten,Filled),		%fill in missing quantifiers & generators
	promote(Filled,Xcifed).			%promote quantifiers



%----------------------------------
% promote/2
%
% promote(+Cif,-Promoted)
%
% Cif		=	CIF to be promoted
% Promoted	=	promoted CIF
%
%
% promote nested quantifiers in CIF
%
% Because of the "weak-translation" of "implication" in a UQC,
% a nested UQC in the form:
%
%	all x, G(x) -> (P(x) ^ (all y, H(x,y) -> Q(x,y)))
%
% is transformed into a conjunction of 2 UQCs (because
% the extra condition may not be true):
%
%	(all x, G(x) -> P(x)) AND (all x,y G(x)^H(x,y) -> P(x)^Q(x,y))
%
% However, this doesn't apply for nested EQCs, because
% there is no "weak-translation" for EQCs.
% Thus we have:
%
%	some x, G(x)^P(x)^(some y, H(x,y)^Q(y))
%
% is transformed into a single EQC:
%
%	some x,y G(x)^H(x,y)^P(x)^Q(y)
%
%----------------------------------

%
% promote/2
%
% the top-level predicate for promoting nested quantifiers
%
promote(Cif,Promoted) :-
	promote(non_group,group,Cif,Promoted).			%by default, UQCs are non_grouped & EQCs grouped


%
% promoted/4
%
% promote nested quantifiers according to promoting-mode
%
% promote(+Uqc_mode,+Eqc_mode,+Cif,-Promoted)
%
% Uqc_mode	=	mode for nested UQCs. Either group/non_group.
% Eqc_mode	=	mode for nested EQCs. Either group/non_group.
% Cif		=	CIF to be promoted
% Promoted	=	the promoted one
%

%
% end of list
%
promote(_,_,[],[]) :-
	!.

%
% CIF is a list
%
promote(Uqc_mode,Eqc_mode,[C|Cs],Promoted) :-
	!,
	promote(Uqc_mode,Eqc_mode,C,P),		%promote the head
	promote(Uqc_mode,Eqc_mode,Cs,Ps),	%and the tail
	append_cif(P,Ps,Promoted).		%join them together
	%
	% NOTE:	we cannot simply put them back as head & tail
	%	as the head may have turned into a list
	%	by promoting the nested quantifiers
	%

%
% CIF is a promotable construct like restrict_subquery/3
%
promote(Uqc_mode,Eqc_mode,C,Promoted) :-
	C=restrict_subquery(Q,G,P),					%C is a quantified constraint
	!,
	promote(Uqc_mode,Eqc_mode,G,Promoted_g),			%*** DO WE NEED TO PROMOTE G TOO?
	promote(Uqc_mode,Eqc_mode,P,Promoted_p),			%promote the predicate P 1st
	promote(Uqc_mode,Eqc_mode,Q,Promoted_g,Promoted_p,Promoted).	%and check for nested quantifiers

%
% all others
%
promote(_,_,C,C).



%
% promote/6
%
% Now we know that the outside one is either a UQC or EQC.
% Look for nested ALL or SOME in the predicate part of a quantified
% constraint and see if they can be promoted.
%
% promote(+Uqc_mode,+Eqc_mode,+Quantifier,+Gen,+Pred,-Promoted)
%
% Uqc_mode	=	mode for nested UQCs. Either group/non_group.
% Eqc_mode	=	mode for nested EQCs. Either group/non_group.
% Quantifier	=	quantifier in all/1 or some/1
% G		=	the generator
% P		=	the predicate
% Promoted	=	the promoted constraint in restrict_subquery/3 format
%

%
% for UQC
%
promote(Uqc_mode,Eqc_mode,all(Vs),G,P,Promoted) :-
	%
	% scan P for any promotion.
	%
	promote(Uqc_mode,Eqc_mode,all(Vs),G,P,[],Remain,Temp_promoted),	%start w/ nothing remaining & see what is left behind which cannot be promoted
	(	(	Remain=[],					%nothing left behind, that's it
			!,
			Promoted=Temp_promoted
		);
		(	First_one=restrict_subquery(all(Vs),G,Remain),	%something left behind, make a UQC from it
			append_cif(First_one,Temp_promoted,Promoted)	%append the 2 together
		)
	).

%
% for EQC
%
promote(Uqc_mode,Eqc_mode,some(Vs),G,P,Promoted) :-
	promote(Uqc_mode,Eqc_mode,some(Vs),G,P,[],Remain,Temp_promoted),	%try to promote nested SOMEs
	(	(	Remain=[],
			!,
			Promoted=Temp_promoted
		);
%		format("WARNING: promote/6 has something remaining~n",[])	%trap for error
		(	First_one=restrict_subquery(some(Vs),G,Remain),
			append_cif(First_one,Temp_promoted,Promoted)
		)
	).



%
% promote/8
%
% promote(Uqc_mode,Eqc_mode,Q,G,P,Previous,Remain,Promoted)
%
% Uqc_mode	=	mode for nested UQCs. Either group/non_group.
% Eqc_mode	=	mode for nested EQCs. Either group/non_group.
% Q		=	quantifier w/ var in all(X) or some(X)
% G		=	the current generator
% P		=	the current predicate
% Previous_remain=	CIF passing down from the scanning process, which cannot be promoted
% Remain	=	constructs that cannot be promoted. Will be passed back.
% Promoted	=	the promoted CIF
%
% scan through P and see if there is any possible promotion of nested ALL/ALL or SOME/SOME
% NOTE:	when calling promote/8, all potential promotion in P & G are already done.
%



promote(non_group,_,all(_),_,[],Remain,Remain,[]) :-
	!.


promote(group,_,all(_),_,[],Remain,Remain,[]) :-
	!,
	format("*** ERROR: group mode of UQC in promote/8 not yet implemented~n",[]),
	fail.


%::::::::::::::::::::::::
%
% something inside an ALL
%
%::::::::::::::::::::::::
%
% ALL within ALL and P is a single UQC in restrict_subquery/3
%
% P simply gets promoted
%
% all x, G(x) -> (all y, H(x,y) -> P(x,y))
%
% becomes:
%
% all x,y, G(x)^H(x,y) -> P(x,y)
%
promote(non_group,_,all(Vs),G,P,Remain,Remain,Promoted) :-
	P=restrict_subquery(all(Nested_vs),Nested_g,Nested_p),		%P is a single UQC
	!,
	my_union(Vs,Nested_vs,New_vs),					%combine my vars w/ the nested vars
	append_cif(G,Nested_g,New_g),					%combine the Gs
	New_p=Nested_p,							%use the nested P
	Promoted=restrict_subquery(all(New_vs),New_g,New_p).		%now this is the promoted one

%
% ALL within ALL, where P is a list
%
% the head of P is an ALL
%
promote(non_group,Eqc_mode,all(Vs),G,[P|Ps],Old_remain,Remain,Promoted) :-
	P=restrict_subquery(all(Nested_vs),Nested_g,Nested_p),				%the head is a UQC
	!,
	%
	% work on the tail and see what is left behind on this level and cannot be promoted
	%
	promote(non_group,Eqc_mode,all(Vs),G,Ps,Old_remain,Remain,Ps_promoted),		%look for promotion in the tail
	%
	% combining the UQC in the head with the UQC in the upper level
	%
	% for Q, the 2 sets of vars are combined
	% for G, the 2 Gs are merged
	% for P, the "Remain" part of P is merged with the "nested P"
	% Because of the weak-translation of the UQ, the "Remaining" part
	% of P is also passed back to contruct another UQC, where only
	% G(x) is true. As illustrated:
	%
	% all x, G(x) -> (P(x) ^ (all y, H(x,y) -> Q(x,y)))
	%
	% (all x, G(x) -> P(x)) ^ (all x,y, G(x)^H(x,y) -> P(x)^Q(x,y))
	%
	my_union(Vs,Nested_vs,New_vs),							%quantify over the union of vars
	append_cif(G,Nested_g,New_g),							%combine w/ the nested G
	append_cif(Nested_p,Remain,New_p),
	P_promoted=restrict_subquery(all(New_vs),New_g,New_p),				%the combined UQC
	append_cif(P_promoted,Ps_promoted,Promoted).

%
% the head of P is NOT an ALL
%
promote(Uqc_mode,Eqc_mode,all(Vs),G,[P|Ps],Old_remain,Remain,Promoted) :-
	!,
	append_cif(Old_remain,P,Temp_remain),				%P is not promotable, pass it on
	promote(Uqc_mode,Eqc_mode,all(Vs),G,Ps,Temp_remain,Remain,Promoted).		%proceed w/ the tail

%
% all others, when P is not a list
%
promote(_,_,all(_),_,P,Old_remain,Remain,Promoted) :-
	Promoted=[],							%nothing gets promoted
	append_cif(Old_remain,P,Remain).				%pass P back as the "remaining" stuff
%	Promoted=restrict_subquery(all(Vs),G,P),
%	Remain=Old_remain.



%::::::::::::::::::::::::
%
% something inside a SOME
%
%::::::::::::::::::::::::
%
%	There are 2 modes in promoting nested EQC
%	In the "group" mode, all nested EQCs on the same level are grouped into a single EQC.
%	i.e.
%		exist x, G(x)^P(x) ^ ( (exist y, H(x,y) ^ Q(x,y)) ^ (exist z, K(x,z)^R(x,z)) )
%
%	becomes:
%
%		exist x,y,z, G(x)^H(x,y)^K(x,z)^P(x)^Q(x,y)^R(x,z)
%
%	In the "non_group" mode, they remain as individual promoted EQC:
%
%		(exist x,y, G(x)^H(x,y)^P(x)^Q(x,y)) ^ (exist x,z, G(x)^K(x,z)^P(x)^R(x,z))
%
%

%
%
% something within SOME
%


promote(_,group,some(Vs),G,[],Remain,[],Promoted) :-
	!,
	Promoted=restrict_subquery(some(Vs),G,Remain).

promote(_,non_group,some(_),_,[],Remain,Remain,[]).

%
% P is a single EQC
% group mode, all "remaining" stuff are put into P
%
promote(_,group,some(Vs),G,P,Remain,[],Promoted) :-
	P=restrict_subquery(some(Nested_vs),Nested_g,Nested_p),		%P is a single EQC
	!,
	my_union(Vs,Nested_vs,New_vs),					%combine my vars w/ the nested vars
	append_cif(G,Nested_g,New_g),					%combine the Gs
	append_cif(Remain,Nested_p,New_p),				%put all "remaining" stuff into P
	Promoted=restrict_subquery(some(New_vs),New_g,New_p).		%now this is the promoted one

%
% P is a single EQC
% non_group mode, all remaining stuff are returned
%
promote(_,non_group,some(Vs),G,P,Remain,Remain,Promoted) :-
	P=restrict_subquery(some(Nested_vs),Nested_g,Nested_p),		%P is a single EQC
	!,
	%
	% the nestd EQC is combined with the EQC in the upper level
	% no change in the "remain" stuff
	%
	my_union(Vs,Nested_vs,New_vs),					%combine my vars w/ the nested vars
	append_cif(G,Nested_g,New_g),					%combine the Gs
	New_p=Nested_p,							%use the nested P
	Promoted=restrict_subquery(some(New_vs),New_g,New_p).		%now this is the promoted one


%
% SOME within SOME, head of P is an EQC
% group mode, 2 nested EQCs are fused
%
promote(Uqc_mode,group,some(Vs),G,[P|Ps],Old_remain,Remain,Promoted) :-
	P=restrict_subquery(some(Nested_vs),Nested_g,Nested_p),			%the head is a EQC
	!,
	%
	% combing the EQC in the head with the EQC in the upper level
	%
	% for Q, the 2 sets of vars are combined
	% for G, the 2 Gs are merged
	% for P, we combine the "remaining" stuff with the original P.
	% i.e.:
	%
	% exists x, G(x) ^ P(x) ^ (exist y, H(x,y) ^ Q(x,y))
	%
	% becomes
	%
	% exists x,y, G(x)^P(x)^H(x,y)^Q(x,y)
	%
	promote(Uqc_mode,group,some(Vs),G,Ps,Old_remain,Remain,Ps_promoted),		%promote tail & get remaining stuff
	%
	% tail promoted MUST BE an EQC
	%
	(	%
		% if Ps_promoted is an empty list, then forget about it
		%
		(	Ps_promoted=[],
			!,
			Ps_vs=[],
			Ps_g=[],
			Ps_p=[]
		);
		%
		% otherwise take its Vs, G & P
		%
		(	Ps_promoted=restrict_subquery(some(Ps_vs),Ps_g,Ps_p),
			!
		);
		format("*** WARNING: promote/8 GROUP-mode error: tail not transformed to as EQC~n",[]),
		write(Ps_promoted),nl
	),
	%
	% in the group mode, combine everybody's Vs, G & P
	%
	my_union(Vs,Nested_vs,Temp_vs),
	my_union(Temp_vs,Ps_vs,New_vs),						%also combine w/ Ps' vars
	append_cif(G,Nested_g,Temp_g),
	append_cif(Temp_g,Ps_g,New_g),
	append_cif(Nested_p,Ps_p,New_p),
	Promoted=restrict_subquery(some(New_vs),New_g,New_p).			%the overall promoted EQC

%
% SOME within SOME, head of P is an EQC
% non-group mode
%
promote(Uqc_mode,non_group,some(Vs),G,[P|Ps],Old_remain,Remain,Promoted) :-
	P=restrict_subquery(some(Nested_vs),Nested_g,Nested_p),			%the head is a EQC
	!,
	%
	% combing the EQC in the head with the EQC in the upper level
	%
	% for Q, the 2 sets of vars are combined
	% for G, the 2 Gs are merged
	% for P, we combine the "remaining" stuff with the original P.
	% i.e.:
	%
	% exists x, G(x) ^ P(x) ^ (exist y, H(x,y) ^ Q(x,y))
	%
	% becomes
	%
	% exists x,y, G(x)^P(x)^H(x,y)^Q(x,y)
	%
	promote(Uqc_mode,some(Vs),G,Ps,Old_remain,Remain,Ps_promoted),			%promote tail & get remaining stuff
	my_union(Vs,Nested_vs,New_vs),
	append_cif(G,Nested_g,New_g),
	append_cif(Nested_p,Remain,New_p),						%still have to include "remaining" stuff in my P
	P_promoted=restrict_subquery(some(New_vs),New_g,New_p),				%P promoted
	append_cif(P_promoted,Ps_promoted,Promoted).



%
% SOME, head of P is NOT a SOME
% group mode
%
promote(Uqc_mode,group,some(Vs),G,[P|Ps],Old_remain,Remain,Promoted) :-
	!,
	append_cif(P,Old_remain,Temp_remain),
	promote(Uqc_mode,group,some(Vs),G,Ps,Temp_remain,Remain,Promoted).


%
% SOME, head of P is NOT a SOME
% non-group mode
%
promote(Uqc_mode,non_group,some(Vs),G,[P|Ps],Old_remain,Remain,Promoted) :-
	!,
	append_cif(P,Old_remain,Temp_remain),
	promote(Uqc_mode,non_group,some(Vs),G,Ps,Temp_remain,Remain,Promoted).


%
% SOME, where P is not a list nor an EQC
%
promote(_,_,some(_),_,P,Old_remain,Remain,Promoted) :-
	Promoted=[],
	append_cif(P,Old_remain,Remain).
%	Promoted=restrict_subquery(some(Vs),G,P).



%----------------------------------------------
% skolemisation
%
% an existentially quantified variable is replaced
% by a skolem constant "skolem(x)" or skolem function "skolem(x,[vars...])"
% depending on its dependence on other variables
%----------------------------------------------

skolemise(Cif,Skolemised) :-
	skolemise([],Cif,Skolemised),	%skolemisation starting with an empty list of quantified variable
	!.

skolemise(_,[],[]) :-
	!.

skolemise(Us,[C|Cs],[S|Ss]) :-
	skolemise(Us,C,S),		%skolemise a list head
	skolemise(Us,Cs,Ss).		%and tail

skolemise(Us,C,Skolemised) :-
	C=restrict_subquery(some(Var),G,P),
	!,
	(	(	Us=[],					%generate a skolem constant
			generate_skolem_constant(Skolem)
		);
		generate_skolem_function(Us,Skolem)		%or a skolem function
	),
	replace_var_in_cif([Var:Skolem],G,Temp_g),		%replace Var by skolem
	replace_var_in_cif([Var:Skolem],P,Temp_p),
	skolemise(Us,Temp_g,Skolemised_g),			%recursively work on G & P
	skolemise(Us,Temp_p,Skolemised_p),
	Skolemised=restrict_subquery(some(Skolem),Skolemised_g,Skolemised_p).

skolemise(Us,C,Skolemised) :-
	C=restrict_subquery(all(Var),G,P),		%a universally quantified variable
	!,
	skolemise(Us,G,Skolemised_g),			%G still using old vars list
	New_u=[Var|Us],					%1 more universally quantified var for P
	skolemise(New_u,P,Skolemised_p),
	Skolemised=restrict_subquery(all(Var),Skolemised_g,Skolemised_p).

skolemise(Us,C,Skolemised) :-
	C=generate_subquery(Type,Var,Sub,Aux1,Aux2),
	!,
	skolemise(Us,Sub,Skolemised_sub),
	skolemise(Us,Aux1,Skolemised_aux1),
	skolemise(Us,Aux2,Skolemised_aux2),
	Skolemised=generate_subquery(Type,Var,Skolemised_sub,Skolemised_aux1,Skolemised_aux2).

skolemise(_,C,C).



%---------------
% simplify a CIF
%---------------

simplify([],[]) :-				%empty list
	!.

simplify([H|T],Simplified) :-	%a list
	!,
	simplify(H,Simplified_h),
	simplify(T,Simplified_t),
	my_append(Simplified_h,Simplified_t,Simplified).
/*
	(	(	is_list(Simplified_h),
			!,
			append(Simplified_h,Simplified_t,Simplified)
		);
		Simplified=[Simplified_h|Simplified_t]
	).
*/

/*
simplify([H|T],[Simplified_h|Simplified_t]) :-	%a list
	!,
	(	(	H=[Something],				%simplify nested singleton list
			!,
			simplify(Something,Simplified_h)
		);
		simplify(H,Simplified_h)
	),
	simplify(T,Simplified_t).		%simplify the tail
*/

%
% different cases to simplify
%

simplify(logical_or([X]),Simplified) :-		%a logical_or with a singleton list
	!,
	simplify(X,Simplified).

simplify(logical_and([X]),Simplified) :-	%a logical_and with a singleton list
	!,
	simplify(X,Simplified).

%
% logical_and/2
% is replaced by a list
%
simplify(logical_and(A,B),Simplified) :-
	!,
	simplify(A,Simplified_a),
	simplify(B,Simplified_b),
	my_append(Simplified_a,Simplified_b,Simplified).

%
% nested logical_or
%
simplify(logical_or(List),Simplified) :-
	member(logical_or(Something),List),		%there is a nested logical_or
	!,
	delete(List,logical_or(Something),Remaining),	%flatten it out
	my_append(Something,Remaining,New_or_list),
	simplify(logical_or(New_or_list),Simplified).

%
% nested logical_and
%
simplify(logical_and(List),Simplified) :-
	member(logical_and(Something),List),		%there is a nested logical_and
	!,
	delete(List,logical_and(Something),Remaining),
	my_append(Something,Remaining,New_and_list),
	simplify(logical_and(New_and_list),Simplified).

simplify(Construct,Construct) :-
	Construct=generate(_,_,_,_,_),
	!.

simplify(Construct,Construct) :-
	Construct=generate(_,_),
	!.


simplify(Construct,Simplified) :-
	Construct=restrict_subquery(Q,G,P),
	!,
	simplify(G,Simplified_g),
	simplify(P,Simplified_p),
	Simplified=restrict_subquery(Q,Simplified_g,Simplified_p).

simplify(Construct,Simplified) :-
	Construct=generate_subquery(Type,Var,Sub,Aux1,Aux2),
	!,
	simplify(Sub,Simplified_sub),
	simplify(Aux1,Simplified_aux1),
	simplify(Aux2,Simplified_aux2),
	Simplified=generate_subquery(Type,Var,Simplified_sub,Simplified_aux1,Simplified_aux2).

/*
%
% recursively work on the arguments
%
simplify(Construct,Simplified) :-
	Construct =.. [Functor|Args],		%all other terms
	!,
	simplify(Args,Simplified_args),		%recursively work on args
	Simplified =.. [Functor|Simplified_args].
*/

simplify(X,X).					%all the rest that cannot be simplified





%------------------------------------------------------------
% rewrite some quantified constraints
%
% no(X) s.t. P(X) is written into all(X) s.t. ~P(X)
% least(X,1) s.t. P(X) is written into some(X) s.t. P(X)
%
%------------------------------------------------------------

rewrite(Cif,Rewritten) :-
	rewrite_cif(Cif,Temp),		%rewrite
	simplify(Temp,Rewritten).	%and simplify


rewrite_cif([],[]) :-
	!.				%end of list

rewrite_cif([C|Cs],[R|Rs]) :-
	!,
	rewrite_cif(C,R),		%rewrite head
	rewrite_cif(Cs,Rs).		%and rest


%
% no(X) s.t. P(X) is written into all(X) s.t. ~P(X)
%
rewrite_cif(C,Rewritten) :-
	C=restrict_subquery(Q,G,P),
	Q=no(V),					%with the "no" quantifier
	!,
	New_q=all(V),					%convert it to an "all"
	negate(logical_and(P),Negated_p),		%negate P
	push_negation(Negated_p,Pushed_p),
	rewrite(Pushed_p,New_p),			%recursively rewrite it
	rewrite(G,New_g),				%rewrite the generator G as well
	Rewritten=restrict_subquery(New_q,New_g,New_p).


%
% least(X,1) s.t. P(X) is written into some(X) s.t. P(X)
%
rewrite_cif(C,Rewritten) :-
	C=restrict_subquery(Q,G,P),
	Q=least(V,1),					%convert least(V,1)
	!,
	New_q=some(V),					%into some(X)
	rewrite(G,G_rewritten),				%rewrite the generator
	rewrite(P,P_rewritten),				%and the predicate
	Rewritten=restrict_subquery(New_q,G_rewritten,P_rewritten).

%
% any other quantifier
%
rewrite_cif(C,Rewritten) :-
	C=restrict_subquery(Q,G,P),
	!,
	rewrite(G,G_rewritten),
	rewrite(P,P_rewritten),
	Rewritten=restrict_subquery(Q,G_rewritten,P_rewritten).

%
% some infrequently used constructs with nested CIF-Code
%
rewrite_cif(C,Rewritten) :-
	C=generate_subquery(Type,Var,Sub,Aux1,Aux2),
	!,
	rewrite(Sub,Sub_rewritten),
	rewrite(Aux1,Aux1_rewritten),
	rewrite(Aux2,Aux2_rewritten),
	Rewritten=generate_subquery(Type,Var,Sub_rewritten,Aux1_rewritten,Aux2_rewritten).

%
% any other construct
%
rewrite_cif(C,C).






%----------------------------------
% push negation into the expression
%----------------------------------

%
% if input is a list
%

push_negation([],[]) :-
	!.

push_negation([C|Cs],[N|Ns]) :-		%if it is a list
	!,
	push_negation(C,N),		%work on each element
	push_negation(Cs,Ns).

%
% if input is a construct
%

%
% not(true) is false
%
push_negation(logical_not(icode_true),icode_false) :-
	!.

%
% not(false) is true
%
push_negation(logical_not(icode_false),icode_true) :-
	!.

%
% not(not(X)) is X
%
push_negation(X,Pushed) :-
	X=logical_not(logical_not(Something)),	%negation of negation
	!,
	push_negation(Something,Pushed).

%
% if it is a list, then push the negation down to each element
% and recursively work on them
%
push_negation(logical_not(Something),Pushed) :-
	is_list(Something),			%a list is considered logical_and
	!,
	negate(Something,Negated_something),
	push_negation(Negated_something,Pushed).

%
% not(and(x1,x2...)) is transformed to or(not(x1),not(x2)...)
%
push_negation(X,Pushed) :-
	X=logical_not(logical_and(Something)),			%not and
	!,
	negate(Something,Negated_something),			%negate elements in the list
	push_negation(Negated_something,Pushed_something),	%push negation on them
	Pushed=logical_or(Pushed_something).			%change logical_and to logical_or

%
% not(or(x1,x2,...) is transformed to and(not(x1),not(x2)...)
%
push_negation(X,Pushed) :-
	X=logical_not(logical_or(Something)),			%not or
	!,
	negate(Something,Negated_something),			%negate elements in the list
	push_negation(Negated_something,Pushed_something),	%push negation on them
	Pushed=logical_and(Pushed_something).			%change logical_or to logical_and


%
% not(restrict_subquery/3)
%
push_negation(X,Pushed) :-
	X=logical_not(restrict_subquery(Q,G,P)),	%not restrict_subquery/3
	Q=all(V),
	!,
	negate(P,Negated_p),
	push_negation(Negated_p,Pushed_p),
	push_negation(G,Pushed_g),
	Pushed=restrict_subquery(some(V),Pushed_g,Pushed_p).

push_negation(X,Pushed) :-
	X=logical_not(restrict_subquery(Q,G,P)),
	Q=some(V),
	!,
	negate(P,Negated_p),
	push_negation(Negated_p,Pushed_p),
	push_negation(G,Pushed_g),
	Pushed=restrict_subquery(all(V),Pushed_g,Pushed_p).


%
% not(restrict_subquery/2)
%
% not(for all X, P(X)) is transformed to: for some X, ~P(X)
%
push_negation(X,Pushed) :-
	X=logical_not(restrict_subquery(Q,P)),		%not restrict_subquery/2
	Q=all(V),					%with universal quantifier
	!,
	negate(P,Negated_p),
	push_negation(Negated_p,Pushed_p),
	Pushed=restrict_subquery(some(V),Pushed_p).	%convert to some(x)

%
% not(restrict_subquery/2)
%
push_negation(X,Pushed) :-
	X=logical_not(restrict_subquery(Q,P)),	%not restrict_subquery/2
	(	Q=some(V);			%with existential quantifier
		Q=least(V,1)			%or at least 1
	),
	!,
	negate(P,Negated_p),
	push_negation(Negated_p,Pushed_p),
	Pushed=restrict_subquery(all(V),Pushed_p).

push_negation(X,Pushed) :-
	X=logical_not(expression(A,B,Expr)),	%logical_not(expression/3)
	!,
	push_negation(logical_not(Expr),Pushed_expr),
	Pushed=expression(A,B,Pushed_expr).

push_negation(X,Pushed) :-
	X=logical_not(expr(Op,Lhs,Rhs)),
	nth0(Index,[=,<>,>,>=,=<,<],Op),	%negate the operator
	!,
	nth0(Index,[<>,=,=<,<,>,>=],Negated_op),
	Pushed=expr(Negated_op,Lhs,Rhs).

push_negation(X,X) :-
	X=logical_not(_),			%all other logical_not(X)
	!.


%
% for all other terms, recursively work on the args
%
push_negation(X,Pushed) :-
	X =.. [Functor|Args],
	!,
	push_negation(Args,Pushed_args),
	Pushed =.. [Functor|Pushed_args].



%-------------
% negate a CIF
%-------------

negate([],[]) :-		%the empty list
	!.

negate([C|Cs],[N|Ns]) :-
	!,
	N=logical_not(C),	%negate each element
	negate(Cs,Ns).

negate(X,logical_not(X)).	%negate the item





%----------------------------------------------------
% generating a skolem contstant in the form skolem(x)
%----------------------------------------------------

generate_skolem_constant(X) :-
	generate_counter(skolem,Count),
	X=skolem(Count).

%--------------------------------------
% resetting the skolem constant counter
%--------------------------------------

reset_skolem_counter :-
	initialize_counter(skolem).

%----------------------------------------------------
% generate a skolem function in the form skolem(n,args...)
%----------------------------------------------------

generate_skolem_function(Args,X) :-
	generate_counter(skolem_function,Count),
	X=skolem(Count,Args).

%--------------------------------------
% resetting the skolem-function counter
%--------------------------------------

reset_skolem_function_counter :-
	initialize_counter(skolem_function).




%----------------------------------------------------------
% fill in missing quantifiers & generators for variables
%
% fill_missing(+Cif,-Filled)
%
% Cif		=	CIF to be filled
% Filled	=	CIF with missing quantifiers filled
%----------------------------------------------------------

fill_missing(Cif,Filled) :-
	fill_missing(Cif,[],[],Filled).				%start with no quantified & generated var

%
% CIF in a list
%
% fill_missing(Cif,Quantified,Generated,Filled)
%
% Cif		=	CIF to be filled
% Quantified	=	list of variables already quantified
% Generated	=	list of variables already generated
% Filled	=	filled CIF
%

%
% end of list
%
fill_missing([],_,_,[]) :-					%end of list
	!.

fill_missing([C|Cs],Quantified,Generated,[F|Fs]) :-
	is_list(C),						%recursively work on nested list
	!,
	fill_missing(C,Quantified,Generated,F),
	fill_missing(Cs,Quantified,Generated,Fs).

%
% we're looking at places where a new variable can be created
% if that var is quantified, then (most) probably we don't
% have to fill in the missing quantifier
%

%
% 1st element is a restrict_subquery/3 of ALL
%
fill_missing([C|Cs],Quantified,Generated,[F|Fs]) :-
	C=restrict_subquery(all(Vs),G,P),						%a restrict_subquery/3
	!,
	%
	% now there are more quantified vars in G context
	%
	my_union(Vs,Quantified,More_quantified),					%more vars are quantified
	fill_missing_for_g(G,More_quantified,Generated,G_filled,Extra_generated),	%fill G and find extra vars generated in G
	%
	% G may generate more vars, which apply to P
	%
	my_union(More_quantified,Extra_generated,All_quantified),			%more quantified vars
	my_union(Generated,Extra_generated,More_generated),				%more generated vars
	fill_missing(P,All_quantified,More_generated,P_filled),				%work on P with even more quantified vars
	%
	% now this is the new quantifier
	%
	my_union(Vs,Extra_generated,Vars_within_all),
	F=restrict_subquery(all(Vars_within_all),G_filled,P_filled),			%the new restrict_subquery/3
	%
	% NB:	the rest of the list (Cs) is not within the scope of G,
	%	so all those extra quantified vars do not apply to Cs
	%
	fill_missing(Cs,Quantified,Generated,Fs).					%work on rest of tail

%
% 1st element is a generate/2 which is already quantified & generated
%
fill_missing([C|Cs],Quantified,Generated,Filled) :-
	C=generate(_,Var),							%generate/2
	member(Var,Quantified),							%var is already quantified
	member(Var,Generated),							%and generated
	!,
	%
	% we can throw C away as the var is already generated by somebody
	%
	fill_missing(Cs,Quantified,Generated,Filled).				%proceed w/ list

%
% a generate/2 which is quantified but not generated
% just pass C along, then it will be generated
%
fill_missing([C|Cs],Quantified,Generated,[C|Fs]) :-
	C=generate(_,Var),
	member(Var,Quantified),							%quantified but not generated
	!,
	fill_missing(Cs,Quantified,[Var|Generated],Fs).				%Var is now generated by C

%
% 1st element is a generate/2 which is NOT yet quantified
% may or may not be generated (does not matter, we will generate it anyway)
%
fill_missing([C|Cs],Quantified,Generated,F) :-
	C=generate(_,Var),							%a generate/2 but var not quantified
	!,
	%
	% now we have to quantify Var
	%
	G=C,									%use C as G
	P=Cs,									%rest of list as P
	my_union(Var,Quantified,More_quantified),				%more var quantified
	fill_missing_for_g(G,More_quantified,Generated,G_filled,Extra_vars),
	my_union(More_quantified,Extra_vars,Even_more_quantified),		%even more vars to quantify
	fill_missing(P,Even_more_quantified,[Var|Generated],P_filled),		%work on P
	F=[restrict_subquery(all(Var),G_filled,P_filled)].			%now have a new restrict_subquery/3

%
% 1st element is a generate/5 where the result is already quantified & generated
%
fill_missing([C|Cs],Quantified,Generated,Filled) :-
	C=generate(_,_,_,_,Var),					%generate/5
	member(Var,Quantified),						%already quantified
	member(Var,Generated),						%also generated
	!,
	fill_missing(Cs,Quantified,Generated,Fs),			%proceed w/ rest of list
	append_cif(C,Fs,Filled).					%C remains

%
% generate/5, quantified but not generated
%
fill_missing([C|Cs],Quantified,Generated,Filled) :-
	C=generate(_,_,_,Class,Var),					%generate/5 but var not quantified
	member(Var,Quantified),
	!,
	fill_missing(Cs,Quantified,[Var|Generated],Fs),
	append_cif([generate(Class,Var),C],Fs,Filled).			%add the generator


%
% 1st element is a generate/5 where the result is NOT yet quantified
%
fill_missing([C|Cs],Quantified,Generated,F) :-
	C=generate(_,_,_,Class,Var),					%generate/5 but var not quantified
	!,
	G=[generate(Class,Var),C],					%add a generate/2 for it
	P=Cs,								%rest of list as P
	my_union(Var,Quantified,More_quantified),			%more quantified vars
%	fill_missing_quantifier(G,More_quantified_vars,G_filled),		%work on G
	fill_missing_for_g(G,More_quantified,Generated,G_filled,Extra_vars),		%work on G
	my_union(More_quantified,Extra_vars,Even_more_quantified),
%	fill_missing_quantifier(P,More_quantified_vars,P_filled),		%work on P
	fill_missing(P,Even_more_quantified,Generated,P_filled),		%work on P
	F=[restrict_subquery(all(Var),G_filled,P_filled)].		%now have a new restrict_subquery/3

%
% 1st element is a casting relative/3 w/ expression/3 already quantified
%
fill_missing([C|Cs],Quantified,Generated,[C|Fs]) :-
	C=expression(_,_,relative(_,_,To)),				%a casting relative/3 w/ expression/3
	member(To,Quantified),						%var To is already quantified
	!,
	fill_missing(Cs,Quantified,Generated,Fs).

%
% 1st element is a casting relative/3 w/ expression/3 NOT yet quantified
%
fill_missing([C|Cs],Quantified,Generated,F) :-
	C=expression(_,_,relative(Class,_,Var)),			%a casting relative/3 w/ expression/3
	!,
	G=[generate(Class,Var),C],
	P=Cs,								%rest of list as P
	my_union(Var,Quantified,More_quantified),			%more quantified vars
%	fill_missing_quantifier(G,More_quantified,Generated,G_filled),		%work on G
	fill_missing_for_g(G,More_quantified,Generated,G_filled,Extra_vars),		%work on G
	my_union(More_quantified,Extra_vars,Even_more_quantified),
%	fill_missing_quantifier(P,More_quantified,P_filled),		%work on P
	fill_missing(P,Even_more_quantified,Generated,P_filled),		%work on P
	F=[restrict_subquery(all(Var),G_filled,P_filled)].		%now have a new restrict_subquery/3

%
% 1st element is a restrict_subquery/3 of SOME
%
% NB:	bug in the quantified vars
%	have to separate UQed w/ EQed
%	fix it later
%
fill_missing([C|Cs],Quantified,Generated,[F|Fs]) :-
	C=restrict_subquery(some(Vs),G,P),						%a EQC in restrict_subquery/3
	!,
	my_union(Vs,Quantified,More_quantified),					%more quantified vars
	%
	% G is within the scope of these quantified var
	% but no extra var is generated so far
	% When G is filled, we know what vars are generated by it
	%
	fill_missing_for_g(G,More_quantified,Generated,G_filled,Extra_generated),
	my_union(More_quantified,Extra_generated,All_quantified),
	my_union(Generated,Extra_generated,More_generated),
	%
	% P is within the scope of all these generated vars
	%
	fill_missing(P,All_quantified,More_generated,P_filled),				%fill P
	%
	% Find all vars within the scope of this existential quantifier.
	% by taking a union of the Vs in some/1 and those extra vars generated by G
	%
	my_union(Vs,Extra_generated,Vars_within_some),
	F=restrict_subquery(some(Vars_within_some),G_filled,P_filled),		%the updated restrict_subquery/3
	%
	% proceed with the original list of quantified vars & generated vars
	% as the tail is not within the scope of this restrict_subquery/3
	%
	fill_missing(Cs,Quantified,Generated,Fs).					%proceed w/ the rest of list

%
% all other constructs as head
%
fill_missing([C|Cs],Quantified,Generated,Filled) :-
	fill_missing(Cs,Quantified,Generated,Fs),			%recursively work on the tail
	append_cif(C,Fs,Filled).					%better use append_cif/3 as C may be already present


%
% cater for missing quantifier in the generator of a restrict_subquery/3
%
% basically we just find all variables in the CIF and put in
% those extra generate/2
%
fill_missing_for_g(Cif,Quantified,Generated,Filled,Extra_generated) :-
	find_var_types(Cif,Types),						%find all vars in Cif
	fill_missing_for_g2(Types,Cif,Quantified,Generated,Filled,Extra_generated).

%
% scan through the list of vars involved
% and fill in those not generated
%
fill_missing_for_g2([],Cif,_,_,Cif,[]).					%end of var-list

fill_missing_for_g2([Var:_|Vs],Cif,Quantified,Generated,Filled,Extra) :-
	member(Var,Quantified),						%Var is already quantified
	member(Var,Generated),						%also generated
	!,
	fill_missing_for_g2(Vs,Cif,Quantified,Generated,Filled,Extra).	%proceed with list

fill_missing_for_g2([Var:Class|Vs],Cif,Quantified,Generated,Filled,[Var|Extra]) :-
	member(Var,Quantified),						%generated but not quantified
	!,
	F=generate(Class,Var),							%Var is not quantified, fill in missing generate/2
	fill_missing_for_g2(Vs,Cif,Quantified,Generated,Fs,Extra),	%proceed with list
	append_cif(F,Fs,Filled).


fill_missing_for_g2([Var:Class|Vs],Cif,Quantified,Generated,Filled,[Var|Extra]) :-
	F=generate(Class,Var),						%not quantified nor generated
	fill_missing_for_g2(Vs,Cif,Quantified,Generated,Fs,Extra),	%proceed with list
	append_cif(F,Fs,Filled).





%
% fill in missing quantifiers & generators
%

fill_miss([],[]) :-				%an empty list, no need to do anything
	!.

fill_miss(C,Filled) :-
	fill_miss(C,[],Missed_with_gen,F),			%start w/ nothing quantified, find anything missed the needs quantifying
	(	(	Missed_with_gen=[],			%nothing extra needs quantifying
			!,
			Filled=F				%just return it
		);
		(
			separate_var_and_gen(Missed_with_gen,Vars,G),
			Filled=restrict_subquery(all(Vars),G,F)		%by default, they are universally quantified
		)
	).

/*
fill_miss(C,Filled) :-
	fill_miss(C,[],Need_with_type,F),			%start w/ nothing quantified, find anything that needs quantifying
	(	(	Need_with_type=[],			%nothing extra needs quantifying
			!,
			Filled=F				%just return it
		);
		(	make_generator(Need_with_type,G),		%make generators for them
			remove_type_from_var(Need_with_type,Vars),	%get var names
			Filled=restrict_subquery(all(Vars),G,F)		%by default, they are universally quantified
		)
	).
*/

%
% fill_miss/4
%
% fill_miss(+Cif,+Quantified,-Missed_with_gen,-Filled)
%
% +Cif			=	the cif to fill in missing generator
% +Quantified		=	a list of variables already quantified
% -Missed_with_gen	=	a list of variable with generators that need to be filled in
% -Filled		=	the CIF with missing generator filled
%

%
% end of list
%
fill_miss([],_,[],[]) :-
	!.

%
% a list
%
fill_miss([C|Cs],Quantified,Missed_with_gen,Filled) :-
	!,
	fill_miss(C,Quantified,C_missed,C_filled),
	fill_miss(Cs,Quantified,Cs_missed,Cs_filled),
	my_union(C_missed,Cs_missed,Missed_with_gen),
	append_cif(C_filled,Cs_filled,Filled).

%
% a restrict_subquery/3
%
fill_miss(C,Quantified,[],Filled) :-
	C=restrict_subquery(Q,G,P),						%it is a restrict_subquery/3
	!,
	Q=..[Quantifier,Vs],							%get quantifier & vars
	fill_miss(G,Quantified,G_missed_with_gen,Filled_g),			%find those missed in G
	separate_var_and_gen(G_missed_with_gen,G_missed_vars,_),		%separate vars from gens
	my_union(Vs,G_missed_vars,Quantified_for_p),				%more vars "will" get quantified by G
	fill_miss(P,Quantified_for_p,P_missed_with_gen,Filled_p),		%find extra in P

	my_union(G_missed_with_gen,P_missed_with_gen,Temp_missed_with_gen),
	findall(Template,(member(Var,Quantified),Template=Var:_),Quantified_with_dummy_gen),
	remove_quantified_with_gen(Temp_missed_with_gen,Quantified_with_dummy_gen,Extra_vars_with_gen),
/*
	findall(Template,(	member(Var:Gen,Temp_missed_with_gen),		%a var
				not(member(Var,Quantified)),			%which is not yet quantified
				Template= Var:Gen),				%take var & its gen
		Extra_vars_with_gen),						%these are the missing ones
*/
	separate_var_and_gen(Extra_vars_with_gen,Extra_vars,Extra_gens),
	my_union(Vs,Extra_vars,New_vs),						%all vars to be quantified
	New_q =.. [Quantifier,New_vs],						%compose new quantifier w/ vars
	append_cif(Extra_gens,Filled_g,New_g),					%add new gens
	New_p=Filled_p,
	Filled=restrict_subquery(New_q,New_g,New_p).

/*
fill_miss(C,Quantified,[],Filled) :-
	C=restrict_subquery(Q,G,P),					%it is a restrict_subquery/3
	!,
	Q=..[Quantifier,Vs],						%get quantifier & vars
	fill_miss(G,Quantified,G_need_with_type,Filled_g),		%find extra in G
	remove_type_from_var(G_need_with_type,G_need),
	my_union(Vs,G_need,Quantified_for_p),				%more "will" get quantified by G
	fill_miss(P,Quantified_for_p,P_need_with_type,Filled_p),	%find extra in P
	my_union(G_need_with_type,P_need_with_type,Temp_need_with_type),
	add_dummy_type_to_var(Quantified,Quantified_with_type),
	my_subtract(Temp_need_with_type,Quantified_with_type,To_be_quantified_with_type),	%subtract those already quantified
	remove_type_from_var(To_be_quantified_with_type,To_be_quantified),
	my_union(Vs,To_be_quantified,New_vs),
	make_generator(To_be_quantified_with_type,Extra_generators),	%make extra generators
	New_q =.. [Quantifier,New_vs],
	append_cif(Extra_generators,Filled_g,New_g),
	New_p=Filled_p,
	Filled=restrict_subquery(New_q,New_g,New_p).
*/

fill_miss(C,Quantified,[],C) :-
	C=generate(_,Var),
	member(Var,Quantified),
	!.

fill_miss(C,_,[Var:C],[]) :-
	C=generate(_,Var),
	!.

fill_miss(C,Quantified,[],C) :-
	C=generate(_,_,_,_,Var),
	member(Var,Quantified),
	!.

fill_miss(C,_,[Var:[generate(Class,Var),C]],[]) :-
	C=generate(_,_,_,Class,Var),
	!.

fill_miss(C,Quantified,[],C) :-
	C=expression(_,_,relative(_,_,Var)),
	member(Var,Quantified),
	!.

fill_miss(C,_,[Var:[generate(Class,Var),C]],[]) :-
	C=expression(_,_,relative(Class,_,Var)),			%a casting relative/3 w/ expression/3
	!.

fill_miss(C,_,[],C).

%
%
%
make_generator([],[]).
make_generator([Var:Class|Rest],[G|Gs]) :-
	G=generate(Class,Var),
	make_generator(Rest,Gs).

remove_type_from_var(Var:_,Var).
remove_type_from_var([],[]).
remove_type_from_var([X|Xs],[V|Vs]) :-
	remove_type_from_var(X,V),
	remove_type_from_var(Xs,Vs).


remove_quantified_with_gen([],_,[]).

remove_quantified_with_gen([Var:_|Rest],Quantified_with_gen,Rest_removed) :-
	member(Var:_,Quantified_with_gen),				%in quantified set
	!,
	remove_quantified_with_gen(Rest,Quantified_with_gen,Rest_removed).

remove_quantified_with_gen([Var:Gen|Rest],Quantified_with_gen,[Var:Gen|Rest_removed]) :-
	remove_quantified_with_gen(Rest,Quantified_with_gen,Rest_removed).


%
% given a list of Var:Gen, separate it into 2 list
% one is a list of vars, another one is a list of generators
%
separate_var_and_gen([],[],[]).

separate_var_and_gen([Var:Gen|Rest],[Var|Vars],[Gen|Gens]) :-
	separate_var_and_gen(Rest,Vars,Gens).




%
% fillmissing/2
%
fillmissing(Cif,Filled) :-
	fillmissing(Cif,[],all,Filled).			%start w/ an empty list of quantified var

%
% fillmissing/4
%

%
% CIF is a restrict_subquery/3
%
/*
fillmissing(Cif,Quantified,Default_quantifier,Filled) :-
	Cif=restrict_subquery(Q,G,P),			%a restrict_subquery/3 construct
	!,
	Q=..[Quantifier,Var],				%get quantifier & var
	my_union(Var,Quantified,New_quantified),
	fillmissing2(G,Quantified,Default_quantifier,G_filled),
	fillmissing(P,New_quantified,Quantifier,P_filled),
	Filled=restrict_subquery(Q,G_filled,P_filled).
*/
%
% for a quantified constraint like restrict_subquery(Q,G,P),
% we pick out the list of all generate/2 & generate/5 from the generator G.
% Then we scan through this list of generators to produce a nested quantifications.
% Condition in G is pushed inward.
%
fillmissing(Cif,Quantified,_,Filled) :-
	Cif=restrict_subquery(Q,G,P),				%a restrict_subquery/3 construct
	!,
	Q=..[Quantifier,Var],					%get quantifier
	Patterns=[generate(_,_),generate(_,_,_,_,_)],		%make up pattern to match all generators
	match_pattern(G,Patterns,Gens,Non_gen),			%match all generate/2 & generate/5
	(	(	Gens=[],				%no gen at all?! (***SHOULD NOT HAPPEN)
			Filled=restrict_subquery(Q,G,P_filled),				%use old G, but try to fill P
			my_union(Var,Quantified,More_quantified),			%at least, 1 more var quantified
			fillmissing(P,More_quantified,Quantifier,P_filled)		%now fill P
		);
		(	Gens=[_|_],							%some gens
			make_quantification_for_gen(Quantifier,Quantified,Gens,Non_gen,P_filled,More_quantified,Filled),	%make up list of nested quantification
			fillmissing(P,More_quantified,Quantifier,P_filled)		%now fill P
		)
	).
%
% CIF is an empty list
%
fillmissing([],_,_,[]).

%
% CIF is a list
%
fillmissing(Cif,Quantified,Default_quantifier,Filled) :-
	is_list(Cif),
	!,
	Patterns=[generate(_,_),generate(_,_,_,_,_)],		%match all generate/2 & generate/5
	match_pattern(Cif,Patterns,Gens,Non_gen),		%split CIF into gen & non-gen
	fillmissing2(Non_gen,Quantified,Default_quantifier,Non_gen_filled),
	make_quantification(Default_quantifier,Quantified,Gens,Non_gen_filled,Filled).

%
% all other CIF
%
fillmissing(Cif,_,_,Cif).



%
% scan through a list & fill individual elements
%
fillmissing2([],_,_,[]).
fillmissing2([Ng|Ngs],Quantified,Default_quantifier,[Ng_filled|Ngs_filled]) :-
	fillmissing(Ng,Quantified,Default_quantifier,Ng_filled),
	fillmissing2(Ngs,Quantified,Default_quantifier,Ngs_filled).

%
% make (nested) quantification for a list of generators
%
make_quantification(_,_,[],Body,Body).				%end of gen

%
% generator of var already quantified
%
make_quantification(Quantifier,Quantified,Gens,Body,Filled) :-
	Gens=[G|_],						%get 1st gen from list
	(	G=generate(Class,Var);				%match var & class
		G=generate(_,_,_,Class,Var)
	),
	member(Var,Quantified),					%var is already quantified, no need for extra quantification
	!,
	Patterns=[generate(_,Var),generate(_,_,_,_,Var)],	%make pattern
	match_pattern(Gens,Patterns,This_gen,Not_this_gen),	%extract all gen on this var
	append_cif(This_gen,Body,New_body),			%these gens will appear in body of quantification
	make_quantification(Quantifier,Quantified,Not_this_gen,New_body,Filled).

%
% generator of var that needs quantification
%
make_quantification(Quantifier,Quantified,Gens,Body,Filled) :-
	Gens=[G|_],						%get 1st gen
	(	G=generate(Class,Var);				%match var
		G=generate(_,_,_,Class,Var)			%which is not yet quantified
	),
	Patterns=[generate(_,Var),generate(_,_,_,_,Var)],	%make pattern for match gen of this var
	match_pattern(Gens,Patterns,This_gen,Not_this_gen),	%find all gen on this var
	Filled=restrict_subquery(Q,This_gen,P),			%quantification for this var
	Q=..[Quantifier,Var],					%using the default quantifier
	my_union(Var,Quantified,New_quantified),		%1 more var quantified
	make_quantification(Quantifier,New_quantified,Not_this_gen,Body,P).

%
% make nested quantification for the generator part of a quantified constraint
%
% This is a list of generate/2 & generate/5 in the G of a quantified constraint.
% We scan through the list and pick up each variable being quantified.
% For each var, we put in a quantification.
%

%
% 1 gen only
%
make_quantification_for_gen(Quantifier,Quantified,[Gen],Non_gen,P_filled,More_quantified,Filled) :-
	(	Gen=generate(_,Var);			%pick up var
		Gen=generate(_,_,_,_,Var)
	),
	!,
	append_cif(Gen,Non_gen,G),			%concat the only generator w/ condition
	Filled=restrict_subquery(Q,G,P_filled),		%the final quantified constraint
	Q=..[Quantifier,Var],				%construct quantification
	my_union(Var,Quantified,More_quantified).

%
% a list of gen
%
make_quantification_for_gen(Quantifier,Quantified,Gens,Non_gen,P_filled,Final_quantified,Filled) :-
	Gens=[G|_],						%get 1st generator
	(	G=generate(_,Var);				%pick up var
		G=generate(_,_,_,_,Var)
	),
	!,
	Patterns=[generate(_,Var),generate(_,_,_,_,Var)],	%make up pattern
	match_pattern(Gens,Patterns,This_gen,Not_this_gen),	%pick up generator of this var
	Q=..[Quantifier,Var],					%construct quantification
	Filled=restrict_subquery(Q,This_gen,This_p),
	my_union(Var,Quantified,More_quantified),		%1 more var quantified
	make_quantification_for_gen(Quantifier,More_quantified,Not_this_gen,Non_gen,P_filled,Final_quantified,This_p).


