/* Quasi-Prolog pur, sans "cut",  en Prolog, by J-F. Perrot , révision 19/03/09 */
/*-------------------------------------------------------------------------------------*/

/* Exemples dans 'ExMplg.pl' */

:- [unif]. /* L'unification en Prolog, même cours */

/* Gestion des nouvelles generations de variables pour la renovation */
:- dynamic generation/1.

generation(0).
new-generation(N) :- generation(A), N is A+1, 
			retract(generation(A)), assert(generation(N)).

new-name(A, N, NA) :- name(A, LA), name(N, LN), append(LA, LN, LNA),
			name(NA, LNA), assert(isvar(NA)).

/* Renovation de termes (alpha-conversion) */

renove-terme(A, N, NA) :- isvar(A), !, new-name(A, N, NA).
renove-terme(A, N, A) :- atomic(A), !.
renove-terme(T, N, NT) :- T =..[Fonc|LArgs],
			 renove-ltermes(LArgs, N, LNArgs),
			 NT =.. [Fonc|LNArgs].

renove-ltermes([], N, []).
renove-ltermes([T|LT], N, [NT|NLT]) :- renove-terme(T, N, NT),
					renove-ltermes(LT, N, NLT).

new-clause([T|Q], [NT|NQ]) :- new-generation(N), 
	renove-terme(T, N, NT), renove-ltermes(Q, N, NQ).

/* Resolution lineaire de clauses de Horn */

resoudre([], Ref, LCl, Subst) :- !. /*resoudre(LButs, LRef, LCl, Subst) */

resoudre([B|SB], LRef, [[T|Q]|LCl], Subst) :-
	new-clause([T|Q], [NT|NQ]), unif(B, NT, Sb),
	appsub(Sb, SB, NSB), appsub(Sb, NQ, SNQ), append(SNQ, NSB, NB),
	resoudre(NB, LRef, LRef, Ssb), append(Sb, Ssb, Subst).

resoudre(LB, LRef, [_|LCl], Subst) :- resoudre(LB, LRef, LCl, Subst).

/* Le predicat d'appel */

prolog(LButs, LRef) :- resoudre(LButs, LRef, LRef, Subst),
	liste-var(LButs, LVar), sort(LVar, SLVar),
	lappsub(Subst, SLVar, SLVal),
	display(SLVar, SLVal).

liste-var(Terme, [Terme]) :- isvar(Terme), !. /* sans duplication */
liste-var(Terme, []) :- atomic(Terme), !.
liste-var(Terme, LV) :- Terme=..[Fonc|LArgs], lliste-var(LArgs, LV).

lliste-var([], []).
lliste-var([T|S], LV) :- liste-var(T, LT), lliste-var(S, LS),
			 add(LT, LS, LV). /* evite les duplications */
add([], X, X).
add([A|S], X, Y) :- present(A, X), !, add(S, X, Y).
add([A|S], X, [A|Y]) :-  add(S, X, Y).

present(A, [B|S]):- A=B, !.
present(A, [_|S]):- present(A, S).

display([], []) :- write('OK !'), nl. /* pour voir les jeux de valeurs */
display([Var|SVar], [Val|SVal]) :- write(Var), write(' = '), write(Val),
					nl, display(SVar, SVal).
