From 09595eca470734537144b4233b81256a260f2cd0 Mon Sep 17 00:00:00 2001
From: Kylian Fontaine <kylian.fontaine@etu.univ-lyon1.fr>
Date: Mon, 15 Jul 2024 11:43:52 +0200
Subject: [PATCH] typo
---
lib/gencoq.ml | 9 +++++----
lib/module.ml | 29 ++++++++++++++++++-----------
2 files changed, 23 insertions(+), 15 deletions(-)
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index faebedd..3c2a4b1 100644
--- a/lib/gencoq.ml
+++ b/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
diff --git a/lib/module.ml b/lib/module.ml
index 08a73e9..f776498 100644
--- a/lib/module.ml
+++ b/lib/module.ml
@@ -1,13 +1,20 @@
+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
--
GitLab