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

   Contents: Prolog predicates writing Coq code.
   
   Usage: See examples of use in examples/endofun/prolog/endofun.pl. */

/* 1. Auxiliary predicates. */
 
/* increasing(K,I,J) holds iff K is in the interval [I..J].
    Generation in increasing order by backtracking. */
increasing(I,I,J) :- J >= I.
increasing(K,I,J) :- J > I, Ip1 is I+1, increasing(K,Ip1,J).

/* nth(L,I,J) iff 0 <= I <= len(L)-1 and J is the (I+1)-th element 
   of the list L. */
nth([X|_],0,X).
nth([_|M],I,J) :- I > 0, Im1 is I-1, nth(M,Im1,J).  

/* 2. Coq writing predicates. */

/* Writes X = 0 \/ X = 1 \/ ... X = N for N >= 0. */
write_coq_nat(X,0) :- write(X), write(' = 0').
write_coq_nat(X,N) :- N > 0, Nm1 is N-1, 
 write_coq_nat(X,Nm1), write(' \\/ '), write(X), write(' = '), write(N).

/* Writes a Prolog list as a Coq list. */
write_list([A|R]) :- write(A), write('::'), write_list(R).
write_list([]) :- write('nil').

/* write_coq_proof_X_leq_Y(X,Y) writes a Coq proof that X <= Y:
   (leb_complete X Y eq_refl). */
write_coq_proof_X_leq_Y(X,Y) :-
 write('(leb_complete '),
 write(X), write(' '), write(Y), 
 write(' eq_refl)').
