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

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

/* Validations by counting of the property is_transitive_funb defined 
   in trans.v, through the function 
    
    Definition is_transitive_listb n l := is_transitive_funb n (list2fun l). 
    
   added at the beginning of the test file. Model:
   
   Eval compute in (length (filter (is_transitive_listb 2) (
    (1::0::nil)::
    (0::1::nil)::
    nil))). */

write_coq_is_transitive_funb_size(PredSym,Size)  :-
 (settings(fd_on) -> SizeT=Size; nat2term(Size,SizeT)),
 Pred=..[PredSym,L,SizeT],  /* Pred is the generator */
 write('Eval compute in (length (filter (is_transitive_listb '),
 write(Size), write(') ('), nl,
 Pred, 
 write(' ('), write_list(L), write(')::'), nl,
 fail. % this causes backtracking 
write_coq_is_transitive_funb_size(_,_) :- 
 write(' nil))).'), nl, 
 flush_output.

write_coq_is_transitive_funb(PredSym,SizeMax)  :-
 increasing(E,0,SizeMax),
 Size is E+E,  /* The size is the number of darts. */
 write_coq_is_transitive_funb_size(PredSym,Size), fail.
write_coq_is_transitive_funb(_,_).

/* One predicate for all the validations. */
write_coq_trans(PredSym,SizeMax) :-
 write('Eval compute in "Validation of is_transitive_funb by counting.".'), nl,
 write_coq_is_transitive_funb(PredSym,SizeMax), nl, nl.


/* 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_trans.pl. *)'), nl,
  write('Require Import Arith Arith.Bool_nat Omega String.'), nl,
  write('Require Import endofun permut trans cut.'), nl, nl, 
  write('Open Scope string_scope.'), nl, nl,  
  write('Require Import List.'), nl, nl,
  write('Set Implicit Arguments.'), nl, nl,
  write('Definition is_transitive_listb n l := is_transitive_funb n (list2fun l).'), nl, nl, 
  ((system_type(sicstus);system_type(swi)) -> statistics(runtime,[T1,_]) ; true),
  ((system_type(gnu)) -> statistics(user_time,[T1,_]) ; true),
  write_coq_trans(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_trans.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).

/* Maximal value: 3. With size 4 the compilation 
    coqc val_trans.v
   generates a core dump. */
:- write_coq_file(3,line,'../../coq/val_trans.v'), halt.
