regroupement des check

lib/ast.ml

@@ -356,23 +356,6 @@ type measure = Measure of G.t
 type description = Description of (information list) * (expr list) * measure
 
   
-(**[check_description d] verifies that the description [d] has the minimum information
-                          expected for a description and for each type of information to be unique
-                          (two definitions of space which one to choose?...)
-    @param [d] description to check
-    @return true if the description meets the criteria false otherwise
-    *)
-let check_description (d : description) :bool =
-			let unique f d = List.length (List.filter f d) = 1
-			in 
-			match d with 
-			| Description (d',_,_) -> if not(unique info_sync d')
-                                  then (print_endline "Error: Problem of defining sync"; false)
-													    else (
-                                  if not(unique info_space d') 
-                                    then (print_endline "Error: Problem of defining space";false)
-													        else true
-														  )  ;;
 
 (**[get_sensors d] Returns the list of sensors contained in description [d]
     @param description 
@@ -450,3 +433,26 @@ let check_light d : bool =
   check (get_robot d)
 
 
+
+(**[check_description d] verifies that the description [d] has the minimum information
+                          expected for a description and for each type of information to be unique
+                          (two definitions of space which one to choose?...)
+    @param [d] description to check
+    @return true if the description meets the criteria false otherwise
+    *)
+    let check_description (d : description) :bool =
+			let unique f d = List.length (List.filter f d) = 1
+			in 
+      let aux d =
+			match d with 
+			| Description (d',_,_) -> if not(unique info_sync d')
+                                  then raise(Failure "Error: Problem of defining sync")
+													      else (
+                                  if not(unique info_space d') 
+                                    then raise(Failure "Error: Problem of defining space")
+													        else true
+														  ) 
+      in if  check_light d && check_activelyup d && check_sensors_desc d && aux d then true else false                   
+;;
+                              
+                                
\ No newline at end of file

lib/gencoq.ml

@@ -348,6 +348,13 @@ match l with
   | h::tl -> Or(Cst(h),generate_or tl) 
   | _ -> Cst("")
 
+(**[generate_definition_phase g] *)
+let generate_defintion_phase (g : G.t) : stmt list =
+  Ast.G.fold_vertex (fun v acc -> 
+    let func_name = string_of_expression v ^" (config : configuration)" in 
+    RawCoq(["Definition "^func_name^":= (* To_Complete *)."])::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]*)
@@ -396,7 +403,8 @@ let generate_measure (Measure(g): measure) (name_png : string) : stmt list =
   Ast.png_from_graph g name_png;
   let measure_per_phase = generate_measure_per_phase g in 
   let lemsgen = let lems = generate_lemmas g in 
-   measure_per_phase
+    Comment("Definition of phase")::generate_defintion_phase g
+    @Comment("Definition of measure per phase ")::measure_per_phase
     @Lemma("InGraph",Forall("config",generate_or (snd lems)),[Comment("TODO")])
     ::List.rev (fst lems) in 
     lemsgen@
@@ -409,9 +417,7 @@ let generate_measure (Measure(g): measure) (name_png : string) : stmt list =
     @param string s
     @return[unit] *)
 let generate_coq (Description(d,r,m) : description) (section_name : string)=
-  if Ast.check_light (Description (d,r,m)) && 
-     Ast.check_activelyup (Description(d,r,m)) &&
-     Ast.check_sensors_desc (Description(d,r,m))
+  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