typo

lib/gencoq.ml

@@ -77,11 +77,12 @@ let multi (s:sensor list) : bool =
 
 
 
+
 (** [expr_to_coq r] returns a Formula.t type expression (ast to write coq by PCourtieux) corresponding to the given expression r
     @param expr DSL ast expression to convert to Formula.t
     @return [Formula.t]*)
 let rec expr_to_coq (r : expr) : Formula.t =
-
+  let  module StringMap = Map.Make(String) in
       match r with
       | Cst c -> Int c
       | PatternMatching (e1,l) -> Match((expr_to_coq e1),List.map (fun x -> match x with | e2,e3 -> (expr_to_coq e2,expr_to_coq e3)) l)
@@ -106,10 +107,10 @@ let rec expr_to_coq (r : expr) : Formula.t =
       | Fun (s,e) -> Fun(Some s, expr_to_coq e)
       | App (f,arg) -> App(expr_to_coq f, [expr_to_coq arg])
       | Set s -> Set (set_to_coq s)
-      | Point (m,f) -> let c = List.assoc_opt m Module.correspondance in 
+      | Point (m,f) -> let c = StringMap.find_opt  m Module.correspondance in 
                        (match c with
                         |None -> raise(Failure("Problem: "^m^" unknow"))
-                        |Some x -> (match List.assoc_opt f x with
+                        |Some x -> (match StringMap.find_opt  f x with
                                   | None -> raise(Failure("Problem "^m^"."^f^" unknow"))
                                   |  Some x' -> x')
                         )
@@ -197,7 +198,7 @@ let instance_rigidity (r:rigidity) (valret : string list) (world: information li
     | [] -> raise(Failure " Error return value") in 
 
   match r with(*TODO: Est-ce la bonne maniere d'ecrire l'UpdateFunc?*)
-  | Rigide -> print_endline(rc_setoid);    Instance("RC",Raw("robot_choice "^rc_return),Raw("{ robot_choice_Setoid := "^rc_setoid^"}")) 
+  | Rigide ->      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 (rc_return) world
                   

lib/module.ml

+module StringMap = Map.Make(String)
 
+let geometry = StringMap.empty
+  |> StringMap.add "isobarycenter" (Formula.Raw "isobarycenter")
+  |> StringMap.add "barycenter" (Formula.Raw "barycenter")
+  |> StringMap.add "on_SEC" (Formula.Raw "on_SEC")
 
-let geometry =[("isobarycenter",Formula.Raw("isobarycenter"));
-               ("barycenter",Formula.Raw("barycenter"));
-                ("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);
-                     ("Directions",direction)]
\ No newline at end of file
+let observation = StringMap.empty
+  |> StringMap.add "elements" (Formula.Raw "(elements s)")
+  |> StringMap.add "support" (Formula.Raw "support s")
+
+let direction= StringMap.empty
+  |> StringMap.add "forward" (Formula.Raw "Forward")
+  |> StringMap.add "backward" (Formula.Raw "Backward")
+  |> StringMap.add "selfloop" (Formula.Raw "Selfloop")
+
+let correspondance = StringMap.empty
+  |> StringMap.add "Geometry" geometry
+  |> StringMap.add "Obs" observation
+  |> StringMap.add "Directions" direction
\ No newline at end of file