From 537d0e7dd42cf863ae11b3a3981e123b592cccd1 Mon Sep 17 00:00:00 2001
From: Kylian Fontaine <kylian.fontaine@etu.univ-lyon1.fr>
Date: Mon, 17 Jun 2024 09:08:31 +0200
Subject: [PATCH] typo

---
 Readme.md           |  6 ++---
 generate/test.v     | 42 ++++++++++++++++----------------
 lib/ast.ml          |  8 +++----
 lib/gencoq.ml       | 58 ++++++++++++++++++++++++++++-----------------
 lib/lexer.mll       |  4 ++--
 lib/parser.mly      |  8 +++----
 sourcegenerate/test | 22 +++++++----------
 7 files changed, 78 insertions(+), 70 deletions(-)

diff --git a/Readme.md b/Readme.md
index d5a5cae..d9b4c87 100644
--- a/Readme.md
+++ b/Readme.md
@@ -24,10 +24,10 @@ exemple :
 Space := Ring 5
 ```
 - Byzantine := Permet de déclarer le nombre de Byzantins ou directement les robots qui le sont via leur id.
-  - x -> un entier correspondant au nombre de Byzantins
+  - x -> un entier correspondant à la proportion de Byzantins
   - [id1;id2;id3] -> liste d'entier correspondant aux id des Byzantins
 ```
-exemple : Byzantin := [1;2;7;8]
+exemple : Byzantine := [1;2;7;8]
 ```
 - Rigidity: Défini si le robot peut etre interrompu lors de son déplacement
         - Rigide -> Le robot finit sont déplacement avant de recommencer un cycle LCM
@@ -50,7 +50,7 @@ Robot := Private :  Temperature; Coordonnee [5;1.8]
 - Sensors := Permet de définir les capteurs des robots, et les fonction de degradations sur informations reçues
   Default :
   - **Range** : Correspond à la distance de vue des robots
-    - Full       -> Le robot à une range ilimité 
+    - F Byzantinull       -> Le robot à une range ilimité 
     - Limited d  -> range limité à un delta
     - K_Rand d k -> range limité à un delta + capable de voir k robots au dela de delta choisie rand
     - K_enemy d k -> range limité à un delta + capable de voir k robots au dela de delta choisie par un ennemie
diff --git a/generate/test.v b/generate/test.v
index d374bda..e2a5475 100644
--- a/generate/test.v
+++ b/generate/test.v
@@ -1,38 +1,38 @@
 Require Import Pactole.Setting Pactole.Util.FSets.FSetInterface.
-Require Import Pactole.Observations.MultisetObservation.
-Require Import Pactole.Models.Rigid.
-Require Import Pactole.Spaces.R.
+Require Import Pactole.Observations.SetObservation.
+Require Import Pactole.Models.Flexible.
+Require Import Pactole.Spaces.R2 Rbase.
 Section test.
   Variable n: nat.
   Instance MyRobots: Names := Robots (9 * n) n.
    
-  Instance Loc: Location := make_Location R.
-  Instance VS: RealVectorSpace location := R_VS.
-  Instance ES: EuclideanSpace location := R_ES.
+  Instance Loc: Location := make_Location R2.
+  Instance VS: RealVectorSpace location := R2_VS.
+  Instance ES: EuclideanSpace location := R2_ES.
+  Definition path_R2:= path location.
+  Definition paths_in_R2: location -> path_R2 := local_straight_path.
+  Coercion paths_in_R2 :location >-> path_R2.
    
   Instance St: State location := OnlyLocation (fun _ => True).
-  Instance Obs: Observation := multiset_observation.
+  Instance Obs: Observation := set_observation.
    
-  Instance RobotChoice: robot_choice location :=
-    { robot_choice_Setoid := location_Setoid}.
-  Instance ActiveChoice: update_choice unit := NoChoice.
+  Instance RobotChoice: robot_choice (path location) :=
+    { robot_choice_Setoid := path_Setoid location}.
+  Instance ActiveChoice: update_choice ratio := Flexible.OnlyFlexible.
+  Variable delta: R.
   Instance UpdateFunc:
-    update_function (location) (Similarity.similarity location) unit :=
-    {update := fun _ _ _ target _ => target;update_compat := ltac:(now repeat intro) }.
-  Instance Rigid : RigidSetting.
-  Proof using . split. reflexivity. Qed.
+    update_function (path location) (Similarity.similarity location) ratio :=
+      FlexibleUpdate delta.
   Instance InactiveChoice : inactive_choice unit := NoChoiceIna.
   Instance InactiveFunc : inactive_function unit := NoChoiceInaFun.
    
-  Definition Robogram_pgm (s : observation): location :=
-    let c := support s
-    in match c with
-       | nil => 0
-       | cons pt nil => pt
-       | cons _ (cons _ _) => isobarycenter c
-       end.
+  Definition Robogram_pgm (s : observation): (path location) :=
+    let aux s := let c := (elements s)
+                 in isobarycenter c
+    in paths_in_R2 (aux s).
   Instance Robogram_pgm_compat : Proper (equiv ==> equiv) Robogram_pgm.
   (* Preuve *)
+  Admitted.
   Definition Robogram: robogram :=
     {| pgm := Robogram_pgm; pgm_compat := Robogram_pgm_compat |}.
 End test.
diff --git a/lib/ast.ml b/lib/ast.ml
index f64df57..1c2217b 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -176,7 +176,7 @@ type field =
   | Private of (string * value)
   | Public of (string * value)
 
-type byzantin = 
+type byzantine = 
   | Number of int
   | Id of int list
 
@@ -195,7 +195,7 @@ type information =
   | Sync of synchro
   | Rigidity of rigidity
   | Space of space
-  | Byzantins of byzantin
+  | Byzantines of byzantine
   | Sensors of sensor list
   | Robot of field list
   | ActivelyUpdate of valretR list(*nom du champ*)
@@ -339,7 +339,7 @@ let string_of_field (f : field) : string =
   match f with
   | Private (s,v)-> "Private: "^s^"->"^ string_of_value v
   | Public (s,v) -> "Public: "^s^"->"^ string_of_value v
-let string_of_byzantin (b : byzantin) : string =
+let string_of_byzantine (b : byzantine) : string =
   match b with
   | Number n -> "Il y a n/" ^ string_of_int n ^ " Byzantin(s)" 
   | Id l -> "Liste des byzantins : [" ^ String.concat "; " (List.map string_of_int l) ^"]"
@@ -365,7 +365,7 @@ and string_of_information (info: information) : string =
                   | Flexible d  -> "Rigidity: Flexible d'une distance delta = " ^ string_of_expression d)
 
   | Space e -> "Espace: "    ^ (string_of_espace e)
-  | Byzantins b ->  string_of_byzantin b
+  | Byzantines b ->  string_of_byzantine b
   | Sensors s -> "Sensors: [" ^ String.concat "; " (List.map string_of_sensor s) ^ "] "
   | Robot r -> "Robot : ["^ String.concat "; " (List.map string_of_field r) ^ "]"
   | Roles r -> "Roles :" ^ String.concat "\n " (List.map string_of_role r)
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 20cd303..8fe7a03 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -5,28 +5,24 @@ open Coq
 
 
 
-let geometry =[("barycenter",Formula.Raw("isobarycenter"));
+let geometry =[("isobarycenter",Formula.Raw("isobarycenter"));
                 ("on_SEC"),Formula.Raw("on_SEC")]
-let observation =[("elements", Formula.Raw("elements s"));
+let observation =[("elements", Formula.Raw("(elements s)"));
                   ("support"), Formula.Raw("support s")]
 let correspondance = [("Geometry",geometry);
-                     ("Obs"),observation]
-
-
-
-
-
+                     ("Obs",observation)]
 let newline =RawCoq([" "])
+let proof_to_complete = [Comment("Preuve");RawCoq(["Admitted."])]
 
 (** [get_nb_byz infos] retourne le nombre de byzantins désirés
     @param information list correspondant à la description du monde
     @return [int]*)
 let get_nb_byz (infos: information list) : int =
-    let byz = List.find_opt (fun x -> match x with |Byzantins _ -> true | _ -> false) infos 
+    let byz = List.find_opt (fun x -> match x with |Byzantines _ -> true | _ -> false) infos 
     in
       match byz with
-      | Some(Byzantins Number x) -> x
-      | Some(Byzantins Id liste) -> List.length liste
+      | Some(Byzantines Number x) -> x
+      | Some(Byzantines Id liste) -> List.length liste (*TODO: Evidement faux mais a traiter plus tard*)
       | _ -> 0
 
 
@@ -48,24 +44,38 @@ let get_val_ret (infos : information list) : string =
     | Some (ActivelyUpdate x) -> locdir x
     | _-> "location"
     
+(**[get_space infos] retourne le string correspondant à l'espace 
+    @param information list correspondant à la description du monde
+    @return [string] correspondant a l'espace (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] retourne le string correspondant à la rigidité 
+    @param information list correspondant à la description du monde
+    @return [string] correspondant à la rigidité (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] retourne l'expression de la range 
+    @param s [sensor list] liste des capteurs de la 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] retourne un booleen, true si il y a de la multiplicité et false sinon
+    @param s [sensor list] liste des capteur de la description
+    @return bool*)
 let multi (s:sensor list) : bool =
   (List.exists (fun x -> match x with 
                         | Multi m->  (match m with
@@ -175,11 +185,11 @@ let instance_info (fl:field list) : stmt list =
   (*TODO: Le reste des info sont a faire*)
   | _ ->Instance("St",Raw("State location"),Raw("OnlyLocation (fun _ => True)")) ::[]) 
   
-(**[instance_byzantin x] retourne une liste de stmt permettant de generer le code coq pour instancier les byzantins
+(**[instance_byzantine x] retourne une liste de stmt permettant de generer le code coq pour instancier les byzantins
         @param int x correspond a la proportion de byzantin voulu (1/8 -> x = 8)
         @return [stmt list]
           *)  
-let instance_byzantin (x : int ) : stmt list = 
+let instance_byzantine (x : int ) : stmt list = 
   if x < 1 then 
     Instance("MyRobots",Var(0,"Names"),App(Var(0,"Robots"),[Var(0,"n");Int 0]))
     ::RawCoq(["Instance NoByz : NoByzantine.";"Proof using . now split. Qed."])
@@ -188,6 +198,10 @@ let instance_byzantin (x : int ) : stmt list =
   Instance("MyRobots",Var(0,"Names"),App(Var(0,"Robots"),[Var(0,"("^string_of_int (x-1) ^ " * n)");Var(0,"n")]))
     ::[]
 
+(**[instance_sync x] retourne une liste de stmt permettant de generer le code coq pour instancier les Active/Inactive Choice/Func correspondant a la synchronisation
+    @param synchro s correspondant a la synchronisation des robots
+    @return [stmt list]
+    *)  
 let instance_sync (s : synchro) : stmt list =
   match s with 
   | Async -> [RawCoq(["Instance InactiveChoice: Async not implemented
@@ -195,6 +209,9 @@ let instance_sync (s : synchro) : stmt list =
   | _ -> [RawCoq([ "Instance InactiveChoice : inactive_choice unit := NoChoiceIna.";
   "Instance InactiveFunc : inactive_function unit := NoChoiceInaFun."])]
 
+(**[instance_sensors s] permet d'instancier l'observation celon la liste des capteurs [s] Ne prend en compte que la range et la multiplicité pour le moment
+    @param s [sensor list] correspondant a la liste des capteurs de la description
+    @return [stmt list] *)
 let instance_sensors (s:sensor list) : stmt list = 
   let range =string_of_expression (get_range s)
   in
@@ -206,9 +223,6 @@ let instance_sensors (s:sensor list) : stmt list =
 
   else Instance("Obs",Var(0, "Observation"),Var(0,m^"set_observation"))::[]
 
-
-
-
 (**[require_rigidity r] retourne un stmt permettant de generer le require pour la rigidite [r]
     @param rigidite [r] est la rigidite renseignée dans la description du monde
     @return stmt *)
@@ -240,10 +254,10 @@ let require_multi (s: sensor list) : stmt =
     then Require(true,["Pactole.Observations."^limited^"MultisetObservation"]) 
     else Require(true,["Pactole.Observations."^limited^"SetObservation"])
 
-(**[require_byzantin nb_byz] retourne un stmt permettant de generer le require des byzantins si il y des byzantins
+(**[require_byzantine nb_byz] retourne un stmt permettant de generer le require des byzantins si il y des byzantins
     @param int [nb_byz] est la proportion de byzantin
     @return stmt *)  
-let require_byzantin (nb_byz : int) : stmt list=
+let require_byzantine (nb_byz : int) : stmt list=
   if nb_byz == 0 then [Require(true,["Pactole.Models.NoByzantine"])] else [] 
 
 
@@ -258,7 +272,7 @@ let generate_requires (world : information list) : stmt list =
     | 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_byzantin nb_byz)@[Require(true,["Pactole.Setting";"Pactole.Util.FSets.FSetInterface"])]) (*util.fset .... car probleme avec elements..*)
+  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] retourne une liste de stmt permettant de generer le code coq pour instancier tout ce qu'il y a dans [world] en theorie
@@ -278,7 +292,7 @@ let valret = get_val_ret world in
           | _ ->genworld t) in
   
   
-   (Var("n",Raw "nat")::instance_byzantin nb_byz)@(genworld world)
+   (Var("n",Raw "nat")::instance_byzantine nb_byz)@(genworld world)
 
 (**[generate_robogram r d] retourne une liste de stmt permettant de generer le code coq du robogram
     @param expr list [r] robogram a convertir en coq
@@ -291,8 +305,8 @@ let generate_robogram (r : expr list) (d: information list) : stmt list =
   | 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."])
-            ::Comment("Preuve")
-            ::Def("Robogram",Raw("robogram"),Raw("{| pgm := Robogram_pgm; pgm_compat := Robogram_pgm_compat |}")):: []
+            ::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)=
diff --git a/lib/lexer.mll b/lib/lexer.mll
index bd796e9..6215f70 100644
--- a/lib/lexer.mll
+++ b/lib/lexer.mll
@@ -24,7 +24,7 @@ rule token = parse
     | "R2"              {R2}
     | "R2m"             {R2M}
     | "Ring"            {ANNEAU}
-    | "Byzantin"        {BYZANTIN}
+    | "Byzantine"        {BYZANTINE}
     | "Sensors"         {SENSORS}
     | "Robot"           {ROBOT}
     | "Roles"           {ROLES}
@@ -113,4 +113,4 @@ rule token = parse
 and comment = parse 
     | "*/" {numero_carac := !numero_carac + 1 ;token lexbuf}
     | "\n" {numero_ligne := !numero_ligne + 1 ;numero_carac := 1; comment lexbuf}
-    | _  {numero_carac := !numero_carac + 1 ;comment lexbuf}
\ No newline at end of file
+    | _  {numero_carac := !numero_carac + 1 ;comment lexbuf}
diff --git a/lib/parser.mly b/lib/parser.mly
index 2ccc86a..692b062 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -8,7 +8,7 @@
 %token IS
 %token SYNC FSYNC SSYNC ASYNC
 %token SPACE R RM R2 R2M ANNEAU 
-%token BYZANTIN
+%token BYZANTINE
 %token SENSORS
 %token RANGE FULL LIMITED K_RAND K_ENEMY
 %token MULTI NO_MEM WEAKL STRONGL WEAKG STRONGG
@@ -61,11 +61,11 @@ information :
     /* Space := e  */
     | SPACE IS e = espace {[Space e]}
     /* Byzantin := entier*/
-    | BYZANTIN IS i = INT {[Byzantins (Number i)]}
+    | BYZANTINE IS i = INT {[Byzantines (Number i)]}
     /* Byzantin := [1;2;8;9] liste d'id correspondant aux bizantins*/
-    | BYZANTIN IS id = list_int {[Byzantins (Id id)]}
+    | BYZANTINE IS id = list_int {[Byzantines (Id id)]}
     /* Roles := 0 : Compagnon; 5 : Byzantin*/
-    | ROLES IS r = separated_list(SEMICOLON,elements_list_role) {[Roles r]}
+    | ROLES IS r = separated_list(SEMICOLON,elements_list_role) {[Roles r]}/*Vraiment utile? avec robot pas sur..*/
     | robot sensors activelyupdate {[$1;$2;$3]}
     | robot activelyupdate sensors  {[$1;$2;$3]}
     | SHARE IS s = share_item {[Share s]}
diff --git a/sourcegenerate/test b/sourcegenerate/test
index 24ebd9b..28041fa 100644
--- a/sourcegenerate/test
+++ b/sourcegenerate/test
@@ -1,29 +1,23 @@
 /*Description environnement et capacité robot*/
 World :
 Sync := FSYNC 
-Space := R
-Rigidity := Rigid
-Byzantin := 10 /*Correspond à 1/8*/
+Space := R2
+Rigidity := Flexible delta
+Byzantine := 10 /*Correspond à 1/8*/
 
 
 Robot := Private : 
          Public : 
 
 Sensors := Range : Full; 
-           Multiplicity : Weak Local;
-           Opacity: Opaque
-ActivelyUpdate := Location ; Light
-Share := Fullcompass 
-Roles := 0 : Compagnon ; 2 : Leader 
+           Multiplicity : No;
+           Opacity: Transparent
+ActivelyUpdate := Location 
     
 Robogram : 
 
-let c = Obs.support in 
-match c with
-| nil -> (0)
-| pt :: nil -> pt
-| _ :: _ :: _ -> Geometry.barycenter c
-end 
+let c = Obs.elements in 
+ Geometry.isobarycenter c 
 
 
 /*Measure : avec description graphe + nuple qui correspond a la measure*/
-- 
GitLab