diff options
Diffstat (limited to 'lib/option.mli')
| -rw-r--r-- | lib/option.mli | 39 |
1 files changed, 25 insertions, 14 deletions
diff --git a/lib/option.mli b/lib/option.mli index 121d6500..d9ad0e11 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,11 +13,26 @@ they actually are similar considering ['a option] as a type of lists with at most one element. *) +exception IsNone + (** [has_some x] is [true] if [x] is of the form [Some y] and [false] otherwise. *) val has_some : 'a option -> bool -exception IsNone +(** Negation of [has_some] *) +val is_empty : 'a option -> bool + +(** [equal f x y] lifts the equality predicate [f] to + option types. That is, if both [x] and [y] are [None] then + it returns [true], if they are both [Some _] then + [f] is called. Otherwise it returns [false]. *) +val equal : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool + +(** Same as [equal], but with comparison. *) +val compare : ('a -> 'a -> int) -> 'a option -> 'a option -> int + +(** Lift a hash to option types. *) +val hash : ('a -> int) -> 'a option -> int (** [get x] returns [y] where [x] is [Some y]. It raises IsNone if [x] equals [None]. *) @@ -32,6 +47,12 @@ val init : bool -> 'a -> 'a option (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) val flatten : 'a option option -> 'a option +(** [append x y] is the first element of the concatenation of [x] and + [y] seen as lists. In other words, [append (Some a) y] is [Some + a], [append None (Some b)] is [Some b], and [append None None] is + [None]. *) +val append : 'a option -> 'a option -> 'a option + (** {6 "Iterators"} ***) @@ -67,7 +88,7 @@ val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b (** [fold_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *) val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option -(** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *) +(** [cata f e x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *) val cata : ('a -> 'b) -> 'b -> 'a option -> 'b (** {6 More Specific Operations} ***) @@ -100,16 +121,6 @@ module List : sig (** [List.flatten l] is the list of all the [y]s such that [l] contains [Some y] (in the same order). *) val flatten : 'a option list -> 'a list -end - -(** {6 Miscelaneous Primitives} *) - -module Misc : sig - (** [Misc.compare f x y] lifts the equality predicate [f] to - option types. That is, if both [x] and [y] are [None] then - it returns [true], if they are bothe [Some _] then - [f] is called. Otherwise it returns [false]. *) - val compare : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool + val find : ('a -> 'b option) -> 'a list -> 'b option end - |