diff options
Diffstat (limited to 'clib')
| -rw-r--r-- | clib/cSig.mli | 1 | ||||
| -rw-r--r-- | clib/hMap.ml | 6 | ||||
| -rw-r--r-- | clib/int.ml | 7 |
3 files changed, 14 insertions, 0 deletions
diff --git a/clib/cSig.mli b/clib/cSig.mli index fb36cc5b51..859018ca4b 100644 --- a/clib/cSig.mli +++ b/clib/cSig.mli @@ -83,6 +83,7 @@ sig val choose: 'a t -> (key * 'a) val split: key -> 'a t -> 'a t * 'a option * 'a t val find: key -> 'a t -> 'a + val find_opt : key -> 'a t -> 'a option val map: ('a -> 'b) -> 'a t -> 'b t val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t end diff --git a/clib/hMap.ml b/clib/hMap.ml index 9c80398e4d..5d634b7af0 100644 --- a/clib/hMap.ml +++ b/clib/hMap.ml @@ -353,6 +353,12 @@ struct let m = Int.Map.find h s in Map.find k m + let find_opt k s = + let h = M.hash k in + match Int.Map.find_opt h s with + | None -> None + | Some m -> Map.find_opt k m + let get k s = try find k s with Not_found -> assert false let split k s = assert false (** Cannot be implemented efficiently *) diff --git a/clib/int.ml b/clib/int.ml index fa21379565..3924c152d6 100644 --- a/clib/int.ml +++ b/clib/int.ml @@ -41,6 +41,13 @@ struct if i < k then find i l else if i = k then v else find i r + + let rec find_opt i s = match map_prj s with + | MEmpty -> None + | MNode (l, k, v, r, h) -> + if i < k then find_opt i l + else if i = k then Some v + else find_opt i r end module List = struct |