/*******************************************************************************/
/* Coq Unit Testing project                                                    */
/* Copyright 2015-2018 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/bet_endofun.pl.

   Contents: Validation of examples/coq/endofun.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. */

/* 2.1. Test suites. */

/* Test suite 1: Validation of the Coq function is_endob. */
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_endob '),
 write(Size),
 write(' (list2fun ('), write_list(L), write('))).'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_1(_,_).

/* Test suite 2: Validation of the Coq predicate is_endo 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_endo '),
 write(Size),
 write(' (list2fun ('), write_list(L), write(')).'), nl,
 write('unfold list2fun. unfold is_endo. intros x H.'), nl,
 write('assert ('), 
 SizeM1 is Size-1,
 write_coq_nat('x',SizeM1), write(') as C. omega.'), nl,
 write('decompose [or] C; try (subst); simpl; omega. Qed.'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_2(_,_).

/* Test suite 3: Validation of is_endo with a reflexive proof. */
write_coq_is_endo_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_endo '),
 write(Size),
 write(' (list2fun ('), write_list(L), write(')).'), nl,
 write('apply is_endo_dec. simpl. auto. Qed.'), nl,
 nl, flush_output,
 fail. % this causes backtracking
write_coq_is_endo_refl(_,_).

/* Test suite 4: Validation that insertion preserves endofunctions. 
   Model: 
   Eval compute in (is_endob 4 (insert_fun 3 (list2fun (2::2::0::nil)) 1)). */
write_coq_insert_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(I,0,Size),
 write('Eval compute in (is_endob '),
 SizeP1 is Size + 1,
 write(SizeP1),
 write(' (insert_fun '),
 write(Size),
 write(' (list2fun ('), write_list(L), write(')) '),
 write(I),
 write(')).'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_insert_endo(_,_).

/* Test suite 5: Validation that direct sum preserves endofunctions. 
   Model: 
   Eval compute in (is_endob 5 (sum_fun 
    3 (list2fun (2::2::0::nil))
    2 (list2fun (0::1::nil))
   )). */
write_coq_sum_endo(PredSym,SizeMax)  :-
 increasing(Size,0,SizeMax),
 increasing(Size1,0,Size),
 Size2 is Size - Size1,
 (settings(fd_on) -> SizeT1=Size1; nat2term(Size1,SizeT1)),
 Pred1=..[PredSym,L1,SizeT1],  /* Generator of the first list L1 */
 (settings(fd_on) -> SizeT2=Size2; nat2term(Size2,SizeT2)),
 Pred2=..[PredSym,L2,SizeT2],  /* Generator of the second list L2 */
 Pred1,
 Pred2, 
 write('Eval compute in (is_endob '),
 write(Size),
 write(' (sum_fun '),
 write(Size1),
 write(' (list2fun ('), write_list(L1), write(')) '),
 write(Size2),
 write(' (list2fun ('), write_list(L2), write(')) '),
 write(')).'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_sum_endo(_,_).

/* 2.2. One predicate for all the validations of Coq concerning endofunctions. */
write_coq_endofun(PredSym,SizeMax) :-
 write('(* Test suite 1: Validation of is_endob. *)'), nl,
 write_coq_1(PredSym,SizeMax), nl, nl,
 write('(* Test suite 2: Validation of is_endo with a non-reflexive proof. *)'), nl,
 write_coq_2(PredSym,SizeMax), nl, nl,
 write('(* Test suite 3: Validation of is_endo with a reflexive proof. *)'), nl,
 write_coq_is_endo_refl(PredSym,SizeMax), nl, nl,
 write('(* Test suite 4: Validation that insertion preserves endofunctions (lemma insert_endo). *)'), nl,
 write_coq_insert_endo(PredSym,SizeMax), nl, nl,
 write('(* Test suite 5: Validation that direct sum preserves endofunctions (lemma sum_endo). *)'), nl,
 write_coq_sum_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 prolog/endofun.pl. *)'), nl,
  write('Require Import Arith Arith.Bool_nat Omega List.'), nl,
  write('Require Import endofun 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_endofun(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 endofun.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_endofun.v'), halt.

