/* Interprete de clauses Prolog:
	-  	sans Predicats predefinis,
	-	avec parcours de l'arbre de recherche en largeur d'abord,
	-	sans conservation de l'arbre de recherche complet  */

/* Recherche au premier niveau */
bf(But):-
	bf_0(But,L_sbuts,Preuves),
	bf_edite(But,But,Preuves),trace,
	bf_elim(L_sbuts,true,L_g1),  /* Elimine les buts deja prouves */
	bf_elim(L_g1,nil,L_g),   /* Ignore les buts non prouvables */
	bf_suite(But,L_g),!.
bf_0(But,L_sbuts,Preuves):-
	bf_listedes(But,clause(But,true),Preuves),
	bf_listedes(X,clause(But,X),L_sousbuts),
	bf_lisser(L_sousbuts,L_sbuts),!.

/* Exploration niveau par niveau */
bf_suite(But,L_g):-
	bf_s(But,L_g,LR), /* Exploration d'un niveau */
	bf_fin(But,LR).   /* teste de fin  */
bf_fin(_,[]):-!.
bf_fin(But,X):- bf_suite(But,L_g).

bf_s(_,[],[]):-!.
bf_s(But,[T|R],Z):-
	bf_s1(But,T,T1),
	bf_s(But,R,R1),
	bf_conc(T1,R1,Z).
bf_s1(But,T,T1):-
	T = [L|R],!,  /* Cas ou T est une liste de sous-buts */
	bf_et(But,T,T1).
bf_s1(But,T):- 
	bf0(T,T1,P),    /* T est un terme simple */
	bf_elim(L_sbuts,true,L_g),  /* Elimine les buts deja prouves */
	bf_elim(L_sbuts,nil,L_g),   /* Ignore les buts non prouvables */
	bf_edite(But,T,P).

bf_et(But,[G|R],T1):-		/* T est une liste de sous-buts */
	bf_listedes(G,clause(G,true),Preuves),
	(Preuves = [nil];bf_et1(X,Preuves,R,L0)),
	bf_listedes(X,clause(G,X),L_g),
	L_g \== [nil],
	bf_et2(L_g,R,L1),
	bf_conc(L0,L1,T1).


bf_et(_,[nil]).	/* En cas d'echec sur un but 
			  la conjonction n'est pas prouvable */
/* Propagation des succes */
bf_et1(X,P1,R,L0):-
	assert(bf_ex(X)),
	bf_et1(X,P1,R,L0),
	retract(bf_ex(X)).
bf_et1([P1|Pr],R,L0):-
	bf_ex(X),	/* Generation d'exemplaires */
	X=P1, bf_et3([],R,L1),
	bf_et1(Pr,R,L2),
	bf_conc(L1,L2,L0).
/* Propagation des sous-buts*/
bf_et2([true|L_g],R,L1):- bf_et2(L_g,R,L1),!.
bf_et2([T|L_g],R,L):-
	bf_et3(T,R,L0),
	bf_et2(L_g,R,L1),
	bf_conc(L0,L1,L).
bf_et3(P,R,L):-
	bf_et(_,R,T),
	bf_et3_p(P,T,L).
bf_et3_p(P,[X|R],[X1|Z1]):-
	bf_conc(P,X,X1),
	bf_et3_p(P,R,Z1).
  


/* L: liste des X verifiant P */ 
bf_listedes(X,P,[nil]):- not P,!.
bf_listedes(X,P,L):- setof(X,P,L).

/* Elimine les occurences de V dans une liste */
bf_elim([],_,[]).
bf_elim([V|Y],V,[Z]):- bf_elim(Y,V,Z).
bf_elim([X|Y],V,[X|Z]):- 
	X \== V,
	bf_elim(Y,V,Z).

/* Teste si une Liste contient nil */
bf_nil([nil]).
bf_nil([nil|_]):-!.
bf_nil([X|Y]) :- bf_nil(Y).

/* Edite X */
bf_edite(_,_,X):-X=[];X=[nil].
bf_edite(But,T,[X|R]):- 
	bf_ecrire(But,T,X),
	bf_edite(But,T,R).
bf_ecrire(But,T,X):-	/* Ecriture avec propagation de l'instanciation */
	T = X, write(But),nl,fail.
bf_ecrire(_,_,_):- !.


/* Construction d'une liste homogene (forme de termes simples et de listes) */
bf_lisser(nil,nil).
bf_lisser([X|Y],Z):-bf_lisser(X,X1),bf_lisser(Y,Y1),bf_conc(X1,Y1,Z).
bf_lisser(X,[Y]):- X =.. [','|_],bf_aplat(X,Y),!.
bf_lisser(X,[X]):-!.
bf_aplat((X,Y),[X|Z]):-bf_aplat(Y,Z).
bf_aplat((X),[X]).
bf_conc([],X,X).
bf_conc([X|R],Y,[X|Z]):-bf_conc(R,Y,Z).

/* Exemple */
p:-p1(x,Y),p2,p3(Y).
p:-p0.
p.
p1(x,5).
p2:-p0.
p3(5).
p3(6).
p0.