% Les termes des systemes de reecriture de Presburger : f(c1,..ci).
% pg.pl

:- use_module(library(lists)).

%:- [compilateur_pg].
%:- [writeclauseS].

phrase_pg(Phrase,Axiome,Compteurs) :-
	But=..[Axiome,Phrase|Compteurs],
	call(But).
	


sigma_pg(pg(_Axiome,Definis,Grammaire),Stream) :-
	set_output(Stream),
	assert(definis(Definis)),
	psi(Grammaire,[],Code),
	retract(definis(Definis)),
	writepaquetS(Code).

% compilateur_pg.pl

%:- [maps].
%:- [gestion_clauses].
%:- [sigma].
:- op(1200,xfx,'->').

psi([],PaquetS,PaquetS).
psi([ReglePresburger|RegleS],PaquetS,NPaquetS) :-
	ReglePresburger=[RegleBase,RegleInductive],
	sigma_Base(RegleBase,ClauseBase),
	sigma_Inductive(RegleInductive,ClauseInductive),
	ajoute_une_clause_dans_paquets(ClauseInductive,PaquetS,IPaquetS),
	ajoute_une_clause_dans_paquets(ClauseBase,IPaquetS,IIPaquetS),
	psi(RegleS,IIPaquetS,NPaquetS).

sigma_V(NewVar,[NewVar|Dico],Dico).


% gestion_clauses.pl

ajoute_une_clause_dans_paquets(Clause,[],[paquet(SymbolePredicat,[Clause])]) :-
	Clause=(Tete :- _),
	functor(Tete, SymbolePredicat,_).
ajoute_une_clause_dans_paquets(Clause,[paquet(SymbolePredicat,ClauseS) | PaquetS], [paquet(SymbolePredicat,[Clause|ClauseS])|PaquetS]) :-
	Clause = (Tete :- _),
	functor(Tete, SymbolePredicat,_), !.
ajoute_une_clause_dans_paquets(Clause,[Paquet|PaquetS],[Paquet|NPaquetS]) :-
	ajoute_une_clause_dans_paquets(Clause,PaquetS,NPaquetS).

writeclauseS([]).
writeclauseS([Clause|ClauseS]) :-
	portray_clause(Clause),
	writeclauseS(ClauseS).

writepaquetS([]).
writepaquetS([paquet(_,ClauseS)|PaquetS]) :-
	writeclauseS(ClauseS),
	writepaquetS(PaquetS).



% emballage
emballage(Redex,VarFoncteurDefini, Dico, Dico, FoncteurDefini, VarFoncteurDefini) :- 
	Redex=..[FoncteurDefini|_], !.
emballage(Redex,NewVar, Dico, [NewVar|Dico],_FoncteurDefini,_VarFoncteurDefini) :-
	redex(Redex).
emballage(Atome,Atome,Dico,Dico,_FoncteurDefini,_VarFoncteurDefini) :-
	atom(Atome).
emballage(Terme,NewTerme,DicoIn,DicoOut,FoncteurDefini,VarFoncteurDefini) :-
	compound(Terme),
	Terme =.. [Foncteur|Args],
	emballage_rec(Args,NewArgs,DicoIn,DicoOut,FoncteurDefini,VarFoncteurDefini),
	NewTerme =.. [Foncteur|NewArgs].

emballage_rec([],[],Dico,Dico,_FoncteurDefini,_VarFoncteurDefini).
emballage_rec([Arg|Args],[NewArg|NewArgs],DicoIn,DicoOut,FoncteurDefini,VarFoncteurDefini) :-
	emballage_rec(Args,NewArgs,DicoIn,DicoInter,FoncteurDefini,VarFoncteurDefini),
	emballage(Arg,NewArg,DicoInter,DicoOut,FoncteurDefini,VarFoncteurDefini).

compteur2var([],[],Dico,Dico).
compteur2var([s(Compteur)|Compteurs],[VarCompteur|VarCompteurs],DicoIn,[(VarCompteur,Compteur)|DicoOut]) :- !,
	compteur2var(Compteurs,VarCompteurs,DicoIn,DicoOut).
compteur2var([Compteur|Compteurs],[VarCompteur|VarCompteurs],DicoIn,[(VarCompteur,Compteur)|DicoOut]) :-
	compteur2var(Compteurs,VarCompteurs,DicoIn,DicoOut).

redex(Terme) :-
	definis(Definis),
	Terme=..[Foncteur|_],
	member(Foncteur,Definis).


% S1<S2
soussuite([],_,[]).
soussuite([A|S1],[(Var,A)|S2],[Var|Vars]) :-
	soussuite(S1,S2,Vars).
soussuite([s(A)|S1],[(Var,A)|S2],[s(Var)|Vars]) :-
	soussuite(S1,S2,Vars).
soussuite(S1,[_|S2],Vars) :-
	soussuite(S1,S2,Vars).


sigma_Base((Mg->Md),(Tete :- Corps)) :-
	sigma_Base_Mg(Mg,Md,Tete,DicoVar,DicoCompteurs),
	sigma_Base_Md(Md,Corps,DicoVar,DicoCompteurs).

sigma_Inductive((Mg->Md),(Tete :- Corps)) :-
	sigma_Inductive_Mg(Mg,Md,Tete,DicoVar,DicoCompteurs,Defini,VarDefini),
	sigma_Inductive_Md(Md,Corps,DicoVar,DicoCompteurs,Defini,VarDefini).

sigma_Base_Mg(MgB,R1,Tete,DicoVar,DicoCompteurs) :-
	MgB=..[Defini,0|Compteurs],
	compteur2var(Compteurs,VarCompteurs,[],DicoCompteurs),
	emballage(R1,TermeR1,[],DicoVar,Defini,_),
	Tete=..[Defini,TermeR1,0|VarCompteurs].

sigma_Base_Md(Terme,Corps,DicoVar,DicoCompteurs) :-
	sigma_Base_Md(Terme,true,Corps,DicoVar,[],DicoCompteurs).

sigma_Base_Md(Terme,Corps,(Corps,But), DicoVarIn,DicoVarOut,DicoCompteurs) :-
	Terme=..[Defini|Compteurs],
	definis(Definis), member(Defini,Definis),
	sigma_V(VarTerme,DicoVarIn,DicoVarOut),
	soussuite(Compteurs,DicoCompteurs,VarCompteurs),
	But=..[Defini,VarTerme|VarCompteurs].

sigma_Base_Md(Atome,Corps,Corps,DicoVar,DicoVar,_DicoCompteurs) :-
	atom(Atome).
sigma_Base_Md(Terme,CorpsIn,CorpsOut,DicoVarIn,DicoVarOut,DicoCompteurs) :-
	compound(Terme),
	Terme =.. [NonDefini|Args],
	definis(Definis), \+ member(NonDefini,Definis),
	sigma_Base_Md_rec(Args,CorpsIn,CorpsOut,DicoVarIn,DicoVarOut,DicoCompteurs).

sigma_Base_Md_rec([],Corps,Corps,DicoVar,DicoVar,_DicoCompteurs).
sigma_Base_Md_rec([Arg|Args], CorpsIn, CorpsOut,DicoVarIn, DicoVarOut, DicoCompteurs) :-
	sigma_Base_Md(Arg,CorpsIn,CorpsInter,DicoVarIn,DicoVarInter,DicoCompteurs),
	sigma_Base_Md_rec(Args,CorpsInter,CorpsOut,DicoVarInter,DicoVarOut,DicoCompteurs).

sigma_Inductive_Mg(MgI,R2,Tete,DicoVar,DicoCompteurs,Defini,VarDefini) :-
	MgI=..[Defini,s(CompteurPrincipal)|Compteurs],
	compteur2var([CompteurPrincipal|Compteurs],[VarCompteurPrincipal|VarCompteurs],[],DicoCompteurs),
	emballage(R2,TermeR2,[],DicoVar,Defini,VarDefini),
	Tete=..[Defini,TermeR2,s(VarCompteurPrincipal)|VarCompteurs].


sigma_Inductive_Md(Terme,Corps,DicoVar,DicoCompteurs,FoncteurDefini,VarFoncteurDefini) :-
	sigma_Inductive_Md(Terme,true,Corps,DicoVar,[],DicoCompteurs,FoncteurDefini,VarFoncteurDefini,_Itere).

sigma_Inductive_Md(Terme,Corps,(Corps,But), DicoVar,DicoVar,DicoCompteurs,FoncteurDefini,VarFoncteurDefini,Itere) :-
	compound(Terme),
	Terme=..[FoncteurDefini|Compteurs],
	var(Itere),
	Itere= ok,
	soussuite(Compteurs,DicoCompteurs,VarCompteurs),
	But=..[FoncteurDefini,VarFoncteurDefini|VarCompteurs].

sigma_Inductive_Md(Terme,Corps,Corps, DicoVar,DicoVar,_DicoCompteurs,FoncteurDefini,_VarFoncteurDefini,Itere) :-
	compound(Terme),
	Terme=..[FoncteurDefini|_Compteurs],
	nonvar(Itere).

sigma_Inductive_Md(Terme,Corps,(Corps,But), DicoVarIn,DicoVarOut,DicoCompteurs,FoncteurDefini,_VarFoncteurDefini,_Itere) :-
	compound(Terme),
	Terme=..[UnDefini|Compteurs],
	 \+ UnDefini = FoncteurDefini,
	definis(Definis), member(UnDefini,Definis),
	sigma_V(VarTerme,DicoVarIn,DicoVarOut),
	soussuite(Compteurs,DicoCompteurs,VarCompteurs),
	But=..[UnDefini,VarTerme|VarCompteurs].

sigma_Inductive_Md(Atome,Corps,Corps,DicoVar,DicoVar,_DicoCompteurs,_FoncteurDefini,_VarFoncteurDefini,_Itere) :-
	atom(Atome).
sigma_Inductive_Md(Terme,CorpsIn,CorpsOut,DicoVarIn,DicoVarOut,DicoCompteurs,FoncteurDefini,VarFoncteurDefini,Itere) :-
	compound(Terme),
	Terme =.. [NonDefini|Args],
	definis(Definis), \+ member(NonDefini,Definis),
	sigma_Inductive_Md_rec(Args,CorpsIn,CorpsOut,DicoVarIn,DicoVarOut,DicoCompteurs,FoncteurDefini,VarFoncteurDefini,Itere).

sigma_Inductive_Md_rec([],Corps,Corps,DicoVar,DicoVar,_DicoCompteurs,_FoncteurDefini,_VarFoncteurDefini,_Itere).
sigma_Inductive_Md_rec([Arg|Args], CorpsIn, CorpsOut,DicoVarIn, DicoVarOut, DicoCompteurs,FoncteurDefini,VarFoncteurDefini,Itere) :-
	sigma_Inductive_Md(Arg,CorpsIn,CorpsInter,DicoVarIn,DicoVarInter,DicoCompteurs,FoncteurDefini,VarFoncteurDefini,Itere),
	sigma_Inductive_Md_rec(Args,CorpsInter,CorpsOut,DicoVarInter,DicoVarOut,DicoCompteurs,FoncteurDefini,VarFoncteurDefini,Itere).
