generation de deux fichiers distincts

bin/main.ml

@@ -5,6 +5,8 @@ print_endline(String.concat "; " files);;
 *)
 
 let gen (x : string) = 
-  Gencoq.generate_coq (Interface.parse_description x) (Filename.basename x);;
+(*  Gencoq.generate_coq (Interface.parse_description x) (Filename.basename x);; *)
+
+  Gencoq.generate_coq_2files (Interface.parse_description x) (Filename.basename x);;
 
 gen Sys.argv.(1);;

lib/gencoq.ml

@@ -501,7 +501,21 @@ let generate_lt (t:string * Formula.t * stmt list -> stmt) : stmt list =
       String.concat "\n" (find_keyword lines)
 
 
-(**[generate_coq d s] generated from the complete description (world, robogram, measure) [d] the named coq instance [s]
+
+(** [write_coq_file gen filename] writes the generated Coq code to the specified file.  
+  @param gen stmt list representing the generated Coq code.
+  @param filename The name of the file to write the generated code to.
+*)
+let write_coq_file (gen: stmt list) (filename : string) =
+  let file_out = open_out (filename) in
+  let format_file = Format.formatter_of_out_channel file_out in
+  Format.fprintf format_file "%a@." Coq.pretty_l (gen);
+  close_out file_out;
+  print_endline(filename^ " has been generated");;
+
+
+
+(**[generate_coq d s] generates the coq file containing the world description module, the type module and the proof module
     @param description of
     @param string s
     @return[unit] *)
@@ -519,19 +533,37 @@ let generate_coq (Description(d,r,Measure g) : description) (name : string)=
                       [RawCoq([read_and_save_after_keyword  ("./generate/"^name^".v") ("End "^name^"_type.")])]
                   else newline::generate_module_proof (Measure g) name gmpp_proof gdp_proof
       in
-      let module_world_type = Module("World",(generate_instances d)@newline::generate_robogram r d)
+      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
-      let file_out = open_out ("./generate/"^name^".v") in
-      let format_file = Format.formatter_of_out_channel file_out in
-      Format.fprintf format_file "%a@." Coq.pretty_l ((generate_requires d)@module_world_type@proof);
-      close_out file_out;
-      print_endline(name^".v is generated")
+      write_coq_file (module_world_type@proof) ("./generate/"^name^"world_type.v");
+
 
   else 
      () 
 
-    
-
 
+(**[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)=
+  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 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")
 
 
+  else 
+     ()