diff --git a/infer/src/backend/iList.ml b/infer/src/backend/iList.ml index 9a73db16a..1a3a1b90a 100644 --- a/infer/src/backend/iList.ml +++ b/infer/src/backend/iList.ml @@ -175,6 +175,15 @@ let map2 f l1 l2 = | _ -> raise Fail in go l1 l2 [] +(** Return the first non-None result found when applying f to elements of l *) +let rec find_map_opt f = function + | [] -> None + | e :: l' -> + let e' = f e in + if e' <> None + then e' + else find_map_opt f l' + let to_string f l = let rec aux l = match l with diff --git a/infer/src/backend/iList.mli b/infer/src/backend/iList.mli index 6d7a240c1..255cbfd16 100644 --- a/infer/src/backend/iList.mli +++ b/infer/src/backend/iList.mli @@ -97,4 +97,7 @@ exception Fail (** Apply [f] to pairs of elements; raise [Fail] if the two lists have different lenghts. *) val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list +(** Return the first non-None result found when applying f to elements of l *) +val find_map_opt : ('a -> 'b option) -> 'a list -> 'b option + val to_string : ('a -> string) -> 'a list -> string