summaryrefslogtreecommitdiff
path: root/lib/hMap.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/hMap.ml')
-rw-r--r--lib/hMap.ml332
1 files changed, 332 insertions, 0 deletions
diff --git a/lib/hMap.ml b/lib/hMap.ml
new file mode 100644
index 00000000..f902eded
--- /dev/null
+++ b/lib/hMap.ml
@@ -0,0 +1,332 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+module type HashedType =
+sig
+ type t
+ val compare : t -> t -> int
+ val hash : t -> int
+end
+
+module SetMake(M : HashedType) =
+struct
+ (** Hash Sets use hashes to prevent doing too many comparison tests. They
+ associate to each hash the set of keys having that hash.
+
+ Invariants:
+
+ 1. There is no empty set in the intmap.
+ 2. All values in the same set have the same hash, which is the int to
+ which it is associated in the intmap.
+ *)
+
+ module Set = Set.Make(M)
+
+ type elt = M.t
+
+ type t = Set.t Int.Map.t
+
+ let empty = Int.Map.empty
+
+ let is_empty = Int.Map.is_empty
+
+ let mem x s =
+ let h = M.hash x in
+ try
+ let m = Int.Map.find h s in
+ Set.mem x m
+ with Not_found -> false
+
+ let add x s =
+ let h = M.hash x in
+ try
+ let m = Int.Map.find h s in
+ let m = Set.add x m in
+ Int.Map.update h m s
+ with Not_found ->
+ let m = Set.singleton x in
+ Int.Map.add h m s
+
+ let singleton x =
+ let h = M.hash x in
+ let m = Set.singleton x in
+ Int.Map.singleton h m
+
+ let remove x s =
+ let h = M.hash x in
+ try
+ let m = Int.Map.find h s in
+ let m = Set.remove x m in
+ if Set.is_empty m then
+ Int.Map.remove h s
+ else
+ Int.Map.update h m s
+ with Not_found -> s
+
+ let union s1 s2 =
+ let fu _ m1 m2 = match m1, m2 with
+ | None, None -> None
+ | (Some _ as m), None | None, (Some _ as m) -> m
+ | Some m1, Some m2 -> Some (Set.union m1 m2)
+ in
+ Int.Map.merge fu s1 s2
+
+ let inter s1 s2 =
+ let fu _ m1 m2 = match m1, m2 with
+ | None, None -> None
+ | Some _, None | None, Some _ -> None
+ | Some m1, Some m2 ->
+ let m = Set.inter m1 m2 in
+ if Set.is_empty m then None else Some m
+ in
+ Int.Map.merge fu s1 s2
+
+ let diff s1 s2 =
+ let fu _ m1 m2 = match m1, m2 with
+ | None, None -> None
+ | (Some _ as m), None -> m
+ | None, Some _ -> None
+ | Some m1, Some m2 ->
+ let m = Set.diff m1 m2 in
+ if Set.is_empty m then None else Some m
+ in
+ Int.Map.merge fu s1 s2
+
+ let compare s1 s2 = Int.Map.compare Set.compare s1 s2
+
+ let equal s1 s2 = Int.Map.equal Set.equal s1 s2
+
+ let subset s1 s2 =
+ let check h m1 =
+ let m2 = try Int.Map.find h s2 with Not_found -> Set.empty in
+ Set.subset m1 m2
+ in
+ Int.Map.for_all check s1
+
+ let iter f s =
+ let fi _ m = Set.iter f m in
+ Int.Map.iter fi s
+
+ let fold f s accu =
+ let ff _ m accu = Set.fold f m accu in
+ Int.Map.fold ff s accu
+
+ let for_all f s =
+ let ff _ m = Set.for_all f m in
+ Int.Map.for_all ff s
+
+ let exists f s =
+ let fe _ m = Set.exists f m in
+ Int.Map.exists fe s
+
+ let filter f s =
+ let ff m = Set.filter f m in
+ let s = Int.Map.map ff s in
+ Int.Map.filter (fun _ m -> not (Set.is_empty m)) s
+
+ let partition f s =
+ let fold h m (sl, sr) =
+ let (ml, mr) = Set.partition f m in
+ let sl = if Set.is_empty ml then sl else Int.Map.add h ml sl in
+ let sr = if Set.is_empty mr then sr else Int.Map.add h mr sr in
+ (sl, sr)
+ in
+ Int.Map.fold fold s (Int.Map.empty, Int.Map.empty)
+
+ let cardinal s =
+ let fold _ m accu = accu + Set.cardinal m in
+ Int.Map.fold fold s 0
+
+ let elements s =
+ let fold _ m accu = Set.fold (fun x accu -> x :: accu) m accu in
+ Int.Map.fold fold s []
+
+ let min_elt _ = assert false (** Cannot be implemented efficiently *)
+
+ let max_elt _ = assert false (** Cannot be implemented efficiently *)
+
+ let choose s =
+ let (_, m) = Int.Map.choose s in
+ Set.choose m
+
+ let split s x = assert false (** Cannot be implemented efficiently *)
+
+end
+
+module Make(M : HashedType) =
+struct
+ (** This module is essentially the same as SetMake, except that we have maps
+ instead of sets in the intmap. Invariants are the same. *)
+ module Set = SetMake(M)
+ module Map = CMap.Make(M)
+
+ type key = M.t
+
+ type 'a t = 'a Map.t Int.Map.t
+
+ let empty = Int.Map.empty
+
+ let is_empty = Int.Map.is_empty
+
+ let mem k s =
+ let h = M.hash k in
+ try
+ let m = Int.Map.find h s in
+ Map.mem k m
+ with Not_found -> false
+
+ let add k x s =
+ let h = M.hash k in
+ try
+ let m = Int.Map.find h s in
+ let m = Map.add k x m in
+ Int.Map.update h m s
+ with Not_found ->
+ let m = Map.singleton k x in
+ Int.Map.add h m s
+
+ let singleton k x =
+ let h = M.hash k in
+ Int.Map.singleton h (Map.singleton k x)
+
+ let remove k s =
+ let h = M.hash k in
+ try
+ let m = Int.Map.find h s in
+ let m = Map.remove k m in
+ if Map.is_empty m then
+ Int.Map.remove h s
+ else
+ Int.Map.update h m s
+ with Not_found -> s
+
+ let merge f s1 s2 =
+ let fm h m1 m2 = match m1, m2 with
+ | None, None -> None
+ | Some m, None ->
+ let m = Map.merge f m Map.empty in
+ if Map.is_empty m then None
+ else Some m
+ | None, Some m ->
+ let m = Map.merge f Map.empty m in
+ if Map.is_empty m then None
+ else Some m
+ | Some m1, Some m2 ->
+ let m = Map.merge f m1 m2 in
+ if Map.is_empty m then None
+ else Some m
+ in
+ Int.Map.merge fm s1 s2
+
+ let compare f s1 s2 =
+ let fc m1 m2 = Map.compare f m1 m2 in
+ Int.Map.compare fc s1 s2
+
+ let equal f s1 s2 =
+ let fe m1 m2 = Map.equal f m1 m2 in
+ Int.Map.equal fe s1 s2
+
+ let iter f s =
+ let fi _ m = Map.iter f m in
+ Int.Map.iter fi s
+
+ let fold f s accu =
+ let ff _ m accu = Map.fold f m accu in
+ Int.Map.fold ff s accu
+
+ let for_all f s =
+ let ff _ m = Map.for_all f m in
+ Int.Map.for_all ff s
+
+ let exists f s =
+ let fe _ m = Map.exists f m in
+ Int.Map.exists fe s
+
+ let filter f s =
+ let ff m = Map.filter f m in
+ let s = Int.Map.map ff s in
+ Int.Map.filter (fun _ m -> not (Map.is_empty m)) s
+
+ let partition f s =
+ let fold h m (sl, sr) =
+ let (ml, mr) = Map.partition f m in
+ let sl = if Map.is_empty ml then sl else Int.Map.add h ml sl in
+ let sr = if Map.is_empty mr then sr else Int.Map.add h mr sr in
+ (sl, sr)
+ in
+ Int.Map.fold fold s (Int.Map.empty, Int.Map.empty)
+
+ let cardinal s =
+ let fold _ m accu = accu + Map.cardinal m in
+ Int.Map.fold fold s 0
+
+ let bindings s =
+ let fold _ m accu = Map.fold (fun k x accu -> (k, x) :: accu) m accu in
+ Int.Map.fold fold s []
+
+ let min_binding _ = assert false (** Cannot be implemented efficiently *)
+
+ let max_binding _ = assert false (** Cannot be implemented efficiently *)
+
+ let fold_left _ _ _ = assert false (** Cannot be implemented efficiently *)
+
+ let fold_right _ _ _ = assert false (** Cannot be implemented efficiently *)
+
+ let choose s =
+ let (_, m) = Int.Map.choose s in
+ Map.choose m
+
+ let find k s =
+ let h = M.hash k in
+ let m = Int.Map.find h s in
+ Map.find k m
+
+ let split k s = assert false (** Cannot be implemented efficiently *)
+
+ let map f s =
+ let fs m = Map.map f m in
+ Int.Map.map fs s
+
+ let mapi f s =
+ let fs m = Map.mapi f m in
+ Int.Map.map fs s
+
+ let modify k f s =
+ let h = M.hash k in
+ let m = Int.Map.find h s in
+ let m = Map.modify k f m in
+ Int.Map.update h m s
+
+ let bind f s =
+ let fb m = Map.bind f m in
+ Int.Map.map fb s
+
+ let domain s = Int.Map.map Map.domain s
+
+ let update k x s =
+ let h = M.hash k in
+ let m = Int.Map.find h s in
+ let m = Map.update k x m in
+ Int.Map.update h m s
+
+ let smartmap f s =
+ let fs m = Map.smartmap f m in
+ Int.Map.smartmap fs s
+
+ let smartmapi f s =
+ let fs m = Map.smartmapi f m in
+ Int.Map.smartmap fs s
+
+ module Unsafe =
+ struct
+ let map f s =
+ let fs m = Map.Unsafe.map f m in
+ Int.Map.map fs s
+ end
+
+end
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 01:51:30 +0000