/*******************************************************************************/
/* Coq Unit Testing project                                                    */
/* Copyright 2015-2016 Catherine Dubois, Richard Genestier and Alain Giorgetti */ 
/* Samovar - FEMTO-ST institute                                                */
/*******************************************************************************/
/*      This file is distributed under the terms of the                        */
/*       GNU Lesser General Public License Version 2.1                         */
/*******************************************************************************/

/* File: examples/endofun/prolog/endofun.pl.

   Contents: Specification of the one-line notation of endofunctions
   on some finite subset {0,...,n-1} of natural numbers. */

/* in(K,I,J) holds iff K is in the interval [I..J]. */
in(J,I,J) :- J >= I.
in(K,I,J) :- J > I, J1 is J-1, in(K,I,J1).

/* 1. Endofunctions in one-line notation. */

/* The function f on {0,...,n-1} is represented by the list
   [f(0),...,f(n-1)] called its 'one-line notation'. */

/* line_endo(L,N,K) iff L is a list of length N with elements in {0,...,K}. */
line_endo([],0,_).
line_endo([V|M],N,K) :- N > 0, Nm1 is N-1, in(V,0,K), line_endo(M,Nm1,K).

/* line_endo(L,N) iff L is (the one-line notation of) an endofunction
   on {0,...,N-1}. Corresponds to (is_endoline L) defined in 
   examples/coq/endoline.v, as a characteristic predicate, when N = length L. */
line_endo(L,N) :- Nm1 is N-1, line_endo(L,N,Nm1).

/* 2. Specification of insertion in a function in one-line notation. 

   Corresponds to insert_fun in endofun.v. */

/* Let F be a list of length N. F is the one-line notation of some function
   [F] from {0,...,N-1} to ran([F]) = set(F), where set(F) denotes the set
   of elements in the list F. 
   
   insert(F,I,G) holds iff G is the one-line notation of the function [G] on
   {0,...,N} such as:
   - N is the length of F,  
   - [G] is [F] completed with [G](N) = N if F does not contain I.
   - [G] is [F] modified at N by [G](N) = I and at J by [G](J) = N if 
     F contains I and [F](J) = I. The specification of this case
     can be illustrated as follows:
        
        0          X            J       Y            N-1       N
   F = [F[0], ..., [F](X), ..., I, ..., [F](Y), ..., [F](N-1)], 
   G = [G[0], ..., [F](X), ..., N, ..., [F](Y), ..., [F](N-1), I],
   F1 is [F[0], ..., [F](J-1)], 
   F2 is [[F](J+1), ..., [F](N-1)],
   J is the length of F1,
   G1 = [G[0], ..., [F](X), ..., N, ..., [F](Y), ..., [F](N-1)]. */
insert(F,I,N,G) :- append(F1,[I|F2],F), append(F1,[N|F2],G1), append(G1,[I],G).
insert(F,I,N,G) :- \+ member(I,F), append(F,[N],G).

insert(F,I,G) :- length(F,N), insert(F,I,N,G).

/* 3. Specification of the direct sum on one-line notations. 

   Corresponds to sum_fun in endofun.v. */

/* Let F1 (resp. F2) be a list of length N1 (resp. N2). F1 (resp. F2)
   is the one-line notation of some function [F1] on {0,...,N1-1} 
   (resp. [F2] on {0,...,N2-1}).
   
   sum(F1,F2,G) holds iff G is the (one-line notation) of the direct sum
   [G] of the functions [F1] and [F2], defined by:
   - G[X] = F1[X] if 0 <= X < N1 and
   - G[X] = F2[X-N1]+N1 if N1 <= X < N1+N2.
   
   As lists, we have:
   F1 = [F1[0], ..., [F1](N1-1)],
   F2 = [F2[0], ..., ..., [F2](N2-1)],
   G2 = [F2[N1], ..., ..., [F2](N1+N2-1)],
   G = [F1[0], ..., [F1](N1-1)], F2[N1], ..., ..., [F2](N1+N2-1)]. */
   
/* add(F,N,G) iff G is the list obtained from F by adding N to each of
   its elements. */
add([],_,[]).      
add([X|F],N,[XpN|G]) :- XpN is X+N, add(F,N,G).
    
sum(F1,F2,G) :- length(F1,N1), add(F2,N1,G2), append(F1,G2,G).
