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

   Contents: 
   1. Validation of permut.pl by counting 
   2. Validation of examples/coq/permut.v by bounded-exhaustive testing (BET). */

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

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

/* 1. Validation by counting. */

:- write('Validation of line by counting:'), nl, iterate(0,6,line).
% 1,1,2,6,24,120,720, factorials.

/* 2. Validations by BET. */

/* Validation of is_permut with a non-reflexive proof.

   Model:

   Goal is_permut 3 (list2fun (1::2::0::nil)). unfold is_permut. unfold list2fun. 
   split.
   - unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2). omega.
     firstorder; rewrite H; simpl; omega.
   - unfold is_inj. intros x y Hx Hy Hxy. assert (x = 0 \/ x = 1 \/ x = 2). omega.
     assert (y = 0 \/ y = 1 \/ y = 2). omega.
     firstorder; rewrite H; rewrite H0; simpl; omega. Qed. */
write_coq_is_permut_non_refl(PredSym,SizeMax) :-
 increasing(Size,1,SizeMax),
 (settings(fd_on) -> SizeT=Size; nat2term(Size,SizeT)),
 Pred=..[PredSym,L,SizeT],  /* Pred is the generator */
 Pred, 
 SizeM1 is Size-1,
 write('Goal is_permut '),
 write(Size),
 write(' (list2fun ('), write_list(L), write(')). unfold is_permut.'), 
 write(' unfold list2fun. split.'), nl,
 write('- unfold is_endo. intros x Hx. '),
 write('assert ('), write_coq_nat('x',SizeM1), write(').'), nl,
 write(' omega. firstorder; subst; simpl; omega.'), nl,
 write('- unfold is_inj. intros x y Hx Hy Hxy.'), nl,
 write('assert ('), write_coq_nat('x',SizeM1), write('). omega. '), nl,
 write('assert ('), write_coq_nat('y',SizeM1), write('). omega. '), nl,
 write('firstorder; subst; simpl; omega. Qed.'),
 nl, flush_output,
 fail. % this causes backtracking
write_coq_is_permut_non_refl(_,_).


/* One predicate for all the validations of Coq concerning permutations. */
write_coq_permut(PredSym,SizeMax) :-
 write('(* Validation of is_permut with a non-reflexive proof. *)'), nl,
 write_coq_is_permut_non_refl(PredSym,SizeMax), nl, 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 ../permutation/prolog/bet_permut_non_refl.pl. *)'), nl,
  write('Require Import Arith Arith.Bool_nat Omega List.'), nl,
  write('Require Import endofun permut cut.'), nl, nl, 
  write('Definition is_permutb n f := andb (is_endob n f) (is_injb n f).'), nl, nl,
  ((system_type(sicstus);system_type(swi)) -> statistics(runtime,[T1,_]) ; true),
  ((system_type(gnu)) -> statistics(user_time,[T1,_]) ; true),
  write_coq_permut(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 permut.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_permut_non_refl.v'), halt.
