premiere esquisse avec les modules

lib/coq.ml

@@ -9,6 +9,8 @@ type stmt =
   | VarMaxImplicit of string * Formula.t
   | Hyp of string * Formula.t
   | Lemma of string * Formula.t * stmt list (* tactics *)
+  | Parameter of string * Formula.t *Formula.t (* Module *)
+  | Parameterlem of string * Formula.t  (* Module *)
   | InstanceLemma of string * Formula.t * stmt list (* tactics *)
   | Def of string * Formula.t * Formula.t
   | Notation of string * Formula.t
@@ -17,6 +19,9 @@ type stmt =
   | Instance of string * Formula.t * Formula.t
   | ExistingInstance of Formula.t
   | Section of string * stmt list
+  | Module of string * stmt list
+  | ModuleType of string * stmt list
+  |ModuleImpType  of string * string * stmt list
   | Proof of stmt list
   | Require of bool * string list (* bool = Import *)
   | Import of string list
@@ -41,6 +46,10 @@ let rec pretty fmt st =
   | Lemma(s,f,lst) ->
      p fmt "@[<v 0>@[<hov 2>Lemma %s: %a.@]@,@[<v 2>Proof.@,%a@]@,Qed.@]"
        s prtyf f (Pp.print_list Pp.brk pretty) lst
+  | Parameter(s,f,lst) -> p fmt "@[<hov 2>@[<hov 2>Parameter %s:@ %a@] ->@ %a.@]\n"
+    s prtyf f prtyf lst 
+  | Parameterlem(s,f) -> p fmt "@[<v 0>@[<hov 2>Parameter %s: %a.@]"
+      s prtyf f 
   | InstanceLemma(s,f,lst) ->
      p fmt "@[<v 0>@[<hov 2>Instance %s: %a.@]@,@[<v 2>Proof.@,%a@]@,Defined.@]"
        s prtyf f (Pp.print_list Pp.brk pretty) lst
@@ -56,6 +65,12 @@ let rec pretty fmt st =
   | 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.@]"
                          s (Pp.print_list Pp.cut pretty) lst s
+  | Module (s,lst) ->  p fmt "@[<v 0>@[<v 2>Module %s.@,%a@]@\nEnd %s.@]"
+  s (Pp.print_list Pp.cut pretty) lst s
+  | ModuleType (s,lst) ->  p fmt "@[<v 0>@[<v 2>Module Type %s_type.@,%a@]@\nEnd %s_type.@]"
+  s (Pp.print_list Pp.cut pretty) lst s
+  | ModuleImpType (s,st,lst) ->  p fmt "@[<v 0>@[<v 2>Module %s : %s.@,%a@]@\nEnd %s.@]"
+  s st (Pp.print_list Pp.cut pretty) lst s
   | Proof (lst) -> p fmt "@[<v 0>@[<v 2>Proof.@,%a@]@\nEnd.@]"
                      (Pp.print_list Pp.cut pretty) lst
   | Require (_,[]) -> ()

lib/gencoq.ml

@@ -367,21 +367,21 @@ match l with
   | h::tl -> Or(Cst(h),generate_or tl) 
   | _ -> Cst("")
 
-(**[generate_definition_phase g]returns the list of stmt to generate the coq code for the definition of the phases of the graph [g]*)
-let generate_definition_phase (g : G.t) : stmt list =
+(**[generate_definition_phase g]returns the list of stmt to generate the coq code for the definition in module type of the phases of the graph [g] and the list of stmt to generate the def in module proof*)
+let generate_definition_phase (g : G.t) : (stmt list * stmt list) =
   Topological.fold (fun v acc -> 
-    let func_name = string_of_expression v ^" (config : configuration)" in 
-    RawCoq(["Definition "^func_name^":= (* To_Complete *)."])::acc
-    ) g []
+    let func_name = string_of_expression v  in 
+    (RawCoq(["Parameter "^func_name^": configuration -> 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 measurement functions for each phase
     @param g [G.t]
     @return [stmt list]*)
-let generate_measure_per_phase (g: Ast.G.t) : 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 (config : configuration)" in 
-      Def(func_name,Raw("nat"),Raw("(* To_Complete *)"))::acc
-      ) g []
+      let func_name = string_of_expression v ^"_meas" in 
+      (RawCoq(["Parameter "^func_name^": configuration -> nat."])::(fst acc),Def(func_name^"(config : configuration)",Raw("nat"),Raw("(* To_Complete *)"))::(snd acc))
+      ) g ([],[])
       
 
 (**[generate_lemmas g] returns the list of stmt corresponding to the lemmas extracted from the graph g
@@ -394,67 +394,152 @@ let generate_lemmas (g : Ast.G.t) : (stmt list * string list) =
     if succs <> [] then
       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
-      (Lemma(string_v^"_next_"^String.concat "_or_" string_succs ^" da",
-            Forall("config",InfixOp(Raw(string_v^" config = true"),"->",(generate_or rcs) )),[Comment("TODO")])::acc,
+      (Parameterlem(string_v^"_next_"^String.concat "_or_" string_succs ,
+            Forall("config da",InfixOp(Raw(string_v^" config = true"),"->",(generate_or rcs) )))::acc,
       ("("^string_v ^" config)")::s)
     else
       (acc,s)
     ) g ([],[])
 
+    let generate_lemmas_proof (g : Ast.G.t) : (stmt list * string list)  =
+      Topological.fold (fun v (acc,s) ->
+      let string_v = string_of_expression v in
+      let succs = Ast.G.succ g v in
+      if succs <> [] then
+        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
+       ( Lemma(string_v^"_next_"^String.concat "_or_" string_succs ,
+              Forall("config da",InfixOp(Raw(string_v^" config = true"),"->",(generate_or rcs))), proof_to_complete)::acc,
+              ("("^string_v ^" config)")::s)
+      else
+        (acc,s)
+      ) g ([],[])
+
 (**[generate_if_measure] generates the body of the measure function 
     @param g [G.t]
     @return [Formula.t]*)
 let generate_if_measure (g: Ast.G.t) : Formula.t  =
 let rec aux l = 
   match l with
-  |(phase,height)::[] -> Formula.Cst("("^ string_of_int height^", "^string_of_expression phase ^"_meas config)")
-  |(phase,height)::tl -> If(Cst(string_of_expression phase ^" config"),Cst("("^ string_of_int height^", "^string_of_expression phase ^"_meas config)"),aux tl )
+  |(phase,height)::[] -> Formula.Cst("("^ string_of_int height^"%nat, "^string_of_expression phase ^"_meas config)")
+  |(phase,height)::tl -> If(Cst(string_of_expression phase ^" config"),Cst("("^ string_of_int height^"%nat, "^string_of_expression phase ^"_meas config)"),aux tl )
   | _ -> Cst("")
 in
   aux (Ast.assign_height g)
 
-(**[generate_measure m] returns the list of stmt corresponding to the generation of the measurement
+let generate_measure_def (g : G.t)(ret : string) =
+  let to_change = generate_if_measure g in
+  Def("measure (config : configuration)",Cst(ret),to_change)
+
+
+(**[generate_measure m] returns the list of stmt corresponding to the generation of the measure
     @param m [measure]
     @return [stmt list] *)
 
-let generate_measure (Measure(g): measure) (name_png : string) : stmt list = 
+let generate_measure_lemme (Measure(g): measure) (name_png : string) : stmt list = 
  let ret = "nat*nat" in
-  let to_change = generate_if_measure g in
+  let m = generate_measure_def g ret in 
   Ast.png_from_graph g name_png;
   Ast.png_from_graph2 (Ast.scc_graph g;) "scc_graph";
   let measure_per_phase = generate_measure_per_phase g in 
-  let lemsgen = let lems = generate_lemmas g in 
-    Comment("Definition of phase")::generate_definition_phase g
-    @Comment("Definition of measure per phase ")::measure_per_phase
-    @Lemma("InGraph",Forall("config",generate_or (snd lems)),[Comment("TODO")])
+  let lemsgen = 
+    let lems = generate_lemmas g in 
+    Comment("Definition of phase")::fst (generate_definition_phase g)
+    @Comment("Definition of measure per phase "):: fst measure_per_phase
+    @Parameterlem("InGraph",Forall("config",generate_or (List.map (fun x -> x ^" = true")(snd lems))))
     ::List.rev (fst lems) in 
     lemsgen@
-    Def("measure (config : configuration)",Cst(ret),to_change)::
-  RawCoq(["Instance measure_compat : Proper (equiv ==> Logic.eq) measure."])::proof_to_complete
+    m::
+  RawCoq(["Parameter measure_compat : Proper (equiv ==> Logic.eq) measure."])::[]
+
+let generate_lt_type = 
+    RawCoq(["Definition lt_config x y := Lexprod.lexprod lt lt (measure (x)) (measure (y))."])
+    :: Parameterlem("wf_lt_config",Cst("well_founded lt_config"))
+    :: Parameterlem("lt_config_compat",Cst ("Proper (equiv ==> equiv ==> iff) lt_config"))
+    :: Parameterlem("round_lt_config" , Cst("forall config,
+    moving robogram da config <> nil ->
+    lt_config (round robogram da config) config")) ::[]
+
 
 let generate_lt = 
-    RawCoq(["Definition lt_config x y := Lexprod.lexprod lt lt (measure (!! x)) (measure (!! y))."])
-    :: Lemma("wf_lt_config",Cst("well_founded lt_config"),[Comment("TODO")])
-    :: RawCoq(["Instance lt_config_compat : Proper (equiv ==> equiv ==> iff) lt_config."])
-    ::proof_to_complete
-    @ RawCoq(["Theorem round_lt_config : forall config,
-    moving robogram da config <> nil ->
-    lt_config (round robogram da config) config."]) ::[]
+   RawCoq(["Definition lt_config x y := Lexprod.lexprod lt lt (measure (x)) (measure (y))."])
+   :: Lemma("wf_lt_config",Cst("well_founded lt_config"),[Comment("TODO")])
+   :: Lemma("lt_config_compat",Cst ("Proper (equiv ==> equiv ==> iff) lt_config"),[Comment("TODO")])
+   :: Lemma("round_lt_config" , Cst("forall config,
+   moving robogram da config <> nil ->
+   lt_config (round robogram da config) config"),[Comment("TODO")]) ::[]
+ let generate_module_type (m : measure) (s:string) =
+   newline
+   ::ModuleType(s,RawCoq(["Import World."])::Parameterlem("da",Cst("demonic_action"))::generate_measure_lemme m s
+   @newline::generate_lt_type)::[]
+
+  let generate_module_proof (Measure g : measure)(s:string) =
+    let lems = generate_lemmas_proof g in 
+    ModuleImpType(s^"_proof",s^"_type", RawCoq(["Import World.";"Variable da : demonic_action."])::snd(generate_definition_phase g)@snd (generate_measure_per_phase g)
+
+    @Lemma("InGraph",Forall("config",generate_or (List.map (fun x -> x ^" = true")(snd lems))),proof_to_complete)::List.rev (fst lems)@(generate_measure_def g "nat*nat")::generate_lt)
+
+
+    let keyword = "  End test_type." 
+
+    let read_and_save_after_keyword filename keyword =
+     
+      let in_channel = open_in filename in
+      let rec loop lines =
+        try
+          let line = input_line in_channel in
+          loop (line :: lines)
+        with End_of_file ->
+          close_in in_channel;
+          List.rev lines
+      in
+      let lines = loop [] in
+      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
+      in
+      String.concat "\n" (find_keyword lines)
+
 
 (**[generate_coq d s] generated from the complete description (world, robogram, measure) [d] the named coq instance [s]
     @param description of
     @param string s
     @return[unit] *)
 let generate_coq (Description(d,r,m) : description) (section_name : string)=
+  
+  let file_exists =
+  Sys.file_exists ("./generate/"^section_name^".v") in
+
+  let proof = if file_exists then RawCoq([read_and_save_after_keyword  ("./generate/"^section_name^".v") keyword ])
+
+  else generate_module_proof m section_name 
+  in
+  print_endline (read_and_save_after_keyword  ("./generate/"^section_name^".v") keyword) ;
+
   if Ast.check_description (Description(d,r,m)) 
    then
     let file_out = open_out ("./generate/"^section_name^".v") in 
     let format_file = Format.formatter_of_out_channel file_out in
-    let section = Section(section_name,(generate_instances d)@newline::generate_robogram r d
-                                                             @newline::generate_measure m section_name
-                                                             @newline::generate_lt) in
-    Format.fprintf format_file "%a@." Coq.pretty_l ((generate_requires d)@[section]);
+    let module_world_type = Module("World",(generate_instances d)@newline::generate_robogram r d)::
+                                                             generate_module_type m section_name in
+
+    
+   
+    Format.fprintf format_file "%a@." Coq.pretty_l ((generate_requires d)@module_world_type@[proof]);
+
     close_out file_out;
-    print_endline(section_name^".v is generated")
+print_endline(section_name^".v is generated")
   else 
-    ()
\ No newline at end of file
+    () 
+
+    
+
+
+
+