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

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

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

:- compile('../../permutation/prolog/permut'). /* Specification of permutations. */

/* Validation of the executable versions of the lemmas of
   preservation of transitivity. */


/* Validation that the insert operation preserves transitivity.
   WARNING: Only tested with i <= n.

Defined in trans.v:

Lemma insert_transitive (n : nat) (f : nat -> nat) (i : nat) :
 is_transitive_fun n f -> 
  ((i < n -> is_transitive_fun (S n) (insert_fun n f i)) /\
  (odd n -> is_transitive_fun (S n) (insert_fun n f n))). 

Definition insert_transitiveb (n : nat) (f : nat -> nat) (i : nat) := 
 if (is_transitive_funb n f)
 then
  (andb
   (if (ltb i n) then (is_transitive_funb (S n) (insert_fun n f i)) else true) 
   (if (NPeano.odd n) then (is_transitive_funb (S n) (insert_fun n f n)) else true)
  )
 else true. */
write_coq_insert_trans(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 (if (@insert_transitiveb '),
 write(Size),
 write(' (list2fun ('), write_list(L), write(')) '),
 write(I),
 write(') then "" else "insert_transitiveb wrong for ('),
 write_list(L), write(')."'),
 write(').'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_insert_trans(_,_).


/* Validation that the non_isthmic operation preserves transitivity. */
write_coq_non_isthmic_trans(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 (let proof := '),
 write_coq_proof_X_leq_Y(I,Size),
 nl, 
 write(' in if (@non_isthmic_fun_transitiveb '),
 write(Size),
 write(' (list2fun ('), write_list(L), write(')) '),
 write(I),
 write(' '), 
 write('proof) then "" else "non_isthmic_fun_transitiveb wrong for ('),
 write_list(L), write(')."'),
 write(').'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_non_isthmic_trans(_,_).


/* Validation that the isthmic operation preserves transitivity. */
write_coq_isthmic_trans(PredSym,SizeMax) :-
 increasing(E,0,SizeMax),
 Em1 is E - 1,
 increasing(E1,0,Em1),
 E2 is Em1 - E1,
 Size1 is E1+E1,
 Size2 is E2+E2,
 (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 (if (isthmic_fun_transitiveb '),
 write(Size1),
 write(' (list2fun ('), write_list(L1), write(')) '),
 write(Size2),
 write(' (list2fun ('), write_list(L2), write('))) then "" else "isthmic_fun_transitive for ('),
 write_list(L1), write(') and ('),
 write_list(L2), write(')").'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_isthmic_trans(_,_).

/* Invalidation that the sum operation preserves transitivity, 
   with all the pairs of lists of even length whose length sum
   is 2*SizeMax or less. */
write_coq_sum_trans(PredSym,SizeMax) :-
 increasing(E,0,SizeMax),
 increasing(E1,0,E),
 E2 is E - E1,
 Size1 is E1+E1,
 Size2 is E2+E2,
 (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 (if (sum_transitiveb '),
 write(Size1),
 write(' (list2fun ('), write_list(L1), write(')) '),
 write(Size2),
 write(' (list2fun ('), write_list(L2), write('))) then "" else "Lemma sum_transitive wrong for ('),
 write_list(L1), write(') and ('),
 write_list(L2), write(')").'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_sum_trans(_,_).


/* One predicate for all the validations of Coq concerning transitivity. 
   WARNING: The invalidation that the sum operation preserves transitivity
   is performed with a smaller maximal size than the other tests (maximal
   sum of list lengths 4 instead of 8). */
write_coq_map(PredSym,SizeMax) :-
 write('Eval compute in "Test suite 1: Validation of the lemma about insertion and transitivity.".'), nl,
 write_coq_insert_trans(PredSym,SizeMax), nl, nl,
 write('Eval compute in "Test suite 2: Validation that the non_isthmic operation preserves transitivity.".'), nl,
 write_coq_non_isthmic_trans(PredSym,SizeMax), nl, nl, 
 write('Eval compute in "Test suite 3: Validation that the isthmic operation preserves transitivity.".'), nl,
 write_coq_isthmic_trans(PredSym,SizeMax), nl, nl,
 write('Eval compute in "Test suite 4: Invalidation that the sum operation preserves transitivity (invalid theorem sum_transitive).".'), nl,
 write_coq_sum_trans(PredSym,2).
 
 
/* 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 ../rotation/prolog/bet_map.pl. *)'), nl,
  write('Require Import Arith Arith.Bool_nat Omega String.'), nl,
  write('Require Import endofun permut trans map exec cut.'), nl, nl, 
  write('Open Scope string_scope.'), nl, nl,  
  write('Require Import List.'), nl, 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_map(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.

/* Some output before writing in the Coq file. */
write_coq_file(Size,PredSym,File) :-
 write('-- File bet_map.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).

:- write_coq_file(4,line,'../../coq/val_map.v').

:- halt.
