/* Create fuzzy normal form of axioms */

not(X) :- \+(X), !.

:- dynamic(gensymval/1).
:- dynamic(ub/3).
?- retractall(ub(_,_,_)).

?- use_module(library(lists)).
?- use_module(library(ordsets)).

/* Default -- op(1100, xfy, ;). */
/* Default -- op(1000, xfy, ','). */
?- op(400, xfx, :). 
?- op(500,xfx,@).
?- op(100, fx, all).
?- op(100, fx, ex).
?- op(100, fx, ^).
?- op(300, fy, ~). /* Override default to allow nested ~'s */
?- op(300, fy, '-').
?- op(1100, xfx, <-->).
?- op(1050, xfx, <--).

/* For conjunction of axioms S get fuzzy normal rules List in sorted conjunctive normal form*/
normalize(S,Answer) :-  
	moveNots(S,U),
        skolemize(U,W,[ ]), 
        findall(Z, distribute(W,Z), L), 
	deleteComplements(L,L1), 
	complementRanges(L1,L2),
	mergeInHeads(L2,L3),
	subsumeAll(L3, Answer,[]).

deleteComplements([],[]).
deleteComplements([H|T],U) :- hasComplements(H), !,deleteComplements(T,U).
deleteComplements([H|T],[H|U]) :- deleteComplements(T,U).

hasComplements(X) :- member(M,X), member(~M,X).

complementRanges([],[]).
complementRanges([H1|T1],[H2|T2]):- doComplements(H1,H2),
	complementRanges(T1,T2).
doComplements([],[]).
doComplements([-in(X,Y)|T1],[in(X,Z)|T2]) :- !, 
	myComplementIntvl(-inf,Y,Z),
	doComplements(T1,T2).
doComplements([~in(X,Y)|T1],[in(X,Z)|T2]) :- !, 
	myComplementIntvl(-inf,Y,Z),
	doComplements(T1,T2).
doComplements([H1|T1],[H1|T2]):- doComplements(T1,T2).

myComplementIntvl(LB,[],[LB:inf]).
myComplementIntvl(LB,[X:Y],[LB: XX, YY:inf]):- 
	myCompl2(X,XX),myCompl2(Y,YY), !.
myComplementIntvl(LB,[R1:R2|T1],[LB:R1C|T2]):- 
	myCompl2(R1,R1C), myCompl2(R2,R2C), !,
	myComplementIntvl(R2C,T1,T2).
myComplementIntvl(LB,[H|T1],[LB: NH | T2]) :- 
	myCompl2(H,NH), 
	myComplementIntvl(NH,T1,T2).

myCompl2(^ X, X):- !.
myCompl2(X, ^ X).

mergeInHeads([],[]).
mergeInHeads([H|T], Ans) :- 
     mergeInHeads(T,T2),
    findall([in(X,I)|Rest], 
	A^Y^Z^Rest1^Rest2^(myRemove(in(X,Y),H,Rest1),
         member(A,T2), 
	 myRemove(in(X,Z),A,Rest2), 
	 myIntersect(Y,Z,I),
         mymerge(Rest1,Rest2,Rest)),
	L),
     append(L,[H|T2],Ans), !.
mergeInHeads([H|T1],[H|T2]) :- mergeInHeads(T1,T2).

myRemove(H,[H|T],T).
myRemove(X,[H|T],[H|T2]) :- myRemove(X,T,T2).

myIntersect([],_,[]):- !.
myIntersect(_,[],[]):- !.
myIntersect([R1:R2|T1],[_ :R4|T2],Z2) :- 
	myge(R1,R4), !, myIntersect([R1:R2|T1],T2,Z), getZ(R1,R4,Z,Z2).
myIntersect([_ :R2|T1],[R3:R4|T2],Z2) :- 
	myge(R3,R2), !, myIntersect(T1,[R3:R4|T2],Z), getZ(R3,R2,Z,Z2).
myIntersect([R1:R2|T1],[R3:R4|T2],[R6:R5|Z]) :- 
	myMax(R1,R3,R6), !, nextIntersect(R1,R2,R3,R4,R5,T1,T2,Z).

getZ(X,X,Z,[X:X|Z]) :- X\= ^ _, !.
getZ(_,_,Z,Z).

nextIntersect(R1,R2,_,R4,R4, T1,T2,Z) :-
        myge(R2,R4), !, myIntersect([R1:R2|T1],T2,Z).
nextIntersect(_,R2,R3,R4,R2, T1,T2,Z) :-
	myIntersect(T1,[R3:R4|T2],Z).

subsumeAll([],[],_):- !.
subsumeAll([H|T],U,New) :- subsumed(H,T), !, subsumeAll(T,U,New).
subsumeAll([H|T],U,New) :- subsumed(H,New), !, subsumeAll(T,U,New).
subsumeAll([H|T],[H|U],New) :- subsumeAll(T,U,[H|New]).

subsumed(A,L) :- member(X,L), superset(A,X).

superset(_,[]).
superset(L, [H|T]) :- member(H,L), !, superset(L,T).
superset(L, [in(X,Y)|T]) :- 
	member(in(X,Z),L), myIntvlContained(Y,Z), superset(L,T).

myIntvlContained([U:V|T],L) :- 
	member(X:Y,L), myge(U,X), myge(Y,V), myIntvlContained(T,L).
myIntvlContained([],_).

moveNots(- ~X,Z) :- !, moveNots(X,Z).
moveNots(- -X,Z) :- !, moveNots(~ -X,Z).
moveNots(~ - -X, Y) :- !, moveNots(-X,Y).
moveNots(~ - ~X, Y) :- !, moveNots(~X,Y).
moveNots(~ ~X, Y) :- !, moveNots(X,Y).
moveNots(- ~X, Y) :- !, moveNots(X,Y).
moveNots(~ ~X,Y) :- !, moveNots(X,Y).
moveNots(~ ex X:Y, all X:Z) :-  !, moveNots(~Y,Z).  
moveNots(~ all X:Y, ex X:Z) :-  !, moveNots(~Y,Z).
moveNots(~ - (X<-->Y), ((XX,YY);(NX,NY))) :- !, 
   moveNots(X,XX), moveNots(Y,YY),
   moveNots(~ -X,NX), moveNots(~ -Y,NY).
moveNots(- (X<-->Y), ((XX,NY);(NX,YY))) :- !, 
   moveNots(X,XX), moveNots(Y,YY),
   moveNots(-X,NX), moveNots(-Y,NY).
moveNots(~ (X<-->Y), ((XX,NY);(NX,YY))) :- !, 
   moveNots(X,XX), moveNots(Y,YY),
   moveNots(~X,NX), moveNots(~Y,NY).
moveNots((X<-->Y),((XX,YY);(NX,NY))) :- !, 
   moveNots(X,XX),moveNots(Y,YY),
   moveNots(~X,NX), moveNots(~Y,NY).
moveNots(~ - (X<--Y), (XX ; NY)) :- !, moveNots(~ - X,XX), moveNots(~Y,NY).
moveNots(- (X<--Y), (NX,YY)) :- !, moveNots(-X,NX), moveNots(Y,YY).
moveNots(~ (X<--Y), (NX,YY)) :- !, moveNots(~X,NX), moveNots(Y,YY).
moveNots((X<--Y), (XX;NY)) :- !, moveNots(X,XX), moveNots(~Y,NY).
moveNots(~ - ((X,Y)), ((U , V))) :-  !, moveNots(~ - X,U), moveNots(~ - Y,V).
moveNots(- ((X,Y)), ((U;V))) :-  !, moveNots(-X,U), moveNots(-Y,V).
moveNots(~ ((X,Y)), ((U;V))) :-  !, moveNots(~X,U), moveNots(~Y,V).
moveNots(((U,V)), ((W,X))) :- !, moveNots(U,W), moveNots(V,X).
moveNots(~ - ((X;Y)), ((U;V))) :-  !, moveNots(~ -X,U), moveNots(~ -Y,V).
moveNots(- ((X;Y)), ((U,V))) :-  !, moveNots(-X,U), moveNots(-Y,V).
moveNots(~ ((X;Y)), ((U,V))) :-  !, moveNots(~X,U), moveNots(~Y,V).
moveNots((U;V), (W;X)) :- !, moveNots(U,W), moveNots(V,X).
moveNots(X:Z,X:Y) :- !, moveNots(Z,Y).
moveNots(~ -X, ~ -X) :- functor(X,F,_), not(member(F,['-', '~',':', ',', ';'])),!.
moveNots(-X,-X) :- functor(X,F,_), not(member(F,['-', '~',':', ',', ';'])),!.
moveNots(~X,~X) :- functor(X,F,_), not(member(F,['-', '~',':', ',', ';'])),!.
moveNots(X,X) :- functor(X,F,_), not(member(F,['-', '~', ':', ',', ';'])), !.
moveNots(X,_) :- print('error: leave blank after ~ and - operators in '), print(X), nl, fail.

skolemize(X,X,_) :- var(X), !.
skolemize(X,Y,All) :- skol2(X,Y,All).

skol2(X,X,_) :- atomic(X), !.
skol2(all X:Y, U, All) :- !,
       recursivesubst(X,Y, NewX, NewY),
       skolemize(NewY, U, [NewX | All]).
skol2(ex X:Y, U, All) :- !,
       gensym(GenSym), S=..[GenSym|All],
       recursivesubst(X, Y, S, NewY),
       skolemize(NewY, U, All).
skol2([Head|Tail], [NewHead | NewTail], All) :- !,
   skolemize(Head, NewHead, All), skolemize(Tail, NewTail, All).
skol2(F, G, All) :-  not(atomic(F)), F=..[Func|Args],
   Func\== ':', Func\=='.', !,
   skolemize(Args,NewArgs,All),
   G=..[Func|NewArgs].
skol2(F,F,_).

gensym(Name) :- retract(gensymval(Old)), X is Old+1, assert(gensymval(X)),
	number_chars(X,List), name(Name,[36, 103, 101, 110 | List]). 
gensymval(0).

distribute((X;Y;Z),W) :- !, 
	appendClauses(X,Y,XY), distribute(Z,ZZ),mymerge(XY,ZZ,W).
distribute(((X,_Y);Z), XZ ) :-  appendClauses(X,Z,XZ).
distribute(((_X,Y);Z), YZ ) :-  !, appendClauses(Y,Z,YZ).
distribute((X;(Y,_Z)), XY ) :-  appendClauses(X,Y,XY).
distribute((X;(_Y,Z)), XZ ) :-  !, appendClauses(X,Z,XZ).
distribute((X;Y),XY) :- 
        functor(X,FX,_), FX\==',',
        functor(Y,FY,_), FY\==',',
	appendClauses(X,Y,XY).
distribute((X,_), Z) :- distribute(X,Z).
distribute((_,Y), Z) :- distribute(Y,Z).
distribute(X,[X]):- functor(X,F,_), F\==';', F\==','.

appendClauses(X,Y,Z) :- distribute(X,XX), distribute(Y,YY),
          mymerge(XX,YY,Z).

mymerge(X,[],X):- !.
mymerge([],Y,Y):- !.
mymerge([A|_],[~A|_],_):- ground(A), !, fail.  /*True*/
mymerge([~A|_],[A|_],_):- ground(A), !, fail.
mymerge([A|D],[~B|E],C):-  
	not(not(A=B)), !, mymerge(D,E,C).  
mymerge([~B|D],[A|E],C):-  
	not(not(A=B)), !, mymerge(D,E,C).
mymerge([declaredClasses(X) | B], [declaredClasses(Y) | D], Z) :- !, append(X,Y,W), 
      list_to_ord_set(W,U), mymerge([declaredClasses(U)|B],D,Z).
mymerge([in(X,[R1:R2|Tail1]) | B], [in(X,[R3:R4|Tail2]) | D],Z) :- !,
       myRangeMerge([R1:R2|Tail1],[R3:R4|Tail2],Ans),
       mymerge([in(X,Ans)|B],D,Z).
mymerge([in(X,L1)|B], [in(X,L2)|D],Z) :- !, append(L1,L2,W),
      list_to_ord_set(W,U), mymerge([in(X,U)|B],D,Z).
mymerge([A|B],[C|D],[A|Z]) :- myLess(A,C), !, mymerge(B,[C|D],Z).
mymerge([A|B],[C|D],Z) :- A==C, !, mymerge(B,[C|D],Z).  /*Identical*/
mymerge(L,[C|D],[C|Z]) :- mymerge(L,D,Z).

myRangeMerge([],X,X).
myRangeMerge(X,[],X).
myRangeMerge([R1:R2,R3:R4|Tail],Y,Z) :- myge(R2,R3), !, notBothN(R2,R3),
        myMax(R2,R4,Max),  /*assume R1<R3 */
        myRangeMerge([R1:Max|Tail],Y,Z).
myRangeMerge([(R1:R2)|Tail1],[(R3:R4)|Tail2],Ans) :-
        myge(R2,R3), notBothN(R2,R3),!, myMin(R1,R3,Min), myMax(R2,R4,Max),
        myRangeMerge([Min:Max|Tail1],Tail2,Ans). 
myRangeMerge([R1:R2|Tail1],[R3:R4|Tail2],[R1:R2|Ans]) :- 
        myRangeMerge(Tail1,[R3:R4|Tail2],Ans). 

notBothN(^ _, ^ _) :- !, fail.
notBothN(_,_).

myge(_, ^ -inf) :- !.
myge(_, -inf) :- !.
myge(inf, _) :- !.
myge(^ inf, _) :- !.
myge(^X, ^Y) :- !, X@>=Y.
myge(^ X,Y) :- !, X@>=Y.
myge(X, ^Y) :- !, X@>=Y.
myge(X,Y) :- X@>=Y.

myMax(X,Y,X) :- myge(X,Y), !.
myMax(_,Y,Y).
myMin(X,Y,X) :- myge(Y,X), !.
myMin(_,Y,Y).

myLess(~A,B):- !, myLess(A,B).
myLess(A,~B):- !, myLess(A,B).
myLess(A,B) :- A@<B.

/*Don't allow head in the body (immediate recursion)*/
getRule(List,_,_,_) :- member(X,List),
	(member( -X,List); member(~X,List)), !, fail. 
/*"Seen" checks prevent indirect recursion */
getRule(List, Seen, (ub(E2,V,Seen):-notSeen(E2,Seen),Body), Z) :- 
    choose1(List, Element, Others), 
    moveNots(~Element,E1),
    mycomplement(E1,E2),
    makeBody(V, [E2|Seen], Others, [Z], Body).

makeBody(V, _, [], Vars, min_list(Vars,V)).
makeBody(V, Seen, [Next|Tail], Vars, 
   (ub(NotNext, NewVar, Seen), TailBody)):-
               mycomplement(Next,NotNext),
               makeBody(V, Seen, Tail, [NewVar | Vars], TailBody).

notSeen(X,Seen) :- not(member(X,Seen)).
mycomplement(~ -(X), -(X)) :- !.
mycomplement(~X,X) :- !.
mycomplement(-X,X) :- !.
mycomplement(X,-X).

choose1([H|T], H, T).
choose1([H|T], Y, [H|Z]) :- choose1(T,Y,Z).

/* e.g. recursivesubst(2,[1,2,3,4],7,[1,7,3,4]).  */
recursivesubst(X,XTerm,Y,YTerm) :- 
      var(XTerm), X==XTerm, YTerm=Y.
recursivesubst(X,XTerm,_,YTerm) :- 
      var(XTerm), X\==XTerm, YTerm=XTerm.
recursivesubst(X,XTerm,Y,YTerm) :- nonvar(XTerm), X==XTerm, YTerm=Y.
recursivesubst(X,XTerm,_,YTerm) :- nonvar(XTerm), X\==XTerm,  
      atomic(XTerm), YTerm=XTerm.
recursivesubst(X,XTerm,Y,[NewHead|NewTail]) :- 
      nonvar(XTerm), XTerm=[Head|Tail],
      recursivesubst(X,Head,Y,NewHead),
      recursivesubst(X,Tail,Y,NewTail).
recursivesubst(X,XTerm,Y,YTerm) :- nonvar(XTerm), not(atomic(XTerm)),
      XTerm=..[F|Args], F\== '.', 
      recursivesubst(X,Args,Y,NewArgs), 
      YTerm=..[F|NewArgs].


add(X):- add(X,1).
add(X,Z) :- normalize(X,List), member(Y,List), print(Y), nl, 
       getRule(Y,_,R,Z), myCondAsserta(R), fail.
add(_,_).

myCondAsserta((H:- B)) :- makeBodyList(B,B1),
        clause(H,D,Ref), makeBodyList(D,B2),
        getBody(B1,C1,Z1), getBody(B2,C2,Z2),
        mymerge(C1,C2,C3), loopOrSucceed(C1,C2,C3,Ref,Z1,Z2), !.
myCondAsserta(R):- asserta(R).

/*Loop to subsume more (longer) clauses with lower fuzzy values.*/
loopOrSucceed(_,C2,C3,Ref,Z1,Z2) :- Z1>=Z2, C2==C3, erase(Ref),
	fail.
/*New clause is subsumed by existing clause*/
loopOrSucceed(C1,_,C3,_,Z1,Z2) :- Z1=<Z2, C1==C3, !.

checkDelete(C1,_,C3,Ref) :- C1==C3, erase(Ref), !.

makeBodyList((X,Y),[X|Z]) :- !, makeBodyList(Y,Z).
makeBodyList(X,[X]).

prettyPrint(X) :- pp2(X,1).
pp2([H|T],Tab) :-  tab(Tab), print('['),nl,
		 T2 is Tab+2, 
                 pp3([H|T],T2), 
		tab(Tab), print(']'), nl, !.
pp2(X,Tab) :- tab(Tab), print(X), nl.

pp3([],_).
pp3([H|T],N):- pp2(H,N), pp3(T,N).

getBody(X,Y,Z) :- append([notSeen(_,_)|Y],[min_list(L,_)],X),
	append(_,[Z],L).

(X@ _) :- not(myground(X)), !, fail.
((~ X)@Z) :- number(Z), N is 1-Z, add(X,N), !.
((~ X)@Z) :- var(Z), !, (X@N), Z is 1-N, !.
X@Z :- var(Z), findall(Y,ub(X,Y,[]),List), max_list([0 | List],Z).
X@Z :- number(Z), add(X,Z).

myground(X) :- var(X), !, fail.
myground(X) :- atomic(X), !.
myground([X|Y]) :- !, myground(X), myground(Y).
myground(X) :- X=..[_|Args], myground(Args).


ub(~X,Y,Seen) :- !, ub(X,Z,Seen), !, Y is 1-Z.


?- p@0.75.
?- q@0.9.
?- add((r<--p,q)).
?- add((q<--r,s),0.7).
?- listing(ub/3).

?- r@0.55.
?- ~r @ 0.6.
?- ~ -r@0.36.
?- s@0.44.
?- ~q @ Y,print(Y),nl.


?-normalize(((p,s;r)<--(s;r)),X),print(X),nl.
?-normalize(((p,s;r)<--s,r),X),print(X),nl.
?-normalize(((p,s,r)<--(s,r)),X),print(X),nl.
?-normalize(((p,s,r)<--(s;r)),X),print(X),nl.
?-normalize(((~ - ~p,s,r)<--(s;r)),X),print(X),nl.
?-normalize(((~ ~ -p,s,r)<--(s;r)),X),print(X),nl.
?- normalize((in(people,[bob,joe,andy,dan]); in(thing,[tree,door]);
     in(people,[sue,hal]); in(thing,[light,computer])),X), print(X),nl.
?- normalize((declaredClasses([a,b,c]);declaredClasses([apple,orange])),X),
   print(X),nl.
?- normalize((in(mynum,[^2:5,^10: ^20]);in(mynum,[4: ^6, ^6: ^15,
    ^18:25])),X), print(X),nl.
?- normalize((in(mynum,[^2:5,^10: ^20]);in(mynum,[4: ^6, 6: ^15,
    ^18:25])),X), print(X),nl.
?- normalize((a,b;c,d),X), print(X), nl.
?- normalize((in(a,[8:10]),in(a,[7:13]); in(a,[1:20]),in(a,[40:60])),X), print(X), nl.
?- normalize(((in(a,[1:10])<--p,q),(in(a,[5:15])<--p,r),(in(a,[9:19])<--s,t)),X), print(X),nl.
?- normalize(((in(a,[1:10])<--in(b,[-1000:5]),in(c,[100:200])),
              (in(a,[5:15])<--in(d,[-20:30]),in(e,[150:230])),
              (in(a,[4:60])<--in(f,[0:100]),in(g,[170:290]))),X),
              prettyPrint(X),nl.
?- normalize(~((in(a,[1: ^50]);in(a,[^50:100]))),X), print(X),nl.
?-  normalize((p,q,r<--((p<--q,r),(q<--s),(r<--s))),X), print(X), nl.
?- normalize((p,q,r<--((p<--q,r),(q<--s),(r<--s),s)),X), print(X),nl.
?- In=(succeed(p3,p3)<--
  ((labels(loop,p3),
   has(p3,ifthen(j=n,p4)),
   has(p4,goto(out)), 
   follows(p5,p4),
   follows(p8,p3), 
   has(p8,goto(loop)), 
   (succeed(A,B)<--follows(A,B)), 
   (succeed(X,U)<-- (has(U,goto(L)),labels(L,X))), 
   (succeed(C,E)<--(succeed(C,D),succeed(D,E))),
   (succeed(G,H)<--has(H, ifthen(Z,G)))))), 
 normalize(In,Out),prettyPrint(Out),nl.
?- nl,nl.
?- In=(succeed(p3,p3)<--
  ((labels(loop,p3),
   has(p3,ifthen(j=n,p4)),
   has(p4,goto(out)), 
   follows(p5,p4),
   follows(p9,p3), 
   has(p8,goto(loop)), 
   (succeed(p8,p3)<--follows(p8,p3)), 
   (succeed(p3,p8)<-- (has(p8,goto(loop)),labels(loop,p3))), 
   (succeed(p3,p3)<--(succeed(p3,p8),succeed(p8,p3))),
   (succeed(p4,p3)<--has(p3, ifthen(Z,p4)))))), 
 normalize(In,Out),prettyPrint(Out),nl.

 ?- normalize((p(X)<--((p(Y)<--q(Y),r(Y)),q(X),r(a))),W), print(W),nl.