Skip to content
Snippets Groups Projects
Commit 7bd70794 authored by Kylian Fontaine's avatar Kylian Fontaine
Browse files

Merge branch 'module' into 'main' 

Module

See merge request !1
parents 5dcd9ee5 1c16e62e
No related branches found
No related tags found
1 merge request!1Module
Hide whitespace changes
Inline Side-by-side
Readme.md
+ 49
− 26
View file @ 7bd70794
# 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
```
bin/main.ml
+ 37
− 6
View file @ 7bd70794
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;;
lib/ast.ml
+ 31
− 35
View file @ 7bd70794
......@@ -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
......
lib/coq.ml
+ 16
− 1
View file @ 7bd70794
......@@ -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 (_,[]) -> ()
......
lib/gencoq.ml
+ 145
− 81
View file @ 7bd70794
......@@ -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
()
lib/lexer.mll
+ 0
− 2
View file @ 7bd70794
......@@ -80,8 +80,6 @@ rule token = parse
| "|" { PIPE}
| "end" { END}
| "->" { ARROW}
| "=>" { IMPLICATION}
| "<=>" { EQUIVALENCE}
| "let" { LET}
| "=" { AFFECT}
| "in" { IN}
......
lib/parser.mly
+ 10
− 21
View file @ 7bd70794
......@@ -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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment