Fix fichier original effacé si erreur

lib/gencoq.ml

@@ -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 
      ()