diff --git a/bin/main.ml b/bin/main.ml
index bdd27e0c2e98a93c11692c54d41eed9c56d6b378..dc353713b56f142e4ab91fb72231a26b5c113c1f 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -3,10 +3,31 @@ open Dsl
let files =Array.to_list (Sys.readdir repo);;
print_endline(String.concat "; " files);;
*)
+(*
+let rec generate_filename base n =
+ let name = base ^ string_of_int n in
+ if Sys.file_exists name then generate_filename base (n+1) else name
+*)
+
-let gen (x : string) =
+
+let gen (args : string array) =
(* Gencoq.generate_coq (Interface.parse_description x) (Filename.basename x);; *)
+ let list_args = Array.to_list args in
+ let rec parse_args args (proof_name : string) (type_name : string) (overwrite: bool) (repo_gen : string) :(string * string * bool * string)=
+ match args with
+ | "-proof" :: proof :: tl -> parse_args tl proof type_name overwrite repo_gen
+ | "-type" :: type_ :: tl -> parse_args tl proof_name type_ overwrite repo_gen
+ | "-n" :: tl -> parse_args tl proof_name type_name (not overwrite) repo_gen
+ | "-r" :: repo :: tl -> parse_args tl proof_name type_name overwrite repo
+ | "-h" :: _ -> print_endline " Usage: dsl filename_dsl [-proof filename_proof] [-type filename_type] [-r repository_out] [-n] [-h] \n -n : don't overwrite type file"; exit 0
+ | _ :: tl ->parse_args tl proof_name type_name overwrite repo_gen
+ | [] -> (proof_name, type_name, overwrite,repo_gen)
+
+ in
+ let name = args.(1) in
+ let (proof_name, type_name, overwrite,repo_gen) = parse_args list_args ((Filename.basename name)^"_proof") ((Filename.basename name)^"_world_type") true "./generate" in
- Gencoq.generate_coq_2files (Interface.parse_description x) (Filename.basename x);;
+ Gencoq.generate_coq_2files (Interface.parse_description name) (Filename.basename name) proof_name type_name overwrite repo_gen;;
-gen Sys.argv.(1);;
+gen Sys.argv;;
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 92253e7c3034ba5ed8f580d63ee90f7d27536427..1a9dd8cd8ab2aa7743a7160866ee2a7ad1fd3f7f 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -542,28 +542,36 @@ let generate_coq (Description(d,r,Measure g) : description) (name : string)=
()
+ let rec generate_filename base n repo=
+ print_endline (base);
+ let name = base ^ string_of_int n in
+ if (Sys.file_exists (repo^"/"^base^".v")) then
+ (if (Sys.file_exists (repo^"/"^name^".v")) then generate_filename base (n+1) repo else name)
+ else base
+
+
(**[generate_coq d s]generates 2 coq files
1 containing the world description module, the type module -> regenerate all the time
the other the proof module -> generate only the first time
@param description
@param string s
@return[unit] *)
-let generate_coq_2files (Description(d,r,Measure g) : description) (name : string)=
+let generate_coq_2files (Description(d,r,Measure g) : description) (name : string) (proof_name:string) (type_name : string) (ecrase : bool) (repo : string)=
if Ast.check_description (Description(d,r,Measure g))
then
let gmpptype, gmpp_proof = generate_measure_per_phase g in
let gdp_type, gdp_proof = generate_definition_phase g in
Ast.png_from_graph g name;
Ast.png_from_graph2 (Ast.scc_graph g;) (name^"_scc_graph");
-
+ let name_gen = if ecrase then type_name else generate_filename type_name 1 repo in
let module_world_type = (generate_requires d)@Module("World",(generate_instances d)@newline::generate_robogram r d)
:: generate_module_type (Measure g) name gmpptype gdp_type in
- write_coq_file module_world_type ("./generate/"^name^"_world_type.v");
- let file_exists =
- Sys.file_exists ("./generate/"^name^"_proof.v") in
- if not(file_exists) then
- write_coq_file ((generate_requires d)@Require(true,["Pactole.CaseStudies.Generate_test."^name^"_world_type"])::generate_module_proof (Measure g) name gmpp_proof gdp_proof) ("./generate/"^name^"_proof.v")
-
+ write_coq_file module_world_type (repo^"/"^name_gen^".v");
+ let file_proof_exists =
+ Sys.file_exists (repo^"/"^proof_name^".v") in
+ if not(file_proof_exists) then
+ write_coq_file ((generate_requires d)@Require(true,["Pactole.CaseStudies.Generate_test."^type_name])::generate_module_proof (Measure g) name gmpp_proof gdp_proof) (repo^"/"^proof_name^".v")
+
else
()