From 4309698add243ad7fdea9e7e2470f2463f0bbd80 Mon Sep 17 00:00:00 2001
From: Kylian Fontaine <kylian.fontaine@etu.univ-lyon1.fr>
Date: Thu, 20 Jun 2024 13:58:11 +0200
Subject: [PATCH] UpdFun et FC ring (explo/definitions) + ring_size_spec +
Debut de measure
---
lib/ast.ml | 19 +++++++++++------
lib/gencoq.ml | 56 ++++++++++++++++++++++++++++++++++----------------
lib/lexer.mll | 2 ++
lib/parser.mly | 17 +++++++++++----
4 files changed, 66 insertions(+), 28 deletions(-)
diff --git a/lib/ast.ml b/lib/ast.ml
index 5ddc16b..0b3e3f4 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -202,9 +202,16 @@ type information =
| Roles of (int * string) list
| Share of share
+(*TODO: a modif selon l'implementation de graph utilisé*)
+type graph = Graph of string
+
+type measure = Measure of int * graph
+
+
+
(* Une description c'est 1: description de l'environnement et des capacites des robot
2: robogram *)
-type description = Description of ((information list) * (expr list))
+type description = Description of ((information list) * (expr list) * measure)
(*FONCTION SUR LES SETS*)
@@ -354,7 +361,7 @@ let string_of_rigidity (r: rigidity) : string =
let rec string_of_description (desc:description) : string =
match desc with
- | Description (infos,robogram) ->
+ | 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 =
@@ -404,7 +411,7 @@ let check_description (d : description) :bool =
let unique f d = List.length (List.filter f d) = 1
in
match d with
- | Description (d',_) -> if not(unique info_sync d')
+ | Description (d',_,_) -> if not(unique info_sync d')
then (print_endline "Error: Problem of defining sync"; false)
else (
if not(unique info_space d')
@@ -418,14 +425,14 @@ let check_description (d : description) :bool =
*)
let get_sensors (d : description) : sensor list =
match d with
- | Description(d', _) -> (match List.find_opt (fun x -> match x with Sensors _ -> true | _-> false) d' with
+ | Description(d', _,_) -> (match List.find_opt (fun x -> match x with Sensors _ -> true | _-> false) d' with
Some (Sensors s) -> s
| _ -> raise(Failure("Error: Not find Sensors")))
(**[get_robot d] Renvoie la liste des champs robot contenu dans la descritpion [d]
@param description
@return [field list]*)
-let get_robot (Description(d', _) : description) : field list =
+let get_robot (Description(d', _,_) : description) : field list =
match List.find_opt (fun x -> match x with Robot _ -> true | _-> false) d' with
Some (Robot r) -> r
| _ -> raise(Failure("Error: Not find Robot"))
@@ -435,7 +442,7 @@ let get_robot (Description(d', _) : description) : field list =
@return [string list] *)
let get_activelyup (d : description) : string list =
match d with
- | Description(d', _) -> (match List.find_opt (fun x -> match x with ActivelyUpdate _ -> true | _-> false) d' with
+ | Description(d', _,_) -> (match List.find_opt (fun x -> match x with ActivelyUpdate _ -> true | _-> false) d' with
Some (ActivelyUpdate a) -> List.map string_of_valretr a
| _ -> raise(Failure("Error: Not find ActivelyUpdate")))
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 3abfb5f..8db81af 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -153,12 +153,13 @@ let instance_R_R2 (s:space) (d: information list): stmt list =
@param int n
@return [stmt list]*)
let instance_ring (n:int) : stmt list =
- if n > 0 then
- Instance("MyRing",Raw("RingSpec"),Record([Raw("ring_size := "^string_of_int n);Raw("ring_size_spec:= (* QUOI METTRE ? *)")]))
- :: Notation("ring_node",App(Cst "finite_node",[Cst "ring_size"] ))
- ::Instance("Loc",Cst "Location",App(Cst "make_Location",[Cst "ring_node"]))::[]
+ let ring = if n > 0 then
+ Instance("MyRing",Raw("RingSpec"),Record([Raw("ring_size := "^string_of_int n);Raw("ring_size_spec:= ltac:(auto)")]))
+
else
- RawCoq(["Context {RR : RingSpec}."])::[]
+ RawCoq(["Context {RR : RingSpec}."])
+ in
+ ring::Notation("ring_node",App(Cst "finite_node",[Cst "ring_size"] ))::Instance("Loc",Cst "Location",App(Cst "make_Location",[Cst "ring_node"]))::[]
(**[instance_space s] retourne une liste de stmt permettant de generer le code coq pour instancier l'espace s
@param space [s] Ã instancier pour le moment seulement R, R2, Ring
@@ -178,11 +179,20 @@ let instance_space (s: space) (d : information list): stmt list =
@param string valeur de retour du robogram
@return stmt
*)
-let instance_updfunc_rigid (valret : string) :stmt =
+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) }"))
-
-let instance_updfunc_Flexible (d:expr) (valret : string) : stmt =
+ ::RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])::[]
+ else
+ Instance("FrameChoice",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("{
+ 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_rigidity r valret] retourne une liste de stmt permettant de generer le code coq pour instancier la rigidite des deplacements
@@ -190,18 +200,16 @@ let instance_updfunc_Flexible (d:expr) (valret : string) : stmt =
@param valret valeur de retour du robogram
@return [stmt list]
*)
-let instance_rigidity (r:rigidity) (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"),[Var(0,"unit")]),Raw("NoChoice"))
- :: instance_updfunc_rigid valret
- ::RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])
- ::[]
+ :: instance_updfunc_rigid valret world
+
| Flexible d -> Instance("RobotChoice",Raw("robot_choice (path "^ valret^")"),Raw("{ robot_choice_Setoid := path_Setoid "^valret^"}"))
::Instance("ActiveChoice",App(Var(0,"update_choice"),[Var(0,"ratio")]),Raw "Flexible.OnlyFlexible")
::Var(string_of_expression d,Raw("R"))
::instance_updfunc_Flexible d valret
- ::[]
(**[instance_info fl] retourne une liste de stmt permettant de generer le code coq pour instancier de l'état du robot
@@ -274,7 +282,7 @@ let require_space (s: space) : stmt =
match s with
| R -> Require(true,["Pactole.Spaces.R"])
| R2 -> Require(true,["Pactole.Spaces.R2";"Rbase"])
- | ZnZ _ -> Require(true,["Pactole.Spaces.Ring"])
+ | ZnZ _ -> Require(true,["Pactole.Spaces.Ring";"Reals";"Pactole.Spaces.Isomorphism"])
| _ ->raise(Failure ("Not implemanted"))
(**[require_multi s] retourne un stmt permettant de generer le require pour la multiplicité
@@ -318,7 +326,7 @@ let valret = get_val_ret world in
| [] -> []
| h::t-> (match h with
| Space s -> newline::(instance_space s world) @ genworld t
- | Rigidity r -> genworld t @newline::(instance_rigidity r valret)
+ | Rigidity r -> genworld t @newline::(instance_rigidity r valret world)
| Robot r -> newline::(instance_info r) @ genworld t
| Sync s -> genworld t @(instance_sync s)
| Sensors s -> genworld t @ (instance_sensors s)
@@ -342,11 +350,23 @@ let generate_robogram (r : expr list) (d: information list) : stmt list =
::[]
| [] -> Def ("Robogram_pgm (s : observation)",Raw(valretcoq),Raw("[]")) ::[]
-let generate (Description(d,r) : description) (section_name : string)=
- if Ast.check_light (Description (d,r)) then
+let rec n_times (x : int) :string =
+ if x > 0 then n_times (x -1)^"*"^"nat"
+ else "nat"
+
+let generate_measure (Measure(i,_): measure) : stmt list =
+ let ret = String.concat "*"(List.init i (fun _ ->"nat")) in
+ let to_change = String.concat ","(List.init i (fun _ ->"0%nat"))in
+ RawCoq(["Function measure (s : observation) : "^ret ^" :=
+ (*A REMPLIR GRACE AU GRAPH*)
+ ("^to_change^")."; (*TODO: à modifié pour utiliser le graph*)
+ "Instance measure_compat : Proper (equiv ==> Logic.eq) measure."])::proof_to_complete
+
+let generate (Description(d,r,m) : description) (section_name : string)=
+ if Ast.check_light (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) 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
else
diff --git a/lib/lexer.mll b/lib/lexer.mll
index 6215f70..e9329f5 100644
--- a/lib/lexer.mll
+++ b/lib/lexer.mll
@@ -14,6 +14,7 @@ let keyword = ['A'-'Z']alpha+
rule token = parse
| "World" {WORLD}
| "Robogram" {ROBOGRAM}
+ | "Measure" {MEASURE}
| "Sync" {SYNC}
| "FSYNC" {FSYNC}
| "SSYNC" {SSYNC}
@@ -102,6 +103,7 @@ rule token = parse
| "/*" {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; comment lexbuf}
| integer {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; INT (int_of_string (Lexing.lexeme lexbuf))}
| float {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; FLOAT (float_of_string(Lexing.lexeme lexbuf) )}
+ | "," {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; COMMA}
| keyword {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; KEYWORD (Lexing.lexeme lexbuf)}
| variable {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; VARIABLE (Lexing.lexeme lexbuf)}
| space {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; token lexbuf}
diff --git a/lib/parser.mly b/lib/parser.mly
index ccfc79c..c4fddcf 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -17,11 +17,12 @@
/*%token MEMOIRE OBLIVIOUS FINITE INFINITE*/
%token SHARE FULLCOMPASS CHIRALITY ONEAXEORIEN
%token RIGIDITY RIGIDE FLEXIBLE
-%token COLON BRACKETOPEN BRACKETCLOSE SEMICOLON PARENOPEN PARENCLOSE
+%token COLON BRACKETOPEN BRACKETCLOSE SEMICOLON PARENOPEN PARENCLOSE COMMA
%token POINT
%token ROBOT PUBLIC PRIVATE ACTIVELYUP
%token ROLES
-%token WORLD ROBOGRAM
+%token WORLD ROBOGRAM MEASURE
+
%token LOCATION DIRECTION
@@ -49,7 +50,10 @@
%%
description :
- | WORLD COLON information* ROBOGRAM COLON robogram EOF {Description (List.flatten $3,$6)}
+ | WORLD COLON information*
+ ROBOGRAM COLON robogram
+ MEASURE COLON measure
+ EOF {Description (List.flatten $3,$6,$9)}
/* DESCRIPTION DE L'ENVIRONNEMENT*/
@@ -300,4 +304,9 @@ resultpattern :
pattern :
| v = VARIABLE {Var v}
| v = VARIABLE COLON COLON e = pattern {Cons(Var v,e)}
- | PARENOPEN s = set PARENCLOSE COLON COLON e = pattern {Cons(Set s,e)}
\ No newline at end of file
+ | PARENOPEN s = set PARENCLOSE COLON COLON e = pattern {Cons(Set s,e)}
+
+
+
+measure:
+| PARENOPEN l = separated_list(COMMA,VARIABLE) PARENCLOSE {Measure(List.length l, Graph"none")}
\ No newline at end of file
--
GitLab