% ----------------------------------------------------------------------
% -- ensure that companion files are charged

:- ensure_loaded(pref0203).

% ----------------------------------------------------------------------
% -- the real transformation

transform_clauses( Rules, NewRules ) :-
	homogenize(Rules,Rules0),
        apply_to_conjuncts(Rules0,add_preferences,Rules1),

        ok_rules(Rules0,OKRules),
        ap_rules(Rules0,APRules),
	nap_rules(Rules0,NAPRules), % MAJOR CHANGE TO V0203
        pref_rules(PrefRules),
        aux_rules(AuxRules0),

        conjoin(  OKRules,AuxRules0,AuxRules1),
        conjoin(  (APRules,NAPRules),AuxRules1,AuxRules2),
        conjoin(PrefRules,AuxRules2,AuxRules ),

        conjoin(Rules1,AuxRules,NewRules).

homogenize( Wff, HWff ) :-
	Wff = (A :- B) ->
                homogenize(A,HA),
                homogenize(B,HB),
		HWff = (HA :- HB);
        Wff = (A , B) ->
                homogenize(A,HA),
                homogenize(B,HB),
		HWff = (HA , HB);
       (Wff = (A ; B) ; 
        Wff = (A | B) ; 
        Wff = (A v B) ) ->
                homogenize(A,HA),
                homogenize(B,HB),
		HWff = (HA ; HB);
       (Wff = (not A) ;
	Wff = (~   A) ) ->
                homogenize(A,HA),
		HWff = (not HA);
       (Wff = (neg A) ;
	Wff = (-   A) ) ->
                homogenize(A,HA),
		HWff = (neg HA);
	Wff = (A \< B) ->
		HWff = (neg (A < B));
	Wff = [N] ->
		HWff = name(N);
	Wff = ( M : List ) ->
	        convert_set(M,List,InPreds),
		HWff = InPreds;
        %true ->
                Wff = HWff.

convert_set(M,[N],in(N,M)).
convert_set(M,[N|R],InPreds) :-
	convert_set(M,R,RI),
	conjoin(in(N,M),RI,InPreds).

add_preferences( (Head :- name(N), Body), Rules ) :-
        add_preferences_body(Body, N, BodyRules),
        HeadRule = (bl(S) :- ok(S), in(N,S), neg Head),     % or 'nhead(N)'
        conjoin(BodyRules,HeadRule,BlockingRules),
        Rule0a   = ( Head    :- ap(N)                ),
        Rule0b   = (nhead(N) :- neg Head             ),     % MAJOR CHANGE TO V0203
        Rule1    = (ap(N) :- name(N), ok(N), Body ),
        conjoin((Rule0a,Rule0b),    Rule1, Rules01  ),
        conjoin( Rules01,           BlockingRules, Rules    ).
add_preferences( (Head :- name(N)), Rules ) :-
        add_preferences( (Head :- name(N), true), Rules ).
add_preferences( F, F ) :-
        write('Leaving ':F:' untouched'),nl.

add_preferences_body( Body, N, Rules ) :-
        Body = (Body1,Body2) ->
             add_preferences_body(Body1,N,Rules1),
             add_preferences_body(Body2,N,Rules2),
             conjoin(Rules1,Rules2,Rules);
        Body = (not Literal) ->
             Rules = (bl(M) :- ok(M), in(N,M),     Literal        );
        Body =      Literal  ->                           % MAJOR CHANGE TO V0203
             Rules = (bl(M) :- ok(M), in(N,M), not Literal, nap(M)). 

ok_rules( Rules, OKRules ) :-
	ok_rules1( Rules, OKNRules ),
	ok_rules2( Rules, OKMRules ),
	conjoin(OKNRules,OKMRules,OKRules),
	writeln(ok_rules:OKRules).

ok_rules1( Rules, OKRules ) :-
        extract_oko_literals_from_rules1(Rules,N,OKOLiterals),
	OKRule1 = ( ok(N) :- in(N,S), ok(S), not ko(S) ),
        OKRule2 = ( ok(N) :- name(N), OKOLiterals                     ),
        conjoin(OKRule1,OKRule2,OKRules).

extract_oko_literals_from_rules1( Rules, N, Literals ) :-
        Rules = (Rules1,Rules2) ->
            extract_oko_literals_from_rules1(Rules1,N,Literals1),
            extract_oko_literals_from_rules1(Rules2,N,Literals2),
            conjoin(Literals1,Literals2,Literals);
        Rules = in(_,S) ->
            Literals = (not in(N,S));
        %true ->
            Literals = true.

ok_rules2( Rules, OKRules ) :-
        extract_oko_literals_from_rules2(Rules,S,OKOLiterals),
        QRule  = (  ok(S)    :- sname(S), OKOLiterals                     ),
        CRules = ( (oko(S,T) :- sname(S), sname(T), not ((S < T))        ),
                   (oko(S,T) :- sname(S), sname(T),      (S < T) , ap(T) ),
                   (oko(S,T) :- sname(S), sname(T),      (S < T) , bl(T) ) ),
        conjoin(QRule,CRules,OKRules).

extract_oko_literals_from_rules2( Rules, S, Literals ) :-
        Rules = (Rules1,Rules2) ->
            extract_oko_literals_from_rules2(Rules1,S,Literals1),
            extract_oko_literals_from_rules2(Rules2,S,Literals2),
            conjoin(Literals1,Literals2,Literals);
        Rules = in(_,T) ->
            Literals = oko(S,T);
        %true ->
            Literals = true.

ap_rules( Rules, APRules ) :-
        extract_apo_literals_from_rules(Rules,S,APOLiterals),
        QRule  = (  ap(S)    :- sname(S), APOLiterals                 ),
        ARules = ( (apo(S,N) :- sname(S), name(N), not in(N,S)        ),
                   (apo(S,N) :- sname(S), name(N),     in(N,S), ap(N) )),
        conjoin(QRule,ARules,APRules).

extract_apo_literals_from_rules( Rules, S, Literals ) :-
        Rules = (Rules1,Rules2) ->
            extract_apo_literals_from_rules(Rules1,S,Literals1),
            extract_apo_literals_from_rules(Rules2,S,Literals2),
            conjoin(Literals1,Literals2,Literals);
        Rules = (_ :- name(N), _) ->
            Literals = apo(S,N);
        Rules = (_ :- name(N)   ) ->
            Literals = apo(S,N);
        %true ->
            Literals = true.

%                                                        MAJOR CHANGE TO V0203
nap_rules( Rules, NoNegHsRules ) :-
        extract_nap_literals_from_rules(Rules,S,NAPLiterals),
%	writeln(nap_rules:NAPLiterals),
        QRule        = (  nap(S)    :- sname(S), NAPLiterals                         ),
        NoNegHRules  = ( (napo(S,N) :- sname(S), name(N), not in(N,S)                ),
                         (napo(S,N) :- sname(S), name(N),     in(N,S), not nhead(N) )),
        conjoin(QRule,NoNegHRules,NoNegHsRules).

extract_nap_literals_from_rules( Rules, S, Literals ) :-
        Rules = (Rules1,Rules2) ->
            extract_nap_literals_from_rules(Rules1,S,Literals1),
            extract_nap_literals_from_rules(Rules2,S,Literals2),
            conjoin(Literals1,Literals2,Literals);
        Rules = (_ :- name(N), _) ->
            Literals = napo(S,N);
        Rules = (_ :- name(N)   ) ->
            Literals = napo(S,N);
        %true ->
            Literals = true.

pref_rules( PrefRules ) :-
        ASRule = ( neg (T < S) :- sname(S), sname(T), (S < T)                    ),
         TRule = (     (S < T) :- sname(S), sname(T), sname(O), (S < O), (O < T) ),
        conjoin(ASRule,TRule,PrefRules).

aux_rules( Rules ) :-
	Rules = ( ( ko(S)    :- bl(S)   ) ,
	          ( sname(S) :- in(N,S) ) ).

% ----------------------------------------------------------------------
% -- Rules to Procedures

builtin(not,1).
builtin(neg,1).
% builtin(-,1).
% builtin(~,1).
% builtin(<,2).

builtin(ok,1).
builtin(oko,2).
builtin(ko,1).
builtin(ap,1).
builtin(apo,2).
builtin(bl,1).
builtin(nap,1).
builtin(napo,2).
builtin(nhead,1).

constraints([[name,1]|Preds],Constraints) :- 
        constraints(Preds,Constraints).
constraints([[sname,1]|Preds],Constraints) :- 
        constraints(Preds,Constraints).
constraints([[P,N]|Preds],Constraints) :-
        builtin(P,N),
        constraints(Preds,Constraints).
constraints([[P,_]|Preds],Constraints) :-
        negative_functor(P),
        constraints(Preds,Constraints).
constraints([[<,2]|Preds],Constraints) :- 
        Lit = (N < M),
        Constraint = (false :- name(N), name(M), Lit, neg Lit),
        constraints(Preds,Constraints1),
        conjoin(Constraint,Constraints1,Constraints).
constraints([[P,N]|Preds],Constraints) :-
        functor(Lit,P,N),
        Constraint = (false :- Lit, neg Lit),
        constraints(Preds,Constraints1),
        conjoin(Constraint,Constraints1,Constraints).
constraints([],true).

% ----------------------------------------------------------------------
% This is to make dlv happy

idb_rule( (Head :- Body) , (Head :- Body) ).
idb_rule( name(X)        , name(X)        ).
idb_rule( in(X,Y)        , in(X,Y)        ).
idb_rule(  Fact          , (Fact :- true) ) :-
	Fact \= ( _ :- _ ),
	write('IDBing (for dlv) ':Fact),nl.