/*******************************************************************************/
/* Coq Unit Testing project                                                    */
/* Copyright 2018 Catherine Dubois 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/bet_endoline.pl.

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

:- compile('../../../prolog/measure'). /* For validation by counting. */
:- compile('../../../prolog/cut').     /* For validation by BET. */

:- compile(endofun). /* Specification of endofunctions in one-line notation. */

/* 1. Validation by counting. */

:- write('Validation of line_endo by counting:'), nl, iterate(0,6,line_endo).
% 1,1,4,27,256,3125,46656. n^n. https://oeis.org/A000312.

/* 2. Validations by BET: Generation of Coq code.

   The predicates write_coq* below are adaptations to Coq of the predicate
   write_all defined in the validation library written by Valerio Senni. */

/* 2.1. Test suites. */

/* Test suite 1: Validation of the Coq function is_endolineb. */
write_coq_1(PredSym,SizeMax) :-
 increasing(Size,0,SizeMax),
 (settings(fd_on) -> SizeT=Size; nat2term(Size,SizeT)),
 Pred=..[PredSym,L,SizeT],  /* Pred is the generator */
 Pred, 
 write('Eval compute in (is_endolineb ('),
 write_list(L), write(')).'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_1(_,_).

/* Test suite 2: Validation of the Coq predicate is_endoline with a 
   non-reflexive proof. */
write_coq_2(PredSym,SizeMax) :-
 increasing(Size,1,SizeMax),
 (settings(fd_on) -> SizeT=Size; nat2term(Size,SizeT)),
 Pred=..[PredSym,L,SizeT],  /* Pred is the generator */
 Pred, 
 write('Goal is_endoline ('),
 write_list(L), write(').'), nl,
 write('unfold is_endoline. simpl. repeat (constructor; try omega). Qed.'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_2(_,_).

/* Test suite 3: Validation of is_endoline with a reflexive proof. */
write_coq_is_endoline_refl(PredSym,SizeMax) :-
 increasing(Size,1,SizeMax),
 (settings(fd_on) -> SizeT=Size; nat2term(Size,SizeT)),
 Pred=..[PredSym,L,SizeT],  /* Pred is the generator */
 Pred, 
 write('Goal is_endoline ('),
 write_list(L), write(').'), nl,
 write('apply is_endoline_dec. simpl. auto. Qed.'), nl,
 nl, flush_output,
 fail. % this causes backtracking
write_coq_is_endoline_refl(_,_).

/* Test suite 4: Validation that cons preserves endofunctions (under some condition). 
   Model: 
   Eval compute in (is_endolineb (cons 3 (2::2::0::nil))). */
write_coq_cons_endo(PredSym,SizeMax) :-
 increasing(Size,0,SizeMax),
 (settings(fd_on) -> SizeT=Size; nat2term(Size,SizeT)),
 Pred=..[PredSym,L,SizeT],  /* Pred is the generator */
 Pred, 
 increasing(N,0,Size),
 write('Eval compute in (is_endolineb (cons '),
 write(N),
 write(' ('),
 write_list(L),
 write('))).'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_cons_endo(_,_).

/* Test suite 5: Validation that lifting preserves endofunctions, limited to
   a position smaller than the size of the endofunction + 2. 
   Model: 
   Eval compute in (is_endolineb (lift 5 (2::2::0::nil))). */
write_coq_lift_endo(PredSym,SizeMax) :-
 increasing(Size,0,SizeMax),
 (settings(fd_on) -> SizeT=Size; nat2term(Size,SizeT)),
 Pred=..[PredSym,L,SizeT],  /* Pred is the generator */
 Pred,
 SizeP2 is Size+2,
 increasing(P,0,SizeP2),
 write('Eval compute in (is_endolineb (lift '),
 write(P),
 write(' ('),
 write_list(L),
 write('))).'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_lift_endo(_,_).

/* 2.2. One predicate for all the validations of Coq concerning endofunctions in one-line notation. */
write_coq_endoline(PredSym,SizeMax) :-
 write('(* Test suite 1: Validation of is_endolineb. *)'), nl,
 write_coq_1(PredSym,SizeMax), nl, nl,
 write('(* Test suite 2: Validation of is_endoline with a non-reflexive proof. *)'), nl,
 write_coq_2(PredSym,SizeMax), nl, nl,
 write('(* Test suite 3: Validation of is_endoline with a reflexive proof. *)'), nl,
 write_coq_is_endoline_refl(PredSym,SizeMax), nl, nl,
 write('(* Test suite 4: Validation that cons preserves endofunctions (lemma cons_endo). *)'), nl,
 write_coq_cons_endo(PredSym,SizeMax), nl, nl,
 write('(* Test suite 5: Validation that lifting preserves endofunctions (lemma lift_endo). *)'), nl,
 write_coq_lift_endo(PredSym,SizeMax),
 nl.


/* 2.3. Coq file opening and closing, with header and time measures. */
write_coq_open_close_file(Size,PredSym,File) :-
 tell(File),
  write('(* File generated by code in endofun/prolog/bet_endoline.pl. *)'), nl,
  write('Require Import Arith Arith.Bool_nat Omega List.'), nl,
  write('Require Import listnat blist endoline cut.'), nl, 
  write('Set Implicit Arguments.'), nl, nl, 
  ((system_type(sicstus);system_type(swi)) -> statistics(runtime,[T1,_]) ; true),
  ((system_type(gnu)) -> statistics(user_time,[T1,_]) ; true),
  write_coq_endoline(PredSym,Size),
  ((system_type(sicstus);system_type(swi)) -> statistics(runtime,[T2,_]) ; true),
  ((system_type(gnu)) -> statistics(user_time,[T2,_]) ; true),
  Time is T2-T1,
  write('(* Time: '), write(Time), write(' ms'), write(' *)'),
 told.

/* 2.4. Some output before writing in the Coq file. */
write_coq_file(Size,PredSym,File) :-
 write('-- File bet_endoline.pl'), nl,
 write('Size: '), write(Size), nl,
 write('Predicate: '), write(PredSym), nl,
 write('Output file: '), write(File), nl,
 write_coq_open_close_file(Size,PredSym,File).
 
/* 2.5. Main predicate for BET. */
:- write_coq_file(4,line_endo,'../../coq/val_endoline.v'), halt.

