aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/option.ml11
-rw-r--r--lib/option.mli7
-rw-r--r--lib/util.ml5
-rw-r--r--lib/util.mli3
4 files changed, 18 insertions, 8 deletions
diff --git a/lib/option.ml b/lib/option.ml
index 96b9c70e88..0ed36b0026 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -29,6 +29,8 @@ let get = function
| Some y -> y
| _ -> raise IsNone
+(** [make x] returns [Some x]. *)
+let make x = Some x
(** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
let flatten = function
@@ -72,6 +74,15 @@ let fold_left f a = function
| Some y -> f a y
| _ -> a
+(** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w].
+ It is [a] if both [x] and [y] are [None]. Otherwise it raises
+ [Heterogeneous]. *)
+let fold_left2 f a x y =
+ match x,y with
+ | Some x, Some y -> f a x y
+ | None, None -> a
+ | _ -> raise Heterogeneous
+
(** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
let fold_right f x a =
match x with
diff --git a/lib/option.mli b/lib/option.mli
index 0a22697e75..f98c45ee72 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -25,6 +25,8 @@ exception IsNone
if [x] equals [None]. *)
val get : 'a option -> 'a
+(** [make x] returns [Some x]. *)
+val make : 'a -> 'a option
(** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
val flatten : 'a option option -> 'a option
@@ -53,6 +55,11 @@ val smartmap : ('a -> 'a) -> 'a option -> 'a option
(** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *)
val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b
+(** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w].
+ It is [a] if both [x] and [y] are [None]. Otherwise it raises
+ [Heterogeneous]. *)
+val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a
+
(** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
diff --git a/lib/util.ml b/lib/util.ml
index 389d0e1296..b61cd88ff6 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -788,15 +788,10 @@ let interval n m =
in
interval_n ([],m)
-let in_some x = Some x
-
let option_cons a l = match a with
| Some x -> x::l
| None -> l
-let option_fold_left2 f e a b = match (a,b) with
- | Some x, Some y -> f e x y
-
let option_compare f a b = match (a,b) with
| None, None -> true
| Some a', Some b' -> f a' b'
diff --git a/lib/util.mli b/lib/util.mli
index 0282f45f5b..71262bb4cd 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -223,10 +223,7 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list
val interval : int -> int -> int list
-val in_some : 'a -> 'a option
val option_cons : 'a option -> 'a list -> 'a list
-val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option ->
- 'c option -> 'a
val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool
val filter_some : 'a option list -> 'a list