diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/option.ml | 111 | ||||
| -rw-r--r-- | lib/option.mli | 78 | ||||
| -rw-r--r-- | lib/util.ml | 25 | ||||
| -rw-r--r-- | lib/util.mli | 6 |
4 files changed, 189 insertions, 31 deletions
diff --git a/lib/option.ml b/lib/option.ml new file mode 100644 index 0000000000..96b9c70e88 --- /dev/null +++ b/lib/option.ml @@ -0,0 +1,111 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(** Module implementing basic combinators for OCaml option type. + It tries follow closely the style of OCaml standard library. + + Actually, some operations have the same name as [List] ones: + they actually are similar considering ['a option] as a type + of lists with at most one element. *) + +(** [has_some x] is [true] if [x] is of the form [Some y] and [false] + otherwise. *) +let has_some = function + | None -> false + | _ -> true + +exception IsNone + +(** [get x] returns [y] where [x] is [Some y]. It raises IsNone + if [x] equals [None]. *) +let get = function + | Some y -> y + | _ -> raise IsNone + + +(** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) +let flatten = function + | Some (Some y) -> Some y + | _ -> None + + +(** {6 "Iterators"} ***) + +(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing + otherwise. *) +let iter f = function + | Some y -> f y + | _ -> () + + +exception Heterogeneous + +(** [iter2 f x y] executes [f z w] if [x] equals [Some z] and [y] equals + [Some w]. It does nothing if both [x] and [y] are [None]. And raises + [Heterogeneous] otherwise. *) +let iter2 f x y = + match x,y with + | Some z, Some w -> f z w + | None,None -> () + | _,_ -> raise Heterogeneous + +(** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *) +let map f = function + | Some y -> Some (f y) + | _ -> None + +(** [smartmap f x] does the same as [map f x] except that it tries to share + some memory. *) +let smartmap f = function + | Some y as x -> let y' = f y in if y' == y then x else Some y' + | _ -> None + +(** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *) +let fold_left f a = function + | Some y -> f a y + | _ -> a + +(** [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 + | Some y -> f y a + | _ -> a + + +(** {6 More Specific operations} ***) + +(** [default f x a] is [f y] if [x] is [Some y] and [a] otherwise. *) +let default f x a = + match x with + | Some y -> f y + | _ -> a + +(** [lift f x] is the same as [map f x]. *) +let lift = map + +(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and + [None] otherwise. *) +let lift_right f a = function + | Some y -> Some (f a y) + | _ -> None + +(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and + [None] otherwise. *) +let lift_left f x a = + match x with + | Some y -> Some (f y a) + | _ -> None + +(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals + [Some w]. It is [None] otherwise. *) +let lift2 f x y = + match x,y with + | Some z, Some w -> Some (f z w) + | _,_ -> None diff --git a/lib/option.mli b/lib/option.mli new file mode 100644 index 0000000000..0a22697e75 --- /dev/null +++ b/lib/option.mli @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(** Module implementing basic combinators for OCaml option type. + It tries follow closely the style of OCaml standard library. + + Actually, some operations have the same name as [List] ones: + they actually are similar considering ['a option] as a type + of lists with at most one element. *) + +(** [has_some x] is [true] if [x] is of the form [Some y] and [false] + otherwise. *) +val has_some : 'a option -> bool + +exception IsNone + +(** [get x] returns [y] where [x] is [Some y]. It raises IsNone + if [x] equals [None]. *) +val get : 'a option -> 'a + + +(** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) +val flatten : 'a option option -> 'a option + + +(** {6 "Iterators"} ***) + +(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing + otherwise. *) +val iter : ('a -> unit) -> 'a option -> unit + +exception Heterogeneous + +(** [iter2 f x y] executes [f z w] if [x] equals [Some z] and [y] equals + [Some w]. It does nothing if both [x] and [y] are [None]. And raises + [Heterogeneous] otherwise. *) +val iter2 : ('a -> 'b -> unit) -> 'a option -> 'b option -> unit + +(** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *) +val map : ('a -> 'b) -> 'a option -> 'b option + +(** [smartmap f x] does the same as [map f x] except that it tries to share + some memory. *) +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_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 + + +(** {6 More Specific operations} ***) + +(** [default f x a] is [f y] if [x] is [Some y] and [a] otherwise. *) +val default : ('a -> 'b) -> 'a option -> 'b -> 'b + +(** [lift f x] is the same as [map f x]. *) +val lift : ('a -> 'b) -> 'a option -> 'b option + +(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and + [None] otherwise. *) +val lift_right : ('a -> 'b -> 'c) -> 'a -> 'b option -> 'c option + +(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and + [None] otherwise. *) +val lift_left : ('a -> 'b -> 'c) -> 'a option -> 'b -> 'c option + +(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals + [Some w]. It is [None] otherwise. *) +val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option diff --git a/lib/util.ml b/lib/util.ml index 3b5c90b020..389d0e1296 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -790,43 +790,18 @@ let interval n m = let in_some x = Some x -let out_some = function - | Some x -> x - | None -> failwith "out_some" - -let option_map f = function - | None -> None - | Some x -> Some (f 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 - | _ -> e - -let option_fold_left f e a = match a with - | Some x -> f e x - | _ -> e - -let option_fold_right f a e = match a with - | Some x -> f x e - | _ -> e let option_compare f a b = match (a,b) with | None, None -> true | Some a', Some b' -> f a' b' | _ -> failwith "option_compare" -let option_iter f = function - | None -> () - | Some x -> f x - -let option_smartmap f a = match a with - | None -> a - | Some x -> let x' = f x in if x'==x then a else Some x' - let rec filter_some = function | [] -> [] | None::l -> filter_some l diff --git a/lib/util.mli b/lib/util.mli index 5e89788b9b..0282f45f5b 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -224,16 +224,10 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list val interval : int -> int -> int list val in_some : 'a -> 'a option -val out_some : 'a option -> 'a -val option_map : ('a -> 'b) -> 'a option -> 'b option val option_cons : 'a option -> 'a list -> 'a list -val option_fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b -val option_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b option -> 'a val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a -val option_iter : ('a -> unit) -> 'a option -> unit val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool -val option_smartmap : ('a -> 'a) -> 'a option -> 'a option val filter_some : 'a option list -> 'a list (* In [map_succeed f l] an element [a] is removed if [f a] raises *) |