prettyprint sur les lemmes

lib/gencoq.ml

@@ -351,21 +351,29 @@ let generate_robogram (r : expr list) (d: information list) : stmt list =
   | [] ->  Def ("Robogram_pgm (s : observation)",Raw(valretcoq),Raw("[]")) ::[]
 
 
+(**[generate_or l] retourne la formule or a partir d'une liste de string 
+    @param string list
+    @return [Formula.t]*)
+let rec generate_or l= 
+match l with 
+  | h::[] -> Formula.Cst(h)
+  | h::tl -> Or(Cst(h),generate_or tl) 
+  | _ -> Cst("")
+
 
 (**[generate_lemmas g] retourne la liste de stmt correspondant aux lemmes extrait du graph g
     @param g [G.t]
     @return [stmt list]*)
 let generate_lemmas (g : Ast.G.t) : (stmt list * string list) =
     Ast.G.fold_vertex (fun v (acc,s) ->
+    let string_v = string_of_expression v in
     let succs = Ast.G.succ g v in
-    let forall v =
-      String.concat " " (List.map string_of_expression (Ast.get_param v))
-    in
     if succs <> [] then
       let string_succs = (List.map string_of_expression succs) in
-      let rcs = List.map (fun x -> x ^ " (round Robogram da config)") string_succs in
-      (Lemma("lem_"^string_of_expression v^"_next_"^String.concat "_or_" string_succs,Forall(("config "^forall v),Raw(string_of_expression v^" config -> ("^String.concat " \\/ " rcs^")")),[])::acc,
-      ("("^string_of_expression v ^" config )")::s)
+      let rcs = List.map (fun x -> x ^ " (round Robogram da config)") (string_v::string_succs) in
+      (Lemma("lem_"^string_v^"_next_"^String.concat "_or_" string_succs,
+            Forall("config",InfixOp(Raw(string_v^" config"),"->",(generate_or rcs) )),[])::acc,
+      ("("^string_v ^" config)")::s)
     else
       (acc,s)
     ) g ([],[])
@@ -380,7 +388,7 @@ let generate_measure (Measure(i,g): measure) : stmt list =
   let to_change = String.concat ","(List.init i (fun _ ->"0%nat"))in
   Ast.png_from_graph g;
   let lemsgen = let lems = generate_lemmas g in 
-    Lemma("InGraph",Forall("config",Raw(String.concat " \\/ " (snd lems))),[])
+    Lemma("InGraph",Forall("config",generate_or (snd lems)),[])
     ::List.rev (fst lems) in 
   RawCoq(["Function measure (s : observation) : "^ret ^" := 
             ("^to_change^")."; (*TODO: *)