%%% version 1.5.0-1

% 1
% Ri-Corretto bug nella definizione di dom_list (precisamente in dom_list3)
% (dom_list(R,{}).o dom_list([],{}) restituiva false)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Predicates for using {log} for the Test Template Framework (TTF)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%           by Maximiliano Cristia' and  Gianfranco Rossi
%                          January 2014 
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


:- consult_lib.
:- abolish.

%%% is_rel(R): true if R is a binary relation, i.e. a set
%%% of ordered pairs [X,Y]

 is_rel(R) :- 
    forall(P in R, pair(P)).


%%% in_dom(X,Rel): true if Rel is a relation and X belongs to
%%% its domain

 in_dom(X,Rel) :- 
    set(Rel) &
    [X,_] in Rel.


%%% nin_dom(X,R): true if X does not belong to the domain of the
%%% binary relation R
 
 nin_dom(X,R) :-
    forall(P in R, exists([X1],fst(P,X1) & X neq X1)).


%%% is_pfun(F): true if F is a partial function, i.e. a set 
%%% of ordered pairs such that for each two elements [X1,Y1] and
%%% [X2,Y2], X1=X2 ==> Y1=Y2

 is_pfun(S) :-
    delay(is_pfun0(S),nonvar(S)).
 is_pfun0(S) :-
    prolog_call((nonvar(S),dom_all_known(S),!,R = scan ; R = gen)) &
    (R == scan & prolog_call(is_pfun(S))
     or
     R == gen & is_pfun2(S)
    ). 

 is_pfun2(F) :- 
    forall(P1 in F, forall(P2 in F, nofork(P1,P2))).

 nofork([X1,Y1],[X2,Y2]) :-  
    (X1 neq X2 or (X1 = X2 & Y1 = Y2)).


%%% apply(F,X,Y): true if Y is the result of applying F to X

 apply(F,X,Y) :-
    [X,Y] in F.


%%% dom(Rel,Dom): true if Rel is a relation and Dom is its domain 
%%% (either a set or an interval)
 
 dom(Rel,Dom) :-
     delay(dom0(Rel,Dom),nonvar(Dom) or nonvar(Rel)).
 dom0(Rel,Dom) :-
     prolog_call((nonvar(Dom),var(Rel),Dom = int(A,B),!,R = int ; 
                  nonvar(Dom),var(Rel),!,R = setnvar ;
                  R = setvar)) &
     dom(R,Rel,Dom). 

 %%% dom(setvar,Rel,Dom)
 dom(setvar,{},{}).
 dom(setvar,{[X,Y]/Rel},Dom) :-
      Dom = {X/D} &
      [X,Y] nin Rel &     
      dom0(Rel,D).    
 
 %%% dom(setnvar,Rel,Dom), where Dom is a non-var set and Rel is a var
 dom(setnvar,{},{}).
 dom(setnvar,{[X,Y]/Rel},Dom) :-
     Dom = {X/D} & [X,Y] nin Rel &
     dom0(Rel,D).    

 %%% dom(int,Rel,Dom), where Dom is an interval
 dom(int,{},Dom) :-
     eq(Dom,int(A,B)) &
     A > B.  
 dom(int,{[A,Y]},Dom) :-
     eq(Dom,int(A,A)).  
 dom(int,{[A,Y]/Rel},Dom) :-
     eq(Dom,int(A,B)) &
     A < B &
     A1 is A + 1 & 
     D = int(A1,B) &
     dom(int,Rel,D).

 dom_size_rel(Rel,Dom,N) :-    % size(Rel) >= N   
     solve(size(Rel,M) & 
     M >= N) &  
     dom(Rel,Dom).
   
 dom_size_pfun(Rel,Dom) :-     % size(Rel) = size(Dom)  (not used, yet) 
     solve(size(Rel,M) & 
     size(Dom,N) &
     M = N) &  
     dom(Rel,Dom).


%%% dom_list(L,Dom): true if L is a list of n elements (n >= 0)
%%% and Dom is the interval 1..n (n > 0) or the empty set (n = 0).  

 dom_list(L,Dom) :-
     prolog_call((nonvar(Dom),!,R = int ; R = set)) &
     (R == int & dom_list3(L,Dom)
      or
      R == set & dom_list2(L,Dom)
     ). 

 %%% dom_list2(?L,-Dom) 
 dom_list2([],Dom) :-  
     Dom = {}.
 dom_list2([X|L],Dom) :-
     length([X|L],SList) &
     call(Dom = int(1,SList)).

 %%% dom_list3(?L,+Dom)         
 dom_list3([],Dom) :-          
     eq(Dom,{}).
 dom_list3(L,Dom) :-          
     Dom = int(1,B) &
     1 =< B &      
     labeling(B) &
     length(L,B)!.
 %dom_list3(L,Dom) :-  % could be useful if Dom can be also a set? TO BE tested
 %    (functor(Dom,with,2) or functor(Dom,{},0)) &
 %    size(Dom,B) &
 %    length(L,B)!.


%%% ran(Rel,Ran): true if Rel is a relation and Ran is its range  
%%% (either a set or an interval)

 ran(Rel,Ran) :-
     delay(ran0(Rel,Ran),nonvar(Ran) or nonvar(Rel)).
 ran0(Rel,Ran) :-
     prolog_call((nonvar(Ran), Ran = int(A,B), !, R = int ; R = set)) &
     (R == int & ran3(Rel,Ran) 
      or
      R == set & ran2(Rel,Ran)
     ). 

 %%% ran2(Rel,Ran), where Ran is either a variable or a set
 ran2({},{}).
 ran2({[X,Y]/Rel},Ran) :-
     Ran = {Y/R} &
     [X,Y] nin Rel &
     ran0(Rel,R).    

 %%% ran3(Rel,Ran), where Ran is an interval
 ran3({},Ran) :-
     eq(Ran,int(A,B)) &
     A > B.  
 ran3({[X,A]},Ran) :-
     eq(Ran,int(A,A)).  
 ran3({[X,A]/Rel},Ran) :-
     eq(Ran,int(A,B)) &
     A < B &
     A1 is A + 1 & 
     R = int(A1,B) &
     ran3(Rel,R).

 ran_subset_ran(Rel,Ran,S) :-      % size(Ran) =< N
     solve(size(Ran,M) & size(S,SS) & 
     M =< SS) &  
     ran(Rel,Ran).
  
 ran_size_rel(Rel,Ran,N) :-        % size(Rel) >= N   (not used, yet)
     solve(size(Rel,M)) & 
     M >= N  &  
     ran(Rel,Ran).

 ran_size_ran(Rel,Ran,N) :-        % size(Ran) =< N   (not used, yet)
     solve(size(Ran,M)) & 
     M =< N  &  
     ran(Rel,Ran).


%%%% ran_list(S,R)

 ran_list(S,R) :- 
    list_to_set(S,R).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% Composition of binary relations. comp(Q,R,QR) is true if 
%%% [X,Y] in Q & [Y,Z] in R <==> [X,Z] in QR

comp(Q,R,{}) :-
   forall(P in Q, exists([X,Y,Z], P=[X,Y] & notYinR(Y,R))).
comp({[X,Y]/Qel},R,{[X,Z]/S1}) :- 
   [X,Y] nin Qel &            
   [Y,Z] in R &
   comp(Qel,R,S1).

notYinR(Y,{}).
notYinR(Y,{[X,Z]/R}) :-
   [X,Z] nin R &
   Y neq X &
   notYinR(Y,R).  

comp0({},R,{}).               %Alternative definition
comp0(Q,{},{}).
comp0(Q,R,QR) :-
   Q neq {} & R neq {} &
   QR = {P : exists([X,Y,Z], P=[X,Z] & [X,Y] in Q & [Y,Z] in R)}.


%%% Composition of binary relations. circ(Q,R,QR) is true if 
%%% [X,Y] in R & [Y,Z] in Q <==> [X,Z] in QR

circ(Q,R,S) :- 
   comp(R,Q,S).


%%% Domain restriction: dres(A,R,S) is true if A is a set, 
%%% R is a binary relation, and S is the set of pairs
%%% [X,Y] belonging to R such that X in A.

dres(A,{},{}). 
dres(A,{[X,Y]/Rel},{[X,Y]/Q}) :-
   [X,Y] nin Rel & 
   X in A &
   dres(A,Rel,Q).
dres(A,{[X,Y]/Rel},Q) :-
   [X,Y] nin Rel & 
   X nin A &
   dres(A,Rel,Q).

dres0(A,{},{}) :- A neq {}.   %Alternative definition
dres0({},R,{}) :- R neq {}.
dres0(A,R,S) :-
   A neq {} & R neq {} &
   S = {P : exists([X,Y], P=[X,Y] & [X,Y] in R & X in A)}.


%%% Range restriction: rres(A,R,S) is true if A is a set, 
%%% R is a binary relation, and S is the set of pairs
%%% [X,Y] belonging to R such that Y in A.

rres(A,{},{}). 
rres(A,{[X,Y]/Rel},{[X,Y]/Q}) :-
   [X,Y] nin Rel & 
   Y in A &
   rres(A,Rel,Q).
rres(A,{[X,Y]/Rel},Q) :-
   [X,Y] nin Rel & 
   Y nin A &
   rres(A,Rel,Q).

rres0(A,{},{}) :- A neq {}.   %Alternative definition
rres0({},R,{}) :- R neq {}.
rres0(A,R,S) :-
   S = {P : exists([X,Y], P=[X,Y] & [X,Y] in R & Y in A)}.


%%% Domain anti-restriction: ndres(A,R,S) is true if A is a set, 
%%% R is a binary relation, and S is the set of pairs
%%% [X,Y] belonging to R such that X nin A.

ndres(A,{},{}). 
ndres(A,{[X,Y]/Rel},{[X,Y]/Q}) :-
   [X,Y] nin Rel & 
   X nin A &
   ndres(A,Rel,Q).
ndres(A,{[X,Y]/Rel},Q) :-
   [X,Y] nin Rel & 
   X in A &
   ndres(A,Rel,Q).

ndres0(A,{},{}) :- A neq {}.   %Alternative definition
ndres0({},R,{}) :- R neq {}.
ndres0(A,R,S) :-
   S = {P : exists([X,Y], P=[X,Y] & [X,Y] in R & X nin A)}.


%%% Range anti-restriction: nrres(A,R,S) is true if A is a set, 
%%% R is a binary relation, and S is the set of pairs
%%% [X,Y] belonging to R such that Y nin A.

nrres(A,{},{}). 
nrres(A,{[X,Y]/Rel},{[X,Y]/Q}) :-
   [X,Y] nin Rel & 
   Y nin A &
   nrres(A,Rel,Q).
nrres(A,{[X,Y]/Rel},Q) :-
   [X,Y] nin Rel & 
   Y in A &
   nrres(A,Rel,Q).

nrres0(A,{},{}) :- A neq {}.   %Alternative definition
nrres0({},R,{}) :- R neq {}.
nrres0(A,R,S) :-
   S = {P : exists([X,Y], P=[X,Y] & [X,Y] in R & Y nin A)}.


%%% Inverse relation. inv(Q,R) is true if Q is a binary relation
%%% and R its inverse, i.e., R = {[Y,X] : [X,Y] in Q}

inv({},{}).
inv({[X,Y]/Rel},{[Y,X]/Q}) :- 
   [X,Y] nin Rel &            
   inv(Rel,Q).

inv0({},{}).                   %Alternative definition
inv0(Q,R) :- 
   R = {P : exists([X,Y], P=[Y,X] & [X,Y] in Q)}.


%%% Relational image. rimg(R,A,S) is true if S is the set of Y
%%% such that [X,Y] belongs to R and X belongs to A.

rimg({},A,{}).
rimg({[X,Y]/Rel},A,{Y/B}) :- 
   [X,Y] nin Rel &             
   X in A & 
   rimg(Rel,A,B).
rimg({[X,Y]/Rel},A,B) :- 
   [X,Y] nin Rel &             
   X nin A & 
   rimg(Rel,A,B).


%%% Overriding ("\oplus"). oplus(R,G,S) is true if R and G are 
%%% binary relations, and S is the union of R and G except those 
%%% elements [X,Y] of R s.t. X in dom(G) 

oplus(R,G,S) :- 
   dom(G,D) & 
   ndres(D,R,S1) & 
   un(S1,G,S).


%%% list_to_rel(L,R): true if L is a list of n elements e_1,...,e_n (n>=0)
%%% and R is a binary relation of the form {[1,e_1],...,[n,e_n]}

list_to_rel([],{}).
list_to_rel([X|List],Rel) :- 
   Rel = {[1,X]/R} & 
   [1,X] nin R & 
   list_to_rel0(List,R,2).

list_to_rel0([],{},N).
list_to_rel0([X|List],Rel,N) :-
   Rel = {[N,X]/R} &
   K is N + 1 &
   list_to_rel0(List,R,K).


%%% extract(S,L,NewL): true if S is a set of integer numbers, L is a 
%%% list of elements of any type, and NewL is a list containing
%%% the i-th element of L, for all i in S
%%% (e.g., extract({4,2},[a,h,g,m,t,r],L) ==> L = [h,m])

extract({},List,[]).
extract(Set,[],[]).
extract(Set,List,NewList) :- 
   set_to_list(Set,L) & 
   prolog_call(sort(L,SL)) & 
   extract0(SL,List,NewList).

extract0([],List,[]).
extract0([N | IndexList], List, NewList) :-
   nth1(N,List,E) &
   NewList = [E | L] &
   extract0(IndexList,List,L).


%%% filter(L,S,NewL): true if L is a list, S is a set, and NewL is a 
%%% list containing the elements of L that are also elements of S; 
%%% L and NewL also verify the following sublist(NewL, L).
%%% (e.g., filter([a,h,g,m,t,r],{m,h,s},L) ==> L = [h,m])

filter(List,{},[]).
filter([],Set,[]) :-
   Set neq {}.
filter([X|List],Set,[X | L]) :-   
   X in Set &
   filter(List,Set,L).
filter([X|List],Set,NewList) :-
   Set neq {} &
   X nin Set & 
   filter(List,Set,NewList).


%%% squash(S,L): true if S is a set of ordered pairs whose first
%%% components are natural numbers >= 1, L is a list containing
%%% the elements Y, for all [X,Y] in S, and L is ordered according
%%% to the values of X (e.g., squash({[2,a],[7,b],[4,c]},L) ==>
%%% [a,c,b])

squash({},[]).
squash(Rel,List) :- 
   Rel neq {} & List neq [] &
   dom(Rel,D) & 
   set_to_list(D,LD) & 
   prolog_call(sort(LD,SLD)) & 
   squash0(Rel,SLD,List).

squash0(Rel,[],[]).
squash0(Rel,[N|List],NewList) :-
   [N,X] in Rel &
   NewList = [X|L] &
   squash0(Rel,List,L).


%%%%%%%%%%%%%%% Auxiliary predicates

 pair([X,Y]).

 fst([X,Y],X).

 snd([X,Y],Y).

 set_to_list({},[]).          % true if S is a set and L is a list containing 
 set_to_list({X/Set},List) :- % all and only the elements of S, WITHOUT REPETITIONS
    X nin Set &
    List = [X|L] & 
    set_to_list(Set,L).


%%%%%%%%%%%%%%% Using delay

 dis_rel(R) :- 
    delay(is_rel(R), nonvar(R)).

 ddom_list(L,Dom) :- 
    delay(dom_list(L,Dom), nonvar(L) & nonvar(Dom)).


%%%%%%%%%%%%%%% General set-theoretic operations

%%% Generalized union ("\bigcup"). 
%%% bun(S,R) is true if R is the union of all the elements
%%% of the set of sets S

bun({},{}).
bun({A/Set},S) :-  
  A nin Set &               
  bun(Set,T) & 
  un(A,T,S).


%%% Generalized intersection ("\bigcap"). 
%%% binters(S,R) is true if R is the inersection of all the 
%%% elements of the set of sets S

binters({A},A).
binters({A/Set},S) :-  
  A nin Set &               
  binters(Set,T) & 
  inters(A,T,S).


%%%%%%%%%%%%%%% Auxiliary predicates - Prolog code

 setlogTTF_prolog :-
    prolog_call(assert((user:is_pfun({}) :- !))) &
    prolog_call(assert((user:is_pfun(S) :- S = (PFun with P), is_pfun_cont(PFun,P), is_pfun(PFun)))) &

    prolog_call(assert((user:is_pfun_cont({},_P1) :- !))) &
    prolog_call(assert((user:is_pfun_cont(S,P1) :- S = (F1 with P2), nofork(P1,P2), is_pfun_cont(F1,P1)))) &

    prolog_call(assert((user:nofork([X1,_Y1],[X2,_Y2]) :- X1 \== X2,!))) &
    prolog_call(assert((user:nofork([X1,Y1],[X2,Y2]) :- X1 = X2, Y1 = Y2))) &

    prolog_call(assert((user:dom_all_known({}) :- !))) &
    prolog_call(assert((user:dom_all_known(S) :- S = (PFun with [X,_]), nonvar(X), dom_all_known(PFun)))).

:- setlogTTF_prolog.