From c17d18840bc269f5fe9502c8916df6bb9f689b8a Mon Sep 17 00:00:00 2001
From: Kylian Fontaine <kylian.fontaine@etu.univ-lyon1.fr>
Date: Mon, 22 Jul 2024 14:25:45 +0200
Subject: [PATCH] graphe png genere dans meme fichier que les .v
---
lib/ast.ml | 12 ++++++------
lib/gencoq.ml | 10 +++++-----
2 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/lib/ast.ml b/lib/ast.ml
index 0f6eea8..55a5ca2 100644
--- a/lib/ast.ml
+++ b/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]
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index a6e76a0..c1ffcf9 100644
--- a/lib/gencoq.ml
+++ b/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)
--
GitLab