diff --git a/lib/gencoq.ml b/lib/gencoq.ml index bfca44430b265843ef9bed97398a031a9ee53f83..f991f9f97ac8b3e1ca9a471122bce6586f6c5f0d 100644 --- a/lib/gencoq.ml +++ b/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: *)