:- op(500,fy,not).
:- op(600,yfx,&).
:- op(700,yfx,v).

:- dynamic labelnum/1.

labelnum(0).

new_label(N):-labelnum(N),M is N+1,retractall(labelnum(_)),asserta(labelnum(M)).

% label(Term,Label,Defs0,Defs)

label(P,P,Ds,Ds) :- atom(P),!.
label(T,L,Ds0,Ds) :-
	T =.. [F|Args], member(F,[(->),(&),(v),(not),(,),(;),(:-)]),!,
	label_args(Args,Ls,Ds0,Ds1),
	T1 =.. [F|Ls],	
	( member(L=T1,Ds1),!,Ds=Ds1
	; new_label(N),concat_atom([aux,N],L),merge_set([L=T1],Ds1,Ds)
      ).

label_args([],[],Ds,Ds):-!.
label_args([T|Ts],[L|Ls],Ds0,Ds):-
	label(T,L,Ds0,Ds1),label_args(Ts,Ls,Ds1,Ds).

lp(F,Rs):-
	label(F,LF,[],Defs),
	defs_rules(Defs,RDefs),
	Rs=[LF|RDefs].

defs_rules([],[]):-!.
defs_rules([D|Ds],Rs):-
	def_rules(D,RsD),
	defs_rules(Ds,RsDs),
	merge_set(RsD,RsDs,Rs).

def_rules(L = F & G,[(L :- F,G),(F :- L),(G :- L)]) :- !.
def_rules(L = F v G,[(F ; G :- L),(L :- F),(L :- G)]) :- !.
def_rules(L = (F -> G),[(G :- L,F),(L :- not F),(L :- G),(F; not G;L)]) :- !.
def_rules(L = (not F),[(L :- not F),(not F :- L)]) :- !.

