← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to lib/option.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
lib/option.mli
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: option.mli 11576 2008-11-10 19:13:15Z msozeau $ *)
 
10
 
 
11
(** Module implementing basic combinators for OCaml option type.
 
12
   It tries follow closely the style of OCaml standard library.
 
13
 
 
14
   Actually, some operations have the same name as [List] ones:
 
15
   they actually are similar considering ['a option] as a type
 
16
   of lists with at most one element. *)
 
17
 
 
18
(** [has_some x] is [true] if [x] is of the form [Some y] and [false]
 
19
    otherwise.  *)
 
20
val has_some : 'a option -> bool
 
21
  
 
22
exception IsNone
 
23
 
 
24
(** [get x] returns [y] where [x] is [Some y]. It raises IsNone
 
25
    if [x] equals [None]. *)
 
26
val get : 'a option -> 'a
 
27
 
 
28
(** [make x] returns [Some x]. *)
 
29
val make : 'a -> 'a option
 
30
 
 
31
(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
 
32
val init : bool -> 'a -> 'a option
 
33
 
 
34
(** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
 
35
val flatten : 'a option option -> 'a option
 
36
 
 
37
 
 
38
(** {6 "Iterators"} ***)
 
39
 
 
40
(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing 
 
41
    otherwise. *)
 
42
val iter : ('a -> unit) -> 'a option -> unit
 
43
 
 
44
exception Heterogeneous
 
45
 
 
46
(** [iter2 f x y] executes [f z w] if [x] equals [Some z] and [y] equals
 
47
    [Some w]. It does nothing if both [x] and [y] are [None]. And raises
 
48
    [Heterogeneous] otherwise. *)
 
49
val iter2 : ('a -> 'b -> unit) -> 'a option -> 'b option -> unit
 
50
 
 
51
(** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *)
 
52
val map : ('a -> 'b) -> 'a option -> 'b option
 
53
 
 
54
(** [smartmap f x] does the same as [map f x] except that it tries to share
 
55
    some memory. *)
 
56
val smartmap : ('a -> 'a) -> 'a option -> 'a option
 
57
 
 
58
(** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *)
 
59
val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b
 
60
 
 
61
(** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w].
 
62
    It is [a] if both [x] and [y] are [None]. Otherwise it raises
 
63
    [Heterogeneous]. *)
 
64
val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a
 
65
 
 
66
(** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
 
67
val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
 
68
 
 
69
(** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *)
 
70
val cata : ('a -> 'b) -> 'b -> 'a option -> 'b
 
71
 
 
72
(** {6 More Specific Operations} ***)
 
73
 
 
74
(** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *)
 
75
val default : 'a -> 'a option -> 'a
 
76
 
 
77
(** [lift] is the same as {!map}. *)
 
78
val lift : ('a -> 'b) -> 'a option -> 'b option
 
79
 
 
80
(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and 
 
81
    [None] otherwise. *)
 
82
val lift_right : ('a -> 'b -> 'c) -> 'a -> 'b option -> 'c option
 
83
 
 
84
(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and 
 
85
    [None] otherwise. *)
 
86
val lift_left : ('a -> 'b -> 'c) -> 'a option -> 'b -> 'c option
 
87
 
 
88
(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals 
 
89
    [Some w]. It is [None] otherwise. *)
 
90
val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option
 
91
 
 
92
 
 
93
(** {6 Operations with Lists} *)
 
94
 
 
95
module List : sig
 
96
  (** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *)
 
97
  val cons : 'a option -> 'a list -> 'a list
 
98
 
 
99
  (** [List.flatten l] is the list of all the [y]s such that [l] contains
 
100
      [Some y] (in the same order). *)
 
101
  val flatten : 'a option list -> 'a list
 
102
end
 
103
 
 
104
 
 
105
(** {6 Miscelaneous Primitives} *)
 
106
 
 
107
module Misc : sig
 
108
  (** [Misc.compare f x y] lifts the equality predicate [f] to 
 
109
      option types. That is, if both [x] and [y] are [None] then 
 
110
      it returns [true], if they are bothe [Some _] then
 
111
      [f] is called. Otherwise it returns [false]. *)
 
112
   val compare : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool
 
113
end
 
114