Select Git revision
gencoq.ml 25.14 KiB
open Ast
open Coq
let newline =RawCoq([" "])
let proof_to_complete = [Comment("Proof");RawCoq(["Admitted."])]
(** [get_nb_byz infos] returns the number of Byzantines desired
@param information list corresponding to the description of the world
@return[int]*)
let get_nb_byz (infos: information list) : int =
let byz = List.find_opt (fun x -> match x with |Byzantines _ -> true | _ -> false) infos
in
match byz with
| Some(Byzantines Number x) -> x
| Some(Byzantines Id _) -> raise(Failure("Generation of byzantines list not implented"))
| _ -> 0
(**[get_val_ret infos] returns the return type of the robogram
@param information list corresponding to the description of the world
@return [string] corresponding to location or direction FOR THE MOMENT*)
let get_val_ret (infos : information list) : string list =
(* TODO: Implementation Light*)
let rec locdir valret = match valret with
| Location::tl -> "location" :: (locdir tl )
| Direction::tl -> "direction" ::(locdir tl)
| Str x ::tl -> if x = "Light" then "light" :: (locdir tl) else (locdir tl)
| [] -> []
in
let valret = List.find_opt (fun x -> match x with |ActivelyUpdate _ -> true | _ -> false) infos
in
match valret with
| Some (ActivelyUpdate x) -> locdir x
| _-> ["location"]
(**[get_space infos] returns the string corresponding to the space
@param information list corresponding to the description of the world
@return [string] corresponding to the space (R, R2, Ring)*)
let get_space (infos : information list) : string =
let space = List.find_opt (fun x -> match x with |Space _ -> true | _ -> false) infos
in
match space with
| Some (Space x) -> string_of_espace x
| _-> ""
(**[get_rigidity infos] returns the string corresponding to the rigidity
@param information list corresponding to the description of the world
@return [string] corresponding to the rigidity (Rigid, Flexible)*)
let get_rigidity (infos : information list) : string =
let space = List.find_opt (fun x -> match x with |Rigidity _ -> true | _ -> false) infos
in
match space with
| Some (Rigidity r) -> string_of_rigidity r
| _-> ""
(**[get_range s] returns the range expression
@param s [sensor list] list of sensors in the description
@return [expr]*)
let get_range (s : sensor list) : expr =
match List.find_opt (fun x -> match x with |Range _ -> true| _ -> false) s with
| Some (Range Limited x) -> x
| Some (Range Full ) -> Var("Full")
| _-> None
(**[multi s] returns a boolean, true if there is multiplicity and false otherwise
@param s [sensor list] list of sensors in the description
@return [bool]*)
let multi (s:sensor list) : bool =
(List.exists (fun x -> match x with
| Multi m-> (match m with
| No -> false
| _ -> true)
| _-> false) s)
(** [expr_to_coq r] returns a Formula.t type expression (ast to write coq by PCourtieux) corresponding to the given expression r
@param expr DSL ast expression to convert to Formula.t
@return [Formula.t]*)
let rec expr_to_coq (r : expr) : Formula.t =
let module StringMap = Map.Make(String) in
match r with
| Cst c -> Int c
| PatternMatching (e1,l) -> Match((expr_to_coq e1),List.map (fun x -> match x with | e2,e3 -> (expr_to_coq e2,expr_to_coq e3)) l)
| Let(s,e1,e2)-> Let(s,expr_to_coq e1,expr_to_coq e2)
| Var s -> Var(0,s)
| Cond (e1,e2,e3) -> If(expr_to_coq e1,expr_to_coq e2, expr_to_coq e3)
| BinOp(x,op ,y) -> (match op with
| Plus -> Infix(expr_to_coq x,"+",expr_to_coq y)
| Minus -> Infix(expr_to_coq x,"-",expr_to_coq y)
| Mult -> Infix(expr_to_coq x,"*",expr_to_coq y)
| Div -> Infix(expr_to_coq x,"/",expr_to_coq y)
| And -> Infix(expr_to_coq x,"&&",expr_to_coq y)
| Or -> Infix(expr_to_coq x,"||",expr_to_coq y)
| Sup -> Infix(expr_to_coq x,">",expr_to_coq y)
| Inf -> Infix(expr_to_coq x,"<",expr_to_coq y)
| Equal -> Infix(expr_to_coq x,"==",expr_to_coq y)
| Diff -> Infix(expr_to_coq x,"!=",expr_to_coq y)
| Impli -> Infix(expr_to_coq x, "->", expr_to_coq y)
| Equiv -> Infix(expr_to_coq x,"<->",expr_to_coq y)
)
| Cons (e1,e2) -> App(Raw("cons"), ([expr_to_coq e1;expr_to_coq e2]))
| Fun (s,e) -> Fun(Some s, expr_to_coq e)
| App (f,arg) -> App(expr_to_coq f, [expr_to_coq arg])
| Set s -> Set (set_to_coq s)
| Point (m,f) -> let c = StringMap.find_opt m Module.correspondance in
(match c with
|None -> raise(Failure("Problem: "^m^" unknow"))
|Some x -> (match StringMap.find_opt f x with
| None -> raise(Failure("Problem "^m^"."^f^" unknow"))
| Some x' -> x')
)
| _ -> Raw("Not Implemented")
and set_to_coq (s:expr set) : Formula.t list =
match s with
| Vide -> []
| Some (s',e) ->expr_to_coq e :: set_to_coq s'
(**[instance_R_R2 s d] generates the coq code to instance R and R2
@param space s
@param information list d
@return [stmt list]
*)
let instance_R_R2 (s:space) (d: information list): stmt list =
let s' = string_of_espace s in
let path = if get_rigidity d = "Flexible" then (* pour chemin droit TODO: check si on ne veut pas de chemin droit, et donc trouve une syntaxe pour le dsl *)
RawCoq(["Definition path_"^s'^ ":= path location."])
::Def("paths_in_"^s',Imply(Raw("location"),Raw("path_"^s')),Raw("local_straight_path"))
::RawCoq(["Coercion paths_in_"^s'^" :location >-> path_"^s'^"."])
::[]
else
[]
in
Instance("Loc",Cst("Location"),App(Cst("make_Location"),[Cst(s')]))
::Instance("VS",Cst("RealVectorSpace location"),Cst(s'^"_VS"))
::Instance("ES",Cst("EuclideanSpace location"),Cst(s'^"_ES"))::path
(**[instance_Ring n] generates the coq code to instantiate a Ring
@param int n
@return [stmt list]*)
let instance_ring (n:int option) : stmt list =
let ring =
match n with
| Some(n') -> Instance("MyRing",Raw("RingSpec"),Record([Raw("ring_size := "^string_of_int n');Raw("ring_size_spec:= ltac:(auto)")]))
| None -> RawCoq(["Context {RR : RingSpec}."])
in
ring::Notation("ring_node",App(Cst "finite_node",[Cst "ring_size"] ))::Instance("Loc",Cst "Location",App(Cst "make_Location",[Cst "ring_node"]))::[]
(**[instance_space s] returns a list of stmt allowing to generate the coq code to instantiate the space s
@param space [s] to instantiate for the moment only R, R2, Ring
@return [stmt list]
*)
let instance_space (s: space) (d : information list): stmt list =
let s' =
match s with
| R -> instance_R_R2 s d
| R2 -> instance_R_R2 s d
| ZnZ n -> instance_ring n
| _ ->raise(Failure ("Space Not implemanted"))
in
s'@[]
(**[instane_updunc_rigid valret] returns the coq code to instantiate the update function
@param string return value of the robogram
@return stmt
*)
let instance_updfunc_rigid (valret : string) (d: information list):stmt list =
if not(get_space d = "Ring") then
Instance("UpdFun",Raw("update_function ("^valret^") (Similarity.similarity location) unit"),Raw("{update := fun _ _ _ target _ => target;update_compat := ltac:(now repeat intro) }"))
::(*RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])::*)[]
else
Instance("FC",App(Cst "frame_choice",[Raw("(Z * bool)")]),Raw(" {frame_choice_bijection :=
fun nb => if snd nb then Ring.sym (fst nb) else Ring.trans (fst nb);
frame_choice_Setoid := eq_setoid _ }"))::
Instance("UpdFun",Raw("update_function direction (Z * bool) unit"),Raw("{
update := fun config g _ dir _ => move_along (config (Good g)) dir;
update_compat := ltac:(repeat intro; subst; now apply move_along_compat) }"))::[]
let instance_updfunc_Flexible (d:expr) (_ : string list): stmt list =
Instance("UpdFun",Raw("update_function (path location) (Similarity.similarity location) ratio"),Raw(" FlexibleUpdate "^string_of_expression d))
::[]
(**[instance_rigidity r valret] returns a list of stmt allowing to generate the coq code to instantiate the rigidity of the displacements
@param rigidity rigidite [r] to instantiate
@param valret return value of the robogram
@return [stmt list]
*)
let instance_rigidity (r:rigidity) (valret : string list) (world: information list): stmt list =
let rc_return, rc_setoid =
match valret with
| x ::[] -> x,x^"_Setoid"
| _ ::_ -> "("^String.concat " * "valret ^")" ,"prod_Setoid "^ String.concat " " (List.map (fun s -> s ^"_Setoid") valret)
| [] -> raise(Failure " Error return value") in
match r with(*TODO: Est-ce la bonne maniere d'ecrire l'UpdateFunc?*)
| Rigide -> Instance("RC",Raw("robot_choice "^rc_return),Raw("{ robot_choice_Setoid := "^rc_setoid^"}"))
::Instance("UC",App(Var(0,"update_choice"),[Cst("unit")]),Raw("NoChoice"))
:: instance_updfunc_rigid (rc_return) world
| Flexible d -> Instance("RC",Raw("robot_choice (path info)"),Raw("{ robot_choice_Setoid := path_Setoid location}"))
::Instance("UC",App(Cst("update_choice"),[Cst("ratio")]),Raw "Flexible.OnlyFlexible")
::Var(string_of_expression d,Raw("R"))
::instance_updfunc_Flexible d valret
(**[instance_info fl] returns a list of stmt allowing to generate the coq code to instantiate the state of the robot
@param field list list of fields to instantiate
@return [stmt list]
*)
let instance_info (fl:field list) : stmt list =
let l = List.assoc_opt "Light" (List.map (fun x -> match x with | Private p -> p | Public p -> p) fl)
in
(match l with
|Some(Light (x)) -> let l' = match x with | Intern p -> p |Extern p -> p | All p -> p in
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.";
"(*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)))."])::[]
(*TODO: Le reste des info sont a faire*)
| _ ->RawCoq(["Definition info := (location)%type."])
::Instance("St",Raw("State location"),Raw("OnlyLocation (fun _ => True)")) ::[])
(**[instance_byzantine x] returns a list of stmt allowing to generate the coq code to instantiate the byzantines
@param int x corresponds to the proportion of Byzantine desired (1/8 -> x = 8)
@return [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."])
::[]
else
Instance("MyRobots",Cst("Names"),App(Cst("Robots"),[Raw("("^string_of_int (x-1) ^ " * n)");Cst("n")]))
::[]
(**[instance_sync x] returns a list of stmt allowing to generate the coq code to instantiate the Active/Inactive Choice/Func corresponding to the synchronization
@param synchro s corresponding to the synchronization of the robots
@return [stmt list]
*)
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_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
@return [stmt list] *)
let instance_sensors (s:sensor list) : stmt list =
let range =string_of_expression (get_range s)
in
let m = if multi s then "multi" else "" in
let errorVS = if multi s then "" else "VS " in
if range != "Full" then Var(range,Raw("R"))
::Instance("Obs",Cst("Observation"),App(Cst ("limited_"^m^"set_observation"),[Cst(errorVS^range)]))
::[]
else Instance("Obs",Cst("Observation"),Cst(m^"set_observation"))::[]
(**[require_rigidity r] returns a stmt allowing to generate the requirement for rigidity [r]
@param rigidity [r] is the rigidity indicated in the description of the world
@return stmt *)
let require_rigidity (r: rigidity) :stmt =
match r with
| Flexible _ -> Require(true,["Pactole.Models.Flexible";"Pactole.Spaces.Similarity"])
| Rigide -> Require(true,["Pactole.Models.Rigid";"Pactole.Models.Similarity";"Pactole.Spaces.Similarity"])
(**[require_space s] returns an stmt allowing to generate the require for space [s]
@param space [s] is the space specified in the world description
@return stmt *)
let require_space (s: space) : stmt =
match s with
| R -> Require(true,["Pactole.Spaces.R"])
| R2 -> Require(true,["Pactole.Spaces.R2";"Rbase"])
| ZnZ _ -> Require(true,["Pactole.Spaces.Ring";"Reals";"Pactole.Spaces.Isomorphism"])
| _ ->raise(Failure ("Not implemanted"))
(**[require_multi s] returns a stmt allowing to generate the require for the multiplicity
@param sensor list [s] is the list of sensors entered in the description of the world allowing the multiplicity to be recovered
@return stmt *)
let require_multi (s: sensor list) : stmt =
let limited = if string_of_expression (get_range s) == "Full" then "" else "Limited"
in
if multi s
then Require(true,["Pactole.Observations."^limited^"MultisetObservation"])
else Require(true,["Pactole.Observations."^limited^"SetObservation"])
(**[require_byzantine nb_byz] returns an stmt allowing to generate the require of the byzantines if there are byzantines
@param int [nb_byz] is the proportion of byzantine
@return stmt *)
let require_byzantine (nb_byz : int) : stmt list=
if nb_byz == 0 then [Require(true,["Pactole.Models.NoByzantine"])] else []
(**[generate_requires world] returns a list of stmt allowing you to generate the necessary imports depending on the [world]
@param information list [world] matches the world description
@return stmt list *)
let generate_requires (world : information list) : stmt list =
let generate_require info acc =
match info with
| Rigidity r -> (require_rigidity r)::acc
| Space s -> (require_space s)::acc
| Sensors s -> (require_multi s) ::acc
| _ -> acc
in let nb_byz = get_nb_byz world in
List.rev (List.fold_right generate_require world (require_byzantine nb_byz)@[Require(true,["Pactole.Setting";"Pactole.Util.FSets.FSetInterface"])]) (*util.fset .... car probleme avec elements..*)
(**[generate_instances world] returns a list of stmt allowing to generate the coq code to instantiate everything there is in [world] in theory
@param information list [world] matches the world description
@return [stmt list]*)
let generate_instances (world : information list): stmt list =
let nb_byz = get_nb_byz world in
let valret = get_val_ret world in
let rec genworld w = match w with
| [] -> []
| h::t-> (match h with
| Space s -> newline::(instance_space s world) @ genworld t
| Rigidity r -> genworld t @newline::(instance_rigidity r valret world)
| Robot r -> newline::(instance_info r) @ genworld t
| Sync s -> genworld t @(instance_sync s)
| Sensors s -> genworld t @ (instance_sensors s)
| _ -> genworld t) in
(Var("n",Raw "nat")::instance_byzantine nb_byz)@(genworld world)
(**[generate_robogram r d] returns a list of stmt used to generate the coq code of the robogram
@param expr list [r] robogram to convert to coq
@param information list [d] allows you to retrieve the return value of the robogram
@return stmt list*)
let generate_robogram (r : expr list) (d: information list) : stmt list =
let valret = get_val_ret d in
let rc_return =
match valret with
| x ::[] -> x
| _ ::_ -> String.concat " * " valret
| [] -> raise(Failure " Error return value") in
let valretcoq = if get_rigidity d = "Flexible" then "(path location)" else rc_return in
match (List.map expr_to_coq r) with
| 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."])
::proof_to_complete
@Def("robogram",Raw("robogram"),Raw("{| pgm := robogram_pgm; pgm_compat := robogram_pgm_compat |}"))
::[]
| [] -> Def ("robogram_pgm (s : observation)",Raw(valretcoq),Raw("[]")) ::[]
module Topological = Graph.Topological.Make(Ast.G)
(**[generate_or l] returns the formula "or" from a list of string
@param string list
@return [Formula.t]*)
let rec generate_or l=
match l with
| h::[] -> Formula.Cst(h)
| 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 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 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 * stmt list) =
Topological.fold (fun v acc ->
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
@param g [G.t]
@return [stmt list]*)
let generate_lemmas (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
(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^"%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)
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_lemme (Measure(g): measure) (name_png : string) : stmt list =
let ret = "nat*nat" 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")::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@
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")])
:: 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 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")
else
()