/*
Copyright 2019 Tiziano Dalmonte, Sara Negri, Nicola Olivetti, Gian Luca Pozzato. 
This file is part of PRONOM. PRONOM 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 PRONOM. If not, see <http://www.gnu.org/licenses/>.
*/

/* imports */
:- use_module(library(lists)).
:- include("operators.pl").
:- include("common.pl").


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

prove(Formula):-
  generate_empty_spheres([x],InitialSpheres),
  terminating_proof_search(InitialSpheres,[],[[x,Formula]],Tree,[],[],[]),write(Tree),!.
% In case of failure, the application builds a counter model from an open saturated branch
prove(Formula):-write('COUNTER'),
  generate_empty_spheres([x],InitialSpheres),
  build_saturate_branch(InitialSpheres,[],[[x,Formula]],Model,[],[],[]),
  write(Model),!.


/* Auxiliary predicate implementing LSE calculi */

% Axioms
terminating_proof_search(Spheres,Gamma,Delta,tree(axiom,[Spheres,Gamma,Delta],no,no),_,_,_):-
    member([X,A],Gamma),
    member([X,A],Delta),
    !.
terminating_proof_search(Spheres,Gamma,Delta,tree(axf,[Spheres,Gamma,Delta],no,no),_,_,_):-
    member([_,false],Gamma),
    !.
terminating_proof_search(Spheres,Gamma,Delta,tree(axt,[Spheres,Gamma,Delta],no,no),_,_,_):-
    member([_,true],Delta),
    !.


% Rules for boolean connectives
terminating_proof_search(Spheres,Gamma,Delta,tree(notR,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
    select([X,-A],Delta,NewDelta),!,
    terminating_proof_search(Spheres,[[X,A]|Gamma],NewDelta,SubTree,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(notL,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
    select([X,-A],Gamma,NewGamma),!,
    terminating_proof_search(Spheres,NewGamma,[[X,A]|Delta],SubTree,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(andL,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
    select([X,A ^ B],Gamma,NewGamma),!,
    terminating_proof_search(Spheres,[[X,A]|[[X,B]|NewGamma]],Delta,SubTree,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(orR,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
    select([X,A ? B],Delta,NewDelta),!,
    terminating_proof_search(Spheres,Gamma,[[X,A]|[[X,B]|NewDelta]],SubTree,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(impR,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
    select([X,A >> B],Delta,NewDelta),!,
    terminating_proof_search(Spheres,[[X,A]|Gamma],[[X,B]|NewDelta],SubTree,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(andR,[Spheres,Gamma,Delta],Sub1,Sub2),RBox,RExist,LAll):-
    select([X,A ^ B],Delta,NewDelta),!,
    terminating_proof_search(Spheres,Gamma,[[X,A]|NewDelta],Sub1,RBox,RExist,LAll),
    terminating_proof_search(Spheres,Gamma,[[X,B]|NewDelta],Sub2,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(orL,[Spheres,Gamma,Delta],Sub1,Sub2),RBox,RExist,LAll):-
    select([X,A ? B],Gamma,NewGamma),!,
    terminating_proof_search(Spheres,[[X,A]|NewGamma],Delta,Sub1,RBox,RExist,LAll),
    terminating_proof_search(Spheres,[[X,B]|NewGamma],Delta,Sub2,RBox,RExist,LAll).
terminating_proof_search(Spheres,Gamma,Delta,tree(impL,[Spheres,Gamma,Delta],Sub1,Sub2),RBox,RExist,LAll):-
    select([X,A >> B],Gamma,NewGamma),!,
    terminating_proof_search(Spheres,NewGamma,[[X,A]|Delta],Sub1,RBox,RExist,LAll),
    terminating_proof_search(Spheres,[[X,B]|NewGamma],Delta,Sub2,RBox,RExist,LAll).


% L[]
terminating_proof_search(Spheres,Gamma,Delta,tree(lbox,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
    select([X,box A],Gamma,NewGamma),!,
    select([X,SpOfX],Spheres,NewSpheres),
    freshSphere(Spheres,T),
    terminating_proof_search([[X,[T|SpOfX]]|NewSpheres],[[forall,T,0,A]|NewGamma],[[exists,T,1,A]|Delta],SubTree,RBox,RExist,LAll).

% L||-exists
terminating_proof_search(Spheres,Gamma,Delta,tree(lexists,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
     select([exists,T,1,A],Gamma,NewGamma),!,
     freshLabel(Spheres,Gamma,Delta,X),
     terminating_proof_search([[X,[]]|Spheres],[[T,1,X]|[[X,A]|NewGamma]],Delta,SubTree,RBox,RExist,LAll).

% R||- forall
terminating_proof_search(Spheres,Gamma,Delta,tree(rforall,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
    select([forall,T,0,A],Delta,NewDelta),!,
    freshLabel(Spheres,Gamma,Delta,X),
    terminating_proof_search([[X,[]]|Spheres],[[T,0,X]|Gamma],[[X,A]|NewDelta],SubTree,RBox,RExist,LAll).

% Rule R||-exists
% No longer needed since the optimization of R[] 
/*
terminating_proof_search(Spheres,Gamma,Delta,tree(rexists,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
    member([exists,T,1,A],Delta),
    member([T,1,X],Gamma),
    \+member([T,1,X,A],RExist),!,
    terminating_proof_search(Spheres,Gamma,[[X,A]|Delta],SubTree,RBox,[[T,1,X,A]|RExist],LAll).
*/

% Rule L ||-forall
terminating_proof_search(Spheres,Gamma,Delta,tree(lforall,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
    member([forall,T,0,A],Gamma),
    member([T,0,X],Gamma),
    \+member([T,0,X,A],LAll),!,
    terminating_proof_search(Spheres,[[X,A]|Gamma],Delta,SubTree,RBox,RExist,[[T,0,X,A]|LAll]).

% Rule R[]
terminating_proof_search(Spheres,Gamma,Delta,tree(rbox,[Spheres,Gamma,Delta],SubTree,no),RBox,RExist,LAll):-
    member([X,box A],Delta),
    member([X,SpOfX],Spheres),
    member(T,SpOfX),
    \+member([X,A,T],RBox),!,
    terminating_proof_search(Spheres,Gamma,[[forall,T,0,A]|Delta],SubTree,[[X,A,T]|RBox],RExist,LAll).


% Predicate checking wheter a sequent is an instance of an axiom
instanceOfAnAxiom(_,Gamma,Delta):-member([X,A],Gamma),member([X,A],Delta),!.
instanceOfAnAxiom(Gamma,_):-member([_,false],Gamma),!.
instanceOfAnAxiom(_,Delta):-member([_,true],Delta),!.


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

% L[]
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([X,box A],Gamma,NewGamma),!,
    select([X,SpOfX],Spheres,NewSpheres),
    freshSphere(Spheres,T),
    build_saturate_branch([[X,[T|SpOfX]]|NewSpheres],[[forall,T,0,A]|NewGamma],[[exists,T,1,A]|Delta],Model,RBox,RExist,LAll).

% L||-exists
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
     select([exists,T,1,A],Gamma,NewGamma),!,
     freshLabel(Spheres,Gamma,Delta,X),
     build_saturate_branch([[X,[]]|Spheres],[[T,1,X]|[[X,A]|NewGamma]],Delta,Model,RBox,RExist,LAll).

% R||- forall
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([forall,T,0,A],Delta,NewDelta),!,
    freshLabel(Spheres,Gamma,Delta,X),
    build_saturate_branch([[X,[]]|Spheres],[[T,0,X]|Gamma],[[X,A]|NewDelta],Model,RBox,RExist,LAll).

% Rule R[]
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    member([X,box A],Delta),
    member([X,SpOfX],Spheres),
    member(T,SpOfX),
    \+member([X,A,T],RBox),
    build_saturate_branch(Spheres,Gamma,[[forall,T,0,A]|Delta],Model,[[X,A,T]|RBox],RExist,LAll).



% Rule R||-exists
% No longer needed since the optimization of R[] 
/*
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    member([exists,T,1,A],Delta),
    member([T,1,X],Gamma),
    \+member([T,1,X,A],RExist),!,
    build_saturate_branch(Spheres,Gamma,[[X,A]|Delta],Model,RBox,[[T,1,X,A]|RExist],LAll).
*/

% Rule L ||-forall
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    member([forall,T,0,A],Gamma),
    member([T,0,X],Gamma),
    \+member([T,0,X,A],LAll),!,
    build_saturate_branch(Spheres,[[X,A]|Gamma],Delta,Model,RBox,RExist,[[T,0,X,A]|LAll]).


% Rules for boolean connectives
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([X,-A],Delta,NewDelta),!,
    build_saturate_branch(Spheres,[[X,A]|Gamma],NewDelta,Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([X,-A],Gamma,NewGamma),!,
    build_saturate_branch(Spheres,NewGamma,[[X,A]|Delta],Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([X,A ^ B],Gamma,NewGamma),!,
    build_saturate_branch(Spheres,[[X,A]|[[X,B]|NewGamma]],Delta,Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([X,A ? B],Delta,NewDelta),!,
    build_saturate_branch(Spheres,Gamma,[[X,A]|[[X,B]|NewDelta]],Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([X,A >> B],Delta,NewDelta),!,
    build_saturate_branch(Spheres,[[X,A]|Gamma],[[X,B]|NewDelta],Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([X,A ^ _],Delta,NewDelta),
    build_saturate_branch(Spheres,Gamma,[[X,A]|NewDelta],Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([X,_ ^ B],Delta,NewDelta),
    build_saturate_branch(Spheres,Gamma,[[X,B]|NewDelta],Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([X,A ? _],Gamma,NewGamma),
    build_saturate_branch(Spheres,[[X,A]|NewGamma],Delta,Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([X,_ ? B],Gamma,NewGamma),
    build_saturate_branch(Spheres,[[X,B]|NewGamma],Delta,Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([X,A >> _],Gamma,NewGamma),
    build_saturate_branch(Spheres,NewGamma,[[X,A]|Delta],Model,RBox,RExist,LAll).
build_saturate_branch(Spheres,Gamma,Delta,Model,RBox,RExist,LAll):-
    select([X,_ >> B],Gamma,NewGamma),
    build_saturate_branch(Spheres,[[X,B]|NewGamma],Delta,Model,RBox,RExist,LAll).


% If no further rule is applicable and the branch is not closed, we have found a closed saturated branch and we are done
build_saturate_branch(Spheres,Gamma,Delta,model(Spheres,Gamma,Delta),_,_,_):-
    true,
    \+instanceOfAnAxiom(Spheres,Gamma,Delta).

% Generate a fresh sphere
freshSphere([],1):-!.
freshSphere(Spheres,T):-
    findMax(Spheres,MaxSph),T is MaxSph+1,!.
findMax(Spheres,Max):-maxAux(Spheres,0,Max).
maxAux([],Max,Max):-!.
maxAux([[_,List]|Tail],Max,MaxDef):-
    maxInList(List,Max,MaxInList),
    maxAux(Tail,MaxInList,MaxDef).
						
printSpheres(_,[]):-!.
printSpheres(Spheres,[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),
    printSphAux(Elements),
    write("}, "),
    printSpheres(Spheres,Labels).
printSpheres(Spheres,[X|Labels]):-
    write("N("),write(X),write(")=&#8709;, "),
    printSpheres(Spheres,Labels).
printSphAux([]):-!.
/*printSphAux([_+s]):-!.
printSphAux([_+s|Tail]):-!,printSphAux(Tail).*/
printSphAux([X]):-!,write("("),betterNameofSphereHTML(X),write(","),betterNameofSignedSphereHTML(X),write(")").
printSphAux([X|Tail]):-!,write("("),betterNameofSphereHTML(X),write(","),betterNameofSignedSphereHTML(X),write("), "),printSphAux(Tail).
removeSigned([],[]):-!.
removeSigned([_+s|Tail],Rest):-!,removeSigned(Tail,Rest).
removeSigned([X|Tail],[X|Rest]):-removeSigned(Tail,Rest).

getWorldsFromSpheres(Spheres,Formulas):-
    getListOfSpheres(Spheres,ListOfSpheres),
    remove_duplicates(ListOfSpheres,OkSph),
    printWorldsFromSpheres(OkSph,Formulas),
    write(', '),
    printWorldsFromSignedSpheres(OkSph,Formulas).
getListOfSpheres([],[]):-!.
getListOfSpheres([[_,List]|Tail],Result):-getListOfSpheres(Tail,ResTail),append(ResTail,List,Result).
printWorldsFromSpheres([],_):-!.
printWorldsFromSpheres([T],Formulas):-!,
    getWorldsInT(T,Formulas,Results),
    printBetter(T,Results).
printWorldsFromSpheres([T|Tail],Formulas):-
    getWorldsInT(T,Formulas,Results),
    printBetter(T,Results),
    write(', '),
    printWorldsFromSpheres(Tail,Formulas).

getSphereFromModel(model(Spheres,_,_)):-!,write(Spheres).
getFormulasFromModel(model(_,Formulas,_)):-!,write(Formulas).
extractWorlds(Formulas,Spheres):-
    extractWorldsFromFormulas(Formulas,ListWorlds1),
    extractWorldsFromSpheres(Spheres,ListWorlds2),
    append(ListWorlds1,ListWorlds2,ListWorldsTemp),
    remove_duplicates(ListWorldsTemp,ListWorlds),
    printOnWebPage(ListWorlds).

extractWorldsFromFormulas([],[]):-!.
extractWorldsFromFormulas([[X,_]|Tail],[X|LabelsTail]):-!,extractWorldsFromFormulas(Tail,LabelsTail).
extractWorldsFromFormulas([_|Tail],Labels):-extractWorldsFromFormulas(Tail,Labels).
    
printEmptySpheres([],_):-!.
printEmptySpheres([T|Tail],Formulas):-
    true,
    \+member([T,1,_],Formulas),
    betterNameofSignedSphereHTML(T),
    write('=&#8709;, '),
    printEmptySpheres(Tail,Formulas).



