Skip to content
Snippets Groups Projects
Select Git revision
  • 423709619949c8961d343a859a93796bb116e5e9
  • main default protected
2 results

gencoq.ml

Blame
  • 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 
        ()