graphe png genere dans meme fichier que les .v

lib/ast.ml

@@ -329,7 +329,7 @@ let graph_from_edges (el : edge list)=
     @param g [G.t]
     @param name [string] png file name 
     @return[unit]*)
-let png_from_graph g name=
+let png_from_graph g name dir =
   let graph = G.fold_vertex (fun v acc ->
     let succs = List.map string_of_expression (G.succ g v)in
     let v' = string_of_expression v in
@@ -338,10 +338,10 @@ let png_from_graph g name=
       acc ^ "\"" ^ v' ^ "\";\n" ^ edges
     ) g "" in
   let dot = "digraph G {\nrankdir=LR;\nranksep=1;\n" ^ graph ^"\nsplines=true;\noverlap=false; "^"}" in
-  let oc = open_out ("./generate/"^name^"_measure.dot") in
+  let oc = open_out (dir^"/"^name^"_measure.dot") in
   Printf.fprintf oc "%s\n" dot;
   close_out oc;
-  ignore (Sys.command ("dot -Tpng ./generate/"^name^"_measure.dot -o ./generate/"^ name^"_measure.png"))
+  ignore (Sys.command ("dot -Tpng ./generate/"^name^"_measure.dot -o "^dir^"/"^ name^"_measure.png"))
 
 (**[assign_heigth g] returns the phase, phase weight association list. The phase weight is deduced from the order
                      topology of the phase
@@ -448,7 +448,7 @@ let string_of_expr_list expr_list =
 
 (**[png_from_graph2 g ] renvoie l'image au format png du graphe [g] 
     @param g de type [G2.t] graphe de liste de liste d'expression, composants fortement connexe *)  
-let png_from_graph2 (g:G2.t) (name : string) :unit =
+let png_from_graph2 (g:G2.t) (name : string) (dir : string) :unit =
   let graph = G2.fold_vertex (fun v acc ->
     let succs = List.map string_of_expr_list (G2.succ g v)in
     let v' = string_of_expr_list v in
@@ -457,10 +457,10 @@ let png_from_graph2 (g:G2.t) (name : string) :unit =
       acc ^ "\"" ^ v' ^ "\";\n" ^ edges
     ) g "" in
   let dot = "digraph G {\nrankdir=LR;\nranksep=1;\n" ^ graph ^"\nsplines=true;\noverlap=false; "^"}" in
-  let oc = open_out ("./generate/"^name^"_measure.dot") in
+  let oc = open_out (dir^"/"^name^"_measure.dot") in
   Printf.fprintf oc "%s\n" dot;
   close_out oc;
-  ignore (Sys.command ("dot -Tpng ./generate/"^name^"_measure.dot -o ./generate/"^ name^"_measure.png"))
+  ignore (Sys.command ("dot -Tpng ./generate/"^name^"_measure.dot -o "^dir^"/"^ name^"_measure.png"))
   
 
 (** [scc_graph g]  retourne le graphe G2.t correspondant au graphe de composants fortement connexe du graphe [g]

lib/gencoq.ml

@@ -514,7 +514,7 @@ let write_coq_file (gen: stmt list) (filename : string) =
   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
@@ -524,7 +524,7 @@ let generate_coq (Description(d,r,Measure g) : description) (name : string)=
   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_graph g name ;
       Ast.png_from_graph2 (Ast.scc_graph g;) (name^"_scc_graph");
       let file_exists =
       Sys.file_exists ("./generate/"^name^".v") in
@@ -540,7 +540,7 @@ let generate_coq (Description(d,r,Measure g) : description) (name : string)=
 
   else 
      () 
-
+*)
 (**[generate_filename base n dir] 
     @param base : string, base file name
     @param  n : integer, number of file iterations
@@ -566,8 +566,8 @@ let generate_coq_2files (Description(d,r,Measure g) : description) (name : strin
       let gdp_type, gdp_proof = generate_definition_phase g in
       let name_gen =  if overwrite then type_name else  generate_filename type_name 1 dir in 
       if gen_graph then begin
-        Ast.png_from_graph g name_gen;
-        Ast.png_from_graph2 (Ast.scc_graph g) (name_gen^"_scc_graph");
+        Ast.png_from_graph g name_gen dir;
+        Ast.png_from_graph2 (Ast.scc_graph g) (name_gen^"_scc_graph") dir;
       end;
 
       let module_world_type = (generate_requires d)@Module("World",(generate_instances d)@newline::generate_robogram r d)