typo

Readme.md

@@ -2,7 +2,7 @@
 
 ### Valeurs possibles pour chaque éléments de la description de l'environnement :
 
-- Sync := Permet de definir le type de synchronisation.
+- Sync := Permet de définir le type de synchronisation.
   - FSYNC -> Full synchrone
   - SSYNC -> Semi synchrone
   - ASYNC -> Asynchrone
@@ -12,7 +12,7 @@ exemple :
 Sync := ASYNC 
 ```
 
-- Space := Permet de definir l'espace dans le quel vont évolués les robots.
+- Space := Permet de définir l'espace dans le quel vont évoluer les robots.
   - R  -> une seul dimension
   - Rm -> millefeuille d'une dimension, correspondant par exemple a x routes paralelles
   - R2 -> plan 

lib/ast.ml

@@ -400,34 +400,44 @@ let info_space (i : information):bool =
     @return true si la description repond aux critères false sinon
     TODO: A finir/ utilisation de valeur par defaut si non fourni? pourquoi pas 
     *)
-
 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 "Probleme de definition de la synchronisation"; false)
+                                  then (print_endline "Error: Problem of defining sync"; false)
 													    else (
                                   if not(unique info_space d') 
-                                    then (print_endline "Probleme de definition de l'espace";false)
+                                    then (print_endline "Error: Problem of defining space";false)
 													        else true
 														  )  ;;
 
-
+(**[get_sensors d] Renvoie la liste de sensors contenu dans la description [d]
+    @param description 
+    @return [sensor list] 
+    *)
 let get_sensors (d : description) : sensor list =
   match d with 
   | Description(d', _) -> (match List.find_opt (fun x -> match x with Sensors _ -> true | _-> false) d' with 
                           Some (Sensors s) -> s 
-                          | _ -> raise(Failure("Not find sensors")))
+                          | _ -> raise(Failure("Error: Not find Sensors")))
+
+(**[get_robot d] Renvoie la liste des champs robot contenu dans la descritpion [d]
+    @param description
+    @return [field list]*)
 let get_robot (Description(d', _) : description) : field list =
   match List.find_opt (fun x -> match x with Robot _ -> true | _-> false) d' with 
                           Some (Robot r) -> r 
-                          | _ -> raise(Failure("Not find sensors"))
+                          | _ -> raise(Failure("Error: Not find Robot"))
+
+(**[get_activelyup d] Renvoie la liste des string correspondant aux champs mis à jour par le robogram
+    @param description
+    @return [string list] *)
 let get_activelyup (d : description) : string list = 
   match d with 
   | Description(d', _) -> (match List.find_opt (fun x -> match x with ActivelyUpdate _ -> true | _-> false) d' with 
                           Some (ActivelyUpdate a) -> List.map string_of_valretr a
-                          | _ -> raise(Failure("Not find ActivelyUpdate")))
+                          | _ -> raise(Failure("Error: Not find ActivelyUpdate")))
 
 (** [check_sensor s r] verifie qu'un sensor [s] soit bien déclarer dans le robot [r],ou alors qu'il soit pas un sensor custom 
     @param [s] sensor à verifié
@@ -443,27 +453,36 @@ let check_sensor (s: sensor) (r:field list):bool =
 
 (** [check_sensors_desc d] verifie que la liste de sensors de la description correspond a des sensors de robot
     @param d description dans la quel on verifie sa liste de sensors avec sa déclaration de robot (field list)
-    @return true si les sensors sont custom et sont bien dans robot ou si il ne sont pas custom*)
+    @return [true] si les sensors sont custom et sont bien dans robot ou si il ne sont pas custom*)
 let check_sensors_desc (d:description) :bool =
    let res= List.find_opt (fun x -> not (check_sensor x (get_robot d))) (get_sensors d) in
     match res with 
-    | Some x -> print_endline("Erreur : " ^(match x with |Custom (x',_)-> x' | _->"")^" n'est pas déclarer en public dans robot"); false
+    | Some x -> print_endline("Error : " ^(match x with |Custom (x',_)-> x' | _->"")^" is not declared public in robot"); false
     | _-> true
 
+(**[check_activelyup d] verifie que les champs renseignés dans activelyupdate soient déclarés dans robot
+    @param d [description]
+    @return [bool]*)
 let check_activelyup (d:description) :bool =
     let field_to_pair f = List.map(fun x -> match x with Public x -> x | Private x -> x) f in
     let aux s l = List.exists (fun (x,_) -> x = s) (field_to_pair l) in
     let res = List.find_opt (fun x -> not (aux x (get_robot d))) (get_activelyup d) in
     match res with 
-    | Some x -> print_endline("Erreur : " ^x^" n'est pas déclarer en public dans robot"); false
+    | Some x -> print_endline("Error : " ^x^" x is not declared in robot"); false
     | _-> true
   
 
 (**[check_light d] si il y a des lumiere intern on verifie qu'elle soit pas renseigné en public
+                   et si extern pas dans private
     @param description [d] description du monde
     @return bool true si pas de lumiere intenre en public *)
 let check_light d : bool = 
-  let rec check flist = (fun x -> match x with 
-    |[] -> true
-    |Public (_,Light(Intern _))::_ -> false| _::t-> check t) flist in
+  let rec check flist = (
+    fun x -> match x with 
+    | [] -> true
+    | Public (_,Light(Intern _))::_ -> false
+    | Private (_, Light(Extern _))::_ -> false
+    | _::t-> check t
+   ) flist 
+  in
   check (get_robot d)
\ No newline at end of file

lib/gencoq.ml

@@ -246,8 +246,6 @@ let require_space (s: space) : stmt =
     @param sensor list [s] est la liste des sensors renseignée dans la description du monde permettant de recupérer la multiplicité
     @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
@@ -302,11 +300,13 @@ let generate_robogram (r : expr list) (d: information list) : stmt list =
   let valret = get_val_ret d in
   let valretcoq = if get_rigidity d = "Flexible"  then "(path " ^ valret ^ ")" else valret 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 |}")):: []
+  | 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("[]")) ::[]
 
 let generate (Description(d,r) : description) (section_name : string)=
@@ -317,4 +317,4 @@ let generate (Description(d,r) : description) (section_name : string)=
     Format.fprintf format_file "%a@." Coq.pretty_l ((generate_requires d)@[section]);
     close_out file_out
   else 
-    raise(Failure("Error internal light in public field"))
\ No newline at end of file
+    raise(Failure("Error light in wrong field"))
\ No newline at end of file