/* Compute the list of labels occurring in a list of formulas */
findLabels([],[]):-!.
findLabels([[X,_]|Tail],[X|LabelsInTail]):-findLabels(Tail,LabelsInTail).


/* Given a list of labels representing worlds, generates the set of spheres for 
   each world, initialized as the empty set */
generate_empty_spheres([],[]):-!.
generate_empty_spheres([X|Tail],[[X,[]]|TailSpheres]):-generate_empty_spheres(Tail,TailSpheres).

/* Remove duplicates in a list */
remove_duplicates([],[]):-!.
remove_duplicates([X|Tail],ResTail):-member(X,Tail),!,remove_duplicates(Tail,ResTail).
remove_duplicates([X|Tail],[X|ResTail]):-remove_duplicates(Tail,ResTail).


% Generate a fresh label
freshLabel(Spheres,Gamma,Delta,NewLabel):-
    append(Gamma,Delta,Formulas),
    extractWorldsFromFormulas(Formulas,ListWorlds1),
    extractWorldsFromSpheres(Spheres,ListWorlds2),
    append(ListWorlds1,ListWorlds2,ListWorldsTemp),
    remove_duplicates(ListWorldsTemp,ListWorlds),!,
    freshLab(ListWorlds,NewLabel).
freshLab(ListWorlds,x):-true,\+member(x,ListWorlds),!.
freshLab(ListWorlds,y):-true,\+member(y,ListWorlds),!.
freshLab(ListWorlds,z):-true,\+member(z,ListWorlds),!.
freshLab(ListWorlds,r):-true,\+member(r,ListWorlds),!.
freshLab(ListWorlds,w):-true,\+member(w,ListWorlds),!.
freshLab(ListWorlds,l+1):-true,\+member(l+1,ListWorlds),!.
freshLab(ListWorlds,L+N1):-member(L+N,ListWorlds),!,N1 is N+1.


/* Maximum value in a list */
maxInList([],Max,Max):-!.
maxInList([N|Tail],Max,MaxDef):-N>Max,!,maxInList(Tail,N,MaxDef).
maxInList([_|Tail],Max,MaxDef):-maxInList(Tail,Max,MaxDef).


% memberOrdSet([Sigma,A],Delta)
% It succeeds if and only if Delta contains a block [Psi,A] such that Sigma \subseteq Psi - To this aim, ordsets are used to compare sets corresponding to lists of formulas
memberOrdSet([Sigma,A],Delta):-
    list_to_ord_set(Sigma,SigmaOrdSet),
    member([Psi,A],Delta),
    list_to_ord_set(Psi,PsiOrdSet),
    %ord_seteq(SigmaOrdSet,PsiOrdSet).
    ord_subset(SigmaOrdSet,PsiOrdSet).


/* Auxiliary predicates for building the latex source file containing a derivation of a sequent */
getRuleName(tree(axiom,_,_,_)):-write('\\mbox{\\bf axiom}'),!.
getRuleName(tree(axt,_,_,_)):-write('\\mbox{\\bf axiom}_\\top'),!.
getRuleName(tree(axf,_,_,_)):-write('\\mbox{\\bf axiom}_\\bot'),!.
getRuleName(tree(notR,_,_,_)):-write('R\\lnot'),!.
getRuleName(tree(notL,_,_,_)):-write('L\\lnot'),!.
getRuleName(tree(orR,_,_,_)):-write('R\\vee'),!.
getRuleName(tree(orL,_,_,_)):-write('L\\vee'),!.
getRuleName(tree(andR,_,_,_)):-write('R\\land'),!.
getRuleName(tree(andL,_,_,_)):-write('L\\land'),!.
getRuleName(tree(impL,_,_,_)):-write('L\\rightarrow'),!.
getRuleName(tree(impR,_,_,_)):-write('R\\rightarrow'),!.
getRuleName(tree(lbox,_,_,_)):-write('L\\square'),!.
getRuleName(tree(rbox,_,_,_)):-write('R\\square'),!.
getRuleName(tree(c,_,_,_)):-write('C'),!.
getRuleName(tree(m,_,_,_)):-write('M'),!.
getRuleName(tree(dec,_,_,_)):-write('dec'),!.
getRuleName(tree(decs,_,_,_)):-write('\\overline{dec}'),!.
getRuleName(tree(lexists,_,_,_)):-write('L\\Vdash^\\exists'),!.
getRuleName(tree(rexists,_,_,_)):-write('R\\Vdash^\\exists'),!.
getRuleName(tree(lforall,_,_,_)):-write('L\\Vdash^\\forall'),!.
getRuleName(tree(rforall,_,_,_)):-write('R\\Vdash^\\forall'),!.
getRuleName(tree(nunsigned,_,_,_)):-write('N\\tau'),!.
getRuleName(tree(nsigned,_,_,_)):-write('N\\overline{\\tau}'),!.
getFirstSon(tree(_,_,SubTree,_)):-write(SubTree),!.
getSecondSon(tree(_,_,_, SubTree)):-write(SubTree),!.

/* Auxiliary predicate extracting a node for displaying it on the web page */
getNode(tree(_,[Spheres,Gamma,Delta],_,_)):-
    listAllSpheres(Spheres),
    listAllFmls(Gamma),
    write(' \\Rightarrow '),
    listAllFmls(Delta),!.


/* Auxiliary predicates for the graphical interface */

listAllSpheres([]):-write(''),!.
listAllSpheres([[_,[]]|Tail]):-!,listAllSpheres(Tail).
listAllSpheres([[_,[]]]):-!,write('').
listAllSpheres([[X,SpheresOfX]]):-!,betterSpheres(X,SpheresOfX),write(', ').
listAllSpheres([[X,SpheresOfX]|Tail]):-betterSpheres(X,SpheresOfX),write(', '),listAllSpheres(Tail).

betterSpheres(_,[]):-!,write('').
betterSpheres(X,[N]):-!,betterNameofSphere(N),write(' \\in N('),write(X),write(')').
betterSpheres(X,[N|Tail]):-betterNameofSphere(N),write(' \\in N('),write(X),write('),'),betterSpheres(X,Tail).

betterNameofSphere(-1):-!,write('\\tau').
betterNameofSphere(1):-!,write('t').
betterNameofSphere(2):-!,write('s').
betterNameofSphere(3):-!,write('u').
betterNameofSphere(4):-!,write('v').
betterNameofSphere(comb(List)):-!,iterateOnComb(List).
betterNameofSphere(N):-write('t_'),N1 is N-4,write(N1).
betterNameofSignedSphere(-1):-!,write('\\overline{\\tau}').
betterNameofSignedSphere(1):-!,write('\\overline{t}').
betterNameofSignedSphere(2):-!,write('\\overline{s}').
betterNameofSignedSphere(3):-!,write('\\overline{u}').
betterNameofSignedSphere(4):-!,write('\\overline{v}').
betterNameofSignedSphere(comb(List)):-!,write('\\overline{'),iterateOnComb(List),write('}').
betterNameofSignedSphere(N):-write('\\overline{t_'),N1 is N-4,write(N1),write('}').

iterateOnComb([]):-!,write('').
iterateOnComb([T|Rest]):-betterNameofSphere(T),iterateOnComb(Rest).


betterNameofSphereHTML(-1):-!,write('&Tau;').
betterNameofSphereHTML(1):-!,write('t').
betterNameofSphereHTML(2):-!,write('s').
betterNameofSphereHTML(3):-!,write('u').
betterNameofSphereHTML(4):-!,write('v').
betterNameofSphereHTML(comb(List)):-!,iterateOnHTML(List).
betterNameofSphereHTML(N):-write('s'),N1 is N-4,write(N1).
betterNameofSignedSphereHTML(-1):-!,write('<SPAN STYLE="text-decoration:overline">&Tau;</SPAN>').
betterNameofSignedSphereHTML(1):-!,write('<SPAN STYLE="text-decoration:overline">t</SPAN>').
betterNameofSignedSphereHTML(2):-!,write('<SPAN STYLE="text-decoration:overline">s</SPAN>').
betterNameofSignedSphereHTML(3):-!,write('<SPAN STYLE="text-decoration:overline">u</SPAN>').
betterNameofSignedSphereHTML(4):-!,write('<SPAN STYLE="text-decoration:overline">v</SPAN>').
betterNameofSignedSphereHTML(comb(List)):-!,write('<SPAN STYLE="text-decoration:overline">'),iterateSignedOnHTML(List),write('</SPAN>').
betterNameofSignedSphereHTML(N):-write(''),N1 is N-4,write(N1),write('</SPAN>').



listAllFmls([]):-write(''),!.
listAllFmls([[X,F]]):-!,write(X),write(': '),betterFormula(F).
listAllFmls([[X,F]|Tail]):-write(X),write(': '),betterFormula(F),write(', '),listAllFmls(Tail).
listAllFmls([[T,0,X]]):-!,write(X),write(' \\in '),betterNameofSphere(T).
listAllFmls([[T,0,X]|Tail]):-!,write(X),write(' \\in '),betterNameofSphere(T),write(', '),listAllFmls(Tail).
listAllFmls([[T,1,X]]):-!,write(X),write(' \\in '),betterNameofSignedSphere(T).
listAllFmls([[T,1,X]|Tail]):-!,write(X),write(' \\in '),betterNameofSignedSphere(T),write(', '),listAllFmls(Tail).
listAllFmls([[forall,T,0,F]]):-!,betterNameofSphere(T),write(' \\models^\\forall '),betterFormula(F).
listAllFmls([[forall,T,0,F]|Tail]):-betterNameofSphere(T),write(' \\models^\\forall '),betterFormula(F),write(', '),listAllFmls(Tail).
listAllFmls([[exists,T,1,F]]):-!,betterNameofSignedSphere(T),write(' \\models^\\exists '),betterFormula(F).
listAllFmls([[exists,T,1,F]|Tail]):-betterNameofSignedSphere(T),write(' \\models^\\exists '),betterFormula(F),write(', '),listAllFmls(Tail).

betterFormula(false):-!,write('\\bot').
betterFormula(true):-!,write('\\top').
betterFormula(-A):-!,write('\\lnot ('),betterFormula(A),write(')').
betterFormula(A ^ B):-!,betterFormula(A),write(' \\land '),betterFormula(B).
betterFormula(A ? B):-!,betterFormula(A),write(' \\vee '),betterFormula(B).
betterFormula(A >> B):-!,betterFormula(A),write(' \\rightarrow '),betterFormula(B).
betterFormula(box A):-!,write(' \\square( '),betterFormula(A),write(')').
betterFormula(P):-write(P).

printTradSpheres(_,_,[]):-!.
printTradSpheres(Spheres,Fml,[X|Labels]):-
    member([X,[]],Spheres),!,
    write("N'("),write(X),write(")=&#8709;, "),
    printTradSpheres(Spheres,Fml,Labels).
printTradSpheres(Spheres,Fml,[X|Labels]):-
    member([X,TempElements],Spheres),!,
    write("N'("),write(X),write(")={"),
    signedSpheres(TempElements,ElementsWithDups),
    append(TempElements,ElementsWithDups,AllWithDups),
    remove_duplicates(AllWithDups,ElementsTemp),
    removeSigned(ElementsTemp,Elements),
    getAllAlfaBeta(Elements,Fml,AlfaBeta,[X|Labels]),
    printBetterAlfaBeta(AlfaBeta),
    write("}, "),
    printTradSpheres(Spheres,Fml,Labels).
printTradSpheres(Spheres,Fml,[X|Labels]):-
    write("N'("),write(X),write(")=&#8709;, "),
    printTradSpheres(Spheres,Fml,Labels).
						
getAllAlfaBeta([],_,[],_):-!.
getAllAlfaBeta([T|Tail],Fml,[AlfaBeta|ResTail],Worlds):-
    getWorldsInT(T,Fml,Alfa),
    getWorldsInBarT(T,Fml,Beta),
    list_to_set(Alfa,SetAlfa),
    list_to_set(Beta,SetBeta),
    list_to_set(Worlds,SetWorlds),
    subtract(SetWorlds,SetBeta,Diff),
    findall(CandidateSet,powerset(Diff,CandidateSet),ListOfCandidates),
    filterSuperSets(ListOfCandidates,SetAlfa,DefListOfCandidates),
    selectLargest(DefListOfCandidates,AlfaBeta),!,
    getAllAlfaBeta(Tail,Fml,ResTail,Worlds).
getAllAlfaBeta([_|Tail],Fml,ResTail,Worlds):-
    getAllAlfaBeta(Tail,Fml,ResTail,Worlds).

printBetterAlfaBeta([]):-!.
printBetterAlfaBeta([[]]):-!.
printBetterAlfaBeta([[]|Tail]):-!,printBetterAlfaBeta(Tail).
printBetterAlfaBeta([List]):-!,write('{'),printBetterList(List),write('}').
printBetterAlfaBeta([List|Tail]):-
    write('{'),printBetterList(List),write('},'),
    printBetterAlfaBeta(Tail).

printBetterList([X]):-!,write(X).
printBetterList([X|Tail]):-write(X),write(', '),printBetterList(Tail).

filterSuperSets([],_,[]):-!.
filterSuperSets([Candidate|Others],Alfa,[Candidate|Tail]):-
    subset(Alfa,Candidate),!,filterSuperSets(Others,Alfa,Tail).
filterSuperSets([_|Others],Alfa,Tail):-
    filterSuperSets(Others,Alfa,Tail).

powerset([], []).
powerset([_|T], P) :- powerset(T,P).
powerset([H|T], [H|P]) :- powerset(T,P).

selectLargest([Set|ListOfSets],Largest):-
    auxLargest(ListOfSets,Set,Largest).
auxLargest([],Largest,Largest):-!.
auxLargest([Set|Others],TempLargest,Largest):-
    length(Set,L),
    length(TempLargest,Max),
    L>Max,
    !,
    auxLargest(Others,Set,Largest).
auxLargest([_|Others],TempLargest,Largest):-
    auxLargest(Others,TempLargest,Largest).

signedSpheres([],[]):-!.
signedSpheres([_+s|Tail],ResTail):-!,signedSpheres(Tail,ResTail).
signedSpheres([T|Tail],[T+s|ResTail]):-signedSpheres(Tail,ResTail).

getWorldsInT(_,[],[]):-!.
getWorldsInT(T,[[T,0,X]|Tail],[X|ResTail]):-!,getWorldsInT(T,Tail,ResTail).
getWorldsInT(T,[_|Tail],ResTail):-getWorldsInT(T,Tail,ResTail).
printBetter(T,[]):-!,betterNameofSphereHTML(T),write("=&#8709;").
printBetter(T,List):-betterNameofSphereHTML(T),write("={"),writeWorlds(List),write("}").
writeWorlds([X]):-!,write(X).
writeWorlds([X|Tail]):-write(X),write(","),writeWorlds(Tail).
printWorldsFromSignedSpheres([],_):-!.
printWorldsFromSignedSpheres([T],Formulas):-!,
    getWorldsInBarT(T,Formulas,Results),
    printBarBetter(T,Results).
printWorldsFromSignedSpheres([T|Tail],Formulas):-
    getWorldsInBarT(T,Formulas,Results),
    printBarBetter(T,Results),
    write(', '),
    printWorldsFromSignedSpheres(Tail,Formulas).
getWorldsInBarT(_,[],[]):-!.
getWorldsInBarT(T,[[T,1,X]|Tail],[X|ResTail]):-!,getWorldsInBarT(T,Tail,ResTail).
getWorldsInBarT(T,[_|Tail],ResTail):-getWorldsInBarT(T,Tail,ResTail).
printBarBetter(T,[]):-!,betterNameofSignedSphereHTML(T),write("=&#8709;").
printBarBetter(T,List):-betterNameofSignedSphereHTML(T),write("={"),writeWorlds(List),write("}").


getEvaluation([],_):-!.
getEvaluation([X],Formulas):-true,\+member([X,_],Formulas),!,write("V("),write(X),write(")=&#8709;").
getEvaluation([X],Formulas):-!,write("V("),write(X),write(")={"),printAtoms(X,Formulas),write("}").
getEvaluation([X|Tail],Formulas):-write("V("),write(X),write(")={"),printAtoms(X,Formulas),write("}, "),getEvaluation(Tail,Formulas).
printAtoms(X,Formulas):-
    extractAtoms(X,Formulas,Atoms),
    printAtomicFormulas(Atoms).
extractAtoms(_,[],[]):-!.
extractAtoms(X,[[_,- _]|Tail],ResTail):-!,extractAtoms(X,Tail,ResTail).
extractAtoms(X,[[_,box _]|Tail],ResTail):-!,extractAtoms(X,Tail,ResTail).
extractAtoms(X,[[_,_ ^ _]|Tail],ResTail):-!,extractAtoms(X,Tail,ResTail).
extractAtoms(X,[[_,_ ? _]|Tail],ResTail):-!,extractAtoms(X,Tail,ResTail).
extractAtoms(X,[[_,_ >> _]|Tail],ResTail):-!,extractAtoms(X,Tail,ResTail).
extractAtoms(X,[[X,A]|Tail],[A|ResTail]):-!,extractAtoms(X,Tail,ResTail).
extractAtoms(X,[_|Tail],ResTail):-!,extractAtoms(X,Tail,ResTail).
printAtomicFormulas([]):-!,write("").
printAtomicFormulas([true]):-!,write("").
printAtomicFormulas([true|Tail]):-!,write(", "),printAtomicFormulas(Tail).
printAtomicFormulas([A]):-!,write(A).
printAtomicFormulas([A|Tail]):-write(A),write(", "),printAtomicFormulas(Tail).

extractWorldsFromSpheres([],[]):-!.
extractWorldsFromSpheres([[X,_]|Tail],[X|LabelsTail]):-!,extractWorldsFromSpheres(Tail,LabelsTail).

printOnWebPage([]):-!,write('').
printOnWebPage([X]):-!,write(X).
printOnWebPage([X|Tail]):-write(X),write(', '),printOnWebPage(Tail).

printEmptySignedSpheres(Spheres,Formulas):-
    getSpheres(Spheres,ListOfSpheres),
    printEmptySpheres(ListOfSpheres,Formulas).

getSpheres([],[]):-!.
getSpheres([[_,List]|Tail],Result):-
    getSpheres(Tail,SpheresInTail),
    append(List,SpheresInTail,Result).




  