From 74713d950afea3aea35433450081119f78f37c73 Mon Sep 17 00:00:00 2001 From: Kylian Fontaine <kylian.fontaine@etu.univ-lyon1.fr> Date: Fri, 19 Jul 2024 10:55:47 +0200 Subject: [PATCH] generation de deux fichiers distincts --- bin/main.ml | 4 +++- lib/gencoq.ml | 50 +++++++++++++++++++++++++++++++++++++++++--------- 2 files changed, 44 insertions(+), 10 deletions(-) diff --git a/bin/main.ml b/bin/main.ml index 7cbc768..bdd27e0 100644 --- a/bin/main.ml +++ b/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);; diff --git a/lib/gencoq.ml b/lib/gencoq.ml index bca01f9..92253e7 100644 --- a/lib/gencoq.ml +++ b/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 + () -- GitLab