%%% version 1.0-0

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%    {log} library for dealing with arrays (as partial functions)
%                         Version 1.0
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%           by Maximiliano Cristia' and  Gianfranco Rossi
%                           April 2026 
%
%                 (requires setlog499-2d or newer) 
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


% In the following, whenever we say "if A is an array"
% we mean that arr(A,N) holds for some N.


% A is a function whose domain is the interval [M,N]
% with 1 =< M.
% A more specific predicate to work with arrays is arr/2
%
arr(A,M,N) :-
  1 =< M & M =< N &
  pfun(A) &
  K is N - M + 1 &
  size(A,K) &
  foreach([X,Y] in A, M =< X & X =< N).

% An array A of length N is a set of ordered pairs that is forced by
% the pfun constraint to  be a (partial) function with a domain equal 
% to the interval [1,N]. 
% Ex.: arr({[1,5],[2,3],[3,8],[4,2]},4). --> true (the array ⟨5,3,8,2⟩)
%
arr(A,N) :- arr(A,1,N).

% If A is a function with domain in the integers,
% iarr(A) states that A is injective. Since arrays have
% domains in the integers, when A is an array, iarr(A)
% states that A is injective (i.e. there are no repeated
% elements). If A's domain is not a subset of the integers,
% then use ipfun/1.
%
iarr(A) :-
  foreach([[X1,Y1] in A, [X2,Y2] in A], X1 < X2 implies Y1 neq Y2).
  
% If R is a function, ipfun(R) states R is injective.
%
ipfun(R) :-
  foreach([[X1,Y1] in R, [X2,Y2] in R], X1 neq X2 implies Y1 neq Y2).

% S is the set of ordered pairs of R whose first components
% are equal to Z.
%
dres_a(Z,R,S) :-
  un(S,N,R) &
  foreach([X,Y] in S, X = Z) &
  foreach([X,Y] in N, X neq Z).

% S is the set of ordered pairs of R whose first components
% belong to [K,M]. R's domain must be a subset of the
% integers.
%
dres_a(K,M,R,S) :-
  un(S,N,R) &
  foreach([X,Y] in S, K =< X & X =< M) &
  foreach([X,Y] in N, X < K or M < X).

% Negation of dres_a/4.
%
n_dres_a(K,M,R,S) :-
  S = {[X,Y]/S1} & X nin int(K,M)
  or
  S = {[X,Y]/S1} & [X,Y] nin R
  or
  X in int(K,M) & R = {[X,Y]/R1} & [X,Y] nin S.

% S is the set of ordered pairs of R whose first component
% is not Z.
%
dares_a(Z,R,S) :-
  un(S,N,R) &
  foreach([X,Y] in S, X neq Z) &
  foreach([X,Y] in N, X = Z).

% S is the set of ordered pairs of R whose first component
% doesn't belong to [K,M]. R's domain must be a subset of
% the integers.
%
dares_a(K,M,R,S) :-
  un(S,N,R) &
  foreach([X,Y] in S, X < K & M < X) &
  foreach([X,Y] in N, K =< X & X =< M).

% Reading array A at position X.
% If A is an array then Y is the element stored at
% index X.
%
get(A,X,Y) :- [X,Y] in A.

% Array update at position X with element Y.
% If A is an array, then B is equal to A except
% at index X where B is equal to Y.
%
upd(A,X,Y,B) :-
  A = {[X,W] / N} & [X,W] nin N & B = {[X,Y] / N}.

% Update map H with the pair [K,V]:
%   - if key K already belongs to H then V
%     is the new value associated to K
%   - if it doesn't then [K,V] is added to H
%   - in any case T is the new map
%
put(H,K,V,T) :-
  H = {[K,Q] / N} & [K,Q] nin N &
  T = {[K,V] / N}
  or
  foreach([X,Y] in H, X neq K) &
  T = {[K,V] / H}.

% Removes key K from map H; T is the resulting map
%
remove(H,K,T) :-
  H = {[K,Q] / T} & [K,Q] nin T
  or
  foreach([X,Y] in H, X neq K) &
  T = H.

% If A is an array of length N, then is sorted
% from index K up until index M
%
sorted(A,N,K,M) :-
  1 =< K & K =< M & M =< N &
  foreach([[I1,E1] in A,[I2,E2] in A],
    K =< I1 & I1 < I2 & I2 =< M implies E1 =< E2
  ).

% If A is an array of length N, then is sorted
% from index 1 up until index M
%
sorted(A,N,M) :-
  foreach([[I1,E1] in A,[I2,E2] in A],
    1 =< I1 & I1 < I2 & I2 =< M implies E1 =< E2
  ).

% If A is a function whose domain and range are
% subsets of the integers, then A is sorted
%
sorted(A) :-
  foreach([[I1,E1] in A,[I2,E2] in A],I1 < I2 implies E1 =< E2).

% If A is an array and M1 =< K2, then all the
% elements if A with indices in [K1,M1] are
% less than or equal to all the elements with
% indices in [K2,M2]
%
partitioned(A,K1,M1,K2,M2) :-
  dres_a(K1,M1,A,N1) &
  M1 =< K2 &
  dres_a(K2,M2,A,N2) &
  foreach([[X1,Y1] in N1, [X2,Y2] in N2], Y1 =< Y2).

% Same as above but implemented with foreach
%
partitioned_fe(A,K1,M1,K2,M2) :-
  foreach([[X1,Y1] in N1, [X2,Y2] in N2],
    K1 =< X1 & X1 =< M1 & M1 =< K2 & K2 =< X2 & X2 =< M2 implies Y1 =< Y2).

% If A is an array then I is the smallest
% index whose element is X, if such element
% exists in A.
%
findf(A,N,X,I) :-
  I =< N &
  get(A,I,X) &
  foreach([J,Y] in A, 1 =< J & J < I implies Y neq X).

% If A is a set of ordered pairs whose
% second components are integer numbers, then
% M is the minimum of the second components
% of A
%
amin(A,M) :-
  exists([J,Y] in A, M = Y) &
  foreach([J,Y] in A, M =< Y).

% If A is an array, then M is greater than or
% equal to the first I components of A
%
agta(A,I,M) :-
  foreach([Q,W] in A, 1 =< Q & Q =< I implies W =< M).

% A is a partial function
%
pfun_fe(A) :-
  foreach([[X1,Y1] in A, [X2,Y2] in A],X1 = X2 implies Y1 = Y2).