Correction require similarity

+ Ajout possibilité d'utiliser un Ring quelconque

lib/gencoq.ml

@@ -16,7 +16,7 @@ let correspondance = [("Geometry",geometry);
                      ("Obs",observation);
                      ("Directions",direction)]
 let newline =RawCoq([" "])
-let proof_to_complete = [Comment("Preuve");RawCoq(["Admitted."])]
+let proof_to_complete = [Comment("Proof");RawCoq(["Admitted."])]
 
 (** [get_nb_byz infos] retourne le nombre de byzantins désirés
     @param information list correspondant à la description du monde
@@ -152,11 +152,13 @@ let instance_R_R2 (s:space) (d: information list): stmt list =
 (**[instance_Ring n] genere le code coq pour instancier un Ring
     @param int n 
     @return [stmt list]*)
-let instance_Ring (n:int) : 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"]))::[]
-
+  else
+    RawCoq(["Context {RR : RingSpec}."])::[]
 
 (**[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
@@ -167,12 +169,16 @@ let instance_space (s: space) (d : information list): stmt list =
   match s with  
   | R -> instance_R_R2 s d
   | R2 -> instance_R_R2 s d
-  | ZnZ n -> instance_Ring n
+  | ZnZ n -> instance_ring n
   | _ ->raise(Failure ("Not implemanted")) 
   in 
   s'@[]
 
-let instance_updfunc_Rigide (valret : string) :stmt  =
+(**[instane_updfunc_rigid valret] retourne le code coq pour instancier la fonction d'update
+  @param string valeur de retour du robogram
+  @return stmt 
+    *)
+let instance_updfunc_rigid (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 =
@@ -188,7 +194,7 @@ 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_updfunc_Rigide valret
+                  :: instance_updfunc_rigid 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^"}")) 
@@ -258,7 +264,7 @@ let instance_sensors (s:sensor list) : stmt list =
 let require_rigidity (r: rigidity) :stmt =
   match r with
   | Flexible _ -> Require(true,["Pactole.Models.Flexible"])
-  | Rigide -> Require(true,["Pactole.Models.Rigid"])
+  | Rigide -> Require(true,["Pactole.Models.Rigid";"Pactole.Models.Similarity"])
 
 
 (**[require_space s] retourne un stmt permettant de generer le require pour l'espace [s]

lib/parser.mly

@@ -126,6 +126,7 @@ ints :
     | R2M {R2m}
     /*Anneau ZnZ avec n donnée*/
     | ANNEAU n = INT {ZnZ(n)}
+    | ANNEAU {ZnZ(0)}
 /*
 %inline capacity :
     /*(Lumiere : l) */