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

:- use_module(library(lists)).

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

phrase_pg(Phrase,Axiome,Compteurs,Stream) :-
	set_output(Stream),
	But=..[Axiome,Phrase,(Mot,Mot,flux([],_))|Compteurs],
	call(But).
	
sigma_pg(pg(_Axiome,Definis,Grammaire),Stream) :-
	set_output(Stream),
	assert(definis(Definis)),
	format("%- op(1200,xfx,'->').~n",[]),
	format("%- [outils_trace].~n",[]),
%	format("phrase_pg(Phrase,Axiome) :-~n",[]),
%	format("~t Axiome=.. AxiomeDecompose,~n",[]),
%	format("~t AxiomeDecompose = [~a|Compteurs],~n",[Axiome]),
%	format("~t name(FileName,\"~s\"),~n",[NomStreamTrace]),
%	format("~t open(FileName,write,Stream),~n",[]),
%	format("~t set_output(Stream),~n",[]),
%	format("~t format(\"~~p~~n\",[Axiome]),~n",[]),
%	format("~t But =.. [~a,Phrase,(Mot,Mot,flux([],_))|Compteurs],~n",[Axiome]),
%	format("~t call(But),~n",[]),
%	format(" close(Stream).~n~n",[]),
	psi(Grammaire,flux([],Code)),
	retract(definis(Definis)),
	writepaquetS(Code).

% compilateur_pg.pl

%:- [gestion_clauses].
%:- [sigma_pg.pl]
:- op(1200,xfx,'->').

psi([],Paquets) :-
	connect_flux(Paquets).
psi([ReglePresburger|RegleS],Paquets) :-
	transmet_flux([PaquetsBase,PaquetsInductif,PaquetsPsi],Paquets),
	ReglePresburger=[RegleBase,RegleInductive],
	sigma_Base(RegleBase,ClauseBase),
	sigma_Inductive(RegleInductive,ClauseInductive),
	ajoute_une_clause_dans_paquets(ClauseInductive,PaquetsBase),
	ajoute_une_clause_dans_paquets(ClauseBase,PaquetsInductif),
	psi(RegleS,PaquetsPsi).


% gestion_clauses.pl

ajoute_une_clause_dans_paquets(Clause,flux(Paquets,NPaquets)) :-
	ajoute_une_clause_dans_paquets(Clause,Paquets,NPaquets).
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.pl
writeclauseS([]).
writeclauseS([Clause|ClauseS]) :-
	portray_clause(Clause),
	writeclauseS(ClauseS).

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


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

emballage_rec([],[],FluxDicoVar,_FoncteurDefini,_VarFoncteurDefini) :-
	connect_flux(FluxDicoVar).
emballage_rec([Arg|Args],[NewArg|NewArgs],FluxDicoVar,FoncteurDefini,VarFoncteurDefini) :-
	transmet_flux(FluxDicoVarArgs,FluxDicoVarArg,FluxDicoVar),
	emballage_rec(Args,NewArgs,FluxDicoVarArgs,FoncteurDefini,VarFoncteurDefini),
	emballage(Arg,NewArg,FluxDicoVarArg,FoncteurDefini,VarFoncteurDefini).

compteur2var([],[],FluxDicoCompteurs) :-
	connect_flux(FluxDicoCompteurs).
compteur2var([s(Compteur)|Compteurs],[VarCompteur|VarCompteurs],FluxDicoCompteurs) :- !,
	ajoute_flux((VarCompteur,Compteur),FluxDicoCompteurs,FluxDicoCompteurs_Rec),
	compteur2var(Compteurs,VarCompteurs,FluxDicoCompteurs_Rec).
compteur2var([Compteur|Compteurs],[VarCompteur|VarCompteurs],FluxDicoCompteurs) :-
	ajoute_flux((VarCompteur,Compteur),FluxDicoCompteurs,FluxDicoCompteurs_Rec),
	compteur2var(Compteurs,VarCompteurs,FluxDicoCompteurs_Rec).

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_pg.pl

%:- [emballage].
%:- [flux].
sigma_V(NewVar,[NewVar|Dico],Dico).


sigma_Base((Mg->Md),(Tete :- imprime(NDicoCibleE,Mot),  Corps)) :-
	sigma_Base_Mg(Mg,Md,Tete,DicoVar,DicoCompteurs,(Mot,TraceMd,flux(DicoCibleE,DicoCibleS))),
	sigma_Base_Md(Md,Corps,DicoVar,DicoCompteurs,(Mot,TraceMd,flux(NDicoCibleE,DicoCibleS),flux([],DicoVarTrace))),
	append(DicoVarTrace,DicoCibleE,NDicoCibleE).

sigma_Inductive((Mg->Md),(Tete :- imprime(NDicoCibleE,Mot),  Corps)) :-
	sigma_Inductive_Mg(Mg,Md,Tete,DicoVar,DicoCompteurs,Defini,VarDefini,(Mot,TraceMd,flux(DicoCibleE,DicoCibleS))),
	sigma_Inductive_Md(Md,Corps,DicoVar,DicoCompteurs,Defini,VarDefini,(Mot,TraceMd,flux(NDicoCibleE,DicoCibleS),flux([],DicoVarTrace))),
	append(DicoVarTrace,DicoCibleE,NDicoCibleE).

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

sigma_Base_Md(Terme,Corps,DicoVar,DicoCompteurs,(Mot,TraceCorps,FluxDicoCible,FluxDicoVarTrace)) :-
	sigma_Base_Md(Terme,true,Corps,flux([],DicoVar),DicoCompteurs,(Mot,TraceCorps,FluxDicoCible,FluxDicoVarTrace)).

sigma_Base_Md(Terme,Corps,(Corps,But), FluxDicoVar,DicoCompteurs, (Mot,VarTrace,FluxDicoCible,FluxDicoVarTrace)) :-
	Terme=..[Defini|Compteurs],
	definis(Definis), member(Defini,Definis),
	ajoute_flux(VarTerme,FluxDicoVar),
	soussuite(Compteurs,DicoCompteurs,VarCompteurs),
	But=..[Defini,VarTerme,(Mot,VarTrace,FluxDicoCible)|VarCompteurs],
	ajoute_flux((VarTrace,Defini),FluxDicoVarTrace).

sigma_Base_Md(Atome,Corps,Corps,FluxDicoVar,_DicoCompteurs,(_,Atome,FluxDicoCible,FluxDicoVarTrace)) :-
	atom(Atome),
	connect_flux(FluxDicoVar),
	connect_flux(FluxDicoCible),
	connect_flux(FluxDicoVarTrace).
sigma_Base_Md(Terme,CorpsIn,CorpsOut,FluxDicoVar,DicoCompteurs,(Mot,TraceT,FluxDicoCible,FluxDicoVarTrace)) :-
	compound(Terme),
	Terme =.. [NonDefini|Args],
	definis(Definis), \+ member(NonDefini,Definis),
	sigma_Base_Md_rec(Args,CorpsIn,CorpsOut,FluxDicoVar,DicoCompteurs,(Mot,TraceArgs,FluxDicoCible,FluxDicoVarTrace)),
	TraceT=.. [NonDefini|TraceArgs].

sigma_Base_Md_rec([],Corps,Corps,FluxDicoVar,_DicoCompteurs, (_Mot,[],FluxDicoCible,FluxDicoVarTrace)) :-
	connect_flux(FluxDicoVar),
	connect_flux(FluxDicoVarTrace),
	connect_flux(FluxDicoCible).
sigma_Base_Md_rec([Arg|Args], CorpsIn, CorpsOut,FluxDicoVar, DicoCompteurs, (Mot,[TraceT|TraceArgs],FluxDicoCible,FluxDicoVarTrace)) :-
	transmet_flux(FluxDicoVarArg,FluxDicoVarArgs,FluxDicoVar),
	transmet_flux(FluxDicoVarTraceArg,FluxDicoVarTraceArgs,FluxDicoVarTrace),
	transmet_flux(FluxDicoCibleArg,FluxDicoCibleArgs,FluxDicoCible),
	sigma_Base_Md(Arg,CorpsIn,CorpsInter,FluxDicoVarArg,DicoCompteurs, (Mot,TraceT,FluxDicoCibleArg,FluxDicoVarTraceArg)),
	sigma_Base_Md_rec(Args,CorpsInter,CorpsOut,FluxDicoVarArgs,DicoCompteurs, (Mot,TraceArgs,FluxDicoCibleArgs,FluxDicoVarTraceArgs)).

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


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

sigma_Inductive_Md(Terme,Corps,(Corps,But), FluxDicoVar,DicoCompteurs,FoncteurDefini,VarFoncteurDefini,Itere, (Mot,VarTrace,FluxDicoCible,FluxDicoVarTrace)) :-
	compound(Terme),
	Terme=..[FoncteurDefini|Compteurs],
	var(Itere),
	Itere= ok,
	soussuite(Compteurs,DicoCompteurs,VarCompteurs),
	But=..[FoncteurDefini,VarFoncteurDefini,(Mot,VarTrace,FluxDicoCible)|VarCompteurs],
	ajoute_flux((VarTrace,FoncteurDefini),FluxDicoVarTrace),
	connect_flux(FluxDicoVar).

sigma_Inductive_Md(Terme,Corps,Corps, FluxDicoVar,_DicoCompteurs,FoncteurDefini,_VarFoncteurDefini,Itere, (_Mot,VarTrace,FluxDicoCible,FluxDicoVarTrace)) :-
	compound(Terme),
	Terme=..[FoncteurDefini|_Compteurs],
	nonvar(Itere),
	membre_flux((VarTrace,FoncteurDefini), FluxDicoVarTrace),
	connect_flux(FluxDicoCible),
	connect_flux(FluxDicoVar).

sigma_Inductive_Md(Terme,Corps,(Corps,But), FluxDicoVar,DicoCompteurs,FoncteurDefini,_VarFoncteurDefini,_Itere, (Mot,VarTrace,FluxDicoCible,FluxDicoVarTrace)) :-
	compound(Terme),
	Terme=..[UnDefini|Compteurs],
	 \+ UnDefini = FoncteurDefini,
	definis(Definis), member(UnDefini,Definis),
	ajoute_flux(VarTerme,FluxDicoVar),
	soussuite(Compteurs,DicoCompteurs,VarCompteurs),
	But=..[UnDefini,VarTerme,(Mot,VarTrace,FluxDicoCible)|VarCompteurs],
	ajoute_flux((VarTrace,UnDefini),FluxDicoVarTrace).

sigma_Inductive_Md(Atome,Corps,Corps,FluxDicoVar,_DicoCompteurs,_FoncteurDefini,_VarFoncteurDefini,_Itere,(_,Atome,FluxDicoCible,FluxDicoVarTrace)) :-
	atom(Atome),
	connect_flux(FluxDicoVar),
	connect_flux(FluxDicoCible),
	connect_flux(FluxDicoVarTrace).
sigma_Inductive_Md(Terme,CorpsIn,CorpsOut,FluxDicoVar,DicoCompteurs,FoncteurDefini,VarFoncteurDefini,Itere,(Mot,TraceT,FluxDicoCible,FluxDicoVarTrace)) :-
	compound(Terme),
	Terme =.. [NonDefini|Args],
	definis(Definis), \+ member(NonDefini,Definis),
	sigma_Inductive_Md_rec(Args,CorpsIn,CorpsOut,FluxDicoVar,DicoCompteurs,FoncteurDefini,VarFoncteurDefini,Itere,(Mot,TraceArgs,FluxDicoCible,FluxDicoVarTrace)),
	TraceT=.. [NonDefini|TraceArgs].

sigma_Inductive_Md_rec([],Corps,Corps,FluxDicoVar,_DicoCompteurs,_FoncteurDefini,_VarFoncteurDefini,_Itere, (_Mot,[],FluxDicoCible,FluxDicoVarTrace)) :-
	connect_flux(FluxDicoVar),
	connect_flux(FluxDicoCible),
	connect_flux(FluxDicoVarTrace).
sigma_Inductive_Md_rec([Arg|Args], CorpsIn, CorpsOut,FluxDicoVar, DicoCompteurs,FoncteurDefini,VarFoncteurDefini,Itere, (Mot,[TraceT|TraceArgs],FluxDicoCible,FluxDicoVarTrace)) :-
	transmet_flux(FluxDicoVarArg,FluxDicoVarArgs,FluxDicoVar),
	transmet_flux(FluxDicoVarTraceArg,FluxDicoVarTraceArgs,FluxDicoVarTrace),
	transmet_flux(FluxDicoCibleArg,FluxDicoCibleArgs,FluxDicoCible),
	sigma_Inductive_Md(Arg,CorpsIn,CorpsInter,FluxDicoVarArg,DicoCompteurs,FoncteurDefini,VarFoncteurDefini,Itere, (Mot,TraceT,FluxDicoCibleArg,FluxDicoVarTraceArg)),
	sigma_Inductive_Md_rec(Args,CorpsInter,CorpsOut,FluxDicoVarArgs,DicoCompteurs,FoncteurDefini,VarFoncteurDefini,Itere, (Mot,TraceArgs,FluxDicoCibleArgs,FluxDicoVarTraceArgs)).

% outils_trace.pl

unifie([]).
unifie([(V,T)|L]) :-
	var(V),
	V=T,
	unifie(L).
unifie([(V,_T)|L]) :-
	nonvar(V),
	unifie(L).

imprime(L,Mot) :-
	\+(\+((unifie(L),print(Mot),nl))).

% flux.pl

ajoute_flux(X,flux(F,[X|F])).
ajoute_flux(X,flux(E,[X|S]),flux(E,S)).
connect_flux(flux(L,L)).
transmet_flux(flux(E,I),flux(I,S),flux(E,S)).
transmet_flux([flux(E,I)|Flux_Intermediaires],flux(E,S)) :-
	transmet_flux_rec(I,Flux_Intermediaires,S).
transmet_flux_rec(S,[],S).
transmet_flux_rec(E,[flux(E,I)|Flux_Intermediaires],S) :-
	transmet_flux_rec(I,Flux_Intermediaires,S).
membre_flux(X,flux(F,F)) :-
	member(X,F).

