diff --git a/Readme.md b/Readme.md
index c9c7fe228cca8d812178588771479678ec287f54..6eab4bf19f18f45ce4f5c39b0a6d804e053570fe 100644
--- a/Readme.md
+++ b/Readme.md
@@ -1,5 +1,12 @@
# DSL pour Robotique en Essaim
+### Environnement
+ Ocaml 4.13
+ Dune 3.15
+ Coq 8.15
+
+
+
### Valeurs possibles pour chaque éléments de la description de l'environnement :
- Sync := Permet de définir le type de synchronisation.
@@ -14,68 +21,84 @@ Sync := ASYNC
- 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
+ - mR X -> mille-feuille d'une dimension, correspondant par exemple à X routes parallèles, X peut ne pas être renseigné.
- R2 -> plan
- - R2m -> millefeuille de plan, correspondant a des plan sur plusieurs etages
- - Ring n -> correspond a un anneau Z/nZ
+ - mR2 X -> mille-feuille de plan, correspondant à des plan sur X étages, X peut ne pas être renseigné.
+ - Ring n -> correspond a un anneau Z/nZ, n peut ne pas être renseigné.
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 à la proportion de Byzantins
+ - x -> un entier correspondant à la proportion de Byzantins tel que n/x avec n le nombre de robot
- [id1;id2;id3] -> liste d'entier correspondant aux id des Byzantins
+
+exemple :
```
-exemple : Byzantine := [1;2;7;8]
+Byzantine := 5
```
-- Rigidity: Défini si le robot peut etre interrompu lors de son déplacement
+
+- Rigidity: Défini si le robot peut être interrompu lors de son déplacement
- Rigide -> Le robot finit sont déplacement avant de recommencer un cycle LCM
- - Flexible f -> f est une variable est correspond a la distance minimal que le robot va parcourir avant de pouvoir etre interrompu et commencer un nouveau cycle LCM
+ - Flexible f -> f est une variable est correspond a la distance minimal que le robot va parcourir avant de pouvoir être interrompu et commencer un nouveau cycle LCM
+
```
Rigidity := Flexible delta
```
-Couleur : Red; Blue; Yellow; Green; Purple; Orange
-- Robot := Permet de definir des champs privés et publiques pour le robot, il est necessaire de lister les éléments privés puis les éléments publiques
- - Private : Champ 1; Champ 2; ...
- - Public : Champ 3; Champ 4; ...
+- Robot := Permet de définir des champs privés et publiques pour le robot, il est nécessaire de lister les éléments privés puis les éléments publiques
+- Private : Champ 1; Champ 2; ...
+- Public : Champ 3; Champ 4; ...
+
+Pour la lumière :
+ - Internal Light
+ - External Light
+ - Full Light
+
+Les champs, ainsi que les couleurs des lumière sont au choix de l'utilisateur.
+
-Les champs sont définis par l'utilisateur, et peuvent prendre des valeurs ou non.
exemple :
+
```
-Robot := Private : Temperature; Coordonnee [5;1.8]
+Robot := Private : Temperature; Internal Light [Rouge;Noir]
Public : Id; Batterie
-```
+
+```
+
- 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
- - F Byzantinull -> Le robot à une range ilimité
+ - Full -> Le robot à une range illimité
- 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
+ - K_Rand d k -> range limité à un delta + capable de voir k robots au delà de delta choisie rand
+ - K_enemy d k -> range limité à un delta + capable de voir k robots au delà de delta choisie par un ennemie
- **Opacity**: Correspond à l'opacité des robots
- Opaque -> les robots derrières un autre robot ne sont pas visibles
- Transparent -> les robots derrières un autre robot sont visibles
- - **Multiplicity** : Correspond à la détection de la multiplicité et la ditance de detection
- - No -> les robots ne detectent pas la multiplicité
- - Weak -> les robots detectent si il y a 1 ou plusieurs robots
- - Strong -> les robots detectent le nombre exacte de robots
+ - **Multiplicity** : Correspond à la détection de la multiplicité et la distance de detection
+ - No -> les robots ne détectent pas la multiplicité
+ - Weak -> les robots détectent si il y a 1 ou plusieurs robots
+ - Strong -> les robots détectent le nombre exacte de robots
- Local -> detection a leur position
- Global -> detection sur toutes les positions observés
On peut aussi utiliser les capacités/champs renseignés en **PUBLIC** dans Robot
-
-exemple:
+
+exemple:
```
-Sensors := Range : Limited 5; Multi : Weak Local;
+Sensors := Range : Limited r;
+ Multi : Weak Local;
Opacity : Opaque;
Batterie : (fun x -> if x > 50 then 100 else 50);
```
-- ActivelyUpdate := Permet de définir les champs de robots qui vont pouvoir etre modifié par le robogram, Location est par defaut.
+- ActivelyUpdate := Permet de définir les champs de robots qui vont pouvoir être modifié par le robogram, Location est par défaut, mais doit être indiqué si il y a plus d'un champs mis à jour
+
```
-ActivelyUpdate := Light
+ActivelyUpdate := Location;Light
```
diff --git a/bin/main.ml b/bin/main.ml
index 7cbc768608d8d673c151523899107ff2b9face39..44640ddeab306f5d1dbbf8d93cc569dbd9e3a3ac 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -1,10 +1,41 @@
open Dsl
-(*let repo = "./sourcegenerate";;
-let files =Array.to_list (Sys.readdir repo);;
-print_endline(String.concat "; " files);;
+
+
+let usage = "Usage: dsl filename_dsl [-proof filename_proof] [-type filename_type] [-r repository_out] [-n] [-g] [-h] \n -n : don't overwrite type file \n -g : generate png from graph"
+
+(** [parse_args argrs proof_name type_name owerwrite repo_gen] Parses the command line arguments and returns a tuple containing the parsed values or default value.
+ @param args string list: The list of command line arguments.
+ @param proof_name string: The name of the proof file.
+ @param type_name string: The name of the type file.
+ @param overwrite : A boolean indicating whether to overwrite the type file.
+ @param dir_gen string: The name of the output repository.
+ @return A tuple containing the parsed values or default value passed as an argument in thr first function's call: (proof_name, type_name, overwrite, repo_gen).
*)
+let rec parse_args args (proof_name : string) (type_name : string) (overwrite: bool) (dir_gen : string) (graph_gen:bool):(string * string * bool * string *bool)=
+ match args with
+ | "-proof" :: proof :: tl -> parse_args tl proof type_name overwrite dir_gen graph_gen
+ | "-type" :: type_ :: tl -> parse_args tl proof_name type_ overwrite dir_gen graph_gen
+ | "-n" :: tl -> parse_args tl proof_name type_name (not overwrite) dir_gen graph_gen
+ | "-r" :: dir :: tl -> parse_args tl proof_name type_name overwrite dir graph_gen
+ | "-g" :: tl -> parse_args tl proof_name type_name overwrite dir_gen (not graph_gen)
+ | "-h" :: _ -> print_endline usage; exit 0
+ | _ :: tl ->parse_args tl proof_name type_name overwrite dir_gen graph_gen
+ | [] -> (proof_name, type_name, overwrite,dir_gen,graph_gen)
+
+
+
-let gen (x : string) =
- Gencoq.generate_coq (Interface.parse_description x) (Filename.basename x);;
+(** [gen args] function that takes a string array [args] as input and generates Coq files based on the provided arguments.
+ @param args: string array, array of command line arguments
+ *)
+let gen (args : string array) =
+
+ if Array.length args < 2 then (print_endline usage; exit 0)
+ else
+ let list_args = Array.to_list args in
+ let name = args.(1) in
+ let (proof_name, type_name, overwrite,repo_gen, graph_gen) = parse_args list_args ((Filename.basename name)^"_proof") ((Filename.basename name)^"_world_type") true "./generate" false in
+ Gencoq.generate_coq_2files (Interface.parse_description name) (Filename.basename name) proof_name type_name overwrite repo_gen graph_gen
+ ;;
-gen Sys.argv.(1);;
+gen Sys.argv;;
diff --git a/lib/ast.ml b/lib/ast.ml
index c78bb1a65e21e470ad1ac723d1ab4a091b43b0e3..25549ae100cac09829cd759722fdb049d409c956 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -12,8 +12,6 @@ type binop =
| Inf
| Equal
| Diff
- | Impli
- | Equiv
(*tail::head au lieu de head::tail pour éviter les empilements inutiles
(((vide,x),y),z)
@@ -25,7 +23,7 @@ type 'a set =
type expr =
| None
- | Bool of bool
+ | Bool of bool
| Cst of int
| Cstf of float
| BinOp of expr * binop * expr
@@ -37,7 +35,7 @@ type expr =
| App of expr * expr
| Affectation of string * expr
| Set of expr set
- | Point of string * string
+ | Point of string * string *int (* int : line to raise error*)
| PatternMatching of expr * (expr * expr)list
| Cons of expr *expr
@@ -104,14 +102,14 @@ type color =
| Orange
-(* type light: List of colors
+(* type light: List of colors * line to raise error (int)
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 string list
- | Extern of string list
- | All of string list
+ | Intern of string list * int
+ | Extern of string list *int
+ | All of string list *int
(* type opacity:
@@ -214,18 +212,16 @@ let rec string_of_expression (e : expr) : string =
| Inf -> "("^string_of_expression(x) ^ " < " ^string_of_expression(y)^")"
| Equal -> string_of_expression(x) ^ " == " ^string_of_expression(y)
| Diff -> string_of_expression(x) ^ " != " ^string_of_expression(y)
- | Impli -> string_of_expression(x) ^ "->" ^string_of_expression(y)
- | Equiv -> string_of_expression(x) ^ " <-> " ^string_of_expression(y)
)
| Not b -> "!("^string_of_expression b^")"
| Var v -> v
| 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
+ | Affectation(v,e) -> v ^ " = " ^ string_of_expression e
| Set s -> string_of_set s string_of_expression
| 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) -> "value " ^ v^ " of "^ k ^""
+ | 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"
@@ -329,7 +325,7 @@ let graph_from_edges (el : edge list)=
@param g [G.t]
@param name [string] png file name
@return[unit]*)
-let png_from_graph g name=
+let png_from_graph g name dir =
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
@@ -338,10 +334,10 @@ let png_from_graph g name=
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 ("./generate/"^name^"_measure.dot") in
+ let oc = open_out (dir^"/"^name^"_measure.dot") in
Printf.fprintf oc "%s\n" dot;
close_out oc;
- ignore (Sys.command ("dot -Tpng ./generate/"^name^"_measure.dot -o ./generate/"^ name^"_measure.png"))
+ ignore (Sys.command ("dot -Tpng "^dir^"/"^name^"_measure.dot -o "^dir^"/"^ 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
@@ -362,19 +358,19 @@ let assign_height (g : G.t) : (expr * int) list =
module NodeMap = Map.Make(Node)
-(** [update_lowlink v w lowlink] met à jour la valeur de lowlink pour le noeud [v] en fonction du noeud [w]. *)
+(** [update_lowlink v w lowlink] updates the lowlink value for node [v] based on node [w].*)
let update_lowlink v w lowlink =
let v_lowlink = NodeMap.find v lowlink in
let w_lowlink = NodeMap.find w lowlink in
NodeMap.add v (min v_lowlink w_lowlink) lowlink
-(** [update_on_stack w on_stack] supprime le noeud [w] de la liste [on_stack]. *)
+(** [update_on_stack w on_stack] remove node [w] from list [on_stack]. *)
let update_on_stack w on_stack =
List.filter (fun v -> v <> w) on_stack
-(** [pop_stack v stack on_stack scc] retire les éléments de la pile jusqu'à atteindre le noeud [v].
- Cela met à jour [on_stack] en supprimant les noeuds retirés de la pile, et [scc] en ajoutant ces noeuds à la nouvelle composante fortement connexe.*)
+(** [pop_stack v stack on_stack scc] removes elements from the [stack] until reaching node [v].
+ This updates [on_stack] by removing nodes removed from the [stack], and [scc] by adding these nodes to the new strongly connected component.*)
let rec pop_stack v stack on_stack scc =
match stack with
| w :: rest -> if w <> v then pop_stack v rest (update_on_stack w on_stack) (w :: scc)
@@ -382,9 +378,9 @@ let update_lowlink v w lowlink =
| [] -> raise(Failure "Error: stack empty")
-(** [strongconnect v index stack indices lowlink on_stack sccs g] est la fonction qui effectue le parcours en profondeur pour trouver les composantes fortement connexes.
- Pour chaque successeur [w] de [v] dans le graphe [g], si [w] n'est pas encore visité, il est récursivement visité.
- Après avoir visité tous les successeurs, si [v] est une racine de SCC, tous les noeuds dans la pile jusqu'à [v] sont ajoutés à une nouvelle SCC.
+(** [strongconnect v index stack indices lowlink on_stack sccs g] is the function that performs the dfs to find strongly connected components.
+ For each successor [w] of [v] in graph [g], if [w] is not yet visited, it is recursively visited.
+ After visiting all successors, if [v] is a root of SCC, all nodes in the stack up to [v] are added to a new SCC..
*)
let rec strongconnect (g : G.t) (v:expr) (index:int) stack indices lowlink on_stack sccs =
let indices = NodeMap.add v index indices in
@@ -417,8 +413,8 @@ let rec strongconnect (g : G.t) (v:expr) (index:int) stack indices lowlink on_st
else
index, stack, indices, lowlink, on_stack, sccs
-(** [tarjan g] est la fonction principale qui initialise les structures de données et lance le parcours en profondeur.
- et renvoie la liste des composants fortements connexes*)
+(** [tarjan g] is the main function that initializes the data structures and initiates dfs .
+ and returns the list of strongly related components *)
let tarjan g =
(*Tarjan : *)
let _, _, _, _, _, sccs =
@@ -441,14 +437,14 @@ let tarjan g =
module G2 = Graph.Imperative.Digraph.ConcreteLabeled(SCC)(Edge)
- (**[string_of_expr_list expr_list] retourne une chaine de caractere à partir d'une liste d'expression tel que [[X;Y]] correspondant à : string_of_expression X, string_of_expression Y, .... *)
+ (**[string_of_expr_list expr_list] returns a character string from a list of expressions such as [[X;Y]] corresponding to: string_of_expression X, string_of_expression Y, .... *)
let string_of_expr_list expr_list =
let string_list = List.map string_of_expression expr_list in
String.concat ", " string_list
(**[png_from_graph2 g ] renvoie l'image au format png du graphe [g]
@param g de type [G2.t] graphe de liste de liste d'expression, composants fortement connexe *)
-let png_from_graph2 (g:G2.t) (name : string) :unit =
+let png_from_graph2 (g:G2.t) (name : string) (dir : string) :unit =
let graph = G2.fold_vertex (fun v acc ->
let succs = List.map string_of_expr_list (G2.succ g v)in
let v' = string_of_expr_list v in
@@ -457,20 +453,20 @@ let png_from_graph2 (g:G2.t) (name : string) :unit =
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 ("./generate/"^name^"_measure.dot") in
+ let oc = open_out (dir^"/"^name^"_measure.dot") in
Printf.fprintf oc "%s\n" dot;
close_out oc;
- ignore (Sys.command ("dot -Tpng ./generate/"^name^"_measure.dot -o ./generate/"^ name^"_measure.png"))
+ ignore (Sys.command ("dot -Tpng "^dir^"/"^name^"_measure.dot -o "^dir^"/"^ name^"_measure.png"))
-(** [scc_graph g] retourne le graphe G2.t correspondant au graphe de composants fortement connexe du graphe [g]
- en recupérant la liste des composants fortement connexe et en les ajoutant au graphe G2.t créé[scc_graph].
- Ensuite, la fonction itère sur chaque SCC et ajoute des arêtes entre les SCC en se basant sur le graphe original [g].
- Pour chaque sommet dans un SCC, elle itère sur ses successeurs et trouve le SCC auquel chaque successeur appartient.
- Si le SCC du sommet et le SCC du successeur sont différents, une arête est ajoutée entre les SCC correspondants dans [scc_graph].
+(** [scc_graph g] returns the graph G2.t corresponding to the strongly connected component graph of graph [g]
+ by retrieving the list of strongly connected components and adding them to the created G2.t graph[scc_graph].
+ Then the function iterates over each SCC and adds edges between the SCCs based on the original graph [g].
+ For each vertex in an SCC, it iterates over its successors and finds the SCC to which each successor belongs.
+ If the vertex SCC and the successor SCC are different, an edge is added between the corresponding SCCs in [scc_graph].
@param g [G.t]
- @return [scc_graph] de type [G2.t], le graphe des composants fortement connexe de [g] *)
+ @return [scc_graph] of type [G2.t], the strongly connected component graph of [g] *)
let scc_graph g =
let scc_list = tarjan g in
let scc_graph = G2.create () in
@@ -567,7 +563,7 @@ let check_light d : bool =
let rec check flist = (
fun x -> match x with
| [] -> true
- | Public (_,Light(Intern _))::_ | Private (_, Light(Extern _))::_ -> raise(Failure("Error light in wrong field"))
+ | Public (_,Light(Intern (_ ,line)))::_ | Private (_, Light(Extern (_ ,line)))::_ -> raise(Failure("Error line "^string_of_int line^" light in wrong field"))
| _::t-> check t
) flist
in
diff --git a/lib/coq.ml b/lib/coq.ml
index 24d7972ad97d886d44648ad2b38dc5703d9ffd8e..9067bb21bf8fbabfa6df15c5c440f9a0a00a3bdb 100644
--- a/lib/coq.ml
+++ b/lib/coq.ml
@@ -9,6 +9,8 @@ type stmt =
| VarMaxImplicit of string * Formula.t
| Hyp of string * Formula.t
| Lemma of string * Formula.t * stmt list (* tactics *)
+ | Parameter of string * Formula.t *Formula.t (* Module *)
+ | Parameterlem of string * Formula.t * stmt list (* Module *)
| InstanceLemma of string * Formula.t * stmt list (* tactics *)
| Def of string * Formula.t * Formula.t
| Notation of string * Formula.t
@@ -17,6 +19,9 @@ type stmt =
| Instance of string * Formula.t * Formula.t
| ExistingInstance of Formula.t
| Section of string * stmt list
+ | Module of string * stmt list
+ | ModuleType of string * stmt list
+ | ModuleImpType of string * string * stmt list
| Proof of stmt list
| Require of bool * string list (* bool = Import *)
| Import of string list
@@ -41,6 +46,10 @@ let rec pretty fmt st =
| Lemma(s,f,lst) ->
p fmt "@[<v 0>@[<hov 2>Lemma %s: %a.@]@,@[<v 2>Proof.@,%a@]@,Qed.@]"
s prtyf f (Pp.print_list Pp.brk pretty) lst
+ | Parameter(s,v,r) -> p fmt "@[<hov 2>@[<hov 2>Parameter %s:@ %a@] ->@ %a.@]"
+ s prtyf v prtyf r
+ | Parameterlem(s,f,_) -> p fmt "@[<v 0>@[<hov 2>Parameter %s: %a.@]"
+ s prtyf f
| InstanceLemma(s,f,lst) ->
p fmt "@[<v 0>@[<hov 2>Instance %s: %a.@]@,@[<v 2>Proof.@,%a@]@,Defined.@]"
s prtyf f (Pp.print_list Pp.brk pretty) lst
@@ -51,11 +60,17 @@ let rec pretty fmt st =
s prtyf ftyp prtyf struc prtyf f
| Fixpoint(s,ftyp,struc,f) -> p fmt "@[<hov 2>@[<hov 2>Fixpoint %s:@ %a@ { %a }@] :=@ %a.@]"
s prtyf ftyp prtyf struc prtyf f
- | Instance(s,ftyp,f) -> p fmt "@[<hov 2>@[<hov 2>Instance %s:@ %a@] :=@ %a.@]"
+ | Instance(s,ftyp,f) -> p fmt "@[<hov 2>@[<hov 2>#[export] Instance %s:@ %a@] :=@ %a.@]"
s prtyf ftyp prtyf f
| ExistingInstance(f) -> p fmt "@[<hov 2>@[<hov 2>Existing Instance %a.@]@]" prtyf f
| Section (s,lst) -> p fmt "@[<v 0>@[<v 2>Section %s.@,%a@]@\nEnd %s.@]"
s (Pp.print_list Pp.cut pretty) lst s
+ | Module (s,lst) -> p fmt "@[<v 0>@[<v 2>Module %s.@,%a@]@\nEnd %s.@]"
+ s (Pp.print_list Pp.cut pretty) lst s
+ | ModuleType (s,lst) -> p fmt "@[<v 0>@[<v 2>Module Type %s_type.@,%a@]@\nEnd %s_type.@]"
+ s (Pp.print_list Pp.cut pretty) lst s
+ | ModuleImpType (s,st,lst) -> p fmt "@[<v 0>@[<v 2>Module %s : %s.@,%a@]@\nEnd %s.@]"
+ s st (Pp.print_list Pp.cut pretty) lst s
| Proof (lst) -> p fmt "@[<v 0>@[<v 2>Proof.@,%a@]@\nEnd.@]"
(Pp.print_list Pp.cut pretty) lst
| Require (_,[]) -> ()
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 4cbe2ecbb9a55dedf49635267b6a15c3e3e31f6b..5bcbea0e23eccf3db34a85d6453e8e4544decf00 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -28,13 +28,13 @@ let get_val_ret (infos : information list) : string list =
| Location::tl -> "location" :: (locdir tl )
| Direction::tl -> "direction" ::(locdir tl)
| Str x ::tl -> if x = "Light" then "light" :: (locdir tl) else (locdir tl)
- | [] -> []
+ | [] -> ["location"]
in
- let valret = List.find_opt (fun x -> match x with |ActivelyUpdate _ -> true | _ -> false) infos
+ let valret = List.find (fun x -> match x with |ActivelyUpdate _ -> true | _ -> false) infos
in
match valret with
- | Some (ActivelyUpdate x) -> locdir x
- | _-> ["location"]
+ | ActivelyUpdate x -> locdir x
+ | _-> []
(**[get_space infos] returns the string corresponding to the space
@param information list corresponding to the description of the world
@@ -100,18 +100,16 @@ let rec expr_to_coq (r : expr) : Formula.t =
| Inf -> App(Cst "lt",[expr_to_coq x;expr_to_coq y])
| Equal -> App(Cst "eq",[expr_to_coq x;expr_to_coq y])
| Diff -> Infix(expr_to_coq x,"!=",expr_to_coq y)
- | Impli -> Infix(expr_to_coq x, "->", expr_to_coq y)
- | Equiv -> Infix(expr_to_coq x,"<->",expr_to_coq y)
)
| Cons (e1,e2) -> App(Raw("cons"), ([expr_to_coq e1;expr_to_coq e2]))
| Fun (s,e) -> Fun(Some s, expr_to_coq e)
| App (f,arg) -> App(expr_to_coq f, [expr_to_coq arg])
| Set s -> Set (set_to_coq s)
- | Point (m,f) -> let c = StringMap.find_opt m Module.correspondance in
+ | Point (m,f,l) -> let c = StringMap.find_opt m Module.correspondance in
(match c with
- |None -> raise(Failure("Problem: "^m^" unknow"))
+ |None -> raise(Failure("Problem line "^string_of_int l^": "^m^" unknow"))
|Some x -> (match StringMap.find_opt f x with
- | None -> raise(Failure("Problem "^m^"."^f^" unknow"))
+ | None -> raise(Failure("Problem line "^string_of_int l^": "^m^"."^f^" unknow"))
| Some x' -> x')
)
| _ -> Raw("Not Implemented")
@@ -216,14 +214,14 @@ 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
(match l with
- |Some(Light (x)) -> let l' = match x with | Intern p -> p |Extern p -> p | All p -> p in
+ |Some(Light (x)) -> let l' = match x with | Intern (p,_) -> p |Extern (p,_) -> p | All (p,_) -> p in
let l'' = String.concat " | " l' in
RawCoq(["Inductive light:= "^l''^"."])
::Instance("light_Setoid",Cst "Setoid light",Cst "eq_setoid light")
- ::RawCoq(["Instance light_EqDec : EqDec light_Setoid.";
+ ::RawCoq(["[export] Instance light_EqDec : EqDec light_Setoid.";
"(*Proof*) Admitted.";
"Definition info := (location * light)%type."])
- ::RawCoq(["Instance St : State info := AddInfo light (OnlyLocation (fun f => sigT (fun sim : similarity location => Bijection.section sim == f)))."])::[]
+ ::Instance("St",Cst"State info",Raw("AddInfo light (OnlyLocation (fun f => sigT (fun sim : similarity location => Bijection.section sim == f)))."))::[]
(*TODO: Le reste des info sont a faire*)
| _ ->RawCoq(["Definition info := (location)%type."])
::Instance("St",Raw("State location"),Raw("OnlyLocation (fun _ => True)")) ::[])
@@ -235,7 +233,7 @@ let instance_info (fl:field list) : stmt list =
let instance_byzantine (x : int ) : stmt list =
if x < 1 then
Instance("MyRobots",Cst("Names"),App(Cst("Robots"),[Cst("n");Int 0]))
- ::RawCoq(["Instance NoByz : NoByzantine.";"Proof using . now split. Qed."])
+ ::RawCoq(["#[export] Instance NoByz : NoByzantine.";"Proof using . now split. Qed."])
::[]
else
Instance("MyRobots",Cst("Names"),App(Cst("Robots"),[Raw("("^string_of_int (x-1) ^ " * n)");Cst("n")]))
@@ -249,8 +247,8 @@ let instance_sync (s : synchro) : stmt list =
match s with
| Async -> [RawCoq(["Instance ic: Async not implemented
Instance InaFun : Async not implemented"])]
- | _ -> [RawCoq([ "Instance IC : inactive_choice unit := NoChoiceIna.";
- "Instance InaFun : inactive_function unit := NoChoiceInaFun."])]
+ | _ -> [Instance("IC",Cst"inactive_choice unit",Cst "NoChoiceIna");
+ Instance("InaFun",Cst "inactive_function unit",Cst "NoChoiceInaFun")]
(**[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
@@ -349,7 +347,7 @@ 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."])
+ ::RawCoq(["#[export] 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 |}"))
::[]
@@ -367,95 +365,161 @@ match l with
| h::tl -> Or(Cst(h),generate_or tl)
| _ -> Cst("")
-(**[generate_definition_phase g]returns the list of stmt to generate the coq code for the definition of the phases of the graph [g]*)
-let generate_definition_phase (g : G.t) : stmt list =
+(**[generate_definition_phase g] returns the list of stmt to generate the coq code for the definition in module type of the phases of the graph [g] and the list of stmt to generate the def in module proof
+ @param g [G.t]
+ @ [stmt list * stmt list] first is for module type, second for module proof
+*)
+let generate_definition_phase (g : G.t) : (stmt list * stmt list) =
Topological.fold (fun v acc ->
- let func_name = string_of_expression v ^" (config : configuration)" in
- RawCoq(["Definition "^func_name^":= (* To_Complete *)."])::acc
- ) g []
+ let func_name = string_of_expression v in
+ (Parameter(func_name,Cst "configuration",Cst"bool")::(fst acc), Def(func_name^" (config: configuration)",Cst("bool"),Cst("(* TODO *)"))::(snd acc))
+ ) g ([],[])
-(**[generate_measure_per_phase g] returns the list of stmt generating the coq code of the measurement functions for each phase
+(**[generate_measure_per_phase g] returns the list of stmt generating the coq code of the measurnatement functions for each phase
+ in module type, and in module proof
@param g [G.t]
- @return [stmt list]*)
-let generate_measure_per_phase (g: Ast.G.t) : stmt list =
+ @return [stmt list * stmt list] first is for module type, second for module proof*)
+let generate_measure_per_phase (g: Ast.G.t) : (stmt list * stmt list) =
Topological.fold (fun v acc ->
- let func_name = string_of_expression v ^"_meas (config : configuration)" in
- Def(func_name,Raw("nat"),Raw("(* To_Complete *)"))::acc
- ) g []
+ let func_name = string_of_expression v ^"_meas" in
+ (Parameter(func_name,Cst "configuration",Cst "nat")::(fst acc),Def(func_name^" (config : configuration)",Cst("nat"),Cst("(* TODO *)"))::(snd acc))
+ ) g ([],[])
-(**[generate_lemmas g] returns the list of stmt corresponding to the lemmas extracted from the graph g
+(**[generate_lemmas g t] returns the list of stmt corresponding to the lemma extracted from the graph [g],
+ the generated stmt depending on the function [t] which corresponds to the desired constructor.
@param g [G.t]
+ @param t [string *Formula.t * stmt list ->stmt)] corresponds to the function of the desired constructor (lemma or parameterlemm).
@return [stmt list]*)
-let generate_lemmas (g : Ast.G.t) : (stmt list * string list) =
+let generate_lemmas (g : Ast.G.t) (t : string *Formula.t * stmt list ->stmt): (stmt list * string list) =
Topological.fold (fun v (acc,s) ->
- let string_v = string_of_expression v in
- let succs = Ast.G.succ g v in
- if succs <> [] then
- let string_succs = (List.map string_of_expression succs) in
- let rcs = List.map (fun x -> x ^ " (round robogram da config) = true") string_succs in
- (Lemma(string_v^"_next_"^String.concat "_or_" string_succs ^" da",
- Forall("config",InfixOp(Raw(string_v^" config = true"),"->",(generate_or rcs) )),[Comment("TODO")])::acc,
- ("("^string_v ^" config)")::s)
- else
- (acc,s)
- ) g ([],[])
+ let string_v = string_of_expression v in
+ let succs = Ast.G.succ g v in
+ if succs <> [] then
+ let string_succs = (List.map string_of_expression succs) in
+ let rcs = List.map (fun x -> x ^ " (round robogram da config) = true") string_succs in
+ (t (string_v^"_next_"^String.concat "_or_" string_succs,
+ Forall("config",InfixOp(Raw(string_v^" config = true"),"->",(generate_or rcs))),
+ [Comment("TODO")])::acc,
+ ("("^string_v ^" config)")::s)
+ else
+ (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
- |(phase,height)::[] -> Formula.Cst("("^ string_of_int height^", "^string_of_expression phase ^"_meas config)")
- |(phase,height)::tl -> If(Cst(string_of_expression phase ^" config"),Cst("("^ string_of_int height^", "^string_of_expression phase ^"_meas config)"),aux tl )
- | _ -> Cst("")
-in
+ let rec aux l =
+ match l with
+ |(phase,height)::[] -> Formula.Cst("("^ string_of_int height^"%nat, "^string_of_expression phase ^"_meas config)")
+ |(phase,height)::tl -> If(Cst(string_of_expression phase ^" config"),Cst("("^ string_of_int height^"%nat, "^string_of_expression phase ^"_meas config)"),aux tl )
+ | _ -> Cst("")
+ in
aux (Ast.assign_height g)
-(**[generate_measure m] returns the list of stmt corresponding to the generation of the measurement
+(**[generate_measure_def g] generates the definition of the measure.
+ @param g [G.t]
+ @return [stmt]*)
+let generate_measure_def (g : G.t)(ret : string) =
+ let body = generate_if_measure g in
+ Def("measure (config : configuration)",Cst(ret),body)
+
+
+(**[generate_measure_all m t gmpp gdp] returns the list of stmt corresponding to the generation of the measure
@param m [measure]
+ @param t function for module type or module proof
+ @param gmpp [stmt list] corresponds to the generation of the measure per phase
+ @param gdp [stmt list] corresponds to the generation of the phase definition
@return [stmt list] *)
-
-let generate_measure (Measure(g): measure) (name_png : string) : stmt list =
+let generate_measure_all (Measure(g): measure)(t : string * Formula.t * stmt list -> stmt)(gmpp : stmt list) (gdp : stmt list ): stmt list =
let ret = "nat*nat" in
- let to_change = generate_if_measure g in
- Ast.png_from_graph g name_png;
- Ast.png_from_graph2 (Ast.scc_graph g;) "scc_graph";
- let measure_per_phase = generate_measure_per_phase g in
- let lemsgen = let lems = generate_lemmas g in
- Comment("Definition of phase")::generate_definition_phase g
- @Comment("Definition of measure per phase ")::measure_per_phase
- @Lemma("InGraph",Forall("config",generate_or (snd lems)),[Comment("TODO")])
+ let m = generate_measure_def g ret in
+ let lemsgen =
+ let lems = generate_lemmas g t in
+ Comment("Definition of phase")::gdp
+ @Comment("Definition of measure per phase "):: gmpp
+ @t("InGraph",Forall("config",generate_or (List.map (fun x -> x ^" = true")(snd lems))),[Comment("TODO")] )
::List.rev (fst lems) in
lemsgen@
- Def("measure (config : configuration)",Cst(ret),to_change)::
- RawCoq(["Instance measure_compat : Proper (equiv ==> Logic.eq) measure."])::proof_to_complete
+ m::
+ t("measure_compat",Cst "Proper (equiv ==> Logic.eq) measure",[Comment("TODO")])::[]
+
+
+(**[generate_lt t] returns the list of stmts corresponding to the generation of lt_config, wf_lt_config, lt_config_compat, and round_lt_config
+ @param t function for module type or module proof
+ @return [stmt list]
+*)
+let generate_lt (t:string * Formula.t * stmt list -> stmt) : stmt list =
+ RawCoq(["Definition lt_config x y := Lexprod.lexprod lt lt (measure (x)) (measure (y))."])
+ :: t("wf_lt_config",Cst("well_founded lt_config"),[Comment("TODO")])
+ :: t("lt_config_compat",Cst ("Proper (equiv ==> equiv ==> iff) lt_config"),[Comment("TODO")])
+ :: t("round_lt_config" , Cst("forall config,
+ moving robogram da config <> nil ->
+ lt_config (round robogram da config) config"),[Comment("TODO")]) ::[]
+
-let generate_lt =
- RawCoq(["Definition lt_config x y := Lexprod.lexprod lt lt (measure (!! x)) (measure (!! y))."])
- :: Lemma("wf_lt_config",Cst("well_founded lt_config"),[Comment("TODO")])
- :: RawCoq(["Instance lt_config_compat : Proper (equiv ==> equiv ==> iff) lt_config."])
- ::proof_to_complete
- @ RawCoq(["Theorem round_lt_config : forall config,
- moving robogram da config <> nil ->
- lt_config (round robogram da config) config."]) ::[]
+ let generate_module_type (m : measure) (s:string) (gmpp:stmt list) (gdp: stmt list) =
+ newline
+ ::ModuleType(s,RawCoq(["Import World."])::Parameterlem("da",Cst("demonic_action"),[Comment("")] )::generate_measure_all m (fun (a,b,c) -> Parameterlem(a, b, c)) gmpp gdp
+ @newline::generate_lt (fun (a,b,c) -> Parameterlem(a, b, c)))::[]
-(**[generate_coq d s] generated from the complete description (world, robogram, measure) [d] the named coq instance [s]
- @param description of
+
+ let generate_module_proof (m: measure)(s:string) (gmpp:stmt list) (gdp : stmt list) =
+ ModuleImpType(s^"_proof",s^"_type", RawCoq(["Import World.";"Variable da : demonic_action."])::generate_measure_all m (fun (a,b,c) -> Lemma(a, b, c)) gmpp gdp
+ @newline::generate_lt (fun (a,b,c) -> Lemma(a, b, c)))::[]
+
+
+(** [write_coq_file gen filename] writes the generated Coq code to the specified file.
+ @param gen stmt list representing the generated Coq code.
+ @param filename The name of the file to write the generated code to.
+*)
+let write_coq_file (gen: stmt list) (filename : string) =
+ let file_out = open_out (filename) in
+ let format_file = Format.formatter_of_out_channel file_out in
+ Format.fprintf format_file "%a@." Coq.pretty_l (gen);
+ close_out file_out;
+ print_endline(filename^ " has been generated");;
+
+(**[generate_filename base n dir]
+ @param base : string, base file name
+ @param n : integer, number of file iterations
+ @param dir : string, file directory
+ @return string, the concatenation of the file name and its number to not overwrite existing files*)
+let rec generate_filename base n dir =
+ let name = base ^ string_of_int n in
+ if (Sys.file_exists (dir^"/"^base^".v")) then
+ (if (Sys.file_exists (dir^"/"^name^".v")) then generate_filename base (n+1) dir else name)
+ else base
+
+
+(**[generate_coq d s] generates 2 coq files
+ 1 containing the world description module, the type module -> regenerate all the time;
+ the other the proof module -> generate only the first time
+ @param description
@param string s
@return[unit] *)
-let generate_coq (Description(d,r,m) : description) (section_name : string)=
- 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
- let section = Section(section_name,(generate_instances d)@newline::generate_robogram r d
- @newline::generate_measure m section_name
- @newline::generate_lt) in
- Format.fprintf format_file "%a@." Coq.pretty_l ((generate_requires d)@[section]);
- close_out file_out;
- print_endline(section_name^".v is generated")
+let generate_coq_2files (Description(d,r,Measure g) : description) (name : string) (proof_name:string) (type_name : string) (overwrite : bool) (dir : string) (gen_graph : bool)=
+ if Ast.check_description (Description(d,r,Measure g))
+ then
+ let gmpptype, gmpp_proof = generate_measure_per_phase g in
+ let gdp_type, gdp_proof = generate_definition_phase g in
+ let name_gen = if overwrite then type_name else generate_filename type_name 1 dir in
+ if gen_graph then begin
+ Ast.png_from_graph g name_gen dir;
+ Ast.png_from_graph2 (Ast.scc_graph g) (name_gen^"_scc_graph") dir;
+ end;
+
+ let module_world_type = (generate_requires d)@Module("World",(generate_instances d)@newline::generate_robogram r d)
+ :: generate_module_type (Measure g) name gmpptype gdp_type in
+ write_coq_file module_world_type (dir^"/"^name_gen^".v");
+ let file_proof_exists =
+ Sys.file_exists (dir^"/"^proof_name^".v") in
+ if not(file_proof_exists) then
+ write_coq_file ((generate_requires d)@Require(true,["Pactole.CaseStudies.Generate_test."^type_name])::generate_module_proof (Measure g) name gmpp_proof gdp_proof) (dir^"/"^proof_name^".v")
+
+
else
- ()
\ No newline at end of file
+ ()
diff --git a/lib/lexer.mll b/lib/lexer.mll
index f96a35cc951416a2c5d7affe62528de5a0b28a51..be04b7a5e38b59ac293851759505765ae63a5b30 100644
--- a/lib/lexer.mll
+++ b/lib/lexer.mll
@@ -80,8 +80,6 @@ rule token = parse
| "|" { PIPE}
| "end" { END}
| "->" { ARROW}
- | "=>" { IMPLICATION}
- | "<=>" { EQUIVALENCE}
| "let" { LET}
| "=" { AFFECT}
| "in" { IN}
diff --git a/lib/parser.mly b/lib/parser.mly
index 294cdc485c907643a2f83acceefe32d254547418..1250f87c956355f086360eaef388045eeb2f42fb 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -29,7 +29,6 @@
%token <string> VARIABLE
%token <string> KEYWORD
%token IF THEN ELSE MATCH WITH PIPE ARROW END
-%token IMPLICATION EQUIVALENCE
%token LET AFFECT IN FUN
%token PLUS MINUS MULT DIV AND OR NOT
%token SUP INF EQUAL DIFF
@@ -166,11 +165,11 @@ value :
lights:
/*Internal light -> visible only to the robot*/
- | INTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(Intern i)}
+ | INTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(Intern (i,$startpos.Lexing.pos_lnum))}
/*External light -> visible only to other robots*/
- | EXTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(Extern i)}
+ | EXTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(Extern (i,$startpos.Lexing.pos_lnum))}
/*Light visible to all*/
- | FULL LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(All i)}
+ | FULL LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(All (i,$startpos.Lexing.pos_lnum))}
%inline range :
@@ -216,8 +215,6 @@ robogram:
| expression * {$1}
expression:
- /*(e)*/
- | PARENOPEN e = expression PARENCLOSE {e}
| e = constant {e}
/*if e1 then e2 else e3*/
| IF e1 = expression THEN e2 = expression ELSE e3 = expression {Cond(e1,e2,e3)} %prec AFFECT
@@ -228,7 +225,7 @@ expression:
| LET v = VARIABLE AFFECT e = expression IN e2=expression {Let(v,e,e2)} %prec AFFECT
/*name_variable = e*/
| v = VARIABLE; AFFECT e = expression {Affectation(v,e)}
- /*[a;z;e;r;t....]*/
+ /*(a;...b;)*/
| 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)}
@@ -261,17 +258,18 @@ argument :
id :
| VARIABLE {Var $1}
- | x = KEYWORD POINT e = VARIABLE {Point(x,e)}
+ | x = KEYWORD POINT e = VARIABLE {Point(x,e,$startpos.Lexing.pos_lnum)}
+
set :
| e = expression COMMA s = set {Some(s,e)}
| e = expression {Some(Vide,e)}
- | e = KEYWORD COMMA s = set {Some(s,Var e)}
+ | e = KEYWORD COMMA s = set {Some(s,Var e)}
| e = KEYWORD {Some(Vide,Var e)}
| {Vide}
%inline binop :
- | PLUS {(*Format.eprintf "PLUS ";*) Plus}
+ | PLUS {Plus}
| MINUS {Minus}
| MULT {Mult}
| DIV {Div}
@@ -307,17 +305,8 @@ edge_list :
sommet :
- | p = prop {p}
+ | p = phase {p}
-prop :
- | PARENOPEN prop propop prop PARENCLOSE {BinOp($2,$3,$4)}
- | NOT prop {Not $2}
+phase :
| VARIABLE {Var $1}
| KEYWORD {Var $1}
- | PARENOPEN f = appfunc PARENCLOSE {f}
-
-propop :
- | AND {And}
- | OR {Or}
- | IMPLICATION {Impli}
- | EQUIVALENCE {Equiv}
\ No newline at end of file