modification sur valeur de retour du robogram -> light

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