%%% version 1.0-3

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%      {log} standard library for dealing with lists (as sets)
%                           Version 1.0
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%           by Maximiliano Cristia' and  Gianfranco Rossi
%                           October 2019 
%
%    (requires {log} with RIS - setlog496-17i or newer) 
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% These definitions follow the standard definitions given in
% the Z mathematical toolkit regarding lists (called sequences).
% See for example:
%
% Saaltink, M.: The Z/EVES mathematical toolkit version 2.2 for 
% Z/EVES version 1.5. Tech. rep., ORA Canada (1997)
%
% Spivey, J. M. The Z notation: a reference manual Prentice Hall
% International (UK) Ltd., 1992
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- consult_lib.

%%% slits(S): true if S is a set representing a list. This means
%%% that S is a partial function whose domain is equal to [1,n]
%%% for some natural n

slist(S) :- 
  pfun(S) & 
  dom(S,D) &
  size(D,N) &
  subset(D,int(1,N)).

%%% shead(S,H): true if H is the first element of list S

shead(S,H) :- 
  slist(S) & 
  [1,H] in S.

%%% slast(S,L): true if L is the last element of list S

slast(S,L) :- 
  pfun(S) & 
  dom(S,D) &
  size(D,N) &
  subset(D,int(1,N)) &
  [N,L] in S.

%%% sadd(S,E,T): true if T is the list obtained by appending E to the list S

sadd(S,E,T) :- 
  pfun(S) & 
  dom(S,D) &
  size(D,N) &
  subset(D,int(1,N)) &
  M is N + 1 &
  T = {[M,E] / S}.

%%% sfront(S,T): true if T is a list equal to list S minus its last element

sfront(S,T) :-
  S = {[N,_] / T} & 
  pfun(S) & 
  dom(S,D) &
  size(D,N) &
  subset(D,int(1,N)) &
  comp({[N,N]},T,{})
  or
  S = {} & T = {}.

%%% stail(S,T): true if T is a list equal to the tail of list S

stail(S,T) :-
  slist(S) &
  S = {[1,_] / U} & comp({[1,1]},U,{}) &
  T = ris([X,Y] in U, [K], true, [K,Y], K is X - 1)
  or
  S = {} & T = {}.

%%% sappend(S,T,U): true if U is a list equal to the concatenation of
%%% lists S and T

sappend(S,T,U) :-
  slist(S) &
  slist(T) &
  size(S,N) &
  un(S,ris([A,B] in T,[K],true,[K,B],K is A + N),U).

%%% sfilter(A,S,T): true if T is a list equal to S after removing from
%%% it the elements located in all the positions given by set A

sfilter(A,S,T) :- 
  slist(S) & 
  dres(A,S,R) & 
  squash(R,T).

%%% sextract(S,A,T): true if T is a list equal to S after removing from
%%% it the elements given by set A

sextract(S,A,T) :- 
  slist(S) & 
  rres(S,A,R) & 
  squash(R,T).

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

ssquash({},{}).
ssquash({X/Rel},{Y/List}) :- 
   X nin Rel & Y nin List &
   pfun({X/Rel}) &
   dom({X/Rel},D) & 
   set_to_list(D,LD) & 
   prolog_call(sort(LD,SLD)) & 
   squash0({X/Rel},SLD,1,{Y/List}).

squash0(_,[],_,{}).
squash0(Rel,[N|List],1,LSet) :-
   integer(N) &
   [N,X] in Rel &
   LSet = {[1,X] / L} & [1,X] nin L &
   squash0(Rel,List,2,L).
squash0(Rel,[N|List],K,LSet) :-
   integer(N) &
   [N,X] in Rel &
   LSet = {[K,X] / L} & [1,X] nin L &
   K1 is K + 1 &
   squash0(Rel,List,K1,L).