diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 6d604f1ea4b25d3b3c1e196443c1ad595338c4d9..ea273af82e45eff480f67b150579dbd59b476b8a 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -374,7 +374,7 @@ match l with
let generate_definition_phase (g : G.t) : (stmt list * stmt list) =
Topological.fold (fun v acc ->
let func_name = string_of_expression v in
- (Parameter(func_name,Cst "configuration",Cst"bool")::(fst acc), Def(func_name^"(config: configuration)",Cst("bool"),Cst("(* TODO *)"))::(snd acc))
+ (Parameter(func_name,Cst "configuration",Cst"bool")::(fst acc), Def(func_name^" (config: configuration)",Cst("bool"),Cst("(* TODO *)"))::(snd acc))
) g ([],[])
(**[generate_measure_per_phase g] returns the list of stmt generating the coq code of the measurnatement functions for each phase
@@ -384,7 +384,7 @@ let generate_definition_phase (g : G.t) : (stmt list * stmt list) =
let generate_measure_per_phase (g: Ast.G.t) : (stmt list * stmt list) =
Topological.fold (fun v acc ->
let func_name = string_of_expression v ^"_meas" in
- (Parameter(func_name,Cst "configuration",Cst "nat")::(fst acc),Def(func_name^"(config : configuration)",Cst("nat"),Cst("(* TODO *)"))::(snd acc))
+ (Parameter(func_name,Cst "configuration",Cst "nat")::(fst acc),Def(func_name^" (config : configuration)",Cst("nat"),Cst("(* TODO *)"))::(snd acc))
) g ([],[])
@@ -401,7 +401,7 @@ let generate_lemmas (g : Ast.G.t) (t : string *Formula.t * stmt list ->stmt): (
let string_succs = (List.map string_of_expression succs) in
let rcs = List.map (fun x -> x ^ " (round robogram da config) = true") string_succs in
(t (string_v^"_next_"^String.concat "_or_" string_succs,
- Forall("config da",InfixOp(Raw(string_v^" config = true"),"->",(generate_or rcs))),
+ Forall("config",InfixOp(Raw(string_v^" config = true"),"->",(generate_or rcs))),
[Comment("TODO")])::acc,
("("^string_v ^" config)")::s)
else
@@ -423,17 +423,18 @@ let generate_if_measure (g: Ast.G.t) : Formula.t =
(**[generate_measure_def g] generates the definition of the measure.
@param g [G.t]
- @return [stmt]
-*)
+ @return [stmt]*)
let generate_measure_def (g : G.t)(ret : string) =
let body = generate_if_measure g in
Def("measure (config : configuration)",Cst(ret),body)
-(**[generate_measure_all m] returns the list of stmt corresponding to the generation of the measure
+(**[generate_measure_all m t gmpp gdp] returns the list of stmt corresponding to the generation of the measure
@param m [measure]
+ @param t function for module type or module proof
+ @param gmpp [stmt list] corresponds to the generation of the measure per phase
+ @param gdp [stmt list] corresponds to the generation of the phase definition
@return [stmt list] *)
-
let generate_measure_all (Measure(g): measure)(t : string * Formula.t * stmt list -> stmt)(gmpp : stmt list) (gdp : stmt list ): stmt list =
let ret = "nat*nat" in
let m = generate_measure_def g ret in
@@ -448,7 +449,11 @@ let generate_measure_all (Measure(g): measure)(t : string * Formula.t * stmt lis
t("measure_compat",Cst "Proper (equiv ==> Logic.eq) measure",[Comment("TODO")])::[]
-let generate_lt (t:string * Formula.t * stmt list -> stmt) =
+(**[generate_lt t] returns the list of stmts corresponding to the generation of lt_config, wf_lt_config, lt_config_compat, and round_lt_config
+ @param t function for module type or module proof
+ @return [stmt list]
+*)
+let generate_lt (t:string * Formula.t * stmt list -> stmt) : stmt list =
RawCoq(["Definition lt_config x y := Lexprod.lexprod lt lt (measure (x)) (measure (y))."])
:: t("wf_lt_config",Cst("well_founded lt_config"),[Comment("TODO")])
:: t("lt_config_compat",Cst ("Proper (equiv ==> equiv ==> iff) lt_config"),[Comment("TODO")])
@@ -456,11 +461,14 @@ let generate_lt (t:string * Formula.t * stmt list -> stmt) =
moving robogram da config <> nil ->
lt_config (round robogram da config) config"),[Comment("TODO")]) ::[]
+
+
let generate_module_type (m : measure) (s:string) (gmpp:stmt list) (gdp: stmt list) =
newline
::ModuleType(s,RawCoq(["Import World."])::Parameterlem("da",Cst("demonic_action"),[Comment("")] )::generate_measure_all m (fun (a,b,c) -> Parameterlem(a, b, c)) gmpp gdp
@newline::generate_lt (fun (a,b,c) -> Parameterlem(a, b, c)))::[]
+
let generate_module_proof (m: measure)(s:string) (gmpp:stmt list) (gdp : stmt list) =
ModuleImpType(s^"_proof",s^"_type", RawCoq(["Import World.";"Variable da : demonic_action."])::generate_measure_all m (fun (a,b,c) -> Lemma(a, b, c)) gmpp gdp
@@ -487,12 +495,8 @@ let generate_lt (t:string * Formula.t * stmt list -> stmt) =
let rec find_keyword lines =
match lines with
| [] -> []
- | line :: rest ->
- try
- ignore (Str.search_forward (Str.regexp keyword) line 0);
- rest
- with Not_found ->
- find_keyword rest
+ | line :: rest -> try ignore (Str.search_forward (Str.regexp keyword) line 0); rest
+ with Not_found -> find_keyword rest
in
String.concat "\n" (find_keyword lines)
@@ -515,13 +519,14 @@ 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 file_out = open_out ("./generate/"^name^".v") in
- let format_file = Format.formatter_of_out_channel file_out in
let module_world_type = 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")
+
else
()