nommage de fichier et de repo + option pour ecraser ou non le fichier module type

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;;

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 
      ()