1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** 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 type SetS =
sig
type t
type elt
val singleton : elt -> t
val union : t -> t -> t
val choose : t -> elt
val iter : (elt -> unit) -> t -> unit
end
(** Minimal interface for sets, subtype of stdlib's Set. *)
module type MapS =
sig
type key
type +'a t
val empty : 'a t
val find : key -> 'a t -> 'a
val add : key -> 'a -> 'a t -> 'a t
val mem : key -> 'a t -> bool
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
end
(** Minimal interface for maps, subtype of stdlib's Map. *)
module Make :
functor (S:SetS) ->
functor (_:MapS with type key = S.elt) ->
PartitionSig with type elt = S.elt and type set = S.t
|