Debut instance ring, updfunc et framechoice à faire

lib/ast.ml

@@ -294,7 +294,7 @@ match e with
   | Rm -> "Rm"
   | R2 -> "R2"
   | R2m  ->"R2m"
-  | ZnZ n -> "Z/"^ string_of_int n ^"Z"
+  | ZnZ _ -> "Ring"
   
 let string_of_color (c : color) : string =
   match c with

lib/gencoq.ml

@@ -9,8 +9,12 @@ let geometry =[("isobarycenter",Formula.Raw("isobarycenter"));
                 ("on_SEC"),Formula.Raw("on_SEC")]
 let observation =[("elements", Formula.Raw("(elements s)"));
                   ("support"), Formula.Raw("support s")]
+let direction =[("forward",Formula.Raw("Forward"));
+                ("backward",Formula.Raw("Backward"));
+                ("selfloop",Formula.Raw("Selfloop"));]
 let correspondance = [("Geometry",geometry);
-                     ("Obs",observation)]
+                     ("Obs",observation);
+                     ("Directions",direction)]
 let newline =RawCoq([" "])
 let proof_to_complete = [Comment("Preuve");RawCoq(["Admitted."])]
 
@@ -125,30 +129,55 @@ let rec expr_to_coq (r : expr) : Formula.t =
         | Vide -> []
         | Some (s',e) -> string_of_expression e :: set_to_coq s'
 
-(**[instance_space s] retourne une liste de stmt permettant de generer le code coq pour instancier l'espace s
-        @param space espace [s] à instancier pour le moment seulement R, R2, Ring
-        @return [stmt list]
-          *)
-let instance_space (s: space) (d : information list): stmt list =
-  let s' =
-  match s with  
-  | R -> "R"
-  | R2 -> "R2"
-  | ZnZ _ ->  "Ring" 
-  | _ ->raise(Failure ("Not implemanted")) 
-  in
+
+(**[instance_R_R2 s d] genere le code coq pour instancer R et R2
+  @param space s 
+  @param information list d
+  @return [stmt list]
+    *)
+let instance_R_R2 (s:space) (d: information list): stmt list =
+  let s' = string_of_espace s in
   let path = if get_rigidity d = "Flexible" then  (* pour chemin droit TODO: check si on ne veut pas de chemin droit, et donc trouve une syntaxe pour le dsl *)
     RawCoq(["Definition path_"^s'^ ":= path location."])
     ::Def("paths_in_"^s',Imply(Raw("location"),Raw("path_"^s')),Raw("local_straight_path")) 
     ::RawCoq(["Coercion paths_in_"^s'^" :location >-> path_"^s'^"."])
     ::[]
   else 
-    []
-  in
-    Instance("Loc",Var(0,"Location"),App(Var(0,"make_Location"),[Var(0,s')]))
+  []
+  in 
+  Instance("Loc",Var(0,"Location"),App(Var(0,"make_Location"),[Var(0,s')]))
   ::Instance("VS",Var(0,"RealVectorSpace location"),Var(0,s'^"_VS"))
-  ::Instance("ES",Var(0,"EuclideanSpace location"),Var(0,s'^"_ES"))
-  ::path@[]
+  ::Instance("ES",Var(0,"EuclideanSpace location"),Var(0,s'^"_ES"))::path
+
+(**[instance_Ring n] genere le code coq pour instancier un Ring
+    @param int n 
+    @return [stmt list]*)
+let instance_Ring (n:int) : stmt list =
+  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"]))::[]
+
+
+(**[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
+        @return [stmt list]
+          *)
+let instance_space (s: space) (d : information list): stmt list =
+  let s' =
+  match s with  
+  | R -> instance_R_R2 s d
+  | R2 -> instance_R_R2 s d
+  | ZnZ n -> instance_Ring n
+  | _ ->raise(Failure ("Not implemanted")) 
+  in 
+  s'@[]
+
+let instance_updfunc_Rigide (valret : string) :stmt  =
+  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 =
+  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 
         @param rigidity rigidite [r] à instancier 
@@ -156,18 +185,18 @@ let instance_space (s: space) (d : information list): stmt list =
         @return [stmt list]
           *)
 let instance_rigidity (r:rigidity) (valret : string) : 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("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."])
-                ::[]
-| 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("UpdateFunc",Raw("update_function (path "^valret^") (Similarity.similarity "^valret^") ratio"),Raw("  FlexibleUpdate delta"))
-                ::[]
-      ) 
+  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_Rigide valret
+                  ::RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])
+                  ::[]
+  | 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
         @param field list  list de champs à instancier
@@ -282,14 +311,12 @@ let valret = get_val_ret world in
   let rec genworld w = match w with
   | [] -> []
   | h::t-> (match h with 
-          | Space s ->newline::(instance_space s world) @ genworld t
-          | Rigidity r ->genworld t @newline::(instance_rigidity r valret) 
+          | Space s -> newline::(instance_space s world) @ genworld t
+          | Rigidity r -> genworld t @newline::(instance_rigidity r valret) 
           | Robot r -> newline::(instance_info r) @ genworld t
-          | Sync s ->genworld t @(instance_sync s) 
+          | Sync s -> genworld t @(instance_sync s) 
           | Sensors s -> genworld t @ (instance_sensors s)
-          | _ ->genworld t) in
-  
-  
+          | _ -> genworld t) in
    (Var("n",Raw "nat")::instance_byzantine nb_byz)@(genworld world)
 
 (**[generate_robogram r d] retourne une liste de stmt permettant de generer le code coq du robogram