% Hoare en Prolog - sur le modèle de Wang
% ---------------------------------------

:- use_module('mil_H.pl').

%--- pour voir :

brutCV(NomFich) :- verCondFromFich(NomFich, LCV), enumCV(LCV, 1).

enumCV([], _) :- nl.
enumCV([CV | LCV], N) :- write(N), write(' : '), writeln(CV), 
	M is N+1, enumCV(LCV, M).

%--- Le prédicat d'appel : verCondFromFich(NomFich, LVC)

:- use_module(library(sgml)).
:- ensure_loaded('tradXML_H.pl').

verCondFromFich(NomFich, LVC) :- 
	load_structure(NomFich, TX, [dialect(xml),space(remove)]),
	tradXML(TX, Tripl),
	hoarExt(Tripl, LVC).
	
%=========================================================================

% changer de format

hoarExt(triplet(progMIL(_, LInst), pre(Pre), post(Post)), LCV) :- 
	hoare(trpl(LInst, Pre, Post), LCV).

% le prédicat-maître hoare(trpl, ListCondVer)

% règle 1

hoare(trpl([], Pre, Post), [Pre imp Post]).

% règles banales

hoare(trpl( [X|Y], Pre, Post), LCV) :- 
	reverse([X|Y], [ecrire _| Q]), !, 
	reverse(Q, P),
	hoare(trpl(P, Pre, Post), LCV).

hoare(trpl( [X|Y], Pre, Post), LCV) :- 
	reverse([X|Y], [lire _| Q]), !, 
	reverse(Q, P),
	hoare(trpl(P, Pre, Post), LCV).	
	
hoare(trpl( [X|Y], Pre, Post), LCV) :- 
	reverse([X|Y], [ligne| Q]), !, 
	reverse(Q, P),
	hoare(trpl(P, Pre, Post), LCV).
	
hoare(trpl( [X|Y], Pre, Post), LCV) :- 
	reverse([X|Y], [espace| Q]), !, 
	reverse(Q, P),
	hoare(trpl(P, Pre, Post), LCV).
	
% règle 2a

hoare(trpl( [X|Y], Pre, Post), LCV) :- 
	reverse([X|Y], [Var := Exp| Q]), !, 
	subst(Var, Exp, Post, NPost),
	reverse(Q, P),
	hoare(trpl(P, Pre, NPost), LCV).
	
% règle 2b

hoare(trpl( [X|Y], Pre, Post), [Inv et non T imp Post | LCV]) :- 
	reverse([X|Y], [tantque(T, invariant(Inv), C)| Q]), !, 
	reverse(Q, P),
	hoare(trpl(P, Pre, Inv), LCV1),
	hoare(trpl(C, Inv et T, Inv), LCV2),
	append(LCV1, LCV2, LCV).
	
% règle 2c

hoare(trpl( [X|Y], Pre, Post), LCV) :- 
	reverse([X|Y], [si(T, V, F)| Q]), !, 
	reverse(Q, P), 
	append(P, [?= T | V], P1), hoare(trpl(P1, Pre, Post), LCV1),
	append(P, [?= (non T) | F], P2), hoare(trpl(P2, Pre, Post), LCV2),	
	append(LCV1, LCV2, LCV).
	
% règle 2d

hoare(trpl( [X|Y], Pre, Post), LCV) :- 
	reverse([X|Y], [?= A| Q]), !,
	reverse(Q, P), 	
	hoare(trpl(P, Pre, A imp Post), LCV).
	
%=========================================================================

/* subst, repris de Sterling & Shapiro p. 140
   
   subst(Old, New, Ancien, Moderne) == 
   Moderne est Ancien dans lequel on a substitué New à toutes les occurrences de Old
*/

subst(Old, New, Old, New). % le terme lui-même
subst(Old, New, Term, Term) :- atomic(Term), Term \= Old. 
      %the backslash (\) is normally used to indicate negation in Prolog.
subst(Old, New, Term, Autre) :- 
    compound(Term), 
    functor(Term, F, N), 
    functor(Autre, F, N),
    subst(N, Old, New, Term, Autre). % arité 4 !
    
subst(N, Old, New, Term, Autre) :- 
    N > 0,
    arg(N, Term, ArgOld),
    subst(Old, New, ArgOld, ArgNew),
    arg(N, Autre, ArgNew),
    M is N-1,
    subst(M, Old, New, Term, Autre).
subst(0, Old, New, Terme, Autre).
