diff --git a/lib/coq.ml b/lib/coq.ml
index 24d7972ad97d886d44648ad2b38dc5703d9ffd8e..1ad71548977996be896fe4669c070a6ace4b284d 100644
--- a/lib/coq.ml
+++ b/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 (_,[]) -> ()
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 3c2a4b11b5ef97570df064cca815aba5641b958c..766eef7c2056aeda8cdad31752d4b8b80c0b06f2 100644
--- a/lib/gencoq.ml
+++ b/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
+ ()
+
+
+
+
+
+