From 143f87e70d1c9c9a8ec4b531548b55e7d581d779 Mon Sep 17 00:00:00 2001 From: Kylian Fontaine <kylian.fontaine@etu.univ-lyon1.fr> Date: Mon, 15 Jul 2024 10:54:41 +0200 Subject: [PATCH] modification sur valeur de retour du robogram -> light --- lib/gencoq.ml | 52 +++++++++++++++++++++++++++++++++------------------ 1 file changed, 34 insertions(+), 18 deletions(-) diff --git a/lib/gencoq.ml b/lib/gencoq.ml index af8f74d..23fcbb7 100644 --- a/lib/gencoq.ml +++ b/lib/gencoq.ml @@ -22,19 +22,19 @@ let get_nb_byz (infos: information list) : int = (**[get_val_ret infos] returns the return type of the robogram @param information list corresponding to the description of the world @return [string] corresponding to location or direction FOR THE MOMENT*) -let get_val_ret (infos : information list) : string = +let get_val_ret (infos : information list) : string list = (* TODO: Implementation Light*) let rec locdir valret = match valret with - | Location::_ -> "location" - | Direction::_ -> "direction" - | _::t -> locdir t - | [] -> "location" + | Location::tl -> "location" :: (locdir tl ) + | Direction::tl -> "direction" ::(locdir tl) + | Str x ::tl -> if x = "Light" then "light" :: (locdir tl) else (locdir tl) + | [] -> [] in let valret = List.find_opt (fun x -> match x with |ActivelyUpdate _ -> true | _ -> false) infos in match valret with | Some (ActivelyUpdate x) -> locdir x - | _-> "location" + | _-> ["location"] (**[get_space infos] returns the string corresponding to the space @param information list corresponding to the description of the world @@ -170,7 +170,7 @@ 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("UpdFun",Raw("update_function ("^valret^") (Similarity.similarity "^valret^") unit"),Raw("{update := fun _ _ _ target _ => target;update_compat := ltac:(now repeat intro) }")) + Instance("UpdFun",Raw("update_function ("^valret^") (Similarity.similarity location) unit"),Raw("{update := fun _ _ _ target _ => target;update_compat := ltac:(now repeat intro) }")) ::RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])::[] else Instance("FC",App(Cst "frame_choice",[Raw("(Z * bool)")]),Raw(" {frame_choice_bijection := @@ -179,8 +179,8 @@ let instance_updfunc_rigid (valret : string) (d: information list):stmt list = 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("UpdFun",Raw("update_function (path "^valret^") (Similarity.similarity "^valret^") ratio"),Raw(" FlexibleUpdate "^string_of_expression d)) +let instance_updfunc_Flexible (d:expr) (_ : string list): stmt list = + Instance("UpdFun",Raw("update_function (path location) (Similarity.similarity location) ratio"),Raw(" FlexibleUpdate "^string_of_expression d)) ::[] @@ -189,13 +189,19 @@ let instance_updfunc_Flexible (d:expr) (valret : string): stmt list = @param valret return value of the robogram @return [stmt list] *) -let instance_rigidity (r:rigidity) (valret : string) (world: information list): stmt list = +let instance_rigidity (r:rigidity) (valret : string list) (world: information list): stmt list = + let rc_return, rc_setoid = + match valret with + | x ::[] -> x,x^"_Setoid" + | _ ::_ -> "("^String.concat " * "valret ^")" ,"prod_Setoid "^ String.concat " " (List.map (fun s -> s ^"_Setoid") valret) + | [] -> raise(Failure " Error return value") in + match r with(*TODO: Est-ce la bonne maniere d'ecrire l'UpdateFunc?*) - | Rigide -> Instance("RC",Raw("robot_choice "^ valret),Raw("{ robot_choice_Setoid := "^valret^"_Setoid}")) + | Rigide -> print_endline(rc_setoid); Instance("RC",Raw("robot_choice "^rc_return),Raw("{ robot_choice_Setoid := "^rc_setoid^"}")) ::Instance("UC",App(Var(0,"update_choice"),[Cst("unit")]),Raw("NoChoice")) - :: instance_updfunc_rigid valret world + :: instance_updfunc_rigid (rc_return) world - | Flexible d -> Instance("RC",Raw("robot_choice (path "^ valret^")"),Raw("{ robot_choice_Setoid := path_Setoid "^valret^"}")) + | Flexible d -> Instance("RC",Raw("robot_choice (path info)"),Raw("{ robot_choice_Setoid := path_Setoid location}")) ::Instance("UC",App(Cst("update_choice"),[Cst("ratio")]),Raw "Flexible.OnlyFlexible") ::Var(string_of_expression d,Raw("R")) ::instance_updfunc_Flexible d valret @@ -212,10 +218,14 @@ let instance_info (fl:field list) : stmt list = |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''^"."]) - ::RawCoq(["Definition info := (location * light)%type."]) + ::Instance("light_Setoid",Cst "Setoid light",Cst "eq_setoid light") + ::RawCoq(["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)))."])::[] (*TODO: Le reste des info sont a faire*) - | _ ->Instance("St",Raw("State location"),Raw("OnlyLocation (fun _ => True)")) ::[]) + | _ ->RawCoq(["Definition info := (location)%type."]) + ::Instance("St",Raw("State location"),Raw("OnlyLocation (fun _ => True)")) ::[]) (**[instance_byzantine x] ​​returns a list of stmt allowing to generate the coq code to instantiate the byzantines @param int x corresponds to the proportion of Byzantine desired (1/8 -> x = 8) @@ -259,8 +269,8 @@ let instance_sensors (s:sensor list) : stmt list = @return stmt *) let require_rigidity (r: rigidity) :stmt = match r with - | Flexible _ -> Require(true,["Pactole.Models.Flexible"]) - | Rigide -> Require(true,["Pactole.Models.Rigid";"Pactole.Models.Similarity"]) + | Flexible _ -> Require(true,["Pactole.Models.Flexible";"Pactole.Spaces.Similarity"]) + | Rigide -> Require(true,["Pactole.Models.Rigid";"Pactole.Models.Similarity";"Pactole.Spaces.Similarity"]) (**[require_space s] returns an stmt allowing to generate the require for space [s] @@ -327,7 +337,13 @@ let valret = get_val_ret world in @return stmt list*) let generate_robogram (r : expr list) (d: information list) : stmt list = let valret = get_val_ret d in - let valretcoq = if get_rigidity d = "Flexible" then "(path " ^ valret ^ ")" else valret in + let rc_return = + match valret with + | x ::[] -> x + | _ ::_ -> String.concat " * " valret + | [] -> raise(Failure " Error return value") in + + let valretcoq = if get_rigidity d = "Flexible" then "(path location)" else rc_return in match (List.map expr_to_coq r) with | 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 -- GitLab