From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- clib/option.mli | 147 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 clib/option.mli (limited to 'clib/option.mli') diff --git a/clib/option.mli b/clib/option.mli new file mode 100644 index 00000000..14fa9da3 --- /dev/null +++ b/clib/option.mli @@ -0,0 +1,147 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* bool + +(** 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]. + @raise IsNone if [x] equals [None]. *) +val get : 'a option -> 'a + +(** [make x] returns [Some x]. *) +val make : 'a -> 'a option + +(** [bind x f] is [f y] if [x] is [Some y] and [None] otherwise *) +val bind : 'a option -> ('a -> 'b option) -> 'b option + +(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *) +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"} *) + +(** [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]. + @raise 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_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]. + @raise Heterogeneous otherwise. *) +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 + +(** [fold_left_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *) +val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option + +(** Same as [fold_left_map] on the right *) +val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b option -> 'a -> 'c option * 'a + +(** @deprecated Same as [fold_left_map] *) +val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option +[@@ocaml.deprecated "Same as [fold_left_map]"] + +(** [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} *) + +(** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *) +val default : 'a -> 'a option -> 'a + +(** [lift] is the same as {!map}. *) +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 + + +(** {6 Operations with Lists} *) + +module List : sig + (** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *) + val cons : 'a option -> 'a list -> 'a list + + (** [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 + + (** [List.find f l] is the first [f a] different from [None], + scrolling through elements [a] of [l] in left-to-right order; + it is [None] if no such element exists. *) + val find : ('a -> 'b option) -> 'a list -> 'b option + + (** [List.map f [a1;...;an]] is the list [Some [b1;...;bn]] if + for all i, there is a [bi] such that [f ai] is [Some bi]; it is + [None] if, for at least one i, [f ai] is [None]. *) + val map : ('a -> 'b option) -> 'a list -> 'b list option + +end -- cgit v1.2.3