An generic imperative union-find, used for deps of evars in Class_tactics

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

4 files changed, 195 insertions, 26 deletions

diff --git a/lib/lib.mllib b/lib/lib.mllib
index 90b90cb4f..cfbedcc52 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -23,3 +23,4 @@ Heap
 Option
 Dnet
 Store
+Unionfind
\ No newline at end of file
diff --git a/lib/unionfind.ml b/lib/unionfind.ml
new file mode 100644
index 000000000..b05f8de0c
--- /dev/null
+++ b/lib/unionfind.ml
@@ -0,0 +1,115 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** An imperative implementation of partitions via Union-Find *)
+
+(** Paths are compressed imperatively at each lookup of a
+    canonical representative. Each union also modifies in-place
+    the partition structure.
+
+    Nota: For the moment we use Pervasive's comparison for
+    choosing the smallest object as representative. This could
+    be made more generic.
+*)
+
+
+
+module type PartitionSig = sig
+
+  (** The type of elements in the partition *)
+  type elt
+
+  (** A set structure over elements *)
+  type set
+
+  (** The type of partitions *)
+  type t
+
+  (** Initialise an empty partition *)
+  val create : unit -> t
+
+  (** Add (in place) an element in the partition, or do nothing
+      if the element is already in the partition. *)
+  val add : elt -> t -> unit
+
+  (** Find the canonical representative of an element.
+      Raise [not_found] if the element isn't known yet. *)
+  val find : elt -> t -> elt
+
+  (** Merge (in place) the equivalence classes of two elements.
+      This will add the elements in the partition if necessary. *)
+  val union : elt -> elt -> t -> unit
+
+  (** Merge (in place) the equivalence classes of many elements. *)
+  val union_set : set -> t -> unit
+
+  (** Listing the different components of the partition *)
+  val partition : t -> set list
+
+end
+
+module Make (S:Set.S)(M:Map.S with type key = S.elt) = struct
+
+  type elt = S.elt
+  type set = S.t
+
+  type node =
+    | Canon of set
+    | Equiv of elt
+
+  type t = node ref M.t ref
+
+  let create () = ref (M.empty : node ref M.t)
+
+  let fresh x p =
+    let node = ref (Canon (S.singleton x)) in
+    p := M.add x node !p;
+    x, node
+
+  let rec lookup x p =
+    let node = M.find x !p in
+    match !node with
+      | Canon _ -> x, node
+      | Equiv y ->
+	let ((z,_) as res) = lookup y p in
+	if not (z == y) then node := Equiv z;
+	res
+
+  let add x p = if not (M.mem x !p) then ignore (fresh x p)
+
+  let find x p = fst (lookup x p)
+
+  let canonical x p = try lookup x p with Not_found -> fresh x p
+
+  let union x y p =
+    let ((x,_) as xcan) = canonical x p in
+    let ((y,_) as ycan) = canonical y p in
+    if x = y then ()
+    else
+      let xcan, ycan = if x < y then xcan, ycan else ycan, xcan in
+      let x,xnode = xcan and y,ynode = ycan in
+      match !xnode, !ynode with
+	| Canon lx, Canon ly ->
+	  xnode := Canon (S.union lx ly);
+	  ynode := Equiv x;
+	| _ -> assert false
+
+  let union_set s p =
+    try
+      let x = S.min_elt s in
+      S.iter (fun y -> union x y p) s
+    with Not_found -> ()
+
+  let partition p =
+    List.rev (M.fold
+		(fun x node acc -> match !node with
+		  | Equiv _ -> acc
+		  | Canon lx -> lx::acc)
+		!p [])
+
+end
diff --git a/lib/unionfind.mli b/lib/unionfind.mli
new file mode 100644
index 000000000..07ee7c2b7
--- /dev/null
+++ b/lib/unionfind.mli
@@ -0,0 +1,57 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** An imperative implementation of partitions via Union-Find *)
+
+(** Paths are compressed imperatively at each lookup of a
+    canonical representative. Each union also modifies in-place
+    the partition structure.
+
+    Nota: for the moment we use Pervasive's comparison for
+    choosing the smallest object as representative. This could
+    be made more generic.
+*)
+
+module type PartitionSig = sig
+
+  (** The type of elements in the partition *)
+  type elt
+
+  (** A set structure over elements *)
+  type set
+
+  (** The type of partitions *)
+  type t
+
+  (** Initialise an empty partition *)
+  val create : unit -> t
+
+  (** Add (in place) an element in the partition, or do nothing
+      if the element is already in the partition. *)
+  val add : elt -> t -> unit
+
+  (** Find the canonical representative of an element.
+      Raise [not_found] if the element isn't known yet. *)
+  val find : elt -> t -> elt
+
+  (** Merge (in place) the equivalence classes of two elements.
+      This will add the elements in the partition if necessary. *)
+  val union : elt -> elt -> t -> unit
+
+  (** Merge (in place) the equivalence classes of many elements. *)
+  val union_set : set -> t -> unit
+
+  (** Listing the different components of the partition *)
+  val partition : t -> set list
+
+end
+
+module Make :
+  functor (S:Set.S) ->
+    functor (M:Map.S with type key = S.elt) ->
+      PartitionSig with type elt = S.elt and type set = S.t
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6300c699b..251b93c87 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -60,9 +60,6 @@ let evars_to_goals p evm =
 
 (** Typeclasses instance search tactic / eauto *)
 
-let intersects s t =
-  Intset.exists (fun el -> Intset.mem el t) s
-
 open Auto
 
 let e_give_exact flags c gl = 
@@ -462,34 +459,33 @@ let has_undefined p oevd evd =
     snd (p oevd ev evi))
     evd false
 
-let rec merge_deps deps = function
-  | [] -> [deps]
-  | hd :: tl ->
-      if intersects deps hd then
-	merge_deps (Intset.union deps hd) tl
-      else hd :: merge_deps deps tl
-
-let deps_of_constraints cstrs deps evm =
-  List.fold_right (fun (_, _, x, y) deps ->
-    let evx = Evarutil.undefined_evars_of_term evm x
-    and evy = Evarutil.undefined_evars_of_term evm y
-    in merge_deps (Intset.union evx evy) deps)
-    cstrs deps
-
-let evar_dependencies evm =
+(** We compute dependencies via a union-find algorithm.
+    Beware of the imperative effects on the partition structure,
+    it should not be shared, but only used locally. *)
+
+module Intpart = Unionfind.Make(Intset)(Intmap)
+
+let deps_of_constraints cstrs evm p =
+  List.iter (fun (_, _, x, y) ->
+    let evx = Evarutil.undefined_evars_of_term evm x in
+    let evy = Evarutil.undefined_evars_of_term evm y in
+    Intpart.union_set (Intset.union evx evy) p)
+    cstrs
+
+let evar_dependencies evm p =
   Evd.fold_undefined
-    (fun ev evi acc ->
-      merge_deps
-	(Intset.add ev (Evarutil.undefined_evars_of_evar_info evm evi)) acc)
-    evm []
+    (fun ev evi _ ->
+      let evars = Intset.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
+      in Intpart.union_set evars p)
+    evm ()
 
 (** [split_evars] returns groups of undefined evars according to dependencies *)
 
 let split_evars evm =
-  let _, cstrs = extract_all_conv_pbs evm in
-  let evmdeps = evar_dependencies evm in
-  let deps = deps_of_constraints cstrs evmdeps evm in
-    List.sort Intset.compare deps
+  let p = Intpart.create () in
+  evar_dependencies evm p;
+  deps_of_constraints (snd (extract_all_conv_pbs evm)) evm p;
+  Intpart.partition p
 
 let select_evars evs evm =
   try