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


prova(Formula):-prove([[],[Formula]],Tree),write(Tree),!.
prova(_):-write('Not Valid').


/* Axioms closing branches */
prove([Gamma,Delta],tree(axb,[Gamma,Delta],no,no)):-member(false,Gamma),!.
prove([Gamma,Delta],tree(axt,[Gamma,Delta],no,no)):-member(true,Delta),!.
prove([Gamma,Delta],tree(init,[Gamma,Delta],no,no)):-member(P,Gamma),member(P,Delta),!.


/* Rules with one premise */
prove([Gamma,Delta],tree(negL,[Gamma,Delta],SubTree,no)):-
  select(-A,Gamma,NewGamma),\+member(A,Delta),!,prove([NewGamma,[A|Delta]],SubTree).
prove([Gamma,Delta],tree(negR,[Gamma,Delta],SubTree,no)):-
  select(-A,Delta,NewDelta),\+member(A,Gamma),!,prove([[A|Gamma],NewDelta],SubTree).
prove([Gamma,Delta],tree(impR,[Gamma,Delta],SubTree,no)):-
  select(A->B,Delta,NewDelta),(\+member(A,Gamma);\+member(B,NewDelta)),!,prove([[A|Gamma],[B|NewDelta]],SubTree).
prove([Gamma,Delta],tree(andL,[Gamma,Delta],SubTree,no)):-
  select(A^B,Gamma,NewGamma),(\+member(A,NewGamma);\+member(B,NewGamma)),!,prove([[A,B|NewGamma],Delta],SubTree).
prove([Gamma,Delta],tree(orR,[Gamma,Delta],SubTree,no)):-
  select(A ? B,Delta,NewDelta),(\+member(A,NewDelta);\+member(B,NewDelta)),!,prove([Gamma,[A,B|NewDelta]],SubTree).
prove([Gamma,Delta],tree(n,[Gamma,Delta],SubTree,no)):-
  \+memberOrdSet([[false],true],Delta),Gamma \== [true],Delta \== [false],!,prove([Gamma,[[[false],true]|Delta]],SubTree).
prove([Gamma,Delta],tree(precR,[Gamma,Delta],SubTree,no)):-
  select(A < B,Delta,NewDelta),\+memberOrdSet([[A],B],Delta),!,prove([Gamma,[[[A],B]|NewDelta]],SubTree).
prove([Gamma,Delta],tree(condR,[Gamma,Delta],SubTree,no)):-
  select(A=>B,Delta,NewDelta),
  (\+member((A^(-B)) < A,Gamma);\+memberOrdSet([[false],A],NewDelta)),
  !,
  prove([[(A^(-B)) < A|Gamma],[[[false],A]|NewDelta]],SubTree).  

/* Rules with two premises */
prove([Gamma,Delta],tree(impL,[Gamma,Delta],Sub1,Sub2)):-
  select(A->B,Gamma,NewGamma),\+member(B,NewGamma),\+member(A,Delta),!,prove([[B|NewGamma],Delta],Sub1),prove([NewGamma,[A|Delta]],Sub2).
prove([Gamma,Delta],tree(andR,[Gamma,Delta],Sub1,Sub2)):-
  select(A^B,Delta,NewDelta),\+member(A,NewDelta),\+member(B,NewDelta),!,prove([Gamma,[A|NewDelta]],Sub1),prove([Gamma,[B|NewDelta]],Sub2).
prove([Gamma,Delta],tree(orL,[Gamma,Delta],Sub1,Sub2)):-
  select(A ? B,Gamma,NewGamma),\+member(A,NewGamma),\+member(B,NewGamma),!,prove([[A|NewGamma],Delta],Sub1),prove([[B|NewGamma],Delta],Sub2).
prove([Gamma,Delta],tree(condL,[Gamma,Delta],Sub1,Sub2)):-
  select(A => B,Gamma,NewGamma),
  \+member(false < A,NewGamma),\+memberOrdSet([[A ^ (-(B))],A],Delta),!,
  prove([[false < A|NewGamma],Delta],Sub1),
  prove([NewGamma,[[[A^(-B)],A]|Delta]],Sub2).
prove([Gamma,Delta],tree(t,[Gamma,Delta],Sub1,Sub2)):-
  member(A < B,Gamma),
  \+member(B,Delta),
  \+memberOrdSet([[false],A],Delta),
  !,
  prove([Gamma,[B|Delta]],Sub1),
  prove([Gamma,[[[false],A]|Delta]],Sub2).
prove([Gamma,Delta],tree(com,[Gamma,Delta],Sub1,Sub2)):-
  select([Sigma1,A],Delta,Temp),
  select([Sigma2,B],Temp,NewDelta),
  append(Sigma1,Sigma2,NewSigma),
  remove_duplicates(NewSigma,SigmaDef),
  \+memberOrdSet([SigmaDef,A],Delta),
  \+memberOrdSet([SigmaDef,B],Delta),
  !,
  prove([Gamma,[[SigmaDef,A],[Sigma2,B]|NewDelta]],Sub1),
  prove([Gamma,[[SigmaDef,B],[Sigma1,A]|NewDelta]],Sub2).
prove([Gamma,Delta],tree(precL,[Gamma,Delta],Sub1,Sub2)):-
  member(A < B,Gamma),select([Sigma,C],Delta,NewDelta),
  remove_duplicates([B|Sigma],NewSigma),
  \+memberOrdSet([NewSigma,C],Delta),
  \+memberOrdSet([Sigma,A],Delta),!,
  prove([Gamma,[[NewSigma,C]|NewDelta]],Sub1),
  prove([Gamma,[[Sigma,A]|Delta]],Sub2).

/* Jump rule */
prove([Gamma,Delta],tree(jump,[Gamma,Delta],SubTree,no)):-member([Sigma,A],Delta),prove([[A],Sigma],SubTree).



% 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).



% It removes duplicated items in the list
remove_duplicates([],[]):-!.
remove_duplicates([Head|Tail],NewTail):-member(Head,Tail),!,remove_duplicates(Tail,NewTail).
remove_duplicates([Head|Tail],[Head|NewTail]):-remove_duplicates(Tail,NewTail).



/* Auxiliary predicates for building the latex source file containing a derivation of a sequent */
getRuleName(tree(init,_,_,_)):-write('\\mbox{\\bf init}'),!.
getRuleName(tree(axt,_,_,_)):-write('\\top_R'),!.
getRuleName(tree(axb,_,_,_)):-write('\\bot_L'),!.
getRuleName(tree(orR,_,_,_)):-write('\\vee_R'),!.
getRuleName(tree(orL,_,_,_)):-write('\\vee_L'),!.
getRuleName(tree(impR,_,_,_)):-write('\\rightarrow_R'),!.
getRuleName(tree(impL,_,_,_)):-write('\\rightarrow_L'),!.
getRuleName(tree(condR,_,_,_)):-write('\\boxright_R'),!.
getRuleName(tree(condL,_,_,_)):-write('\\boxright_L'),!.
getRuleName(tree(andR,_,_,_)):-write('\\land_R'),!.
getRuleName(tree(andL,_,_,_)):-write('\\land_L'),!.
getRuleName(tree(precR,_,_,_)):-write('\\preccurlyeq_R'),!.
getRuleName(tree(precL,_,_,_)):-write('\\preccurlyeq_L'),!.
getRuleName(tree(negR,_,_,_)):-write('\\lnot_R'),!.
getRuleName(tree(negL,_,_,_)):-write('\\lnot_L'),!.
getRuleName(tree(com,_,_,_)):-write('\\mbox{\\bf com}'),!.
getRuleName(tree(jump,_,_,_)):-write('\\mbox{\\bf jump}'),!.
getRuleName(tree(n,_,_,_)):-write('\\mbox{\\bf N}'),!.
getRuleName(tree(t,_,_,_)):-write('\\mbox{\\bf T}^{\\mbox{i}}'),!.
getFirstSon(tree(_,_,SubTree,_)):-write(SubTree),!.
getSecondSon(tree(_,_,_, SubTree)):-write(SubTree),!.


%getNode(tree(_,Node,_,_)):-betterNode(Node,BNode),listAllFmls(BNode),!.
getNode(tree(_,[Gamma,Delta],_,_)):-listAllFmls(Gamma),write(' \\Rightarrow '),listAllFmls(Delta),!.

listAllFmls([]):-write(''),!.
listAllFmls([[ListOfFormulas,A]]):-is_list(ListOfFormulas),!,write('['),listAllFmls(ListOfFormulas),write(' \\vartriangleleft '),betterFormula(A),write(']').
listAllFmls([F]):-!,betterFormula(F).
listAllFmls([[ListOfFormulas,A]|Tail]):-is_list(ListOfFormulas),!,write('['),listAllFmls(ListOfFormulas),write(' \\vartriangleleft '),betterFormula(A),write('], '),listAllFmls(Tail).
listAllFmls([F|Tail]):-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(A => B):-!,betterFormula(A),write(' \\boxright '),betterFormula(B).
betterFormula(A < B):-!,betterFormula(A),write(' \\preccurlyeq '),betterFormula(B).
betterFormula(P):-write(P).

						
