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

/* program prepared for SAS2000 */
/* written by Gianluca Amato    */
/* developed in SWI-Prolog 3.2  */

/**** 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,-NewBindings) 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(andr,Gamma->and(G1,G2),X,[]):-
	sort2(Gamma->G1,Gamma->G2,X).
rule(orr1,Gamma->or(G1,_),[Gamma->G1],[]).
rule(orr2,Gamma->or(_,G2),[Gamma->G2],[]).
rule(implr,Gamma->impl(C,G),[NewGamma->G],[]):-
	merge_set([C],Gamma,NewGamma).
rule(existsr,Gamma->exists(Var,G),[Gamma->G2],[bind(Var,g)]):-
	replacevarinformula(Var,groundterm(Var),G,G2).
rule(existsr,Gamma->exists(Var,G),[Gamma->G2],[bind(Var,ng)]):-
	replacevarinformula(Var,ngroundterm(Var),G,G2).
rule(forallr,Gamma->forall(_,G),[Gamma->G2],[]):-
	replacevarinformula(Var,ngroundterm(Var),G,G2).
rule(falser,Gamma->_G,[Gamma->false],[]).
rule(andl,Gamma->G,[NewGamma->G],[]) :-
	member(and(F1,F2),Gamma),
	merge_set([F1],Gamma,Gamma1),
	merge_set([F2],Gamma1,NewGamma).
rule(orl,Gamma->G,X,[]):-
	member(or(F1,F2),Gamma),
	merge_set([F1],Gamma,NewGamma1),
	merge_set([F2],Gamma,NewGamma2),
	sort2(NewGamma1->G,NewGamma2->G,X).
rule(impll,Gamma->G,X,[]):-
	member(impl(Body,Head),Gamma),
	merge_set([Head],Gamma,NewGamma),
	sort2(Gamma->Body, NewGamma->G, X).
rule(foralll,Gamma->G,[NewGamma->G],[]):-
	member(forall(Var,Clause),Gamma),
	(
	    replacevarinformula(Var,ngroundterm(Var),Clause,Clause1)
	;
	    replacevarinformula(Var,groundterm(Var),Clause,Clause1)
	),
	merge_set([Clause1],Gamma,NewGamma).
rule(existsl,Gamma->G,[NewGamma->G],[]):-
	member(exists(Var,F),Gamma),
	replacevarinformula(Var,ngroundterm(Var),F,F1),
	merge_set([F1],Gamma,NewGamma).

/*****  ABSTRACT TRANSITION SYSTEM ******/

% mergebindings implements the meet case in the definition of the
% function \ground. 
% mergebindings(+Bind1,+Bind2,-Bind) is true iff Bind=Bind1 \meet Bind2

mergebindings(Bindings,[],Bindings):-!.
mergebindings([],Bindings,Bindings):-!.
mergebindings([bind(V1,Vl1)|R1],[bind(V1,Vl2)|R2],R):-
	!,
	(
	    Vl1==Vl2 
	->
	    R=[bind(V1,Vl1)|R3],
	    mergebindings(R1,R2,R3)
        ;
	    mergebindings(R1,R2,R)
	).
mergebindings([bind(V1,Vl1)|R1],[bind(V2,Vl2)|R2],[bind(V3,Vl3)|R3]):-	
	V1 @< V2 
    ->  V3=V1, Vl3=Vl1,
	mergebindings(R1,[bind(V2,Vl2)|R2],R3)
    ;   V3=V2, Vl3=Vl2,
	mergebindings([bind(V1,Vl1)|R1],R2,R3).

% 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(Bindings,Tail),der(NewBindings,NewTail)):-
	transitionstep(false,Tail,Bindings,[],NewBindings,NewTail).

transitionstep(true,[],Bindings,NewTail,Bindings,NewTail).
transitionstep(_,[Leaf|Remain],Bindings,Tail,NewBindings,NewTail):-
	rule(_,Leaf,AddedTail,AddedBindings),
	mergebindings(Bindings,AddedBindings,NewBindings1),
	merge_set(AddedTail,Tail,NewTail1),
	transitionstep(true,Remain,NewBindings1,NewTail1,NewBindings,NewTail).
transitionstep(V,[Leaf|Remain],Bindings,Tail,NewBindings,NewTail):-
	merge_set([Leaf],Tail,Tail1),
	transitionstep(V,Remain,Bindings,Tail1,NewBindings,NewTail).

/***** 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

subsumebind(Binds1,Binds2):-
	subset_ordered(Binds2,Binds1).

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

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

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

operationalstep(Ders,NewDers):-
	operationalstep2(Ders,TempDers),
	normalize(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),
	append(SetDer,TempSetDer,Temp1),
	normalize(Temp1,Temp2),
	(subset_ordered(Temp2,SetDer) -> 
	    NewDer=SetDer
	    ; 
	    omegaoperational(Temp2,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).
	
/******** 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(v1,p(t(v1))),forall(v1,impl(p(v1),p(t(v1))))]->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: {{}} Computed answer: {{v1/ng}}

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

% EXAMPLE 11. Best and computd 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: {{v1/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))).