:- module(cif_util,[	find_var_types/2,			%find all vars in CIF with types
			extract_var_with_type/2,
			find_vars/2,				%find all vars in CIF
			replace_var_in_cif/3,			%replace vars in CIF
			initialize_counter/1,			%create & init a counter from 1
			initialize_counter/2,			%init counter from a certain no.
			clear_counter/1,			%remove a counter
			generate_counter/2,			%get counter value & increment it
			generate_counter/3,			%get counter value w/ prefix
			generate_daplex_variable/1,		%generate a daplex var
			generate_daplex_variable/2,		%generate a daplex var w/ prefix
			reset_daplex_counter/0,
			is_skolem/1,				%check for skolem constant/function
			is_skolem_constant/1,
			is_skolem_function/1,
			find_generator/3,
			extract_generator/4,
			create_template/3,			%create template from CIF
			append_cif/2,				%append a list of CIFs together
			append_cif/3,				%append 2 CIFs together
			minus_cif/3,				%minus 1 CIF from another
			my_union/2,
			my_union/3,
			my_append/2,
			my_append/3,
			my_subtract/3,
			refresh_vars/2,				%refresh all var names
%			fill_in_implicit_generator/2,		%fill in implicit generators
			my_intersect/5,				%find intersection of 2 lists
			my_subset/2,				%test for subset
			cif_about_var/4,
			filter_generator/2,
			filter_generate2/3,
			xx_fill_implicit/2,
			negate_cif/2,				%negate a CIF
			filter_basic_types_generate/2,		%filter generate/2 of basic types
			match_pattern/4				%match CIF against a list of patterns/templates
		]).

:- [prolog_detect].
:- prolog_detect:prolog(Prolog),
	(	(Prolog=pfdm,
		use_module(library(lists))
		);
		(Prolog=sicstus,
		use_module(library(lists))
		);
		Prolog=eclipse;
		Prolog=swi;
		(	write('*** ERROR: Unsupported Prolog system ***'),
			fail
		)
	).
:- [is_daplex_variable].

:- dynamic(counter/2).



%---------------------
% find all vars in CIF
%---------------------

find_vars(Cif,Vars) :-
	find_var_types(Cif,[],Types),
	findall(X,member(X:_,Types),Vars).


%---------------------------------------
% given a CIF construct or a list of CIF
% find all vars w/ types
%---------------------------------------
find_var_types(Cif,Types) :-
	find_var_types(Cif,[],Types).			%start with an empty list of types

%
% end of CIF list
%
find_var_types([],Bindings,Bindings) :-
	!.

%
% cater for group/2
%
find_var_types(Group,Old_bindings,New_bindings) :-
	Group=group(_,Cif),
	!,
	find_var_types(Cif,Old_bindings,New_bindings).

%
% and a list of group/2
%
find_var_types([group(_,Cif)|Rest],Old_bindings,New_bindings) :-
	!,							%avoid group/2 to be retried as other patterns
	find_var_types(Cif,Old_bindings,Temp_bindings),
	find_var_types(Rest,Temp_bindings,New_bindings).


%
% run through list of CIF
%
find_var_types([P|Ps],Old_bindings,New_bindings) :-
	!,
	extract_var_with_type(P,Vars_with_type),			%find var w/ types in a construct
	add_var_with_type(Vars_with_type,Old_bindings,Temp_bindings),	%combine with existing one
	find_var_types(Ps,Temp_bindings,New_bindings).			%proceed with the rest

%
% a single CIF construct
%
find_var_types(Cif,Old_bindings,Bindings) :-
	extract_var_with_type(Cif,Vars_with_type),			%find var w/ types in a construct
	add_var_with_type(Vars_with_type,Old_bindings,Bindings).		%combine with existing one



%
% given a construct, find all vars w/ type info
%

%
% generate/2
%
extract_var_with_type(P,Filtered) :-
	P=generate(Class,Var),
	!,
	Vars_with_type=[Var:Class],
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% generate/3
%
extract_var_with_type(P,Filtered) :-
	P=generate(Class,_,Var),
	!,
	Vars_with_type=[Var:Class],
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% generate/5
%
extract_var_with_type(P,Filtered) :-
	P=generate(_,Arg_types,Args,Class,Var),		%a function call
	!,
	findall(X,(	nth0(N,Arg_types,Type),		%find list of args w/ type
			nth0(N,Args,Arg),
			X=Arg:Type
			),
		Args_with_type),
	Vars_with_type=[Var:Class|Args_with_type],	%the overall list
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% restrict/4
%
% *** Note: restrict/4 is removed in CIF
%
extract_var_with_type(P,Filtered) :-
	P=restrict(_,Arg_types,Args,Var),
	!,
	write('*** WARNING: restrict/4 is removed in CIF'),
	findall(X,(	nth0(N,Arg_types,Type),		%find list of args w/ type
			nth0(N,Args,Arg),
			X=Arg:Type
			),
		Args_with_type),
	Vars_with_type=[Var:_|Args_with_type],		%the overall list, Var has an unknown type
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% relative/3
%
extract_var_with_type(P,Filtered) :-
	P=relative(Class,Instance,Var),
	!,
	Vars_with_type=[Instance:_,Var:Class],
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% expression/3
%
extract_var_with_type(P,Filtered) :-
	P=expression(Gen,Req,Pattern),
	!,
	findall(X,(	member(V,[Gen|Req]),
			X=V:_
			),
		Bindings_1),
	extract_var_with_type(Pattern,Bindings_2),
	append(Bindings_1,Bindings_2,Vars_with_type),
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% expr/1
%
extract_var_with_type(P,Filtered) :-
	P=expr(Var),
	!,
	Vars_with_type=[Var:_],
	filter_non_daplex_var(Vars_with_type,Filtered).


%
% expr/3 w/ op '='
%
extract_var_with_type(P,Filtered) :-
	P=expr(=,V1,V2),
	!,
	Vars_with_type=[V1:Class,V2:Class],
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% expr/3 w/ other operators
%
extract_var_with_type(P,Filtered) :-
	P=expr(_,V1,V2),
	!,
	Vars_with_type=[V1:_,V2:_],
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% int_set/3
%
extract_var_with_type(P,Filtered) :-
	P=int_set(_,_,Var),
	!,
	Vars_with_type=[Var:integer],
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% expression/4
%
extract_var_with_type(P,Filtered) :-
	P=expression(Gen,Req,_,Set),
	!,
	findall(X,(	member(V,[Gen|Req]),
			X=V:_
			),
		Bindings_1),
	find_var_types(Set,Bindings_2),			%find vars in the set-code
	append(Bindings_1,Bindings_2,Vars_with_type),	%join them together
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% restrict_subquery/3
%
extract_var_with_type(P,Filtered) :-
	P=restrict_subquery(Quantifier,Set_cif,Pred_cif),
	!,
	(	(	Quantifier =.. [Functor,Var],
			member(Functor,[all,some,no])
		);
		(	Quantifier =.. [Functor,Var,Num],
			integer(Num),
			member(Functor,[least,most,exactly])
		)
	),
	(	(	is_list(Var),			%if Var is a list
			!,
			findall(Wanted,(member(V,Var),	%then create a list of var:_
					Wanted=V:_),
				Bindings_1)
		);
		(	Bindings_1=[Var:_]		%otherwise just a single var
		)
	),
	find_var_types(Set_cif,Bindings_2),
	find_var_types(Pred_cif,Bindings_3),
	append(Bindings_1,Bindings_2,Temp),
	append(Temp,Bindings_3,Vars_with_type),
	filter_non_daplex_var(Vars_with_type,Filtered).

/*
extract_var_with_type(P,Filtered) :-
	P=restrict_subquery(Quantifier,Set_cif,Pred_cif),
	!,
	(	(	Quantifier =.. [Functor,Var],
			member(Functor,[all,some,no]),
			Bindings_1=[Var:_]
		);
		(	Quantifier =.. [Functor,Var,Num],
			integer(Num),
			member(Functor,[least,most,exactly]),
			Bindings_1=[Var:_]
		)
	),
	find_var_types(Set_cif,Bindings_2),
	find_var_types(Pred_cif,Bindings_3),
	append(Bindings_1,Bindings_2,Temp),
	append(Temp,Bindings_3,Vars_with_type),
	filter_non_daplex_var(Vars_with_type,Filtered).
*/

%
% generate_subquery/5
%
extract_var_with_type(P,Filtered) :-
	P=generate_subquery(Type,Var,Sub,Aux1,Aux2),
	!,
	Bindings_1=[Var:Type],
	find_var_types(Sub,Bindings_sq),
	find_var_types(Aux1,Bindings_a1),
	find_var_types(Aux2,Bindings_a2),
	flatten([Bindings_1,Bindings_sq,Bindings_a1,Bindings_a2],Vars_with_type),
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% the/1
%
extract_var_with_type(P,Filtered) :-
	P=the(Code),
	!,
	find_var_types(Code,Vars_with_type),
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% any/3
%
extract_var_with_type(P,Filtered) :-
	P=any(Card,Set,Var),
	!,
	find_var_types(Card,Bindings_1),
	find_var_types(Set,Bindings_2),
	flatten([[Var:_],Bindings_1,Bindings_2],Vars_with_type),
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% set/2
%
extract_var_with_type(P,Filtered) :-
	P=set(Var,Set),
	!,
	find_var_types(Set,Bindings_1),
	Vars_with_type=[Var:_|Bindings_1],
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% logical_or/2 or logical_and/2
%
extract_var_with_type(P,Filtered) :-
	(	P=logical_or(Lhs,Rhs);
		P=logical_and(Lhs,Rhs)
	),
	!,
	find_var_types(Lhs,Bindings_1),
	find_var_types(Rhs,Bindings_2),
	append(Bindings_1,Bindings_2,Vars_with_type),
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% logical_or/1 or logical_and/1 (extended CIF)
%
extract_var_with_type(P,Filtered) :-
	(	P=logical_or(Cifs);
		P=logical_and(Cifs)
	),
	!,
	find_var_types(Cifs,Filtered).



%
% logical_not/1
%
extract_var_with_type(P,Filtered) :-
	P=logical_not(Code),
	!,
	find_var_types(Code,Vars_with_type),
	filter_non_daplex_var(Vars_with_type,Filtered).

%
% all other patterns
%
extract_var_with_type(P,Vars) :-
%	format("WARNING: non-Icode construct->~q~n",[P]),
	P =.. [_|Args],
	findall(X:_,(	X=var(_),
			member(X,Args)
		),
		Vars).

/*
extract_var_with_type(_,[]).
*/


%
% add a var:class pair (or a list of pairs)
% into the var:class binding list
% avoiding duplicate
%
% NOTE:	a var can have multiple types because of class hierachy
%	in this case, the type is a list
%

%
% a list of pairs
%
add_var_with_type([],Old,Old) :-
	!.				%end of to add list

add_var_with_type([B|Bs],Old,New) :-
	!,
	add_var_with_type(B,Old,Temp),	%add 1st one
	add_var_with_type(Bs,Temp,New).	%then the rest

%
% a single pair
%
add_var_with_type(Var:Class,Old,Old) :-
	member(Var:Class,Old),		%var w/ class already in list
	!.				%ok

add_var_with_type(Var:Class,Old,Old) :-
	member(Var:Classes,Old),	%class already in list of classes
	member(Class,Classes),
	!.

add_var_with_type(Var:Class,Old,New) :-
	member(Var:Current_class,Old),			%var in list
	!,
	delete(Old,Var:Current_class,Temp),		%take it out
	my_union(Class,Current_class,New_classes),	%add the new class
	my_union(Var:New_classes,Temp,New).		%put it back in
%
% NOTE:	in the past it fails, now it doesn't
%
%	fail.						%but class doesn't match

add_var_with_type(Var:Class,Old,New) :-
	New=[Var:Class|Old],				%var not in list, put it in
	!.


%
% given a list of variable replacement in the form From:To
% replace variables in a CIF
%
replace_var_in_cif([],Cif,Cif) :-				%no replacement at all
	!.

replace_var_in_cif(Replacements,Old_cif,New_cif) :-
	is_list(Old_cif),					%if CIF is a list
	!,
	replace_var_in_list(Replacements,Old_cif,New_cif).	%proceed with list

replace_var_in_cif(Replacements,Old_cif,New_cif) :-
	replace_var_in_list(Replacements,[Old_cif],[New_cif]).	%CIF is not a list, just a construct


replace_var_in_list(_,[],[]).					%end of CIF list

replace_var_in_list(Replacements,[From|Rest],[To|New_rest]) :-
	member(From:To,Replacements),				%1st element is in replacement list
	!,
	replace_var_in_list(Replacements,Rest,New_rest).	%proceed with the rest

replace_var_in_list(Replacements,[Head|Rest],[New_head|New_rest]) :-
	is_list(Head),						%1st element is a list
	!,
	replace_var_in_cif(Replacements,Head,New_head),		%recursively work on 1st element
	replace_var_in_list(Replacements,Rest,New_rest).	%and rest of list

replace_var_in_list(Replacements,[Head|Rest],[Head|New_rest]) :-
	functor(Head,_,0),					%1st element is an atom
	!,
	replace_var_in_list(Replacements,Rest,New_rest).	%proceed with list

replace_var_in_list(Replacements,[Term|Rest],[New_term|New_rest]) :-
	Term =.. List,						%1st element is a term
	replace_var_in_list(Replacements,List,New_list),	%work on all arguments
	New_term =.. New_list,
	!,
	replace_var_in_list(Replacements,Rest,New_rest).	%proceed with list


%
% in a X:Type binding list,
% filter out those non-Daplex variables
%

filter_non_daplex_var([],[]).

filter_non_daplex_var([X:Type|Rest],[X:Type|Filtered_rest]) :-
	var(X),
	!,
	filter_non_daplex_var(Rest,Filtered_rest).

filter_non_daplex_var([X:Type|Rest],[X:Type|Filtered_rest]) :-
	is_daplex_variable:is_daplex_variable(X),
	!,
	filter_non_daplex_var(Rest,Filtered_rest).

filter_non_daplex_var([X:Type|Rest],[X:Type|Filtered_rest]) :-
	is_skolem(X),
	!,
	filter_non_daplex_var(Rest,Filtered_rest).

filter_non_daplex_var([_|Rest],Filtered_rest) :-
	filter_non_daplex_var(Rest,Filtered_rest).


%
% general purpose counter management
%

initialize_counter(Counter) :-
	retractall(counter(Counter,_)),			%retract existing value
	!,
	asserta(counter(Counter,1)).			%and set it to 1

initialize_counter(Counter) :-
	asserta(counter(Counter,1)).			%if no current value exists, just set it

initialize_counter(Counter,Count) :-
	retractall(counter(Counter,_)),			%retract existing value
	!,
	asserta(counter(Counter,Count)).		%and set it to the value specified

initalize_count(Counter,Count) :-
	asserta(counter(Counter,Count)).		%if no current value exists

%
% remove a counter
%
clear_counter(Counter) :-
	retractall(counter(Counter,_)).


%
% generate_counter/3
%
% like generate_counter/2 but with a prefix
%
generate_counter(Counter,Prefix,Final) :-
	generate_counter(Counter,Count),
	name(Prefix,Prefix_in_string),
	name(Count,Count_in_string),
	append(Prefix_in_string,Count_in_string,Final_in_string),
	name(Final,Final_in_string).

%
% get the value of a counter and advances it
%
generate_counter(Counter,Count) :-
	retract(counter(Counter,Count)),		%retract old one
	!,
	Next is Count+1,				%increment it
	asserta(counter(Counter,Next)).			%and save for next use

generate_counter(Counter,Count) :-
	initialize_counter(Counter),			%no value exist, just create a new one
	generate_counter(Counter,Count).		%and get value


%
% generate_daplex_variable/3
%
% like generate_daplex_variable/1 but w/ prefix
%
generate_daplex_variable(Prefix,X) :-
	generate_counter(daplex,Prefix,Count),
	X=var(Count).

%
% generate a Daplex variable
%
generate_daplex_variable(X) :-
	generate_counter(daplex,Count),			%get counter for daplex
	X=var(Count).

reset_daplex_counter :-
	initialize_counter(daplex).			%initialize it


%
% check for skolem/constant/function
%
is_skolem(X) :-
	is_skolem_constant(X).

is_skolem(X) :-
	is_skolem_function(X).

is_skolem_constant(skolem(_)).
is_skolem_function(skolem(_,_)).



%
% create a CIF template by replacing all Daplex
% variables by Prolog variables
%
create_template(Cif,Template,Replacements) :-
	find_var_types(Cif,Vtypes),
	findall(X,(	member(Var:_,Vtypes),
			X=Var:_),
		Replacements),
	replace_var_in_cif(Replacements,Cif,Template),
	!.


%----------------------------------------------
% find_generator/3
%
% given a list of generators, find the relevant
% one for a particular variable
%
%----------------------------------------------
find_generator(_,[],[]).

find_generator(Var,[C|Cs],[C|Gens]) :-
	C=generate(_,Var),
	find_generator(Var,Cs,Gens).

find_generator(Var,[C|Cs],[C|Gens]) :-
	C=generate(_,_,_,_,Var),
	find_generator(Var,Cs,Gens).

%
% cater for a list of vars
%
find_generator(Vars,[C|Cs],[C|Gens]) :-
	C=generate(_,V),
	member(V,Vars),
	find_generator(Vars,Cs,Gens).

find_generator(Vars,[C|Cs],[C|Gens]) :-
	C=generate(_,_,_,_,V),
	member(V,Vars),
	find_generator(Vars,Cs,Gens).

find_generator(Vars,[_|Cs],Gens) :-
	find_generator(Vars,Cs,Gens).


%
% find generator but also remove them from original list
%

extract_generator(_,[],[],[]).				%end of input list

extract_generator(Var,[C|Cs],Gen,Leftover) :-
	C=generate(_,Var),				%var matches generator/2
	extract_generator(Var,Cs,G,Leftover),
	!,
	(	(	member(C,G),
			Gen=G
		);
		Gen=[C|G]
	).

extract_generator(Var,[C|Cs],Gen,Leftover) :-
	C=generate(_,_,_,_,Var),
	extract_generator(Var,Cs,G,Leftover),
	!,
	(	(	member(C,G),
			Gen=G
		);
		Gen=[C|G]
	).

extract_generator(Vars,[C|Cs],Gen,Leftover) :-
	C=generate(_,V),				%var matches generator/2
	member(V,Vars),
	extract_generator(Vars,Cs,G,Leftover),
	!,
	(	(	member(C,G),
			Gen=G
		);
		Gen=[C|G]
	).

extract_generator(Vars,[C|Cs],Gen,Leftover) :-
	C=generate(_,_,_,_,V),
	member(V,Vars),
	extract_generator(Vars,Cs,G,Leftover),
	!,
	(	(	member(C,G),
			Gen=G
		);
		Gen=[C|G]
	).

extract_generator(Var,[C|Cs],Gen,[C|Leftover]) :-	%C doesn't match, it's a leftover
	extract_generator(Var,Cs,Gen,Leftover).


%
% append_cif/2
%
% append a list of CIF together
%
% append_cif(+List,-Cif)
%
% List	=	list of CIF to be appended together
% Cif	=	the appended CIF
%
append_cif([],[]).

append_cif([C|Cs],Cif) :-
	append_cif(Cs,Temp),
	append_cif(C,Temp,Cif).

%--------------------------------
% append 2 cif/construct together
%--------------------------------

append_cif(C1,C2,Cif) :-
	my_union(C1,C2,Cif).


%
% my_union/2
%
% take a union of multiple sets
%
% my_union(+Sets,-Union)
%
% Sets	=	the list of sets
% Union	=	the union of all sets
%

my_union([],[]).

my_union([S|Ss],U) :-
	my_union(Ss,Temp),
	my_union(S,Temp,U).


%----------------------------------------------
% a union/3 that works with list/single element
%----------------------------------------------

my_union(X,Y,Z) :-
	is_list(X),
	is_list(Y),
	!,
	my_union2(X,Y,Z).
my_union(X,Y,Z) :-
	is_list(Y),
	!,
	my_union2([X],Y,Z).
my_union(X,Y,Z) :-
	is_list(X),
	!,
	my_union2(X,[Y],Z).
my_union(X,Y,Z) :-
	my_union2([X],[Y],Z).


my_union2([],L,L).
my_union2([H|T],L,Result) :-
	my_union2(T,L,Temp),			%proceed w/ tail 1st
	(	(	member(H,Temp),		%if H is already in temp result
			!,
			Result=Temp		%then ommit H
		);
		(	Result=[H|Temp]		%otherwise keep H
		)
	).


%
% my_append/2
%
my_append([],[]).
my_append([X|Xs],Appended) :-
	my_append(Xs,Temp),
	my_append(X,Temp,Appended).


%
% my_append/3
%
my_append(X,Y,Z) :-
	is_list(X),
	is_list(Y),
	!,
	append(X,Y,Z).

my_append(X,Y,Z) :-
	is_list(X),
	!,
	append(X,[Y],Z).

my_append(X,Y,Z) :-
	is_list(Y),
	!,
	append([X],Y,Z).

my_append(X,Y,Z) :-
	append(X,Y,Z).



my_subtract([],_,[]).

my_subtract([C|Cs],Cif,Left) :-
	member(C,Cif),
	!,
	my_subtract(Cs,Cif,Left).

my_subtract([C|Cs],Cif,[C|Left]) :-
	my_subtract(Cs,Cif,Left).



%-----------------------------------
% minus the 2nd CIF from the 1st CIF
%-----------------------------------
minus_cif(A,B,C) :-
	my_subtract(A,B,C).

/*
minus_cif([],[],[]).

minus_cif([C|Cs],Cif,Left) :-
	member(C,Cif),
	!,
	minus_cif(Cs,Cif,Left).

minus_cif([C|Cs],Cif,[C|Left]) :-
	minus_cif(Cs,Cif,Left).
*/

%
% change all variable names
%
refresh_vars(Cif,Refreshed) :-
	find_var_types(Cif,Types),
	findall(X,	(	member(Old_name:_,Types),
				generate_daplex_variable(New_name),
				X=Old_name:New_name
			),
		Replacement),
	replace_var_in_cif(Replacement,Cif,Refreshed).



%------------------------------------------------------
% fill in implicit generators at the appropriate places
%------------------------------------------------------
/*
%
% fill_implicit/2
%

fill_implicit(Cif,Filled) :-
	find_var_types(Cif,Types),			%find all var types
	fill_implicit(Cif,Types,Filled).		%then start


%
% fill_implicit/3
% the main predicate for filling in implicit generators
%

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

fill_implicit([C|Cs],Types,Filled) :-
	!,
	fill_implicit(C,Types,F),			%work on every element in the list
	fill_implicit(Cs,Types,Fs),
	append_cif(F,Fs,Filled).


fill_implicit(C,Types,Filled) :-
	find_and_fill_implicit(C,Types,New_c,Needed),
	generate_implicit(Needed,Gens),
	append_cif(New_c,Gens,Filled).

%
% if you have a list, just summarize their "needs"
%
find_and_fill_implicit([],_,[],[]) :-
	!.

find_and_fill_implicit([C|Cs],Types,New,Needed) :-
	!,
	find_and_fill_implicit(C,Types,New_c,C_needed),
	find_and_fill_implicit(Cs,Types,New_cs,Cs_needed),
	append_cif(New_c,New_cs,New),
	my_union(C_needed,Cs_needed,Needed).



%
% generate/2
%
% no change & no need
%
find_and_fill_implicit(C,Types,C,[]) :-
	C=generate(Class,Var),
	member(Var:Class,Types),
	!.

find_and_fill_implicit(C,_,C,[]) :-
	C=generate(_,_),
	format("WARNING: find_and_fill_implicit/4 generate/2 unmatch var-type~n",[]).

%
% generate/5
%
% no change to C but has a need
%
find_and_fill_implicit(C,Types,C,[Var:Class]) :-
	C=generate(_,_,_,Class,Var),
	member(Var:Class,Types),
	!.

find_and_fill_implicit(C,_,C,[]) :-
	C=generate(_,_,_,_,_),
	!,
	format("WARNING: find_and_fill_implicit/4 generate/5 unmatch var-type~n",[]).

%
% restrict_subquery/3
%
% may change G & P but no need
%
find_and_fill_implicit(C,Types,Filled,[]) :-
	C=restrict_subquery(Q,G,P),
	!,
	find_and_fill_implicit(G,Types,New_g,G_needed),
	find_and_fill_implicit(P,Types,New_p,P_needed),
	generate_implicit(G_needed,G_gens),
	generate_implicit(P_needed,P_gens),
	append_cif(New_g,G_gens,Temp_g),
	append_cif(Temp_g,P_gens,Final_g),
	Filled=restrict_subquery(Q,Final_g,New_p).

%
% all others
%
find_and_fill_implicit(C,Types,Filled,Needed) :-
	C =.. [Functor|Args],
	find_and_fill_implicit(Args,Types,Filled_args,Needed),
	Filled =.. [Functor|Filled_args].


%----------------------------------------------------
% given a list of Var:Type, generate those generate/2
%----------------------------------------------------

generate_implicit([],[]).

generate_implicit([Var:Type|Rest],[generate(Type,Var)|Gs]) :-
	generate_implicit(Rest,Gs).

*/



%------------------------------------------
% scan a CIF and fill in missing generate/2
%------------------------------------------

xx_fill_implicit(Cif,Filled) :-
	find_var_types(Cif,Types),		%find all var w/ types
	xx_fill_implicit(Cif,Types,Filled).	%call the real predicate

%
% CIF as a list
%
xx_fill_implicit([],_,[]).			%end of list

xx_fill_implicit([C|Cs],Types,Filled) :-
	xx_fill_implicit(C,Types,F),		%work on head
	xx_fill_implicit(Cs,Types,Fs),		%then tail
	append_cif(F,Fs,Filled).		%concate them together


%
% different CIF construct
%

%
% restrict_subquery/3 w/ ALL
%
xx_fill_implicit(C,Types,Filled) :-
	C=restrict_subquery(all(Vs),G,P),				%restrict_subquery/3 w/ ALL
	!,
	xx_fill_implicit_subtree_only(G,Types,G_filled,G_missing),	%recursive fill P but leave out top level
	xx_fill_implicit_subtree_only(P,Types,P_filled,P_missing),	%recursive fill P but leave out top level
	append_cif(G_missing,P_missing,Missing),			%sum up all missing generators
	append_cif(Missing,G_filled,New_g),				%add into G to give New_g
	findall(X,member(generate(_,X),Missing),Extra_vars),		%find all new vars
	my_union(Vs,Extra_vars,New_vs),					%put into quantifier
	Filled=restrict_subquery(all(New_vs),New_g,P_filled).

/*
xx_fill_implicit(C,Types,Filled) :-
	C=restrict_subquery(some(Vs),G,P),
	!,
	xx_fill_implicit_subtree_only(G,Types,G_filled,G_missing),	%recursive fill P but leave out top level
	xx_fill_implicit_subtree_only(P,Types,P_filled,P_missing),	%recursive fill P but leave out top level
	append_cif(G_missing,P_missing,Missing),			%sum up all missing generators
	append_cif(Missing,G_filled,New_g),				%add into G to give New_g
	findall(X,member(generate(_,X),Missing),Extra_vars),		%find all new vars
	my_union(Vs,Extra_vars,New_vs),					%put into quantifier
	Filled=restrict_subquery(all(New_vs),New_g,P_filled).
*/


%
% generate/2
%
xx_fill_implicit(C,Types,C) :-
	C=generate(Class,Var),				%generate/2
	member(Var:Class,Types),			%found in var-type list
	!.

xx_fill_implicit(C,_,C) :-
	C=generate(_,_),						%generate/2
	!,
	format("WARNING: ~q doesn not match var-type list~n",[C]).	%trap error

%
% generate/5
%
xx_fill_implicit(C,Types,Filled) :-
	C=generate(_,_,_,Class,Var),			%generate/5
	member(Var:Class,Types),			%found in var-type list
	!,
	Filled=[generate(Class,Var),C].			%this could be the missing type

xx_fill_implicit(C,_,C) :-
	C=generate(_,_,_,_,_),						%generate/5
	!,
	format("WARNING: ~q doesn not match var-type list~n",[C]).	%trap error

%
% all other term w/ arity 0
%
xx_fill_implicit(C,_,C) :-
	functor(C,_,0),
	!.

%
% all other constructs
%
xx_fill_implicit(C,Types,Filled) :-
	C =.. [F|Args],
	!,
	xx_fill_implicit(Args,Types,Filled_args),		%recursively work on all args
	Filled =.. [F|Filled_args].



%
% fill a CIF but excluding the top level
%
xx_fill_implicit_subtree_only([],_,[],[]).

xx_fill_implicit_subtree_only([C|Cs],Types,[F|Fs],Missing) :-
	xx_fill_implicit_subtree_only(C,Types,F,M),		%work on head
	xx_fill_implicit_subtree_only(Cs,Types,Fs,Ms),		%and tail
	append_cif(M,Ms,Missing).				%summarise missing gens, but don't fill

%
% different constructs
%

%
% generate/2
%
xx_fill_implicit_subtree_only(C,Types,C,[]) :-
	C=generate(Class,Var),				%generate/2
	member(Var:Class,Types),			%found in var-type list
	!.

xx_fill_implicit_subtree_only(C,_,C,[]) :-
	C=generate(_,_),						%generate/2
	!,
	format("WARNING: ~q doesn not match var-type list~n",[C]).	%trap error

%
% generate/5
%
xx_fill_implicit_subtree_only(C,Types,C,Missing) :-
	C=generate(_,_,_,Class,Var),			%generate/5
	member(Var:Class,Types),			%consistent type in var-type list
	!,
	Missing=[generate(Class,Var)].

xx_fill_implicit_subtree_only(C,_,C,[]) :-
	C=generate(_,_,_,_,_),						%generate/5
	!,
	format("WARNING: ~q doesn not match var-type list~n",[C]).	%trap error


%
% restrict_subquery/3
%
xx_fill_implicit_subtree_only(C,Types,Filled,[]) :-
	C=restrict_subquery(_,_,_),			%restrict_subquery/3
	!,
	xx_fill_implicit(C,Types,Filled).		%just fill it up

%
% all other terms w/ arity 0
%
xx_fill_implicit_subtree_only(C,_,C,[]) :-
	functor(C,_,0),
	!.

%
% all other constructs
%
xx_fill_implicit_subtree_only(C,Types,Filled,[]) :-
	C =.. [F|Args],
	!,
	xx_fill_implicit(Args,Types,Filled_args),	%just fill it up
	Filled =.. [F|Filled_args].


/*

%
% fill_in_implicit_generator(Cif,Filled)
%
% Cif		=	CIF to be filled
% Filled	=	the filled version
%

fill_in_implicit_generator(Cif,Filled) :-
	find_var_types(Cif,Types),				%find all vars w/ types
	fill_in_implicit_generator(Cif,Types,Filled).		%fill in missing generators



%
% CIF as a list
%
fill_in_implicit_generator([],_,[]) :-
	!.

fill_in_implicit_generator(Cif,Types,Filled) :-
	find_implicit_generator(Cif,Types,Missing),		%find missing gen
	append_cif(Missing,Cif,Filled).				%put them in



fill_in_implicit_generator([C|Cs],Types,Filled) :-
	fill_in_implicit_generator(C,Types,Filled_c),		%handle the head
	fill_in_implicit_generator(Cs,Types,Filled_cs),		%then the tail
	append_cif(Filled_c,Filled_cs,Filled),			%append them together
	!.

%
% find all implicit generators in a CIF list
%
find_implicit_generator([],_,[]).			%end of list

find_implicit_generator([C|Cs],Types,Missing) :-
	find_implicit_generator(C,Types,M),		%work on head
	find_implicit_generator(Cs,Types,Ms),		%then tail
	append_cif(M,Ms,Missing).			%concate them together

%
% different constructs
%

%
% generate/2
%
find_implicit_generator(C,Types,[]) :-
	C=generate(Class,Var),				%generate/2
	member(Var:Class,Types),			%consistent type in var-type list
	!.

find_implicit_generator(C,_,[]) :-
	C=generate(_,_),				%generate/2 with inconsistent type
	!,
	format("WARNING: generate/2 does not match var-type in list.~n",[]).

%
% generate/5
%
find_implicit_generator(C,Types,Missing) :-
	C=generate(_,_,_,Class,Var),			%generate/5
	member(Var:Class,Types),			%consistent type in var-type list
	!,
	Missing=generate(Class,Var).			%this could be the missing type

find_implicit_generator(C,_,[]) :-
	C=generate(_,_,_,_,_),				%generate/5
	!,
	format("WARNING: generate/5 does not match var-type list.~n",[]).

%
% restrict_subquery/3
%
find_implicit_generator(C,Types,Missing) :-
	C=restrict_subquery(_,G,P),
	!,
	find_implicit_generator(G,Types,G_missing),		%work on G
	find_implicit_generator(P,Types,P_missing),		%work on P
	append_cif(G_missing,P_missing,Missing).

%
% term of arity 0 (prevent an empty list from looping)
%
find_implicit_generator(C,_,[]) :-
	functor(C,_,0),
	!.

%
% all other constructs
%
find_implicit_generator(C,Types,Missing) :-
	C =.. [_|Args],
	find_implicit_generator(Args,Types,Missing),
	!.



%
% handling individual CIF construct
%

%
% generate/2
%
fill_in_implicit_generator(C,Types,C) :-
	C=generate(Class,Var),
	member(Var:Class,Types),		%appear in the var-type list
	!.

fill_in_implicit_generator(C,_,C) :-
	C=generate(_,_),
	format("WARNING: generate/2 does not match var-type list.~n",[]),	%cannot find it in var-type list
	!.

%
% generate/5
%
fill_in_implicit_generator(C,Types,Filled) :-
	C=generate(_,_,_,Class,Var),				%a generate/5
	member(Var:Class,Types),				%find it in the var-type list
	!,
	Filled=[generate(Class,Var),C].				%fill int the missing generate/2

fill_in_implicit_generator(C,_,C) :-
	C=generate(_,_,_,_,_),					%a generate/5
	format("WARNING: generate/5 does not match var-type list.~n",[]),
	!.

%
% restrict_subquery/3
%
fill_in_implicit_generator(C,Types,Filled) :-
	C=restrict_subquery(Q,G,P),
	fill_in_implicit_generator(G,Types,Filled_g),			%recursively work on G
	fill_in_implicit_generator(P,Types,Filled_p),			%and P
	Filled=restrict_subquery(Q,Filled_g,Filled_p).


fill_in_implicit_generator(C,_,C) :-
	functor(C,_,0),
	!.

%
% all other term
%
fill_in_implicit_generator(C,Types,Filled) :-
	C =.. [F|Args],
	fill_in_implicit_generator_in_args(Args,Types,Filled_args),
	Filled =.. [F|Filled_args],
	!.

fill_in_implicit_generator_in_args([],_,[]).
fill_in_implicit_generator_in_args([A|As],Types,[F|Fs]) :-
	fill_in_implicit_generator(A,Types,F),
	fill_in_implicit_generator_in_args(As,Types,Fs).
*/



%
% my_intersect(List1,List2,L1_left,Match,L2_left)
%
% List1=	1st list
% List2=	2nd list
% L1_left=	remain part of L1
% Match=	matching part of the 2 lists
% L2_left=	remain part of L2
%
% match 2 lists against each other
% return the overlapping & non-overlapping part in both lists
%
my_intersect([],L,[],[],L) :-				%end of 1st list
	!.

my_intersect(L,[],L,[],[]) :-				%end of 2nd list
	!.

my_intersect([T|Ts],C,Left,[T|Match],Right) :-
	member(T,C),					%T matches something in C
	delete(C,T,C_rest),				%find the rest of C
	my_intersect(Ts,C_rest,Left,Match,Right).	%carry on

my_intersect([T|Ts],C,[T|Left],Match,Right) :-
	not(member(T,C)),
	my_intersect(Ts,C,Left,Match,Right).		%T doesn't match anything in C


%
% see if A is a subset of B
%
my_subset(A,B) :-
	my_intersect(A,B,[],_,_).			%when A & B intersects, nothing left in A








%
% cif_about_var/4
%
% split a CIF into 2 parts
%
% similar to cif_with_var/4 but take care of the
% chain-reaction-like relationship among vars
%
% 1st, we scan through the CIF and mark related vars in groups
% then we split the CIF into 2 parts accordingly
%
cif_about_var(Var,Cif,About,Remain) :-
	is_daplex_variable:is_daplex_variable(Var),				%Var is a single daplex var
	!,
	cif_about_var([Var],Cif,About,Remain).

cif_about_var(Vars,Cif,About,Remain) :-
	find_related_vars(Vars,Cif,Related_vars),	%find all related vars
	cif_with_var(Related_vars,Cif,About,Remain).	%then use cif_with_var/4

%
% given a var/list of vars and a CIF
% find the list of related vars
%
find_related_vars(Var,Cif,Related_vars) :-
	build_vars_relationship(Cif,Relationship),	%build relationship among vars
	mark_vars_relationship(Var,Relationship),	%now mark those related to vars we want
	find_related_vars(Relationship,Related_vars).


find_related_vars([],[]).

find_related_vars([_:Status|Rest],Related) :-
	var(Status),
	!,
	find_related_vars(Rest,Related).

find_related_vars([Var:related|Rest],[Var|Related]) :-
	!,
	find_related_vars(Rest,Related).

find_related_vars([_:_|Rest],Related) :-
	format("WARNING: unexpected value of var status in find_related_vars/2~n",[]),
	find_related_vars(Rest,Related).


%
% scan through the list of vars and mark those related
%
mark_vars_relationship(Var,Relationship) :-
	is_daplex_variable:is_daplex_variable(Var),			%a single var
	member(Var:Status,Relationship),	%that appears in the relationship list
	!,
	Status=related.				%now they are related

mark_vars_relationship(Var,_) :-
	is_daplex_variable:is_daplex_variable(Var),			%a single var
	!.					%not found in the list, just forget it

mark_vars_relationship([],_).			%end of var list

mark_vars_relationship([V|Vs],Relationship) :-
	member(V:related,Relationship),		%a list of var, and it is found in the relationship list
	!,
	mark_vars_relationship(Vs,Relationship).

mark_vars_relationship([_|Vs],Relationship) :-
	mark_vars_relationship(Vs,Relationship).	%1st var not found, just proceed


%
% build up relationship among vars
%
build_vars_relationship(Cif,Relationship) :-
	build_vars_relationship(Cif,[],Relationship).

%
% for a list
%
build_vars_relationship([],Old,Old) :-			%end of CIF
	!.

build_vars_relationship([C|Cs],Old,New) :-
	!,
	build_vars_relationship(C,Old,Temp),		%work on the head
	build_vars_relationship(Cs,Temp,New).		%then proceed w/ the tail

%
% for an individual construct
%
build_vars_relationship(C,Old,New) :-
	get_vars_in_construct(C,Vars_in_c),		%find all vars in C
	build_common_relationship(Vars_in_c,_,Common),
%	Goal=(Relation=X:_Status,member(X,Vars_in_c)),	%they are all related
%	findall(Relation,call(Goal),Relationships),	%now they share the same relationship status
	my_union(Old,Common,New).		%more relationships added

build_common_relationship([],_,[]).
build_common_relationship([V|Vs],Status,[V:Status|Rest]) :-
	build_common_relationship(Vs,Status,Rest).




%
% find all vars in a construct
%
get_vars_in_construct(C,Vars) :-
	find_vars(C,Vars).				%we can use the more general find_vars/2 to do it









%
% cif_with_var/4
%
% split a CIF into 2 parts
%
% cif_with_var(+Vars,+Cif,-About,-Remain)
%
% Vars		=	list of Daplex vars
% Cif		=	the CIF to split
% About		=	the subset in 'Cif' that deals w/ vars directly
% Remain	=	the remaining 'Cif' which doesn't deal with vars directly
%
%

%
% with CIF is a list
%

cif_with_var(_,[],[],[]).				%end of CIF

%
% C is a Daplex variable
%
cif_with_var(Var,[C|Cs],About,Remain) :-
	(	Var=C;					%C is a daplex var
		member(C,Var)				%OR Var is a list w/ C in there
	),
	!,
	cif_with_var(Var,Cs,As,Remain),			%proceed w/ tail
	About=[C|As].

%
% C is a construct/term
%
cif_with_var(Var,[C|Cs],About,Remain) :-
	C =.. [_|Args],					%get args
	(	(	is_daplex_variable:is_daplex_variable(Var),		%Var is a Daplex var
			member(Var,Args)		%and is 1 of the args
		);
		(	member(X,Var),			%1 var in the list of Var
			member(X,Args)			%is 1 of the args
		);
		(	member(A,Args),			%or a 1 of the args is a term
			\+(A=[]),
			(	cif_with_var(Var,A,[_|_],_);	%which is concerning Var
				cif_with_var(Var,A,A,_)	%which is concerning Var
			)
		)
	),
	!,
	cif_with_var(Var,Cs,As,Remain),			%continue w/ the rest of the CIF list
	About=[C|As].

cif_with_var(Var,[C|Cs],About,[C|Remain]) :-
	!,
	cif_with_var(Var,Cs,About,Remain).		%nothing about var in C, continue w/ the list

%
% when CIF is a construct
%
cif_with_var(Var,Cif,Cif,[]) :-
	is_daplex_variable:is_daplex_variable(Cif),				%Cif is a Daplex var
	!,
	(	Var=Cif;				%which is equal to Var
		member(Cif,Var)				%or 1 of Var
	).

cif_with_var(Var,Cif,Cif,[]) :-
	Cif =.. [_|Args],				%get args
	(	(	is_daplex_variable:is_daplex_variable(Var),		%Var is a Daplex var
			member(Var,Args)		%and is 1 of the args
		);
		(	member(X,Var),			%1 var in the Var list
			is_daplex_variable:is_daplex_variable(X),		%is a Daplex var
			member(X,Args)			%which is 1 of the args
		);
		(	member(A,Args),			%an arg
			(	cif_with_var(Var,A,[_|_],_);	%is involved w/ Var
				cif_with_var(Var,A,A,_)	%is involved w/ Var
			)
		)
	).




%
% filter out any generator
%
filter_generator([],[]).
filter_generator([C|Cs],Filtered) :-
	functor(C,generate,2),
	!,
	filter_generator(Cs,Filtered).

filter_generator([C|Cs],[C|Filtered]) :-
	filter_generator(Cs,Filtered).


%
% filter out generate/2
%
filter_generate2([],[],[]).

filter_generate2([C|Cs],[C|Gs],Left) :-
	C=generate(_,_),
	!,
	filter_generate2(Cs,Gs,Left).

filter_generate2([C|Cs],Gs,[C|Left]) :-
	filter_generate2(Cs,Gs,Left).

%
% negate_cif/2
%
% given a CIF, return the negated version
%
% negate_cif(+Cif,-Negated)
%
% Cif		=	the original CIF
% Negated	=	the negated version
%

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

%
% cater for a list of CIF
%
negate_cif([C|Cs],[N|Ns]) :-
	!,
	negate_cif(C,N),
	negate_cif(Cs,Ns).

%
% cater for different CIF construct
%
negate_cif(icode_true,icode_false).

negate_cif(icode_false,icode_true).

negate_cif(C,N) :-
	C=expr(Op,Lhs,Rhs),
	!,
	Ops=[=,<,=<,>,>=,<>],
	Negated_ops=[<>,>=,>,=<,<,=],
	nth0(Index,Ops,Op),
	nth0(Index,Negated_ops,Negated_op),
	N=expr(Negated_op,Lhs,Rhs).

negate_cif(C,N) :-
	C=restrict_subquery(some(Vs),G,P),
	!,
	negate_cif(P,Negated_p),
	N=restrict_subquery(all(Vs),G,Negated_p).

negate_cif(C,N) :-
	C=expression(X,Y,Expr),
	!,
	negate_cif(Expr,Negated_expr),
	N=expression(X,Y,Negated_expr).

negate_cif(C,N) :-
	C=logical_not(N),
	!.

negate_cif(C,N) :-
	C=restrict_subquery(all(Vs),G,P),
	!,
	negate_cif(P,Negated_p),
	N=restrict_subquery(some(Vs),G,Negated_p).

%
% by default there is no negation
%
negate_cif(C,C).



filter_basic_types_generate([],[]).
filter_basic_types_generate([C|Cs],Fs) :-
	(	C=generate(integer,_);
		C=generate(string,_);
		C=generate(boolean,_);
		C=generate(float,_)
	),
	!,
	filter_basic_types_generate(Cs,Fs).
filter_basic_types_generate([C|Cs],[C_filtered|Fs]) :-
	C=restrict_subquery(Q,G,P),
	!,
	filter_basic_types_generate(G,G_filtered),
	filter_basic_types_generate(P,P_filtered),
	C_filtered=restrict_subquery(Q,G_filtered,P_filtered),
	filter_basic_types_generate(Cs,Fs).

filter_basic_types_generate([C|Cs],[C|Fs]) :-
	filter_basic_types_generate(Cs,Fs).


%
% split a list of CIF according to a list of patterns
%
match_pattern([],_,[],[]).

match_pattern(Cif,Patterns,Match,Not_match) :-
	is_list(Patterns),			%pattern is a list
	Goal=(	member(T,Patterns),
		member(T,Cif)
		),
	findall(T,call(Goal),Match),		%and there is at least 1 match
	!,
	my_subtract(Cif,Match,Not_match).

match_pattern(Cif,Patterns,[],Cif) :-
	is_list(Patterns),			%pattern is a list but NO match
	!.

match_pattern(Cif,Pattern,Match,Not_match) :-
	Goal=member(Pattern,Cif),		%pattern is NOT a list
	findall(Pattern,call(Goal),Match),	%and there is at least 1 match
	!,
	my_subtract(Cif,Match,Not_match).

match_pattern(Cif,_,[],Cif).		%pattern is NOT a list & there is NO match
