
% 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),0,BI,CF,BO):- !,
    next_int(E),
    assertz(e(0,R,E)),         % assert e(C,R,E) E is always new
    rewrite(WFF,E,BI,CF,BO),!. % Context is now E
*/
rewrite(some(R, WFF),C,BI,CF,BO):- !,
    next_int(E),
    assertz(e(C,R,f(E,C))),         % assert e(C,R,f(E,C)) E is always new
    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),!.
%    merge_set(BO1,BO2,BO).

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

rewrite(implies(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite_negated(WFF1,C,BI,CF1,BO1),!,
    rewrite(WFF2,C,BO1,CF2,BO),!,
    disj_cnf(CF1,CF2,CFR),!.
%    merge_set(BO1,BO2,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),0,BI,CF,BO):- !,
    next_int(E),
    assertz(e(0,R,E)),         % assert e(0,R,E) E is always new
    rewrite_negated(WFF,E,BI,CF,BO),!. % Context is now E
*/
rewrite_negated(all(R, WFF),C,BI,CF,BO):- !,
    next_int(E),
    assertz(e(C,R,f(E,C))),         % assert e(C,R,f(E,C)) E is always new
    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),!.
%    merge_set(BO1,BO2,BO).

rewrite_negated(and(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite_negated(WFF1,C,BI,CF1,BO1),!,
    rewrite_negated(WFF2,C,BO1,CF2,BO),!,
    disj_cnf(CF1,CF2,CFR),!.
%    merge_set(BO1,BO2,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),!.
%    merge_set(BO1,BO2,BO).

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,BI,BI):-
    member(e(C,R,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]):-
        append(A,B,D00),!,
        list_to_set(D00,D0),!,
        append_to_all(A,C,D1),!.
