/*******************************************************************************/
/* Coq Unit Testing project                                                    */
/* Copyright 2017 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 : bet_rom.pl

   Contents: Validation of rom.pl by counting. */

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

:- compile(rom). /* Specification of ROM terms. */

:- write('Validation of romterm by counting:'), nl, iterate(0,7,romterm), halt.
% 1,2,10,74,706,8162,110410,1708394.
% Is https://oeis.org/A000698 but the first number.

write_coq_enum_rom(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_permutb '),
 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_enum_rom(_,_).



/* One predicate for all the validations. */
write_coq_rom(PredSym,SizeMax) :-
 write('(* Test suite 1: Enumeration of small maps. *)'), nl,
 write_coq_enum_rom(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 ../rom/prolog/bet_rom.pl. *)'), nl,
  write('Require Import Arith Arith.Bool_nat Omega List.'), nl,
  write('Require Import endofun permut cut revsubex rom.'), nl, nl, 
  ((system_type(sicstus);system_type(swi)) -> statistics(runtime,[T1,_]) ; true),
  ((system_type(gnu)) -> statistics(user_time,[T1,_]) ; true),
  write_coq_rom(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_rom.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,romterm,'../../coq/val_rom.v'), halt.
