Plus de combinateurs sont passés de Util à Option. Le module Options

devient Flags.




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

7 files changed, 50 insertions, 18 deletions

diff --git a/lib/options.ml b/lib/flags.ml
index 589069567..12b2ed037 100644
--- a/lib/options.ml
+++ b/lib/flags.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: options.ml 10106 2007-08-30 16:56:10Z herbelin $ *)
 
 open Util
 
@@ -100,13 +100,13 @@ let dump_it () =
 
 let _ = at_exit dump_it
 
-(* Options for the virtual machine *)
+(* Flags.for the virtual machine *)
 
 let boxed_definitions = ref true
 let set_boxed_definitions b = boxed_definitions := b
 let boxed_definitions _ = !boxed_definitions 
  
-(* Options for external tools *)
+(* Flags.for external tools *)
 
 let browser_cmd_fmt =
  try
diff --git a/lib/options.mli b/lib/flags.mli
index 73962735d..248b59b0d 100644
--- a/lib/options.mli
+++ b/lib/flags.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: options.mli 9679 2007-02-24 15:22:07Z herbelin $ i*)
 
 (* Global options of the system. *)
 
diff --git a/lib/option.ml b/lib/option.ml
index 0ed36b002..436358b55 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -32,6 +32,14 @@ let get = function
 (** [make x] returns [Some x]. *)
 let make x = Some x
 
+(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
+let init b x =
+  if b then 
+    Some x
+  else
+    None
+    
+
 (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
 let flatten = function
   | Some (Some y) -> Some y
@@ -120,3 +128,22 @@ let lift2 f x y =
   match x,y with
   | Some z, Some w -> Some (f z w)
   | _,_ -> None
+
+
+
+(** {6 Operations with Lists} *)
+
+module List =
+ struct 
+  (** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *)
+  let cons x l =
+    match x with
+    | Some y -> y::l
+    | _ -> l
+ 
+  (** [List.flatten l] is the list of all the [y]s such that [l] contains
+      [Some y] (in the same order). *)
+  let rec flatten = function
+    | x::l -> cons x (flatten l)
+    | [] -> [] 
+end
diff --git a/lib/option.mli b/lib/option.mli
index f98c45ee7..8e768d8af 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -28,6 +28,9 @@ 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
 
@@ -64,7 +67,7 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a
 val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
 
 
-(** {6 More Specific operations} ***)
+(** {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
@@ -83,3 +86,15 @@ 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
+end
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 415a3002a..067c52700 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -11,10 +11,10 @@
 open Pp_control
 
 (* This should not be used outside of this file. Use
-   Options.print_emacs instead. This one is updated when reading
+   Flags.print_emacs instead. This one is updated when reading
    command line options. This was the only way to make [Pp] depend on
-   an option without creating a circularity: [Options] -> [Util] ->
-   [Pp] -> [Options] *)
+   an option without creating a circularity: [Flags. -> [Util] ->
+   [Pp] -> [Flags. *)
 let print_emacs = ref false
 let make_pp_emacs() = print_emacs:=true
 let make_pp_nonemacs() = print_emacs:=false
diff --git a/lib/util.ml b/lib/util.ml
index b61cd88ff..99a203d52 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -788,19 +788,11 @@ let interval n m =
   in 
   interval_n ([],m)
 
-let option_cons a l = match a with
-  | Some x -> x::l
-  | None -> l
-
 let option_compare f a b = match (a,b) with
   | None, None -> true
   | Some a', Some b' -> f a' b'
   | _ -> failwith "option_compare"
 
-let rec filter_some = function
-  | [] -> []
-  | None::l -> filter_some l
-  | Some a::l -> a :: filter_some l
 
 let map_succeed f = 
   let rec map_f = function 
diff --git a/lib/util.mli b/lib/util.mli
index 71262bb4c..331363f0a 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -223,9 +223,7 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list
 
 val interval : int -> int -> int list
 
-val option_cons : 'a option -> 'a list -> 'a list
 val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool 
-val filter_some : 'a option list -> 'a list
 
 (* In [map_succeed f l] an element [a] is removed if [f a] raises *)
 (* [Failure _] otherwise behaves as [List.map f l] *)