1 files changed, 48 insertions, 12 deletions

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index e4e3650c7..b61279cd5 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -47,6 +47,18 @@ let display_system_flag = ref false
 let display_action_flag = ref false
 let old_style_flag = ref false
 
+(* Should we reset all variable labels between two runs of omega ? *)
+
+let reset_flag = ref true
+
+(* Coq < 8.5 was not performing such resets, hence omega was slightly
+   non-deterministic: successive runs of omega on the same problem may
+   lead to distinct proof-terms.
+   At the very least, these terms differed on the inner
+   variable names, but they could even be non-convertible :
+   the OmegaSolver relies on Hashtbl.iter, it can hence find a different
+   solution when variable indices differ. *)
+
 let read f () = !f
 let write f x = f:=x
 
@@ -79,31 +91,44 @@ let _ =
       optread  = read old_style_flag;
       optwrite = write old_style_flag }
 
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = true;
+      optname  = "Omega automatic reset of generated names";
+      optkey   = ["Stable";"Omega"];
+      optread  = read reset_flag;
+      optwrite = write reset_flag }
+
+let intref, reset_all_references =
+  let refs = ref [] in
+  (fun n -> let r = ref n in refs := (r,n) :: !refs; r),
+  (fun () -> List.iter (fun (r,n) -> r:=n) !refs)
 
 let new_identifier =
-  let cpt = ref 0 in
+  let cpt = intref 0 in
   (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s)
 
 let new_identifier_state =
-  let cpt = ref 0 in
+  let cpt = intref 0 in
   (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s)
 
 let new_identifier_var =
-  let cpt = ref 0 in
+  let cpt = intref 0 in
   (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s)
 
 let new_id =
-  let cpt = ref 0 in fun () -> incr cpt; !cpt
+  let cpt = intref 0 in fun () -> incr cpt; !cpt
 
 let new_var_num =
-  let cpt = ref 1000 in (fun () -> incr cpt; !cpt)
+  let cpt = intref 1000 in (fun () -> incr cpt; !cpt)
 
 let new_var =
-  let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt)
+  let cpt = intref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt)
 
 let display_var i = Printf.sprintf "X%d" i
 
-let intern_id,unintern_id =
+let intern_id,unintern_id,reset_intern_tables =
   let cpt = ref 0 in
   let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in
   (fun (name : Id.t) ->
@@ -115,7 +140,8 @@ let intern_id,unintern_id =
   (fun idx ->
      try Hashtbl.find co_table idx with Not_found ->
        let v = new_var () in
-       Hashtbl.add table v idx; Hashtbl.add co_table idx v; v)
+       Hashtbl.add table v idx; Hashtbl.add co_table idx v; v),
+  (fun () -> cpt := 0; Hashtbl.clear table)
 
 let mk_then = tclTHENLIST
 
@@ -134,13 +160,14 @@ let rev_assoc k =
   in
   loop
 
-let tag_hypothesis,tag_of_hyp, hyp_of_tag =
+let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags =
   let l = ref ([]:(Id.t * int) list) in
   (fun h id -> l := (h,id):: !l),
   (fun h -> try Id.List.assoc h !l with Not_found -> failwith "tag_hypothesis"),
-  (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis")
+  (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"),
+  (fun () -> l := [])
 
-let hide_constr,find_constr,clear_tables,dump_tables =
+let hide_constr,find_constr,clear_constr_tables,dump_tables =
   let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in
   (fun h id eg b -> l := (h,(id,eg,b)):: !l),
   (fun h ->
@@ -148,6 +175,14 @@ let hide_constr,find_constr,clear_tables,dump_tables =
   (fun () -> l := []),
   (fun () -> !l)
 
+let reset_all () =
+  if !reset_flag then begin
+    reset_all_references ();
+    reset_intern_tables ();
+    clear_tags ();
+    clear_constr_tables ()
+  end
+
 (* Lazy evaluation is used for Coq constants, because this code
  is evaluated before the compiled modules are loaded.
  To use the constant Zplus, one must type "Lazy.force coq_Zplus"
@@ -1381,7 +1416,7 @@ open Proofview.Notations
 
 let coq_omega =
   Proofview.Goal.enter begin fun gl ->
-  clear_tables ();
+  clear_constr_tables ();
   let hyps_types = Tacmach.New.pf_hyps_types gl in
   let destructure_omega = Tacmach.New.of_old destructure_omega gl in
   let tactic_normalisation, system =
@@ -1828,4 +1863,5 @@ let destructure_goal = destructure_goal
 let omega_solver =
   Proofview.tclUNIT () >= fun () -> (* delay for [check_required_library] *)
   Coqlib.check_required_library ["Coq";"omega";"Omega"];
+  reset_all ();
   destructure_goal