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

/* program prepared for AGP00   */
/* written by Gianluca Amato    */
/* developed in SWI-Prolog 3.3  */

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

/**** 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(Term,Var,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(implr,Gamma->impl(C,G),[NewGamma->G],[]):-
	!,
	merge_set([C],Gamma,NewGamma).
rule(forallr,Gamma->forall(_,G),[Gamma->G2],[]):-
	!,
	replacevarinformula(Var,ngroundterm(Var),G,G2).
rule(andl,Gamma->G,[NewGamma->G],[]) :-
	select(Gamma,and(F1,F2),Gamma0),
	!,
	merge_set([F1],Gamma0,Gamma1),
	merge_set([F2],Gamma1,NewGamma).
rule(foralll,Gamma->G,[NewGamma->G],[]):-
	select(Gamma,forall(Var,Clause),Gamma0),
	!,
	replacevarinformula(Var,ngroundterm(Var),Clause,Clause1),
	replacevarinformula(Var,groundterm(Var),Clause,Clause2),
	merge_set([Clause1],Gamma0,Gamma1),
	merge_set([Clause2],Gamma1,NewGamma).
rule(existsl,Gamma->G,[NewGamma->G],[]):-
	select(Gamma,exists(Var,F),Gamma0),
	!,
	replacevarinformula(Var,ngroundterm(Var),F,F1),
	merge_set([F1],Gamma0,NewGamma).
rule(orl,Gamma->G,X,[]):-
	select(Gamma,or(F1,F2),Gamma0),
	!,
	merge_set([F1],Gamma0,NewGamma1),
	merge_set([F2],Gamma0,NewGamma2),
	sort2(NewGamma1->G,NewGamma2->G,X).
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(existsr,Gamma->exists(Var,G),[Gamma->G2],[]):-
	(
	    replacevarinformula(Var,groundterm(Var),G,G2);
	    replacevarinformula(Var,ngroundterm(Var),G,G2)
	).

rule(impll,Gamma->G,X,[]):-
	select(Gamma,impl(Body,Head),Gamma0),
	merge_set([Head],Gamma0,NewGamma),
	sort2(Gamma0->Body, NewGamma->G, X).

rule(falser,Gamma->G,[Gamma->false],[]):-
	G\==false.

/***** ABSTRACT NORMALIZATION *********/

%% normalize implements the abstract join. If Set1 and
%% Set2 are two abstract interpretation, Set1 \join Set2 is given by
%% normalization(Set1::Set2).

%% normalize(+SetIn,-SetOut) simply deletes from SetIn the irrelevant
%% elements, i.e. those which have an upper bound in SetIn according to the
%% ordering in D_{rg}, and gives the result in SetOut

normalize(Ders,NewDers):-
	normalize(Ders,[],NewDers).
normalize([],Accumulate,Accumulate).
normalize([der(Binds,Tail)|Remain],Accumulate,NewDers):-
	(
	    (
		member(der(Binds,Tail1),Remain) ; 
		member(der(Binds,Tail1),Accumulate)
	    ),
	    subset_ordered(Tail1,Tail)
	)
    ->
	normalize(Remain,Accumulate,NewDers)
    ;
	merge_set([der(Binds,Tail)],Accumulate,NewAcc),
	normalize(Remain,NewAcc,NewDers).

/******* 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(Ders,NewDers):-
	operationalstep2(Ders,TempDers),
%	normalize(TempDers,NewDers).
%	list_to_set(TempDers,NewDers).
	TempDers=NewDers.

operationalstep2([],[]).
operationalstep2([Der|SetDers],NewSetDers):-
	(setof(X,transitionstep(Der,X),NewListDers), ! ; NewListDers=[]),
	operationalstep2(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).

/******** 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},{v1/ng}}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

example(8,[forall(v1,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 answer: {{v1/ng}} Computed answer: {{v1/ng}}

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

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

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: {{v2/ng}}

example(14,[forall(v1,p(v1,v1))]->forall(v1,exists(v2,p(v1,v2)))).
 
% EXAMPLE 15. Best answer {{v1/g}}  Computed answer: stack overflow

example(15,[forall(v1,append(nil,v1,v1)),
	forall(v1,forall(v2,forall(v3,forall(v4,
	impl(append(v2,v3,v4),append(cons(v1,v2),v3,cons(v1,v4)))))))]
    ->exists(v1,append(cons(a,nil),nil,v1))).

% EXAMPLE 16.  Best answer {}, Computed answer: {}

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

% EXAMPLE 17. Best answer {}, Computed Answer: { {} }

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