diff --git a/lib/ast.ml b/lib/ast.ml
index ded326a480848accb8dd281cc6f00ae5b6e25550..55fe4f3e5c2b5560e7128094ce4958a8794e52f9 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -15,7 +15,7 @@ type binop =
| Impli
| Equiv
-(*tail::head au lieu de head::tail pour optimisation mémoire, éviter les empilements inutiles
+(*tail::head au lieu de head::tail pour éviter les empilements inutiles
(((vide,x),y),z)
pour le set x,y,z*)
type 'a set =
@@ -23,28 +23,20 @@ type 'a set =
| Some of ('a set) * 'a
-(*type pour l'utilisation de point avec obs, self, les package etc
-type objet =
- | Self
- | Obs
- | Geometry *)
-
type expr =
- | None (*variable declaré mais non défini*)
+ | None
| Bool of bool
| Cst of int
| Cstf of float
| BinOp of expr * binop * expr
| Not of expr
| Cond of expr * expr *expr
- | Var of string (* est ce qu'on ratache un type a la variable?*)
+ | Var of string
| Let of string * expr * expr
| Fun of string * expr
| App of expr * expr
- | Affectation of string * expr (* variable deja declaré avec let et on change sa valeur*)
- | Set of expr set (* FIXME: Est ce qu'on veut vraiment un set d'expression? donc avoir des possibilités tel que : [Boucle(cond, e); Cst 1;....] *)
- | LengthSet of expr (* lors de l'interpretation qu'on checkera que l'expression donné soit bien un set*)
- | PushSet of expr * expr
+ | Affectation of string * expr
+ | Set of expr set
| Point of string * string
| PatternMatching of expr * (expr * expr)list
| Cons of expr *expr
@@ -54,21 +46,21 @@ type expr =
(*DESCRIPTION DE L'ENVIRONNEMENT*)
-(** type syncho :
- Fsync -> Full synchronisé
- Ssync -> Semi synchronisé
- Async -> Asynchronisé*)
+(** type synchro:
+ Fsync -> Full synchronized
+ Ssync -> Semi synchronized
+ Async -> Asynchronized*)
type synchro =
| Fsync
| Ssync
| Async
-(** type space :
- R -> une ligne
- Rm -> un millefeuille de ligne (convoie)
- R2 -> un plan
- R2m -> millefeuille de plan (simplification de R3)
- ZnZ -> anneau prennant n -> positions congruantes
+(** type space:
+ R -> one line
+ Rm -> a line millefeuille (convoy)
+ R2 -> a plan
+ R2m -> plan millefeuille (convoy)
+ ZnZ -> ring taking n -> congruent positions
*)
type space =
| R
@@ -77,23 +69,23 @@ type space =
| R2m
| ZnZ of int
-(* type range :
- Full -> Full range
- Limited -> range limité a un delta
- K_rand -> range limité a un delta + capable de voir k robots au dela de delta choisie rand
- K_enemy -> range limité a un delta + capable de voir k robots au dela de delta choisie par un ennemie*)
+(* type range:
+ Full -> Full range
+ Limited -> range limited to a delta
+ K_rand -> range limited to a delta + capable of seeing k robots beyond delta chosen random
+ K_enemy -> range limited to a delta + capable of seeing k robots beyond delta chosen by an enemy*)
type range =
| Full
| Limited of expr
| K_rand of expr * expr
| K_enemy of expr * expr
-(* type multiplicite :
- No -> Pas de multiplicité
- Weak -> Multiplicité faible : sait si 1 ou plusieurs robots mais pas combien de robot
- Strong -> Multiplicité forte : connait le nombre de robot
- Local -> robot ne connait que sur sa position
- Global -> robot connait pour toute les positions observés
+(* type multiplicity:
+ No -> No multiplicity
+ Weak -> Low multiplicity: knows if 1 or more robots but not how many robots
+ Strong -> Strong multiplicity: knows the number of robots
+ Local -> robot only knows its position
+ Global -> robot knows for all observed positions
*)
type multiplicite =
| No
@@ -102,17 +94,7 @@ type multiplicite =
| Weak_Global
| Strong_Global
-(* type light : Liste de couleurs
- Intern -> Les lumieres vu par le robot lui meme
- Extern -> Les lumieres vu par les robots autre que lui meme
- All -> Les lumieres vu par tout les robots lui meme compris
- Vaut mieux liste de string pour chaque couleurs ou autre chose, un simple int correspondant au nombre de lumiere ?
- *)
-(*type lumiere =
- | Interne of int
- | Externe of int
- | All of int
-*)
+
type color =
| Red
| Blue
@@ -122,59 +104,53 @@ type color =
| Orange
-type lights =
+(* type light: List of colors
+ Intern -> Light seen by the robot itself
+ Extern -> Light seen by robots other than himself
+ All -> Light seen by all robots including themselves *)
+type light =
| Intern of color list
| Extern of color list
| All of color list
-(* type memoire :
- Oblivious -> memoire reset a chaque Look-Compute-Move
- Finite -> memoire persistante entre deux Look-Compute-Move
- Infinite -> se rappel de tout
- *)
-(*type memory =
- | Oblivious
- | Finite of int
- | Infinite
-*)
- (* type opacity :
- Opaque -> Les robots sont opaques
- Transparant -> Les robots sont transparant
- SemiOpaque n -> Transparant a partir d'une distance n ? (aucune idée des decomposition possible des probleme)
- *)
+
+(* type opacity:
+ Opaque -> Robots are opaque
+ Transparent -> Robots are transparent *)
type opacity =
| Opaque
| Transparent
- (*type rigidity :
- Rigide -> les robots atteignent leur destination final, ils ne sont pas interrompu pendant leur mouvement
- Flexible of float -> Les robots peuvent etre interrompu pendant leur mouvement, ils n'atteignent pas forcement leur
- destinations final cependant il parcourt au minimum une distance delta
- *)
+(* type rigidity:
+ Rigid -> the robots reach their final destination, they are not interrupted during their movement
+ Flexible of float -> Robots can be interrupted during their movement, they do not necessarily reach their
+ final destinations however it travels at least a delta distance *)
type rigidity =
| Rigide
| Flexible of expr
-(*type representant les fonction de degradation*)
+(* type representing degradation functions *)
type degrfunc =
| Str of string
| Fun of expr
-(* type sensor : regroupement des capteurs des robots *)
+
+(* type sensor: robot's sensors *)
type sensor =
| Range of range
| Opacity of opacity
| Multi of multiplicite
| Custom of string * degrfunc
-(** type value : valeur pouvant etre utilisant dans les champs field*)
+(* value type: value that can be used in field fields*)
type value =
| Empty
| Int of int
| Float of float
| String of string
| Liste of value list
- | Light of lights
-(** type field : type correspondant au champs que l'utilisateur va renseigner pour le robot*)
+ | Light of light
+
+(* type field: type corresponding to the field that the user will fill in for the robot *)
type field =
| Private of (string * value)
| Public of (string * value)
@@ -201,27 +177,12 @@ type information =
| Byzantines of byzantine
| Sensors of sensor list
| Robot of field list
- | ActivelyUpdate of valretR list(*nom du champ*)
+ | ActivelyUpdate of valretR list
| Roles of (int * string) list
| Share of share
-(*FONCTION SUR LES SETS*)
-(** [length s] retourne la longueur du set [s]
- @param [s] 'a set dont on veut la longueur
- @return int la longueur du set*)
-let rec length_set (s:'a set): int =
- match s with
- | Vide -> 0
- | Some (s,_) -> 1 + (length_set s)
-
-(**[push s e] ajoute un element e au set s
- @param s de type 'a set
- @param e de type 'a
- @return un set correspondant au set s avec l'ajout de e *)
-let push (s:'a set) (e : 'a) :'a set = Some(s,e)
-
-(*CONVERTION EN STRING*)
+(*STRING CONVERSION*)
let string_of_valretr (v : valretR) :string =
match v with
|Location -> "Location"
@@ -229,14 +190,12 @@ let string_of_valretr (v : valretR) :string =
|Str s -> s
let rec string_of_set (s: 'a set) (f : 'a -> string) : string =
match s with
- | Vide -> "Vide"
+ | Vide -> "()"
| Some (s',e) -> "("^ string_of_set s' f ^"," ^ f e ^")"
-
-
-(** [string_of_expression e] Permet d'obtenir un string correspondant a l'expression [e]
- @param [e] expression dont on souhaite le string
- @return string correspondant a l'expression [e]
+(** [string_of_expression e] Allows you to obtain a string corresponding to the expression [e]
+ @param [e] expression whose string we want
+ @return string corresponding to the expression [e]
*)
let rec string_of_expression (e : expr) : string =
match e with
@@ -263,39 +222,15 @@ let rec string_of_expression (e : expr) : string =
| Cond(c,e1,e2) -> "if (" ^string_of_expression c ^ ") then \n {" ^ string_of_expression e1 ^ "} \n else {" ^ string_of_expression e2 ^ "}"
| Affectation(v,e) -> v ^ " prend la valeur " ^ string_of_expression e
| Set s -> string_of_set s string_of_expression
- | Let (v,e1,e2) -> "Déclaration de la variable " ^ v ^ " avec definition : " ^ string_of_expression e1 ^ " dans \n(" ^string_of_expression e2 ^")"
- | Fun (s,e) -> "Fonction qui prend en parametre " ^ s ^ " et retourne (" ^ string_of_expression e ^")"
+ | Let (v,e1,e2) -> "Let " ^ v ^ " = " ^ string_of_expression e1 ^ " in \n(" ^string_of_expression e2 ^")"
+ | Fun (s,e) -> "Function " ^ s ^ " = (" ^ string_of_expression e ^")"
| App (f,arg) -> "("^string_of_expression f ^" "^ string_of_expression arg^")"
- | Point (k,v) -> "Valeur du champ " ^ v^ " de "^ k ^""
- | LengthSet s -> (match s with
- | Set s' -> "Taille de "^string_of_expression s ^ " : " ^ string_of_int (length_set s')
- | Var _ -> "Taille du set "^string_of_expression s
- | _ -> "Pas un set")
- | PushSet (e,s)-> (match s with
- | Set s' -> "Push "^string_of_expression e ^ " dans le set " ^ string_of_expression s ^ " : " ^ string_of_expression (Set(push s' e))
- | Var _ -> "Push "^string_of_expression e ^ " dans le set " ^ string_of_expression s ^ " : "
- | _ -> "Pas un set")
+ | Point (k,v) -> "value " ^ v^ " of "^ k ^""
| PatternMatching (m,l) -> "match "^string_of_expression m^" with \n | "^ String.concat "\n | "(List.map (fun e -> match e with |
e1,e2 -> string_of_expression e1 ^" => "^string_of_expression e2 )
l)^ "\nend"
| Cons (head,tail) -> string_of_expression head ^ " :: " ^ string_of_expression tail
-(**[get_param f] retourne la liste des paramtre d'une application de fonction,
- si un des parametre et aussi une application de fonction, cela retournera les parametre de la deuxieme application
- @param f [expr]
- @return [expr list]*)
-let rec get_param (f:expr) : expr list=
- match f with
- | App(f',Var v)-> Var v:: get_param f'
- | App(f',v)-> get_param v @ get_param f'
- | _-> []
-
-let string_of_synchro (s:synchro) : string =
- match s with
- | Fsync -> "Full Synchro"
- | Ssync -> "Semi Synchro"
- | Async -> "Asynchro"
-
let string_of_espace (e:space) : string =
match e with
| R -> "R"
@@ -313,47 +248,7 @@ let string_of_color (c : color) : string =
| Purple -> "Purple"
| Orange -> "Orange"
-let string_of_sensor (s : sensor) : string =
- match s with
- | Range r -> (match r with
- | Full -> "Range Full"
- | Limited x -> "Range Limité a : " ^ string_of_expression x
- | K_rand(x,y) -> "Range K_rand limité a : " ^ string_of_expression x ^ " et k = " ^ string_of_expression y
- | K_enemy(x,y) -> "Range K_enemy limité a : " ^ string_of_expression x ^ " et k = " ^ string_of_expression y)
- | Multi m -> (match m with
- | No -> "Multiplicity Aucune multiplicité"
- | Weak_Local -> "Multiplicity Faible local"
- | Strong_Local -> "Multiplicity Forte local"
- | Weak_Global -> "Multiplicity Faible global"
- | Strong_Global -> "Multiplicity Forte global")
- | Opacity o -> (match o with
- | Opaque -> "Opacity Opaque"
- | Transparent -> "Opacity Transparent")
- | Custom (s,f) -> "Fonction de degradation du champ " ^ s ^" : "^(match f with Str f' -> f'
- | Fun f' -> string_of_expression f')
-let rec string_of_value (v : value) : string =
- match v with
- | Empty -> "None"
- | Int i -> string_of_int i
- | String s -> s
- | Float f -> string_of_float f
- | Liste l -> "[" ^String.concat "; " (List.map string_of_value l) ^"]"
- | Light l -> (match l with
- | Intern c -> "Lumiere interne avec couleur :" ^ String.concat ", " (List.map string_of_color c)
- | Extern c ->"Lumiere externe avec couleur :" ^ String.concat ", " (List.map string_of_color c)
- | All c ->"Lumiere visible par tous avec couleur :" ^ String.concat ", " (List.map string_of_color c)
- )
-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_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) ^"]"
-let string_of_role (r : int*string) : string=
- match r with
- | id,role -> "Le robot d'id " ^ string_of_int id ^" a comme role : " ^role
+
let string_of_rigidity (r: rigidity) : string =
match r with
@@ -362,7 +257,7 @@ let string_of_rigidity (r: rigidity) : string =
-(** [info_sync i] verifie qu'une information est une information sur la synchronisation
+(** [info_sync i] verifies that an information is information on synchronization
@param i information
@return bool *)
let info_sync (i : information):bool =
@@ -370,7 +265,7 @@ let info_sync (i : information):bool =
| Sync _ -> true
| _ -> false
-(** [info_espace i] verifie qu'une information est une information sur l'espace
+(** [info_espace i] verifies that information is information about space
@param i information
@return bool *)
let info_space (i : information):bool =
@@ -379,9 +274,6 @@ let info_space (i : information):bool =
| _ -> false
-
-
-
(*GRAPH*)
module Node = struct
type t = expr
@@ -404,6 +296,9 @@ module Topological = Graph.Topological.Make(G)
type edge =
| Nolab of (expr * expr)
+(**[graph_from_edges el] creates a graph from a list of edges [el]
+ @param edge [list]
+ @return [G.t]*)
let graph_from_edges (el : edge list)=
let g = G.create () in
let nolab = fun (x, y) ->
@@ -418,81 +313,54 @@ let graph_from_edges (el : edge list)=
in add_edge el;
g
-
- let png_from_graph g =
+(**[png_from_graph g name] generates a png file of the graph [g]
+ @param g [G.t]
+ @param name [string] png file name
+ @return[unit]*)
+let png_from_graph g name=
let graph = G.fold_vertex (fun v acc ->
let succs = List.map string_of_expression (G.succ g v)in
let v' = string_of_expression v in
let edges = List.fold_left (fun acc s ->
-
+
acc ^ "\"" ^ v' ^ "\" -> \"" ^ s ^ "\";\n") "" succs in
acc ^ "\"" ^ v' ^ "\";\n" ^ edges
) g "" in
let dot = "digraph G {\nrankdir=LR;\nranksep=1;\n" ^ graph ^"\nsplines=true;\noverlap=false; "^"}" in
- let oc = open_out "graph.dot" in
+ let oc = open_out ("./generate/"^name^"_measure.dot") in
Printf.fprintf oc "%s\n" dot;
close_out oc;
- ignore (Sys.command "dot -Tpng graph.dot -o graph.png")
-
- (**[assign_heigth g ] retourne la liste d'association phase,poids de phase. Le poids de phase est déduit de l'ordre
- topologique de la phase
- @param G.t le graphe dans le quel il faut attribuer les poids aux sommets
- @return (expr * int) list *)
- let assign_height (g : G.t) : (expr * int) list =
- (*let total_nodes = G.nb_vertex g in*)
- let rec assign_order nodes counter order =
- match nodes with
- | [] -> order
- | h :: tl -> assign_order tl (counter +1) ((h, counter) :: order)
- in
- let nodes = Topological.fold (fun node acc -> node :: acc) g [] in
- assign_order nodes 0 []
+ ignore (Sys.command ("dot -Tpng "^name^".dot -o ./generate/"^ name^"_measure.png"))
+
+(**[assign_heigth g] returns the phase, phase weight association list. The phase weight is deduced from the order
+ topology of the phase
+ @param G.t the graph in which we must assign the weights to the vertices
+ @return [(expr * int) list]*)
+let assign_height (g : G.t) : (expr * int) list =
+ (*let total_nodes = G.nb_vertex g in*)
+ let rec assign_order nodes counter order =
+ match nodes with
+ | [] -> order
+ | h :: tl -> assign_order tl (counter +1) ((h, counter) :: order)
+ in
+ let nodes = Topological.fold (fun node acc -> node :: acc) g [] in
+ assign_order nodes 0 []
(*/GRAPH*)
-type measure = Measure of int * G.t
-(* Une description c'est 1: description de l'environnement et des capacites des robot
- 2: robogram *)
+type measure = Measure of G.t
+(* A description is 1: description of the environment and the robot's capabilities
+ 2: robogram which is the distributed algorithm
+ 3: a graph representing the measure*)
type description = Description of (information list) * (expr list) * measure
-
-
-let rec string_of_description (desc:description) : string =
- match desc with
- | Description (infos,robogram,_) ->
- "Description environnement:\n" ^String.concat "\n" (List.map string_of_information infos)
- ^"\nRobogram : \n " ^ String.concat "\n" (List.map string_of_expression robogram)
-
-
-and string_of_information (info: information) : string =
-match info with
-| Sync s -> "Sync: " ^ (string_of_synchro s)
-| Rigidity r ->(match r with
- | Rigide -> "Rigidity: Rigide"
- | Flexible d -> "Rigidity: Flexible d'une distance delta = " ^ string_of_expression d)
-
-| Space e -> "Espace: " ^ (string_of_espace e)
-| 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)
-| ActivelyUpdate a -> "Champ qui sont mise a jour par le robogram: " ^ String.concat ", " (List.map string_of_valretr a )
-| Share s ->"Share : " ^ (match s with
- |Fullcompass -> "Fullcompass"
- |Chirality -> "Chirality"
- |DirectionShare -> "Direction"
- |OneAxisOrientation ->"1-axis orientation")
-
-
-
-(** [check_description d] verifie que la description [d] possède bien les informations minimales
- attendu pour une description et que chaque type d'information soit unique
- (deux définition de l'espace le quel choisir ?...)
- @param [d] description à vérifier
- @return true si la description repond aux critères false sinon
- TODO: A finir/ utilisation de valeur par defaut si non fourni? pourquoi pas
+(**[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
@@ -506,9 +374,9 @@ let check_description (d : description) :bool =
else true
) ;;
-(**[get_sensors d] Renvoie la liste de sensors contenu dans la description [d]
+(**[get_sensors d] Returns the list of sensors contained in description [d]
@param description
- @return [sensor list]
+ @return [sensor list]
*)
let get_sensors (d : description) : sensor list =
match d with
@@ -516,7 +384,7 @@ let get_sensors (d : description) : sensor list =
Some (Sensors s) -> s
| _ -> raise(Failure("Error: Not find Sensors")))
-(**[get_robot d] Renvoie la liste des champs robot contenu dans la descritpion [d]
+(**[get_robot d] Returns the list of robot fields contained in the description [d]
@param description
@return [field list]*)
let get_robot (Description(d', _,_) : description) : field list =
@@ -524,7 +392,7 @@ let get_robot (Description(d', _,_) : description) : field list =
Some (Robot r) -> r
| _ -> raise(Failure("Error: Not find Robot"))
-(**[get_activelyup d] Renvoie la liste des string correspondant aux champs mis à jour par le robogram
+(**[get_activelyup d] Returns the list of strings corresponding to the fields updated by the robogram
@param description
@return [string list] *)
let get_activelyup (d : description) : string list =
@@ -533,10 +401,10 @@ let get_activelyup (d : description) : string list =
Some (ActivelyUpdate a) -> List.map string_of_valretr a
| _ -> 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é
- @param [r] field list correspondant au robot dans le quel on verifie [s]
- @return true si [s] n'est pas custom ou qu'il est custom et qu'il est contenu dans [r]
+(** [check_sensor s r] verifies that a sensor [s] is indeed declared in the robot [r], or that it is not a custom sensor
+ @param [s] sensor to be checked
+ @param [r] field list corresponding to the robot in which we check [s]
+ @return true if [s] is not custom or it is custom and contained in [r]
*)
let check_sensor (s: sensor) (r:field list):bool =
let only_public flist = List.filter (fun x -> match x with Public _ -> true| _-> false) flist in
@@ -545,16 +413,16 @@ let check_sensor (s: sensor) (r:field list):bool =
| Custom (s',_)-> List.exists (fun (x,_) -> x = s') (field_to_pair (only_public r))
| _ -> true
-(** [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*)
+(** [check_sensors_desc d] checks that the list of sensors in the description matches robot sensors
+ @param d description in which we check its list of sensors with its robot declaration (field list)
+ @return [true] if the sensors are custom and are in robot or if they are not 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 -> raise(Failure("Error : " ^(match x with |Custom (x',_)-> x' | _->"")^" is not declared public in robot"))
| _-> true
-(**[check_activelyup d] verifie que les champs renseignés dans activelyupdate soient déclarés dans robot
+(**[check_activelyup d] verifies that the fields entered in activelyupdate are declared in robot
@param d [description]
@return [bool]*)
let check_activelyup (d:description) :bool =
@@ -567,10 +435,10 @@ let check_activelyup (d:description) :bool =
| _-> 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 *)
+(**[check_light d] if there is internal light we check that it is not indicated in public
+ and if extern not in private
+ @param description [d] description of the world
+ @return bool true if no internal light in public *)
let check_light d : bool =
let rec check flist = (
fun x -> match x with
diff --git a/lib/coordonnee.ml b/lib/coordonnee.ml
deleted file mode 100644
index 694854651f24c4f3da25976b9c11d4288b4f9bc1..0000000000000000000000000000000000000000
--- a/lib/coordonnee.ml
+++ /dev/null
@@ -1,15 +0,0 @@
-type ('a,'b,'c) coord =
- | Coord1D of 'a
- | Coord2D of 'a * 'b
- | Coord3D of 'a * 'b * 'c
-
-let string_of_coord (string_of_a: 'a -> string)
- ?(f' = fun _ -> "")
- ?(f'' = fun _ -> "")
- (c:('a,'b,'c) coord) : string =
- match c with
- | Coord1D x -> string_of_a x
- | Coord2D (x,y) -> string_of_a x ^"; "^f' y
- | Coord3D (x,y,z) -> string_of_a x^"; "^f' y^"; "^f'' z
-
-
\ No newline at end of file
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index b499cb94a446f146c53f68aba032918870f52ff5..8362bea5ba5ff4bf7bebd2f64e18d126a348b360 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -7,9 +7,9 @@ open Coq
let newline =RawCoq([" "])
let proof_to_complete = [Comment("Proof");RawCoq(["Admitted."])]
-(** [get_nb_byz infos] retourne le nombre de byzantins désirés
- @param information list correspondant à la description du monde
- @return [int]*)
+(** [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
@@ -19,12 +19,11 @@ let get_nb_byz (infos: information list) : int =
| _ -> 0
-(** [get_val_ret infos] retourne le type de retour du robogram
- @param information list correspondant à la description du monde
- @return [string] correspondant a location ou direction POUR LE MOMENT
- *)
+(**[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 =
- (* Seulement location et direction pour le moment, TODO: Implementation Light*)
+ (* TODO: Implementation Light*)
let rec locdir valret = match valret with
| Location::_ -> "location"
| Direction::_ -> "direction"
@@ -37,9 +36,9 @@ 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)*)
+(**[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
@@ -47,9 +46,9 @@ let get_space (infos : information list) : string =
| 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)*)
+(**[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
@@ -57,18 +56,18 @@ let get_rigidity (infos : information list) : string =
| 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 *)
+(**[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] 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*)
+(**[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
@@ -78,8 +77,8 @@ let multi (s:sensor list) : bool =
-(** [expr_to_coq r] retourne une expression de type Formula.t (ast pour écrire du coq PCourtieux) correspondante à l'expression r donnée
- @param expr expression de l'ast du DSL a convertir en Formula.t
+(** [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 =
@@ -109,9 +108,9 @@ let rec expr_to_coq (r : expr) : Formula.t =
| Set s -> Raw("(" ^ String.concat "," (set_to_coq s) ^")")
| Point (m,f) -> let c = List.assoc_opt m Module.correspondance in
(match c with
- |None -> raise(Failure("Probleme "^m^" inconnu"))
+ |None -> raise(Failure("Problem: "^m^" unknow"))
|Some x -> (match List.assoc_opt f x with
- | None -> raise(Failure("Probleme"^m^"."^f^" inconnu"))
+ | None -> raise(Failure("Problem "^m^"."^f^" unknow"))
| Some x' -> x')
)
| _ -> Raw("Not Implemented")
@@ -121,7 +120,7 @@ let rec expr_to_coq (r : expr) : Formula.t =
| Some (s',e) -> string_of_expression e :: set_to_coq s'
-(**[instance_R_R2 s d] genere le code coq pour instancer R et R2
+(**[instance_R_R2 s d] generates the coq code to instance R and R2
@param space s
@param information list d
@return [stmt list]
@@ -140,7 +139,7 @@ let instance_R_R2 (s:space) (d: information list): stmt list =
::Instance("VS",Cst("RealVectorSpace location"),Cst(s'^"_VS"))
::Instance("ES",Cst("EuclideanSpace location"),Cst(s'^"_ES"))::path
-(**[instance_Ring n] genere le code coq pour instancier un Ring
+(**[instance_Ring n] generates the coq code to instantiate a Ring
@param int n
@return [stmt list]*)
let instance_ring (n:int) : stmt list =
@@ -151,8 +150,8 @@ let instance_ring (n:int) : stmt list =
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] retourne une liste de stmt permettant de generer le code coq pour instancier l'espace s
- @param space [s] Ã instancier pour le moment seulement R, R2, Ring
+(**[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 =
@@ -165,9 +164,9 @@ let instance_space (s: space) (d : information list): stmt list =
in
s'@[]
-(**[instane_updfunc_rigid valret] retourne le code coq pour instancier la fonction d'update
- @param string valeur de retour du robogram
- @return stmt
+(**[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
@@ -185,9 +184,9 @@ let instance_updfunc_Flexible (d:expr) (valret : string): stmt list =
::[]
-(**[instance_rigidity r valret] retourne une liste de stmt permettant de generer le code coq pour instancier la rigidite des deplacements
- @param rigidity rigidite [r] Ã instancier
- @param valret valeur de retour du robogram
+(**[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) (world: information list): stmt list =
@@ -202,10 +201,10 @@ let instance_rigidity (r:rigidity) (valret : string) (world: information list):
::instance_updfunc_Flexible d valret
-(**[instance_info fl] retourne une liste de stmt permettant de generer le code coq pour instancier de l'état du robot
- @param field list list de champs à instancier
+(**[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
@@ -218,10 +217,10 @@ 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_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)
+(**[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]))
@@ -231,10 +230,10 @@ let instance_byzantine (x : int ) : stmt list =
Instance("MyRobots",Cst("Names"),App(Cst("Robots"),[Raw("("^string_of_int (x-1) ^ " * n)");Cst("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
+(**[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
@@ -242,8 +241,8 @@ let instance_sync (s : synchro) : stmt list =
| _ -> [RawCoq([ "Instance IC : inactive_choice unit := NoChoiceIna.";
"Instance InaFun : 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
+(**[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)
@@ -255,8 +254,8 @@ let instance_sensors (s:sensor list) : stmt list =
::[]
else Instance("Obs",Cst("Observation"),Cst(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
+(**[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
@@ -264,8 +263,8 @@ let require_rigidity (r: rigidity) :stmt =
| Rigide -> Require(true,["Pactole.Models.Rigid";"Pactole.Models.Similarity"])
-(**[require_space s] retourne un stmt permettant de generer le require pour l'espace [s]
- @param space [s] est l'espace renseigné dans la description du monde
+(**[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
@@ -274,8 +273,8 @@ let require_space (s: space) : stmt =
| ZnZ _ -> Require(true,["Pactole.Spaces.Ring";"Reals";"Pactole.Spaces.Isomorphism"])
| _ ->raise(Failure ("Not implemanted"))
-(**[require_multi s] retourne un stmt permettant de generer le require pour la multiplicité
- @param sensor list [s] est la liste des sensors renseignée dans la description du monde permettant de recupérer la multiplicité
+(**[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"
@@ -284,15 +283,15 @@ let require_multi (s: sensor list) : stmt =
then Require(true,["Pactole.Observations."^limited^"MultisetObservation"])
else Require(true,["Pactole.Observations."^limited^"SetObservation"])
-(**[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 *)
+(**[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 []
-(**[genereate_requires world] retourne une liste de stmt permettant de generer les require import necessaire en fonction du [world]
- @param information list [world] correspond à la description du monde
+(**[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 =
@@ -305,8 +304,8 @@ let generate_requires (world : information list) : stmt list =
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
- @param information list [world] correspond à la description du monde
+(**[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
@@ -322,10 +321,10 @@ let valret = get_val_ret world in
| _ -> genworld t) in
(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
- @param information list [d] permet de recupéré la valeur de retour du robogram TODO: a retravailler
- @return stmt list*)
+(**[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 valretcoq = if get_rigidity d = "Flexible" then "(path " ^ valret ^ ")" else valret in
@@ -340,7 +339,7 @@ let generate_robogram (r : expr list) (d: information list) : stmt list =
| [] -> Def ("Robogram_pgm (s : observation)",Raw(valretcoq),Raw("[]")) ::[]
-(**[generate_or l] retourne la formule or a partir d'une liste de string
+(**[generate_or l] returns the formula "or" from a list of string
@param string list
@return [Formula.t]*)
let rec generate_or l=
@@ -349,13 +348,16 @@ match l with
| h::tl -> Or(Cst(h),generate_or tl)
| _ -> Cst("")
+(**[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 =
Ast.G.fold_vertex (fun v acc ->
let func_name = string_of_expression v ^"_lt (config : configuration)" in
Def(func_name,Raw("nat"),Raw("(* To_Complete *)"))::acc
) g []
-(**[generate_lemmas g] retourne la liste de stmt correspondant aux lemmes extrait du graph 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) =
@@ -372,6 +374,9 @@ let generate_lemmas (g : Ast.G.t) : (stmt list * string list) =
(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
@@ -381,16 +386,14 @@ let rec aux l =
in
aux (Ast.assign_height g)
- (* List.map (fun (phase,height) -> Comment(string_of_expression phase ^" poid = " ^ string_of_int height) ) height_phase *)
-
-
-(**[generate_measure m] retourne la liste de stmt correspondant a la generation de la mesure
+(**[generate_measure m] returns the list of stmt corresponding to the generation of the measurement
@param m [measure]
@return [stmt list] *)
-let generate_measure (Measure(i,g): measure) : stmt list =
- let ret = String.concat "*"(List.init i (fun _ ->"nat")) in
+
+let generate_measure (Measure(g): measure) (name_png : string) : stmt list =
+ let ret = "nat*nat" in
let to_change = generate_if_measure g in
- Ast.png_from_graph g;
+ 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
@@ -401,10 +404,10 @@ let generate_measure (Measure(i,g): measure) : stmt list =
RawCoq(["Instance measure_compat : Proper (equiv ==> Logic.eq) measure."])::proof_to_complete
-(**[generate_coq d s] genere a partir de la description complete (world,robogram,measure) [d] l'instance coq nommé [s]
- @param description d
+(**[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] *)
+ @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)) &&
@@ -412,7 +415,7 @@ let generate_coq (Description(d,r,m) : description) (section_name : string)=
then
let file_out = open_out ("./generate/"^section_name^".v") in
let format_file = Format.formatter_of_out_channel file_out in
- let section = Section(section_name,(generate_instances d)@newline::generate_robogram r d@newline::generate_measure m) in
+ let section = Section(section_name,(generate_instances d)@newline::generate_robogram r d@newline::generate_measure m section_name) in
Format.fprintf format_file "%a@." Coq.pretty_l ((generate_requires d)@[section]);
close_out file_out;
print_endline(section_name^".v is generated")
diff --git a/lib/interface.ml b/lib/interface.ml
index 29665b4178232271e697e04b9eb83b88175b7da4..8479d2677dfe75c625617a0a1e37cc5c67dfa964 100644
--- a/lib/interface.ml
+++ b/lib/interface.ml
@@ -1,10 +1,10 @@
-(** [parse f filename] est une fonction qui prend en paramètres une fonction [f] et une chaîne de caractères [filename].
- Elle utilise un analyseur lexical pour convertir la chaîne de caractères en un flux de tokens,
- puis utilise la fonction [f] pour analyser les tokens et renvoyer le résultat.
- Si une erreur de parsing se produit, une exception de type [Failure] est levée avec le message "Parse error".
- @param [f] fonction d'analyse des tokens
- @param [filename] string correspondant au chemin du fichier a parser.
- @return L'arbre syntaxique résultant du parsing.*)
+(** [parse f filename] is a function which takes a function [f] and a character string [filename] as parameters.
+ It uses a lexical analyzer to convert the character string into a stream of tokens,
+ then use the [f] function to parse the tokens and return the result.
+ If a parsing error occurs, an exception of type [Failure] is thrown with the message "Parse error".
+ @param [f] token analysis function
+ @param [filename] string corresponding to the path of the file to be parsed.
+ @return The syntactic tree resulting from the parsing.*)
let parse_file f filename =
let in_channel = open_in filename in
diff --git a/lib/lexer.mll b/lib/lexer.mll
index a0aca650c88252e0da05709f951fee0fa00ec084..620667eb36d3a1e81f439f827dd9abf0445fd12f 100644
--- a/lib/lexer.mll
+++ b/lib/lexer.mll
@@ -24,8 +24,8 @@ rule token = parse
| "Rm" {RM}
| "R2" {R2}
| "R2m" {R2M}
- | "Ring" {ANNEAU}
- | "Byzantine" {BYZANTINE}
+ | "Ring" {RING}
+ | "Byzantine" {BYZANTINE}
| "Sensors" {SENSORS}
| "Robot" {ROBOT}
| "Roles" {ROLES}
@@ -43,10 +43,6 @@ rule token = parse
| "Strong Local" {STRONGL}
| "Weak Global" {WEAKG}
| "Strong Global" {STRONGG}
- (*| "Memory" {MEMOIRE}
- | "Oblivious" {OBLIVIOUS}
- | "Finite" {FINITE}
- | "Infinite" {INFINITE} *)
| "Light" {LIGHT}
| "Internal" {INTERNE}
| "External" {EXTERNE}
@@ -87,7 +83,7 @@ rule token = parse
| "=>" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; IMPLICATION}
| "<=>" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; EQUIVALENCE}
| "let" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; LET}
- | "=" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ;AFFECT}
+ | "=" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; AFFECT}
| "in" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; IN}
| ":=" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; IS}
| '+' {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; PLUS}
@@ -96,8 +92,8 @@ rule token = parse
| '/' {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; DIV}
| "&&" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; AND}
| "||" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; OR}
- | '>' {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ;SUP}
- | '<' {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ;INF}
+ | '>' {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; SUP}
+ | '<' {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; INF}
| "==" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; EQUAL}
| "!=" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; DIFF}
| "!" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; NOT}
diff --git a/lib/parser.mly b/lib/parser.mly
index 60f3cc88a321c5345b5cb13fe1c554e008f1d0a3..6976383770c9efa8b366aed40c8fa89aafa1006d 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -7,14 +7,13 @@
%token <float> FLOAT
%token IS
%token SYNC FSYNC SSYNC ASYNC
-%token SPACE R RM R2 R2M ANNEAU
+%token SPACE R RM R2 R2M RING
%token BYZANTINE
%token SENSORS
%token RANGE FULL LIMITED K_RAND K_ENEMY
%token MULTI NO_MEM WEAKL STRONGL WEAKG STRONGG
%token LIGHT INTERNE EXTERNE RED BLUE YELLOW GREEN PURPLE ORANGE
%token OPACITY OPAQUE TRANSPARENT
-/*%token MEMOIRE OBLIVIOUS FINITE INFINITE*/
%token SHARE FULLCOMPASS CHIRALITY ONEAXEORIEN
%token RIGIDITY RIGIDE FLEXIBLE
%token COLON BRACKETOPEN BRACKETCLOSE SEMICOLON PARENOPEN PARENCLOSE COMMA
@@ -42,7 +41,7 @@
%left OR
%left AND
%nonassoc NOT
-%right VARIABLE KEYWORD PARENOPEN INT FLOAT BOOLEAN /*regle conflit f = appfunc arg = argmument { App(f,arg)} ET id reduit en */
+%right VARIABLE KEYWORD PARENOPEN INT FLOAT BOOLEAN
%type <Ast.description> description
@@ -65,11 +64,11 @@ information :
| RIGIDITY IS r = rigidite {[Rigidity r]}
/* Space := e */
| SPACE IS e = espace {[Space e]}
- /* Byzantin := entier*/
+ /* Byzantine := integer*/
| BYZANTINE IS i = INT {[Byzantines (Number i)]}
- /* Byzantin := [1;2;8;9] liste d'id correspondant aux bizantins*/
+ /* Byzantine := [1;2;8;9] list of ids corresponding to Byzantines*/
| BYZANTINE IS id = list_int {[Byzantines (Id id)]}
- /* Roles := 0 : Compagnon; 5 : Byzantin*/
+ /* Roles := 0 : Compagnon; 5 */
| 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]}
@@ -94,7 +93,7 @@ valret :
| LOCATION {Location}
| DIRECTION {Direction}
-/*liste des champs de robots*/
+/*list of robot fields*/
list_field :
| PRIVATE COLON l1 = separated_list(SEMICOLON,elements_private) PUBLIC COLON l2 = separated_list(SEMICOLON,elements_public) {l1@l2}
elements_private :
@@ -121,24 +120,18 @@ ints :
| ASYNC {Async}
%inline espace :
- /* Espace R */
+ /* Space R */
| R {R}
- /*Esapce R en millefeuille*/
+ /* Space R millefeuille*/
| RM {Rm}
- /*Espace RxR */
+ /* Space RxR */
| R2 {R2}
- /*Espace RxR en millefeuille*/
+ /* Space RxR millefeuille*/
| R2M {R2m}
- /*Anneau ZnZ avec n donnée*/
- | ANNEAU n = INT {ZnZ(n)}
- | ANNEAU {ZnZ(0)}
-/*
-%inline capacity :
- /*(Lumiere : l) */
-/* | LUMIERE COLON l = lights {Lights l}
- /*(Memoire : m)*/
-/* | MEMOIRE COLON m = memoire {Memory m}
-*/
+ /*Ring Z/nZ */
+ | RING n = INT {ZnZ(n)}
+ | RING {ZnZ(0)}
+
%inline sensor :
/*Multi : m*/
| MULTI COLON m = multi {Multi m}
@@ -170,11 +163,11 @@ value :
lights:
- /*Nombre de lumiere interne -> visible que par le robot*/
+ /*Internal light -> visible only to the robot*/
| INTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,color) BRACKETCLOSE {Light(Intern i)}
- /*Nombre de lumiere externe -> visible que par les autres robots*/
+ /*External light -> visible only to other robots*/
| EXTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,color) BRACKETCLOSE {Light(Extern i)}
- /*Nombre de lumiere visible par tous */
+ /*Light visible to all*/
| FULL LIGHT BRACKETOPEN i = separated_list(SEMICOLON,color) BRACKETCLOSE {Light(All i)}
%inline color :
@@ -186,32 +179,32 @@ lights:
| ORANGE {Orange}
%inline range :
- /*Range maximal */
+ /* Full Range */
| FULL {Full}
- /*Range Limité a une distance r*/
+ /* Limited Range to r */
| LIMITED r = VARIABLE {Limited (Var r)}
- /*Limite a une distance r et k ,un nombre random, de robot au dela de r*/
+ /* Limit to a distance r and k, a random number, of robot beyond r */
| K_RAND r = VARIABLE k = VARIABLE {K_rand(Var r,Var k)}
- /*Limite a une distance r et k ,un nombre choisie par l'ennemie, de robot au dela de r*/
+ /* Limit to a distance r and k, a number chosen by the enemy, from robot beyond r */
| K_ENEMY r = VARIABLE k = VARIABLE {K_enemy(Var r,Var k)}
%inline multi :
- /* Pas de multiplicité */
+ /* No multiplicity */
| NO_MEM {No}
- /*Multiplicité faible local -> 1 robot ou des robots la ou je suis*/
+ /* Weak local multiplicity -> 1 robot or robots where I am */
| WEAKL {Weak_Local}
- /*Multiplicité forte local -> connait le nombre de robot la ou je suis*/
+ /* String local multiplicity -> knows the number of robots where I am */
| STRONGL {Strong_Local}
- /* Multiplicité faible global -> 1 robot ou des robots partout*/
+ /* Weak global multiplicity -> 1 robot or robots everywhere */
| WEAKG {Weak_Global}
- /*Multiplicité forte local -> connait le nombre de robot partout*/
+ /*Strong local multiplicity -> knows the number of robots everywhere*/
| STRONGG {Strong_Global}
%inline opacite:
- /*Autres robots ne peuvent pas voir derriere lui*/
+ /* Other robots can't see behind him */
| OPAQUE {Opaque}
- /*Autres robots peuvent voir derriere lui*/
+ /* Other robots can see behind him */
| TRANSPARENT {Transparent}
%inline rigidite:
@@ -224,8 +217,6 @@ lights:
| DIRECTION {DirectionShare}
| ONEAXEORIEN {OneAxisOrientation}
-
-
robogram:
| expression * {$1}
@@ -238,17 +229,17 @@ expression:
/*e1 binop e2 avec binop appartient a {+ ; - ; * ; / ; || ; &&; == ; != ; < ; > ;*/
| e1 = expression op = binop e2 = expression {BinOp(e1,op,e2)}
| NOT expression {Not $2}
- /*let nom_variable = e in */
+ /*let name_variable = e in */
| LET v = VARIABLE AFFECT e = expression IN e2=expression {Let(v,e,e2)} %prec AFFECT
- /*nom_variable = e*/
+ /*name_variable = e*/
| v = VARIABLE; AFFECT e = expression {Affectation(v,e)}
/*[a;z;e;r;t....]*/
| PARENOPEN s = set PARENCLOSE {Set s}
| MATCH PARENOPEN i= appfunc PARENCLOSE WITH p = patternmatch END {PatternMatching(i,p)}
| MATCH i= id WITH p = patternmatch END {PatternMatching(i,p)}
| f = deffun {f}
- | f = appfunc {f} %prec VARIABLE /*si conflit : si on peut resoudre a droite on le fait sinon shift */
- | i = id {i} %prec VARIABLE /*si conflit : si on peut resoudre a droite on le fait sinon shift */
+ | f = appfunc {f} %prec VARIABLE /*if conflict: if we can resolve it on the right we do it otherwise shift */
+ | i = id {i} %prec VARIABLE
constant :
/*booleen*/
@@ -278,7 +269,7 @@ id :
| x = KEYWORD POINT e = VARIABLE {Point(x,e)}
set :
- | e = expression SEMICOLON s = set {Some(s,e)}
+ | e = expression COMMA s = set {Some(s,e)}
| e = expression {Some(Vide,e)}
| {Vide}
@@ -307,10 +298,8 @@ pattern :
| v = VARIABLE COLON COLON e = pattern {Cons(Var v,e)}
| PARENOPEN s = set PARENCLOSE COLON COLON e = pattern {Cons(Set s,e)}
-
-
measure:
- | PARENOPEN l = separated_list(COMMA,VARIABLE) PARENCLOSE el = edge_list {Measure(List.length l,graph_from_edges (List.flatten el))}
+ | el = edge_list {Measure(graph_from_edges (List.flatten el))}
edge :
| v1 = sommet ARROW v2 = sommet {[Nolab(v1,v2)]}