Factorisation des opérations sur le type option de Util dans un module

lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting 
des fonctions (à un ou deux arguments tous ou partie de type option).

Il reste quelques opérations dans Util à propos desquelles je ne suis 
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain 
car il est tard (comme some_in qui devrait devenir Option.make je 
suppose) . Elles s'expriment souvent facilement en fonction des 
autres, par exemple "option_compare x y"  est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est 
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.

J'en ai profité aussi pour remplacer les trop nombreux "failwith" par 
des erreurs locales au module, donc plus robustes.

J'ai trouvé aussi une fonction qui était définie deux fois, et une 
définie dans un module particulier.

Mon seul bémol (mais facile à traiter) c'est la proximité entre le 
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de 
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7

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 *)