%% Copyright (C) 2012 Igor Stéphan
%% 
%% This program is free software; you can redistribute it and/or
%% modify it under the terms of the GNU General Public License
%% as published by the Free Software Foundation; either version 2
%% of the License, or (at your option) any later version.
%% 
%% This program is distributed in the hope that it will be useful,
%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%% GNU General Public License for more details.
%% 
%% You should have received a copy of the GNU General Public License
%% along with this program; if not, write to the Free Software
%% Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
%% http:%%www.gnu.org/copyleft/gpl.html
%%
%% igor.stephan@univ-angers.fr
%% 
:- module('RECURSIVE_COMPILATION', [recursive_compilation/3]).
:- use_module('QCSP_BASE', [combine_e/4, combine_a/3]).
:- use_module(library(lists)).
:- use_module(library(clpfd)).
% symboles de predicat
%  recursive_compilation  : Liste(_) x Clp x Base_Litterale
%  insatisfiable : Base_Litterale

% bltop, blbottom : Bl
% bl : Liste(Vlva) -> Bl
% vlva : Var x Liste(Va) -> Vlva
% va : Val x Arbre_Etiquete -> Va
% (_,_) : Val x Arbre_Etiquete
% top, bottom : Arbre_Etiquete 
 
%% recursive_compilation : Liste(Quant)  x Csp x Bl
recursive_compilation(Quant, Contraintes, Base) :-
	recursive_compilation(Quant, Quant, Contraintes, Base).

%% recursive_compilation : Liste(Quant) x Liste(Quant)  x Csp x Bl
recursive_compilation([],[], Contraintes, bltop) :-
	call(Contraintes), !.

recursive_compilation([e(Xinit, _) | VariablesInit], [e(X,D_X) | Variables], Contraintes, Base) :-
	\+(\+(call(Contraintes))),
	e_map_recursive_compilation(D_X,X, VariablesInit, Variables, Contraintes, Bases),
	(
	  Bases = []
	->
	  Base = blbottom
	;
	  combine_e(Xinit, D_X, Bases, Base)
	),
	!.

recursive_compilation([a(Xinit, _) | VariablesInit], [a(X,D_X) | Variables], Contraintes, Base) :-
	\+(\+(call(Contraintes))),
	a_map_recursive_compilation(D_X,X, VariablesInit, Variables, Contraintes, Bases),
	combine_a(Xinit, Bases, Base),
	!.

recursive_compilation(_, _, _Contraintes, blbottom).
	

%% e_map_recursive_compilation : Liste(Val) x Var x Liste(Quant) x Liste(Quant) x Csp x Liste(Bl)
e_map_recursive_compilation([], _X, _VariablesInit, _Variables, _Contraintes, []).
e_map_recursive_compilation([Val | D_X], X, VariablesInit, Variables, Contraintes, Bases):-
	copy_term((Variables, X, Contraintes), (Variables_Val, Val, Contraintes_Val)),
	recursive_compilation(VariablesInit, Variables_Val, Contraintes_Val, Base_Val),
	e_map_recursive_compilation(D_X, X, VariablesInit, Variables, Contraintes, Bases_),
 	(
 	  Base_Val = blbottom
 	->
 	  Bases = Bases_
 	;
	  Bases = [(Val, Base_Val) | Bases_]
	).


%% a_map_recursive_compilation : Liste(Val) x Var x Liste(Quant) x Liste(Quant) x Csp x Liste(Bl)
a_map_recursive_compilation([], _X, _VariablesInit, _Variables, _Contraintes, []).
a_map_recursive_compilation([Val | D_X], X, VariablesInit, Variables, Contraintes, [(Val, Base_Val) | Bases]):-
	copy_term((Variables, X, Contraintes), (Variables_Val, Val, Contraintes_Val)),
	recursive_compilation(VariablesInit, Variables_Val, Contraintes_Val, Base_Val),
	\+ (Base_Val = blbottom),
	a_map_recursive_compilation(D_X, X, VariablesInit, Variables, Contraintes, Bases).