:- module(lub_operations, [lub/1, set_union/1, set_union/2,   msg_union/1]).

% lub operations for several domains.
% the generic interpreters determine the correct operation at call
% time; the specialised interpreters access directly the appropriate
% lub operation.

:- use_module(domain, [domain/1]).
:- use_module(facts, [fact/1, flag/0, fact/2]).
:- use_module(library(terms), [term_subsumer/3]).
:- use_module(library(lists),[select/3]).


lub(F) :- domain(D),
    ( D = concrete -> set_union(F);true ),
    ( D = parity   -> set_union(F);true ),
    ( D = parity1  -> set_union(F);true ),
    ( D = pos      -> set_union(F);true ),
    ( D = pattern  -> msg_union(F);true ),
    ( D = depth(K) -> depth(K,F,NewF),set_union(NewF) ; true ),
    ( D = parity_p -> depth(5,F,NewF),set_union(NewF) ; true ).


% this operator adds a fact to the set of facts in the database IF
% it is new (if there is not a more general fact already there)

 set_union(F) :-                    % assert or fail
     \+ (numbervars(F,0,_), fact(F)), 
     assert(fact(F)),
     raise_flag.


% this operator is almost the same as set_union/1 except that it is
% used with semi-naive evaluation and hence needs an additional
% argument to keep track of the iteration number.


 set_union(N,F) :-                    % assert or fail
     \+ (numbervars(F,0,_), fact(_,F)), 
     assert(fact(N,F)).



% this operator checks if a fact is new and if so replaces any
% corresponding fact already there with the most specific
% generalisation of the two. in this way there is always at most one
% fact per predicate. There are special cases for analyses that
% collect calls and answers seperately.


 msg_union(call(I,J,F)) :-   !,                 % assert or fail
    \+ (numbervars(F,0,_), fact(call(I,J,F))), 
    functor(F,N,A), functor(F1,N,A),
    ( retract(fact(call(I,J,F1))) ->
      term_subsumer(F1,F,GF)
      ;
      GF = F
    ),
    assert(fact(call(I,J,GF))),
    raise_flag.

 msg_union(ans(F)) :-   !,                 % assert or fail
    \+ (numbervars(F,0,_), fact(ans(F))), 
    functor(F,N,A), functor(F1,N,A),
    ( retract(fact(ans(F1))) ->
      term_subsumer(F1,F,GF)
      ;
      GF = F
    ),
    assert(fact(ans(GF))),
    raise_flag.

 msg_union(F) :-                    % assert or fail
    \+ (numbervars(F,0,_), fact(F)), 
    functor(F,N,A), functor(F1,N,A),
    ( retract(fact(F1)) ->
      term_subsumer(F1,F,GF)
      ;
      GF = F
    ),
    assert(fact(GF)),
    raise_flag.



%%% DEPTH_K ABSTRACTION

depth(K,Term,NewTerm) :-
	depth(K,Term,NewTerm,Dic-[]),
	unify_same(Dic).

unify_same([]).
unify_same([T1-NewT1|Ts]) :-
	select(T2-NewT2,Ts,Rest),
	T1 == T2,
	!,
	NewT1 = NewT2,
	unify_same([T1-NewT1|Rest]).
unify_same([_|Ts]) :-
	unify_same(Ts).

	

depth(_K,Term,Term,[Term-Term|Tail]-Tail) :-
	var(Term),
	!.

depth(0,Term,NewTerm,[Term-NewTerm|Tail]-Tail).
	
depth(K,Term,NewTerm,Head-Tail) :-
	K>0,
	Term =.. [F|Args],
	K1 is K-1,
	depth_list(Args,NewArgs,K1,Head-Tail),
	NewTerm =.. [F|NewArgs].

depth_list([],[],_K,Tail-Tail).
depth_list([T|Ts],[NT|NTs],K,Head-Tail) :-
	depth(K,T,NT,Head-Tail1),
	depth_list(Ts,NTs,K,Tail1-Tail).













% raise_flag is not relevant for all of the analyzers. its here for
% uniformity. 

  raise_flag :- (flag -> true;assert(flag)).
 

