
% modal_rewrite.pl


rewrite(all(R, WFF),C,BI,CF,BO):- !,
    getVarBind(C,R,V,BI,BL),   % update the Binding set by e(C,R,v(V)), V may be new - e is functional
    rewrite(WFF,V,BL,CF,BO),!. % Context is now V

rewrite(some(R, WFF),C,BI,CF,[e(C,R,f(E,C))|BO]):- !, % add e(C,R,f(E,C)) E is always new
    next_int(E),
    rewrite(WFF,f(E,C),BI,CF,BO),!. % Context is now E

rewrite(and(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite(WFF1,C,BI,CF1,BO1),!,
    rewrite(WFF2,C,BO1,CF2,BO),!,
    conj_cnf(CF1,CF2,CFR),!.

rewrite(or(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite(WFF1,C,BI,CF1,BO1),!,
    rewrite(WFF2,C,BI,CF2,BO2),!,
    disj_cnf(CF1,CF2,CFR),!,
    append(BO1,BO2,BO3),!,
    list_to_set(BO3,BO),!.

rewrite(implies(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite_negated(WFF1,C,BI,CF1,BO1),!,
    rewrite(WFF2,C,BI,CF2,BO2),!,
    disj_cnf(CF1,CF2,CFR),!,
    append(BO1,BO2,BO3),!,
    list_to_set(BO3,BO),!.

rewrite(not(WFF),C,BI,CFR,BO):- rewrite_negated(WFF,C,BI,CFR,BO).

rewrite(WFF,C,BI,[[[WFF,C]]],BI):- !.



rewrite_negated(some(R, WFF),C,BI,CF,BO):- !,
    getVarBind(C,R,V,BI,BL),   % update the Binding set by e(C,R,v(V)), V may be new - e is functional
    rewrite_negated(WFF,V,BL,CF,BO),!. % Context is now V

rewrite_negated(all(R, WFF),C,BI,CF,[e(C,R,f(E,C))|BO]):- !, % add e(C,R,f(E,C)) E is always new
    next_int(E),
    rewrite_negated(WFF,f(E,C),BI,CF,BO),!. % Context is now f(E)

rewrite_negated(or(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite_negated(WFF1,C,BI,CF1,BO1),!,
    rewrite_negated(WFF2,C,BO1,CF2,BO),!,
    conj_cnf(CF1,CF2,CFR),!.

rewrite_negated(and(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite_negated(WFF1,C,BI,CF1,BO1),!,
    rewrite_negated(WFF2,C,BI,CF2,BO2),!,
    disj_cnf(CF1,CF2,CFR),!,
    append(BO1,BO2,BO3),!,
    list_to_set(BO3,BO),!.

rewrite_negated(implies(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite(WFF1,C,BI,CF1,BO1),!,
    rewrite_negated(WFF2,C,BO1,CF2,BO),!,
    conj_cnf(CF1,CF2,CFR),!.

rewrite_negated(not(WFF),C,BI,CFR,BO):- rewrite(WFF,C,BI,CFR,BO).

rewrite_negated(WFF,C,BI,[[[not(WFF),C]]],BI):- !.

%getVarBind(C,R,v(V),BI,BI):-
%    member(e(C,R,v(V)),BI),!.
getVarBind(C,R,v(V),BI,[e(C,R,v(V))|BI]):-
    next_var(V),!.


conj_cnf(A,B,C):- append(A,B,C),!.

disj_cnf(C,[],C):-!.
disj_cnf([],_,[]):-!.
disj_cnf([A|B],C,D):-
        list_to_set(A,AA),!,
        append_to_all(AA,C,D0),!,
        disj_cnf(B,C,D1),!,
        append(D0,D1,D),!.

append_to_all(_,[],[]):-!.

/*
append_to_all(A,[B|C],[D0|D1]):-
        modal_clash(A,B,AA),!,
        append(AA,B,D00),!,
        list_to_set(D00,D0),!,
        append_to_all(AA,C,D1),!.
*/
append_to_all(A,[B|C],[D0|D1]):-
        append(A,B,D00),!,
        list_to_set(D00,D0),!,
        append_to_all(A,C,D1),!.

modal_clash(A,B,AR):-
    member([_P,v(V)],A),
    member([_Q,v(V)],B),!,
    next_var(W),
    rename(V,W,A,AA),
    modal_clash(AA,B,AR),!.
    
modal_clash(A,_,A):-!.

rename(_,_,[],[]):-!.
rename(V,W,[[P,v(V)]|A],[[P,v(W)]|AA]):-!,
    rename(V,W,A,AA),!.
rename(V,W,[[P,T]|A],[[P,T]|AA]):-
    rename(V,W,A,AA),!.
