/* Fichier "norm.pl" version du 21/05/2011

/ Normalisation des relations arithmétiques binaires.
     Le terme gauche est toujours avant le terme droit dans l'ordre standard.
     Les comparaisons larges sont décomposées en strict ou égal.
    ?- normalise(>=(y, x), T). --> T = (x<y).
    ?- normalise(>(y, x), T).  --> T = ou(x<y, x=y).
/ */

:- use_module('mil_H.pl').
:- ensure_loaded('wang2.pl').

%--- Normalisation

normalise(C, N) :- ordonne(C, OC), azero(OC, OD), decompose(OD, N).

ordonne(C, C) :- C =.. [Rel, Tg, Td], Tg@=<Td, !.
ordonne(C, Oc) :- C =.. [Rel, Tg, Td], Tg@>Td, !, invRel(Rel, Rvl), Oc =.. [Rvl, Td, Tg].
ordonne(C, C). % cas des prédicats spécifiques P, Q, ...

azero(C, D) :- C =.. [Rel, 0, Td], member(Rel, ['=', '<', '>', '<=', '>=', '<>']), !, 
	spl0(Td, Dd), D =.. [Rel, 0, Dd].
azero(C, D) :- C =.. [Rel, Tg, Td], member(Rel, ['=', '<', '>', '<=', '>=', '<>']), !, 
	spl0(Td-Tg, Dd), D =.. [Rel, 0, Dd].
azero(C, C). % cas des prédicats spécifiques P, Q, ...

decompose(Tg<=Td, Tg<Td ou Tg=Td) :- !.
decompose(Tg>=Td, Tg>Td ou Tg=Td) :- !.
decompose(Tg<>Td, non Tg=Td) :- !.
decompose(C, C).

invRel(<, >).
invRel(>=, <=).
invRel(>, <).
invRel(<=, >=).
invRel(=, =).
invRel(<>, <>).

% simplification des produits et sommes avec 0
spl0(X+0, X):- !.
spl0(0+X, X):- !.
spl0(X*0, 0):- !.
spl0(0*X, 0):- !.
spl0(X-X, 0):- !.
spl0(X+Y-Y, Z):- !, spl0(X, Z).
spl0(X+Y-X, Z):- !, spl0(Y, Z).
spl0(A+B, X) :- spl0(A, C), spl0(B, D), spl0s(A+B, C+D, X), !. % cut indispensables, car
spl0(A-B, X) :- spl0(A, C), spl0(B, D), spl0s(A-B, C-D, X), !. % ...
spl0(A*B, X) :- spl0(A, C), spl0(B, D), spl0s(A*B, C*D, X), !. % la dernière clause est plus générale que les autres
spl0(X, X).

spl0s(X, X, X) :- !. % cut indispensable, la 2è clause étant plus générale que la 1ère
spl0s(X, Y, Z) :- spl0(Y, Z).

% reste à faire l'analyse de la structure logique (cut indispensables vu la dernière clause "attrape-tout"

normTop(X imp Y, XX imp YY) :- !, normTop(X, XX), normTop(Y, YY).
normTop(X ou Y, XX ou YY) :- !, normTop(X, XX), normTop(Y, YY).
normTop(X et Y, XX et YY) :- !, normTop(X, XX), normTop(Y, YY).
normTop(non Y, non YY) :- !, normTop(Y, YY).
normTop(T, T) :- T =.. [F | Args], estMaj(F), !. % cas des "prédicats spéciaux"
normTop(X, XX) :- normalise(X, XX).

estMaj(C) :- atom_length(C, 1), char_code(C, N), N>64, N<91.

%==============================================================================================================

%--- Simplification finale
% spll(LSeq, NLSeq)
% prend une liste de séquents LSeq et en élimine ceux dont le conséquent est VRAI, résultat NLSeq.
% Rappel : le conséquent est interprété comme la disjonction des termes qui le composent.
% Pour qu'il soit VRAI il suffit donc qu'il contienne un terme qui est VRAI 
% ou plusieurs termes complémentaires, i.e. dont la disjonction est VRAIe.

% On est donc conduit à donner au système une liste de termes qui sont connus comme VRAIs
% et à l'exploiter ici :

base0( [
	'Q'(X, X), % Q(x,y) <=> "y divise x et le quotient x/y est une puissance de 2".
	'P'(X,Y,X,Y), % P(x, y, a, b) <=> PGCD(x,y) = PGCD(a,b)
	'R'(Y, Y, Y, R), % R(y, x, r, x) <=> y mod x = r mod x
	X=X ]).
	
spll([], []).
% Si un terme de la liste 'base0' apparaît dans le conséquent, le séquent est VRAI
spll([[Ant, Cons] | Suite], NSuite) :- base0(F), member(X, F), member(X, Cons), !, % cut indispensable
	spll(Suite, NSuite). 
% Si les trois termes complémentaires X<Y, X=Y et X>Y apparaissent simultanément dans le conséquent, le séquent est VRAI
spll([[Ant, Cons] | Suite], NSuite) :- 
	member(X<Y, Cons), member(X=Y, Cons), member(X>Y, Cons), !, spll(Suite, NSuite). % id.
% Dans les autres cas on ne sait rien dire	
spll([Seq|LSeq] , [Seq|NLSeq]) :- spll(LSeq, NLSeq).

%==============================================================================================================

%--- Synthèse

nw(A, X) :- write(A), nl, normTop(A, B), write(B), nl, wang(B, Y), write(Y), nl, spll(Y, X), write(X), nl.

nwl(L, LX) :- maplist(nw, L, LX).

voirCV(NomFich, L) :- verCondFromFich(NomFich, LCV), nwl(LCV, L).

voirCV(NomFich) :- voirCV(NomFich, L), writeln('-----------'), writeCV(L).

% writeCV(LCV) pour afficherles CV de manière lisible

writeCV([]).
writeCV([[]| SCV]) :- !, writeln('VRAI'), writeCV(SCV).
writeCV([CV | SCV]) :- maplist(writeln, CV), writeCV(SCV).

