% les précédences pour la syntaxe MIL + assertions
% de manière à ce que le lecteur de PROLOG lise et écrive le programme
% directement comme un terme = arbre de syntaxe abstraite.
% y compris les conventions de Wang
 
:- module(mil_H,
	[ %% MIL -------
	  op( 800, xfy, [ := ]),	% ":=" idem, de plus forte priorité 
	  op( 800, fx, [ lire, ecrire, '?=' ]), % unaires, de même priorité 
	  op( 700, xfx, [<=, <>]),  % relateurs inconnus de Prolog
	  %% Wang --------
	  op(950, yfx, [imp]),
	  op(925, yfx, [ou]),
      op(900, yfx, [et]),
      op(850, fx, [non]),

	  prog1/1,
	  prog2/1,
	  prog3/1,
	  prog4/1,
	  prog5/1,
	  estTopMIL_H/1
	]
).

% N.B. La précédence de la virgule (pour les listes) est de 1000 (non-redéfinissable)
% elle est donc inférieure à celle des opérateurs MIL, OK.
% Pour Wanf, il faut éviter le conflit avec les relateurs, qui ont tous précédence 700 !

%--- Exemples de programmes dans la syntaxe correspondante 

prog1(triplet(progMIL([a, b, q, r], [lire a , lire b , q := 0 , r := a ,
      tantque(r >= b, invariant((a = ((b * q) + r)) et (r >= 0)), 
      [q := q+1 , r := r-b]) , ecrire q , espace, ecrire r, ligne]),
      pre((a >= 0) et (b > 0)),
      post(((a = ((b * q) + r)) et (r >= 0)) et (r < b))
    )
).

prog2(triplet(progMIL([n, m, p], [lire n , si( n <= 0, [ecrire 0],  [m := n , p := 1 , 
		   tantque( m > 0,  invariant(m>=0 et 'M'(p,m,n)),
		      [p := p*m , m := m-1]), ecrire p, ligne])]),
		   pre(n=n),
		   post(n>0 imp 'F'(p, n))
		)
).

%%%% F(p, n) <=> p=n! et M(p,m,n) <=> p = n!/m!
%%%% on doit mettre dans la base que "M(p, 1, n) imp F(p, n)"

prog3(triplet(
	progMIL([a, b, d, t, q, r],
	[lire a,lire b,t:=b,
	tantque(t-a=<0, invariant((0 =< a) et 'Q'(t, b)), [t:=2*t]),
	q:=0, r:=a, d:=t,
	tantque(0>b-d,
	invariant((((a =:= ((d * q) + r)) et (r < d)) et (0 =< r)) et 'Q'(d, b)),
		[d:=d//2,
		si(r-d>=0,
			[r:=r-d, q:=2*q+1],
			[q:=2*q])
		]
	),
	ecrire q,
	espace,
	ecrire r,
	ligne ]),
	pre((a >= 0) et (b > 0)),
	post(((a =:= ((b * q) + r)) et (r >= 0)) et (r < b))
	)
).

prog4(triplet(progMIL([a, b, z, x, y],[lire a, lire b, x:=a, y:=b , si(y>x, [z:=x, x:=y, y:=z], []), ecrire a, espace, ecrire b, ligne]), pre(a=a), post(y<=x))).

prog5(triplet(progMIL([x, y], [lire x, lire y, x := x+y, y := x-y, x := x-y, ecrire x, espace, ecrire y, ligne]), pre(x=a et y=b), post(x=b et y=a))).

%--- Contrôleur syntaxique

estTopMIL_H(triplet(progMIL(LVar, LInst), pre(Pre), post(Post))) :- 
	estDecVar(LVar), estSeqMIL_H(LInst), estAss(Pre), estAss(Post). %****

estAss(A) :- A =.. [Op, G, D], member(Op, [imp, ou, et]), estAss(G), estAss(D).
estAss(non A) :- estAss(A).
estAss(A) :- functor(A, F, _), estMaj(F), !.
estAss(A) :- estExpBool(A).

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

%--- estDecVar(LVar)
estDecVar([]).
estDecVar([V | LV]) :- atom(V), estDecVar(LV).

%--- estSeqMIL_H(LInst)
estSeqMIL_H([]).
estSeqMIL_H([X|Y]) :- estInstMIL_H(X), estSeqMIL_H(Y).

estCorpsMIL_H(X) :- estSeqMIL_H(X).
% estCorpsMIL_H(X) :- estInstMIL_H(X). % incompatible avec le programme Hoare

%--- estInstMIL_H(Inst)
estInstMIL_H(espace).
estInstMIL_H(ligne).
estInstMIL_H(lire A) :- estVar(A).
estInstMIL_H(ecrire E) :- estExpAr(E).
estInstMIL_H(A := E) :- estVar(A), estExpAr(E).
estInstMIL_H(tantque(T, invariant(Inv), C)) :- estExpBool(T), estAss(Inv), estSeqMIL_H(C). %****
estInstMIL_H(si(T, V, F)) :- estExpBool(T), estSeqMIL_H(V), estSeqMIL_H(F).

estExpAr(E) :- estCte(E).
estExpAr(E) :- estVar(E).
estExpAr(E) :- E =..[Op, G, D], member(Op, ['+', '*', '-', '/']), estExpAr(G), estExpAr(D).

estExpBool(E) :- E =..[Op, G, D], member(Op, ['=', '<', '>', '<=', '>=', '<>']), estExpAr(G), estExpAr(D).
estCte(E) :- integer(E).
estVar(E) :- atom(E).	

%--- test

t4 :- prog4(X), estTopMIL_H(X).