1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** 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. *)
exception IsNone
(** [has_some x] is [true] if [x] is of the form [Some y] and [false]
otherwise. *)
val has_some : 'a option -> 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
(** [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_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 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
|
