Merge PR #9237: Add Map.find_opt

4 files changed, 25 insertions, 11 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
diff --git a/engine/evd.ml b/engine/evd.ml
index 7bc3be87a4..31c326df6a 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -601,19 +601,19 @@ let is_defined d e = EvMap.mem e d.defn_evars
 
 let is_undefined d e = EvMap.mem e d.undf_evars
 
-let existential_value d (n, args) =
-  let info = find d n in
-  match evar_body info with
-  | Evar_defined c ->
-    instantiate_evar_array info c args
-  | Evar_empty ->
-    raise NotInstantiatedEvar
+let existential_opt_value d (n, args) =
+  match EvMap.find_opt n d.defn_evars with
+  | None -> None
+  | Some info ->
+    match evar_body info with
+    | Evar_defined c -> Some (instantiate_evar_array info c args)
+    | Evar_empty -> None (* impossible but w/e *)
 
-let existential_value0 = existential_value
+let existential_value d ev = match existential_opt_value d ev with
+  | None -> raise NotInstantiatedEvar
+  | Some v -> v
 
-let existential_opt_value d ev =
-  try Some (existential_value d ev)
-  with NotInstantiatedEvar -> None
+let existential_value0 = existential_value
 
 let existential_opt_value0 = existential_opt_value