/* Groundness analisys for full first-order intutionistic logic */

/* written by Gianluca Amato    */
/* developed in SWI-Prolog 3.4  */

/**** GENERIC PREDICATES *****/

%if S1 and S2 are ordered sets, subset_ordered(+S1,+S2) is true iff
% S1 is a subset of S2

subset_ordered([],_):-
        !.
subset_ordered([X|L],[X|R]):-
        !,
        subset_ordered(L,R).
subset_ordered(L,[_|R]):-
        subset_ordered(L,R).

% sort2(+X,+Y,-Z) is true iff Z is the ordered set whose 
% elements are X and Y

sort2(X,X,[X]):-
	!.
sort2(X,Y,[X,Y]):-
	X@<Y, !.
sort2(X,Y,[Y,X]).	

% minimal(X,K) is true if X is minimal in K

minimal(X,K):- 
	forall(member(Y,K), \+ subset(Y,X) ; X=Y).

% minimizeset(X,Y) takes a set of sets X and gives in Y only the
% minimal elements.

minimizeset(X,Y):-
	minimizeset(X,X,Y).
minimizeset([],_,[]).
minimizeset([X|R],K,[X|R1]):-
	minimal(X,K),
	!,
	minimizeset(R,K,R1).
minimizeset([_|R],K,R1):-	
	minimizeset(R,K,R1).

/**** LANGUAGE *****/

% atomic_formula(+F) is true iff F is an atomic formula

atomic_formula(Formula):-
	Formula=..[Func|_],
	\+(member(Func,[exists,and,or,forall,impl,false])).

% The abstraction function follows. They have the form 
% absxxx(+Var,+X,-AbsX) where Var is the set of variables that should 
% be considered bound, apart from those actually bound in X.

absterm(Vars,Term,[Term]):-
	memberchk(Term,Vars),
	!.

absterm(Vars,Term,AbsTerm):-
        Term=..[_|List],
        maplist(absterm(Vars),List,AbsList),
	flatten(AbsList,AbsList2),
	sort(AbsList2,AbsTerm).

absatom(Vars,Atom,AbsAtom):-
	Atom=..[Symbol|List],
	maplist(absterm(Vars),List,AbsList),
	AbsAtom=..[Symbol|AbsList].

absformula(_Vars,false,false):-
	!.
absformula(Vars,and(F1,F2),and(A1,A2)):-
	!, 
	absformula(Vars,F1,A1), absformula(Vars,F2,A2).
absformula(Vars,or(F1,F2),or(A1,A2)):-
	!, 
	absformula(Vars,F1,A1), absformula(Vars,F2,A2).
absformula(Vars,impl(F1,F2),impl(A1,A2)):-
	!, 
	absformula(Vars,F1,A1), 
	absformula(Vars,F2,A2).
absformula(Vars,exists(Var,Formula),exists(Var,AbsFormula)):-
	!, 
	union([Var],Vars,Vars2),
	absformula(Vars2,Formula,AbsFormula).
absformula(Vars,forall(Var,Formula),forall(Var,AbsFormula)):-
	!, 
	union([Var],Vars,Vars2),
	absformula(Vars2,Formula,AbsFormula).
absformula(Vars,Atom,AbsAtom):-
	absatom(Vars,Atom,AbsAtom).

% absseq(+Sequent,-AbsSequent) is true iff AbsSequent is the
% abstraction of Sequent. Note that the left-hand side of an abstract
% sequent is an ordered set.

absseq(Clauses->Goal,AbsClauses->AbsGoal):-
	absformula([],Goal,AbsGoal),
	maplist(absformula([]),Clauses,AbsClauses1),
	sort(AbsClauses1,AbsClauses).

% absder(+Sequent,-Der) is true iff Der is the abstraction of the
% empty proofschema for Sequent.

absemptyder(Sequent,der([],[AbsSequent])):-
	absseq(Sequent,AbsSequent).

/******** INFERENCE RULES *********/

% In groundterm(+Var,+Term,-Termg), Termg is the abstract term 
% obtained by the abstract term Term by replacing Var with a 
% ground term.

groundterm(Var,Term,Termg):-
        select(Var,Term,Termg),
	!.
groundterm(_Var,Term,Term).

% In ngroundterm(+Var,+Term,-Termg), Termg is the abstract term 
% obtained by the abstract term Term by replacing Var with a 
% non-ground term.

ngroundterm(Var,Term,ng):-
	member(Var,Term),
	!.
ngroundterm(_Var,Term,Term).

replacevarinatom(_,Op,A,Ar):-
	A=..[Symbol|List],
	maplist(Op,List,Listr),
	Ar=..[Symbol|Listr].

% replacevarinformula(+Var,+Op,+FormulaIn,-FormulaOut) gives in 
% FormulaOut the result of replacing Var with a ground or non-ground 
% term in FormulaIn, respectively if Op=groundterm or Op=ngroundterm.

replacevarinformula(Var,Op,and(F1,F2),and(Fr1,Fr2)):-
	!,
	replacevarinformula(Var,Op,F1,Fr1),
	replacevarinformula(Var,Op,F2,Fr2).
replacevarinformula(Var,Op,or(F1,F2),or(Fr1,Fr2)):-
	!,
	replacevarinformula(Var,Op,F1,Fr1),
	replacevarinformula(Var,Op,F2,Fr2).
replacevarinformula(Var,Op,impl(F1,F2),impl(Fr1,Fr2)):-
	!,
	replacevarinformula(Var,Op,F1,Fr1),
	replacevarinformula(Var,Op,F2,Fr2).
replacevarinformula(Var,Op,exists(V,F),exists(V,Fr)):-
	!,
	replacevarinformula(Var,Op,F,Fr).
replacevarinformula(Var,Op,forall(V,F),forall(V,Fr)):-
	!,
	replacevarinformula(Var,Op,F,Fr).
replacevarinformula(_Var,_Op,false,false):-
	!.
replacevarinformula(Var,Op,A,Ar):-
	replacevarinatom(Var,Op,A,Ar).

% rule(?Name,+Sequent,-NewSequent,-NGround) gives the abstract 
% version of the inference rules.

rule(id,Gamma->Goal,[],[]) :-
	atomic_formula(Goal),
	memberchk(Goal,Gamma).
rule(idfalse,Gamma->false,[],[]):-
	memberchk(false,Gamma).
rule(falser,Gamma->G,[Gamma->false],[]):-
	G\==false.
rule(implr,Gamma->impl(C,G),[NewGamma->G],[]):-
	merge_set([C],Gamma,NewGamma).
rule(andr,Gamma->and(G1,G2),X,[]):-
	sort2(Gamma->G1,Gamma->G2,X).
rule(orr,Gamma->or(G1,G2),[Gamma->G],[]):-
	(
	    G=G1;
	    G=G2
	).
rule(forallr,Gamma->forall(_,G),[Gamma->G2],[bind(Var,ng)]):-
	replacevarinformula(Var,ngroundterm(Var),G,G2).
rule(existsr,Gamma->exists(Var,G),[Gamma->G2],[K]):-
	(
	    replacevarinformula(Var,groundterm(Var),G,G2),
	    K=bind(Var,g);
	    replacevarinformula(Var,ngroundterm(Var),G,G2),
	    K=bind(Var,ng)
	).
rule(andl,Gamma->G,[NewGamma->G],[]) :-
	select(and(F1,F2),Gamma,Gamma0),
	merge_set([F1],Gamma0,Gamma1),
	merge_set([F2],Gamma1,NewGamma).
rule(orl,Gamma->G,X,[]):-
	select(or(F1,F2),Gamma,Gamma0),
	merge_set([F1],Gamma0,NewGamma1),
	merge_set([F2],Gamma0,NewGamma2),
	sort2(NewGamma1->G,NewGamma2->G,X).
rule(impll,Gamma->G,X,[]):-
	select(impl(Body,Head),Gamma,Gamma0),
	merge_set([Head],Gamma0,NewGamma),
	sort2(Gamma0->Body, NewGamma->G, X).
rule(foralll,Gamma->G,[NewGamma->G],K):-
	select(forall(Var,Clause),Gamma,Gamma0),
        replacevarinformula(Var,ngroundterm(Var),Clause,Clause1),
	replacevarinformula(Var,groundterm(Var),Clause,Clause2),
	(
	    merge_set([Clause1],Gamma0,NewGamma),
	    K=[bind(Var,ng)];
	    merge_set([Clause2],Gamma0,NewGamma),
	    K=[bind(Var,g)];
	    merge_set([Clause1],Gamma0,Gamma1),
	    merge_set([Clause2],Gamma1,NewGamma),
	    K=[bind(Var,g), bind(Var,ng)]	    
	).
rule(existsl,Gamma->G,[NewGamma->G],[bind(Var,ng)]):-
	select(exists(Var,F),Gamma,Gamma0),
	replacevarinformula(Var,ngroundterm(Var),F,F1),
	merge_set([F1],Gamma0,NewGamma).


/******* ABSTRACT OPERATIONAL SEMANTICS ********/

% transitionstep(+AbsDerIn,-AbsDerOut)  is the implementation of the
% abstract transition system. It non deterministically gives 
% in AbsDerOut the results of 
% \alpha(\gamma(\{AbsDerInt\}) \glue (R \cup \epsilon))
 
transitionstep(der(NG,Tail),der(NG1,Tail1)):-
	transitionstep(Tail,NG,Tail1,NG1,[]).

transitionstep([],NG,Acc,NG,Acc).
transitionstep([ASeq|Rest],NG,Tail1,NG1,Acc):-
	rule(_,ASeq,ASeqSet,NGNew),
	merge_set(NGNew,NG,NG2),
	merge_set(ASeqSet,Acc,Acc1),
	transitionstep(Rest,NG2,Tail1,NG1,Acc1).

%% operationalstep(+AbsIntIn,-AbsIntOut) is true iff 
%% AbsIntOut=U_{L,\alpha}(AbsIntIn)

operationalstep([],[]).
operationalstep([Der|SetDers],NewSetDers):-
	(setof(X,transitionstep(Der,X),NewListDers), ! ; NewListDers=[]),
	operationalstep(SetDers,PartialSet),
	merge_set(NewListDers,PartialSet,NewSetDers).

%% just some debugging stuff 

operational(0,Der,Der).
operational(N,Der,NewDer):-
	N>0,
        operationalstep(Der,NewDer1),    
        N1 is N-1,
        operational(N1,NewDer1,NewDer).

%% omegaoperational(+AbsInt,-AbsIntOut) is true iff AbsIntOut is the
%% least fixpoint of the abstract U_L greater then AbsIntIn.

omegaoperational(SetDer,NewDer):-
	operationalstep(SetDer,TempSetDer),
	(TempSetDer=SetDer ->
	    NewDer=SetDer
	; 
	    omegaoperational(TempSetDer,NewDer)).

%% it is what we want.
%% answersemantics(+Seq,-Bindings) gives a correct approximation 
%% of the correct groundness answers for Seq.
	
answersemantics(Seq,Binding):-
	absemptyder(Seq,ADer),
	omegaoperational([ADer],Semantics),
	member(der(Binding,[]),Semantics).

%%
%% minimalsemantics(+Seq,-Bindings) gives the minimal correct
%% groundness answers fo Seq
%% 

minimalsemantics(Seq,B):-
	absemptyder(Seq,ADer),
	omegaoperational([ADer],Semantics),
	setof(Binding,member(der(Binding,[]),Semantics),List),
	minimizeset(List,ListMin),
	member(B,ListMin).

/******** EXTRA OPTIMIZED *******/

absproof(Seq,Bind):-
	rule(_,Seq,ListSeq,B),
	maplist(absproof,ListSeq,ListB),
	flatten(ListB,FlatB),
	append(B,FlatB,Bind).
	
sem(Seq,Bindings):-
	absseq(Seq,ASeq),
	setof(Bind,absproof(ASeq,Bind),Bindings).
	
/******** EXAMPLES  **********/

%% Here follows some examples. We mean by computed answer the best
%% possible groundness answer for the abstracted sequent.

% EXAMPLE 1. Best and computed answer: {{v1/g, v2/g},{v1/ng, v2/ng}}

example(1,[forall(v1, p(v1))]->exists(v2, p(v2))).

% EXAMPLE 2. Best and computed answer: {{v1/g, v2/g}}

example(2,[forall(v1,and(p(a,v1),p(v1,b)))]->exists(v2,p(v2,v2))).

% EXAMPLE 3. Best and computed answer: {{v2/g}}

example(3,[p(a),forall(v1,impl(p(v1),p(v1)))]->exists(v2,p(v2))).

% EXAMPLE 4. Best and computed answer: {{v1/g,v3/g},{v1/ng,v3/ng},
%                                       {v2/g,v3/g},{v2/ng,v3/ng}}

example(4,[forall(v1,p(t(v1))),forall(v2,p(s(v2)))]->
	exists(v3,p(v3))).

% EXAMPLE 5. Best and computed answer:{{v1/g,v2/g,v3/g},
%				       {v1/ng,v2/ng,v3/ng}}

example(5,[forall(v1,p(v1,v1))]->exists(v2,exists(v3,p(v2,v3)))).

% EXAMPLE 6. Best and computed answer: {{v1/ng,v2/g,v3/ng}}

example(6,[forall(v1,and(p(a,v1),p(v1,b)))]->
	exists(v2,forall(v3,p(v2,v3)))).

% EXAMPLE 7. Best and computed answer: {{v1/g,v2/g},{v1/ng,v2/g}}

example(7,[forall(v1,and(p(a),r(b)))]->exists(v2,or(p(v2),r(v2)))).

% EXAMPLE 8. Best and computed answer: {{v1/g, v2/ng},{v1/ng,v2/g},
%					{v1/g,v2/g}}

example(8,[and(p(a),r(b))]->
	exists(v1,exists(v2,or(p(v1),r(v2))))).

% EXAMPLE 9. Best and computed answer: {{v1/g}}

example(9,[or(p(a),r(b))]->exists(v1,or(p(v1),r(v1)))).

% EXAMPLE 10. Best and computed answer: {{v1/ng,v2/ng}}

example(10,[exists(v1,p(v1))]->exists(v2,p(v2))).

% EXAMPLE 11. Best and computed answer: {{}}

example(11,[false]->exists(v1,p(v1))).

% EXAMPLE 12. Best and computed answer: {{v1/g},{v1/ng}}

example(12,[p(a)]->exists(v1,or(q(v1),p(a)))).

% EXAMPLE 13. Best and computed answer: {{v1/g},{v1/ng}}

example(13,[q(b),p(a)]->exists(v1,or(q(v1),p(a)))).

% EXAMPLE 14. Best and computed answer: {{v1/ng,v2/ng,v3/ng}}

example(14,[forall(v1,p(v1,v1))]->forall(v2,exists(v3,p(v2,v3)))).
 
% EXAMPLE 15.  Best and computed answer: {}

example(16,[]->exists(x,p(x))). 

% EXAMPLE 16. Best answer {}, 
%             Computed Answer: {{v1/ng, v2/ng, v3/ng}}

example(16,[forall(v1,exists(v2,(p(v1,v2))))]->forall(v3,p(v3,v3))).

% EXAMPLE 17. Best answer {}, 
%             Computed Answer: { {v1/ng, v2/ng, v3/ng} }

example(17,[forall(v1,exists(v2,(p(v1,v2))))]->exists(v3,p(v3,v3))).

% EXAMPLE 18. Best and omputed Answer: { {v1/ng, v2/{g,ng}} }

example(18,[or(p(a),exists(v1,r(v1)))]->exists(v2,or(p(v2),r(v2)))).