%%% --------------------------------------------------------------------
%% Simplistic Abstract Interpreter for logic programs
%% run under SICStus Prolog
%% By: Michael Codish
%% Last updated: June 6th 2001
%% --------------------------------------------------------------------
%
%    goal independent  or dependent 
%
%    with or without program points
%
%    various abstract domains
%    
%    should add a few demo builtins

:- module(analyser, [go/2,go/1,set_domain/1]).

:- use_module(library(lists),[member/2,append/3,select/3]).
:- use_module(library(terms), [term_subsumer/3]).

:- dynamic domain/1, points/1, my_clause/2, fact/1.



%% goal dependent interface 
  go(File,Goal) :-              % Goal is atomic
      retractall(fact(_)),  
      load_file(File),
      (domain(_) -> true ; set_domain(domain(concrete))),
      (points(_) -> true ; set_domain(points(off))),
      new(call(0,0, Goal)),
      fail.
  go(_,_)   :- showfacts.

%% goal in dependent interface 

  go(File) :-
      retractall(fact(_)),
      load_file(File),
      (domain(_) -> true ; set_domain(domain(pos))),
      (points(_) -> true ; set_domain(points(off))),
      eager_gi(true),
      fail.
  go(_) :-  showfacts.

%% logic (goal independent)

  eager_gi(true) :-                       
          my_clause(Head,Body),
          prove(Body),
          eager_gi(ans(Head)).

  eager_gi(ans(Atom)) :- 
          lub(ans(Atom)),
          my_clause(Head,Body),
          select(pp(_,_,Atom),Body,Rest),
          prove(Rest),
          eager_gi(ans(Head)).


%% logic (goal dependent)

  new(Fact) :- lub(Fact), eager(Fact).

  eager(ans(Atom)) :-                       
          my_clause(Head,Body),
          fact(call(_,_,Head)),
          append(Left,[pp(_,_,Atom)|Right],Body), 
          prove(Left),
          prove_right(Right),
          new(ans(Head)).

  eager(call(_,_, Atom)) :-                       
          my_clause(Atom,Body),
          prove_right(Body),
          new(ans(Atom)).

%% proving bodies (both gi and gd)

  prove([pp(_,_,B)|Bs]) :- 
        fact(ans(B)), prove(Bs).  
  prove([unify(A,B)|Bs]) :- 
        unify(A,B), prove(Bs).  
  prove([]).

  prove_right([pp(I,J,B)|_]) :-
      new(call(I,J,B)).
  prove_right([pp(_,_,B)|Bs]) :- 
      fact(ans(B)), prove_right(Bs).  
  prove_right([unify(A,B)|Bs]) :- 
      unify(A,B), prove_right(Bs).  
  prove_right([]).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% :- module(input_normalize,[load_file/1, my_clause/2]). %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% normalizes the clauses and marks the 
% body calls as program points


load_file(F) :-
    retractall(my_clause(_,_)),
	see(F),
	remember_all(1),
	seen.

remember_all(N) :-
	read(C),
	(
	    C == end_of_file -> true
	;
            N1 is N + 1,
	    remember_clause(C,N),
	    remember_all(N1)
	).

remember_clause((A :- Body),N) :-
	!,
        normalize(A,ANorm,As1-As2),
	tuple2list(Body,As2-[],N,1),
	assert(my_clause(ANorm,As1)).

remember_clause(A,_N) :-
        normalize(A,ANorm,Unifs-[]),
	assert(my_clause(ANorm,Unifs)).

normalize(Atom,ANorm,DUs) :-
    Atom =.. [Pred|Args],
    normalize_args(Args,VArgs,DUs),
    ANorm =.. [Pred|VArgs].

normalize_args([],[],X-X).
normalize_args([T|Ts], [V|Vs], [unify(V,T)|Us]-Us1) :-
    normalize_args(Ts,Vs,Us-Us1).


tuple2list((B,Bs),Bs1-Bs3,I,J) :-
	!, J1 is J+1,
        normalize(B,BNorm,Bs1-[pp(I,J,BNorm)|Bs2]),
	tuple2list(Bs,Bs2-Bs3,I,J1).

tuple2list(B,Bs1-Bs2,I,J) :-
    normalize(B,BNorm,Bs1-[pp(I,J,BNorm)|Bs2]).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%:- module(unification_operations, [unify/2]).              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

unify(A,B) :- domain(D),
    ( D = concrete -> A=B;true ),
    ( D = parity   -> parity(A,B);true ),
    ( D = parity1  -> parity1(A,B);true ),
    ( D = pos      -> pos_unify(A,B);true ),
    ( D = depth(_) -> A=B;true ),
    ( D = pattern  -> A=B;true ),
    ( D = parity_p -> parity_p(A,B);true ).


/* abstract unification for the parity domain: {odd,even} */

  parity(X,Y) :-
        nonvar(Y), Y=s(T),
        parity(S,T),
        (  S=even,X=odd;
           S=odd,X=even
        ).

  parity(even,Y) :-
        Y==0.
        
  parity(X,Y) :-
        (Y==even; Y==odd),
        X=Y.

  parity(X,Y) :-
        var(Y),
        X=Y.


/* abstract unification for the enhanced parity domain: 
                                         {zero,one,odd,even} */


 parity1(X,Y) :-
        nonvar(Y), Y=s(T),
        parity1(S,T),
        (  S=zero,X=one;
           S=one,X=even;
           S=even,X=odd;
           S=odd,X=even
        ).
  
  parity1(zero,Y) :-
        Y==0.
        
  parity1(X,Y) :-
        (Y==even; Y==odd; Y==zero; Y==one),
        X=Y.

  parity1(X,Y) :-
        var(Y),
        X=Y.


/* abstract unification for the pos domain */


pos_unify(X,Y) :-                                   
   var(Y), X=Y.                                 
pos_unify(X,Y) :-                                
   nonvar(Y),                                
   ( (Y == true ; Y == false) ->             
       X=Y                                   
   ;   (term_vars(Y,Vars), iff(X,Vars)) 
   ).

iff(true,[]).
iff(true,[true|Vars]) :- iff(true,Vars).
iff(false,Vars) :- member(false,Vars).

%% term_vars(T,V) :- 
%% V is the set of variables in term T.
%% almost the same as  term_variables/2 from library(terms)
%% but adapted so that if "false" is a  subterm of T then V contains
%% also the "false".

term_vars(T,V) :- term_vars(T,[],V).

term_vars(V,VIn,VOut) :- var(V),!, add_var(V,VIn,VOut).
term_vars(A,VIn,VOut) :- A = false,!, add_var(false,VIn,VOut).
term_vars(A,VIn,VIn) :- atom(A),!.
term_vars(T,VIn,VOut) :- T =.. [_|Args], term_vars_list(Args,VIn,VOut).

term_vars_list([],VIn,VIn).
term_vars_list([T|Ts],VIn,VOut) :-
    term_vars(T,VIn,V1),
    term_vars_list(Ts,V1,VOut).

add_var(V,[],[V]).
add_var(V,[V1|Vs],[V1|Vs]) :- V == V1,!.
add_var(V,[V1|Vs], [V1|V2s]) :- add_var(V,Vs,V2s).




/*  abstract unification for the parity domain where
    natural numbers are abstracted to parity and 
    lists by depth (done in the lub) 
 */

  parity_p(X,Y) :- parity(X,Y).

  parity_p(X,Y) :- 
         nonvar(Y),
         (Y = []; Y=[_|_]),
         X=Y.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% :- module(lub_operations, [lub/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.



lub(F1) :- 
    domain(D), points(P),
    ( (P,F1) = (off,call(_,_,G)) -> F=call(G) ; F = F1 ), 
    ( 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)).



% 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))).

 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))).

 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)).



%%% 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).





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% :- module(facts,[fact/1,showfacts/0]).  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


showfacts :-
         fact(F),
         numbervars(F,0,_),
         print(F), nl,
         fail ; true.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%:- module(domain,[domain/1,points/1,set_domain/1]).%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


set_domain(points(X)) :-
    write('program points set to '),write(X),nl,
    write('to change use set_domain(points(on/off))'),nl,nl,
    retractall(points(_)),
    assert(points(X)).

set_domain(domain(X)) :-
    write('domain set to '),write(X),nl,
    write('to change use set_domain(domain(D)) with:'),nl,
    write('  D = concrete '),nl,
    write('  D = parity '),nl,
    write('  D = parity1 '),nl,
    write('  D = pos '),nl,
    write('  D = pattern '),nl,
    write('  D = depth(K) '),nl,
    write('  D = parity_p '),nl,
     retractall(domain(_)),
     assert(domain(X)).






