/*******************************************************************************/
/* 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: permut.pl

   Contents: Validation of examples/coq/permut.v by counting and 
   bounded-exhaustive testing (BET). */

/* 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. Permutations in one-line notation. */

/* The permutation p on {0,...,n-1} is represented by the list
   [p(0),...,p(n-1)] called its 'one-line notation'. Any such list
   contains each element of {0,...,n-1} exactly once. */

/* line(L,K,N) iff L is a linear list (no duplicates) of length K 
   with elements in {0,...,N-1}. */
line([],0,_).
line([Y|P],K,N) :- K > 0, Km1 is K-1, Nm1 is N-1, in(Y,0,Nm1), 
 line(P,Km1,N), \+ member(Y,P).

/* line(L,N) iff L is a linear list (no duplicates) of length N 
   with elements in {0,...,N-1}. Corresponds to:
   - (is_permut n) in permut.v, as a characteristic predicate,
   - (permut n) in permut.v, as a datatype
   - gen_permutl in val_qc_permut.v, as a data generator. */
line(P,N) :- line(P,N,N).
