/*
Copyright 2020 Tiziano Dalmonte, Nicola Olivetti, Gian Luca Pozzato. 
This file is part of HYPNO. HYPNO is free software: you can redistribute it and/or modify it under 
the terms of the GNU General Public License as published by the Free Software Foundation, either version 
3 of the License, or (at your option) any later version. NESCOND is distributed in the hope that it will 
be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR 
A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy 
of the GNU General Public License along with HYPNO. If not, see <http://www.gnu.org/licenses/>.
*/

/* imports */
:- use_module(library(lists)).
:- op(800,fy,-),
op(700,fy,box),
op(650,xfy,->),
op(600,xfy,^),
op(600,xfy,?).


/* Top level predicates for launching the theorem prover */

prove(Formula):-
  terminating_proof_search([singleSeq([[],[Formula]],[])],Tree),write(Tree),!.
% In case of failure, the application builds a counter model from an open saturated branch
prove(_):-write('COUNTER').
counter(Formula):-
  write('COUNTER'),
  build_saturated_branch([singleSeq([[],[Formula]],[])],model(PrintableHyper)),
  partitionPrintable(PrintableHyper,Sigma,Delta), 
  extractWorlds(Sigma,ListOfWorlds),
  write('<hr><table border="0"><tr><td width="30%">'),
  write('W = {'),
  writeListOfWorlds(ListOfWorlds),
  write('}</td><td width="15%"></td><td width="50%">'),
  length(ListOfWorlds,N),
  extractEval(Sigma,N,PropEval),
  evalPropVars(PropEval,ByPropVars),
  writeBetterPropVars(ByPropVars),
  write('</td></tr></table><hr>'),
  extractBlocks(Sigma,Sigma,Delta,N,SigmaPlus,SigmaMinus),
  extractEvalSigmas(Sigma,N,SigmaPlus,SigmaMinus,Nonmon,Monot),
  write('<h5>N (monotonic case):</h5> '),
  writeBetter(Monot),
%  write('<h5>N (non-monotonic case):</h5> '),
%  writeBetter(Nonmon),
  write('<hr>').



/* Auxiliary predicate implementing the calculi */

% Axioms
terminating_proof_search(Hyper,tree(axiom,PrintableHyper,no,no)):-
    member(singleSeq([Gamma,Delta],_),Hyper),
    member(P,Gamma),
    member(P,Delta),
    !,
    extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(axf,PrintableHyper,no,no)):-
    member(singleSeq([Gamma,_],_),Hyper),
    member(false,Gamma),
    !,
    extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(axt,PrintableHyper,no,no)):-
    member(singleSeq([_,Delta],_),Hyper),
    member(true,Delta),
    !,
    extractPrintableSequents(Hyper,PrintableHyper).

% Rule N
terminating_proof_search(Hyper,tree(n,PrintableHyper,SubTree,no)):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    \+member(n,Additional),
    !,
    terminating_proof_search([singleSeq([[[true]|Gamma],Delta],[n|Additional])|NewHyper],SubTree),
    extractPrintableSequents(Hyper,PrintableHyper).


% []L
terminating_proof_search(Hyper,tree(lbox,PrintableHyper,SubTree,no)):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(box A,Gamma),
    \+member(box A,Additional),
    !,
    terminating_proof_search([singleSeq([[[A]|Gamma],Delta],[box A|Additional])|NewHyper],SubTree),
    extractPrintableSequents(Hyper,PrintableHyper).

% M[]R
terminating_proof_search(Hyper,tree(mrbox,PrintableHyper,Sub1,no)):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),   
    member(Sigma,Gamma),
    is_list(Sigma),
    member(box B,Delta),
    list_to_ord_set(Sigma,SigmaOrd),
    \+member(apdR(SigmaOrd,B),Additional),
    !,
    terminating_proof_search([singleSeq([Sigma,[B]],[])|[singleSeq([Gamma,Delta],[apdR(SigmaOrd,B)|Additional])|NewHyper]],Sub1),
    extractPrintableSequents(Hyper,PrintableHyper).


% Rules for boolean connectives
terminating_proof_search(Hyper,tree(andL,PrintableHyper,SubTree,no)):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A ^ B,Gamma),
    \+member(left(A ^ B),Additional),
    !,
    terminating_proof_search([singleSeq([[A|[B|Gamma]],Delta],[left(A ^ B)|Additional])|NewHyper],SubTree), 
    extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(orR,PrintableHyper,SubTree,no)):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A ? B,Delta),
    \+member(right(A ? B),Additional),
    !,
    terminating_proof_search([singleSeq([Gamma,[A|[B|Delta]]],[right(A ? B)|Additional])|NewHyper],SubTree), 
    extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(notL,PrintableHyper,SubTree,no)):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(-A,Gamma),
    \+member(left(-A),Additional),
    !,
    terminating_proof_search([singleSeq([Gamma,[A|Delta]],[left(-A)|Additional])|NewHyper],SubTree), 
    extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(notR,PrintableHyper,SubTree,no)):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(-A,Delta),
    \+member(right(-A),Additional),
    !,
    terminating_proof_search([singleSeq([[A|Gamma],Delta],[right(-A)|Additional])|NewHyper],SubTree), 
    extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(impR,PrintableHyper,SubTree,no)):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A -> B,Delta),
    \+member(right(A -> B),Additional),
    !,
    terminating_proof_search([singleSeq([[A|Gamma],[B|Delta]],[right(A -> B)|Additional])|NewHyper],SubTree), 
    extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(andR,PrintableHyper,Sub1,Sub2)):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A ^ B,Delta),
    \+member(right(A ^ B),Additional),
    !,
    terminating_proof_search([singleSeq([Gamma,[A|Delta]],[right(A ^ B)|Additional])|NewHyper],Sub1), 
    terminating_proof_search([singleSeq([Gamma,[B|Delta]],[right(A ^ B)|Additional])|NewHyper],Sub2), 
    extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(orL,PrintableHyper,Sub1,Sub2)):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A ? B,Gamma),
    \+member(left(A ? B),Additional),
    !,
    terminating_proof_search([singleSeq([[A|Gamma],Delta],[left(A ? B)|Additional])|NewHyper],Sub1), 
    terminating_proof_search([singleSeq([[B|Gamma],Delta],[left(A ? B)|Additional])|NewHyper],Sub2), 
    extractPrintableSequents(Hyper,PrintableHyper).
terminating_proof_search(Hyper,tree(impL,PrintableHyper,Sub1,Sub2)):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A -> B,Gamma),
    \+member(left(A -> B),Additional),
    !,
    terminating_proof_search([singleSeq([Gamma,[A|Delta]],[left(A -> B)|Additional])|NewHyper],Sub1), 
    terminating_proof_search([singleSeq([[B|Gamma],Delta],[left(A -> B)|Additional])|NewHyper],Sub2), 
    extractPrintableSequents(Hyper,PrintableHyper).



% Predicate checking whether a sequent is an instance of an axiom
instanceOfAnAxiom(Hyper):-
    member(singleSeq([Gamma,Delta],_),Hyper),
    member(P,Gamma),
    member(P,Delta),
    !.
instanceOfAnAxiom(Hyper):-
    member(singleSeq([Gamma,_],_),Hyper),
    member(false,Gamma),
    !.
instanceOfAnAxiom(Hyper):-
    member(singleSeq([_,Delta],_),Hyper),
    member(true,Delta),!.


/* Auxiliary predicate implementing the construction of a countermodel */

% Rule N
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    \+member(n,Additional),
    !,
    build_saturated_branch([singleSeq([[[true]|Gamma],Delta],[n|Additional])|NewHyper],Model).

% []L
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(box A,Gamma),
    \+member(box A,Additional),
    !,
    build_saturated_branch([singleSeq([[[A]|Gamma],Delta],[box A|Additional])|NewHyper],Model).


% M[]R
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),   
    member(Sigma,Gamma),
    is_list(Sigma),
    member(box B,Delta),
    list_to_ord_set(Sigma,SigmaOrd),
    \+member(apdR(SigmaOrd,B),Additional),
    build_saturated_branch([singleSeq([Sigma,[B]],[])|[singleSeq([Gamma,Delta],[apdR(SigmaOrd,B)|Additional])|NewHyper]],Model).

% Rules for boolean connectives
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A ^ B,Gamma),
    \+member(left(A ^ B),Additional),
    !,
    build_saturated_branch([singleSeq([[A|[B|Gamma]],Delta],[left(A ^ B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A ? B,Delta),
    \+member(right(A ? B),Additional),
    !,
    build_saturated_branch([singleSeq([Gamma,[A|[B|Delta]]],[right(A ? B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(-A,Gamma),
    \+member(left(-A),Additional),
    !,
    build_saturated_branch([singleSeq([Gamma,[A|Delta]],[left(-A)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(-A,Delta),
    \+member(right(-A),Additional),
    !,
    build_saturated_branch([singleSeq([[A|Gamma],Delta],[right(-A)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A -> B,Delta),
    \+member(right(A -> B),Additional),
    !,
    build_saturated_branch([singleSeq([[A|Gamma],[B|Delta]],[right(A -> B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A ^ B,Delta),
    \+member(right(A ^ B),Additional),
    build_saturated_branch([singleSeq([Gamma,[A|Delta]],[right(A ^ B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A ^ B,Delta),
    \+member(right(A ^ B),Additional),
    build_saturated_branch([singleSeq([Gamma,[B|Delta]],[right(A ^ B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A ? B,Gamma),
    \+member(left(A ? B),Additional),
    build_saturated_branch([singleSeq([[A|Gamma],Delta],[left(A ? B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A ? B,Gamma),
    \+member(left(A ? B),Additional),
    build_saturated_branch([singleSeq([[B|Gamma],Delta],[left(A ? B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A -> B,Gamma),
    \+member(left(A -> B),Additional),
    build_saturated_branch([singleSeq([Gamma,[A|Delta]],[left(A -> B)|Additional])|NewHyper],Model).
build_saturated_branch(Hyper,Model):-
    select(singleSeq([Gamma,Delta],Additional),Hyper,NewHyper),
    member(A -> B,Gamma),
    \+member(left(A -> B),Additional),
    build_saturated_branch([singleSeq([[B|Gamma],Delta],[left(A -> B)|Additional])|NewHyper],Model).


% If no further rule is applicable and the branch is not closed, we have found a closed saturated branch and we are done
build_saturated_branch(Hyper,model(Hyper)):-
    true,
    \+instanceOfAnAxiom(Hyper).
 %    extractPrintableSequents(Hyper,PrintableHyper),


% Auxiliary predicates for building the countermodel and showing it by means of the graphical interface

extractPrintableSequents([],[]):-!.
extractPrintableSequents([singleSeq([Sigma,Delta],_)|Tail],[[Sigma,Delta]|PrintTail]):-
    !,
    extractPrintableSequents(Tail,PrintTail).

writeBetterPropVars([]):-!,write(' For all atomic variables P, V(P)=&#8709;').
writeBetterPropVars([[P,[]]]):-
    write('V('),write(P),write(')=&#8709;'),write('<br>For all other atomic variables P (if any), V(P)=&#8709;').
writeBetterPropVars([[P,[]]|Tail]):-
    write('V('),write(P),write(')=&#8709;, '),writeBetterPropVars(Tail).
writeBetterPropVars([[P,ListOfWorlds]]):-
    write('V('),write(P),write(')={'),writeListOfWorlds(ListOfWorlds),write('}'),write('<br>For all other atomic variables P (if any), V(P)=&#8709;').
writeBetterPropVars([[P,ListOfWorlds]|Tail]):-
    write('V('),write(P),write(')={'),writeListOfWorlds(ListOfWorlds),
    write('}, '),writeBetterPropVars(Tail).

evalPropVars(PropEval,ByPropVars):-
    listOfAtomicFormulas(PropEval,Atoms),
    whereAtomIsTrue(Atoms,PropEval,ByPropVars).

whereAtomIsTrue([],_,[]):-!.
whereAtomIsTrue([P|OtherAtoms],PropEval,[[P,ListOfWorlds]|RestOfAtoms]):-
    findall(W,(member([W,WEval],PropEval),member(P,WEval)),ListOfWorlds),
    whereAtomIsTrue(OtherAtoms,PropEval,RestOfAtoms).

listOfAtomicFormulas([],[]):-!.
listOfAtomicFormulas([[_,ListOfFormulas]|Tail],DefAtoms):-
    listOfAtoms(ListOfFormulas,Atoms),
    listOfAtomicFormulas(Tail,ResTail),
    list_to_ord_set(Atoms,A1),
    list_to_ord_set(ResTail,A2),
    ord_union(A1,A2,DefAtoms).

listOfAtoms([],[]):-!.
listOfAtoms([true|Tail],ResTail):-!,listOfAtoms(Tail,ResTail).
listOfAtoms([false|Tail],ResTail):-!,listOfAtoms(Tail,ResTail).
listOfAtoms([Fml|Tail],[Fml|ResTail]):-atom(Fml),!,listOfAtoms(Tail,ResTail).
listOfAtoms([_|Tail],ResTail):-listOfAtoms(Tail,ResTail).

writeListOfWorlds([W]):-write(W),!.
writeListOfWorlds([W|Tail]):-write(W),write(', '),writeListOfWorlds(Tail).

writeFormulas([]):-!.
writeFormulas([Fml]):-!,write(Fml).
writeFormulas([Fml|Tail]):-write(Fml),write(', '),writeFormulas(Tail).

writeBetter([]):-!.
writeBetter([(N,[])|Tail]):-
    write('N('),write(N),write(')=&#8709;<br>'),
    writeBetter(Tail).
writeBetter([(N,List)|Tail]):-
    write('N('),write(N),write(')={'),
    writeList(List),
    write('}<br>'),
    writeBetter(Tail).

writeList([(Plus,Minus)]):-!,
    write('('),
    write(Plus),
    write(','),
    write(Minus),
    write(')').
writeList([(Plus,Minus)|Tail]):-!,
    write('('),
    write(Plus),
    write(','),
    write(Minus),
    write('),'),
    writeList(Tail).

extractEvalSigmas([],_,_,_,[],[]):-!.
extractEvalSigmas([Hyper|Tail],N,SigmaPlus,SigmaMinus,[(N,MonotBlock)|MonotOthers],[(N,NonmonBlock)|NonmonOthers]):-
    valBlocks(Hyper,N,SigmaPlus,SigmaMinus,MonotBlock,NonmonBlock),
    N1 is N-1,
    extractEvalSigmas(Tail,N1,SigmaPlus,SigmaMinus,MonotOthers,NonmonOthers).

valBlocks([],_,_,_,[],[]):-!.
valBlocks([Block|Tail],N,SigmaPlus,SigmaMinus,[(SP,SM)|Monot],[(SP,[])|Nonmon]):-
    is_list(Block),
    !,
    flatten(SigmaPlus,FlatSP),
    flatten(SigmaMinus,FlatSM),
    member(plus(Block,SP),FlatSP),
    member(minus(Block,SM),FlatSM),
    valBlocks(Tail,N,SigmaPlus,SigmaMinus,Monot,Nonmon).
valBlocks([_|Tail],N,SigmaPlus,SigmaMinus,Monot,Nonmon):-
    valBlocks(Tail,N,SigmaPlus,SigmaMinus,Monot,Nonmon).

extractBlocks([],_,_,_,[],[]):-!.
extractBlocks([Hyper|Tail],Sigma,Delta,N,[HyperPlus|TailPlus],[HyperMinus|TailMinus]):-
    forEachBlock(Hyper,Sigma,Delta,N,HyperPlus,HyperMinus),
    extractBlocks(Tail,Sigma,Delta,N,TailPlus,TailMinus).

forEachBlock([],_,_,_,[],[]):-!.
forEachBlock([Block|Tail],Sigma,Delta,N,[plus(Block,BlockPlus)|TailPlus],[minus(Block,BlockMinus)|TailMinus]):-
    is_list(Block),!,
    blockSetPlus(Block,Sigma,N,BlockPlus),
    blockSetMinus(Block,Delta,N,BlockMinus),
    forEachBlock(Tail,Sigma,Delta,N,TailPlus,TailMinus).
forEachBlock([_|Tail],Sigma,Delta,N,TailPlus,TailMinus):-
    forEachBlock(Tail,Sigma,Delta,N,TailPlus,TailMinus).

partitionPrintable([],[],[]):-!.
partitionPrintable([singleSeq([Sigma,Delta],_)|Tail],[Sigma|SigmaTail],[Delta|DeltaTail]):-
    partitionPrintable(Tail,SigmaTail,DeltaTail).

% blockSetPlus(Block,Model,N,SigmaPlus)
blockSetPlus(_,_,0,[]):-!.
blockSetPlus(Block,[Hyper|Rest],N,[N|Others]):-
    list_to_ord_set(Block,SetSigma),
    list_to_ord_set(Hyper,SetHyper),
    ord_subset(SetSigma,SetHyper),
    !,
    N1 is N-1,
    blockSetPlus(Block,Rest,N1,Others).
blockSetPlus(Block,[_|Rest],N,Others):-
    N1 is N-1,
    blockSetPlus(Block,Rest,N1,Others).

% blockSetMinus(Block,Model,N,SigmaMinus)
blockSetMinus(_,_,0,[]):-!.
blockSetMinus(Block,[Hyper|Rest],N,Others):-
    intersection(Block,Hyper,[]),
    !,
    N1 is N-1,
    blockSetMinus(Block,Rest,N1,Others).
blockSetMinus(Block,[_|Rest],N,[N|Others]):-
    N1 is N-1,
    blockSetMinus(Block,Rest,N1,Others).

extractEval([],_,[]):-!.
extractEval([SatSeq|Tail],N,[[N,PropEvalCurSatSeq]|PropEvalOthers]):-
    auxPropEval(SatSeq,PropEvalCurSatSeq),
    N1 is N-1,
    extractEval(Tail,N1,PropEvalOthers).
auxPropEval([],[]):-!.
auxPropEval([List|Tail],PropEvalTail):-is_list(List),!,auxPropEval(Tail,PropEvalTail).
auxPropEval([Head|Tail],[Head|ResTail]):-auxPropEval(Tail,ResTail).

extractWorlds(Hyper,ListOfWorlds):-length(Hyper,N),buildWorlds(N,ListOfWorlds).
buildWorlds(0,[]):-!.
buildWorlds(N,[N|Tail]):-N1 is N-1,buildWorlds(N1,Tail).


/* 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).




/* Auxiliary predicates for building the latex source file containing a derivation of a sequent */
getRuleName(tree(axiom,_,_,_)):-write('\\mbox{\\bf init}'),!.
getRuleName(tree(axt,_,_,_)):-write('\\top_R'),!.
getRuleName(tree(axf,_,_,_)):-write('\\bot_L'),!.
getRuleName(tree(notR,_,_,_)):-write('\\lnot_R'),!.
getRuleName(tree(notL,_,_,_)):-write('\\lnot_L'),!.
getRuleName(tree(orR,_,_,_)):-write('\\vee_R'),!.
getRuleName(tree(orL,_,_,_)):-write('\\vee_L'),!.
getRuleName(tree(n,_,_,_)):-write('N'),!.
getRuleName(tree(c,_,_,_)):-write('C'),!.
getRuleName(tree(m,_,_,_)):-write('M'),!.
getRuleName(tree(prv,_,_,_)):-write('E\\Rrightarrow'),!.
getRuleName(tree(andR,_,_,_)):-write('\\land_R'),!.
getRuleName(tree(andL,_,_,_)):-write('\\land_L'),!.
getRuleName(tree(impL,_,_,_)):-write('\\rightarrow_L'),!.
getRuleName(tree(impR,_,_,_)):-write('\\rightarrow_R'),!.
getRuleName(tree(lbox,_,_,_)):-write('\\square_L'),!.
getRuleName(tree(rbox,_,_,_)):-write('\\square_R'),!.
getRuleName(tree(mrbox,_,_,_)):-write('M\\square_R'),!.
getFirstSon(tree(_,_,SubTree,_)):-write(SubTree),!.
getSecondSon(tree(_,_,_, SubTree)):-write(SubTree),!.


getNode(tree(_,HyperSequent,_,_)):-
  listAllHyper(HyperSequent),!.

listAllHyper([[Sigma,Delta]]):-
    listAllFmls(Sigma),
    write(' \\Rightarrow '),
    listAllFmls(Delta).
listAllHyper([[Sigma,Delta]|OtherSeqs]):-
    listAllFmls(Sigma),
    write(' \\Rightarrow '),
    listAllFmls(Delta),
    write(' \\ \\mid \\ '),
    listAllHyper(OtherSeqs).

listAllFmls([]):-!.
listAllFmls([Fml]):-
    is_list(Fml),!,
    write('\\langle '),
    listAllFmls(Fml),
    write('\\rangle ').
listAllFmls([Fml]):-
    betterFormula(Fml).
listAllFmls([Fml|Tail]):-
    is_list(Fml),!,
    write('\\langle '),
    listAllFmls(Fml),
    write('\\rangle, '),
    listAllFmls(Tail).
listAllFmls([Fml|Tail]):-
    betterFormula(Fml),
    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).

						

printAtomicFormulas([]):-!,write("").
printAtomicFormulas([true]):-!,write("").
printAtomicFormulas([true|Tail]):-!,write(", "),printAtomicFormulas(Tail).
printAtomicFormulas([A]):-!,write(A).
printAtomicFormulas([A|Tail]):-write(A),write(", "),printAtomicFormulas(Tail).


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

