From 0e2476f33089c4b29bf4fb128344e6f293bf9396 Mon Sep 17 00:00:00 2001
From: Kylian Fontaine <kylian.fontaine@etu.univ-lyon1.fr>
Date: Mon, 17 Jun 2024 09:49:25 +0200
Subject: [PATCH] typo
---
Readme.md | 4 ++--
lib/ast.ml | 45 ++++++++++++++++++++++++++++++++-------------
lib/gencoq.ml | 16 ++++++++--------
3 files changed, 42 insertions(+), 23 deletions(-)
diff --git a/Readme.md b/Readme.md
index d9b4c87..3ce2a25 100644
--- a/Readme.md
+++ b/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
diff --git a/lib/ast.ml b/lib/ast.ml
index 1c2217b..c865a8d 100644
--- a/lib/ast.ml
+++ b/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
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 8fe7a03..a952400 100644
--- a/lib/gencoq.ml
+++ b/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
--
GitLab