correctifs de bug pour romega:

1) dans refl_omega, on donnait a OmegaSolver un generateur de numero
d'equations new_eq_id qui pouvait clasher avec les numeros d'equations 
initiaux créés avec new_omega_id.
=> 
on sépare en deux compteurs, un pour les equations omegas, l'autre 
pour les variables omegas. On en profite pour reinitialiser ces 
compteurs à chaque session romega, histoire que romega devienne 
reproductible. 

2) dans omega.ml, le role de new_eq_id et new_var_id etait interverti 
à un endroit. 
ATTENTION: ceci peut changer le comportement d'omega. Surveiller le 
resultat du prochain bench nocturne. 

3) dans ReflOmegaCore.v, on ne traitait pas le cas d'une implication 
dans une hypothese lors du recalcul final. 




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8657 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 39 insertions, 13 deletions

diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml
index 69e57ca42e..fd774c16d0 100644
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
@@ -512,7 +512,7 @@ let product new_eq_id dark_shadow low high =
          accu high)
     [] low
 
-let fourier_motzkin (_,new_eq_id,print_var) dark_shadow system =
+let fourier_motzkin (new_eq_id,_,print_var) dark_shadow system =
   let v = select_variable system in
   let (ineq_out, ineq_low,ineq_high) = classify v system in
   let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index fbe4157072..2aa3516f1d 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -2624,6 +2624,10 @@ Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps :=
            decompose_solve s1 (Tnot x :: h) ++
            decompose_solve s2 (Tnot y :: h)
           else h :: nil
+      | Timp x y => 
+          if decidability x then 
+            decompose_solve s1 (Tnot x :: h) ++ decompose_solve s2 (y :: h)
+          else h::nil
       | _ => h :: nil
       end
   | E_EXTRACT i dl s1 =>
@@ -2647,13 +2651,19 @@ intro s; apply goal_valid; unfold valid_list_hyps in |- *; elim s;
           | simpl in |- *; auto ]
        | intros p1 p2 H2; apply append_valid; simpl in |- *; elim H2;
           [ intros H3; left; apply H; simpl in |- *; auto
-          | intros H3; right; apply H0; simpl in |- *; auto ] ]
+          | intros H3; right; apply H0; simpl in |- *; auto ] 
+       | intros p1 p2 H2;
+         pattern (decidability p1) in |- *; apply bool_ind2;
+          [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4;
+             apply append_valid; elim H4; intro H5; 
+             [ right; apply H0; simpl in |- *; tauto
+             | left; apply H; simpl in |- *; tauto ]
+          | simpl in |- *; auto ] ]
     | elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto ]
  | intros; apply H; simpl in |- *; split;
     [ elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto
     | auto ]
  | apply omega_valid with (1 := H) ].
-
 Qed.
 
 (* \subsection{La dernière étape qui élimine tous les séquents inutiles} *)
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index c552da6212..99fafd2638 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -204,7 +204,7 @@ let new_environment () = {
 }
 
 (* Génération d'un nom d'équation *)
-let new_eq_id env =
+let new_connector_id env =  
    env.cnt_connectors <- succ env.cnt_connectors; env.cnt_connectors
 
 (* Calcul de la branche complémentaire *)
@@ -229,9 +229,23 @@ let print_env_reification env =
 
 (* \subsection{Gestion des environnements de variable pour Omega} *)
 (* generation d'identifiant d'equation pour Omega *)
-let new_omega_id = let cpt = ref 0 in function () -> incr cpt; !cpt
+
+let new_omega_eq, rst_omega_eq = 
+  let cpt = ref 0 in 
+  (function () -> incr cpt; !cpt), 
+  (function () -> cpt:=0)
+
+(* generation d'identifiant de variable pour Omega *)
+
+let new_omega_var, rst_omega_var = 
+  let cpt = ref 0 in 
+  (function () -> incr cpt; !cpt), 
+  (function () -> cpt:=0)
+
 (* Affichage des variables d'un système *)
-let display_omega_id i = Printf.sprintf "O%d" i
+
+let display_omega_var i = Printf.sprintf "OV%d" i
+
 (* Recherche la variable codant un terme pour Omega et crée la variable dans
    l'environnement si il n'existe pas. Cas ou la variable dans Omega représente
    le terme d'un monome (le plus souvent un atome) *)
@@ -239,7 +253,7 @@ let display_omega_id i = Printf.sprintf "O%d" i
 let intern_omega env t =
   begin try List.assoc t env.om_vars
   with Not_found -> 
-    let v = new_omega_id () in 
+    let v = new_omega_var () in 
     env.om_vars <- (t,v) :: env.om_vars; v
   end
 
@@ -335,7 +349,7 @@ let omega_of_oformula env kind =
     | Oplus(Omult(v,Oint n),r) -> 
 	loop ({v=intern_omega env v; c=n} :: accu) r
     | Oint n ->
-	let id = new_omega_id () in
+	let id = new_omega_eq () in
 	(*i tag_equation name id; i*)
 	{kind = kind; body = List.rev accu; 
 	 constant = n; id = id}
@@ -443,7 +457,7 @@ let reified_of_omega env body c  =
   begin try 
     reified_of_omega env body c 
   with e -> 
-    display_eq display_omega_id (body,c); raise e 
+    display_eq display_omega_var (body,c); raise e 
   end
 
 (* \section{Opérations sur les équations}
@@ -728,7 +742,7 @@ and  binop env c t1 t2 =
 
 and  binprop env (neg2,depends,origin,path) 
              add_to_depends neg1 gl c t1 t2 =
-  let i = new_eq_id env in
+  let i = new_connector_id env in
   let depends1 = if add_to_depends then Left i::depends else depends in
   let depends2 = if add_to_depends then Right i::depends else depends in
   if add_to_depends then
@@ -875,7 +889,7 @@ let display_systems syst_list =
   let display_omega om_e = 
     Printf.printf "  E%d : %a %s 0\n"
       om_e.id
-      (fun _ -> display_eq display_omega_id) 
+      (fun _ -> display_eq display_omega_var) 
       (om_e.body, om_e.constant)
       (operator_of_eq om_e.kind) in
 
@@ -1209,14 +1223,14 @@ let resolution env full_reified_goal systems_list =
     let system = List.map (fun eq -> eq.e_omega) list_eq in
     let trace = 
       simplify_strong 
-	((fun () -> new_eq_id env),new_omega_id,display_omega_id) 
+	(new_omega_eq,new_omega_var,display_omega_var) 
 	system in 
     (* calcule les hypotheses utilisées pour la solution *)
     let vars = hyps_used_in_trace trace in
     let splits = get_eclatement env vars in
     if !debug then begin
       Printf.printf "SYSTEME %d\n" index;
-      display_action display_omega_id trace;
+      display_action display_omega_var trace;
       print_string "\n  Depend :";
       List.iter (fun i -> Printf.printf " %d" i) vars;
       print_string "\n  Split points :";
@@ -1309,6 +1323,8 @@ let resolution env full_reified_goal systems_list =
 
 let total_reflexive_omega_tactic gl = 
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
+  rst_omega_eq (); 
+  rst_omega_var ();
   try
   let env = new_environment () in
   let full_reified_goal = reify_gl env gl in