diff --git a/lib/ast.ml b/lib/ast.ml
index c865a8d086a272512f55792c447d9ec64bfd5528..5ddc16b0a68070ed68e920905455f0ba960dbf3a 100644
--- a/lib/ast.ml
+++ b/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
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index a95240015e92ffb4b5410d4ab5d29291944491cb..bf967b376cb7ab11130cdab7c40e78fc9b6ee1b5 100644
--- a/lib/gencoq.ml
+++ b/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