From 73e25248dea9880f51646ba41e09da38e32ef516 Mon Sep 17 00:00:00 2001
From: Kylian Fontaine <kylian.fontaine@etu.univ-lyon1.fr>
Date: Mon, 22 Jul 2024 10:46:40 +0200
Subject: [PATCH] commentaire + fix warning coq local/export instance module
---
bin/main.ml | 50 +++++++++++++++++++++++++++-----------------------
lib/coq.ml | 2 +-
lib/gencoq.ml | 50 ++++++++++++++++++++++++++++----------------------
lib/parser.mly | 6 +++---
4 files changed, 59 insertions(+), 49 deletions(-)
diff --git a/bin/main.ml b/bin/main.ml
index dc35371..d00cb91 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -1,33 +1,37 @@
open Dsl
-(*let repo = "./sourcegenerate";;
-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
+
+
+
+
+(** [parse_args argrs proof_name type_name owerwrite repo_gen] Parses the command line arguments and returns a tuple containing the parsed values or default value.
+ @param args string list: The list of command line arguments.
+ @param proof_name string: The name of the proof file.
+ @param type_name string: The name of the type file.
+ @param overwrite : A boolean indicating whether to overwrite the type file.
+ @param dir_gen string: The name of the output repository.
+ @return A tuple containing the parsed values or default value passed as an argument in thr first function's call: (proof_name, type_name, overwrite, repo_gen).
*)
+let rec parse_args args (proof_name : string) (type_name : string) (overwrite: bool) (dir_gen : string) (graph_gen:bool):(string * string * bool * string *bool)=
+ match args with
+ | "-proof" :: proof :: tl -> parse_args tl proof type_name overwrite dir_gen graph_gen
+ | "-type" :: type_ :: tl -> parse_args tl proof_name type_ overwrite dir_gen graph_gen
+ | "-n" :: tl -> parse_args tl proof_name type_name (not overwrite) dir_gen graph_gen
+ | "-r" :: dir :: tl -> parse_args tl proof_name type_name overwrite dir graph_gen
+ | "-g" :: tl -> parse_args tl proof_name type_name overwrite dir_gen (not graph_gen)
+ | "-h" :: _ -> print_endline "Usage: dsl filename_dsl [-proof filename_proof] [-type filename_type] [-r repository_out] [-n] [-g] [-h] \n -n : don't overwrite type file \n -g : generate png from graph"; exit 0
+ | _ :: tl ->parse_args tl proof_name type_name overwrite dir_gen graph_gen
+ | [] -> (proof_name, type_name, overwrite,dir_gen,graph_gen)
+
+(** [gen args] function that takes a string array [args] as input and generates Coq files based on the provided arguments.
+ @param args: string array, array of command line arguments
+ *)
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 name) (Filename.basename name) proof_name type_name overwrite repo_gen;;
+ let (proof_name, type_name, overwrite,repo_gen, graph_gen) = parse_args list_args ((Filename.basename name)^"_proof") ((Filename.basename name)^"_world_type") true "./generate" false in
+ Gencoq.generate_coq_2files (Interface.parse_description name) (Filename.basename name) proof_name type_name overwrite repo_gen graph_gen;;
gen Sys.argv;;
diff --git a/lib/coq.ml b/lib/coq.ml
index f8b1173..9067bb2 100644
--- a/lib/coq.ml
+++ b/lib/coq.ml
@@ -60,7 +60,7 @@ let rec pretty fmt st =
s prtyf ftyp prtyf struc prtyf f
| Fixpoint(s,ftyp,struc,f) -> p fmt "@[<hov 2>@[<hov 2>Fixpoint %s:@ %a@ { %a }@] :=@ %a.@]"
s prtyf ftyp prtyf struc prtyf f
- | Instance(s,ftyp,f) -> p fmt "@[<hov 2>@[<hov 2>Instance %s:@ %a@] :=@ %a.@]"
+ | Instance(s,ftyp,f) -> p fmt "@[<hov 2>@[<hov 2>#[export] Instance %s:@ %a@] :=@ %a.@]"
s prtyf ftyp prtyf f
| ExistingInstance(f) -> p fmt "@[<hov 2>@[<hov 2>Existing Instance %a.@]@]" prtyf f
| Section (s,lst) -> p fmt "@[<v 0>@[<v 2>Section %s.@,%a@]@\nEnd %s.@]"
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 1a9dd8c..a6e76a0 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -220,10 +220,10 @@ let instance_info (fl:field list) : stmt list =
let l'' = String.concat " | " l' in
RawCoq(["Inductive light:= "^l''^"."])
::Instance("light_Setoid",Cst "Setoid light",Cst "eq_setoid light")
- ::RawCoq(["Instance light_EqDec : EqDec light_Setoid.";
+ ::RawCoq(["[export] Instance light_EqDec : EqDec light_Setoid.";
"(*Proof*) Admitted.";
"Definition info := (location * light)%type."])
- ::RawCoq(["Instance St : State info := AddInfo light (OnlyLocation (fun f => sigT (fun sim : similarity location => Bijection.section sim == f)))."])::[]
+ ::Instance("St",Cst"State info",Raw("AddInfo light (OnlyLocation (fun f => sigT (fun sim : similarity location => Bijection.section sim == f)))."))::[]
(*TODO: Le reste des info sont a faire*)
| _ ->RawCoq(["Definition info := (location)%type."])
::Instance("St",Raw("State location"),Raw("OnlyLocation (fun _ => True)")) ::[])
@@ -235,7 +235,7 @@ let instance_info (fl:field list) : stmt list =
let instance_byzantine (x : int ) : stmt list =
if x < 1 then
Instance("MyRobots",Cst("Names"),App(Cst("Robots"),[Cst("n");Int 0]))
- ::RawCoq(["Instance NoByz : NoByzantine.";"Proof using . now split. Qed."])
+ ::RawCoq(["#[export] Instance NoByz : NoByzantine.";"Proof using . now split. Qed."])
::[]
else
Instance("MyRobots",Cst("Names"),App(Cst("Robots"),[Raw("("^string_of_int (x-1) ^ " * n)");Cst("n")]))
@@ -249,8 +249,8 @@ let instance_sync (s : synchro) : stmt list =
match s with
| Async -> [RawCoq(["Instance ic: Async not implemented
Instance InaFun : Async not implemented"])]
- | _ -> [RawCoq([ "Instance IC : inactive_choice unit := NoChoiceIna.";
- "Instance InaFun : inactive_function unit := NoChoiceInaFun."])]
+ | _ -> [Instance("IC",Cst"inactive_choice unit",Cst "NoChoiceIna");
+ Instance("InaFun",Cst "inactive_function unit",Cst "NoChoiceInaFun")]
(**[instance_sensors s] allows to instantiate the observation according to the list of sensors [s] Only takes the range and the multiplicity for the moment
@param s [sensor list] corresponding to the list of sensors in the description
@@ -349,7 +349,7 @@ let generate_robogram (r : expr list) (d: information list) : stmt list =
| h::_ -> let h' = if get_rigidity d = "Flexible" then Formula.Let("aux s",h,Raw("paths_in_"^get_space d^" (aux s)"))
else h in
Def ("robogram_pgm (s : observation)",Raw(valretcoq),h')
- ::RawCoq(["Instance robogram_pgm_compat : Proper (equiv ==> equiv) robogram_pgm."])
+ ::RawCoq(["#[export] Instance robogram_pgm_compat : Proper (equiv ==> equiv) robogram_pgm."])
::proof_to_complete
@Def("robogram",Raw("robogram"),Raw("{| pgm := robogram_pgm; pgm_compat := robogram_pgm_compat |}"))
::[]
@@ -541,36 +541,42 @@ 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
+ @param dir : string, file directory
+ @return string, the concatenation of the file name and its number to not overwrite existing files*)
+let rec generate_filename base n dir =
+ let name = base ^ string_of_int n in
+ if (Sys.file_exists (dir^"/"^base^".v")) then
+ (if (Sys.file_exists (dir^"/"^name^".v")) then generate_filename base (n+1) dir else name)
+ else base
- 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
+(**[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) (proof_name:string) (type_name : string) (ecrase : bool) (repo : string)=
+let generate_coq_2files (Description(d,r,Measure g) : description) (name : string) (proof_name:string) (type_name : string) (overwrite : bool) (dir : string) (gen_graph : bool)=
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 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");
+ end;
+
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 (repo^"/"^name_gen^".v");
+ write_coq_file module_world_type (dir^"/"^name_gen^".v");
let file_proof_exists =
- Sys.file_exists (repo^"/"^proof_name^".v") in
+ Sys.file_exists (dir^"/"^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")
+ write_coq_file ((generate_requires d)@Require(true,["Pactole.CaseStudies.Generate_test."^type_name])::generate_module_proof (Measure g) name gmpp_proof gdp_proof) (dir^"/"^proof_name^".v")
else
diff --git a/lib/parser.mly b/lib/parser.mly
index a271f5a..9a4ae99 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -217,7 +217,6 @@ robogram:
expression:
/*(e)*/
- | PARENOPEN e = expression PARENCLOSE {e}
| e = constant {e}
/*if e1 then e2 else e3*/
| IF e1 = expression THEN e2 = expression ELSE e3 = expression {Cond(e1,e2,e3)} %prec AFFECT
@@ -228,7 +227,7 @@ expression:
| LET v = VARIABLE AFFECT e = expression IN e2=expression {Let(v,e,e2)} %prec AFFECT
/*name_variable = e*/
| v = VARIABLE; AFFECT e = expression {Affectation(v,e)}
- /*[a;z;e;r;t....]*/
+ /*(a;...b;)*/
| PARENOPEN s = set PARENCLOSE {Set s}
| MATCH PARENOPEN i= appfunc PARENCLOSE WITH p = patternmatch END {PatternMatching(i,p)}
| MATCH i= id WITH p = patternmatch END {PatternMatching(i,p)}
@@ -263,10 +262,11 @@ id :
| VARIABLE {Var $1}
| x = KEYWORD POINT e = VARIABLE {Point(x,e,$startpos.Lexing.pos_lnum)}
+
set :
| e = expression COMMA s = set {Some(s,e)}
| e = expression {Some(Vide,e)}
- | e = KEYWORD COMMA s = set {Some(s,Var e)}
+ | e = KEYWORD COMMA s = set {Some(s,Var e)}
| e = KEYWORD {Some(Vide,Var e)}
| {Vide}
--
GitLab