From a2c8a0ce4cd2cb5e583c8c8c37ffe4736f8dde19 Mon Sep 17 00:00:00 2001
From: Kylian Fontaine <kylian.fontaine@etu.univ-lyon1.fr>
Date: Fri, 28 Jun 2024 14:52:15 +0200
Subject: [PATCH] da hors lemmes, declaration des forall
---
Readme.md | 2 +-
bin/main.ml | 15 +--
lib/ast.ml | 162 +++++++++++++++++++-------
lib/gencoq.ml | 82 +++++++------
lib/{graphtest.ml => graphmeasure.ml} | 0
lib/parser.mly | 24 ++--
6 files changed, 183 insertions(+), 102 deletions(-)
rename lib/{graphtest.ml => graphmeasure.ml} (100%)
diff --git a/Readme.md b/Readme.md
index f6b3f3b..c9c7fe2 100644
--- a/Readme.md
+++ b/Readme.md
@@ -37,7 +37,7 @@ Rigidity := Flexible delta
```
Couleur : Red; Blue; Yellow; Green; Purple; Orange
-- Robot := Permet de definir des champs privée et publique pour le robot, il est necessaire de lister les éléments privée puis les éléments public
+- 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; ...
diff --git a/bin/main.ml b/bin/main.ml
index c4a96a9..7cbc768 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -1,15 +1,10 @@
open Dsl
-let repo = "./sourcegenerate";;
+(*let repo = "./sourcegenerate";;
let files =Array.to_list (Sys.readdir repo);;
print_endline(String.concat "; " files);;
-
+*)
let gen (x : string) =
- let path = repo ^"/"^ x in
- Gencoq.generate (Interface.parse_description path) x;;
-
-List.map gen files;;
-(*
-if (Ast.check_sensors_desc desc) && (Ast.check_activelyup desc)then
-print_endline (Ast.string_of_description desc);;
-*)
\ No newline at end of file
+ Gencoq.generate_coq (Interface.parse_description x) (Filename.basename x);;
+
+gen Sys.argv.(1);;
diff --git a/lib/ast.ml b/lib/ast.ml
index b3633a4..a6ff2f8 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -1,4 +1,4 @@
-open Graphtest
+
(*ROBOGRAM*)
type binop =
@@ -205,14 +205,6 @@ type information =
| Roles of (int * string) list
| Share of share
-
-
-type measure = Measure of int * G.t
-(* Une description c'est 1: description de l'environnement et des capacites des robot
- 2: robogram *)
-type description = Description of (information list) * (expr list) * measure
-
-
(*FONCTION SUR LES SETS*)
(** [length s] retourne la longueur du set [s]
@param [s] 'a set dont on veut la longueur
@@ -222,7 +214,7 @@ let rec length_set (s:'a set): int =
| Vide -> 0
| Some (s,_) -> 1 + (length_set s)
-(*[push s e] ajoute un element e au 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 *)
@@ -273,7 +265,7 @@ let rec string_of_expression (e : expr) : string =
| 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 ^")"
- | App (f,arg) -> "("^ string_of_expression f ^") appliqué a (" ^ string_of_expression arg ^")"
+ | 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')
@@ -288,7 +280,15 @@ let rec string_of_expression (e : expr) : string =
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
@@ -342,7 +342,7 @@ let rec string_of_value (v : value) : string =
| 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
@@ -360,30 +360,8 @@ let string_of_rigidity (r: rigidity) : string =
| Rigide -> "Rigide"
| Flexible _ -> "Flexible"
-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")
-
+
+
(** [info_sync i] verifie qu'une information est une information sur la synchronisation
@param i information
@return bool *)
@@ -400,6 +378,101 @@ let info_space (i : information):bool =
| Space _ -> true
| _ -> false
+
+
+
+
+(*GRAPH*)
+module Node = struct
+ type t = expr
+ let compare = compare
+ let hash = Hashtbl.hash
+ let equal = (=)
+end
+
+module Edge = struct
+ type t = string
+ let compare = compare
+ let default = ""
+end
+
+
+module G = Graph.Imperative.Digraph.ConcreteLabeled(Node)(Edge)
+
+
+type edge =
+| Nolab of (expr * expr)
+
+let graph_from_edges (el : edge list)=
+ let g = G.create () in
+ let nolab = fun (x, y) ->
+ let vx = G.V.create x in
+ let vy = G.V.create y in
+ G.add_edge g vx vy
+ in
+ let rec add_edge (el : edge list) =
+ match el with
+ | [] -> ()
+ | (Nolab h)::t -> nolab h ; add_edge t
+ in add_edge el;
+ g
+
+
+ let png_from_graph g =
+ 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;\n" ^ graph ^ "}" in
+ let oc = open_out "graph.dot" in
+ Printf.fprintf oc "%s\n" dot;
+ close_out oc;
+ ignore (Sys.command "dot -Tpng graph.dot -o graph.png")
+
+
+(*/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 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
@@ -465,7 +538,7 @@ let check_sensor (s: sensor) (r:field list):bool =
let check_sensors_desc (d:description) :bool =
let res= List.find_opt (fun x -> not (check_sensor x (get_robot d))) (get_sensors d) in
match res with
- | Some x -> print_endline("Error : " ^(match x with |Custom (x',_)-> x' | _->"")^" is not declared public in robot"); false
+ | 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
@@ -474,9 +547,10 @@ let check_sensors_desc (d:description) :bool =
let check_activelyup (d:description) :bool =
let field_to_pair f = List.map(fun x -> match x with Public x -> x | Private x -> x) f in
let aux s l = List.exists (fun (x,_) -> x = s) (field_to_pair l) in
- let res = List.find_opt (fun x -> not (aux x (get_robot d))) (get_activelyup d) in
+ let fields_to_check f = List.filter (fun x -> (x <> "Location") && (x <> "Direction")) f ;in
+ let res = List.find_opt (fun x -> not (aux x (get_robot d))) (fields_to_check(get_activelyup d)) in
match res with
- | Some x -> print_endline("Error : " ^x^" x is not declared in robot"); false
+ | Some x -> raise(Failure("Error : " ^x^" is not declared in robot"))
| _-> true
@@ -488,9 +562,11 @@ let check_light d : bool =
let rec check flist = (
fun x -> match x with
| [] -> true
- | Public (_,Light(Intern _))::_ -> false
- | Private (_, Light(Extern _))::_ -> false
+ | Public (_,Light(Intern _))::_ -> raise(Failure("Error light in wrong field"))
+ | Private (_, Light(Extern _))::_ -> raise(Failure("Error light in wrong field"))
| _::t-> check t
) flist
in
- check (get_robot d)
\ No newline at end of file
+ check (get_robot d)
+
+
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index e11f80a..991f658 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -1,11 +1,11 @@
open Ast
-(*open Formula*)
open Coq
let geometry =[("isobarycenter",Formula.Raw("isobarycenter"));
+ ("barycenter",Formula.Raw("barycenter"));
("on_SEC"),Formula.Raw("on_SEC")]
let observation =[("elements", Formula.Raw("(elements s)"));
("support"), Formula.Raw("support s")]
@@ -113,8 +113,6 @@ let rec expr_to_coq (r : expr) : Formula.t =
| 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)
@@ -185,17 +183,17 @@ let instance_space (s: space) (d : information list): stmt list =
*)
let instance_updfunc_rigid (valret : string) (d: information list):stmt list =
if not(get_space d = "Ring") then
- Instance("UpdateFunc",Raw("update_function ("^valret^") (Similarity.similarity "^valret^") unit"),Raw("{update := fun _ _ _ target _ => target;update_compat := ltac:(now repeat intro) }"))
- ::RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])::[]
+ Instance("UpdFun",Raw("update_function ("^valret^") (Similarity.similarity "^valret^") unit"),Raw("{update := fun _ _ _ target _ => target;update_compat := ltac:(now repeat intro) }"))
+ ::RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])::[]
else
- Instance("FrameChoice",App(Cst "frame_choice",[Raw("(Z * bool)")]),Raw(" {frame_choice_bijection :=
+ Instance("FC",App(Cst "frame_choice",[Raw("(Z * bool)")]),Raw(" {frame_choice_bijection :=
fun nb => if snd nb then Ring.sym (fst nb) else Ring.trans (fst nb);
frame_choice_Setoid := eq_setoid _ }"))::
- Instance("UpdateFunc",Raw("update_function direction (Z * bool) unit"),Raw("{
+ Instance("UpdFun",Raw("update_function direction (Z * bool) unit"),Raw("{
update := fun config g _ dir _ => move_along (config (Good g)) dir;
update_compat := ltac:(repeat intro; subst; now apply move_along_compat) }"))::[]
let instance_updfunc_Flexible (d:expr) (valret : string): stmt list =
- Instance("UpdateFunc",Raw("update_function (path "^valret^") (Similarity.similarity "^valret^") ratio"),Raw(" FlexibleUpdate "^string_of_expression d))
+ Instance("UpdFun",Raw("update_function (path "^valret^") (Similarity.similarity "^valret^") ratio"),Raw(" FlexibleUpdate "^string_of_expression d))
::[]
@@ -206,12 +204,12 @@ let instance_updfunc_Flexible (d:expr) (valret : string): stmt list =
*)
let instance_rigidity (r:rigidity) (valret : string) (world: information list): stmt list =
match r with(*TODO: Est-ce la bonne maniere d'ecrire l'UpdateFunc?*)
- | Rigide -> Instance("RobotChoice",Raw("robot_choice "^ valret),Raw("{ robot_choice_Setoid := "^valret^"_Setoid}"))
- ::Instance("ActiveChoice",App(Var(0,"update_choice"),[Cst("unit")]),Raw("NoChoice"))
+ | Rigide -> Instance("RC",Raw("robot_choice "^ valret),Raw("{ robot_choice_Setoid := "^valret^"_Setoid}"))
+ ::Instance("UC",App(Var(0,"update_choice"),[Cst("unit")]),Raw("NoChoice"))
:: instance_updfunc_rigid valret world
- | Flexible d -> Instance("RobotChoice",Raw("robot_choice (path "^ valret^")"),Raw("{ robot_choice_Setoid := path_Setoid "^valret^"}"))
- ::Instance("ActiveChoice",App(Cst("update_choice"),[Cst("ratio")]),Raw "Flexible.OnlyFlexible")
+ | Flexible d -> Instance("RC",Raw("robot_choice (path "^ valret^")"),Raw("{ robot_choice_Setoid := path_Setoid "^valret^"}"))
+ ::Instance("UC",App(Cst("update_choice"),[Cst("ratio")]),Raw "Flexible.OnlyFlexible")
::Var(string_of_expression d,Raw("R"))
::instance_updfunc_Flexible d valret
@@ -251,10 +249,10 @@ let instance_byzantine (x : int ) : stmt list =
*)
let instance_sync (s : synchro) : stmt list =
match s with
- | Async -> [RawCoq(["Instance InactiveChoice: Async not implemented
- Instance InactiveFunc : Async not implemented"])]
- | _ -> [RawCoq([ "Instance InactiveChoice : inactive_choice unit := NoChoiceIna.";
- "Instance InactiveFunc : inactive_function unit := NoChoiceInaFun."])]
+ | 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_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
@@ -354,39 +352,51 @@ let generate_robogram (r : expr list) (d: information list) : stmt list =
::[]
| [] -> Def ("Robogram_pgm (s : observation)",Raw(valretcoq),Raw("[]")) ::[]
-let rec n_times (x : int) :string =
- if x > 0 then n_times (x -1)^"*"^"nat"
- else "nat"
-
-let generate_lemmas (g : Graphtest.G.t) : stmt list =
- Graphtest.G.fold_vertex (fun v acc ->
- let succs = Graphtest.G.succ g v in
+
+(**[generate_lemmas g] retourne la liste de stmt correspondant au lemme extrait du graph g
+ @param g [G.t]
+ @return [stmt list]*)
+let generate_lemmas (g : Ast.G.t) : stmt list =
+ Ast.G.fold_vertex (fun v acc ->
+ let succs = Ast.G.succ g v in
+ let forall v =
+ String.concat " " (List.map string_of_expression (Ast.get_param v))
+ in
if succs <> [] then
- let rcs = List.map (fun x -> x ^ " (round config)") succs in
- Lemma("lemma"^string_of_int (List.length acc),Raw(v^" config -> "^String.concat " \\/ " rcs),[])::acc
+ let rcs = List.map (fun x -> x ^ " (round Robogram da config)") (List.map string_of_expression succs) in
+ Lemma("lemma"^string_of_int (List.length acc),Forall(("config "^forall v),Raw(string_of_expression v^" config -> "^String.concat " \\/ " rcs)),[])::acc
else
acc
) g []
-
+(**[generate_measure m] retourne la liste de stmt correspondant a la generation de la mesure
+ @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 ret = String.concat "*"(List.init i (fun _ ->"nat")) in
let to_change = String.concat ","(List.init i (fun _ ->"0%nat"))in
- Graphtest.png_from_graph g;
- Graphtest.print_relations_test g;
- let lems =List.rev (generate_lemmas g) in
+ Ast.png_from_graph g;
+ let lems =Var("da",Cst "demonic_action")::List.rev (generate_lemmas g) in
RawCoq(["Function measure (s : observation) : "^ret ^" :=
-
- ("^to_change^")."; (*TODO: à modifié pour utiliser le graph*)
+ ("^to_change^")."; (*TODO: *)
"Instance measure_compat : Proper (equiv ==> Logic.eq) measure."])::proof_to_complete@lems
-let generate (Description(d,r,m) : description) (section_name : string)=
- if Ast.check_light (Description (d,r,m)) then
+
+(**[generate_coq d] genere a partir de la description complete (world,robogram,measure) l'instance coq
+ @param descritpion
+ @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)) &&
+ Ast.check_sensors_desc (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) in
Format.fprintf format_file "%a@." Coq.pretty_l ((generate_requires d)@[section]);
- close_out file_out
+ close_out file_out;
+ print_endline(section_name^".v is generated")
else
- raise(Failure("Error light in wrong field"))
\ No newline at end of file
+ ()
\ No newline at end of file
diff --git a/lib/graphtest.ml b/lib/graphmeasure.ml
similarity index 100%
rename from lib/graphtest.ml
rename to lib/graphmeasure.ml
diff --git a/lib/parser.mly b/lib/parser.mly
index 777e464..113c850 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -1,6 +1,5 @@
%{
open Ast
- open Graphtest
%}
%token EOF
@@ -311,23 +310,24 @@ pattern :
measure:
-| PARENOPEN l = separated_list(COMMA,VARIABLE) PARENCLOSE el = edge_list {Measure(List.length l,graph_from_edges el)}
+ | PARENOPEN l = separated_list(COMMA,VARIABLE) PARENCLOSE el = edge_list {Measure(List.length l,graph_from_edges el)}
edge :
-| v1 = sommet ARROW v2 = sommet {Nolab(v1,v2)}
+ | v1 = sommet ARROW v2 = sommet {Nolab(v1,v2)}
edge_list :
-| v = list(edge) { v }
+ | v = list(edge) { v }
sommet :
-| p = prop {string_of_expression p}
+ | p = prop {p}
prop :
-| PARENOPEN prop propop prop PARENCLOSE {BinOp($2,$3,$4)}
-| NOT prop {Not $2}
-| VARIABLE {Var $1}
+ | PARENOPEN prop propop prop PARENCLOSE {BinOp($2,$3,$4)}
+ | NOT prop {Not $2}
+ | VARIABLE {Var $1}
+ | PARENOPEN f = appfunc PARENCLOSE {f}
propop :
-| AND {And}
-| OR {Or}
-| IMPLICATION {Impli}
-| EQUIVALENCE {Equiv}
\ No newline at end of file
+ | AND {And}
+ | OR {Or}
+ | IMPLICATION {Impli}
+ | EQUIVALENCE {Equiv}
\ No newline at end of file
--
GitLab