/*
Copyright 2019 Bjoern Lellman, Marianna Girlando, Nicola Olivetti, Stefano Pesce, Gian Luca Pozzato. 
This file is part of tuCLEVER. tuCLEVER 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. tuCLEVER 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 tuCLEVER. If not, see <http://www.gnu.org/licenses/>.
*/

:- use_module(library(lists)).

:- op(400,fy,-),
   op(100,fy,transfer),
   op(650,xfy,->),
   op(600,xfy,and),
   op(610,xfy,or),
   op(700,xfy,<).

/*
Default time limit is 10 seconds. Feel free to change it according to your needs.
*/
prova(Formula,FileName) :-
 catch(
    (call_with_time_limit(10,prove([[[],[Formula]]],Tree)),stampa(Tree,FileName),writeln("Valid.")),
    time_limit_exceeded,
    (writeln("Timeout."))),
  !.

prova(_,_) :-
  writeln("Not valid.").

prova(Formula):-
  prove([[[],[Formula]]],_),writeln("Valid."),!.

prova(_):-
  writeln("Not valid.").

prova2(Formula):-
  prove([[[Formula],[]]],_),writeln("Valid."),!.

prova2(_):-
  writeln("Not valid.").

/**************** AXIOM SCHEMATA ************************/

prove(Hypersequent, tree(falseL,Hypersequent,[Gamma,Delta],no, no, no)) :-
	member([Gamma,Delta],Hypersequent), member(false,Gamma),!.

prove(Hypersequent, tree(trueR,Hypersequent,[Gamma,Delta],no, no, no)) :-
  member([Gamma,Delta], Hypersequent), member(true,Delta),!.

prove(Hypersequent, tree(init,Hypersequent,[Gamma,Delta],no,no,no)) :-
	member([Gamma,Delta],Hypersequent), member(X,Gamma), member(X,Delta), atom(X),!.



/*--------------- ONE PREMISE RULES -------------------*/

prove(Hypersequent, tree(orR,Hypersequent,[Gamma,Delta],no, SubTree1, no)) :-
  select([Gamma,Delta], Hypersequent, Remainder),
  member(A or B, Delta),
  (\+member(A,Delta) ; \+member(B,Delta)),
  !,
  prove([[Gamma,[A,B|Delta]]|Remainder],SubTree1).

prove(Hypersequent, tree(notL,Hypersequent,[Gamma,Delta],no, SubTree1, no)) :-
  select([Gamma,Delta], Hypersequent, Remainder),
  member(- A, Gamma),
  \+member(A,Delta),
  !,
  prove([[Gamma,[A|Delta]]|Remainder],SubTree1).

prove(Hypersequent, tree(notR,Hypersequent,[Gamma,Delta],no, SubTree1,no)) :-
  select([Gamma,Delta], Hypersequent, Remainder),
  member(- A, Delta),
  \+member(A,Gamma),
  !,
  prove([[[A|Gamma],Delta]|Remainder],SubTree1).

prove(Hypersequent, tree(andL,Hypersequent,[Gamma,Delta],no,SubTree1, no)) :-
  select([Gamma,Delta], Hypersequent, Remainder),
  member(A and B, Gamma),
  (\+member(A,Gamma); \+member(B,Gamma)),
  !,
  prove([[[A,B|Gamma],Delta]|Remainder],SubTree1).

prove(Hypersequent, tree(implR,Hypersequent,[Gamma,Delta],no,SubTree1, no)) :-
	select([Gamma,Delta], Hypersequent, Remainder),
	member(A -> B, Delta),
  (\+member(A,Gamma); \+member(B,Delta)),
	!,
	prove([[[A|Gamma],[B|Delta]]|Remainder],SubTree1).

prove(Hypersequent, tree(in,Hypersequent,[Gamma,Delta],no,SubTree1, no)) :-
	select([Gamma,Delta],Hypersequent, Remainder) ,
	\+member(transfer (_), Delta),
	!,
	prove([[Gamma,[transfer [false]|Delta]]|Remainder],SubTree1).

prove(Hypersequent, tree(jumpT,Hypersequent,[Gamma,Delta],no,SubTree1,no)) :-
	select([Gamma,Delta], Hypersequent, Remainder),
	member(transfer Theta, Delta),
  \+subset(Theta,Delta),
	append(Delta, Theta, NewDelta),
	!,
	prove([[Gamma,NewDelta]|Remainder],SubTree1).

prove(Hypersequent, tree(jumpU,Hypersequent,[Gamma,Delta],[Gamma2,Delta2],SubTree1,no)) :-
	select([Gamma,Delta], Hypersequent, Remainder),
	member(transfer Theta, Delta),
	select([Gamma2,Delta2], Remainder, Remainder2),
  \+subset(Theta,Delta2),
	append(Delta2,Theta,NewDelta2),
	!,
	prove([[Gamma,Delta],[Gamma2,NewDelta2]|Remainder2],SubTree1).

prove(Hypersequent, tree(jump,Hypersequent,[Gamma,Delta],no,SubTree1,no)) :-
  select([Gamma,Delta],Hypersequent,Remainder),
  member([Sigma,A],Delta),
  \+findSequent(Hypersequent,[[A],Sigma]),
  !,
  prove([[Gamma,Delta],[[A],Sigma]|Remainder],SubTree1).

prove(Hypersequent, tree(precR,Hypersequent,[Gamma,Delta],no, SubTree1,no)) :-
  select([Gamma,Delta], Hypersequent,Remainder),
  member(A < B, Delta),
  \+findBlock(Delta,[[A],B]),
  !,
  prove([[Gamma,[[[A],B]|Delta]]|Remainder],SubTree1).

/*
prove(Hypersequent, tree(w,Hypersequent,[Gamma,Delta],no,SubTree1,no)) :-
  select([Gamma,Delta], Hypersequent,Remainder),
  member([Sigma,_],Delta),
  \+subset(Sigma,Delta),
  append(Delta,Sigma,NewDelta),
  !,
  prove([[Gamma,NewDelta]|Remainder],SubTree1).
*/
prove(Hypersequent, tree(absR,Hypersequent,[Gamma,Delta],[Gamma2,Delta2],SubTree1, no)) :-
  select([Gamma,Delta], Hypersequent, Remainder),
  member(A < B, Delta),
  select([Gamma2,Delta2], Remainder, Remainder2),
  \+member(A < B, Delta2),
  !,
  prove([[Gamma,Delta], [Gamma2,[A < B|Delta2]]|Remainder2],SubTree1).

prove(Hypersequent, tree(absL,Hypersequent,[Gamma,Delta],[Gamma2,Delta2], SubTree1, no)) :-
  select([Gamma,Delta], Hypersequent, Remainder),
  member(A < B, Gamma),
  select([Gamma2,Delta2], Remainder, Remainder2),
  \+member(A < B, Gamma2),
  !,
  prove([[Gamma,Delta], [[A < B|Gamma2],Delta2]|Remainder2],SubTree1).

/*----------------- TWO PREMISES RULES -------------------------*/

prove(Hypersequent, tree(orL, Hypersequent,[Gamma,Delta],no, SubTree1, SubTree2)) :-
  select([Gamma,Delta],Hypersequent,Remainder),
  member(A or B, Gamma),
  \+member(A,Gamma),
  \+member(B,Gamma),
  !,
  prove([[[A|Gamma],Delta]|Remainder],SubTree1),
  prove([[[B|Gamma], Delta]|Remainder],SubTree2).

prove(Hypersequent, tree(andR,Hypersequent,[Gamma,Delta],no, SubTree1, SubTree2)) :-
  select([Gamma,Delta], Hypersequent, Remainder),
  member(A and B, Delta),
  \+member(A,Delta),
  \+member(B,Delta),
  !,
  prove([[Gamma,[A|Delta]]|Remainder],SubTree1),
  prove([[Gamma,[B|Delta]]|Remainder],SubTree2).

prove(Hypersequent, tree(implL,Hypersequent,[Gamma,Delta],no, SubTree1, SubTree2)) :-
  select([Gamma,Delta], Hypersequent, Remainder),
  member(A -> B, Gamma),
  \+member(A,Delta),
  \+member(B,Gamma),
  !,
  prove([[[B|Gamma],Delta]|Remainder],SubTree1),
  prove([[Gamma,[A|Delta]]|Remainder],SubTree2).

prove(Hypersequent, tree(c,Hypersequent,[Gamma,Delta],no,SubTree1,SubTree2)) :-
  select([Gamma,Delta], Hypersequent,Remainder),
  member(C < D, Gamma),
  \+member(C,Gamma),
  \+member(D,Delta),
  !,
  prove([[[C|Gamma],Delta]|Remainder],SubTree1),
  prove([[Gamma,[D|Delta]]|Remainder],SubTree2).

prove(Hypersequent, tree(precL,Hypersequent,[Gamma,Delta],no, SubTree1, SubTree2)) :-
  select([Gamma,Delta], Hypersequent, Remainder),
  select([Sigma,A], Delta,Delta2),
  member(C < D, Gamma),
  \+member(D,Sigma),
  \+findBlock(Delta,[Sigma,C]),
  !,
  prove([[Gamma,[[[D|Sigma],A]|Delta2]]|Remainder],SubTree1),
  prove([[Gamma, [[Sigma,A],[Sigma,C]|Delta2]]|Remainder],SubTree2).

prove(Hypersequent, tree(com,Hypersequent,[Gamma,Delta],no, SubTree1, SubTree2)) :-
  select([Gamma,Delta], Hypersequent, Remainder),
  select([Sigma1,A], Delta, Delta2),
  select([Sigma2,B], Delta2, Delta3),
  append(Sigma1,Sigma2,NewSigma),
  \+subset(Sigma1,Sigma2),
  \+subset(Sigma2,Sigma1),
  !,
  prove([[Gamma, [[Sigma2,B],[NewSigma,A]|Delta3]]|Remainder],SubTree1),
  prove([[Gamma, [[Sigma1,A],[NewSigma,B]|Delta3]]|Remainder],SubTree2).

prove(Hypersequent, tree(t,Hypersequent,[Gamma,Delta],no,SubTree1,SubTree2)) :-
  select([Gamma,Delta], Hypersequent, Remainder),
  member(A < B, Gamma),
  select(transfer Theta, Delta, Delta2),
  \+member(B,Theta),
  \+findSequent(Hypersequent,[[A],Theta]),
  !,
  prove([[Gamma,Delta], [[A],Theta]|Remainder],SubTree1),
  prove([[Gamma,[transfer [B|Theta]|Delta2]]|Remainder],SubTree2).

findSequent(Hypersequent,[Gamma,Delta]) :-
  member([Gamma2,Delta2],Hypersequent),
  subset(Gamma,Gamma2),
  subset(Delta,Delta2),!.

findBlock(Delta,[Sigma,A]) :-
  member([Sigma2,A],Delta),
  subset(Sigma,Sigma2),!.

/********* LATEX ***************/

stampa(Tree,FileName) :-
  open(FileName,write,Stream),
  writeln(Stream,"\\documentclass[a3paper]{article}"),
  writeln(Stream,"\\usepackage{amssymb}"),
  writeln(Stream,"\\usepackage{amsmath}"),
  writeln(Stream,"\\usepackage[landscape]{geometry}"),
  writeln(Stream,"\\usepackage{bussproofs}"),
  writeln(Stream,"\\usepackage[export]{adjustbox}"),
  writeln(Stream,"\\begin{document}"),
  writeln(Stream,"\\begin{center}"),
  parse(Tree,Stream),
  writeln(Stream,"\\resizebox{\\textwidth}{!}{\\DisplayProof}"),
  writeln(Stream,"\\end{center}"),
  writeln(Stream,"\\end{document}"),
  close(Stream).

parse(tree(Op,Hypersequent,Sequent1,no,no,no),Stream) :-
  !,
  writeln(Stream,"\\AxiomC{}"),
  rule(Op,Stream),
  length(Hypersequent,Length),
  ((Length > 1) ->  write(Stream,"\\UnaryInfC{$\\mathcal{G}\\; \\vert \\;"); write(Stream,"\\UnaryInfC{$")),
  betterSequent(Sequent1,Stream),
  writeln(Stream,"$}").

parse(tree(Op,Hypersequent,Sequent1,no,SubTree1,no),Stream) :-
  !,
  parse(SubTree1,Stream),
  rule(Op,Stream),
  length(Hypersequent,Length),
  ((Length > 1) ->  write(Stream,"\\UnaryInfC{$\\mathcal{G}\\; \\vert \\;"); write(Stream,"\\UnaryInfC{$")),
  betterSequent(Sequent1,Stream),
  writeln(Stream,"$}").

parse(tree(Op,Hypersequent,Sequent1,Sequent2,SubTree1,no),Stream) :-
  !,
  parse(SubTree1,Stream),
  rule(Op,Stream),
  length(Hypersequent,Length),
  ((Length > 2) ->  write(Stream,"\\UnaryInfC{$\\mathcal{G}\\; \\vert \\;"); write(Stream,"\\UnaryInfC{$")),
  betterSequent(Sequent1,Stream), 
  write(Stream,"\\; \\vert \\;"), 
  betterSequent(Sequent2,Stream),
  writeln(Stream,"$}").

parse(tree(Op,Hypersequent,Sequent1,no,SubTree1,SubTree2),Stream):-
  !,
  parse(SubTree1,Stream),
  parse(SubTree2,Stream),
  rule(Op,Stream),
  length(Hypersequent,Length),
  ((Length > 1) -> write(Stream,"\\BinaryInfC{$\\mathcal{G}\\; \\vert \\;"); write(Stream,"\\BinaryInfC{$")),
  betterSequent(Sequent1,Stream),
  writeln(Stream,"$}").

rule(init,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\text{init}^i$)}").
rule(trueR,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\top^i_R$)}").
rule(falseL,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\bot^i_L$)}").
rule(orR,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\lor^i_R$)}").
rule(orL,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\lor^i_L$)}").
rule(implR,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\rightarrow^i_R$)}").
rule(implL,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\rightarrow^i_L$)}").
rule(andR,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\land^i_R$)}").
rule(andL,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\land^i_L$)}").
rule(precR,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\preccurlyeq^i_R$)}").
rule(precL,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\preccurlyeq^i_L$)}").
rule(notR,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\neg^i_R$)}").
rule(notL,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\neg^i_L$)}").
rule(com,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\text{com}^i$)}").
rule(jump,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\text{jump}^i$)}").
rule(jumpU,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\text{jump}^i_U$)}").
rule(jumpT,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\text{jump}^i_T$)}").
rule(in,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\text{in}^i_{\\text{trf}}$)}").
rule(t,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\text{T}^i$)}").
rule(w,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\text{W}^i$)}").
rule(c,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\text{C}^i$)}").
rule(absL,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\text{abs}^i_L$)}").
rule(absR,Stream):-writeln(Stream,"\\LeftLabel{\\scriptsize($\\text{abs}^i_R$)}").

/*******FORMULAS FORMATTING***********************/

betterSequent([Gamma,Delta],Stream) :-
  listOfAllFmls(Gamma,Stream), write(Stream,"\\Rightarrow "), listOfAllFmls(Delta,Stream).

listOfAllFmls([],Stream) :-
  write(Stream,"").

listOfAllFmls([A|T],Stream) :-
  betterFormula(A,Stream), ((T == []) -> write(Stream,""); write(Stream,",")), listOfAllFmls(T,Stream).

betterFormula(false,Stream):-!,write(Stream,'\\bot').
betterFormula(true,Stream):-!,write(Stream,'\\top').
betterFormula(-A,Stream):-atom(A),!,write(Stream,'\\lnot '),betterFormula(A,Stream).
betterFormula(-A,Stream):-compound(A),!,write(Stream,'\\lnot ('),betterFormula(A,Stream),write(Stream,')').
betterFormula(A and B,Stream):-compound(A),compound(B),!,write(Stream,"("),betterFormula(A,Stream),write(Stream,")"),write(Stream,'\\land '),write(Stream,"("),betterFormula(B,Stream),write(Stream,")").
betterFormula(A and B,Stream):-atom(A),compound(B),!,betterFormula(A,Stream),write(Stream,'\\land '),write(Stream,"("),betterFormula(B,Stream),write(Stream,")").
betterFormula(A and B,Stream):-compound(A),atom(B),!,write(Stream,"("),betterFormula(A,Stream),write(Stream,")"),write(Stream,'\\land '),betterFormula(B,Stream).
betterFormula(A and B,Stream):-atom(A), atom(B),!,betterFormula(A,Stream),write(Stream,'\\land '),betterFormula(B,Stream).
betterFormula(A or B,Stream):-compound(A), compound(B),!,write(Stream,"("),betterFormula(A,Stream),write(Stream,")"),write(Stream,'\\vee '),write(Stream,"("),betterFormula(B,Stream),write(Stream,")").
betterFormula(A or B,Stream):-atom(A), compound(B),!,betterFormula(A,Stream),write(Stream,'\\vee '),write(Stream,"("),betterFormula(B,Stream),write(Stream,")").
betterFormula(A or B,Stream):-compound(A), atom(B),!,write(Stream,"("),betterFormula(A,Stream),write(Stream,")"),write(Stream,'\\vee '),betterFormula(B,Stream).
betterFormula(A or B,Stream):-atom(A), atom(B),!,betterFormula(A,Stream),write(Stream,'\\vee '),betterFormula(B,Stream).
betterFormula(A -> B,Stream):-compound(A), compound(B),!,write(Stream,"("),betterFormula(A,Stream),write(Stream,")"),write(Stream,'\\rightarrow '),write(Stream,"("),betterFormula(B,Stream),write(Stream,")").
betterFormula(A -> B,Stream):-atom(A),compound(B),!,betterFormula(A,Stream),write(Stream,'\\rightarrow '),write(Stream,"("),betterFormula(B,Stream),write(Stream,")").
betterFormula(A -> B,Stream):-compound(A), atom(B),!,write(Stream,"("),betterFormula(A,Stream),write(Stream,")"),write(Stream,'\\rightarrow '),betterFormula(B,Stream).
betterFormula(A -> B,Stream):-atom(A), atom(B),!,betterFormula(A,Stream),write(Stream,'\\rightarrow '),betterFormula(B,Stream).
betterFormula(A < B,Stream):-compound(A), compound(B),!,write(Stream,"("),betterFormula(A,Stream),write(Stream,")"),write(Stream,'\\preccurlyeq '),write(Stream,"("),betterFormula(B,Stream),write(Stream,")").
betterFormula(A < B,Stream):-atom(A), compound(B),!,betterFormula(A,Stream),write(Stream,'\\preccurlyeq '),write(Stream,"("),betterFormula(B,Stream),write(Stream,")").
betterFormula(A < B,Stream):-compound(A), atom(B),!,write(Stream,"("),betterFormula(A,Stream),write(Stream,")"),write(Stream,'\\preccurlyeq '),betterFormula(B,Stream).
betterFormula(A < B,Stream):-atom(A), atom(B),!,betterFormula(A,Stream),write(Stream,'\\preccurlyeq '),betterFormula(B,Stream).
betterFormula(transfer X,Stream) :- !, write(Stream,"\\langle "), listOfAllFmls(X,Stream), write(Stream," \\rangle ").
betterFormula([Sigma,A],Stream) :-!, write(Stream,"["), listOfAllFmls(Sigma,Stream), write(Stream,"\\triangleleft "), betterFormula(A,Stream), write(Stream,"]").
betterFormula(P,Stream):-!,write(Stream,P).
